New abstraction layer: transition executor #432
Conversation
…d ExecutionSnapshot
CHANGES.md
Outdated
| - Compile the manuals into [a static | ||
| site](http://informalsystems.github.io/apalache/docs/) using | ||
| [mdBook](https://github.com/rust-lang/mdBook), see #400 | ||
| - ADR003: [Architecture of TransitionExecutor](./docs/internal/adr/003adr-trex.md) |
There was a problem hiding this comment.
This will conflict with #419
There was a problem hiding this comment.
True. I will have to resolve that.
Co-authored-by: Shon Feder <[email protected]>
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/RecordingZ3SolverContext.scala
Outdated
Show resolved
Hide resolved
|
|
||
| /** | ||
| * The sequence of logs (the last added element is in the head), | ||
| * one per context, except the last log, which is maintained in lastLog. |
There was a problem hiding this comment.
I don't see any lastLog in this module. Am I missing it? Or does doc need a tweak? Should this be lastLogRev?
| * one per context, except the last log, which is maintained in lastLog. | ||
| * Every list in logStackRev is stored in the reverse order. | ||
| */ | ||
| private var logStackRev: List[List[Record]] = List() |
There was a problem hiding this comment.
Just a nit on naming, but if, conceptually, this is a stack, then it seems like needlessly exposing an implementation detail to prefix the name with rev, cause we'd expect the last added item to be on the top of the stack.
There was a problem hiding this comment.
It is indeed a confusing name. Changed it to stackOfInverseLogs to stress that every log on the stack is in the inverse order.
| /** | ||
| * The current log, the last added element is in the head. | ||
| */ | ||
| private var lastLogRev: List[Record] = List() |
There was a problem hiding this comment.
Same nit re: naming here.
Is this lastLog meaning the most recent log, that should be the head of logStack? If so, why do we keep that in a separate variable? Getting the head of the logStack should be trivial, right? If we do indeed need this pointer to the head element for some reason, I think a line or two up here explaining to the reader why we need it would be helpful.
There was a problem hiding this comment.
It is hard to justify why I did it like that. It was months ago. I am going to refactor the code as you are suggesting. Good catch!
| lastLogRev = logStackRev.head | ||
| logStackRev = logStackRev.tail |
There was a problem hiding this comment.
- Why not define this as
pop(1)? - Wont these crash when the stack is empty? Afaict, nothing ensures the logs won't be empty. Unless something guarantees this invariant, should either raise a clear exception when trying to pop a nonempty stack or (better, if not too inconvenient), make
pop(): Optional[Unit](same goes forpop n.
There was a problem hiding this comment.
Totally true. I will add an exception on the empty log. This would be an irrecoverable error though.
| * @param cell a (previously undeclared) cell | ||
| */ | ||
| override def declareCell(cell: ArenaCell): Unit = { | ||
| lastLogRev = DeclareCellRecord(cell) :: lastLogRev |
There was a problem hiding this comment.
Seems like it might be cleaner to abstract this mutable stack pushing by adding a method like push(r: Record): Unit that took care of the consing and mutation of lastLogRev.
There was a problem hiding this comment.
Yep. Added appendToTopLog.
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/RecordingZ3SolverContext.scala
Outdated
Show resolved
Hide resolved
| * @return Some(result), if no timeout happened; otherwise, None | ||
| */ | ||
| override def satOrTimeout(timeoutSec: Long): Option[Boolean] = { | ||
| solver.satOrTimeout(timeoutSec) |
There was a problem hiding this comment.
Too bad all these passthrough's are needed and we can't just inherit the methods. Makes for a lot of boilerplate!
There was a problem hiding this comment.
True. It is weird. However, this wrapper should work for any SolverContext, not just Z3SolverContext. I should refactor it to either directly inherit from Z3SolverContext, or wrap an arbitrary SolverContext. I would prefer the latter.
There was a problem hiding this comment.
I've renamed RecordingZ3SolverContext to RecordingSolverContext and introduced the factory method RecordingSolveContext.createZ3.
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SmtLog.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Shon Feder <[email protected]>
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/RecordingSolverContext.scala
Show resolved
Hide resolved
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala
Outdated
Show resolved
Hide resolved
| * <p>A general-purpose symbolic transition executor (or T-Rex). | ||
| * It accumulates the basic logic for executing TLA+ | ||
| * transitions, which is used both in the sequential and parallel model checkers. | ||
| * (It could be used to implement predicate abstraction too.) | ||
| * This class is imperative, as taking SMT snapshots and recovering them | ||
| * in the non-incremental case is far from being functional.</p> | ||
| * | ||
| * <p>This class is parameterized by the type of an executor context. Currently, there are two choices: | ||
| * (1) IncrementalExecutorContext and (2) OfflineExecutorContext.</p> | ||
| * |
There was a problem hiding this comment.
Do we need to duplicate the doc comments? Would be nice if we could just have them written in one place. E.g., perhaps this could just refer the reader to the documentation on the trait?
There was a problem hiding this comment.
Right. I think Intellij Idea is copy-pasting the docs. Will fix that.
| lastState = nextState.setBinding(finalVarBinding ++ constBinding) | ||
| // the sparse oracle is mapping the oracle values to the transition numbers | ||
| val sparseOracle = new SparseOracle(oracle, preparedTransitions.keySet) | ||
| revStack = (lastState.binding.shiftBinding(consts), sparseOracle) :: revStack |
There was a problem hiding this comment.
I guess the same nits re: naming and abstracting pushing to the stack could apply through this file, but that's non-essential of course.
There was a problem hiding this comment.
Good point. Fixed that too.
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Shon Feder <[email protected]>
|
Thanks for the comprehensive review @shonfeder. I cannot wait for the next PR, where this transition executor is integrated with the model checker. |
This is a copy of the transition executor, which has been introduced some time ago in ik/multicore. It contains a very nice abstraction layer. This layer has not been plugged into the current model checker. It will be plugged in the future PRs.
This layer may be also useful for more targeted model-based testing.
This PR also includes ADR003 that describes how the transition executor is working.