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

--------------------------- MODULE MCInnerSerial ----------------------------
(***************************************************************************)
(* This is a module to test the InnerSerial specification.                 *)
(***************************************************************************)

EXTENDS InnerSerial \* , TLC

CONSTANT MaxQLen
    (***********************************************************************)
    (* To bound the state space, we constrain the length of opQ[p] to be   *)
    (* at most MaxQLen, for all p.                                         *)
    (***********************************************************************)

MCNat == 0 .. MaxQLen 
  (*************************************************************************)
  (* The liveness condition contains quantification over the set           *)
  (*                                                                       *)
  (*       [proc : Proc, idx : Nat]                                        *)
  (*                                                                       *)
  (* However, it suffices that the quantification be over all possible     *)
  (* elements of opId, and hence for idx at most MaxQLen.  We therefore    *)
  (* have TLC substitute MCNat for Nat.                                    *)
  (*************************************************************************)

MCInitMem == [adr \in Adr |-> CHOOSE v \in Val  : TRUE]
  (*************************************************************************)
  (* We have to tell TLC what value to use for the constant parameter      *)
  (* InitMem.  We let it use MCInitMem, an arbitrary choice.               *)
  (*************************************************************************)
  
Constraint == \A p \in Proc : Len(opQ[p]) \leq MaxQLen
  (*************************************************************************)
  (* The constraint used to bound the size of the state space.             *)
  (*************************************************************************)
  
AlwaysResponds == 
  (*************************************************************************)
  (* Some simple liveness properties, implied by the fact that every       *)
  (* request eventually generates a response.                              *)
  (*************************************************************************)
  /\ \A p \in Proc, r \in Reg :
       (regFile[p][r].op # "Free") ~> (regFile[p][r].op = "Free")
  /\ \A oi \in [proc : Proc, idx : Nat] :
         (oi \in opId) ~> (oi \in opId /\ opIdQ(oi).reg = Done)

=============================================================================