From 8e38d2b7dd500840b9805b59ef707b3c7213e078 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 5 Jul 2016 11:16:39 +0000 Subject: [PATCH] Some tidying + documentation in prism.StateList classes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11461 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StateList.java | 66 +++++++++-- prism/src/prism/StateListMTBDD.java | 177 +++++++++++++++------------- 2 files changed, 152 insertions(+), 91 deletions(-) diff --git a/prism/src/prism/StateList.java b/prism/src/prism/StateList.java index 5218a719..a2e063ec 100644 --- a/prism/src/prism/StateList.java +++ b/prism/src/prism/StateList.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -31,21 +31,71 @@ import java.util.List; import jdd.*; import parser.Values; -// interface for state list classes - +/** + * Interface for classes that store a list of states. + */ public interface StateList { + /** + * Get the number of states in the list. + */ int size(); + + /** + * Get the number of states in the list as a string + * (useful when the number is too big to fit in an integer). + */ String sizeString(); + + /** + * Print the states to a log. + */ void print(PrismLog log); + + /** + * Print the first {@code n} states in the list to a log. + */ + void print(PrismLog log, int n); + + /** + * Print the states to a log, in Matlab format. + */ void printMatlab(PrismLog log); + + /** + * Print the first {@code n} states in the list to a log, in Matlab format. + */ + void printMatlab(PrismLog log, int n); + + /** + * Print the states to a log, in Dot format. + */ void printDot(PrismLog log); + + /** + * Format the list of states as a list of strings. + */ public List exportToStringList(); - void print(PrismLog log, int n); - void printMatlab(PrismLog log, int n); - boolean includes(JDDNode state); + + /** + * Check whether a set of states, specified as a BDD, is *partially* included in this list, + * i.e. whether there is any intersection between the two sets. + */ + boolean includes(JDDNode set); + + /** + * Check whether a set of states, specified as a BDD, is *fully* included in this list, + * i.e. whether every state in {@code set} is in this list. + */ + boolean includesAll(JDDNode set); + + /** + * Get the first state in this list, as a {@link parser.Values} object. + */ Values getFirstAsValues() throws PrismException; + + /** + * Free any memory associated with storing this list of states. + */ void clear(); } - -//------------------------------------------------------------------------------ diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index 8e7b9a62..a17a8ebf 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -34,49 +34,55 @@ import parser.Values; import parser.VarList; import parser.type.*; -// list of states (mtbdd) - +/** + * Stores a list of states as a BDD (or as a 0-1 MTBDD). + */ public class StateListMTBDD implements StateList { - // states vector mtbdd - JDDNode states; + // States list, as a (0-1) MTBDD + protected JDDNode states; - // info from model - JDDVars vars; - int numVars; - ODDNode odd; - VarList varList; - double size; + // Info needed from model + protected JDDVars vars; + protected int numVars; + protected ODDNode odd; + protected VarList varList; + protected double size; // stuff to keep track of variable values in print method - int[] varSizes; - int[] varValues; - int currentVar; - int currentVarLevel; + protected int[] varSizes; + protected int[] varValues; + protected int currentVar; + protected int currentVarLevel; // stuff to control printing limit - boolean limit; - int numToPrint; - int count; + protected boolean limit; + protected int numToPrint; + protected int count; // log for output from print method - PrismLog outputLog; + protected PrismLog outputLog; // string array when exporting - List strList; + protected List strList; // output format - enum OutputFormat { NORMAL, MATLAB, DOT, STRINGS }; - OutputFormat outputFormat = OutputFormat.NORMAL; + protected enum OutputFormat { NORMAL, MATLAB, DOT, STRINGS }; + protected OutputFormat outputFormat = OutputFormat.NORMAL; // Constructors - public StateListMTBDD(JDDNode s, Model model) + /** + * Create a states list from a BDD and the associated model. + * @param states The list of states + * @param model The model + */ + public StateListMTBDD(JDDNode states, Model model) { int i; - // store states vector mtbdd - states = s; + // store states list bdd + this.states = states; // get info from model vars = model.getAllDDRowVars(); @@ -95,14 +101,21 @@ public class StateListMTBDD implements StateList varValues = new int[varList.getNumVars()]; } - public StateListMTBDD(JDDNode s, JDDVars vars, ODDNode odd, VarList varList) + /** + * Create a states list from a BDD and the associated info about variables/indexing. + * @param states The list of states + * @param vars BDD variables used to represent states + * @param odd ODD storing state indexing info + * @param varList Information about (language-level) variables + */ + public StateListMTBDD(JDDNode states, JDDVars vars, ODDNode odd, VarList varList) { int i; // store states vector mtbdd - states = s; + this.states = states; - // get info from model + // store variable/indexing info this.vars = vars; this.numVars = vars.n(); this.odd = odd; @@ -119,20 +132,19 @@ public class StateListMTBDD implements StateList varValues = new int[varList.getNumVars()]; } - // return size (number of states in list) - + @Override public int size() { return (size > Integer.MAX_VALUE) ? -1 : (int)Math.round(size); } + @Override public String sizeString() { return (size > Long.MAX_VALUE) ? "" + size : "" + Math.round(size); } - // print/export whole list - + @Override public void print(PrismLog log) { outputFormat = OutputFormat.NORMAL; @@ -142,54 +154,61 @@ public class StateListMTBDD implements StateList if (count == 0) outputLog.println("(none)"); } - public void printMatlab(PrismLog log) + + @Override + public void print(PrismLog log, int n) { - outputFormat = OutputFormat.MATLAB; - limit = false; + outputFormat = OutputFormat.NORMAL; + limit = true; + numToPrint = n; outputLog = log; doPrint(); + if (count == 0) + outputLog.println("(none)"); } - public void printDot(PrismLog log) + + @Override + public void printMatlab(PrismLog log) { - outputFormat = OutputFormat.DOT; + outputFormat = OutputFormat.MATLAB; limit = false; outputLog = log; doPrint(); } - public List exportToStringList() - { - strList = new ArrayList((int)size); - outputFormat = OutputFormat.STRINGS; - limit = false; - doPrint(); - return strList; - } - - // print first n states of list - public void print(PrismLog log, int n) + @Override + public void printMatlab(PrismLog log, int n) { - outputFormat = OutputFormat.NORMAL; + outputFormat = OutputFormat.MATLAB; limit = true; numToPrint = n; outputLog = log; doPrint(); - if (count == 0) - outputLog.println("(none)"); } - public void printMatlab(PrismLog log, int n) + @Override + public void printDot(PrismLog log) { - outputFormat = OutputFormat.MATLAB; - limit = true; - numToPrint = n; + outputFormat = OutputFormat.DOT; + limit = false; outputLog = log; doPrint(); } - // printing method + @Override + public List exportToStringList() + { + strList = new ArrayList((int)size); + outputFormat = OutputFormat.STRINGS; + limit = false; + doPrint(); + return strList; + } - public void doPrint() + /** + * Implementation of printing. + */ + private void doPrint() { int i; @@ -203,14 +222,12 @@ public class StateListMTBDD implements StateList //log.println(); } - // recursive bit of print - // (nb: traversal of mtbdd/odd is quite simple, - // tricky bit is keeping track of variable values - // throughout traversal - we want to be efficient - // and not compute the values from scratch each - // time, but we also want to avoid passing arrays - // into the resursive method) - + /** + * Main recursive part of state printing. + * NB: Traversal of the MTBDD/ODD is quite simple; the tricky bit is keeping track of variable values + * throughout traversal - we want to be efficient and not compute the values from scratch each + * time, but we also want to avoid passing arrays into the recursive method. + */ private void printRec(JDDNode dd, int level, ODDNode o, long n) { int i, j; @@ -230,6 +247,7 @@ public class StateListMTBDD implements StateList case NORMAL: outputLog.print(n + ":("); break; case MATLAB: break; case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break; + case STRINGS: break; } j = varList.getNumVars(); varsString = ""; @@ -275,42 +293,37 @@ public class StateListMTBDD implements StateList varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); } - /** - * Check for (partial) state inclusion - state(s) given by BDD - */ - public boolean includes(JDDNode state) + @Override + public boolean includes(JDDNode set) { JDDNode tmp; boolean incl; JDD.Ref(states); - JDD.Ref(state); - tmp = JDD.And(states, state); + JDD.Ref(set); + tmp = JDD.And(states, set); incl = !tmp.equals(JDD.ZERO); JDD.Deref(tmp); return incl; } - /** - * Check for (full) state inclusion - state(s) given by BDD - */ - public boolean includesAll(JDDNode state) + @Override + public boolean includesAll(JDDNode set) { JDDNode tmp; boolean incl; JDD.Ref(states); - JDD.Ref(state); - tmp = JDD.And(states, state); - incl = tmp.equals(state); + JDD.Ref(set); + tmp = JDD.And(states, set); + incl = tmp.equals(set); JDD.Deref(tmp); return incl; } - // get first state as Values object - + @Override public Values getFirstAsValues() throws PrismException { Values values; @@ -359,11 +372,9 @@ public class StateListMTBDD implements StateList return values; } - // clear - + @Override public void clear() { JDD.Deref(states); } } -