From 6bc5aefa502769dd946a6fc219ae9d805a4584c3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 13 Sep 2016 10:57:29 +0000 Subject: [PATCH] Extend ModelGenerator2MTBDD to generate/store label info too. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11810 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ModelGenerator2MTBDD.java | 24 +++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index e15576f0..fc134a0e 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -51,6 +51,7 @@ public class ModelGenerator2MTBDD // Model info private ModelType modelType; private VarList varList; + private int numLabels; private int numVars; private int numRewardStructs; private String[] rewardStructNames; @@ -89,6 +90,8 @@ public class ModelGenerator2MTBDD private Vector synchs; // list of action names private JDDNode transActions; // dd for transition action labels (MDPs) private Vector transPerAction; // dds for transition action labels (D/CTMCs) + // labels + private JDDNode[] labelsArray; // rewards private JDDNode[] stateRewardsArray; private JDDNode[] transRewardsArray; @@ -109,6 +112,7 @@ public class ModelGenerator2MTBDD this.modelGen = modelGen; modelType = modelGen.getModelType(); varList = modelGen.createVarList(); + numLabels = modelGen.getNumLabels(); numVars = varList.getNumVars(); numRewardStructs = modelGen.getNumRewardStructs(); rewardStructNames = modelGen.getRewardStructNames().toArray(new String[0]); @@ -166,9 +170,6 @@ public class ModelGenerator2MTBDD // mainLog.println(); // JDD.Deref(tmp); - // load labels - //loadLabels(); - int numModules = 1; // just one module String moduleNames[] = new String[] { "M" }; Values constantValues = modelGen.getConstantValues(); @@ -206,6 +207,11 @@ public class ModelGenerator2MTBDD // find any deadlocks model.findDeadlocks(prism.getFixDeadlocks()); + // attach labels + for (int l = 0; l < numLabels; l++) { + model.addLabelDD(modelGen.getLabelName(l), labelsArray[l]); + } + // deref spare dds JDD.Deref(moduleIdentities[0]); JDD.Deref(moduleRangeDDs[0]); @@ -412,7 +418,11 @@ public class ModelGenerator2MTBDD transActions = JDD.Constant(0); } start = JDD.Constant(0); - reach = JDD.Constant(0); + reach = JDD.Constant(0); + labelsArray = new JDDNode[numLabels]; + for (int l = 0; l < numLabels; l++) { + labelsArray[l] = JDD.Constant(0); + } stateRewardsArray = new JDDNode[numRewardStructs]; transRewardsArray = new JDDNode[numRewardStructs]; for (int r = 0; r < numRewardStructs; r++) { @@ -516,6 +526,12 @@ public class ModelGenerator2MTBDD // TODO progress.updateIfReady(src + 1); } + for (int l = 0; l < numLabels; l++) { + if (modelGen.isLabelTrue(l)) { + labelsArray[l] = JDD.Or(labelsArray[l], ddState.copy()); + } + } + // Add state rewards for (int r = 0; r < numRewardStructs; r++) { double sr = modelGen.getStateReward(r, state);