From 17863ef170f0b61ba6ebb503103d93a4f3e61229 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 14 Oct 2020 21:55:57 +0100 Subject: [PATCH] Enable (explicit engine) model checking of LTSs. There is no explicit model type keyword added to the parser. Instead, LTSs are auto-detected by the absence of probabilities. ConstructModel is extended to build LTSs. Model checking (CTL+LTL) can be done out of the box using the existing NonProbModelChecker class. A few MDP regression tests are clarified to make it clear that the models are MDPs, not LTSs. --- .../functionality/testing/testing.prism | 2 +- .../mdps/multi-general/test-cumulative1.nm | 2 ++ prism/src/explicit/ConstructModel.java | 17 +++++++-- prism/src/explicit/StateModelChecker.java | 3 ++ prism/src/parser/ast/ModulesFile.java | 35 +++++++++++++++++-- prism/src/prism/Prism.java | 30 ++++++++++++++++ prism/tests/lec9ctl1.prism | 17 +++++++++ prism/tests/lec9ctl1.prism.props | 16 +++++++++ 8 files changed, 116 insertions(+), 6 deletions(-) create mode 100644 prism/tests/lec9ctl1.prism create mode 100644 prism/tests/lec9ctl1.prism.props diff --git a/prism-tests/functionality/testing/testing.prism b/prism-tests/functionality/testing/testing.prism index d3449816..9d1bd832 100644 --- a/prism-tests/functionality/testing/testing.prism +++ b/prism-tests/functionality/testing/testing.prism @@ -4,6 +4,6 @@ module M x : [0..1] init 0; - [] x=0 -> true; + [] x=0 -> 1.0:true; endmodule diff --git a/prism-tests/functionality/verify/mdps/multi-general/test-cumulative1.nm b/prism-tests/functionality/verify/mdps/multi-general/test-cumulative1.nm index 1cfc9ba4..adcb16a7 100644 --- a/prism-tests/functionality/verify/mdps/multi-general/test-cumulative1.nm +++ b/prism-tests/functionality/verify/mdps/multi-general/test-cumulative1.nm @@ -2,6 +2,8 @@ // The model is in fact a MC // We also check -lp although it does not support the feature, but the testing ensures that an exception (and not a wrong result) is given. +mdp + module M x:[0..4] init 0; diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index c262054c..e5a46c99 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -170,6 +170,7 @@ public class ConstructModel extends PrismComponent CTMCSimple ctmc = null; MDPSimple mdp = null; CTMDPSimple ctmdp = null; + LTSSimple lts = null; ModelExplicit model = null; Distribution distr = null; // Misc @@ -207,10 +208,12 @@ public class ConstructModel extends PrismComponent case CTMDP: modelSimple = ctmdp = new CTMDPSimple(); break; + case LTS: + modelSimple = lts = new LTSSimple(); + break; case STPG: case SMG: case PTA: - case LTS: throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s"); } // Attach variable info @@ -273,10 +276,16 @@ public class ConstructModel extends PrismComponent case CTMDP: distr.add(dest, modelGen.getTransitionProbability(i, j)); break; + case LTS: + if (distinguishActions) { + lts.addActionLabelledTransition(src, dest, modelGen.getChoiceAction(i)); + } else { + lts.addTransition(src, dest); + } + break; case STPG: case SMG: case PTA: - case LTS: throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s"); } } @@ -354,10 +363,12 @@ public class ConstructModel extends PrismComponent case CTMDP: model = sortStates ? new CTMDPSimple(ctmdp, permut) : ctmdp; break; + case LTS: + model = sortStates ? new LTSSimple(lts, permut) : lts; + break; case STPG: case SMG: case PTA: - case LTS: throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s"); } model.setStatesList(statesList); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index f73b6283..657e5753 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -196,6 +196,9 @@ public class StateModelChecker extends PrismComponent case STPG: mc = new STPGModelChecker(parent); break; + case LTS: + mc = new NonProbModelChecker(parent); + break; default: throw new PrismException("Cannot create model checker for model type " + modelType); } diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 5de6d999..03fb42bd 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -37,6 +37,7 @@ import parser.State; import parser.Values; import parser.VarList; import parser.type.Type; +import parser.visitor.ASTTraverse; import parser.visitor.ASTVisitor; import parser.visitor.ModulesFileSemanticCheck; import parser.visitor.ModulesFileSemanticCheckAfterConstants; @@ -1287,9 +1288,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato */ private void finaliseModelType() { - // Default (if unspecified) is MDP + // If unspecified, auto-detect model type if (modelTypeInFile == null) { - modelType = ModelType.MDP; + boolean nonProb = isNonProbabilistic(); + // MDP/LTS depending if probabilistic + modelType = nonProb ? ModelType.LTS : ModelType.MDP; } // Otherwise, it's just whatever was specified else { @@ -1297,6 +1300,34 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato } } + /** + * Check whether this model is non-probabilistic, + * i.e., whether none of the commands are probabilistic. + */ + private boolean isNonProbabilistic() + { + try { + // Search through commands, checking for probabilities + accept(new ASTTraverse() + { + public Object visit(Updates e) throws PrismLangException + { + int n = e.getNumUpdates(); + for (int i = 0; i < n; i++) { + if (e.getProbability(i) != null) { + throw new PrismLangException("Found one"); + } + } + visitPost(e); + return null; + } + }); + } catch (PrismLangException e) { + return false; + } + return true; + } + // Methods required for ASTElement: /** diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 787bb574..b00b7b77 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -285,6 +285,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Has the CUDD library been initialised yet? private boolean cuddStarted = false; + // Info about automatic engine switching + private int engineOld = -1; + private boolean engineSwitched = false; + //------------------------------------------------------------------------------ // Constructors + options methods //------------------------------------------------------------------------------ @@ -1783,6 +1787,32 @@ public class Prism extends PrismComponent implements PrismSettingsListener } mainLog.println(); + // For some models, automatically switch engine + switch (currentModelType) { + case LTS: + if (!getExplicit()) { + mainLog.println("\nSwitching to explicit engine, which supports " + currentModelType + "s..."); + engineOld = getEngine(); + engineSwitched = true; + try { + setEngine(Prism.EXPLICIT); + } catch (PrismException e) { + // Won't happen + } + } + break; + // For other models, switch engine back if changed earlier + default: + if (engineSwitched) { + try { + setEngine(engineOld); + } catch (PrismException e) { + // Won't happen + } + engineSwitched = false; + } + } + // If required, export parsed PRISM model if (exportPrism) { try { diff --git a/prism/tests/lec9ctl1.prism b/prism/tests/lec9ctl1.prism new file mode 100644 index 00000000..90226269 --- /dev/null +++ b/prism/tests/lec9ctl1.prism @@ -0,0 +1,17 @@ +// Simple LTS from Lec 9 of Computer-Aided Verification + +module M + +s:[0..3]; + +[] s=0 -> (s'=1); +[] s=0 -> (s'=2); +[] s=1 -> (s'=1); +[] s=1 -> (s'=3); +[] s=2 -> (s'=1); +[] s=3 -> (s'=3); + +endmodule + +label "a" = s=0 | s=1; +label "b" = s=0 | s=3; diff --git a/prism/tests/lec9ctl1.prism.props b/prism/tests/lec9ctl1.prism.props new file mode 100644 index 00000000..cfea1136 --- /dev/null +++ b/prism/tests/lec9ctl1.prism.props @@ -0,0 +1,16 @@ +// Simple LTS from Lec 9 of Computer-Aided Verification + +// RESULT: ? +"ex": A[ X "a" ] & E[ X !"b"]; +// RESULT: true +filter(forall, "ex" <=> (s=2)); + +// RESULT: ? +"ex_lhs": A[ X "a" ] +// RESULT: true +filter(forall, "ex_lhs" <=> (s=2)); + +// RESULT: ? +"ex_rhs": E[ X !"b"]; +// RESULT: true +filter(forall, "ex_rhs" <=> (s=0|s=1|s=2));