From 4c13267ded0aa46d0053b6a541694875ea3f50e2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 10 Dec 2015 01:45:22 +0000 Subject: [PATCH] Add test methods for special cases in ExpressionLabels. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11028 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 6 +++--- prism/src/param/ParamModelChecker.java | 8 ++++---- prism/src/parser/ast/ExpressionLabel.java | 16 ++++++++++++++++ .../GetAllUndefinedConstantsRecursively.java | 2 +- prism/src/prism/StateModelChecker.java | 6 +++--- prism/src/pta/PTAModelChecker.java | 4 ++-- 6 files changed, 29 insertions(+), 13 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 5b017e4f..60b30891 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -746,14 +746,14 @@ public class StateModelChecker extends PrismComponent int i; // treat special cases - if (expr.getName().equals("deadlock")) { + if (expr.isDeadlockLabel()) { int numStates = model.getNumStates(); BitSet bs = new BitSet(numStates); for (i = 0; i < numStates; i++) { bs.set(i, model.isDeadlockState(i)); } return StateValues.createFromBitSet(bs, model); - } else if (expr.getName().equals("init")) { + } else if (expr.isInitLabel()) { int numStates = model.getNumStates(); BitSet bs = new BitSet(numStates); for (i = 0; i < numStates; i++) { @@ -824,7 +824,7 @@ public class StateModelChecker extends PrismComponent throw new PrismException("Filter satisfies no states"); } // Remember whether filter is for the initial state and, if so, whether there's just one - boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); + boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).isInitLabel()); boolean filterInitSingle = filterInit & model.getNumInitialStates() == 1; // Print out number of states satisfying filter if (!filterInit) { diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index dddd10e1..c1b57abc 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -449,14 +449,14 @@ final public class ParamModelChecker extends PrismComponent int i; // treat special cases - if (expr.getName().equals("deadlock")) { + if (expr.isDeadlockLabel()) { int numStates = model.getNumStates(); StateValues stateValues = new StateValues(numStates, model.getFirstInitialState()); for (i = 0; i < numStates; i++) { stateValues.setStateValue(i, model.isDeadlockState(i)); } return regionFactory.completeCover(stateValues); - } else if (expr.getName().equals("init")) { + } else if (expr.isInitLabel()) { int numStates = model.getNumStates(); StateValues stateValues = new StateValues(numStates, model.getFirstInitialState()); for (i = 0; i < numStates; i++) { @@ -523,7 +523,7 @@ final public class ParamModelChecker extends PrismComponent } // Remember whether filter is for the initial state and, if so, whether there's just one - boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); + boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).isInitLabel()); // Print out number of states satisfying filter if (!filterInit) { mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); @@ -603,7 +603,7 @@ final public class ParamModelChecker extends PrismComponent /* // Remember whether filter is for the initial state and, if so, whether there's just one - filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); + filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).isInitLabel()); filterInitSingle = filterInit & model.getNumInitialStates() == 1; // Print out number of states satisfying filter if (!filterInit) diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java index fac2e3e5..e1e2c718 100644 --- a/prism/src/parser/ast/ExpressionLabel.java +++ b/prism/src/parser/ast/ExpressionLabel.java @@ -48,6 +48,22 @@ public class ExpressionLabel extends Expression return name; } + /** + * Is this the special "init" label? + */ + public boolean isInitLabel() + { + return getName().equals("init"); + } + + /** + * Is this the special "deadlock" label? + */ + public boolean isDeadlockLabel() + { + return getName().equals("deadlock"); + } + // Methods required for Expression: @Override diff --git a/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java b/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java index e1e2998c..8270c35a 100644 --- a/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java +++ b/prism/src/parser/visitor/GetAllUndefinedConstantsRecursively.java @@ -77,7 +77,7 @@ public class GetAllUndefinedConstantsRecursively extends ASTTraverse public void visitPost(ExpressionLabel e) throws PrismLangException { // Ignore special cases of labels (no constants there) - if (e.getName().equals("deadlock") || e.getName().equals("init")) { + if (e.isDeadlockLabel() || e.isInitLabel()) { return; } // Look up this label in the label list, if possible diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 53b9092f..3520ce41 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -974,11 +974,11 @@ public class StateModelChecker implements ModelChecker int i; // treat special cases - if (expr.getName().equals("deadlock")) { + if (expr.isDeadlockLabel()) { dd = model.getDeadlocks(); JDD.Ref(dd); return new StateValuesMTBDD(dd, model); - } else if (expr.getName().equals("init")) { + } else if (expr.isInitLabel()) { dd = start; JDD.Ref(dd); return new StateValuesMTBDD(dd, model); @@ -1027,7 +1027,7 @@ public class StateModelChecker implements ModelChecker throw new PrismException("Filter satisfies no states"); } // Remember whether filter is for the initial state and, if so, whether there's just one - boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); + boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).isInitLabel()); boolean filterInitSingle = filterInit & model.getNumStartStates() == 1; // For some types of filter, store info that may be used to optimise model checking diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index faa799e6..d17bda7b 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -345,9 +345,9 @@ public class PTAModelChecker extends PrismComponent // (note: currently not used - these are expanded earlier) if (expr instanceof ExpressionLabel) { ExpressionLabel exprLabel = (ExpressionLabel) expr; - if (exprLabel.getName().equals("deadlock")) + if (exprLabel.isDeadlockLabel()) throw new PrismException("The \"deadlock\" label is not yet supported for PTAs"); - if (exprLabel.getName().equals("init")) + if (exprLabel.isInitLabel()) throw new PrismException("The \"init\" label is not yet supported for PTAs"); i = labelList.getLabelIndex(exprLabel.getName()); if (i == -1)