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

Refactor: switch from prism.DRA<BitSet> to prism.DA<BitSet, AcceptanceRabin>. Changes access to the Rabin pairs. [Joachim Klein] 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9578 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
02aa30d5bf
commit
c00ffea7d8
10 changed files with 105 additions and 91 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. 7
      prism/src/explicit/DTMCModelChecker.java
  2. 26
      prism/src/explicit/LTLModelChecker.java
  3. 7
      prism/src/explicit/MDPModelChecker.java
  4. 22
      prism/src/jltl2dstar/DRA.java
  5. 4
      prism/src/jltl2dstar/LTL2Rabin.java
  6. 29
      prism/src/prism/LTL2RabinLibrary.java
  7. 51
      prism/src/prism/LTLModelChecker.java
  8. 30
      prism/src/prism/MultiObjModelChecker.java
  9. 15
      prism/src/prism/NondetModelChecker.java
  10. 5
      prism/src/prism/ProbModelChecker.java

7
prism/src/explicit/DTMCModelChecker.java
View File

@ -32,9 +32,10 @@ import java.util.List;
import java.util.Map;
import java.util.Vector;
import acceptance.AcceptanceRabin;
import parser.ast.Expression;
import parser.type.TypeDouble;
import prism.DRA;
import prism.DA;
import prism.Pair;
import prism.PrismComponent;
import prism.PrismException;
@ -64,7 +65,7 @@ public class DTMCModelChecker extends ProbModelChecker
LTLModelChecker mcLtl;
StateValues probsProduct, probs;
Expression ltl;
DRA<BitSet> dra;
DA<BitSet,AcceptanceRabin> dra;
Model modelProduct;
DTMCModelChecker mcProduct;
long time;
@ -86,7 +87,7 @@ public class DTMCModelChecker extends ProbModelChecker
time = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
int draSize = dra.size();
mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time;
mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
// If required, export DRA

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

