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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MemoryInterface.tla
---
---------------------------- MODULE MemoryInterface ----------------------------
VARIABLE memInt
CONSTANTS Send(_, _, _, _) ,
    Reply(_, _, _, _) ,
    InitMemInt,
    Proc,
    Adr,
    Val

(***************************************************************************)
(* We comment out the assumption because TLC cannot handle unbounded       *)
(* quantifiers.                                                            *)
(***************************************************************************)
\* ASSUME \A p, d, miOld, miNew : 
\*         /\ Send(p,d,miOld,miNew)  \in BOOLEAN
\*         /\ Reply(p,d,miOld,miNew) \in BOOLEAN  

--------------------------------------------------------------------------------
MReq == [op: {"Rd"}, adr: Adr]
\union [op: {"Wr"}, adr: Adr, val: Val]

NoVal == CHOOSE v: v \notin Val
================================================================================