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

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/HourClock2.tla
---
------------------------------ MODULE HourClock2 -------------------------------
(***************************************************************************)
(* This module contains the definition of the specification HC2 from the   *)
(* book.                                                                   *)
(***************************************************************************)

EXTENDS HourClock
(*************************************************************************)
  (* This statement includes in the current module all the definitions and *)
  (* declarations from module HourClock, including the definitions of +    *)
  (* and % from the Naturals module and the declaration of the variable    *)
  (* hr.                                                                   *)
  (*************************************************************************)

HCnxt2 == hr' = (hr % 12) + 1
HC2 == HCini /\ [][HCnxt2]_hr
--------------------------------------------------------------------------------
THEOREM HC <=> HC2
(*************************************************************************)
  (* This theorem asserts that formulas HC and HC2 are equivalent.  The    *)
  (* symbol <=> , which can also be typed as \equiv , is typeset as an     *)
  (* equivalence symbole (a three-lined equals sign).                      *)
  (*************************************************************************)
================================================================================