@ -36,8 +36,8 @@ import java.util.List;
import java.util.Map;
import java.util.Vector;
import acceptance.AcceptanceRabin;
import common.IterableStateSet;
import parser.ast.Expression;
import parser.ast.ExpressionBinaryOp;
import parser.ast.ExpressionLabel;
@ -45,7 +45,7 @@ import parser.ast.ExpressionTemporal;
import parser.ast.ExpressionUnaryOp;
import parser.type.TypeBool;
import parser.type.TypePathBool;
import prism.DRA;
import prism.DA;
import prism.LTL2RabinLibrary;
import prism.Pair;
import prism.PrismComponent;
@ -68,7 +68,7 @@ public class LTLModelChecker extends PrismComponent
* Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
* in which atomic propositions are represented by ExpressionLabel objects.
*/
public static DRA<BitSet> convertLTLFormulaToDRA(Expression ltl) throws PrismException
public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl) throws PrismException
{
return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl);
}
@ -135,7 +135,7 @@ public class LTLModelChecker extends PrismComponent
* @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @return The product DTMC and a list of each of its states (s,q), encoded as (s * draSize + q)
*/
public Pair<Model, int[]> constructProductMC(DRA<BitSet> dra, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
public Pair<Model, int[]> constructProductMC(DA<BitSet,AcceptanceRabin> dra, DTMC dtmc, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
{
DTMCSimple prodModel = new DTMCSimple();
@ -226,7 +226,7 @@ public class LTLModelChecker extends PrismComponent
* @param statesOfInterest the set of states for which values should be calculated (null = all states)
* @return The product MDP and a list of each of its states (s,q), encoded as (s * draSize + q)
*/
public Pair<NondetModel, int[]> constructProductMDP(DRA<BitSet> dra, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
public Pair<NondetModel, int[]> constructProductMDP(DA<BitSet,AcceptanceRabin> dra, MDP mdp, Vector<BitSet> labelBS, BitSet statesOfInterest) throws PrismException
{
MDPSimple prodModel = new MDPSimple();
@ -320,7 +320,7 @@ public class LTLModelChecker extends PrismComponent
* @param model The model
* @param invMap The map returned by the constructProduct method(s)
*/
public BitSet findAcceptingBSCCsForRabin(DRA<BitSet> dra, Model model, int invMap[]) throws PrismException
public BitSet findAcceptingBSCCsForRabin(DA<BitSet,AcceptanceRabin> dra, Model model, int invMap[]) throws PrismException
{
// Compute bottom strongly connected components (BSCCs)
SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model);
@ -328,7 +328,7 @@ public class LTLModelChecker extends PrismComponent
List<BitSet> bsccs = sccComputer.getBSCCs();
int draSize = dra.size();
int numAcceptancePairs = dra.getNumAcceptancePairs();
int numAcceptancePairs = dra.getAcceptance().size();
BitSet result = new BitSet();
for (BitSet bscc : bsccs) {
@ -337,8 +337,8 @@ public class LTLModelChecker extends PrismComponent
boolean isLEmpty = true;
boolean isKEmpty = true;
BitSet L = dra.getAcceptanceL(acceptancePair);
BitSet K = dra.getAcceptanceK(acceptancePair);
BitSet L = dra.getAcceptance().get(acceptancePair).getL();
BitSet K = dra.getAcceptance().get(acceptancePair).getK();
for (int state = bscc.nextSetBit(0); state != -1; state = bscc.nextSetBit(state + 1)) {
int draState = invMap[state] % draSize;
isLEmpty &= !L.get(draState);
@ -362,16 +362,16 @@ public class LTLModelChecker extends PrismComponent
* @param model The model
* @param invMap The map returned by the constructProduct method(s)
*/
public BitSet findAcceptingECStatesForRabin(DRA<BitSet> dra, NondetModel model, int invMap[]) throws PrismException
public BitSet findAcceptingECStatesForRabin(DA<BitSet,AcceptanceRabin> dra, NondetModel model, int invMap[]) throws PrismException
{
BitSet allAcceptingStates = new BitSet();
int numStates = model.getNumStates();
int draSize = dra.size();
// Go through the DRA acceptance pairs (L_i, K_i)
for (int i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (int i = 0; i < dra.getAcceptance().size(); i++) {
// Find model states *not* satisfying L_i
BitSet bitsetLi = dra.getAcceptanceL(i);
BitSet bitsetLi = dra.getAcceptance().get(i).getL();
BitSet statesLi_not = new BitSet();
for (int s = 0; s < numStates; s++) {
if (!bitsetLi.get(invMap[s] % draSize)) {
@ -386,7 +386,7 @@ public class LTLModelChecker extends PrismComponent
ecComputer.computeMECStates(statesLi_not);
List<BitSet> mecs = ecComputer.getMECStates();
// Check with MECs contain a K_i state
BitSet bitsetKi = dra.getAcceptanceK(i);
BitSet bitsetKi = dra.getAcceptance().get(i).getK();
for (BitSet mec : mecs) {
for (int s = mec.nextSetBit(0); s != -1; s = mec.nextSetBit(s + 1)) {
if (bitsetKi.get(invMap[s] % draSize)) {

7
prism/src/explicit/MDPModelChecker.java
View File

@ -32,8 +32,9 @@ import java.util.List;
import java.util.Map;
import java.util.Vector;
import acceptance.AcceptanceRabin;
import parser.ast.Expression;
import prism.DRA;
import prism.DA;
import prism.Pair;
import prism.PrismComponent;
import prism.PrismDevNullLog;
@ -67,7 +68,7 @@ public class MDPModelChecker extends ProbModelChecker
LTLModelChecker mcLtl;
StateValues probsProduct, probs;
Expression ltl;
DRA<BitSet> dra;
DA<BitSet,AcceptanceRabin> dra;
NondetModel modelProduct;
MDPModelChecker mcProduct;
long time;
@ -94,7 +95,7 @@ public class MDPModelChecker extends ProbModelChecker
time = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
int draSize = dra.size();
mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
time = System.currentTimeMillis() - time;
mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
// If required, export DRA

22
prism/src/jltl2dstar/DRA.java
View File

@ -26,9 +26,9 @@ import java.io.FileWriter;
import java.io.PrintStream;
import java.util.*;
import acceptance.AcceptanceRabin;
import jltl2ba.APElement;
import jltl2ba.APSet;
import prism.PrismException;
/**
@ -146,17 +146,18 @@ public class DRA extends DA {
/**
* Convert the DRA from jltl2dstar to PRISM data structures.
*/
public prism.DRA<BitSet> createPrismDRA() throws PrismException
public prism.DA<BitSet,AcceptanceRabin> createPrismDRA() throws PrismException
{
int i, k, numLabels, numStates, src, dest;
List<String> apList;
BitSet bitset, bitset2;
BitSet bitset;
RabinAcceptance acc;
prism.DRA<BitSet> draNew;
prism.DA<BitSet,AcceptanceRabin> draNew;
AcceptanceRabin accNew = new AcceptanceRabin();
numLabels = getAPSize();
numStates = size();
draNew = new prism.DRA<BitSet>(numStates);
draNew = new prism.DA<BitSet,AcceptanceRabin>(numStates);
// Copy AP set
apList = new ArrayList<String>(numLabels);
for (i = 0; i < numLabels; i++) {
@ -181,14 +182,15 @@ public class DRA extends DA {
// Copy acceptance pairs
acc = acceptance();
for (i = 0; i < acc.size(); i++) {
bitset = new BitSet();
bitset.or(acc.getAcceptance_U(i));
bitset2 = new BitSet();
bitset2.or(acc.getAcceptance_L(i));
// Note: Pairs (U_i,L_i) become (L_i,K_i) in PRISM's notation
draNew.addAcceptancePair(bitset, bitset2);
BitSet newL = (BitSet)acc.getAcceptance_U(i).clone();
BitSet newK = (BitSet)acc.getAcceptance_L(i).clone();
AcceptanceRabin.RabinPair pair = new AcceptanceRabin.RabinPair(newL, newK);
accNew.add(pair);
}
draNew.setAcceptance(accNew);
return draNew;
}

4
prism/src/jltl2dstar/LTL2Rabin.java
View File

@ -27,9 +27,11 @@ import prism.PrismException;
import java.util.BitSet;
import acceptance.AcceptanceRabin;
public class LTL2Rabin {
public static prism.DRA<BitSet> ltl2rabin(SimpleLTL ltlFormula) throws PrismException {
public static prism.DA<BitSet,AcceptanceRabin> ltl2rabin(SimpleLTL ltlFormula) throws PrismException {
SimpleLTL ltl = ltlFormula.simplify();
return ltl2rabin(ltl, ltl.getAPs()).createPrismDRA();
}

29
prism/src/prism/LTL2RabinLibrary.java
View File

@ -29,6 +29,8 @@ package prism;
import java.io.*;
import java.util.*;
import acceptance.AcceptanceRabin;
import acceptance.AcceptanceRabin.RabinPair;
import jltl2dstar.*;
import parser.ast.*;
import parser.visitor.ASTTraverse;
@ -65,7 +67,7 @@ public class LTL2RabinLibrary
* Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
* in which atomic propositions are represented by ExpressionLabel objects.
*/
public static DRA<BitSet> convertLTLFormulaToDRA(Expression ltl) throws PrismException
public static DA<BitSet, AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl) throws PrismException
{
// Get list of labels appearing
labels = new ArrayList<String>();
@ -104,17 +106,19 @@ public class LTL2RabinLibrary
* Create a DRA from a string, e.g.:
* "2 states (start 0), 1 labels: 0-{0}->1 0-{}->0 1-{0}->1 1-{}->0; 1 acceptance pairs: ({},{1})"
*/
private static DRA<BitSet> createDRAFromString(String s, List<String> labels) throws PrismException
private static DA<BitSet,AcceptanceRabin> createDRAFromString(String s, List<String> labels) throws PrismException
{
int ptr = 0, i, j, k, n, from, to;
String bs;
prism.DRA<BitSet> draNew;
DA<BitSet,AcceptanceRabin> draNew;
AcceptanceRabin acceptance = new AcceptanceRabin();
try {
// Num states
j = s.indexOf("states", ptr);
n = Integer.parseInt(s.substring(0, j).trim());
draNew = new prism.DRA<BitSet>(n);
draNew = new DA<BitSet,AcceptanceRabin>(n);
draNew.setAcceptance(acceptance);
draNew.setAPList(labels);
// Start state
i = s.indexOf("start", j) + 6;
@ -141,7 +145,9 @@ public class LTL2RabinLibrary
while (i != -1) {
j = s.indexOf("},{", i);
k = s.indexOf("})", j);
draNew.addAcceptancePair(createBitSetFromString(s.substring(i + 2, j)), createBitSetFromString(s.substring(j + 3, k)));
BitSet L = createBitSetFromString(s.substring(i + 2, j));
BitSet K = createBitSetFromString(s.substring(j + 3, k));
acceptance.add(new AcceptanceRabin.RabinPair(L,K));
i = s.indexOf("({", k);
}
} catch (NumberFormatException e) {
@ -170,15 +176,16 @@ public class LTL2RabinLibrary
}
// Example: manual creation of DRA for: !(F ("L0"&(X "L1")))
public static DRA<BitSet> draForNotFaCb(String l0, String l1) throws PrismException
public static DA<BitSet,AcceptanceRabin> draForNotFaCb(String l0, String l1) throws PrismException
{
int numStates;
List<String> apList;
prism.DRA<BitSet> draNew;
DA<BitSet,AcceptanceRabin> draNew;
// 4 states (start 3), 2 labels: 0-{1}->0 0-{0, 1}->1 0-{}->0 0-{0}->1 1-{1}->2 1-{0, 1}->2 1-{}->0 1-{0}->1 2-{1}->2 2-{0, 1}->2 2-{}->2 2-{0}->2 3-{1}->0 3-{0, 1}->1 3-{}->0 3-{0}->1; 1 acceptance pairs: ({2},{0, 1})
numStates = 4;
draNew = new prism.DRA<BitSet>(numStates);
draNew = new DA<BitSet,AcceptanceRabin>(numStates);
draNew.setAcceptance(new AcceptanceRabin());
// AP set
apList = new ArrayList<String>(2);
apList.add(l0);
@ -219,7 +226,7 @@ public class LTL2RabinLibrary
BitSet bitsetK = new BitSet();
bitsetK.set(01);
bitsetK.set(1);
draNew.addAcceptancePair(bitsetL, bitsetK);
draNew.getAcceptance().add(new AcceptanceRabin.RabinPair(bitsetL, bitsetK));
return draNew;
}
@ -241,9 +248,9 @@ public class LTL2RabinLibrary
System.out.println(ltl);
System.out.println(expr.toString());
System.out.println(ltl.equals(expr.toString()));
DRA<BitSet> dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba());
DA<BitSet,AcceptanceRabin> dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba());
System.out.println(dra1);
DRA<BitSet> dra2 = convertLTLFormulaToDRA(expr);
DA<BitSet,AcceptanceRabin> dra2 = convertLTLFormulaToDRA(expr);
System.out.println(dra2);
System.out.println(dra1.toString().equals(dra2.toString()));
//dra2.printDot(new PrintStream(new File("dra")));

51
prism/src/prism/LTLModelChecker.java
View File

@ -32,6 +32,7 @@ import java.util.BitSet;
import java.util.List;
import java.util.Vector;
import acceptance.AcceptanceRabin;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
@ -63,7 +64,7 @@ public class LTLModelChecker extends PrismComponent
* Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
* in which atomic propositions are represented by ExpressionLabel objects.
*/
public static DRA<BitSet> convertLTLFormulaToDRA(Expression ltl) throws PrismException
public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl) throws PrismException
{
return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl);
}
@ -129,7 +130,7 @@ public class LTLModelChecker extends PrismComponent
* @param model The DTMC/CTMC
* @param labelDDs BDDs giving the set of states for each AP in the DRA
*/
public ProbModel constructProductMC(DRA<BitSet> dra, ProbModel model, Vector<JDDNode> labelDDs) throws PrismException
public ProbModel constructProductMC(DA<BitSet,AcceptanceRabin> dra, ProbModel model, Vector<JDDNode> labelDDs) throws PrismException
{
return constructProductMC(dra, model, labelDDs, null, null, true);
}
@ -142,7 +143,7 @@ public class LTLModelChecker extends PrismComponent
* @param draDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA
* @param draDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
*/
public ProbModel constructProductMC(DRA<BitSet> dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
public ProbModel constructProductMC(DA<BitSet,AcceptanceRabin> dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
throws PrismException
{
return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true);
@ -158,7 +159,7 @@ public class LTLModelChecker extends PrismComponent
* @param allInit Do we assume that all states of the original model are initial states?
* (just for the purposes of reachability)
*/
public ProbModel constructProductMC(DRA<BitSet> dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy,
public ProbModel constructProductMC(DA<BitSet,AcceptanceRabin> dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy,
boolean allInit) throws PrismException
{
// Existing model - dds, vars, etc.
@ -329,7 +330,7 @@ public class LTLModelChecker extends PrismComponent
* @param model The MDP
* @param labelDDs BDDs giving the set of states for each AP in the DRA
*/
public NondetModel constructProductMDP(DRA<BitSet> dra, NondetModel model, Vector<JDDNode> labelDDs) throws PrismException
public NondetModel constructProductMDP(DA<BitSet,AcceptanceRabin> dra, NondetModel model, Vector<JDDNode> labelDDs) throws PrismException
{
return constructProductMDP(dra, model, labelDDs, null, null, true, null);
}
@ -342,7 +343,7 @@ public class LTLModelChecker extends PrismComponent
* @param draDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA
* @param draDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
*/
public NondetModel constructProductMDP(DRA<BitSet> dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
public NondetModel constructProductMDP(DA<BitSet,AcceptanceRabin> dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
throws PrismException
{
return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true, null);
@ -360,7 +361,7 @@ public class LTLModelChecker extends PrismComponent
* @param init The initial state(s) (of the original model) used to build the product;
* if null; we just take the existing initial states from model.getStart().
*/
public NondetModel constructProductMDP(DRA<BitSet> dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy,
public NondetModel constructProductMDP(DA<BitSet,AcceptanceRabin> dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy,
boolean allInit, JDDNode init) throws PrismException
{
// Existing model - dds, vars, etc.
@ -551,7 +552,7 @@ public class LTLModelChecker extends PrismComponent
* So the BDD is over column variables for model states (permuted from those found in the BDDs in
* {@code labelDDs}) and row/col variables for the DRA (from {@code draDDRowVars}, {@code draDDColVars}).
*/
public JDDNode buildTransMask(DRA<BitSet> dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars,
public JDDNode buildTransMask(DA<BitSet,AcceptanceRabin> dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars,
JDDVars draDDColVars)
{
JDDNode draMask, label, exprBDD, transition;
@ -595,7 +596,7 @@ public class LTLModelChecker extends PrismComponent
* So the BDD is over row variables for model states (as found in the BDDs in {@code labelDDs})
* and row variables for the DRA (from {@code draDDRowVars}).
*/
public JDDNode buildStartMask(DRA<BitSet> dra, Vector<JDDNode> labelDDs, JDDVars draDDRowVars)
public JDDNode buildStartMask(DA<BitSet,AcceptanceRabin> dra, Vector<JDDNode> labelDDs, JDDVars draDDRowVars)
{
JDDNode startMask, label, exprBDD, dest, tmp;
int i, j, k, numAPs, numEdges;
@ -636,9 +637,9 @@ public class LTLModelChecker extends PrismComponent
* the set L_i from the i-th pair (L_i,K_i) of the acceptance condition for a DRA.
* @param complement If true, build the complement of the set L_i instead
*/
public JDDNode buildLStatesForRabinPair(JDDVars draDDRowVars, DRA<BitSet> dra, int i, boolean complement)
public JDDNode buildLStatesForRabinPair(JDDVars draDDRowVars, DA<BitSet,AcceptanceRabin> dra, int i, boolean complement)
{
BitSet bitsetLi = dra.getAcceptanceL(i);
BitSet bitsetLi = dra.getAcceptance().get(i).getL();
JDDNode statesLi = JDD.Constant(0);
for (int j = 0; j < dra.size(); j++) {
if (bitsetLi.get(j) ^ complement) {
@ -652,9 +653,9 @@ public class LTLModelChecker extends PrismComponent
* Build a (referenced) BDD over variables {@code draDDRowVars} representing
* the set K_i from the i-th pair (L_i,K_i) of the acceptance condition for a DRA.
*/
public JDDNode buildKStatesForRabinPair(JDDVars draDDRowVars, DRA<BitSet> dra, int i)
public JDDNode buildKStatesForRabinPair(JDDVars draDDRowVars, DA<BitSet,AcceptanceRabin> dra, int i)
{
BitSet bitsetKi = dra.getAcceptanceK(i);
BitSet bitsetKi = dra.getAcceptance().get(i).getK();
JDDNode statesKi = JDD.Constant(0);
for (int j = 0; j < dra.size(); j++) {
if (bitsetKi.get(j)) {
@ -672,7 +673,7 @@ public class LTLModelChecker extends PrismComponent
* @param model The model
* @return A referenced BDD for the union of all states in accepting BSCCs
*/
public JDDNode findAcceptingBSCCsForRabin(DRA<BitSet> dra, ProbModel model, JDDVars draDDRowVars, JDDVars draDDColVars) throws PrismException
public JDDNode findAcceptingBSCCsForRabin(DA<BitSet,AcceptanceRabin> dra, ProbModel model, JDDVars draDDRowVars, JDDVars draDDColVars) throws PrismException
{
JDDNode allAcceptingStates;
List<JDDNode> vectBSCCs;
@ -688,7 +689,7 @@ public class LTLModelChecker extends PrismComponent
// Build BDDs for !L_i and K_i
ArrayList<JDDNode> statesL_not = new ArrayList<JDDNode>();
ArrayList<JDDNode> statesK = new ArrayList<JDDNode>();
for (i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (i = 0; i < dra.getAcceptance().size(); i++) {
statesL_not.add(buildLStatesForRabinPair(draDDRowVars, dra, i, true));
statesK.add(buildKStatesForRabinPair(draDDRowVars, dra, i));
}
@ -696,7 +697,7 @@ public class LTLModelChecker extends PrismComponent
// Go through the BSCCs
for (JDDNode bscc : vectBSCCs) {
// Go through the DRA acceptance pairs (L_i, K_i)
for (i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (i = 0; i < dra.getAcceptance().size(); i++) {
// Check each BSCC for inclusion in !L_i and intersection with K_i
if (JDD.IsContainedIn(bscc, statesL_not.get(i)) && JDD.AreInterecting(bscc, statesK.get(i))) {
// This BSCC is accepting: add and move on onto next one
@ -726,7 +727,7 @@ public class LTLModelChecker extends PrismComponent
* @param fairness Consider fairness?
* @return A referenced BDD for the union of all states in accepting MECs
*/
public JDDNode findAcceptingECStatesForRabin(DRA<BitSet> dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness)
public JDDNode findAcceptingECStatesForRabin(DA<BitSet,AcceptanceRabin> dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness)
throws PrismException
{
JDDNode acceptingStates = null, allAcceptingStates, acceptanceVector_L_not, acceptanceVector_K, candidateStates;
@ -734,13 +735,13 @@ public class LTLModelChecker extends PrismComponent
allAcceptingStates = JDD.Constant(0);
if (dra.getNumAcceptancePairs() > 1) {
if (dra.getAcceptance().size() > 1) {
acceptanceVector_L_not = JDD.Constant(0);
acceptanceVector_K = JDD.Constant(0);
ArrayList<JDDNode> statesLnot = new ArrayList<JDDNode>();
ArrayList<JDDNode> statesK = new ArrayList<JDDNode>();
for (i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (i = 0; i < dra.getAcceptance().size(); i++) {
JDDNode tmpLnot = buildLStatesForRabinPair(draDDRowVars, dra, i, true);
JDDNode tmpK = buildKStatesForRabinPair(draDDRowVars, dra, i);
statesLnot.add(tmpLnot);
@ -763,7 +764,7 @@ public class LTLModelChecker extends PrismComponent
JDD.Deref(acceptanceVector_K);
JDD.Deref(candidateStates);
for (i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (i = 0; i < dra.getAcceptance().size(); i++) {
// build the acceptance vectors L_i and K_i
acceptanceVector_L_not = statesLnot.get(i);
acceptanceVector_K = statesK.get(i);
@ -813,7 +814,7 @@ public class LTLModelChecker extends PrismComponent
JDD.Deref(ec);
} else {
// Go through the DRA acceptance pairs (L_i, K_i)
for (i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (i = 0; i < dra.getAcceptance().size(); i++) {
// Build BDDs for !L_i and K_i
JDDNode statesLi_not = buildLStatesForRabinPair(draDDRowVars, dra, i, true);
JDDNode statesK_i = buildKStatesForRabinPair(draDDRowVars, dra, i);
@ -856,7 +857,7 @@ public class LTLModelChecker extends PrismComponent
return allAcceptingStates;
}
public JDDNode findMultiAcceptingStates(DRA<BitSet> dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness,
public JDDNode findMultiAcceptingStates(DA<BitSet,AcceptanceRabin> dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness,
List<JDDNode> allecs, List<JDDNode> statesH, List<JDDNode> statesL) throws PrismException
{
JDDNode acceptingStates = null, allAcceptingStates, candidateStates;
@ -867,7 +868,7 @@ public class LTLModelChecker extends PrismComponent
// for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i
// and compute the maximal ECs in H'_i
for (i = 0; i < dra.getNumAcceptancePairs(); i++) {
for (i = 0; i < dra.getAcceptance().size(); i++) {
// build the acceptance vectors H_i and L_i
acceptanceVector_H = statesH.get(i);
acceptanceVector_L = statesL.get(i);
@ -920,7 +921,7 @@ public class LTLModelChecker extends PrismComponent
return allAcceptingStates;
}
public void findMultiConflictAcceptingStates(DRA<BitSet>[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List<JDDNode> targetDDs,
public void findMultiConflictAcceptingStates(DA<BitSet,AcceptanceRabin>[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List<JDDNode> targetDDs,
List<List<JDDNode>> allstatesH, List<List<JDDNode>> allstatesL, List<JDDNode> combinations, List<List<Integer>> combinationIDs)
throws PrismException
{
@ -961,7 +962,7 @@ public class LTLModelChecker extends PrismComponent
}
}
private void computeCombinations(DRA<BitSet>[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List<JDDNode> targetDDs,
private void computeCombinations(DA<BitSet,AcceptanceRabin>[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List<JDDNode> targetDDs,
List<List<JDDNode>> allstatesH, List<List<JDDNode>> allstatesL, List<queueElement> queue, int sp) throws PrismException
{
queueElement e = queue.get(sp);

30
prism/src/prism/MultiObjModelChecker.java
View File

@ -35,15 +35,13 @@ import java.util.BitSet;
import java.util.List;
import java.util.Vector;
import acceptance.AcceptanceRabin;
import parser.ast.Expression;
import parser.ast.RelOp;
import dv.DoubleVector;
import mtbdd.PrismMTBDD;
import sparse.NDSparseMatrix;
import sparse.PrismSparse;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
@ -67,7 +65,7 @@ public class MultiObjModelChecker extends PrismComponent
}
//TODO: dra's element is changed here, not neat.
protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DRA<BitSet> dra[], Operator operator,
protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DA<BitSet,AcceptanceRabin> dra[], Operator operator,
Expression targetExpr, JDDVars draDDRowVars, JDDVars draDDColVars, JDDNode ddStateIndex) throws PrismException
{
// Model check maximal state formulas
@ -82,7 +80,7 @@ public class MultiObjModelChecker extends PrismComponent
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
long l = System.currentTimeMillis();
dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl);
mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs.");
mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics()+".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
// If required, export DRA
@ -165,7 +163,7 @@ public class MultiObjModelChecker extends PrismComponent
//computes accepting end component for the Rabin automaton dra.
//Vojta: in addition to calling a method which does the computation
//there are some other bits which I don't currently understand
protected JDDNode computeAcceptingEndComponent(DRA<BitSet> dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars,
protected JDDNode computeAcceptingEndComponent(DA<BitSet,AcceptanceRabin> dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars,
List<JDDNode> allecs, List<JDDNode> statesH, List<JDDNode> statesL, //Vojta: at the time of writing this I have no idea what these two parameters do, so I don't know how to call them
LTLModelChecker mcLtl, boolean conflictformulaeGtOne, String name) throws PrismException
{
@ -186,7 +184,7 @@ public class MultiObjModelChecker extends PrismComponent
}
protected void removeNonZeroMecsForMax(NondetModel modelProduct, LTLModelChecker mcLtl, List<JDDNode> rewardsIndex, OpsAndBoundsList opsAndBounds,
int numTargets, DRA<BitSet> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException
int numTargets, DA<BitSet,AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException
{
List<JDDNode> mecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach());
JDDNode removedActions = JDD.Constant(0);
@ -230,7 +228,7 @@ public class MultiObjModelChecker extends PrismComponent
Vector<JDDNode> tmptargetDDs = new Vector<JDDNode>();
List<JDDNode> tmpmultitargetDDs = new ArrayList<JDDNode>();
List<Integer> tmpmultitargetIDs = new ArrayList<Integer>();
ArrayList<DRA<BitSet>> tmpdra = new ArrayList<DRA<BitSet>>();
ArrayList<DA<BitSet,AcceptanceRabin>> tmpdra = new ArrayList<DA<BitSet,AcceptanceRabin>>();
ArrayList<JDDVars> tmpdraDDRowVars = new ArrayList<JDDVars>();
ArrayList<JDDVars> tmpdraDDColVars = new ArrayList<JDDVars>();
int count = 0;
@ -244,7 +242,7 @@ public class MultiObjModelChecker extends PrismComponent
}
if (count > 0) {
// TODO: distinguish whether rtarget is empty
DRA newdra[] = new DRA[count];
DA<BitSet,AcceptanceRabin> newdra[] = new DA[count];
tmpdra.toArray(newdra);
JDDVars newdraDDRowVars[] = new JDDVars[count];
tmpdraDDRowVars.toArray(newdraDDRowVars);
@ -298,11 +296,11 @@ public class MultiObjModelChecker extends PrismComponent
//TODO is conflictformulae actually just no of prob?
protected void checkConflictsInObjectives(NondetModel modelProduct, LTLModelChecker mcLtl, int conflictformulae, int numTargets,
OpsAndBoundsList opsAndBounds, DRA<BitSet> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs,
OpsAndBoundsList opsAndBounds, DA<BitSet,AcceptanceRabin> dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs,
List<ArrayList<JDDNode>> allstatesH, List<ArrayList<JDDNode>> allstatesL, List<JDDNode> multitargetDDs, List<Integer> multitargetIDs)
throws PrismException
{
DRA[] tmpdra = new DRA[conflictformulae];
DA<BitSet,AcceptanceRabin>[] tmpdra = new DA[conflictformulae];
JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae];
JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae];
List<JDDNode> tmptargetDDs = new ArrayList<JDDNode>(conflictformulae);
@ -350,7 +348,7 @@ public class MultiObjModelChecker extends PrismComponent
}
}
protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], DRA dra[],
protected void findTargetStates(NondetModel modelProduct, LTLModelChecker mcLtl, int numTargets, int conflictformulae, boolean reachExpr[], DA<BitSet,AcceptanceRabin> dra[],
JDDVars draDDRowVars[], JDDVars draDDColVars[], List<JDDNode> targetDDs, List<JDDNode> multitargetDDs, List<Integer> multitargetIDs)
throws PrismException
{
@ -366,14 +364,14 @@ public class MultiObjModelChecker extends PrismComponent
if (!reachExpr[i]) {
ArrayList<JDDNode> statesH = new ArrayList<JDDNode>();
ArrayList<JDDNode> statesL = new ArrayList<JDDNode>();
for (int k = 0; k < dra[i].getNumAcceptancePairs(); k++) {
for (int k = 0; k < dra[i].getAcceptance().size(); k++) {
JDDNode tmpH = JDD.Constant(0);
JDDNode tmpL = JDD.Constant(0);
for (j = 0; j < dra[i].size(); j++) {
if (!dra[i].getAcceptanceL(k).get(j)) {
if (!dra[i].getAcceptance().get(k).getL().get(j)) {
tmpH = JDD.SetVectorElement(tmpH, draDDRowVars[i], j, 1.0);
}
if (dra[i].getAcceptanceK(k).get(j)) {
if (dra[i].getAcceptance().get(k).getK().get(j)) {
tmpL = JDD.SetVectorElement(tmpL, draDDRowVars[i], j, 1.0);
}
}
@ -455,7 +453,7 @@ public class MultiObjModelChecker extends PrismComponent
// check if there are conflicts in objectives
if (conflictformulae > 1) {
DRA[] tmpdra = new DRA[conflictformulae];
DA<BitSet,AcceptanceRabin>[] tmpdra = new DA[conflictformulae];
JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae];
JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae];
List<JDDNode> tmptargetDDs = new ArrayList<JDDNode>(conflictformulae);

15
prism/src/prism/NondetModelChecker.java
View File

@ -33,6 +33,7 @@ import java.io.File;
import java.io.FileNotFoundException;
import java.util.*;
import acceptance.AcceptanceRabin;
import odd.ODDUtils;
import jdd.*;
@ -271,7 +272,7 @@ public class NondetModelChecker extends NonProbModelChecker
MultiObjModelChecker mcMo;
LTLModelChecker mcLtl;
Expression[] ltl;
DRA<BitSet>[] dra;
DA<BitSet,AcceptanceRabin>[] dra;
// State index info
// Misc
boolean negateresult = false;
@ -320,7 +321,7 @@ public class NondetModelChecker extends NonProbModelChecker
// Create arrays to store LTL/DRA info
ltl = new Expression[numObjectives];
dra = new DRA[numObjectives];
dra = new DA[numObjectives];
draDDRowVars = new JDDVars[numObjectives];
draDDColVars = new JDDVars[numObjectives];
@ -380,14 +381,14 @@ public class NondetModelChecker extends NonProbModelChecker
if (opsAndBounds.isProbabilityObjective(i)) {
ArrayList<JDDNode> statesH = new ArrayList<JDDNode>();
ArrayList<JDDNode> statesL = new ArrayList<JDDNode>();
for (int k = 0; k < dra[i].getNumAcceptancePairs(); k++) {
for (int k = 0; k < dra[i].getAcceptance().size(); k++) {
JDDNode tmpH = JDD.Constant(0);
JDDNode tmpL = JDD.Constant(0);
for (int j = 0; j < dra[i].size(); j++) {
if (!dra[i].getAcceptanceL(k).get(j)) {
if (!dra[i].getAcceptance().get(k).getL().get(j)) {
tmpH = JDD.SetVectorElement(tmpH, draDDRowVars[i], j, 1.0);
}
if (dra[i].getAcceptanceK(k).get(j)) {
if (dra[i].getAcceptance().get(k).getK().get(j)) {
tmpL = JDD.SetVectorElement(tmpL, draDDRowVars[i], j, 1.0);
}
}
@ -943,7 +944,7 @@ public class NondetModelChecker extends NonProbModelChecker
StateValues probsProduct = null, probs = null;
Expression ltl;
Vector<JDDNode> labelDDs;
DRA<BitSet> dra;
DA<BitSet,AcceptanceRabin> dra;
NondetModel modelProduct;
NondetModelChecker mcProduct;
JDDNode startMask;
@ -978,7 +979,7 @@ public class NondetModelChecker extends NonProbModelChecker
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
// If required, export DRA

5
prism/src/prism/ProbModelChecker.java
View File

@ -34,6 +34,7 @@ import java.util.BitSet;
import java.util.List;
import java.util.Vector;
import acceptance.AcceptanceRabin;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
@ -492,7 +493,7 @@ public class ProbModelChecker extends NonProbModelChecker
StateValues probsProduct = null, probs = null;
Expression ltl;
Vector<JDDNode> labelDDs;
DRA<BitSet> dra;
DA<BitSet,AcceptanceRabin> dra;
ProbModel modelProduct;
ProbModelChecker mcProduct;
JDDNode startMask;
@ -516,7 +517,7 @@ public class ProbModelChecker extends NonProbModelChecker
mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs.");
mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");
// If required, export DRA

Write Preview
Loading…
Cancel
Save