From c00ffea7d8d5e7498df4e7e14f73d3c60f4a914c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 28 Jan 2015 14:59:15 +0000 Subject: [PATCH] Refactor: switch from prism.DRA to prism.DA. 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 --- prism/src/explicit/DTMCModelChecker.java | 7 ++-- prism/src/explicit/LTLModelChecker.java | 26 ++++++------ prism/src/explicit/MDPModelChecker.java | 7 ++-- prism/src/jltl2dstar/DRA.java | 22 +++++----- prism/src/jltl2dstar/LTL2Rabin.java | 4 +- prism/src/prism/LTL2RabinLibrary.java | 29 ++++++++----- prism/src/prism/LTLModelChecker.java | 51 ++++++++++++----------- prism/src/prism/MultiObjModelChecker.java | 30 +++++++------ prism/src/prism/NondetModelChecker.java | 15 +++---- prism/src/prism/ProbModelChecker.java | 5 ++- 10 files changed, 105 insertions(+), 91 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index ed04b719..793205a1 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -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 dra; + DA 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 diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 339f571d..20b3745c 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -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 convertLTLFormulaToDRA(Expression ltl) throws PrismException + public static DA 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 constructProductMC(DRA dra, DTMC dtmc, Vector labelBS, BitSet statesOfInterest) throws PrismException + public Pair constructProductMC(DA dra, DTMC dtmc, Vector 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 constructProductMDP(DRA dra, MDP mdp, Vector labelBS, BitSet statesOfInterest) throws PrismException + public Pair constructProductMDP(DA dra, MDP mdp, Vector 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 dra, Model model, int invMap[]) throws PrismException + public BitSet findAcceptingBSCCsForRabin(DA 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 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 dra, NondetModel model, int invMap[]) throws PrismException + public BitSet findAcceptingECStatesForRabin(DA 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 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)) { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 1d2a0518..2d4f2343 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -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 dra; + DA 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 diff --git a/prism/src/jltl2dstar/DRA.java b/prism/src/jltl2dstar/DRA.java index 371711f6..bde3b3a8 100644 --- a/prism/src/jltl2dstar/DRA.java +++ b/prism/src/jltl2dstar/DRA.java @@ -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 createPrismDRA() throws PrismException + public prism.DA createPrismDRA() throws PrismException { int i, k, numLabels, numStates, src, dest; List apList; - BitSet bitset, bitset2; + BitSet bitset; RabinAcceptance acc; - prism.DRA draNew; + prism.DA draNew; + AcceptanceRabin accNew = new AcceptanceRabin(); numLabels = getAPSize(); numStates = size(); - draNew = new prism.DRA(numStates); + draNew = new prism.DA(numStates); // Copy AP set apList = new ArrayList(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; } diff --git a/prism/src/jltl2dstar/LTL2Rabin.java b/prism/src/jltl2dstar/LTL2Rabin.java index a2babc38..131bc0d2 100644 --- a/prism/src/jltl2dstar/LTL2Rabin.java +++ b/prism/src/jltl2dstar/LTL2Rabin.java @@ -27,9 +27,11 @@ import prism.PrismException; import java.util.BitSet; +import acceptance.AcceptanceRabin; + public class LTL2Rabin { - public static prism.DRA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { + public static prism.DA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { SimpleLTL ltl = ltlFormula.simplify(); return ltl2rabin(ltl, ltl.getAPs()).createPrismDRA(); } diff --git a/prism/src/prism/LTL2RabinLibrary.java b/prism/src/prism/LTL2RabinLibrary.java index 8739f013..8064fbe9 100644 --- a/prism/src/prism/LTL2RabinLibrary.java +++ b/prism/src/prism/LTL2RabinLibrary.java @@ -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 convertLTLFormulaToDRA(Expression ltl) throws PrismException + public static DA convertLTLFormulaToDRA(Expression ltl) throws PrismException { // Get list of labels appearing labels = new ArrayList(); @@ -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 createDRAFromString(String s, List labels) throws PrismException + private static DA createDRAFromString(String s, List labels) throws PrismException { int ptr = 0, i, j, k, n, from, to; String bs; - prism.DRA draNew; + DA 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(n); + draNew = new DA(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 draForNotFaCb(String l0, String l1) throws PrismException + public static DA draForNotFaCb(String l0, String l1) throws PrismException { int numStates; List apList; - prism.DRA draNew; + DA 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(numStates); + draNew = new DA(numStates); + draNew.setAcceptance(new AcceptanceRabin()); // AP set apList = new ArrayList(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 dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba()); + DA dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba()); System.out.println(dra1); - DRA dra2 = convertLTLFormulaToDRA(expr); + DA dra2 = convertLTLFormulaToDRA(expr); System.out.println(dra2); System.out.println(dra1.toString().equals(dra2.toString())); //dra2.printDot(new PrintStream(new File("dra"))); diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index a2189d20..7a84c324 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -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 convertLTLFormulaToDRA(Expression ltl) throws PrismException + public static DA 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 dra, ProbModel model, Vector labelDDs) throws PrismException + public ProbModel constructProductMC(DA dra, ProbModel model, Vector 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 dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) + public ProbModel constructProductMC(DA dra, ProbModel model, Vector 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 dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, + public ProbModel constructProductMC(DA dra, ProbModel model, Vector 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 dra, NondetModel model, Vector labelDDs) throws PrismException + public NondetModel constructProductMDP(DA dra, NondetModel model, Vector 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 dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy) + public NondetModel constructProductMDP(DA dra, NondetModel model, Vector 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 dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, + public NondetModel constructProductMDP(DA dra, NondetModel model, Vector 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 dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, + public JDDNode buildTransMask(DA dra, Vector 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 dra, Vector labelDDs, JDDVars draDDRowVars) + public JDDNode buildStartMask(DA dra, Vector 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 dra, int i, boolean complement) + public JDDNode buildLStatesForRabinPair(JDDVars draDDRowVars, DA 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 dra, int i) + public JDDNode buildKStatesForRabinPair(JDDVars draDDRowVars, DA 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 dra, ProbModel model, JDDVars draDDRowVars, JDDVars draDDColVars) throws PrismException + public JDDNode findAcceptingBSCCsForRabin(DA dra, ProbModel model, JDDVars draDDRowVars, JDDVars draDDColVars) throws PrismException { JDDNode allAcceptingStates; List vectBSCCs; @@ -688,7 +689,7 @@ public class LTLModelChecker extends PrismComponent // Build BDDs for !L_i and K_i ArrayList statesL_not = new ArrayList(); ArrayList statesK = new ArrayList(); - 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 dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) + public JDDNode findAcceptingECStatesForRabin(DA 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 statesLnot = new ArrayList(); ArrayList statesK = new ArrayList(); - 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 dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness, + public JDDNode findMultiAcceptingStates(DA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness, List allecs, List statesH, List 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[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List targetDDs, + public void findMultiConflictAcceptingStates(DA[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List targetDDs, List> allstatesH, List> allstatesL, List combinations, List> combinationIDs) throws PrismException { @@ -961,7 +962,7 @@ public class LTLModelChecker extends PrismComponent } } - private void computeCombinations(DRA[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List targetDDs, + private void computeCombinations(DA[] dra, NondetModel model, JDDVars[] draDDRowVars, JDDVars[] draDDColVars, List targetDDs, List> allstatesH, List> allstatesL, List queue, int sp) throws PrismException { queueElement e = queue.get(sp); diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 64cd02c6..7177ea62 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -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 dra[], Operator operator, + protected NondetModel constructDRAandProductMulti(NondetModel model, LTLModelChecker mcLtl, ModelChecker modelChecker, Expression ltl, int i, DA 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 dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars, + protected JDDNode computeAcceptingEndComponent(DA dra, NondetModel modelProduct, JDDVars draDDRowVars, JDDVars draDDColVars, List allecs, List statesH, List 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 rewardsIndex, OpsAndBoundsList opsAndBounds, - int numTargets, DRA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException + int numTargets, DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[]) throws PrismException { List mecs = mcLtl.findMECStates(modelProduct, modelProduct.getReach()); JDDNode removedActions = JDD.Constant(0); @@ -230,7 +228,7 @@ public class MultiObjModelChecker extends PrismComponent Vector tmptargetDDs = new Vector(); List tmpmultitargetDDs = new ArrayList(); List tmpmultitargetIDs = new ArrayList(); - ArrayList> tmpdra = new ArrayList>(); + ArrayList> tmpdra = new ArrayList>(); ArrayList tmpdraDDRowVars = new ArrayList(); ArrayList tmpdraDDColVars = new ArrayList(); 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 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 dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, + OpsAndBoundsList opsAndBounds, DA dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List> allstatesH, List> allstatesL, List multitargetDDs, List multitargetIDs) throws PrismException { - DRA[] tmpdra = new DRA[conflictformulae]; + DA[] tmpdra = new DA[conflictformulae]; JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; List tmptargetDDs = new ArrayList(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 dra[], JDDVars draDDRowVars[], JDDVars draDDColVars[], List targetDDs, List multitargetDDs, List multitargetIDs) throws PrismException { @@ -366,14 +364,14 @@ public class MultiObjModelChecker extends PrismComponent if (!reachExpr[i]) { ArrayList statesH = new ArrayList(); ArrayList statesL = new ArrayList(); - 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[] tmpdra = new DA[conflictformulae]; JDDVars[] tmpdraDDRowVars = new JDDVars[conflictformulae]; JDDVars[] tmpdraDDColVars = new JDDVars[conflictformulae]; List tmptargetDDs = new ArrayList(conflictformulae); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f356b1b4..4152916c 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -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[] dra; + DA[] 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 statesH = new ArrayList(); ArrayList statesL = new ArrayList(); - 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 labelDDs; - DRA dra; + DA 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 diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index a001fc53..34f6c1ae 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -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 labelDDs; - DRA dra; + DA 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