Explicit engine handles "deadlock" and "init" labels, if not embedded in a (logical) expression.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3124 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -101,6 +101,11 @@ public class DTMCEmbeddedSimple implements DTMC
 		return ctmc.isInitialState(i);
 	}
 
+	public boolean isFixedDeadlockState(int i)
+	{
+		return ctmc.isFixedDeadlockState(i);
+	}
+
 	public List<State> getStatesList()
 	{
 		return ctmc.getStatesList();

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -92,6 +92,11 @@ public class DTMCFromMDPMemorylessAdversary implements DTMC
 		return mdp.isInitialState(i);
 	}
 
+	public boolean isFixedDeadlockState(int i)
+	{
+		return mdp.isFixedDeadlockState(i);
+	}
+
 	public List<State> getStatesList()
 	{
 		return mdp.getStatesList();

prism/src/explicit/DTMCSimple.java

@@ -313,6 +313,7 @@ public class DTMCSimple extends ModelSimple implements DTMC
 		if (fix) {
 			for (i = deadlocks.nextSetBit(0); i >= 0; i = deadlocks.nextSetBit(i + 1)) {
 				setProbability(i, i, 1.0);
+				addFixedDeadlockState(i);
 			}
 		}
 		return deadlocks;

prism/src/explicit/DTMCUniformisedSimple.java

@@ -107,6 +107,11 @@ public class DTMCUniformisedSimple implements DTMC
 		return ctmc.isInitialState(i);
 	}
 
+	public boolean isFixedDeadlockState(int i)
+	{
+		return ctmc.isFixedDeadlockState(i);
+	}
+
 	public List<State> getStatesList()
 	{
 		return ctmc.getStatesList();

prism/src/explicit/MDPSimple.java

@@ -443,6 +443,7 @@ public class MDPSimple extends ModelSimple implements MDP
 				Distribution distr = new Distribution();
 				distr.add(i, 1.0);
 				addChoice(i, distr);
+				addFixedDeadlockState(i);
 			}
 		}
 		return deadlocks;

prism/src/explicit/Model.java

@@ -72,6 +72,13 @@ public interface Model
 	 */
 	public boolean isInitialState(int i);
 
+	/**
+	 * Check whether a state is a "fixed" deadlock, i.e. a state that was
+	 * originally a deadlock but has been fixed through the addition of a self-loop,
+	 * or a state that is still a deadlock but in a model where this acceptable, e.g. a CTMC.
+	 */
+	public boolean isFixedDeadlockState(int i);
+	
 	/**
 	 * Get access to an (optional) list of states.
 	 */
@@ -118,7 +125,8 @@ public interface Model
 
 	/**
 	 * Find all deadlocks and return a BitSet of these states.
-	 * If requested (if fix=true, then add self-loops in these states).
+	 * If requested (if fix=true), then add self-loops in these states
+	 * (and update the "fixed" deadlock information).
 	 */
 	public BitSet findDeadlocks(boolean fix) throws PrismException;
 

prism/src/explicit/ModelSimple.java

@@ -42,11 +42,17 @@ public abstract class ModelSimple implements Model
 	protected int numStates;
 	// Initial states
 	protected List<Integer> initialStates; // TODO: should be a (linkedhash?) set really
+	/**
+	 * States with deadlocks that have been "fixed", i.e. a state that was
+	 * originally a deadlock but has been fixed through the addition of a self-loop,
+	 * or a state that is still a deadlock but in a model where this acceptable, e.g. a CTMC.
+	 */
+	protected TreeSet<Integer> deadlocksFixed;
 	// State info (read only, just a pointer)
 	protected List<State> statesList;
 	// Constant info (read only, just a pointer)
 	protected Values constantValues;
-	
+
 	// Mutators
 
 	/**
@@ -63,7 +69,7 @@ public abstract class ModelSimple implements Model
 		statesList = model.statesList;
 		constantValues = model.constantValues;
 	}
-	
+
 	/**
 	 * Copy data from another ModelSimple and a state index permutation,
 	 * i.e. state index i becomes index permut[i]
@@ -82,7 +88,7 @@ public abstract class ModelSimple implements Model
 		statesList = null;
 		constantValues = model.constantValues;
 	}
-	
+
 	/**
 	 * Initialise: create new model with fixed number of states.
 	 */
@@ -90,9 +96,10 @@ public abstract class ModelSimple implements Model
 	{
 		this.numStates = numStates;
 		initialStates = new ArrayList<Integer>();
+		deadlocksFixed = new TreeSet<Integer>();
 		statesList = null;
 	}
-	
+
 	/**
 	 * Add a state to the list of initial states.
 	 */
@@ -100,12 +107,20 @@ public abstract class ModelSimple implements Model
 	{
 		initialStates.add(i);
 	}
-	
+
+	/**
+	 * Add a state to the list of "fixed" deadlock states.
+	 */
+	public void addFixedDeadlockState(int i)
+	{
+		deadlocksFixed.add(i);
+	}
+
 	/**
 	 * Clear all information for a state (i.e. remove all transitions).
 	 */
 	public abstract void clearState(int i);
-	
+
 	/**
 	 * Add a new state and return its index.
 	 */
