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

@@ -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) {

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)

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

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

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

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)