libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/TCommit.tla
---
-------------------------------- MODULE TCommit --------------------------------
CONSTANT RM       \* The set of participating resource managers
VARIABLE rmState  \* `rmState[rm]' is the state of resource manager rm.
--------------------------------------------------------------------------------
TCTypeOK ==
    (*************************************************************************)
  (* The type-correctness invariant                                        *)
  (*************************************************************************)
    rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]

TCInit == rmState = [rm \in RM |-> "working"]
(*************************************************************************)
  (* The initial predicate.                                                *)
  (*************************************************************************)

canCommit == \A rm \in RM: rmState[rm] \in {"prepared", "committed"}
(*************************************************************************)
  (* True iff all RMs are in the "prepared" or "committed" state.          *)
  (*************************************************************************)

notCommitted == \A rm \in RM: rmState[rm] /= "committed"
(*************************************************************************)
  (* True iff neither no resource manager has decided to commit.           *)
  (*************************************************************************)
--------------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the RMs, and then    *)
(* define the complete next-state action of the specification to be the    *)
(* disjunction of the possible RM actions.                                 *)
(***************************************************************************)
Prepare(rm) ==
    /\ rmState[rm] = "working"
    /\ rmState' = [rmState EXCEPT ![rm] = "prepared"]

Decide(rm) ==
    \/
        /\ rmState[rm] = "prepared"
        /\ canCommit
        /\ rmState' = [rmState EXCEPT ![rm] = "committed"]
    \/
        /\ rmState[rm] \in {"working", "prepared"}
        /\ notCommitted
        /\ rmState' = [rmState EXCEPT ![rm] = "aborted"]

TCNext == \E rm \in RM: Prepare(rm) \/ Decide(rm)
(*************************************************************************)
  (* The next-state action.                                                *)
  (*************************************************************************)
--------------------------------------------------------------------------------
TCSpec == TCInit /\ [][TCNext]_rmState
(*************************************************************************)
  (* The complete specification of the protocol.                           *)
  (*************************************************************************)
--------------------------------------------------------------------------------
(***************************************************************************)
(* We now assert invariance properties of the specification.               *)
(***************************************************************************)
TCConsistent ==
    (*************************************************************************)
  (* A state predicate asserting that two RMs have not arrived at          *)
  (* conflicting decisions.                                                *)
  (*************************************************************************)
    \A rm1, rm2 \in RM: ~
        /\ rmState[rm1] = "aborted"
        /\ rmState[rm2] = "committed"

THEOREM TCSpec => [](TCTypeOK /\ TCConsistent)
(*************************************************************************)
  (* Asserts that TCTypeOK and TCConsistent are invariants of the protocol. *)
  (*************************************************************************)
================================================================================