Simulator: fix evaluation of "deadlock"/"init" labels in property formulas#282
Merged
Conversation
The statistical model checking engine did not support the built-in "deadlock" label (e.g. P=?[F "deadlock"]), because it cannot be treated in the same way as user-defined labels, where these are replaced with their (Expression) definitions before simulation. The solution is in two parts: (i) Add getLabelValue(String) to EvaluateContext (returning null by default, meaning unsupported), used in ExpressionLabel.evaluate(). (ii) Path.evaluateBooleanInCurrentState can now also take a ModelGenerator allowing it to reason about transitions in the current state (notably using modelGen.isDeadlock()).
Re-using mechanism just added to support "deadlock", allow the statistical model checking engine to check "init". Only supports models with a single initial state for now (as does the simulator). Not super efficient, but ok for now.
There were some errors in path evaluation for time-bounded properties.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The statistical model checking (simulation) engine crashed when properties referenced the built-in
"deadlock"or"init"labels (e.g.P=?[F "deadlock"]), becauseExpressionLabel.evaluate()always threw"Cannot evaluate labels". Unlike user-defined labels, these two are never expanded to a Boolean state formula byexpandPropRefsAndLabels—"deadlock"depends on available transitions and"init"on the initial state, neither of which is a function of state variables alone.getLabelValue(String)hook toEvaluateContext(returnsnullby default = unsupported).ExpressionLabel.evaluate()now calls this hook first and only throws if it returnsnull.Path.evaluateBooleanInCurrentState(Expression, ModelGenerator), which provides a label-aware context:"deadlock"delegates toModelGenerator.isDeadlock(),"init"to a newModelGenerator.isInitialState()helper, and other labels toModelGenerator.isLabelTrue(). Compound expressions like"deadlock" & s=7work correctly since the context is applied recursively by the expression evaluator.SamplerUntil,SamplerBoundedUntilDisc,SamplerBoundedUntilCont,SamplerNext) to use this overload.fixDeadlocksis off, report the deadlock state and throw an error (matching the behaviour of the non-simulation engines).Test plan
./bin/prism dice-deadlock.prism -pf 'P=?[F "deadlock"]' -sim— previously crashed; now returns1.0./bin/prism dice-deadlock.prism -pf 'P=?[F "deadlock"]' -ex— cross-check against explicit engine (also1.0)prism-tests/bugfixes/sim-deadlock-label.*andprism-tests/functionality/verify/sim/sim-deadlock-*.*pass on both-simand-exchain.prism,samplerboundeduntildisc.pm,sim-ctmc-until-false.prism) unaffectedmake unittests— all 25 480 tests pass🤖 Generated with Claude Code