Skip to content

Commit

Permalink
Bugfix for #2747 (#2748)
Browse files Browse the repository at this point in the history 
* Intermediate cell type fix

* .

* Fixed tests containing Untyped

* PR suggestion

* fmt
  • Loading branch information
@Kukovec
Kukovec authored Oct 10, 2023
1 parent 9ec6f9e commit 5316435
Show file tree
Hide file tree
Showing 4 changed files with 48 additions and 41 deletions.
8 changes: 4 additions & 4 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PrimeRule.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.rules

import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.oper.TlaActionOper
import at.forsyte.apalache.tla.lir.{NameEx, OperEx}
import at.forsyte.apalache.tla.lir.UntypedPredefs._
import at.forsyte.apalache.tla.lir.{NameEx, OperEx, TlaType1}
import at.forsyte.apalache.tla.types.tla

/**
* Rename x' to NameEx("x'"). We only consider the case when prime is applied to a variable.
Expand All @@ -21,8 +21,8 @@ class PrimeRule extends RewritingRule {

override def apply(state: SymbState): SymbState = {
state.ex match {
case OperEx(TlaActionOper.prime, NameEx(name)) =>
state.setRex(NameEx(name + "'"))
case OperEx(TlaActionOper.prime, nEx @ NameEx(name)) =>
state.setRex(tla.name(name + "'", TlaType1.fromTypeTag(nEx.typeTag)))

case _ =>
throw new RewriterException("Prime operator is only implemented for variables", state.ex)
Expand Down
3 changes: 1 addition & 2 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ package at.forsyte.apalache.tla.bmcmt.rules

import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.NameEx
import at.forsyte.apalache.tla.lir.UntypedPredefs._
import at.forsyte.apalache.tla.pp.TlaInputError
import com.typesafe.scalalogging.LazyLogging

Expand All @@ -29,7 +28,7 @@ class SubstRule extends RewritingRule with LazyLogging {
case NameEx(x) =>
if (state.binding.contains(x)) {
val cell = state.binding(x)
state.setRex(NameEx(cell.toString))
state.setRex(cell.toBuilder)
} else {
logger.error("This error may show up when CONSTANTS are not initialized.")
logger.error("Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html")
Expand Down
9 changes: 4 additions & 5 deletions tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,18 +2,17 @@ package at.forsyte.apalache.tla.bmcmt

import at.forsyte.apalache.infra.passes.options.SMTEncoding
import at.forsyte.apalache.tla.bmcmt.SymbStateRewriter.Continue
import at.forsyte.apalache.tla.lir.{IntT1, NameEx}
import at.forsyte.apalache.tla.lir.convenience._
import at.forsyte.apalache.tla.lir.UntypedPredefs._
import at.forsyte.apalache.tla.lir.IntT1
import at.forsyte.apalache.tla.types.tla

trait TestSymbStateRewriterAction extends RewriterBase {
test("""x' is rewritten to the binding of x'""") { rewriterType: SMTEncoding =>
val rewriter = create(rewriterType)
arena.appendCell(IntT1) // the type finder is strict about unassigned types, so let's create a cell for x'
val state = new SymbState(tla.prime(NameEx("x")), arena, Binding("x'" -> arena.topCell))
val state = new SymbState(tla.prime(tla.name("x", IntT1)), arena, Binding("x'" -> arena.topCell))
rewriter.rewriteOnce(state) match {
case Continue(next) =>
assert(next.ex == NameEx("x'"))
assert(next.ex == tla.name("x'", IntT1).build)

case _ =>
fail("Expected x to be renamed to x'")
Expand Down
69 changes: 39 additions & 30 deletions tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.trex

import at.forsyte.apalache.tla.bmcmt.{Binding, StateInvariant}
import at.forsyte.apalache.tla.lir._
import at.forsyte.apalache.tla.lir.convenience.tla
import at.forsyte.apalache.tla.lir.UntypedPredefs._
import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
import at.forsyte.apalache.tla.types.tla

/**
* An abstract test suite that is parameterized by the snapshot type.
Expand All @@ -15,14 +15,18 @@ import at.forsyte.apalache.tla.lir.UntypedPredefs._
* the snapshot type
*/
trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {

def nX: TBuilderInstruction = tla.name("x", IntT1)
def nY: TBuilderInstruction = tla.name("y", IntT1)

test("constant initialization") { exeCtx: ExecutorContextT =>
// N' <- 1
val trex = new TransitionExecutorImpl(Set("N"), Set("x", "y"), exeCtx)
trex.debug = true
assert(trex.stepNo == 0)
val constInit = mkAssign("N", 10)
trex.initializeConstants(constInit)
val init = tla.and(mkAssign("x", tla.name("N")), mkAssign("y", 1))
val init = tla.and(mkAssignInt("x", tla.name("N", IntT1)), mkAssign("y", 1))
// init is a potential transition with index 3 (the index is defined by the input spec)
val isTranslated = trex.prepareTransition(3, init)
assert(isTranslated)
Expand All @@ -32,7 +36,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
trex.nextState()
assert(trex.stepNo == 1)
// assert something about the current state
trex.assertState(tla.eql(tla.name("x"), tla.int(5)))
trex.assertState(tla.eql(nX, tla.int(5)))
assert(trex.sat(60).contains(false))
}

Expand All @@ -51,13 +55,13 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
trex.nextState()
assert(trex.stepNo == 1)
// assert something about the current state
trex.assertState(tla.eql(tla.name("y"), tla.int(1)))
trex.assertState(tla.eql(nY, tla.int(1)))
assert(trex.sat(60).contains(true))
}

