Merge branch 'unstable' into jk/unboundedForms

apalache-mc · Mar 4, 2022 · 325b56e · 325b56e
2 parents 047f9a2 + b908195
commit 325b56e
Show file tree

Hide file tree

Showing 37 changed files with 165 additions and 236 deletions.
diff --git a/Makefile b/Makefile
@@ -50,12 +50,12 @@ test/tla/%.md: target/test/tla/%.md.corrected
 fmt-check:
   # TODO: rm if we decide to keep running on all source files
 	# git fetch origin
-	sbt scalafmtCheckAll scalafmtSbtCheck || \
+	sbt scalafmtCheckAll scalafmtSbtCheck scalafixEnable "scalafixAll --check RemoveUnused" || \
 		( echo "TO FIX: run 'make fmt-fix' and commit the changes" ; \
 		  exit 1 )
 
 fmt-fix:
-	sbt "scalafix RemoveUnused" scalafmtAll scalafmtSbt
+	sbt scalafixEnable "scalafixAll RemoveUnused" scalafmtAll scalafmtSbt
 
 clean:
 	sbt clean

diff --git a/build.sbt b/build.sbt
@@ -56,7 +56,6 @@ ThisBuild / scalafmtPrintDiff := true
 // scalafix
 // https://scalacenter.github.io/scalafix/docs/rules/RemoveUnused.html
 ThisBuild / scalacOptions ++= Seq("-Ywarn-unused")
-ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
 
 ///////////////////////////////

diff --git a/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala b/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala
@@ -2,7 +2,6 @@ package at.forsyte.apalache.infra.passes
 
 import org.junit.runner.RunWith
 import org.scalatest.funsuite.AnyFunSuite
-import org.scalatestplus.easymock.EasyMockSugar
 import org.scalatestplus.junit.JUnitRunner
 import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
 

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala
@@ -1,6 +1,6 @@
 package at.forsyte.apalache.tla.bmcmt
 
