minor

lbinria · Sep 4, 2023 · 50569a1 · 50569a1
1 parent cd44416
commit 50569a1
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 23 deletions.
diff --git a/spec/TraceSpec.tla b/spec/TraceSpec.tla
@@ -7,7 +7,6 @@ ASSUME TLCGet("config").mode = "bfs"
 
 VARIABLES l
 
-
 (* Operators to override *)
 Vars == Print(<<"Trace spec isn't valid, you should override 'Vars'.">>, <<>>)
 BaseInit == Print(<<"Trace spec isn't valid, you should override 'BaseInit'.">>, Nil)
@@ -33,8 +32,6 @@ Trace ==
 logline ==
  Trace[l]
 
-
-
 IsEvent(e) ==
  \* Equals FALSE if we get past the end of the log, causing model checking to stop.
  /\ l \in 1..Len(Trace)

diff --git a/spec/tictac.tla b/spec/tictac.tla
@@ -3,11 +3,6 @@ EXTENDS Naturals, FiniteSets, Sequences, TLC
 
 \*CONSTANTS test
 
-\* A reserved value.
-CONSTANTS Nil
-
-----
-
 VARIABLE hour, minute
 
 vars == <<hour, minute>>
@@ -16,11 +11,6 @@ Init ==
  /\ hour \in 0..23
  /\ minute \in 0..59
 
-(* Invariant *)
-TypeInv ==
- /\ hour \in 0..23
- /\ minute \in 0..59
-
 Tick ==
  IF minute >= 59 THEN
  /\ minute' = 0
@@ -35,7 +25,11 @@ Tick ==
 
 Next == Tick
 
-
 Spec == Init /\ [][Next]_vars
 
+(* Invariant *)
+TypeInv ==
+ /\ hour \in 0..23
+ /\ minute \in 0..59
+
 ===============================================================================
diff --git a/spec/tictacTrace.cfg b/spec/tictacTrace.cfg
@@ -5,8 +5,8 @@ CONSTANTS
  (* Set variables of TraceSpec module *)
  Vars <- vars
  BaseInit <- Init
- MapVariables <- MapVariablesImpl
  TraceNext <- TraceNextImpl
+ MapVariables <- MapVariablesImpl
 
 SPECIFICATION
  TraceSpec

diff --git a/spec/tictacTrace.tla b/spec/tictacTrace.tla
@@ -1,11 +1,11 @@
 --------------------------- MODULE tictacTrace ---------------------------
 (***************************************************************************)
-(* Simplified specification of 2PC *)
+(* clock *)
 (***************************************************************************)
 
-EXTENDS TLC, Sequences, SequencesExt, Naturals, FiniteSets, Bags, Json, IOUtils, tictac, TVOperators, TraceSpec
+EXTENDS TLC, Sequences, SequencesExt, Naturals, FiniteSets, Bags, Json, IOUtils, tictac, TraceSpec
 
-(* Override CONSTANTS *)
+(* Override CONSTANTS from the original spec *)
 
 (* Replace Nil constant *)
 TraceNil == "null"
@@ -14,11 +14,12 @@ TraceNil == "null"
 \*TraceServer ==
 \* ToSet(JsonTrace[1].Server)
 
-(* Can be extracted from init *)
+(* Can be extracted from Init in original spec*)
 DefaultImpl(varName) ==
  CASE varName = "hour" -> 0..23
  [] varName = "minute" -> 0..59
 
+(* Can be extracted from vars in original spec*)
 MapVariablesImpl(t) ==
  /\
  IF "hour" \in DOMAIN t
@@ -29,18 +30,16 @@ MapVariablesImpl(t) ==
  THEN minute' = MapVariable(minute, "minute", t)
  ELSE TRUE
 
-
-
 IsTick ==
  /\ IsEvent("Tick")
  /\ Tick
 
-
 TraceNextImpl ==
  \/ IsTick
 
+(* if we want to compose actions *)
 ComposedNext == FALSE
 
 BaseSpec == Init /\ [][Next \/ ComposedNext]_vars
 -----------------------------------------------------------------------------
-=============================================================================
+=============================================================================