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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/LiveHourClock.tla
---
----------------------------- MODULE LiveHourClock -----------------------------
(***************************************************************************)
(* This module adds the liveness condition to the hour clock specification *)
(* of module HourClock.                                                    *)
(***************************************************************************)

EXTENDS HourClock

LSpec == HC /\ WF_hr(HCnxt)
(*************************************************************************)
  (* The specification with the liveness condition conjoined.              *)
  (*************************************************************************)

(***************************************************************************)
(* We now define some properties that LSpec satisfies.                     *)
(***************************************************************************)
AlwaysTick == []<> <<HCnxt>>_hr
(*************************************************************************)
  (* Asserts that infinitely many <<HCnxt>>_hr steps occur.                *)
  (*************************************************************************)

AllTimes == \A n \in 1..12: []<>(hr = n)
(*************************************************************************)
  (* Asserts that, for each time n in 1..12, hr infinitely often equals n. *)
  (*************************************************************************)

TypeInvariance == []HCini
(*************************************************************************)
  (* The temporal formula asserting that HCini is always true.  It is      *)
  (* stated in this way to show you another way of telling TLC to check an *)
  (* invariant.                                                            *)
  (*************************************************************************)

--------------------------------------------------------------------------------
THEOREM LSpec => AlwaysTick /\ AllTimes /\ TypeInvariance
================================================================================