Increase code coverage

apalache-mc · Jan 21, 2024 · e8c3b16 · e8c3b16
1 parent 7b925d2
commit e8c3b16
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 1 deletion.
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -1,11 +1,15 @@
 package at.forsyte.apalache.io.quint
 
-import at.forsyte.apalache.tla.lir.{IntT1, OperT1, RecRowT1, RowT1, SetT1, TlaEx, TlaType1, Typed, VarT1}
+import at.forsyte.apalache.tla.lir.{
+  BoolT1, IntT1, OperT1, RecRowT1, RowT1, SetT1, TlaAssumeDecl, TlaEx, TlaType1, Typed, ValEx, VarT1,
+}
 import org.junit.runner.RunWith
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatestplus.junit.JUnitRunner
 import QuintType._
 import QuintEx._
+import at.forsyte.apalache.io.quint.QuintDef.QuintAssume
+import at.forsyte.apalache.tla.lir.values.TlaBool
 import at.forsyte.apalache.tla.typecomp.build
 
 // You can run all these tests in watch mode in the
@@ -789,4 +793,18 @@ class TestQuintEx extends AnyFunSuite {
     val err = intercept[QuintIRParseError](convert(Q.oneOfSet))
     assert(err.getMessage().contains("`oneOf` can only occur as the principle operator of a `nondet` declaration"))
   }
+
+  test("can convert ASSUME declaration") {
+    val translator = new Quint(Q.quintOutput)
+    val nullaryOps = Set[String]()
+
+    val name = "myAssume"
+    val namedAssume = QuintAssume(1, name, QuintBool(2, true))
+    val tlaNamedAssumeDef = translator.tlaDef(namedAssume).run(nullaryOps).get._2
+    assert(tlaNamedAssumeDef == TlaAssumeDecl(Some(name), ValEx(TlaBool(true))(Typed(BoolT1)))(Typed(BoolT1)))
+
+    val unnamedAssume = QuintAssume(1, "_", QuintBool(2, true))
+    val tlaUnnamedAssumeDef = translator.tlaDef(unnamedAssume).run(nullaryOps).get._2
+    assert(tlaUnnamedAssumeDef == TlaAssumeDecl(None, ValEx(TlaBool(true))(Typed(BoolT1)))(Typed(BoolT1)))
+  }
 }
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintIR.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintIR.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.io.quint
 
+import at.forsyte.apalache.io.quint.QuintDef.QuintAssume
+import at.forsyte.apalache.io.quint.QuintEx.QuintBool
 import org.junit.runner.RunWith
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatestplus.junit.JUnitRunner
@@ -37,6 +39,14 @@ class TestQuintIR extends AnyFunSuite {
     assert(QuintDeserializer.write[BigInt](BigInt(s"-${someBigIntStr}")) == s"-${someBigIntStr}")
   }
 
+  test("QuintAssume#isUnnamed works correctly") {
+    val namedAssume = QuintAssume(1, "myAssume", QuintBool(2, true))
+    assert(!namedAssume.isUnnamed)
+
+    val unnamedAssume = QuintAssume(1, "_", QuintBool(2, true))
+    assert(unnamedAssume.isUnnamed)
+  }
+
   // tictactoe.json is located in tla-io/src/test/resources/tictactoe.json
   test("Can load tictactoe.json") {
     val tictactoeQuintJson = scala.io.Source.fromResource("tictactoe.json").mkString

diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestPrinter.scala
@@ -195,6 +195,14 @@ class TestPrinter extends AnyFunSuite with TestingPredefs {
     }
   }
 
+  test("Test UTF8: TlaAssumeDecl") {
+    val namedAssume: String = toUtf(TlaAssumeDecl(Some("myAssume"), tla.eql(tla.name("x"), tla.bool(true))))
+    assert(namedAssume == s"ASSUME myAssume ≜ x = TRUE")
+
+    val unnamedAssume: String = toUtf(TlaAssumeDecl(None, tla.eql(tla.name("x"), tla.bool(true))))
+    assert(unnamedAssume == s"ASSUME x = TRUE")
+  }
+
   // regression
   test("Test UTF8: OperFormalParam") {
     val d = TlaOperDecl("Foo", List(OperParam("Bar", 1)), ValEx(TlaInt(1)))