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

Refactor explicit engine product construction. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10393 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
e893970d22
commit
80c8dcd09d
1 changed files with 119 additions and 156 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 275
      prism/src/explicit/LTLModelChecker.java

275
prism/src/explicit/LTLModelChecker.java
View File

@ -278,143 +278,42 @@ public class LTLModelChecker extends PrismComponent
// Build product of model and automaton
mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product...");
LTLProduct<DTMC> product = constructProductMC(da, model, labelBS, statesOfInterest);
LTLProduct<DTMC> product = constructProductModel(da, model, labelBS, statesOfInterest);
mainLog.print("\n" + product.getProductModel().infoStringTable());
return product;
}
/**
* Construct the product of a DA and a DTMC.
* @param dra The DA
* @param dtmc The DTMC
* @param labelBS BitSets giving the set of states for each AP in the DA
* Generate a deterministic automaton for the given LTL formula
* and construct the product of this automaton with an MDP.
*
* @param mc a ProbModelChecker, used for checking maximal state formulas
* @param model the model
* @param expr a path expression
* @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @return The product DTMC
* @param allowedAcceptance the allowed acceptance conditions
* @return the product with the DA
* @throws PrismException
*/
public LTLProduct<DTMC> constructProductMC(DA<BitSet,? extends AcceptanceOmega> da, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
public LTLProduct<MDP> constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
{
DTMCSimple prodModel = new DTMCSimple();
int daSize = da.size();
int numAPs = da.getAPList().size();
int modelNumStates = dtmc.getNumStates();
int prodNumStates = modelNumStates * daSize;
int s_1, s_2, q_1, q_2;
BitSet s_labels = new BitSet(numAPs);
List<State> prodStatesList = null, daStatesList = null;
// Encoding:
// each state s' = <s, q> = s * daSize + q
// s(s') = s' / daSize
// q(s') = s' % daSize
LinkedList<Point> queue = new LinkedList<Point>();
int map[] = new int[prodNumStates];
Arrays.fill(map, -1);
if (dtmc.getStatesList() != null) {
prodStatesList = new ArrayList<State>();
daStatesList = new ArrayList<State>(da.size());
for (int i = 0; i < da.size(); i++) {
daStatesList.add(new State(1).setValue(0, i));
}
}
// We need results for all states of the original model in statesOfInterest
// We thus explore states of the product starting from these states.
// These are designated as initial states of the product model
// (a) to ensure reachability is done for these states; and
// (b) to later identify the corresponding product state for the original states
// of interest
for (int s_0 : new IterableStateSet(statesOfInterest, dtmc.getNumStates())) {
// Get BitSet representing APs (labels) satisfied by state s_0
for (int k = 0; k < numAPs; k++) {
s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_0));
}
// Find corresponding initial state in DA
int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels);
if (q_0 < 0) {
throw new PrismException("The deterministic automaton is not complete (state " + da.getStartState() + ")");
}
// Add (initial) state to product
queue.add(new Point(s_0, q_0));
prodModel.addState();
prodModel.addInitialState(prodModel.getNumStates() - 1);
map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1;
if (prodStatesList != null) {
// store DTMC state information for the product state
prodStatesList.add(new State(daStatesList.get(q_0), dtmc.getStatesList().get(s_0)));
}
}
// Product states
BitSet visited = new BitSet(prodNumStates);
while (!queue.isEmpty()) {
Point p = queue.pop();
s_1 = p.x;
q_1 = p.y;
visited.set(s_1 * daSize + q_1);
// Go through transitions from state s_1 in original DTMC
Iterator<Map.Entry<Integer, Double>> iter = dtmc.getTransitionsIterator(s_1);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
s_2 = e.getKey();
double prob = e.getValue();
// Get BitSet representing APs (labels) satisfied by successor state s_2
for (int k = 0; k < numAPs; k++) {
s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2));
}
// Find corresponding successor in DRA
q_2 = da.getEdgeDestByLabel(q_1, s_labels);
if (q_2 < 0) {
throw new PrismException("The deterministic automaton is not complete (state " + q_1 + ")");
}
// Add state/transition to model
if (!visited.get(s_2 * daSize + q_2) && map[s_2 * daSize + q_2] == -1) {
queue.add(new Point(s_2, q_2));
prodModel.addState();
map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1;
if (prodStatesList != null) {
// store DTMC state information for the product state
prodStatesList.add(new State(daStatesList.get(q_2), dtmc.getStatesList().get(s_2)));
}
}
prodModel.setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob);
}
}
// Build a mapping from state indices to states (s,q), encoded as (s * draSize + q)
int invMap[] = new int[prodModel.getNumStates()];
for (int i = 0; i < map.length; i++) {
if (map[i] != -1) {
invMap[map[i]] = i;
}
}
prodModel.findDeadlocks(false);
if (prodStatesList != null) {
prodModel.setStatesList(prodStatesList);
}
LTLProduct<DTMC> product = new LTLProduct<DTMC>(prodModel, dtmc, null, daSize, invMap);
// generate acceptance for the product model by lifting
product.setAcceptance(liftAcceptance(product, da.getAcceptance()));
// Convert LTL formula to automaton
Vector<BitSet> labelBS = new Vector<BitSet>();
DA<BitSet,? extends AcceptanceOmega> da;
da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance);
// lift the labels
for (String label : dtmc.getLabels()) {
BitSet liftedLabel = product.liftFromModel(dtmc.getLabelStates(label));
prodModel.addLabel(label, liftedLabel);
}
// Build product of model and automaton
mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
LTLProduct<MDP> product = constructProductModel(da, model, labelBS, statesOfInterest);
mainLog.print("\n" + product.getProductModel().infoStringTable());
return product;
}
/**
* Generate a deterministic automaton for the given LTL formula
* and construct the product of this automaton with an MDP.
* and construct the product of this automaton with a model.
*
* @param mc a ProbModelChecker, used for checking maximal state formulas
* @param model the model
@ -424,7 +323,7 @@ public class LTLModelChecker extends PrismComponent
* @return the product with the DA
* @throws PrismException
*/
public LTLProduct<MDP> constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
public <M extends Model> LTLProduct<M> constructProductSTPG(ProbModelChecker mc, M model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException
{
// Convert LTL formula to automaton
Vector<BitSet> labelBS = new Vector<BitSet>();
@ -432,44 +331,58 @@ public class LTLModelChecker extends PrismComponent
da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance);
// Build product of model and automaton
mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
LTLProduct<MDP> product = constructProductMDP(da, model, labelBS, statesOfInterest);
mainLog.println("\nConstructing " + model.getModelType() + "-" + da.getAutomataType() + " product...");
LTLProduct<M> product = constructProductModel(da, model, labelBS, statesOfInterest);
mainLog.print("\n" + product.getProductModel().infoStringTable());
return product;
}
/**
* Construct the product of a DA and an MDP.
* Construct the product of a DA and a model.
* @param da The DA
* @param mdp The MDP
* @param model The model
* @param labelBS BitSets giving the set of states for each AP in the DA
* @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @return The product MDP
* @return The product model
*/
public LTLProduct<MDP> constructProductMDP(DA<BitSet,? extends AcceptanceOmega> da, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
public <M extends Model> LTLProduct<M> constructProductModel(DA<BitSet,? extends AcceptanceOmega> da, M model, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
{
MDPSimple prodModel = new MDPSimple();
ModelType modelType = model.getModelType();
int daSize = da.size();
int numAPs = da.getAPList().size();
int modelNumStates = mdp.getNumStates();
int modelNumStates = model.getNumStates();
int prodNumStates = modelNumStates * daSize;
int s_1, s_2, q_1, q_2;
BitSet s_labels = new BitSet(numAPs);
List<State> prodStatesList = null, daStatesList = null;
// Create a (simple, mutable) model of the appropriate type
ModelSimple prodModel = null;
switch (modelType) {
case DTMC:
prodModel = new DTMCSimple();
break;
case MDP:
prodModel = new MDPSimple();
break;
case STPG:
prodModel = new STPGExplicit();
break;
default:
throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
}
// Encoding:
// each state s' = <s, q> = s * draSize + q
// s(s') = s' / draSize
// q(s') = s' % draSize
// each state s' = <s, q> = s * daSize + q
// s(s') = s' / daSize
// q(s') = s' % daSize
LinkedList<Point> queue = new LinkedList<Point>();
int map[] = new int[prodNumStates];
Arrays.fill(map, -1);
if (mdp.getStatesList() != null) {
if (model.getStatesList() != null) {
prodStatesList = new ArrayList<State>();
daStatesList = new ArrayList<State>(da.size());
for (int i = 0; i < da.size(); i++) {
@ -483,24 +396,31 @@ public class LTLModelChecker extends PrismComponent
// (a) to ensure reachability is done for these states; and
// (b) to later identify the corresponding product state for the original states
// of interest
for (int s_0 : new IterableStateSet(statesOfInterest, mdp.getNumStates())) {
for (int s_0 : new IterableStateSet(statesOfInterest, model.getNumStates())) {
// Get BitSet representing APs (labels) satisfied by state s_0
for (int k = 0; k < numAPs; k++) {
s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_0));
}
// Find corresponding initial state in DRA
// Find corresponding initial state in DA
int q_0 = da.getEdgeDestByLabel(da.getStartState(), s_labels);
if (q_0 < 0) {
throw new PrismException("The deterministic automaton is not complete (state " + da.getStartState() + ")");
}
// Add (initial) state to product
queue.add(new Point(s_0, q_0));
prodModel.addState();
switch (modelType) {
case STPG:
((STPGExplicit) prodModel).addState(((STPG) model).getPlayer(s_0));
break;
default:
prodModel.addState();
break;
}
prodModel.addInitialState(prodModel.getNumStates() - 1);
map[s_0 * daSize + q_0] = prodModel.getNumStates() - 1;
if (prodStatesList != null) {
// store MDP state information for the product state
prodStatesList.add(new State(daStatesList.get(q_0), mdp.getStatesList().get(s_0)));
// Store state information for the product
prodStatesList.add(new State(daStatesList.get(q_0), model.getStatesList().get(s_0)));
}
}
@ -512,11 +432,27 @@ public class LTLModelChecker extends PrismComponent
q_1 = p.y;
visited.set(s_1 * daSize + q_1);
// Go through transitions from state s_1 in original MDP
int numChoices = mdp.getNumChoices(s_1);
// Go through transitions from state s_1 in original model
int numChoices = (model instanceof NondetModel) ? ((NondetModel) model).getNumChoices(s_1) : 1;
for (int j = 0; j < numChoices; j++) {
Distribution prodDistr = new Distribution();
Iterator<Map.Entry<Integer, Double>> iter = mdp.getTransitionsIterator(s_1, j);
Iterator<Map.Entry<Integer, Double>> iter;
switch (modelType) {
case DTMC:
iter = ((DTMC) model).getTransitionsIterator(s_1);
break;
case MDP:
iter = ((MDP) model).getTransitionsIterator(s_1, j);
break;
case STPG:
iter = ((STPG) model).getTransitionsIterator(s_1, j);
break;
default:
throw new PrismNotSupportedException("Product construction not implemented for " + modelType + "s");
}
Distribution prodDistr = null;
if (modelType.nondeterministic()) {
prodDistr = new Distribution();
}
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
s_2 = e.getKey();
@ -525,7 +461,7 @@ public class LTLModelChecker extends PrismComponent
for (int k = 0; k < numAPs; k++) {
s_labels.set(k, labelBS.get(Integer.parseInt(da.getAPList().get(k).substring(1))).get(s_2));
}
// Find corresponding successor in DRA
// Find corresponding successor in DA
q_2 = da.getEdgeDestByLabel(q_1, s_labels);
if (q_2 < 0) {
throw new PrismException("The deterministic automaton is not complete (state " + q_1 + ")");
@ -533,20 +469,46 @@ public class LTLModelChecker extends PrismComponent
// Add state/transition to model
if (!visited.get(s_2 * daSize + q_2) && map[s_2 * daSize + q_2] == -1) {
queue.add(new Point(s_2, q_2));
prodModel.addState();
switch (modelType) {
case STPG:
((STPGExplicit) prodModel).addState(((STPG) model).getPlayer(s_2));
break;
default:
prodModel.addState();
break;
}
map[s_2 * daSize + q_2] = prodModel.getNumStates() - 1;
if (prodStatesList != null) {
// store MDP state information for the product state
prodStatesList.add(new State(daStatesList.get(q_2), mdp.getStatesList().get(s_2)));
// Store state information for the product
prodStatesList.add(new State(daStatesList.get(q_2), model.getStatesList().get(s_2)));
}
}
prodDistr.set(map[s_2 * daSize + q_2], prob);
switch (modelType) {
case DTMC:
((DTMCSimple) prodModel).setProbability(map[s_1 * daSize + q_1], map[s_2 * daSize + q_2], prob);
break;
case MDP:
case STPG:
prodDistr.set(map[s_2 * daSize + q_2], prob);
break;
default:
throw new PrismNotSupportedException("Product construction not implemented for " + modelType + "s");
}
}
switch (modelType) {
case MDP:
((MDPSimple) prodModel).addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, ((MDP) model).getAction(s_1, j));
break;
case STPG:
((STPGExplicit) prodModel).addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, ((STPG) model).getAction(s_1, j));
break;
default:
break;
}
prodModel.addActionLabelledChoice(map[s_1 * daSize + q_1], prodDistr, mdp.getAction(s_1, j));
}
}
// Build a mapping from state indices to states (s,q), encoded as (s * draSize + q)
// Build a mapping from state indices to states (s,q), encoded as (s * daSize + q)
int invMap[] = new int[prodModel.getNumStates()];
for (int i = 0; i < map.length; i++) {
if (map[i] != -1) {
@ -560,14 +522,15 @@ public class LTLModelChecker extends PrismComponent
prodModel.setStatesList(prodStatesList);
}
LTLProduct<MDP> product = new LTLProduct<MDP>(prodModel, mdp, null, daSize, invMap);
@SuppressWarnings("unchecked")
LTLProduct<M> product = new LTLProduct<M>((M) prodModel, model, null, daSize, invMap);
// generate acceptance for the product model by lifting
product.setAcceptance(liftAcceptance(product, da.getAcceptance()));
// lift the labels
for (String label : mdp.getLabels()) {
BitSet liftedLabel = product.liftFromModel(mdp.getLabelStates(label));
for (String label : model.getLabels()) {
BitSet liftedLabel = product.liftFromModel(model.getLabelStates(label));
prodModel.addLabel(label, liftedLabel);
}

Write Preview
Loading…
Cancel
Save