From 1a21d7f3421bc896b118fcc096d9cfb1f1f6221c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Jun 2011 11:28:51 +0000 Subject: [PATCH] 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 | 5 ++ .../DTMCFromMDPMemorylessAdversary.java | 5 ++ prism/src/explicit/DTMCSimple.java | 1 + prism/src/explicit/DTMCUniformisedSimple.java | 5 ++ prism/src/explicit/MDPSimple.java | 1 + prism/src/explicit/Model.java | 10 ++- prism/src/explicit/ModelSimple.java | 61 +++++++++++++------ prism/src/explicit/ModelSparse.java | 21 +++++++ prism/src/explicit/STPGAbstrSimple.java | 1 + prism/src/explicit/StateModelChecker.java | 20 +++--- 10 files changed, 101 insertions(+), 29 deletions(-) diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index d2e58c16..28daee6c 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/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 getStatesList() { return ctmc.getStatesList(); diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index 78c63037..6838d8d7 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/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 getStatesList() { return mdp.getStatesList(); diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 9aa29760..6259da13 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/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; diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 569f75f7..6daa2b11 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/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 getStatesList() { return ctmc.getStatesList(); diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 41ce65be..bd5519a8 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/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; diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index fe1de9e1..5f8974c0 100644 --- a/prism/src/explicit/Model.java +++ b/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; diff --git a/prism/src/explicit/ModelSimple.java b/prism/src/explicit/ModelSimple.java index aee48a7d..696a1dcd 100644 --- a/prism/src/explicit/ModelSimple.java +++ b/prism/src/explicit/ModelSimple.java @@ -42,11 +42,17 @@ public abstract class ModelSimple implements Model protected int numStates; // Initial states protected List 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 deadlocksFixed; // State info (read only, just a pointer) protected List 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(); + deadlocksFixed = new TreeSet(); 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 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 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 diff --git a/prism/src/explicit/ModelSparse.java b/prism/src/explicit/ModelSparse.java index c6ed2585..afb3f4e0 100644 --- a/prism/src/explicit/ModelSparse.java +++ b/prism/src/explicit/ModelSparse.java @@ -42,6 +42,12 @@ public abstract class ModelSparse implements Model protected int numStates; // Initial states protected List 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 deadlocksFixed; // State info protected List statesList; // Constant info @@ -56,6 +62,7 @@ public abstract class ModelSparse implements Model { this.numStates = numStates; initialStates = new ArrayList(); + deadlocksFixed = new TreeSet(); 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 getStatesList() { return statesList; diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index a8ee3be6..94b301a6 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/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; diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index b7e3f9fe..45a3f6ca 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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());