#121 JsonReader: update TestCounterexampleWriter

apalache-mc · May 19, 2020 · 067e659 · 067e659
1 parent 6bd4b9e
commit 067e659
Showing 1 changed file with 40 additions and 10 deletions.
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestCounterexampleWriter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestCounterexampleWriter.scala
@@ -251,7 +251,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "InvariantViolation",
@@ -260,7 +263,10 @@ class TestCounterexampleWriter extends FunSuite {
         |          "x",
         |          1
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    }
         |  ]
         |}""".stripMargin
@@ -290,7 +296,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "State2",
@@ -303,7 +312,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "State3",
@@ -316,7 +328,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "InvariantViolation",
@@ -325,7 +340,10 @@ class TestCounterexampleWriter extends FunSuite {
         |          "x",
         |          1
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    }
         |  ]
         |}""".stripMargin
@@ -361,7 +379,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "State2",
@@ -380,7 +401,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "State3",
@@ -399,7 +423,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    },
         |    {
         |      "OPERATOR": "InvariantViolation",
@@ -418,7 +445,10 @@ class TestCounterexampleWriter extends FunSuite {
         |            ]
         |          }
         |        ]
-        |      }
+        |      },
+        |      "params": [
+        |        
+        |      ]
         |    }
         |  ]
         |}""".stripMargin