Integrating types 4: migrated tests to Snowcat (#652)

* annotated all tests and fixed some * Integrating types 5: made Inliner, Unroller, and ParameterNormalizer type-aware (#657) * bugfix: translating labels * fixing types in Unroller and Inliner * moved and rewrote TestInlinerofUserOper, made it type-aware * made TestUnroller type-aware * made ParameterNormalizer type-aware * made TestUnroller and Unroller type-aware * running the type checker right after the parser * a reference to the closed issue * Integrating types 6: made Desugarer type aware (#658) * add a watchdog listener * close #647: Desugarer preprocesses the general case of EXCEPT * unrelease notes * type-aware test for Desugarer * made Desugarer type-aware! * fixed a type bug that was found by the type watchdog * propagating types in AssignmentOperatorIntroduction * made SkolemizationMarker type-aware * made ExpansionMarker type-aware * fixed TestSymbTransGenerator * moved the integration tests to test/tla * removed the Paxos tests, which is already in the integration tests * enabled snowcat by default, as the preprocessing is type-aware * Integrating types 7: victory over enthropy (#663) * a temporary fix for the old type annotations * a fix for lazy annotations of nullary operators * fix SymbTransGenerator * fixed plenty of integration tests * fixed a bug in ITE, found by Jure * made the TLC config parser type-aware * add type annotations to the tests * made VCGenerator type-aware * moved TlaType1, TypedPredefs, and TypingException to lir, to break cyclic dependencies * fixing types in TestConstAndDefRewriter * made TlcConfigImporter type-aware * fixed TestTlcConfigImporter * removed the reference to lir. * Integrating types 8: using new types in the checker core (#668) * migrated rewriting rules to use the types inferred by snowcat * forbid the old type annotations * fixed FunExcept * the error about old type annotations is qualified as a normal user error * fixed: set constructor, map, and in * fix the CHOOSE rule * removed the old type annotations, as they are no longer supported * Mad TestSymbStateRewriterBool, AndRule, and OrRule type-aware * made TestSymbStateRewriterInt typed * fixed all but one tests in TestSymbStateRewriterAssignment * remove the tests that are labelled as ignore * fix a funny bug in caching expressions * fix arena corruption in PowSetCtorRule * fix a bug in Builder: produced Int instead of Nat * equality throws when incomparable types are met * fixed an error message for infinite sets * made tests in TestSymbStateRewriterSet type-aware * eliminated the old TrivialTypeFinder and ModelChecker, no need to maintain them * fix a bug in FunExceptRule * fix TestSymbStateRewriterFun * fix TestSymbStateRewriterStr and TestSymbStateRewriterTuple * fix TestSymbStateRewriterRecord and a bug in EXCEPT * fix TestCherryPick * remove the unit test that is covered by TestKeramelizer * fix TestSymbStateRewriterChoose * fix TestSymbStateRewriterControl * fix TestSymbStateRewriterExpand * fix TestSymbStateRewriterFiniteSets * TestSymbStateRewriterFunSet * fix TestSymbStateRewriterRecFun * fix TestSymbStateRewriterSequence * fix TestSeqModelChecker * fix TestSymbStateDecoder * fix TestSymbStateRewriterTlc * old annotations are expected to throw an error now * fix TestSymbStateRewriterPowerset * fixed cherry picking of records that have compatible but different domains * fixed type annotations in SimpT1 * fix cherry-picking of records that was broken in Paxos * removed --with-snowcat from CLI * changelog * Integrating types 9: a few bugfixes (#671) * a better error message * fix the structure of EXCEPT expressions + add support for sequences * fixed the comment by Shon * fixed the accidental bug introduced in refactoring
apalache-mc · Mar 24, 2021 · cbeda08 · cbeda08
1 parent eb7860f
commit cbeda08
Show file tree

Hide file tree

Showing 206 changed files with 5,044 additions and 8,081 deletions.
diff --git a/UNRELEASED.md b/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
 

diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/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)
 

diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/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")
 }
diff --git a/test/tla/Assignments20200309.tla b/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

diff --git a/test/tla/Bug20190118.tla b/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
 
 =============================================================================
diff --git a/test/tla/Bug20190921.tla b/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
 

diff --git a/test/tla/Bug20200306.tla b/test/tla/Bug20200306.tla
@@ -1,5 +1,7 @@
 ----- MODULE Bug20200306 -----
-VARIABLE a
+VARIABLE
+    \* @type: Int;
+    a
 Init == a = 1
 Next == a' = a
 Inv == FALSE

diff --git a/test/tla/Callback.tla b/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:

diff --git a/test/tla/Config.tla b/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 ==

diff --git a/test/tla/ConfigParams.tla b/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

diff --git a/test/tla/ConfigReplacements.tla b/test/tla/ConfigReplacements.tla
@@ -1,5 +1,7 @@
 ----------------------- MODULE ConfigReplacements -----------------------------
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 Value == 0
 

diff --git a/test/tla/ConfigUnsorted.tla b/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

diff --git a/test/tla/Counter.tla b/test/tla/Counter.tla
@@ -1,7 +1,9 @@
 ------ MODULE Counter ------
 EXTENDS Naturals
 
-VARIABLES x
+VARIABLES
+    \* @type: Int;
+    x
 
 Init == x \in 1..1000
 

diff --git a/test/tla/EWD840.tla b/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"}

diff --git a/test/tla/ExistsAsValue.tla b/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

diff --git a/test/tla/Fix365_ExistsSubset3.tla b/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
 
 ===============================================================================
diff --git a/test/tla/HandshakeWithTypes.tla b/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]}

diff --git a/test/tla/HourClock.tla b/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

diff --git a/...t/resources/assignmentSolver/ITE_CASE.tla → test/tla/ITE_CASE.tla b/...t/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
 
 =============================================================================
diff --git a/test/tla/Inline.tla b/test/tla/Inline.tla
@@ -1,5 +1,7 @@
 ---------------------------- MODULE Inline -------------------------------
-VARIABLE x
+VARIABLE
+    \* @type: Int;
+    x
 
 A == 3
 

diff --git a/test/tla/NatCounter.tla b/test/tla/NatCounter.tla
@@ -1,7 +1,9 @@
 ----------------------------- MODULE NatCounter ------------------------
 EXTENDS Naturals
 
-VARIABLE x
+VARIABLE
+    \* @type: Int;
+    x
 
 Init == x = 3
 

diff --git a/test/tla/NeedForTypesWithTypes.tla b/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)

diff --git a/test/tla/NonNullaryLet.tla b/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
-===========================================
+===========================================