test("check enabled and discard") { exeCtx: ExecutorContextT =>
// an obviously disabled transition: y' <- 1 /\ y' <- 2
val init = tla.and(mkAssign("y", 1), tla.eql(tla.prime(tla.name("y")), tla.int(2)), mkAssign("x", 3))
val init = tla.and(mkAssign("y", 1), tla.eql(tla.prime(nY), tla.int(2)), mkAssign("x", 3))
val trex = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx)
trex.debug = true
assert(trex.stepNo == 0)
Expand All @@ -83,7 +87,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
// create a snapshot for a later rollback
val snapshot = trex.snapshot()
// assert invariant violation and check it
val notInv = tla.not(tla.eql(tla.prime(tla.name("y")), tla.prime(tla.name("x"))))
val notInv = tla.not(tla.eql(tla.prime(nY), tla.prime(nX)))
trex.assertState(notInv)
assert(trex.sat(60).contains(false))
// rollback the snapshot
Expand All @@ -96,8 +100,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
// x' <- 1 /\ y' <- 1
val init: TlaEx = tla.and(mkAssign("y", 1), mkAssign("x", 1))
// x' <- y /\ y' <- x + y
val trans1: TlaEx = tla.and(mkAssign("x", tla.name("y")), mkAssign("y", tla.plus(tla.name("x"), tla.name("y"))))
val trans2: TlaEx = tla.and(mkAssign("x", tla.name("x")), mkAssign("y", tla.name("y")))
val trans1: TlaEx =
tla.and(mkAssignInt("x", nY), mkAssignInt("y", tla.plus(nX, nY)))
val trans2: TlaEx = tla.and(mkAssignInt("x", nX), mkAssignInt("y", nY))
val trex = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx)
trex.prepareTransition(1, init)
trex.pickTransition()
Expand All @@ -123,17 +128,21 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
assert(Binding().toMap == decPath(0)._1)
// state 1 is produced by transition 1
assert(1 == decPath(1)._2)
assert(Map("x" -> tla.int(1).untyped(), "y" -> tla.int(1).untyped()) == decPath(1)._1)

def mapWithBuild(pairs: (String, TBuilderInstruction)*): Map[String, TlaEx] =
pairs.map { case (a, b) => a -> b.build }.toMap

assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(1)) == decPath(1)._1)
// state 2 is produced by transition 1
assert(1 == decPath(2)._2)
assert(Map("x" -> tla.int(1).untyped(), "y" -> tla.int(2).untyped()) == decPath(2)._1)
assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(2)) == decPath(2)._1)
// state 3 is produced by transition 1
assert(1 == decPath(3)._2)
assert(Map("x" -> tla.int(2).untyped(), "y" -> tla.int(3).untyped()) == decPath(3)._1)
assert(mapWithBuild("x" -> tla.int(2), "y" -> tla.int(3)) == decPath(3)._1)
// state 4 is produced either by transition 1, or by transition 2
assert(1 == decPath(4)._2 || 2 == decPath(4)._2)
assert(Map("x" -> tla.int(2).untyped(), "y" -> tla.int(3).untyped()) == decPath(4)._1
|| Map("x" -> tla.int(3).untyped(), "y" -> tla.int(5).untyped()) == decPath(4)._1)
assert(mapWithBuild("x" -> tla.int(2), "y" -> tla.int(3)) == decPath(4)._1
|| mapWithBuild("x" -> tla.int(3), "y" -> tla.int(5)) == decPath(4)._1)