-import java.io.{PrintWriter, StringWriter}
+import java.io.StringWriter
 
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.convenience.tla

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala
@@ -30,7 +30,6 @@ trait TestArena extends FixtureAnyFunSuite {
 
   test("BOOLEAN has FALSE and TRUE") { _ =>
     val arena = Arena.create(solver)
-    val boolean = arena.cellBooleanSet()
     assert(List(arena.cellFalse(), arena.cellTrue()) == arena.getHas(arena.cellBooleanSet()))
   }
 }
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerTrait.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerTrait.scala
@@ -750,7 +750,6 @@ trait TestSeqModelCheckerTrait extends FixtureAnyFunSuite {
     val checkerInput =
       new CheckerInput(mkModuleWithX(), initTrans, nextTrans, None, CheckerInputVC(List((inv, notInv))))
     // initialize the model checker
-    val filter = "0,0,0,0,0,0,0,0,0,0,0" // old syntax
     val tuning = Map.empty[String, String] // Map("search.transitionFilter" -> filter)
     val params = new ModelCheckerParams(checkerInput, stepsBound = 10, new File("."), tuning, false)
     val ctx = new IncrementalExecutionContext(rewriter)
@@ -813,8 +812,4 @@ trait TestSeqModelCheckerTrait extends FixtureAnyFunSuite {
       .typed(types, "b")
   }
 
-  private def mkNotAssign(varName: String, rhs: BuilderEx, tt: TlaType1): TlaEx = {
-    eql(prime(name(varName) ? "_tt") ? "_tt", rhs)
-      .typed(types + ("_tt" -> tt), "b")
-  }
 }
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala
@@ -457,7 +457,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase {
 
     val state = new SymbState(asgn, arena, Binding())
     val rewriter = create(rewriterType)
-    val nextState = rewriter.rewriteUntilDone(state)
+    rewriter.rewriteUntilDone(state)
     assert(rewriter.solverContext.sat())
   // there is not much to check here, since it is just a function that returns an integer
   }

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterBool.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterBool.scala
@@ -123,7 +123,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs {
     rewriter.rewriteOnce(state) match {
       case SymbStateRewriter.Continue(nextState) =>
         nextState.ex match {
-          case NameEx(name) =>
+          case NameEx(_) =>
             val eq = tla
               .eql(cell.toNameEx ? "b", arena.cellFalse().toNameEx ? "b")
               .typed(boolTypes, "b")
@@ -229,7 +229,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs {
     rewriter.rewriteOnce(state) match {
       case SymbStateRewriter.Continue(nextState) =>
         nextState.ex match {
-          case NameEx(name) =>
+          case NameEx(_) =>
             assert(solverContext.sat())
             solverContext.assertGroundExpr(nextState.ex)
             rewriter.push()
@@ -316,7 +316,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs {
     rewriter.rewriteOnce(state) match {
       case SymbStateRewriter.Continue(nextState) =>
         nextState.ex match {
-          case NameEx(name) =>
+          case NameEx(_) =>
             val eq1 = tla
               .eql(left.toNameEx ? "b", arena.cellFalse().toNameEx ? "b")
               .typed(boolTypes, "b")
@@ -353,7 +353,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case predEx @ NameEx(name) =>
+      case predEx @ NameEx(_) =>
         solverContext.assertGroundExpr(predEx)
         rewriter.push()
         // both false

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChoose.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChoose.scala
@@ -45,7 +45,7 @@ trait TestSymbStateRewriterChoose extends RewriterBase with TestingPredefs {
       .typed(types, "i")
     val state = new SymbState(ex, arena, Binding())
     val rewriter = create(rewriterType)
-    val nextState = rewriter.rewriteUntilDone(state)
+    rewriter.rewriteUntilDone(state)
     // the buggy implementation of choose fails on a dynamically empty set
     assert(solverContext.sat())
   // The semantics of choose does not restrict the outcome on the empty sets,

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFoldSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFoldSet.scala
@@ -7,17 +7,6 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.ApalacheOper
 
 trait TestSymbStateRewriterFoldSet extends RewriterBase {
-  private val types = Map(
-      "b" -> BoolT1(),
-      "i" -> IntT1(),
-      "(i)" -> TupT1(IntT1()),
-      "I" -> SetT1(IntT1()),
-      "ib" -> TupT1(IntT1(), BoolT1()),
-      "ibs" -> TupT1(IntT1(), BoolT1(), StrT1()),
-      "IB" -> SetT1(TupT1(IntT1(), BoolT1())),
-      "ibI" -> TupT1(IntT1(), BoolT1(), SetT1(IntT1())),
-  )
-
   test("""FoldSet( LAMBDA x,y: C, v, S ) = C""") { rewriterType: SMTEncoding =>
     // A : (a,b) => a
     // A(p,q) == 0

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala
@@ -43,7 +43,7 @@ trait TestSymbStateRewriterFunSet extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case NameEx(name) =>
+      case NameEx(_) =>
         val cell = nextState.arena.findCellByNameEx(nextState.ex)
         assert(cell.cellType == FinFunSetT(FinSetT(IntT()), FinSetT(BoolT())))
         val dom = nextState.arena.getDom(cell)
@@ -71,7 +71,7 @@ trait TestSymbStateRewriterFunSet extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case NameEx(name) =>
+      case NameEx(_) =>
         val cell = nextState.arena.findCellByNameEx(nextState.ex)
         assert(cell.cellType == FinFunSetT(FinSetT(IntT()), FinSetT(FinSetT(BoolT()))))
         val dom = nextState.arena.getDom(cell)
@@ -242,7 +242,7 @@ trait TestSymbStateRewriterFunSet extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case NameEx(name) =>
+      case NameEx(_) =>
         val cell = nextState.arena.findCellByNameEx(nextState.ex)
         assert(cell.cellType == FinFunSetT(FinSetT(IntT()), FinSetT(BoolT())))
         val dom = nextState.arena.getDom(cell)

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterInt.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterInt.scala
@@ -59,7 +59,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case predEx @ NameEx(name) =>
+      case predEx @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(22)).as(Bool))
         rewriter.push()
@@ -95,7 +95,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case cmpEx @ NameEx(name) =>
+      case cmpEx @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(cmpEx)
         solverContext.assertGroundExpr(eql(leftCell.toNameEx.as(Int), int(4)).as(Bool))
@@ -125,7 +125,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case cmpEx @ NameEx(name) =>
+      case cmpEx @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(cmpEx)
         solverContext.assertGroundExpr(eql(leftCell.toNameEx.as(Int), int(4)).as(Bool))
@@ -155,7 +155,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case cmpEx @ NameEx(name) =>
+      case cmpEx @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(cmpEx)
         solverContext.assertGroundExpr(eql(leftCell.toNameEx.as(Int), int(4)).as(Bool))
@@ -182,7 +182,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case cmpEx @ NameEx(name) =>
+      case cmpEx @ NameEx(_) =>
         assert(solverContext.sat())
         rewriter.push()
         solverContext.assertGroundExpr(cmpEx)
@@ -206,7 +206,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case cmpEx @ NameEx(name) =>
+      case cmpEx @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(cmpEx)
         solverContext.assertGroundExpr(eql(leftCell.toNameEx.as(Int), int(4)).as(Bool))
@@ -236,7 +236,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case predEx @ NameEx(name) =>
+      case predEx @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(22)).as(Bool))
         rewriter.push()
@@ -273,7 +273,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case result @ NameEx(name) =>
+      case result @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(1981)).as(Bool))
         rewriter.push()
@@ -301,7 +301,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case result @ NameEx(name) =>
+      case result @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(2017)).as(Bool))
         rewriter.push()
@@ -327,7 +327,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case result @ NameEx(name) =>
+      case result @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(2017)).as(Bool))
         rewriter.push()
@@ -353,7 +353,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case result @ NameEx(name) =>
+      case result @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(7)).as(Bool))
         rewriter.push()
@@ -381,7 +381,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case result @ NameEx(name) =>
+      case result @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(30)).as(Bool))
         rewriter.push()
@@ -409,7 +409,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case result @ NameEx(name) =>
+      case result @ NameEx(_) =>
         assert(solverContext.sat())
         solverContext.assertGroundExpr(eql(leftInt.as(Int), int(30)).as(Bool))
         rewriter.push()
@@ -436,7 +436,7 @@ trait TestSymbStateRewriterInt extends RewriterBase {
     val rewriter = create(rewriterType)
     val nextState = rewriter.rewriteUntilDone(state)
     nextState.ex match {
-      case predEx @ NameEx(name) =>
+      case predEx @ NameEx(_) =>
         assert(solverContext.sat())
         // check equality
         rewriter.push()

diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterPowerset.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterPowerset.scala
@@ -139,7 +139,6 @@ trait TestSymbStateRewriterPowerset extends RewriterBase {
     var nextState = rewriter.rewriteUntilDone(state)
     val baseCell = nextState.asCell
     nextState = new PowSetCtor(rewriter).confringo(nextState, baseCell)
-    val powCell = nextState.asCell
     // check equality
     val eq = eql(nextState.ex,
         enumSet(enumSet() ? "I", enumSet(int(1)) ? "I", enumSet(int(2)) ? "I", enumSet(int(1), int(2)) ? "I") ? "II")