Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Bugfix for #2747 #2748

Merged
merged 7 commits into from
Oct 10, 2023
Merged

Bugfix for #2747 #2748

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
466953e
Intermediate cell type fix
Kukovec Sep 26, 2023
901aa2e
.
Kukovec Sep 26, 2023
05d2fe2
Fixed tests containing Untyped
Kukovec Oct 10, 2023
3eb00dc
PR suggestion
Kukovec Oct 10, 2023
a56c29d
Merge branch 'main' into jk/2747
Kukovec Oct 10, 2023
0180e47
fmt
Kukovec Oct 10, 2023
9af1495
Merge branch 'main' into jk/2747
Kukovec Oct 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/PrimeRule.scala
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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)
}
Loading