s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Improve explicit.ConstructModel: generalise to use new ModelGenerator interface (not just ModulesFiles via the simulator) and tidy up the settings within the class. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10976 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
a959beb7a7
commit
0e01288705
4 changed files with 130 additions and 84 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 190
      prism/src/explicit/ConstructModel.java
  2. 9
      prism/src/explicit/PrismExplicit.java
  3. 6
      prism/src/explicit/QuantAbstractRefineExample.java
  4. 9
      prism/src/prism/Prism.java

190
prism/src/explicit/ConstructModel.java
View File

@ -29,97 +29,127 @@ package explicit;
import java.io.File; import java.io.File;
import java.io.FileNotFoundException; import java.io.FileNotFoundException;
import java.util.BitSet;
import java.util.LinkedList; import java.util.LinkedList;
import java.util.List; import java.util.List;
import parser.State; import parser.State;
import parser.Values; import parser.Values;
import parser.VarList; import parser.VarList;
import parser.ast.Expression;
import parser.ast.ModulesFile;
import prism.ModelGenerator;
import prism.ModelType; import prism.ModelType;
import prism.Prism; import prism.Prism;
import prism.PrismComponent; import prism.PrismComponent;
import prism.PrismException; import prism.PrismException;
import prism.PrismLog; import prism.PrismLog;
import prism.PrismPrintStreamLog;
import prism.PrismNotSupportedException; import prism.PrismNotSupportedException;
import prism.PrismPrintStreamLog;
import prism.ProgressDisplay; import prism.ProgressDisplay;
import prism.UndefinedConstants; import prism.UndefinedConstants;
import simulator.SimulatorEngine;
/**
* Class to perform explicit-state reachability and model construction.
* The information about the model to be built is provided via a {@link prism.ModelGenerator} interface.
* To build a PRISM model, use {@link simulator.ModulesFileModelGenerator}.
*/
public class ConstructModel extends PrismComponent public class ConstructModel extends PrismComponent
{ {
// The simulator engine
protected SimulatorEngine engine;
// The model generator
protected ModelGenerator modelGen;
// Options: // Options:
// Find deadlocks during model construction?
/** Find deadlocks during model construction? */
protected boolean findDeadlocks = true; protected boolean findDeadlocks = true;
// Automatically fix deadlocks?
/** Automatically fix deadlocks? */
protected boolean fixDeadlocks = true; protected boolean fixDeadlocks = true;
/** Build a sparse representation, if possible?
* (e.g. MDPSparse rather than MDPSimple data structure) */
protected boolean buildSparse = true;
/** Should actions be attached to distributions (and used to distinguish them)? */
protected boolean distinguishActions = true;
/** Should labels be processed and attached to the model? */
protected boolean attachLabels = true;
// Details of built model
// Details of built model:
/** Reachable states */
protected List<State> statesList; protected List<State> statesList;
public ConstructModel(PrismComponent parent, SimulatorEngine engine) throws PrismException
public ConstructModel(PrismComponent parent) throws PrismException
{ {
super(parent); super(parent);
this.engine = engine;
} }
/**
* Get the list of states associated with the last model construction performed.
*/
public List<State> getStatesList() public List<State> getStatesList()
{ {
return statesList; return statesList;
} }
public void setFixDeadlocks(boolean b)
/**
* Automatically fix deadlocks, if needed?
* (by adding self-loops in those states)
*/
public void setFixDeadlocks(boolean fixDeadlocks)
{ {
fixDeadlocks = b;
this.fixDeadlocks = fixDeadlocks;
} }
/** /**
* Build the set of reachable states for a PRISM model language description and return.
* @param modulesFile The PRISM model
* Build a sparse representation, if possible?
* (e.g. MDPSparse rather than MDPSimple data structure)
*/ */
public List<State> computeReachableStates(ModulesFile modulesFile) throws PrismException
public void setBuildSparse(boolean buildSparse)
{ {
constructModel(modulesFile, true, false);
return statesList;
this.buildSparse = buildSparse;
} }
/** /**
* Construct an explicit-state model from a PRISM model language description and return.
* @param modulesFile The PRISM model
* Should actions be attached to distributions (and used to distinguish them)?
*/ */
public Model constructModel(ModulesFile modulesFile) throws PrismException
public void setDistinguishActions(boolean distinguishActions)
{ {
return constructModel(modulesFile, false, true);
this.distinguishActions = distinguishActions;
} }
/** /**
* Construct an explicit-state model from a PRISM model language description and return.
* If {@code justReach} is true, no model is built and null is returned;
* the set of reachable states can be obtained with {@link #getStatesList()}.
* @param modulesFile The PRISM model
* @param justReach If true, just build the reachable state set, not the model
* @param buildSparse Build a sparse version of the model (if possible)?
* Should labels be processed and attached to the model?
*/
public void setAttachLabels(boolean attachLabels)
{
this.attachLabels = attachLabels;
}
/**
* Build the set of reachable states for a model and return it.
* @param modelGen The ModelGenerator interface providing the model
*/
public List<State> computeReachableStates(ModelGenerator modelGen) throws PrismException
{
constructModel(modelGen, true);
return getStatesList();
}
/**
* Construct an explicit-state model and return it.
* @param modelGen The ModelGenerator interface providing the model
*/ */
public Model constructModel(ModulesFile modulesFile, boolean justReach, boolean buildSparse) throws PrismException
public Model constructModel(ModelGenerator modelGen) throws PrismException
{ {
return constructModel(modulesFile, justReach, buildSparse, true);
return constructModel(modelGen, false);
} }
/** /**
* Construct an explicit-state model from a PRISM model language description and return.
* Construct an explicit-state model and return it.
* If {@code justReach} is true, no model is built and null is returned; * If {@code justReach} is true, no model is built and null is returned;
* the set of reachable states can be obtained with {@link #getStatesList()}. * the set of reachable states can be obtained with {@link #getStatesList()}.
* @param modulesFile The PRISM model
* @param modelGen The ModelGenerator interface providing the model
* @param justReach If true, just build the reachable state set, not the model * @param justReach If true, just build the reachable state set, not the model
* @param buildSparse Build a sparse version of the model (if possible)?
* @param distinguishActions True if actions should be attached to distributions (and used to distinguish them)
*/ */
public Model constructModel(ModulesFile modulesFile, boolean justReach, boolean buildSparse, boolean distinguishActions) throws PrismException
public Model constructModel(ModelGenerator modelGen, boolean justReach) throws PrismException
{ {
// Model info // Model info
ModelType modelType; ModelType modelType;
@ -140,11 +170,11 @@ public class ConstructModel extends PrismComponent
long timer; long timer;
// Get model info // Get model info
modelType = modulesFile.getModelType();
modelType = modelGen.getModelType();
// Display a warning if there are unbounded vars // Display a warning if there are unbounded vars
VarList varList = modulesFile.createVarList();
if (modulesFile.containsUnboundedVariables())
VarList varList = modelGen.createVarList();
if (modelGen.containsUnboundedVariables())
mainLog.printWarning("Model contains one or more unbounded variables: model construction may not terminate"); mainLog.printWarning("Model contains one or more unbounded variables: model construction may not terminate");
// Starting reachability... // Starting reachability...
@ -154,9 +184,6 @@ public class ConstructModel extends PrismComponent
progress.start(); progress.start();
timer = System.currentTimeMillis(); timer = System.currentTimeMillis();
// Initialise simulator for this model
engine.createNewOnTheFlyPath(modulesFile);
// Create model storage // Create model storage
if (!justReach) { if (!justReach) {
// Create a (simple, mutable) model of the appropriate type // Create a (simple, mutable) model of the appropriate type
@ -187,25 +214,9 @@ public class ConstructModel extends PrismComponent
// Initialise states storage // Initialise states storage
states = new IndexedSet<State>(true); states = new IndexedSet<State>(true);
explore = new LinkedList<State>(); explore = new LinkedList<State>();
// Add initial state(s) to 'explore'
// Easy (normal) case: just one initial state
if (modulesFile.getInitialStates() == null) {
state = modulesFile.getDefaultInitialState();
explore.add(state);
}
// Otherwise, there may be multiple initial states
// For now, we handle this is in a very inefficient way
else {
Expression init = modulesFile.getInitialStates();
List<State> allPossStates = varList.getAllStates();
for (State possState : allPossStates) {
if (init.evaluateBoolean(modulesFile.getConstantValues(), possState)) {
explore.add(possState);
}
}
}
// Copy initial state(s) to 'states' and to the model
for (State initState : explore) {
// Add initial state(s) to 'explore', 'states' and to the model
for (State initState : modelGen.getInitialStates()) {
explore.add(initState);
states.add(initState); states.add(initState);
if (!justReach) { if (!justReach) {
modelSimple.addState(); modelSimple.addState();
@ -219,19 +230,19 @@ public class ConstructModel extends PrismComponent
// (they are stored in order found so know index is src+1) // (they are stored in order found so know index is src+1)
state = explore.removeFirst(); state = explore.removeFirst();
src++; src++;
// Use simulator to explore all choices/transitions from this state
engine.initialisePath(state);
// Explore all choices/transitions from this state
modelGen.exploreState(state);
// Look at each outgoing choice in turn // Look at each outgoing choice in turn
nc = engine.getNumChoices();
nc = modelGen.getNumChoices();
for (i = 0; i < nc; i++) { for (i = 0; i < nc; i++) {
// For nondet models, collect transitions in a Distribution // For nondet models, collect transitions in a Distribution
if (!justReach && modelType.nondeterministic()) { if (!justReach && modelType.nondeterministic()) {
distr = new Distribution(); distr = new Distribution();
} }
// Look at each transition in the choice // Look at each transition in the choice
nt = engine.getNumTransitions(i);
nt = modelGen.getNumTransitions(i);
for (j = 0; j < nt; j++) { for (j = 0; j < nt; j++) {
stateNew = engine.computeTransitionTarget(i, j);
stateNew = modelGen.computeTransitionTarget(i, j);
// Is this a new state? // Is this a new state?
if (states.add(stateNew)) { if (states.add(stateNew)) {
// If so, add to the explore list // If so, add to the explore list
@ -247,14 +258,14 @@ public class ConstructModel extends PrismComponent
if (!justReach) { if (!justReach) {
switch (modelType) { switch (modelType) {
case DTMC: case DTMC:
dtmc.addToProbability(src, dest, engine.getTransitionProbability(i, j));
dtmc.addToProbability(src, dest, modelGen.getTransitionProbability(i, j));
break; break;
case CTMC: case CTMC:
ctmc.addToProbability(src, dest, engine.getTransitionProbability(i, j));
ctmc.addToProbability(src, dest, modelGen.getTransitionProbability(i, j));
break; break;
case MDP: case MDP:
case CTMDP: case CTMDP:
distr.add(dest, engine.getTransitionProbability(i, j));
distr.add(dest, modelGen.getTransitionProbability(i, j));
break; break;
case STPG: case STPG:
case SMG: case SMG:
@ -267,13 +278,13 @@ public class ConstructModel extends PrismComponent
if (!justReach) { if (!justReach) {
if (modelType == ModelType.MDP) { if (modelType == ModelType.MDP) {
if (distinguishActions) { if (distinguishActions) {
mdp.addActionLabelledChoice(src, distr, engine.getTransitionAction(i, 0));
mdp.addActionLabelledChoice(src, distr, modelGen.getTransitionAction(i, 0));
} else { } else {
mdp.addChoice(src, distr); mdp.addChoice(src, distr);
} }
} else if (modelType == ModelType.CTMDP) { } else if (modelType == ModelType.CTMDP) {
if (distinguishActions) { if (distinguishActions) {
ctmdp.addActionLabelledChoice(src, distr, engine.getTransitionAction(i, 0));
ctmdp.addActionLabelledChoice(src, distr, modelGen.getTransitionAction(i, 0));
} else { } else {
ctmdp.addChoice(src, distr); ctmdp.addChoice(src, distr);
} }
@ -339,16 +350,46 @@ public class ConstructModel extends PrismComponent
throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s"); throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
} }
model.setStatesList(statesList); model.setStatesList(statesList);
model.setConstantValues(new Values(modulesFile.getConstantValues()));
model.setConstantValues(new Values(modelGen.getConstantValues()));
//mainLog.println("Model: " + model); //mainLog.println("Model: " + model);
} }
// Discard permutation // Discard permutation
permut = null; permut = null;
if (attachLabels)
attachLabels(modelGen, model);
return model; return model;
} }
private void attachLabels(ModelGenerator modelGen, ModelExplicit model) throws PrismException
{
// Get state info
List <State> statesList = model.getStatesList();
int numStates = statesList.size();
// Create storage for labels
int numLabels = modelGen.getNumLabels();
BitSet bitsets[] = new BitSet[numLabels];
for (int j = 0; j < numLabels; j++) {
bitsets[j] = new BitSet();
}
// Construct bitsets for labels
for (int i = 0; i < numStates; i++) {
State state = statesList.get(i);
modelGen.exploreState(state);
for (int j = 0; j < numLabels; j++) {
if (modelGen.isLabelTrue(j)) {
bitsets[j].set(i);
}
}
}
// Attach labels/bitsets
for (int j = 0; j < numLabels; j++) {
model.addLabel(modelGen.getLabelName(j), bitsets[j]);
}
}
/** /**
* Test method. * Test method.
*/ */
@ -358,13 +399,14 @@ public class ConstructModel extends PrismComponent
// Simple example: parse a PRISM file from a file, construct the model and export to a .tra file // Simple example: parse a PRISM file from a file, construct the model and export to a .tra file
PrismLog mainLog = new PrismPrintStreamLog(System.out); PrismLog mainLog = new PrismPrintStreamLog(System.out);
Prism prism = new Prism(mainLog, mainLog); Prism prism = new Prism(mainLog, mainLog);
ModulesFile modulesFile = prism.parseModelFile(new File(args[0]));
parser.ast.ModulesFile modulesFile = prism.parseModelFile(new File(args[0]));
UndefinedConstants undefinedConstants = new UndefinedConstants(modulesFile, null); UndefinedConstants undefinedConstants = new UndefinedConstants(modulesFile, null);
if (args.length > 2) if (args.length > 2)
undefinedConstants.defineUsingConstSwitch(args[2]); undefinedConstants.defineUsingConstSwitch(args[2]);
modulesFile.setUndefinedConstants(undefinedConstants.getMFConstantValues()); modulesFile.setUndefinedConstants(undefinedConstants.getMFConstantValues());
ConstructModel constructModel = new ConstructModel(prism, prism.getSimulator());
Model model = constructModel.constructModel(modulesFile);
ConstructModel constructModel = new ConstructModel(prism);
simulator.ModulesFileModelGenerator modelGen = new simulator.ModulesFileModelGenerator(modulesFile, constructModel);
Model model = constructModel.constructModel(modelGen);
model.exportToPrismExplicitTra(args[1]); model.exportToPrismExplicitTra(args[1]);
} catch (FileNotFoundException e) { } catch (FileNotFoundException e) {
System.out.println("Error: " + e.getMessage()); System.out.println("Error: " + e.getMessage());

9
prism/src/explicit/PrismExplicit.java
View File

@ -31,6 +31,7 @@ import java.io.*;
import parser.ast.*; import parser.ast.*;
import parser.type.TypeBool; import parser.type.TypeBool;
import prism.*; import prism.*;
import simulator.ModulesFileModelGenerator;
import simulator.SimulatorEngine; import simulator.SimulatorEngine;
import explicit.Model; import explicit.Model;
import explicit.StateModelChecker; import explicit.StateModelChecker;
@ -54,7 +55,7 @@ public class PrismExplicit extends PrismComponent
* @param modulesFile Model to build * @param modulesFile Model to build
* @param simEngine PRISM simulator engine (for model exploration) * @param simEngine PRISM simulator engine (for model exploration)
*/ */
public Model buildModel(ModulesFile modulesFile, SimulatorEngine simEngine) throws PrismException
public Model buildModel(ModulesFile modulesFile, ModelGenerator simEngine) throws PrismException
{ {
long l; // timer long l; // timer
Model modelExpl; Model modelExpl;
@ -67,11 +68,11 @@ public class PrismExplicit extends PrismComponent
mainLog.print("\nBuilding model...\n"); mainLog.print("\nBuilding model...\n");
// create translator // create translator
constructModel = new ConstructModel(this, simEngine);
constructModel = new ConstructModel(this);
// build model // build model
l = System.currentTimeMillis(); l = System.currentTimeMillis();
modelExpl = constructModel.constructModel(modulesFile, false, true);
modelExpl = constructModel.constructModel(simEngine);
l = System.currentTimeMillis() - l; l = System.currentTimeMillis() - l;
mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds."); mainLog.println("\nTime for model construction: " + l / 1000.0 + " seconds.");
@ -426,7 +427,7 @@ public class PrismExplicit extends PrismComponent
PropertiesFile propertiesFile = prism.parsePropertiesFile(modulesFile, new File(args[1])); PropertiesFile propertiesFile = prism.parsePropertiesFile(modulesFile, new File(args[1]));
propertiesFile.setUndefinedConstants(null); propertiesFile.setUndefinedConstants(null);
PrismExplicit pe = new PrismExplicit(prism.getMainLog(), prism.getSettings()); PrismExplicit pe = new PrismExplicit(prism.getMainLog(), prism.getSettings());
Model modelExpl = pe.buildModel(modulesFile, prism.getSimulator());
Model modelExpl = pe.buildModel(modulesFile, new ModulesFileModelGenerator(modulesFile, prism));
pe.modelCheck(modelExpl, modulesFile, propertiesFile, propertiesFile.getProperty(0)); pe.modelCheck(modelExpl, modulesFile, propertiesFile, propertiesFile.getProperty(0));
} catch (PrismException e) { } catch (PrismException e) {
System.out.println(e); System.out.println(e);

6
prism/src/explicit/QuantAbstractRefineExample.java
View File

@ -40,6 +40,7 @@ import prism.PrismLog;
import prism.PrismPrintStreamLog; import prism.PrismPrintStreamLog;
import prism.PrismNotSupportedException; import prism.PrismNotSupportedException;
import prism.UndefinedConstants; import prism.UndefinedConstants;
import simulator.ModulesFileModelGenerator;
public class QuantAbstractRefineExample extends QuantAbstractRefine public class QuantAbstractRefineExample extends QuantAbstractRefine
{ {
@ -327,8 +328,9 @@ public class QuantAbstractRefineExample extends QuantAbstractRefine
modulesFile = (ModulesFile) modulesFile.deepCopy().expandConstants(modulesFile.getConstantList()); modulesFile = (ModulesFile) modulesFile.deepCopy().expandConstants(modulesFile.getConstantList());
// Build the model (explicit-state reachability) // Build the model (explicit-state reachability)
ConstructModel constructModel = new ConstructModel(prism, prism.getSimulator());
ModelSimple model = (ModelSimple) constructModel.constructModel(modulesFile, false, false);
ConstructModel constructModel = new ConstructModel(prism);
constructModel.setBuildSparse(false);
ModelSimple model = (ModelSimple) constructModel.constructModel(new ModulesFileModelGenerator(modulesFile, prism));
model.exportToPrismExplicitTra(args[1]); model.exportToPrismExplicitTra(args[1]);
// Create/initialise abstraction-refinement engine // Create/initialise abstraction-refinement engine

9
prism/src/prism/Prism.java
View File

@ -59,6 +59,7 @@ import parser.ast.Property;
import pta.DigitalClocks; import pta.DigitalClocks;
import pta.PTAModelChecker; import pta.PTAModelChecker;
import simulator.GenerateSimulationPath; import simulator.GenerateSimulationPath;
import simulator.ModulesFileModelGenerator;
import simulator.PrismModelExplorer; import simulator.PrismModelExplorer;
import simulator.SimulatorEngine; import simulator.SimulatorEngine;
import simulator.method.SimulationMethod; import simulator.method.SimulationMethod;
@ -1917,9 +1918,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModel = mod2mtbdd.translate(); currentModel = mod2mtbdd.translate();
currentModelExpl = null; currentModelExpl = null;
} else { } else {
ConstructModel constructModel = new ConstructModel(this, getSimulator());
ConstructModel constructModel = new ConstructModel(this);
constructModel.setFixDeadlocks(getFixDeadlocks()); constructModel.setFixDeadlocks(getFixDeadlocks());
currentModelExpl = constructModel.constructModel(currentModulesFile, false, true);
currentModelExpl = constructModel.constructModel(new ModulesFileModelGenerator(currentModulesFile, this));
currentModel = null; currentModel = null;
} }
// if (...) ... currentModel = buildModelExplicit(currentModulesFile); // if (...) ... currentModel = buildModelExplicit(currentModulesFile);
@ -2070,8 +2071,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0) if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
mainLog.println("Model constants: " + currentDefinedMFConstants); mainLog.println("Model constants: " + currentDefinedMFConstants);
constructModel = new ConstructModel(this, getSimulator());
modelExpl = constructModel.constructModel(modulesFile);
constructModel = new ConstructModel(this);
modelExpl = constructModel.constructModel(new ModulesFileModelGenerator(modulesFile, this));
statesList = constructModel.getStatesList(); statesList = constructModel.getStatesList();
// create Explicit2MTBDD object // create Explicit2MTBDD object

Write Preview
Loading…
Cancel
Save