Integrating types 4: migrated tests to Snowcat

UNRELEASED.md

@@ -13,12 +13,17 @@
 
 ### Features
 
+* Model checker: receiving the types from with the type checker Snowcat, see #668 and #350
+* Type checker: the old Apalache type annotations are no longer supported, see #668
 * Type checker: tagging all expressions with the reconstructed types, see #608
-* Type checker: experimental option `check --with-snowcat`, see #632
+* Type checker: handling TLA+ labels like `lab("a", "b") :: e`, see #653
+* Preprocessing: handling the general case of EXCEPT, see #647
 
 ### Changed
 
 * Preprocessing: massive refactoring of the passes to support types. This may have introduced unexpected bugs.
+* Model checker: translation rules for records and functions have been modified, in order to support new types. Bugs to
+  be expected.
 
 ### Known issues
 

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -170,7 +170,7 @@ object Tool extends App with LazyLogging {
     executor.options.set("checker.noDeadlocks", check.noDeadlocks)
     executor.options.set("checker.algo", check.algo)
     // this option enables the new type checker in the pipeline
-    executor.options.set("typechecker.snowcatOn", check.withSnowcat)
+    executor.options.set("typechecker.snowcatOn", true)
     // for now, enable polymorphic types. We probably want to disable this option for the type checker
     executor.options.set("typechecker.inferPoly", true)
 

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -42,6 +42,4 @@ class CheckCmd extends Command(name = "check", description = "Check a TLA+ speci
         "pre-check, whether a transition is disabled, and discard it, to make SMT queries smaller, default: true")
   var noDeadlocks: Boolean =
     opt[Boolean](name = "no-deadlock", default = true, description = "do not check for deadlocks, default: true")
-  var withSnowcat: Boolean =
-    opt[Boolean](name = "with-snowcat", default = false, description = "use the new type checker Snowcat")
 }

test/tla/Assignments20200309.tla

@@ -1,5 +1,8 @@
 ----- MODULE Assignments20200309 -----
-VARIABLE a
+VARIABLE
+    \* @type: Int;
+    a
+
 \* this specification fails, as it has no expression
 \* that can be treated as an assignment
 Init == TRUE

test/tla/Bug20190118.tla

@@ -5,8 +5,6 @@
 (* BMCMT extensions *)
 RM == {"r1", "r2"}
 
-a <: b == a \* a type annotation
-
 \* new: a message type
 MT == [type |-> STRING, rm |-> STRING]
 (* END OF BMCMT extensions *)
@@ -23,19 +21,19 @@ VARIABLES
 Message ==
   {[type |-> t, rm |-> r]: t \in {"Prepared"}, r \in RM }
     \cup
-  {([type |-> t] <: MT) : t \in {"Commit", "Abort"} }
+  {[type |-> t] : t \in {"Commit", "Abort"} }
 
 Init ==  
   /\ rmState \in [RM -> {"working", "prepared"}]
   /\ msgs \in SUBSET Message \* this is a problematic statement
   /\ rmState["r1"] = "working"
   /\ rmState["r2"] = "prepared"
   /\ tmPrepared = {"r2"}
-  /\ msgs = {[type |-> "Prepared", rm |-> "r2"] <: MT}
+  /\ msgs = {[type |-> "Prepared", rm |-> "r2"]}
 
 TMCommit ==
   /\ tmPrepared = RM
-  /\ msgs' = msgs \cup {[type |-> "Commit"] <: MT}
+  /\ msgs' = msgs \cup {[type |-> "Commit"]}
   /\ UNCHANGED <<rmState, tmPrepared>>
 
 RMPrepare(rm) == 
@@ -47,6 +45,6 @@ RMPrepare(rm) ==
 Next == TMCommit \/ RMPrepare("r1")
 -----------------------------------------------------------------------------
 \* this invariant cannot be violated in one step
-Inv == ([type |-> "Commit"] <: MT) \notin msgs
+Inv == [type |-> "Commit"] \notin msgs
 
 =============================================================================

test/tla/Bug20190921.tla

@@ -3,9 +3,13 @@ EXTENDS Integers
 
 \* constants and variables should propagate
 \* in the transformations
-CONSTANT N
+CONSTANT
+    \* @type: Int;
+    N
 
-VARIABLE x
+VARIABLE
+    \* @type: Int;
+    x
 
 CInit == N \in 1..10
 

test/tla/Bug20200306.tla

@@ -1,5 +1,7 @@
 ----- MODULE Bug20200306 -----