@@ -122,57 +137,63 @@ public abstract class ModelSimple implements Model
 	public abstract void buildFromPrismExplicit(String filename) throws PrismException;
 
 	// Accessors (for Model interface)
-	
+
 	public abstract ModelType getModelType();
 
 	public int getNumStates()
 	{
 		return numStates;
 	}
-	
+
 	public int getNumInitialStates()
 	{
 		return initialStates.size();
 	}
-	
+
 	public Iterable<Integer> getInitialStates()
 	{
 		return initialStates;
 	}
-	
+
 	public int getFirstInitialState()
 	{
 		return initialStates.isEmpty() ? -1 : initialStates.get(0);
 	}
-	
+
 	public boolean isInitialState(int i)
 	{
 		return initialStates.contains(i);
 	}
+
+	@Override
+	public boolean isFixedDeadlockState(int i)
+	{
+		return deadlocksFixed.contains(i);
+	}
 	
 	public List<State> getStatesList()
 	{
 		return statesList;
 	}
-	
+
 	public Values getConstantValues()
 	{
 		return constantValues;
 	}
-	
+
 	public abstract int getNumTransitions();
-	
+
 	public abstract boolean isSuccessor(int s1, int s2);
-	
+
 	public abstract int getNumChoices(int s);
-	
+
 	public void checkForDeadlocks() throws PrismException
 	{
 		checkForDeadlocks(null);
 	}
-	
+
 	public abstract void checkForDeadlocks(BitSet except) throws PrismException;
-	
+
 	@Override
 	public void exportToPrismExplicit(String baseFilename) throws PrismException
 	{
@@ -190,9 +211,9 @@ public abstract class ModelSimple implements Model
 	}
 
 	public abstract void exportToDotFile(String filename, BitSet mark) throws PrismException;
-	
+
 	public abstract void exportToPrismLanguage(String filename) throws PrismException;
-	
+
 	public abstract String infoString();
 
 	@Override

prism/src/explicit/ModelSparse.java

@@ -42,6 +42,12 @@ public abstract class ModelSparse implements Model
 	protected int numStates;
 	// Initial states
 	protected List<Integer> initialStates; // TODO: should be a (linkedhash?) set really
+	/**
+	 * States with deadlocks that have been "fixed", i.e. a state that was
+	 * originally a deadlock but has been fixed through the addition of a self-loop,
+	 * or a state that is still a deadlock but in a model where this acceptable, e.g. a CTMC.
+	 */
+	protected TreeSet<Integer> deadlocksFixed;
 	// State info
 	protected List<State> statesList;
 	// Constant info
@@ -56,6 +62,7 @@ public abstract class ModelSparse implements Model
 	{
 		this.numStates = numStates;
 		initialStates = new ArrayList<Integer>();
+		deadlocksFixed = new TreeSet<Integer>();
 		statesList = null;
 	}
 	
@@ -67,6 +74,14 @@ public abstract class ModelSparse implements Model
 		initialStates.add(i);
 	}
 	
+	/**
+	 * Add a state to the list of "fixed" deadlock states.
+	 */
+	public void addFixedDeadlockState(int i)
+	{
+		deadlocksFixed.add(i);
+	}
+
 	/**
 	 * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file).
 	 */
@@ -101,6 +116,12 @@ public abstract class ModelSparse implements Model
 		return initialStates.contains(i);
 	}
 	
+	@Override
+	public boolean isFixedDeadlockState(int i)
+	{
+		return deadlocksFixed.contains(i);
+	}
+	
 	public List<State> getStatesList()
 	{
 		return statesList;

prism/src/explicit/STPGAbstrSimple.java

@@ -396,6 +396,7 @@ public class STPGAbstrSimple extends ModelSimple implements STPG
 				distr.add(i, 1.0);
 				distrs.add(distr);
 				addDistributionSet(i, distrs);
+				addFixedDeadlockState(i);
 			}
 		}
 		return deadlocks;

prism/src/explicit/StateModelChecker.java

@@ -554,15 +554,19 @@ public class StateModelChecker
 
 		// treat special cases
 		if (expr.getName().equals("deadlock")) {
-			throw new PrismException("Not supported"); // TODO
-			//dd = model.getFixedDeadlocks();
-			//JDD.Ref(dd);
-			//return new StateValuesMTBDD(dd, model);
+			int numStates = model.getNumStates();
+			BitSet bs = new BitSet(numStates);
+			for (i = 0; i < numStates; i++) {
+				bs.set(i, model.isFixedDeadlockState(i));
+			}
+			return bs;
 		} else if (expr.getName().equals("init")) {
-			throw new PrismException("Not supported"); // TODO
-			//dd = start;
-			//JDD.Ref(dd);
-			//return new StateValuesMTBDD(dd, model);
+			int numStates = model.getNumStates();
+			BitSet bs = new BitSet(numStates);
+			for (i = 0; i < numStates; i++) {
+				bs.set(i, model.isInitialState(i));
+			}
+			return bs;
 		} else {
 			ll = propertiesFile.getCombinedLabelList();
 			i = ll.getLabelIndex(expr.getName());