From 7d9beeaf216017d0ccbe25677dbce25f2b44da0c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 25 Aug 2016 16:07:20 +0000 Subject: [PATCH] ExplicitFiles2MTBDD/import: fully load label information and attach to model [with Steffen Maercker] In the same method, we also determine the initial states git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11739 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ExplicitFiles2MTBDD.java | 140 ++++++++++++----------- 1 file changed, 76 insertions(+), 64 deletions(-) diff --git a/prism/src/prism/ExplicitFiles2MTBDD.java b/prism/src/prism/ExplicitFiles2MTBDD.java index 32d20126..afeae609 100644 --- a/prism/src/prism/ExplicitFiles2MTBDD.java +++ b/prism/src/prism/ExplicitFiles2MTBDD.java @@ -30,8 +30,13 @@ import java.io.BufferedReader; import java.io.File; import java.io.FileReader; import java.io.IOException; +import java.util.BitSet; +import java.util.LinkedHashMap; +import java.util.Map; import java.util.Vector; +import java.util.Map.Entry; +import common.IterableStateSet; import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; @@ -100,6 +105,7 @@ public class ExplicitFiles2MTBDD private Vector transPerAction; // dds for transition action labels (D/CTMCs) private int maxNumChoices = 0; + private LinkedHashMap labelsDD; public ExplicitFiles2MTBDD(Prism prism) { @@ -229,6 +235,9 @@ public class ExplicitFiles2MTBDD // mainLog.println(); // JDD.Deref(tmp); + // load labels + loadLabels(); + // calculate dd for initial state buildInit(); @@ -286,6 +295,9 @@ public class ExplicitFiles2MTBDD // find any deadlocks model.findDeadlocks(prism.getFixDeadlocks()); + // attach labels (might overwrite deadlock state information) + attachLabels(model); + // deref spare dds JDD.Deref(moduleIdentities[0]); JDD.Deref(moduleRangeDDs[0]); @@ -306,6 +318,11 @@ public class ExplicitFiles2MTBDD JDD.Deref(ddChoiceVars[i]); } } + if (labelsDD != null) { + for (JDDNode d : labelsDD.values()) { + JDD.Deref(d); + } + } return model; } @@ -649,81 +666,76 @@ public class ExplicitFiles2MTBDD /** calculate dd for initial state */ private void buildInit() throws PrismException { - BufferedReader in; - String s, s1, s2, ss[]; - int i, r, lineNum = 0, count = 0; - JDDNode tmp; - - // If no labels file provided, just use state 0 (i.e. min value for each var) - if (labelsFile == null) { + // If no labels are provided, just use state 0 (i.e. min value for each var) + if (labelsDD == null) { start = JDD.Constant(1); - for (i = 0; i < numVars; i++) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], 0, 1); + for (int i = 0; i < numVars; i++) { + JDDNode tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], 0, 1); start = JDD.And(start, tmp); } } - // Otherwise, construct from labels file + // Otherwise, construct from the labels else { - start = JDD.Constant(0); - try { - // open file for reading - in = new BufferedReader(new FileReader(labelsFile)); - // read first line (label names) and ignore - in.readLine(); - lineNum = 1; - // read remaining lines - s = in.readLine(); - lineNum++; - while (s != null) { - // skip blank lines - s = s.trim(); - if (s.length() > 0) { - // split string - ss = s.split(":"); - s1 = ss[0].trim(); - s2 = ss[1].trim(); - // search right hand part for 0 (which is index of "init" label) - ss = s2.split(" "); - for (i = 0; i < ss.length; i++) { - if (ss[i].trim().equals("0")) { - count++; - r = Integer.parseInt(s1); - // set element in init states bdd - // case where we don't have a state list... - if (statesFile == null) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[0], r, 1); - } - // case where we do have a state list... - else { - tmp = JDD.Constant(1); - for (i = 0; i < numVars; i++) { - tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], statesArray[r][i], 1)); - } - } - // add it into bdd - JDD.Ref(tmp); - start = JDD.Or(start, tmp); - JDD.Deref(tmp); - } - } + start = labelsDD.get("init"); + if (start == null || start.equals(JDD.ZERO)) { + throw new PrismException("No initial states found in labels file"); + } + } + } + + /** Load label information form label file (if exists) */ + private void loadLabels() throws PrismException + { + if (labelsFile == null) { + return; + } + + // we construct BitSets for the labels + Map labels = explicit.StateModelChecker.loadLabelsFile(labelsFile.getAbsolutePath()); + labelsDD = new LinkedHashMap<>(); + + for (Entry e : labels.entrySet()) { + // compute dd + + JDDNode labelStatesDD = JDD.Constant(0); + + for (int state : new IterableStateSet(e.getValue(), numStates)) { + JDDNode tmp; + // case where we don't have a state list... + if (statesFile == null) { + tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[0], state, 1); + } + // case where we do have a state list... + else { + tmp = JDD.Constant(1); + for (int i = 0; i < numVars; i++) { + tmp = JDD.Apply(JDD.TIMES, tmp, JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], statesArray[state][i], 1)); } - // read next line - s = in.readLine(); - lineNum++; } - // close file - in.close(); - } catch (IOException e) { - throw new PrismException("File I/O error reading from \"" + labelsFile + "\""); - } catch (NumberFormatException e) { - throw new PrismException("Error detected at line " + lineNum + " of labels file \"" + labelsFile + "\""); - } - if (count < 1) { - throw new PrismException("No initial states found in labels file"); + + // add it into bdd + labelStatesDD = JDD.Or(labelStatesDD, tmp); } + + // store the dd + labelsDD.put(e.getKey(), labelStatesDD); } } + /** Attach the computed label information to the model */ + private void attachLabels(Model model) throws PrismNotSupportedException + { + if (labelsDD == null) + return; + + for (Entry e : labelsDD.entrySet()) { + if (e.equals("init")) { + // handled in buildInit() + continue; + } + model.addLabelDD(e.getKey(), e.getValue().copy()); + } + } /** Read info about state rewards from states file */ private void computeStateRewards() throws PrismException