|
|
|
@ -31,7 +31,6 @@ import java.util.Vector; |
|
|
|
import java.util.HashMap; |
|
|
|
|
|
|
|
import jdd.*; |
|
|
|
import mtbdd.*; |
|
|
|
import parser.*; |
|
|
|
import parser.ast.*; |
|
|
|
|
|
|
|
@ -39,13 +38,13 @@ import parser.ast.*; |
|
|
|
|
|
|
|
public class Explicit2MTBDD |
|
|
|
{ |
|
|
|
// prism |
|
|
|
private Prism prism; |
|
|
|
|
|
|
|
// logs |
|
|
|
private PrismLog mainLog; // main log |
|
|
|
private PrismLog techLog; // tech log |
|
|
|
|
|
|
|
// flags/settings |
|
|
|
private boolean doReach = true; // by default, do reachability (sometimes might want to skip it though) |
|
|
|
|
|
|
|
// files to read in from |
|
|
|
private File statesFile; |
|
|
|
private File transFile; |
|
|
|
@ -78,10 +77,7 @@ public class Explicit2MTBDD |
|
|
|
// dds/dd vars - whole system |
|
|
|
private JDDNode trans; // transition matrix dd |
|
|
|
private JDDNode range; // dd giving range for system |
|
|
|
private JDDNode trans01; // 0-1 transition matrix dd |
|
|
|
private JDDNode start; // dd for start state |
|
|
|
private JDDNode reach; // dd of reachable states |
|
|
|
private JDDNode deadlocks; // dd of deadlock states |
|
|
|
private JDDNode stateRewards; // dd of state rewards |
|
|
|
private JDDNode transRewards; // dd of transition rewards |
|
|
|
private JDDVars allDDRowVars; // all dd vars (rows) |
|
|
|
@ -112,10 +108,11 @@ public class Explicit2MTBDD |
|
|
|
|
|
|
|
// constructor |
|
|
|
|
|
|
|
public Explicit2MTBDD(PrismLog log1, PrismLog log2, File sf, File tf, int t, String is) |
|
|
|
public Explicit2MTBDD(Prism prism, File sf, File tf, int t, String is) |
|
|
|
{ |
|
|
|
mainLog = log1; |
|
|
|
techLog = log2; |
|
|
|
this.prism = prism; |
|
|
|
mainLog = prism.getMainLog(); |
|
|
|
techLog = prism.getTechLog(); |
|
|
|
statesFile = sf; |
|
|
|
transFile = tf; |
|
|
|
// set type at this point |
|
|
|
@ -131,28 +128,6 @@ public class Explicit2MTBDD |
|
|
|
initString = is; |
|
|
|
} |
|
|
|
|
|
|
|
// set options (generic) |
|
|
|
|
|
|
|
public void setOption(String option, boolean b) |
|
|
|
{ |
|
|
|
if (option.equals("doreach")) { |
|
|
|
doReach = b; |
|
|
|
} |
|
|
|
else { |
|
|
|
mainLog.println("\nWarning: option \""+option+"\" not supported by Explicit2MTBDD translator."); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
public void setOption(String option, int i) |
|
|
|
{ |
|
|
|
mainLog.println("\nWarning: option \""+option+"\" not supported by Explicit2MTBDD translator."); |
|
|
|
} |
|
|
|
|
|
|
|
public void setOption(String option, String s) |
|
|
|
{ |
|
|
|
mainLog.println("\nWarning: option \""+option+"\" not supported by Explicit2MTBDD translator."); |
|
|
|
} |
|
|
|
|
|
|
|
// build state space |
|
|
|
|
|
|
|
public ModulesFile buildStates() throws PrismException |
|
|
|
@ -461,20 +436,16 @@ public class Explicit2MTBDD |
|
|
|
// mainLog.println(); |
|
|
|
// JDD.Deref(tmp); |
|
|
|
|
|
|
|
// calculate dd for initial state |
|
|
|
start = JDD.Constant(1); |
|
|
|
for (i = 0; i < numVars; i++) { |
|
|
|
tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); |
|
|
|
start = JDD.And(start, tmp); |
|
|
|
} |
|
|
|
|
|
|
|
// compute state rewards |
|
|
|
computeStateRewards(); |
|
|
|
|
|
|
|
// do reachability (or not!) |
|
|
|
if (doReach) { |
|
|
|
doReachability(); |
|
|
|
} |
|
|
|
else { |
|
|
|
skipReachability(); |
|
|
|
} |
|
|
|
|
|
|
|
// find any deadlocks |
|
|
|
findDeadlocks(); |
|
|
|
|
|
|
|
int numModules = 1; // just one module |
|
|
|
String moduleNames[] = modulesFile.getModuleNames(); // whose name is stored here |
|
|
|
Values constantValues = new Values(); // no constants |
|
|
|
@ -485,22 +456,42 @@ public class Explicit2MTBDD |
|
|
|
|
|
|
|
// create new Model object to be returned |
|
|
|
if (type == ModulesFile.PROBABILISTIC) { |
|
|
|
model = new ProbModel(trans, trans01, start, reach, deadlocks, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, |
|
|
|
model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, |
|
|
|
numModules, moduleNames, moduleDDRowVars, moduleDDColVars, |
|
|
|
numVars, varList, varDDRowVars, varDDColVars, constantValues); |
|
|
|
} |
|
|
|
else if (type == ModulesFile.NONDETERMINISTIC) { |
|
|
|
model = new NondetModel(trans, trans01, start, reach, deadlocks, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, |
|
|
|
model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, |
|
|
|
allDDSynchVars, allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, |
|
|
|
numModules, moduleNames, moduleDDRowVars, moduleDDColVars, |
|
|
|
numVars, varList, varDDRowVars, varDDColVars, constantValues); |
|
|
|
} |
|
|
|
else if (type == ModulesFile.STOCHASTIC) { |
|
|
|
model = new StochModel(trans, trans01, start, reach, deadlocks, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, |
|
|
|
model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, |
|
|
|
numModules, moduleNames, moduleDDRowVars, moduleDDColVars, |
|
|
|
numVars, varList, varDDRowVars, varDDColVars, constantValues); |
|
|
|
} |
|
|
|
|
|
|
|
// do reachability (or not) |
|
|
|
if (prism.getDoReach()) { |
|
|
|
mainLog.print("\nComputing reachable states...\n"); |
|
|
|
model.doReachability(prism.getExtraReachInfo()); |
|
|
|
model.filterReachableStates(); |
|
|
|
} |
|
|
|
else { |
|
|
|
mainLog.print("\nSkipping reachable state computation.\n"); |
|
|
|
model.skipReachability(); |
|
|
|
model.filterReachableStates(); |
|
|
|
} |
|
|
|
|
|
|
|
// Print some info (if extraddinfo flag on) |
|
|
|
if (prism.getExtraDDInfo()) { |
|
|
|
mainLog.print("Reach: " + JDD.GetNumNodes(model.getReach()) + " nodes\n"); |
|
|
|
} |
|
|
|
|
|
|
|
// find any deadlocks |
|
|
|
model.findDeadlocks(); |
|
|
|
|
|
|
|
// deref spare dds |
|
|
|
JDD.Deref(moduleIdentities[0]); |
|
|
|
JDD.Deref(moduleRangeDDs[0]); |
|
|
|
@ -893,139 +884,6 @@ public class Explicit2MTBDD |
|
|
|
throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\""); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
// do reachability |
|
|
|
|
|
|
|
private void doReachability() |
|
|
|
{ |
|
|
|
int i; |
|
|
|
JDDNode tmp; |
|
|
|
|
|
|
|
// calculate dd for initial state |
|
|
|
start = JDD.Constant(1); |
|
|
|
for (i = 0; i < numVars; i++) { |
|
|
|
tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); |
|
|
|
start = JDD.And(start, tmp); |
|
|
|
} |
|
|
|
|
|
|
|
// calculate 0-1 version of trans |
|
|
|
JDD.Ref(trans); |
|
|
|
trans01 = JDD.GreaterThan(trans, 0); |
|
|
|
|
|
|
|
// remove any nondeterminism |
|
|
|
if (type == ModulesFile.NONDETERMINISTIC) { |
|
|
|
JDD.Ref(trans01); |
|
|
|
tmp = JDD.MaxAbstract(trans01, allDDNondetVars); |
|
|
|
} |
|
|
|
else { |
|
|
|
JDD.Ref(trans01); |
|
|
|
tmp = trans01; |
|
|
|
} |
|
|
|
|
|
|
|
// compute reachable states |
|
|
|
mainLog.print("\nComputing reachable states...\n"); |
|
|
|
reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); |
|
|
|
JDD.Deref(tmp); |
|
|
|
|
|
|
|
// remove non-reachable states from transition matrix |
|
|
|
JDD.Ref(reach); |
|
|
|
trans = JDD.Apply(JDD.TIMES, reach, trans); |
|
|
|
JDD.Ref(reach); |
|
|
|
tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); |
|
|
|
trans = JDD.Apply(JDD.TIMES, tmp, trans); |
|
|
|
|
|
|
|
// recalculate 0-1 version of trans |
|
|
|
JDD.Deref(trans01); |
|
|
|
JDD.Ref(trans); |
|
|
|
trans01 = JDD.GreaterThan(trans, 0); |
|
|
|
|
|
|
|
// remove non-reachable states from states rewards vector |
|
|
|
JDD.Ref(reach); |
|
|
|
stateRewards = JDD.Apply(JDD.TIMES, reach, stateRewards); |
|
|
|
|
|
|
|
// remove non-reachable states from transition reward matrix |
|
|
|
JDD.Ref(reach); |
|
|
|
transRewards = JDD.Apply(JDD.TIMES, reach, transRewards); |
|
|
|
JDD.Ref(reach); |
|
|
|
tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); |
|
|
|
transRewards = JDD.Apply(JDD.TIMES, tmp, transRewards); |
|
|
|
} |
|
|
|
|
|
|
|
// this method allows you to skip the reachability phase |
|
|
|
// there are two versions - one which actually does skip it |
|
|
|
// and one which does it anyway but doesn't filter out the |
|
|
|
// unreachable states from the transition matrix. |
|
|
|
// these are only here for experimental purposes - not general use. |
|
|
|
|
|
|
|
// (do reach but don't filter) |
|
|
|
|
|
|
|
// private void skipReachability() |
|
|
|
// { |
|
|
|
// int i; |
|
|
|
// JDDNode tmp; |
|
|
|
// |
|
|
|
// // calculate dd for initial state |
|
|
|
// start = JDD.Constant(1); |
|
|
|
// for (i = 0; i < numVars; i++) { |
|
|
|
// tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); |
|
|
|
// start = JDD.And(start, tmp); |
|
|
|
// } |
|
|
|
// |
|
|
|
// // calculate 0-1 version of trans |
|
|
|
// JDD.Ref(trans); |
|
|
|
// trans01 = JDD.GreaterThan(trans, 0); |
|
|
|
// |
|
|
|
// // remove any nondeterminism |
|
|
|
// if (type == ModulesFile.NONDETERMINISTIC) { |
|
|
|
// JDD.Ref(trans01); |
|
|
|
// tmp = JDD.MaxAbstract(trans01, allDDNondetVars); |
|
|
|
// } |
|
|
|
// else { |
|
|
|
// JDD.Ref(trans01); |
|
|
|
// tmp = trans01; |
|
|
|
// } |
|
|
|
// |
|
|
|
// // compute reachable states |
|
|
|
// mainLog.print("\nComputing reachable states...\n"); |
|
|
|
// reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); |
|
|
|
// JDD.Deref(tmp); |
|
|
|
// } |
|
|
|
|
|
|
|
// (no reach and no filter) |
|
|
|
|
|
|
|
private void skipReachability() |
|
|
|
{ |
|
|
|
int i; |
|
|
|
JDDNode tmp; |
|
|
|
|
|
|
|
// calculate dd for initial state |
|
|
|
start = JDD.Constant(1); |
|
|
|
for (i = 0; i < numVars; i++) { |
|
|
|
tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); |
|
|
|
start = JDD.And(start, tmp); |
|
|
|
} |
|
|
|
|
|
|
|
// calculate 0-1 version of trans |
|
|
|
JDD.Ref(trans); |
|
|
|
trans01 = JDD.GreaterThan(trans, 0); |
|
|
|
|
|
|
|
// don't compute reachable states - assume all reachable |
|
|
|
reach = JDD.Constant(1); |
|
|
|
} |
|
|
|
|
|
|
|
private void findDeadlocks() |
|
|
|
{ |
|
|
|
// find states with at least one transition |
|
|
|
JDD.Ref(trans01); |
|
|
|
deadlocks = JDD.ThereExists(trans01, allDDColVars); |
|
|
|
if (type == ModulesFile.NONDETERMINISTIC) { |
|
|
|
deadlocks = JDD.ThereExists(deadlocks, allDDNondetVars); |
|
|
|
} |
|
|
|
|
|
|
|
// find reachable states with no transitions |
|
|
|
JDD.Ref(reach); |
|
|
|
deadlocks = JDD.And(reach, JDD.Not(deadlocks)); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
//------------------------------------------------------------------------------ |
Dave Parker
18 years ago