diff --git a/Makefile b/Makefile index 5c33372c0f..d39d17193c 100644 --- 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 index fde37ad353..b6caf25a3d 100644 --- 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 index 1ad247364c..10710d604d 100644 --- 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 index 1cdc9236d5..a67ca1a5f3 100644 --- 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 index 13734010b5..b7d004a12d 100644 --- 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 index 9d2ed6fd87..49e959be2e 100644 --- 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 index f0b76082af..ef236d13c3 100644 --- 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 index eab5d36360..6ba978c2ed 100644 --- 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 index e3ff42142f..69b01a7691 100644 --- 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 index c0dccf07f4..c8c20a58e3 100644 --- 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 index d0b3718eea..e4866f5535 100644 --- 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 index ca7e7618de..d64eaa1d1e 100644 --- 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 index c623e9a265..c084a2ac14 100644 --- 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") diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala index c2a54e8455..c8d240607b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala @@ -77,7 +77,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(predEx) assert(solverContext.sat()) @@ -99,7 +99,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(predEx) assert(solverContext.sat()) @@ -118,7 +118,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(predEx) assert(!solverContext.sat()) @@ -181,7 +181,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { rewriter.rewriteOnce(state) match { case SymbStateRewriter.Continue(nextState) => nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(not(predEx.as(boolT)).as(boolT)) assert(!solverContext.sat()) @@ -204,7 +204,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val state = new SymbState(ex, arena, Binding()) val rewriter = create(rewriterType) rewriter.rewriteUntilDone(state).ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(not(predEx.as(boolT)).as(boolT)) assert(solverContext.sat()) @@ -227,7 +227,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { rewriter.rewriteOnce(state) match { case SymbStateRewriter.Continue(nextState) => nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() // cell = \TRUE solverContext.assertGroundExpr(eql(arena.cellTrue().toNameEx.as(boolT), cell.toNameEx.as(boolT)).as(boolT)) @@ -260,7 +260,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => nextState.arena.appendCell(IntT()) // the buggy rule implementation triggered an error here rewriter.push() solverContext.assertGroundExpr(predEx) @@ -284,7 +284,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val state = new SymbState(ex, arena, Binding()) val rewriter = create(rewriterType) rewriter.rewriteUntilDone(state).ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() // cell = TRUE solverContext.assertGroundExpr(eql(arena.cellTrue().toNameEx.as(boolT), cell.toNameEx.as(boolT)).as(boolT)) @@ -403,7 +403,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() // not equal solverContext.assertGroundExpr(predEx) @@ -451,7 +451,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() // equal solverContext.assertGroundExpr(predEx) @@ -510,7 +510,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case newSet @ NameEx(name) => + case NameEx(_) => rewriter.push() assert(solverContext.sat()) // we check actual membership in another test @@ -619,7 +619,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case membershipEx @ NameEx(name) => + case membershipEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(membershipEx) assert(!solverContext.sat()) @@ -659,7 +659,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case membershipEx @ NameEx(name) => + case membershipEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(membershipEx) assert(solverContext.sat()) @@ -682,7 +682,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case membershipEx @ NameEx(name) => + case membershipEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(membershipEx) assert(!solverContext.sat()) @@ -716,7 +716,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case membershipEx @ NameEx(name) => + case membershipEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(membershipEx) assert(solverContext.sat()) @@ -747,7 +747,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case membershipEx @ NameEx(name) => + case membershipEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(membershipEx) assert(solverContext.sat()) @@ -816,7 +816,7 @@ trait TestSymbStateRewriterSet 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() @@ -882,7 +882,7 @@ trait TestSymbStateRewriterSet extends RewriterBase { val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) nextState.ex match { - case predEx @ NameEx(name) => + case predEx @ NameEx(_) => rewriter.push() solverContext.assertGroundExpr(predEx) assert(solverContext.sat()) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterStr.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterStr.scala index 7e984e58e6..4014e2fcb0 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterStr.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterStr.scala @@ -2,11 +2,10 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.tla.lir.TypedPredefs._ import at.forsyte.apalache.tla.lir.convenience.tla._ -import at.forsyte.apalache.tla.lir.{BoolT1, StrT1} +import at.forsyte.apalache.tla.lir.BoolT1 trait TestSymbStateRewriterStr extends RewriterBase { test(""" rewrite "red" """) { rewriterType: SMTEncoding => - val string = str("red").typed(StrT1()) val neq = not(eql(str("red"), str("blue")).typed(BoolT1())) .typed(BoolT1()) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterTuple.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterTuple.scala index 7740da0d7b..751741cca6 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterTuple.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterTuple.scala @@ -43,7 +43,7 @@ trait TestSymbStateRewriterTuple extends RewriterBase { .typed(types, "IB") val state = new SymbState(tupleSet, arena, Binding()) - val nextState = create(rewriterType).rewriteUntilDone(state) + create(rewriterType).rewriteUntilDone(state) assert(solverContext.sat()) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala index e32d8bd4f2..7aa2b727b4 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala @@ -12,7 +12,7 @@ trait TestSparseOracle extends RewriterBase with TestingPredefs { var state = new SymbState(tla.bool(true), arena, Binding()) // introduce an oracle val (nextState, oracle) = PropositionalOracle.create(rewriter, state, 2) - val sparseOracle = new SparseOracle(oracle, Set(1, 10)) + new SparseOracle(oracle, Set(1, 10)) assert(solverContext.sat()) } diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala index 35c1d635bd..2be100be76 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala @@ -192,20 +192,6 @@ class TestPrettyWriter extends AnyFunSuite with BeforeAndAfterEach { | 8, | 9, | 10 }""".stripMargin - // Igor: I would prefer the layout below, but do not know how to do it with kiama - val iLikeItBetterButItDoesNotWork = - """{ - | 1, - | 2, - | 3, - | 4, - | 5, - | 6, - | 7, - | 8, - | 9, - | 10 - |}""".stripMargin val result = stringWriter.toString assert(expected == result) } diff --git a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala index 5c82c1592d..e0af1605cd 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala @@ -493,14 +493,13 @@ class TestSanyImporter extends SanyImporterTestBase { val (rootName, modules) = sanyImporter .loadFromSource("builtins", Source.fromString(text)) - val mod = expectSingleModule("builtins", rootName, modules) + expectSingleModule("builtins", rootName, modules) val root = modules(rootName) expectSourceInfoInDefs(root) def expectDecl(name: String, body: TlaEx): Unit = findAndExpectOperDecl(root, name, List(), body) - val trueOperDecl = mod.declarations(1) expectDecl("True", ValEx(TlaBool(true))) val trueOperEx = OperEx(TlaOper.apply, NameEx("True")) @@ -790,7 +789,7 @@ class TestSanyImporter extends SanyImporterTestBase { val (rootName, modules) = sanyImporter .loadFromSource("comprehensions", Source.fromString(text)) - val mod = expectSingleModule("comprehensions", rootName, modules) + expectSingleModule("comprehensions", rootName, modules) val root = modules(rootName) expectSourceInfoInDefs(root) @@ -1475,7 +1474,7 @@ class TestSanyImporter extends SanyImporterTestBase { case TlaOperDecl( _, _, - OperEx(TlaOper.apply, NameEx("A"), lambda, ValEx(TlaInt(i))), + OperEx(TlaOper.apply, NameEx("A"), lambda, ValEx(TlaInt(_))), ) => lambda match { case LetInEx( @@ -1582,7 +1581,6 @@ class TestSanyImporter extends SanyImporterTestBase { // The caveat here is that the formal parameter R does not appear in the list of the R's formal parameters, // but it is accessible via the field recParam. assert(d.isRecursive) - val recParam = OperParam(name, nparams) assert(d.body == expectedBody) assert(sourceStore.contains(d.body.ID)) // and source file information has been saved @@ -1627,7 +1625,6 @@ class TestSanyImporter extends SanyImporterTestBase { // The caveat here is that the formal parameter F does not appear in the list of the F's formal parameters, // but it is accessible via the field recParam. assert(d.isRecursive) - val recParam = OperParam("F", 1) val ite = OperEx( TlaControlOper.ifThenElse, OperEx(TlaOper.eq, NameEx("n"), ValEx(TlaInt(0))), diff --git a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterAnnotations.scala b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterAnnotations.scala index 3774d7eee6..e89e81d286 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterAnnotations.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterAnnotations.scala @@ -1,6 +1,6 @@ package at.forsyte.apalache.tla.imp -import at.forsyte.apalache.io.annotations.{Annotation, AnnotationParserError} +import at.forsyte.apalache.io.annotations.Annotation import at.forsyte.apalache.io.annotations.store._ import at.forsyte.apalache.tla.imp.src.SourceStore import at.forsyte.apalache.tla.lir._ @@ -164,7 +164,7 @@ class TestSanyImporterAnnotations extends AnyFunSuite with BeforeAndAfter { module.declarations.find(_.name == "A") match { // SanyImporter introduces a let-definition before application of a LOCAL operator - case Some(d @ TlaOperDecl(_, _, LetInEx(_, localDef))) => + case Some(TlaOperDecl(_, _, LetInEx(_, localDef))) => val annotations = annotationStore(localDef.ID) val expected = Annotation("pure") :: Annotation( "type", @@ -199,7 +199,7 @@ class TestSanyImporterAnnotations extends AnyFunSuite with BeforeAndAfter { val module = loadModule(text, "oper") module.declarations.find(_.name == "A") match { - case Some(d @ TlaOperDecl(_, _, LetInEx(_, incDecl))) => + case Some(TlaOperDecl(_, _, LetInEx(_, incDecl))) => val annotations = annotationStore(incDecl.ID) val expected = Annotation("pure") :: Annotation( "type", diff --git a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterStandardModules.scala b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterStandardModules.scala index 026d91d0fc..2610c789c2 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterStandardModules.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterStandardModules.scala @@ -133,10 +133,10 @@ class TestSanyImporterStandardModules extends SanyImporterTestBase { ) // check the source info - val plus = root.declarations.find { + root.declarations.find { _.name == "Plus" } match { - case Some(TlaOperDecl(_, _, oe @ OperEx(oper, _*))) => + case Some(TlaOperDecl(_, _, oe @ OperEx(_, _*))) => val loc = sourceStore.find(oe.ID).get assert( SourceRegion(SourcePosition(4, 9), SourcePosition(4, 13)) == loc.region diff --git a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/src/TestRegionTree.scala b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/src/TestRegionTree.scala index ca75ae97f9..42eea6d1e9 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/src/TestRegionTree.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/tla/imp/src/TestRegionTree.scala @@ -63,7 +63,7 @@ class TestRegionTree extends AnyFunSuite { test("find non-existing index") { val tree = new RegionTree() val region = SourceRegion(SourcePosition(1, 20), SourcePosition(3, 10)) - val idx = tree.add(region) + tree.add(region) assertThrows[IndexOutOfBoundsException] { tree(999) } diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala index 9f5ad8efdf..11628d0ef1 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala @@ -93,7 +93,6 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach { } test("""Cardinality(S) >= 1 becomes ~(S = {})""") { - val types = Map("i" -> IntT1(), "S" -> SetT1(IntT1()), "b" -> BoolT1()) val input = ge(card(name("S").as(intSetT)).as(intT), int(1)).as(boolT) val output = optimizer.apply(input) val expected = @@ -102,7 +101,6 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach { } test("""Cardinality(S) /= 0 becomes ~(S = {})""") { - val types = Map("i" -> IntT1(), "S" -> SetT1(IntT1()), "b" -> BoolT1()) val input = ge(card(name("S").as(intSetT)).as(intT), int(1)).as(boolT) val output = optimizer.apply(input) val expected = diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestNormalizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestNormalizer.scala index d300beffbc..9c815b93c2 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestNormalizer.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestNormalizer.scala @@ -6,7 +6,6 @@ import at.forsyte.apalache.tla.lir.IntT1 import at.forsyte.apalache.tla.lir.convenience._ import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.TypedPredefs._ -import at.forsyte.apalache.tla.typecheck._ import org.junit.runner.RunWith import org.scalatestplus.junit.JUnitRunner import org.scalatest.BeforeAndAfterEach diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestConstSubstitution.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestConstSubstitution.scala index 14b8b21373..b54b91b4c3 100644 --- a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestConstSubstitution.scala +++ b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestConstSubstitution.scala @@ -1,7 +1,6 @@ package at.forsyte.apalache.tla.typecheck.etc import at.forsyte.apalache.tla.lir.{ConstT1, IntT1, SeqT1, SetT1, StrT1, TupT1, TypingException} -import at.forsyte.apalache.io.typecheck.parser.{DefaultType1Parser, Type1Parser} import org.junit.runner.RunWith import org.scalatest.funsuite.AnyFunSuite import org.scalatestplus.easymock.EasyMockSugar @@ -9,7 +8,6 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestConstSubstitution extends AnyFunSuite with EasyMockSugar with EtcBuilder { - private val parser: Type1Parser = DefaultType1Parser test("simple substitution") { val sub = ConstSubstitution(Map("A" -> IntT1())) diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala index b25ffabbd6..a76dc6d674 100644 --- a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala +++ b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala @@ -126,8 +126,7 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf val arg = mkUniqConst(BoolT1()) val app = mkUniqApp(Seq(oper), arg) val listener = mock[TypeCheckerListener] - app.typeErrorExplanation = ( - expectedTypes: List[TlaType1], actualTypes: List[TlaType1]) => Some("Mocked explanation") + app.typeErrorExplanation = (_: List[TlaType1], _: List[TlaType1]) => Some("Mocked explanation") val wrapper = wrapWithLet(app) expecting { listener.onTypeError(app.sourceRef.asInstanceOf[ExactRef], "Mocked explanation") @@ -240,8 +239,7 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf val operTypes = Seq(parser("a => Int"), parser("a => Bool")) val arg = mkUniqConst(IntT1()) val app = mkUniqApp(operTypes, arg) - app.typeErrorExplanation = ( - expectedTypes: List[TlaType1], actualTypes: List[TlaType1]) => Some("Mocked explanation") + app.typeErrorExplanation = (_: List[TlaType1], _: List[TlaType1]) => Some("Mocked explanation") val listener = mock[TypeCheckerListener] val wrapper = wrapWithLet(app) expecting { diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala index 47d959ed8b..6c6638f8b5 100644 --- a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala +++ b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala @@ -7,7 +7,6 @@ import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaFunOper} import at.forsyte.apalache.tla.lir.values.TlaReal import at.forsyte.apalache.tla.lir.UntypedPredefs._ -import at.forsyte.apalache.tla.typecheck._ import at.forsyte.apalache.io.typecheck.parser.{DefaultType1Parser, Type1Parser} import org.junit.runner.RunWith import org.scalatestplus.junit.JUnitRunner @@ -98,9 +97,6 @@ class TestToEtcExpr extends AnyFunSuite with BeforeAndAfterEach with EtcBuilder } test("equality and inequality") { - // equality and inequality - val a2ToBool = parser("(a, a) => Bool") - def mkExpected(tt: TlaType1) = mkConstAppByType(tt, parser("Int"), parser("Int")) assert(mkExpected(parser("(a, a) => Bool")) == gen(tla.eql(tla.int(1), tla.int(2)))) @@ -290,8 +286,6 @@ class TestToEtcExpr extends AnyFunSuite with BeforeAndAfterEach with EtcBuilder } test("\\union, \\intersect, \\setminus") { - val binarySetOp = parser("(Set(a), Set(a)) => Set(a)") - def mkExpected(tt: TlaType1) = mkConstAppByType(tt, parser("Set(Int)"), parser("Set(Int)")) assert(mkExpected(parser("(Set(a), Set(a)) => Set(a)")) == gen(tla.cup(tla.intSet(), tla.intSet()))) diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeCheckerTool.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeCheckerTool.scala index 720e84e045..98de9733ff 100644 --- a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeCheckerTool.scala +++ b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeCheckerTool.scala @@ -8,7 +8,7 @@ import at.forsyte.apalache.tla.typecheck.{TypeCheckerListener, TypeCheckerTool} import at.forsyte.apalache.io.annotations.store._ import at.forsyte.apalache.io.json.impl.{DefaultTagReader, TlaToUJson, UJsonToTla} import at.forsyte.apalache.io.lir.TlaType1PrinterPredefs -import at.forsyte.apalache.tla.lir.{TlaModule, TlaType1, Typed, TypingException, UID} +import at.forsyte.apalache.tla.lir.{TlaType1, Typed, TypingException, UID} import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.{TlaType1, Typed, TypingException, UID} import at.forsyte.apalache.tla.typecheck.{TypeCheckerListener, TypeCheckerTool} @@ -36,7 +36,6 @@ class TestTypeCheckerTool extends AnyFunSuite with BeforeAndAfterEach with EasyM private var parser: Type1Parser = _ private val megaSpec = "MegaSpec1" - private val tlcSpec = "TlcSpec1" override def beforeEach() { sourceStore = new SourceStore() diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeUnifier.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeUnifier.scala index 87a65e2474..10826eecf4 100644 --- a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeUnifier.scala +++ b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeUnifier.scala @@ -36,7 +36,6 @@ class TestTypeUnifier extends AnyFunSuite with EasyMockSugar with BeforeAndAfter val sparse2 = parser("{3: Str}") val sparse3 = parser("{2: Int, 3: Str, 4: Bool}") val sparse4 = parser("{1: Int}") - val sparse5 = parser("{1: Int, 2: Bool}") assert(unifier.unify(Substitution.empty, sparse1, sparse2).contains((Substitution.empty, sparse3))) assert(unifier.unify(Substitution.empty, tup1, sparse4).contains((Substitution.empty, tup1))) assert(unifier.unify(Substitution.empty, sparse4, tup1).contains((Substitution.empty, tup1))) diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala index c9936bb7fe..108f37c6e2 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestAux.scala @@ -13,7 +13,6 @@ class TestAux extends AnyFunSuite with TestingPredefs { val ar0Decl1 = TlaOperDecl("X", List.empty, n_x) val ar0Decl2 = TlaOperDecl("Y", List.empty, n_y) - val ar0Decl3 = TlaOperDecl("Z", List.empty, n_z) val arGe0Decl1 = TlaOperDecl("A", List(OperParam("t")), n_a) val arGe0Decl2 = TlaOperDecl("B", List(OperParam("t")), n_b) diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestIncrementalRenaming.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestIncrementalRenaming.scala index a2d7e7bc8d..350675df25 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestIncrementalRenaming.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestIncrementalRenaming.scala @@ -223,8 +223,6 @@ class TestIncrementalRenaming extends AnyFunSuite with TestingPredefs with Befor filter(n_x, n_S, eql(n_x, int(1))), filter(n_x, n_S, eql(n_x, int(2))), ) - val x1 = makeName("x", 1) - val x2 = makeName("x", 2) def expected(offset: Int): TlaEx = cup( diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala index 218e6800cb..7678b6dfd5 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestModule.scala @@ -16,16 +16,16 @@ class TestModule extends AnyFunSuite { test("AlternatingBit module from Lamport's book") { /** CONSTANTS Data */ - val Data = new TlaConstDecl("Data") + new TlaConstDecl("Data") /** VARIABLES msgQ, ackQ, sBit, sAck, rBit, sent, rcvd */ - val msgQ = new TlaVarDecl("msgQ") - val ackQ = new TlaVarDecl("ackQ") - val sBit = new TlaVarDecl("sBit") - val sAck = new TlaVarDecl("sAck") - val rBit = new TlaVarDecl("rBit") - val sent = new TlaVarDecl("sent") - val rcvd = new TlaVarDecl("rcvd") + new TlaVarDecl("msgQ") + new TlaVarDecl("ackQ") + new TlaVarDecl("sBit") + new TlaVarDecl("sAck") + new TlaVarDecl("rBit") + new TlaVarDecl("sent") + new TlaVarDecl("rcvd") /** Constants {0,1} and <<>> */ val ZeroOneSet = OperEx(TlaSetOper.enumSet, ValEx(TlaInt(0)), ValEx(TlaInt(1))) @@ -39,26 +39,24 @@ class TestModule extends AnyFunSuite { * ABInit = /\ msgQ = <<>> /\ ackQ = <<>> /\ sBit \in {0,1} /\ sAck = sBit /\ rBit = sBit /\ sent \in Data /\ rcvd * \in Data */ - val ABInit = - new TlaOperDecl("ABInit", List(), - OperEx(TlaBoolOper.and, OperEx(TlaOper.eq, NameEx("msgQ"), emptySeq), - OperEx(TlaOper.eq, NameEx("ackQ"), emptySeq), OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet), - OperEx(TlaOper.eq, NameEx("sAck"), NameEx("sBit")), OperEx(TlaOper.eq, NameEx("rBit"), NameEx("sBit")), - OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet), OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet))) + new TlaOperDecl("ABInit", List(), + OperEx(TlaBoolOper.and, OperEx(TlaOper.eq, NameEx("msgQ"), emptySeq), + OperEx(TlaOper.eq, NameEx("ackQ"), emptySeq), OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet), + OperEx(TlaOper.eq, NameEx("sAck"), NameEx("sBit")), OperEx(TlaOper.eq, NameEx("rBit"), NameEx("sBit")), + OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet), OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet))) /** * ABTypeInv == /\ msgQ \in Seq( {0,1} \times Data ) /\ ackQ \in Seq( {0,1} ) /\ sBit \in {0,1} /\ sAck \in {0,1} /\ * rBit \in {0,1} /\ sent \in Data /\ rcvd \in Data */ - val ABTypeInv = - new TlaOperDecl("ABTypeInv", List(), - OperEx(TlaBoolOper.and, - OperEx(TlaSetOper.in, NameEx("msgQ"), - OperEx(TlaSetOper.seqSet, OperEx(TlaSetOper.times, ZeroOneSet, NameEx("Data")))), - OperEx(TlaSetOper.in, NameEx("ackQ"), OperEx(TlaSetOper.seqSet, ZeroOneSet)), - OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet), OperEx(TlaSetOper.in, NameEx("sAck"), ZeroOneSet), - OperEx(TlaSetOper.in, NameEx("rBit"), ZeroOneSet), OperEx(TlaSetOper.in, NameEx("sent"), NameEx("Data")), - OperEx(TlaSetOper.in, NameEx("rcvd"), NameEx("Data")))) + new TlaOperDecl("ABTypeInv", List(), + OperEx(TlaBoolOper.and, + OperEx(TlaSetOper.in, NameEx("msgQ"), + OperEx(TlaSetOper.seqSet, OperEx(TlaSetOper.times, ZeroOneSet, NameEx("Data")))), + OperEx(TlaSetOper.in, NameEx("ackQ"), OperEx(TlaSetOper.seqSet, ZeroOneSet)), + OperEx(TlaSetOper.in, NameEx("sBit"), ZeroOneSet), OperEx(TlaSetOper.in, NameEx("sAck"), ZeroOneSet), + OperEx(TlaSetOper.in, NameEx("rBit"), ZeroOneSet), OperEx(TlaSetOper.in, NameEx("sent"), NameEx("Data")), + OperEx(TlaSetOper.in, NameEx("rcvd"), NameEx("Data")))) /** * --------------------------------------------------------------------------------------------------------------- @@ -68,119 +66,110 @@ class TestModule extends AnyFunSuite { * SndNewValue(d) == /\ sAck = sBit /\ sent' = d /\ sBit' = 1 - sBit /\ msgQ' = Append( msgQ, << sBit', d >> ) /\ * UNCHANGED << ackQ, sAck, rBit, rcvd >> */ - val SndNewValue = - new TlaOperDecl("SndNewValue", List(OperParam("d")), - OperEx( - TlaBoolOper.and, - OperEx(TlaOper.eq, NameEx("sAck"), NameEx("sBit")), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("sent")), NameEx("d")), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("sBit")), - OperEx(TlaArithOper.minus, ValEx(TlaInt(1)), NameEx("sBit"))), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("msgQ")), - OperEx(TlaSeqOper.append, NameEx("msgQ"), - OperEx(TlaFunOper.tuple, OperEx(TlaActionOper.prime, NameEx("sBit")), NameEx("d")))), - OperEx(TlaActionOper.unchanged, - OperEx(TlaFunOper.tuple, NameEx("ackQ"), NameEx("sAck"), NameEx("rBit"), NameEx("rcvd"))), - )) + new TlaOperDecl("SndNewValue", List(OperParam("d")), + OperEx( + TlaBoolOper.and, + OperEx(TlaOper.eq, NameEx("sAck"), NameEx("sBit")), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("sent")), NameEx("d")), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("sBit")), + OperEx(TlaArithOper.minus, ValEx(TlaInt(1)), NameEx("sBit"))), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("msgQ")), + OperEx(TlaSeqOper.append, NameEx("msgQ"), + OperEx(TlaFunOper.tuple, OperEx(TlaActionOper.prime, NameEx("sBit")), NameEx("d")))), + OperEx(TlaActionOper.unchanged, + OperEx(TlaFunOper.tuple, NameEx("ackQ"), NameEx("sAck"), NameEx("rBit"), NameEx("rcvd"))), + )) /** * ReSndMsg == /\ sAck # sBit /\ msgQ' = Append( msgQ, << sBit, sent >> ) /\ UNCHANGED << ackQ, sBit, sAck, rBit, * sent, rcvd >> */ - val ReSndMsg = - new TlaOperDecl("ReSndMsg", List(), - OperEx(TlaBoolOper.and, OperEx(TlaOper.ne, NameEx("sAck"), NameEx("sBit")), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("msgQ")), - OperEx(TlaSeqOper.append, NameEx("msgQ"), OperEx(TlaFunOper.tuple, NameEx("sBit"), NameEx("sent")))), - OperEx(TlaActionOper.unchanged, - OperEx(TlaFunOper.tuple, NameEx("ackQ"), NameEx("sBit"), NameEx("sAck"), NameEx("rBit"), - NameEx("sent"), NameEx("rcvd"))))) + new TlaOperDecl("ReSndMsg", List(), + OperEx(TlaBoolOper.and, OperEx(TlaOper.ne, NameEx("sAck"), NameEx("sBit")), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("msgQ")), + OperEx(TlaSeqOper.append, NameEx("msgQ"), OperEx(TlaFunOper.tuple, NameEx("sBit"), NameEx("sent")))), + OperEx(TlaActionOper.unchanged, + OperEx(TlaFunOper.tuple, NameEx("ackQ"), NameEx("sBit"), NameEx("sAck"), NameEx("rBit"), NameEx("sent"), + NameEx("rcvd"))))) /** * RcvMsg == /\ msgQ # <<>> /\ msgQ' = Tail( msgQ ) /\ rBit' = Head( msgQ ) [ 1 ] /\ rcvd' = Head( msgQ ) [ 2 ] /\ * UNCHANGED << ackQ, sBit, sAck, sent >> */ - val RcvMsg = - new TlaOperDecl("RcvMsg", List(), - OperEx( - TlaBoolOper.and, - OperEx(TlaOper.ne, NameEx("msgQ"), emptySeq), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("msgQ")), OperEx(TlaSeqOper.tail, NameEx("msgQ"))), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("rBit")), - OperEx(TlaFunOper.app, OperEx(TlaSeqOper.head, NameEx("msgQ")), ValEx(TlaInt(1)))), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("rcvd")), - OperEx(TlaFunOper.app, OperEx(TlaSeqOper.head, NameEx("msgQ")), ValEx(TlaInt(2)))), - OperEx(TlaActionOper.unchanged, - OperEx(TlaFunOper.tuple, NameEx("ackQ"), NameEx("sBit"), NameEx("sAck"), NameEx("sent"))), - )) + new TlaOperDecl("RcvMsg", List(), + OperEx( + TlaBoolOper.and, + OperEx(TlaOper.ne, NameEx("msgQ"), emptySeq), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("msgQ")), OperEx(TlaSeqOper.tail, NameEx("msgQ"))), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("rBit")), + OperEx(TlaFunOper.app, OperEx(TlaSeqOper.head, NameEx("msgQ")), ValEx(TlaInt(1)))), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("rcvd")), + OperEx(TlaFunOper.app, OperEx(TlaSeqOper.head, NameEx("msgQ")), ValEx(TlaInt(2)))), + OperEx(TlaActionOper.unchanged, + OperEx(TlaFunOper.tuple, NameEx("ackQ"), NameEx("sBit"), NameEx("sAck"), NameEx("sent"))), + )) /** * SndAck == /\ ackQ' = Append( ackQ, rBit ) /\ UNCHANGED << msgQ, sBit, sAck, rBit, sent, rcvd >> */ - val SndAck = - new TlaOperDecl("SndAck", List(), - OperEx(TlaBoolOper.and, - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("ackQ")), - OperEx(TlaSeqOper.append, NameEx("ackQ"), NameEx("rBit"))), - OperEx(TlaActionOper.unchanged, - OperEx(TlaFunOper.tuple, NameEx("msgQ"), NameEx("sBit"), NameEx("sAck"), NameEx("rBit"), - NameEx("sent"), NameEx("rcvd"))))) + new TlaOperDecl("SndAck", List(), + OperEx(TlaBoolOper.and, + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("ackQ")), + OperEx(TlaSeqOper.append, NameEx("ackQ"), NameEx("rBit"))), + OperEx(TlaActionOper.unchanged, + OperEx(TlaFunOper.tuple, NameEx("msgQ"), NameEx("sBit"), NameEx("sAck"), NameEx("rBit"), NameEx("sent"), + NameEx("rcvd"))))) /** * RcvAck == /\ ackQ # <<>> /\ ackQ' = Tail( ackQ ) /\ sAck' = Head( ackQ ) /\ UNCHANGED << msgQ, sBit, rBit, sent, * rcvd >> */ - val RcvAck = - new TlaOperDecl("RcvAck", List(), - OperEx(TlaBoolOper.and, OperEx(TlaOper.ne, NameEx("ackQ"), emptySeq), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("ackQ")), OperEx(TlaSeqOper.tail, NameEx("ackQ"))), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("sAck")), OperEx(TlaSeqOper.head, NameEx("ackQ"))), - OperEx(TlaActionOper.unchanged, - OperEx(TlaFunOper.tuple, NameEx("msgQ"), NameEx("sBit"), NameEx("rBit"), NameEx("sent"), - NameEx("rcvd"))))) + new TlaOperDecl("RcvAck", List(), + OperEx(TlaBoolOper.and, OperEx(TlaOper.ne, NameEx("ackQ"), emptySeq), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("ackQ")), OperEx(TlaSeqOper.tail, NameEx("ackQ"))), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("sAck")), OperEx(TlaSeqOper.head, NameEx("ackQ"))), + OperEx(TlaActionOper.unchanged, + OperEx(TlaFunOper.tuple, NameEx("msgQ"), NameEx("sBit"), NameEx("rBit"), NameEx("sent"), + NameEx("rcvd"))))) /** * Lose( q ) == /\ q # <<>> /\ \exists i \in 1 .. Len( q ) : q' = [ j \in 1 .. ( Len( q ) - 1 ) |-> IF j < i THEN q[ * j ] ELSE q[ j + 1 ] ] /\ UNCHANGED << sBit, sAck, rBit, sent, rcvd >> */ - val Lose = - new TlaOperDecl("Lose", List(OperParam("q")), - OperEx(TlaBoolOper.exists, NameEx("i"), - OperEx(TlaArithOper.dotdot, ValEx(TlaInt(1)), OperEx(TlaSeqOper.len, NameEx("q"))), - OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("q")), - OperEx(TlaFunOper.funDef, NameEx("j"), - OperEx(TlaArithOper.dotdot, ValEx(TlaInt(1)), - OperEx(TlaArithOper.minus, OperEx(TlaSeqOper.len, NameEx("q")), ValEx(TlaInt(1)))), - OperEx(TlaControlOper.ifThenElse, OperEx(TlaArithOper.lt, NameEx("j"), NameEx("i")), - OperEx(TlaFunOper.app, NameEx("q"), NameEx("j")), - OperEx(TlaFunOper.app, NameEx("q"), - OperEx(TlaArithOper.plus, NameEx("j"), ValEx(TlaInt(1))))))))) + new TlaOperDecl("Lose", List(OperParam("q")), + OperEx(TlaBoolOper.exists, NameEx("i"), + OperEx(TlaArithOper.dotdot, ValEx(TlaInt(1)), OperEx(TlaSeqOper.len, NameEx("q"))), + OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx("q")), + OperEx(TlaFunOper.funDef, NameEx("j"), + OperEx(TlaArithOper.dotdot, ValEx(TlaInt(1)), + OperEx(TlaArithOper.minus, OperEx(TlaSeqOper.len, NameEx("q")), ValEx(TlaInt(1)))), + OperEx(TlaControlOper.ifThenElse, OperEx(TlaArithOper.lt, NameEx("j"), NameEx("i")), + OperEx(TlaFunOper.app, NameEx("q"), NameEx("j")), + OperEx(TlaFunOper.app, NameEx("q"), + OperEx(TlaArithOper.plus, NameEx("j"), ValEx(TlaInt(1))))))))) /** * LoseMsg == Lose( msgQ ) /\ UNCHANGED ackQ */ - val LoseMsg = - new TlaOperDecl("LoseMsg", List(), - OperEx(TlaBoolOper.and, OperEx(TlaOper.apply, NameEx("Lose"), NameEx("msgQ")), - OperEx(TlaActionOper.unchanged, NameEx("ackQ")))) + new TlaOperDecl("LoseMsg", List(), + OperEx(TlaBoolOper.and, OperEx(TlaOper.apply, NameEx("Lose"), NameEx("msgQ")), + OperEx(TlaActionOper.unchanged, NameEx("ackQ")))) /** * LoseAck == Lose( ackQ ) /\ UNCHANGED msgQ */ - val LoseAck = - new TlaOperDecl("LoseAck", List(), - OperEx(TlaBoolOper.and, OperEx(TlaOper.apply, NameEx("Lose"), NameEx("ackQ")), - OperEx(TlaActionOper.unchanged, NameEx("msgQ")))) + new TlaOperDecl("LoseAck", List(), + OperEx(TlaBoolOper.and, OperEx(TlaOper.apply, NameEx("Lose"), NameEx("ackQ")), + OperEx(TlaActionOper.unchanged, NameEx("msgQ")))) /** * ABNext == \/ \exists d \in Data : SndNewValue(d) \/ ReSndMsg \/ RcvMsg \/ SndAck \/ RcvAck \/ LoseMsg \/ LoseAck */ - val ABNext = - new TlaOperDecl("ABNext", List(), - OperEx(TlaBoolOper.or, - OperEx(TlaBoolOper.exists, NameEx("d"), NameEx("Data"), - OperEx(TlaOper.apply, NameEx("SndNewValue"), NameEx("d"))), NameEx("ReSndMsg"), NameEx("RcvMsg"), - NameEx("SndAck"), NameEx("RcvAck"), NameEx("LoseMsg"), NameEx("LoseAck"))) + new TlaOperDecl("ABNext", List(), + OperEx(TlaBoolOper.or, + OperEx(TlaBoolOper.exists, NameEx("d"), NameEx("Data"), + OperEx(TlaOper.apply, NameEx("SndNewValue"), NameEx("d"))), NameEx("ReSndMsg"), NameEx("RcvMsg"), + NameEx("SndAck"), NameEx("RcvAck"), NameEx("LoseMsg"), NameEx("LoseAck"))) /** * --------------------------------------------------------------------------------------------------------------- @@ -189,21 +178,19 @@ class TestModule extends AnyFunSuite { /** * abvars == << msgQ, ackQ, sBit, sAck, rBit, sent, rcvd >> */ - val abvars = - new TlaOperDecl("abvars", // NOTE: Is this really an operator? Seems contrived. - List(), - OperEx(TlaFunOper.tuple, NameEx("msgQ"), NameEx("ackQ"), NameEx("sBit"), NameEx("sAck"), NameEx("rBit"), - NameEx("sent"), NameEx("rcvd"))) + new TlaOperDecl("abvars", // NOTE: Is this really an operator? Seems contrived. + List(), + OperEx(TlaFunOper.tuple, NameEx("msgQ"), NameEx("ackQ"), NameEx("sBit"), NameEx("sAck"), NameEx("rBit"), + NameEx("sent"), NameEx("rcvd"))) /** * ABFairness == /\ WF_abvars( ReSndMsg ) /\ WF_abvars( SndAck ) /\ SF_abvars( RcvMsg ) /\ SF_abvars( RcvAck ) */ - val ABFairness = - new TlaOperDecl("AbFairness", List(), - OperEx(TlaBoolOper.and, OperEx(TlaTempOper.weakFairness, NameEx("abvars"), NameEx("ReSndMsg")), - OperEx(TlaTempOper.weakFairness, NameEx("abvars"), NameEx("SndAck")), - OperEx(TlaTempOper.strongFairness, NameEx("abvars"), NameEx("RcvMsg")), - OperEx(TlaTempOper.strongFairness, NameEx("abvars"), NameEx("RcvAck")))) + new TlaOperDecl("AbFairness", List(), + OperEx(TlaBoolOper.and, OperEx(TlaTempOper.weakFairness, NameEx("abvars"), NameEx("ReSndMsg")), + OperEx(TlaTempOper.weakFairness, NameEx("abvars"), NameEx("SndAck")), + OperEx(TlaTempOper.strongFairness, NameEx("abvars"), NameEx("RcvMsg")), + OperEx(TlaTempOper.strongFairness, NameEx("abvars"), NameEx("RcvAck")))) /** * --------------------------------------------------------------------------------------------------------------- @@ -213,10 +200,9 @@ class TestModule extends AnyFunSuite { * ABSpec == ABInit /\ [][ABNext]_abvars /\ ABFairness */ - val ABSpec = - new TlaOperDecl("ABSpec", List(), - OperEx(TlaBoolOper.and, NameEx("ABInit"), OperEx(TlaActionOper.stutter, NameEx("ABNext"), NameEx("abvars")), - NameEx("ABFairness"))) + new TlaOperDecl("ABSpec", List(), + OperEx(TlaBoolOper.and, NameEx("ABInit"), OperEx(TlaActionOper.stutter, NameEx("ABNext"), NameEx("abvars")), + NameEx("ABFairness"))) /** * --------------------------------------------------------------------------------------------------------------- diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala index 692cd91361..63e2734cc5 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala @@ -45,7 +45,6 @@ class TestTlaDeclLevelFinder extends AnyFunSuite with Checkers { val prop = forAll(gens.genTlaModule(gens.genTlaEx(operators))) { module => val finder = new TlaDeclLevelFinder(module) - val vars = module.varDeclarations.map(_.name).toSet def expectedLevel(decl: TlaOperDecl): Prop = { val level = finder(decl) diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala index ab7783a413..d90736ed07 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExpr.scala @@ -162,6 +162,7 @@ class TestTlaExpr extends AnyFunSuite { } } + // TODO What are these testing? Just that no exceptions are thrown? test("declaring an order 2 operator") { // f(_, _) val fOper = OperParam("f", 2) @@ -183,7 +184,7 @@ class TestTlaExpr extends AnyFunSuite { OperEx(TlaBoolOper.existsUnbounded, NameEx("x"), OperEx(TlaOper.eq, NameEx("x"), NameEx("x"))) val ex2 = OperEx(TlaBoolOper.existsUnbounded, NameEx("x"), OperEx(TlaOper.eq, NameEx("x"), NameEx("x"))) - val conj = OperEx(TlaBoolOper.and, ex1, ex2) + OperEx(TlaBoolOper.and, ex1, ex2) } } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTransformations.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTransformations.scala index ec9e14d1a9..13ee6d864c 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTransformations.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTransformations.scala @@ -1,6 +1,5 @@ package at.forsyte.apalache.tla.lir -import at.forsyte.apalache.tla.lir.storage.BodyMapFactory import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard._ import at.forsyte.apalache.tla.lir.convenience._ diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/impl/TestStableTopologicalSort.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/impl/TestStableTopologicalSort.scala index 7812ef02b3..f3c181ab9c 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/impl/TestStableTopologicalSort.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/impl/TestStableTopologicalSort.scala @@ -19,7 +19,7 @@ class TestStableTopologicalSort extends AnyFunSuite with BeforeAndAfterEach with uses <- Gen.listOfN(size, Gen.choose(0, size - 1)) // the declarations below the threshold do not refer to other declarations threshold <- Gen.choose(0, size - 1) - } yield nodes.zip(uses).map { case (n, i) => + } yield nodes.zip(uses).map { case (_, i) => // either no dependencies or a single dependency if (i <= threshold) (i, Set.empty[Int]) else (i, Set(uses(i))) } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala index 3dd6455e70..62a891be67 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestFlatLanguagePred.scala @@ -23,9 +23,9 @@ class TestFlatLanguagePred extends LanguagePredTestSuite { test("a non-nullary let-in ") { val app = tla.appOp(tla.name("UserOp"), tla.int(3)) - val letIn = + val letin = tla.letIn(app, tla.declOp("UserOp", tla.plus(tla.int(1), tla.name("x")), OperParam("x")).untypedOperDecl()) - expectFail(pred.isExprOk(app)) + expectFail(pred.isExprOk(letin)) } test("a nullary let-in ") {