// test the symbolic execution
val exe = trex.execution
Expand All @@ -143,23 +152,23 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {

// state 1 is the state right after Init, that is, Init(state0)
val state1 = exe.path(1)._1
assertValid(trex, tla.eql(state1("x").toNameEx, tla.int(1)))
assertValid(trex, tla.eql(state1("y").toNameEx, tla.int(1)))
assertValid(trex, tla.eql(state1("x").toBuilder, tla.int(1)))
assertValid(trex, tla.eql(state1("y").toBuilder, tla.int(1)))

// state 2 is the state Next(Init(state0))
val state2 = exe.path(2)._1
assertValid(trex, tla.eql(state2("x").toNameEx, tla.int(1)))
assertValid(trex, tla.eql(state2("y").toNameEx, tla.int(2)))
assertValid(trex, tla.eql(state2("x").toBuilder, tla.int(1)))
assertValid(trex, tla.eql(state2("y").toBuilder, tla.int(2)))

// state 3 is the state Next(Next(Init(state0)))
val state3 = exe.path(3)._1
assertValid(trex, tla.eql(state3("x").toNameEx, tla.int(2)))
assertValid(trex, tla.eql(state3("y").toNameEx, tla.int(3)))
assertValid(trex, tla.eql(state3("x").toBuilder, tla.int(2)))
assertValid(trex, tla.eql(state3("y").toBuilder, tla.int(3)))

// state 4 is the state Next(Next(Next(Init(state0)))
val state4 = exe.path(4)._1
assertValid(trex, tla.or(tla.eql(state4("x").toNameEx, tla.int(2)), tla.eql(state4("x").toNameEx, tla.int(3))))
assertValid(trex, tla.or(tla.eql(state4("y").toNameEx, tla.int(3)), tla.eql(state4("y").toNameEx, tla.int(5))))
assertValid(trex, tla.or(tla.eql(state4("x").toBuilder, tla.int(2)), tla.eql(state4("x").toBuilder, tla.int(3))))
assertValid(trex, tla.or(tla.eql(state4("y").toBuilder, tla.int(3)), tla.eql(state4("y").toBuilder, tla.int(5))))

// regression in multi-core
val snapshot = trex.snapshot()
Expand All @@ -177,7 +186,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
// x' <- 1 /\ y' <- 1
val init = tla.and(mkAssign("y", 1), mkAssign("x", 1))
// x' <- x /\ y' <- x + y
val nextTrans = tla.and(mkAssign("x", tla.name("x")), mkAssign("y", tla.plus(tla.name("x"), tla.name("y"))))
val nextTrans = tla.and(mkAssignInt("x", nX), mkAssignInt("y", tla.plus(nX, nY)))
// push Init
val trex = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx)
trex.prepareTransition(1, init)
Expand All @@ -186,10 +195,10 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
// prepare Next
trex.prepareTransition(1, nextTrans)
// check what has changed
val inv0 = tla.ge(tla.name("x"), tla.int(3))
val inv0 = tla.ge(nX, tla.int(3))
val mayChange0 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0)
assert(!mayChange0)
val inv1 = tla.ge(tla.name("y"), tla.name("x"))
val inv1 = tla.ge(nY, nX)
val mayChange1 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1)
assert(mayChange1)
}
Expand All @@ -198,7 +207,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
// y' <- 1
val init = tla.and(mkAssign("y", 1))
// y' <- y + 1
val nextTrans = mkAssign("y", tla.plus(tla.name("y"), tla.int(1)))
val nextTrans = mkAssignInt("y", tla.plus(nY, tla.int(1)))
// push Init
val trex = new TransitionExecutorImpl(Set.empty, Set("y"), exeCtx)
trex.prepareTransition(1, init)
Expand All @@ -216,9 +225,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] {
assert(!mayChange2)
}

private def mkAssign(name: String, value: Int) =
tla.assignPrime(tla.name(name), tla.int(value))
private def mkAssign(name: String, value: Int): TBuilderInstruction =
tla.assign(tla.prime(tla.name(name, IntT1)), tla.int(value))

private def mkAssign(name: String, rhs: TlaEx) =
tla.assignPrime(tla.name(name), rhs)
private def mkAssignInt(name: String, rhs: TBuilderInstruction) =
tla.assign(tla.prime(tla.name(name, IntT1)), rhs)
}

0 comments on commit 5316435

Please sign in to comment.