-VARIABLE a
+VARIABLE
+    \* @type: Int;
+    a
 Init == a = 1
 Next == a' = a
 Inv == FALSE

test/tla/Callback.tla

@@ -1,7 +1,9 @@
 ----------------------------- MODULE Callback ----------------------------
 EXTENDS Integers
 
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 Pick(Cb(_)) ==
     \E i \in 1..10:

test/tla/Config.tla

@@ -2,7 +2,9 @@
 (* a specification to check whether the configuration files are parsed *)
 EXTENDS Integers
 
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 \* the default init
 Init ==

test/tla/ConfigParams.tla

@@ -1,13 +1,27 @@
 --------------------------- MODULE ConfigParams -------------------------------
 CONSTANTS
+  \* @type: Int;
   MyInt,
+  \* @type: Str;
   MyStr,
+  \* TODO: use a model type here
+  \* when #570 is closed: https://github.com/informalsystems/apalache/issues/570
+  \* @type: Str;
   MyModelValue1,
+  \* @type: Str;
   MyModelValue2,
+  \* @type: Set(Int);
   MySet
 
 VARIABLES
-  x, y, z, w
+  \* @type: Int;
+  x,
+  \* @type: Str;
+  y,
+  \* @type: Str;
+  z,
+  \* @type: Set(Int);
+  w
 
 Init ==
     /\ x = MyInt

test/tla/ConfigReplacements.tla

@@ -1,5 +1,7 @@
 ----------------------- MODULE ConfigReplacements -----------------------------
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 Value == 0
 

test/tla/ConfigUnsorted.tla

@@ -1,6 +1,8 @@
 -------------------------- MODULE ConfigUnsorted ----------------------------------------
 (* A specification that introduces preprocessing issues *)
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 A == 1
 B == 2

test/tla/Counter.tla

@@ -1,7 +1,9 @@
 ------ MODULE Counter ------
 EXTENDS Naturals
 
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 Init == x \in 1..1000
 

test/tla/EWD840.tla

@@ -10,7 +10,15 @@ EXTENDS Naturals
 N == 4
 (*ASSUME NAssumption == N \in Nat \ {0}*)
 
-VARIABLES active, color, tpos, tcolor
+VARIABLES
+    \* @type: Int -> Bool;
+    active,
+    \* @type: Int -> Str;
+    color,
+    \* @type: Int;
+    tpos,
+    \* @type: Str;
+    tcolor
 
 Nodes == 0 .. N-1
 Color == {"white", "black"}

test/tla/ExistsAsValue.tla

@@ -1,6 +1,8 @@
 ------------------------ MODULE ExistsAsValue -------------------------
 \* a test for the issue #148
-VARIABLES x
+VARIABLES
+    \* @type: Bool;
+    x
 
 Init ==
     x = TRUE

test/tla/Fix365_ExistsSubset3.tla

@@ -2,9 +2,6 @@
 (* A tricky bug that happened in evidence handling *)
 EXTENDS Integers
 
-\* old apalache annotations
-a <: b == a
-
 Proc == {"p1", "p2"}
 Rounds == { 0, 1, 2 }
 
@@ -27,7 +24,7 @@ Next ==
     LET \* @type: Set(Str);
         Y == { m.src: m \in msgs } IN
     \* the third ingredient of the bug
-    /\ msgs /= {} <: {MT}
+    /\ msgs /= {}
     /\ UNCHANGED msgs
 
 ===============================================================================

test/tla/HandshakeWithTypes.tla

@@ -7,18 +7,22 @@
  *)
 EXTENDS Integers
 
-VARIABLES msgs,     \* the set of all messages
-          iseqno,   \* Initiator's sequence number
-          rseqno,   \* Receiver's sequence number
-          istate,   \* Initiator's state
-          rstate    \* Receiver's state
-
-a <: b == a
+VARIABLES
+    \* @type: Set([syn: Bool, ack: Bool, seqno: Int, ackno: Int]);
+    msgs,     \* the set of all messages
+    \* @type: Int;
+    iseqno,   \* Initiator's sequence number
+    \* @type: Int;
+    rseqno,   \* Receiver's sequence number
+    \* @type: Str;
+    istate,   \* Initiator's state
+    \* @type: Str;
+    rstate    \* Receiver's state
 
 MT == [syn |-> BOOLEAN, ack |-> BOOLEAN, seqno |-> Int, ackno |-> Int]
 
 Init ==
