From bb1d0dcd5b3ee57ef332de3f3398455cc3b67b0e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 27 Jun 2015 22:19:26 +0000 Subject: [PATCH] Add label export functionality to explicit engine git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10108 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 121 ++++++++++++++++++++-- prism/src/prism/Prism.java | 17 ++- 2 files changed, 127 insertions(+), 11 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 92b8ead9..948e6bd5 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -62,9 +62,11 @@ import parser.type.TypeInt; import parser.visitor.ASTTraverseModify; import prism.Filter; import prism.ModelType; +import prism.Prism; import prism.PrismComponent; import prism.PrismException; import prism.PrismLangException; +import prism.PrismLog; import prism.PrismNotSupportedException; import prism.PrismSettings; import prism.Result; @@ -748,15 +750,27 @@ public class StateModelChecker extends PrismComponent if (bs != null) { return StateValues.createFromBitSet((BitSet) bs.clone(), model); } - // Failing that, look in the properties file - ll = propertiesFile.getCombinedLabelList(); - i = ll.getLabelIndex(expr.getName()); - if (i == -1) - throw new PrismException("Unknown label \"" + expr.getName() + "\" in property"); - // check recursively - return checkExpression(model, ll.getLabel(i), statesOfInterest); + // Failing that, look in the properties file (if possible) + if (propertiesFile != null) { + ll = propertiesFile.getCombinedLabelList(); + i = ll.getLabelIndex(expr.getName()); + if (i != -1) { + // check recursively + return checkExpression(model, ll.getLabel(i), statesOfInterest); + } + } + // Or just the model file + else { + ll = modulesFile.getLabelList(); + i = ll.getLabelIndex(expr.getName()); + if (i != -1) { + // check recursively + return checkExpression(model, ll.getLabel(i), statesOfInterest); + } + } } - } + throw new PrismException("Unknown label \"" + expr.getName() + "\""); +} // Check property ref @@ -1071,6 +1085,24 @@ public class StateModelChecker extends PrismComponent return resVals; } + /** + * Export a set of labels and the states that satisfy them. + * @param model The model + * @param labels The states that satisfy each label, specified as a BitSet + * @param labelNames The name of each label + * @param exportType The format in which to export + * @param out Where to export + */ + public void exportLabels(Model model, List labelNames, int exportType, PrismLog out) throws PrismException + { + List labels = new ArrayList(); + for (String labelName : labelNames) { + StateValues sv = checkExpression(model, new ExpressionLabel(labelName), null); + labels.add(sv.getBitSet()); + } + exportLabels(model, labels, labelNames, exportType, out); + } + /** * Extract maximal propositional subformulas of an expression, model check them and * replace them with ExpressionLabel objects (L0, L1, etc.) Expression passed in is modified directly, but the result @@ -1286,4 +1318,77 @@ public class StateModelChecker extends PrismComponent throw new PrismException("Error in labels file"); } } + + /** + * Export a set of labels and the states that satisfy them. + * @param model The model + * @param labels The states that satisfy each label, specified as a BitSet + * @param labelNames The name of each label + * @param exportType The format in which to export + * @param out Where to export + */ + public void exportLabels(Model model, List labels, List labelNames, int exportType, PrismLog out) + { + String matlabVarName = "l"; + int numStates = model.getNumStates(); + + // Print list of labels + int numLabels = labels.size(); + if (exportType == Prism.EXPORT_MRMC) { + out.println("#DECLARATION"); + } + for (int i = 0; i < numLabels; i++) { + switch (exportType) { + case Prism.EXPORT_PLAIN: + out.print((i > 0 ? " " : "") + i + "=\"" + labelNames.get(i) + "\""); + break; + case Prism.EXPORT_MATLAB: + out.println(matlabVarName + "_" + labelNames.get(i) + "=sparse(" + numStates + ",1);"); + break; + case Prism.EXPORT_MRMC: + out.print((i > 0 ? " " : "") + labelNames.get(i)); + break; + } + } + out.println(); + if (exportType == Prism.EXPORT_MRMC) { + out.println("#END"); + } + + // Go through states and print satisfying label indices for each one + for (int s = 0; s < numStates; s++) { + boolean first = true; + for (int i = 0; i < numLabels; i++) { + if (labels.get(i).get(s)) { + if (first) { + switch (exportType) { + case Prism.EXPORT_PLAIN: + out.print(s + ":"); + break; + case Prism.EXPORT_MATLAB: + break; + case Prism.EXPORT_MRMC: + out.print(s + 1); + break; + } + first = false; + } + switch (exportType) { + case Prism.EXPORT_PLAIN: + out.print(" " + i); + break; + case Prism.EXPORT_MATLAB: + out.println(matlabVarName + "_" + labelNames.get(i) + "(" + (s + 1) + ")=1;"); + break; + case Prism.EXPORT_MRMC: + out.print(" " + labelNames.get(i)); + break; + } + } + } + if (!first && exportType != Prism.EXPORT_MATLAB) { + out.println(); + } + } + } } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ff69767b..6508a184 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2595,9 +2595,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener JDDNode dd, labels[]; String labelNames[]; - if (getExplicit()) - throw new PrismException("Export of labels not yet supported by explicit engine"); - // get label list and size if (propertiesFile == null) { ll = currentModulesFile.getLabelList(); @@ -2615,6 +2612,20 @@ public class Prism extends PrismComponent implements PrismSettingsListener mainLog.print(getStringForExportType(exportType) + " "); mainLog.println(getDestinationStringForFile(file)); + if (getExplicit()) { + PrismLog out = getPrismLogForFile(file); + List labelNamesExpl = new ArrayList(); + labelNamesExpl.add("init"); + labelNamesExpl.add("deadlock"); + for (i = 0; i < n; i++) { + labelNamesExpl.add(ll.getLabelName(i)); + } + explicit.StateModelChecker mcExpl = createModelCheckerExplicit(propertiesFile); + mcExpl.exportLabels(currentModelExpl, labelNamesExpl, exportType, out); + out.close(); + return; + } + // convert labels to bdds if (n > 0) { mc = new prism.StateModelChecker(this, currentModel, propertiesFile);