Merge branch 'unstable' into ik/example1837

apalache-mc · Jun 1, 2022 · e4c94d9 · e4c94d9
2 parents b3bfc9d + 98b37f0
commit e4c94d9
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 8 deletions.
diff --git a/.unreleased/bug-fixes/1839.md b/.unreleased/bug-fixes/1839.md
@@ -0,0 +1 @@
+Output rare expressions as unserializable to ITF, see #1841
diff --git a/docs/src/adr/015adr-trace.md b/docs/src/adr/015adr-trace.md
@@ -1,7 +1,11 @@
 ---
-authors: Igor Konnov
-proposed by: Vitor Enes, Andrey Kupriyanov
-last revised: 2021-12-23
+
+**authors:** Igor Konnov
+
+**proposed by:** Vitor Enes, Andrey Kupriyanov
+
+**last revised:** 2022-06-01
+
 ---
 
 # ADR-015: Informal Trace Format in JSON
@@ -302,6 +306,11 @@ specified in the field `vars`. Each state must define a value for every specifie
    `p[1]` is the map value. Importantly, a key may be an arbitrary expression. It does not have to be a string or an integer. TLA+ functions are written as maps
    in this format.
 
+1. An expression that cannot be serialized: `{ "#unserializable": "<string
+representation>" }`. For instance, the set of all integers is represented with
+`{ "#unserializable": "Int" }`. This should be a very rare expression, which
+should not occur in normal traces. Usually, it indicates some form of an
+error.
 
 ### Example
 

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala
@@ -124,6 +124,8 @@ class ItfCounterexampleWriter(writer: PrintWriter) extends CounterexampleWriter
       ujson.Obj("#map" -> ujson.Arr(keyValueArrays: _*))
 
     case e =>
-      throw new IllegalArgumentException("Unexpected expression in an ITF counterexample: " + e)
+      // We don't know how to serialize this TLA+ expression (e.g., Int, Nat, FunSet, PowSet).
+      // Output it as a serialization error.
+      ujson.Obj("#unserializable" -> ujson.Str(e.toString))
   }
 }
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala
@@ -63,16 +63,17 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
   test("ITF JSON single state") {
     val intSeq = SeqT1(IntT1)
     val intAndStr = TupT1(IntT1, StrT1)
-    val intSet = SetT1(IntT1)
+    val intSetT = SetT1(IntT1)
     val fooBar = RecT1("foo" -> IntT1, "bar" -> BoolT1)
     val intToStr = FunT1(IntT1, StrT1)
+    val boolToInt = FunT1(BoolT1, IntT1)
 
     def pair(i: Int, s: String) = tuple(int(i), str(s)).as(intAndStr)
     val decls = List(
         TlaVarDecl("a")(Typed(IntT1)),
         TlaVarDecl("b")(Typed(StrT1)),
         TlaVarDecl("c")(Typed(intSeq)),
-        TlaVarDecl("d")(Typed(intSet)),
+        TlaVarDecl("d")(Typed(intSetT)),
         TlaVarDecl("e")(Typed(fooBar)),
         TlaVarDecl("f")(Typed(intAndStr)),
         TlaVarDecl("g")(Typed(intToStr)),
@@ -93,7 +94,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
                     "c" -> tuple(int(3), int(BigInt("1000000000000000000", 10))).as(intSeq),
                     // { 5, 6 }
                     "d" -> enumSet(int(5), int(6))
-                      .as(intSet),
+                      .as(intSetT),
                     // [ foo |-> 3, bar |-> TRUE ]
                     "e" -> enumFun(str("foo"), int(3), str("bar"), bool(true))
                       .as(fooBar),
@@ -107,6 +108,14 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
                     "h" -> (apalacheSetAsFun(enumSet().as(SetT1(intAndStr))).as(intToStr)),
                     // SetAsFun({ <<1, "a">> })
                     "i" -> (apalacheSetAsFun(enumSet(pair(1, "a")).as(SetT1(intAndStr))).as(intToStr)),
+                    // [ BOOLEAN -> Int ]
+                    "j" -> funSet(booleanSet(), intSet()).as(SetT1(boolToInt)),
+                    // SUBSET BOOLEAN
+                    "k" -> powSet(booleanSet()).as(SetT1(BoolT1)),
+                    // Int
+                    "l" -> intSet().as(intSetT),
+                    // Nat
+                    "m" -> natSet().as(intSetT),
                 )),
         ),
         """{
@@ -127,7 +136,11 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
           |      "f": { "#tup": [ 7, "myStr" ] },
           |      "g": { "#map": [[1, "a"], [2, "b"], [3, "c"]] },
           |      "h": { "#map": [] },
-          |      "i": { "#map": [[1, "a"]] }
+          |      "i": { "#map": [[1, "a"]] },
+          |      "j": { "#unserializable": "[BOOLEAN → Int]" },
+          |      "k": { "#unserializable": "SUBSET BOOLEAN" },
+          |      "l": { "#unserializable": "Int" },
+          |      "m": { "#unserializable": "Nat" }
           |    }
           |  ]
           |}""".stripMargin,