-    /\ msgs = {} <: {MT}
+    /\ msgs = {}
     /\ iseqno = 0
     /\ rseqno = 0
     /\ istate = "INIT"
@@ -28,15 +32,15 @@ SendSyn ==
     /\ istate = "INIT"
     /\ \E no \in Nat:
         /\ msgs' = msgs \union {[syn |-> TRUE,
-                                 ack |-> FALSE, seqno |-> no] <: MT}
+                                 ack |-> FALSE, seqno |-> no]}
         /\ iseqno' = no + 1
         /\ istate' = "SYN-SENT"
         /\ UNCHANGED <<rseqno, rstate>>
 
 SendSynAck ==
     /\ rstate = "LISTEN"
     /\ \E seqno, ackno \in Nat:
-        /\ ([syn |-> TRUE, ack |-> FALSE, seqno |-> seqno] <: MT) \in msgs
+        /\ [syn |-> TRUE, ack |-> FALSE, seqno |-> seqno] \in msgs
         /\ msgs' = msgs \union {[syn |-> TRUE, ack |-> TRUE,
                                  seqno |-> seqno + 1,
                                  ackno |-> ackno]}

test/tla/HourClock.tla

@@ -2,7 +2,10 @@
 \* This is a local copy of the example from Specifying Systems:
 \* https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/HourClock.tla
 EXTENDS Naturals
-VARIABLE hr
+VARIABLE
+    \* @type: Int;
+    hr
+
 HCini  ==  hr \in (1 .. 12)
 HCnxt  ==  hr' = IF hr # 12 THEN hr + 1 ELSE 1
 HC  ==  HCini /\ [][HCnxt]_hr

tla-assignments/src/test/resources/assignmentSolver/ITE_CASE.tla → test/tla/ITE_CASE.tla

@@ -1,5 +1,9 @@
 ------------------------------ MODULE ITE_CASE ------------------------------
-VARIABLES x, y
+VARIABLES
+    \* @type: Int;
+    x,
+    \* @type: Int;
+    y
 
 S == {1,2,3}
 
@@ -11,6 +15,9 @@ ITE(p, et, ee) ==  /\ IF p THEN et ELSE ee
 
 Next == ITE( x = y', x' = 2, x' \in S )
 
-Spec == /\ Init /\ [][Next]_<<x,y>>
+\* @type: <<Int, Int>>;
+vars == <<x, y>>
+
+Spec == /\ Init /\ [][Next]_vars
 
 =============================================================================

test/tla/Inline.tla

@@ -1,5 +1,7 @@
 ---------------------------- MODULE Inline -------------------------------
-VARIABLE x
+VARIABLE
+    \* @type: Int;
+    x
 
 A == 3
 

test/tla/NatCounter.tla

@@ -1,7 +1,9 @@
 ----------------------------- MODULE NatCounter ------------------------
 EXTENDS Naturals
 
-VARIABLE x
+VARIABLE
+    \* @type: Int;
+    x
 
 Init == x = 3
 

test/tla/NeedForTypesWithTypes.tla

@@ -4,20 +4,24 @@
  *)
 EXTENDS Integers, Sequences, FiniteSets
 
-CONSTANTS InSet     \* an input set
-VARIABLES Left,     \* a storage for the yet untransformed elements
-          OutSeq    \* the output sequence
+CONSTANTS
+    \* @type: Set(Int);
+    InSet     \* an input set
 
-a <: b == a          
+VARIABLES
+    \* @type: Set(Int);
+    Left,     \* a storage for the yet untransformed elements
+    \* @type: Seq(Int);
+    OutSeq    \* the output sequence
 
 ConstInit == InSet = 1..4
 
 Init ==
-    /\ OutSeq = << >> <: Seq(Int)
+    /\ OutSeq = << >>
     /\ Left = InSet
 
 Next ==
-    IF Left = {} <: {Int}
+    IF Left = {}
     THEN UNCHANGED <<Left, OutSeq>>
     ELSE \E x \in Left:
           /\ OutSeq' = Append(OutSeq, x)

test/tla/NonNullaryLet.tla

@@ -1,10 +1,12 @@
 --------------- MODULE NonNullaryLet ----------------
 EXTENDS Integers
-VARIABLE n
+VARIABLE
+    \* @type: Int;
+    n
 
 Foo == LET r(x) == TRUE IN r(1)
 
 Init == n = 0
 
 Next == Foo /\ n' = 1
-===========================================
+===========================================