diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java
index 94833c9c..13122255 100644
--- a/prism/src/explicit/LTLModelChecker.java
+++ b/prism/src/explicit/LTLModelChecker.java
@@ -60,10 +60,13 @@ import acceptance.AcceptanceBuchi;
import acceptance.AcceptanceGenRabin;
import acceptance.AcceptanceOmega;
import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceReach;
import acceptance.AcceptanceStreett;
import acceptance.AcceptanceType;
import automata.DA;
import automata.LTL2DA;
+import automata.LTL2WDBA;
+import jltl2ba.SimpleLTL;
import common.IterableStateSet;
import common.StopWatch;
@@ -255,7 +258,56 @@ public class LTLModelChecker extends PrismComponent
return da;
}
-
+
+ /**
+ * Constructs a deterministic finite automaton (DFA) for the given syntactically co-safe
+ * LTL formula, for use in reward computations for co-safe LTL.
+ *
+ * First, extracted maximal state formulas are model checked with the passed in model checker.
+ * The maximal state formulas are assigned labels (L0, L1, etc.) which become the atomic
+ * propositions in the resulting DA. BitSets giving the states which satisfy each label
+ * are put into the vector {@code labelBS}, which should be empty when this function is called.
+ *
+ * To achieve "strong" semantics for the next-step operator, an additional atomic
+ * proposition is added and X phi is transformed to X (phi & fresh_ap). This
+ * ensures that, e.g., X X true results in two steps of accumulation.
+ * @param mc the underlying model checker (for recursively handling maximal state formulas)
+ * @param model the model
+ * @param expr the co-safe LTL formula
+ * @param labelBS empty vector to be filled with BitSets for subformulas
+ * @return a DA with AcceptanceReach acceptance condition
+ */
+ public DA constructDFAForCosafetyRewardLTL(StateModelChecker mc, Model model, Expression expr, Vector labelBS) throws PrismException
+ {
+ // Model check maximal state formulas
+ Expression ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS);
+
+ SimpleLTL sltl = ltl.convertForJltl2ba();
+ // convert to positive normal form (negation only in front of APs)
+ sltl = sltl.toBasicOperators();
+ sltl = sltl.pushNegation();
+ if (sltl.hasNextStep()) {
+ // we have do add another atomic proposition to ensure "strong" semantics for
+ // the X operator
+ String stepLabel = "L" + labelBS.size();
+ BitSet allStates = new BitSet();
+ allStates.set(0, model.getNumStates(), true);
+ labelBS.add(allStates);
+ sltl = sltl.extendNextStepWithAP(stepLabel);
+ // mainLog.println("Adding step label " + stepLabel);
+ }
+
+ // Convert LTL formula to deterministic automaton, with Reach acceptance
+ LTL2WDBA ltl2wdba = new LTL2WDBA(this);
+ mainLog.println("\nBuilding deterministic finite automaton via LTL2WDBA construction (for " + sltl + ")...");
+ StopWatch timer = new StopWatch(getLog());
+ timer.start("constructing DFA");
+ DA dfa = ltl2wdba.cosafeltl2dfa(sltl);
+ timer.stop("DFA has " + dfa.size() + " states");
+
+ return dfa;
+ }
+
/**
* Generate a deterministic automaton for the given LTL formula
* and construct the product of this automaton with a Markov chain.
diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 01d5e8e9..fffcc145 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -39,13 +39,16 @@ import acceptance.AcceptanceOmega;
import acceptance.AcceptanceOmegaDD;
import acceptance.AcceptanceRabin;
import acceptance.AcceptanceRabinDD;
+import acceptance.AcceptanceReach;
import acceptance.AcceptanceType;
import automata.DA;
import automata.LTL2DA;
+import automata.LTL2WDBA;
import common.StopWatch;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
+import jltl2ba.SimpleLTL;
import parser.VarList;
import parser.ast.Declaration;
import parser.ast.DeclarationInt;
@@ -247,6 +250,52 @@ public class LTLModelChecker extends PrismComponent
return expr;
}
+ /**
+ * Constructs a deterministic finite automaton (DFA) for the given syntactically co-safe
+ * LTL formula, for use in reward computations for co-safe LTL.
+ *
+ * First, extracted maximal state formulas are model checked with the passed in model checker.
+ * The maximal state formulas are assigned labels (L0, L1, etc.) which become the atomic
+ * propositions in the resulting DA. DDNodes giving the states which satisfy each label
+ * are put into the vector {@code labelDDs}, which should be empty when this function is called.
+ *
+ * To achieve "strong" semantics for the next-step operator, an additional atomic
+ * proposition is added and X phi is transformed to X (phi & fresh_ap). This
+ * ensures that, e.g., X X true results in two steps of accumulation.
+ * @param mc the underlying model checker (for recursively handling maximal state formulas)
+ * @param model the model
+ * @param expr the co-safe LTL formula
+ * @param labelDDs empty vector to be filled with JDDNodes for subformulas
+ * @return a DA with AcceptanceReach acceptance condition
+ */
+ public DA constructDFAForCosafetyRewardLTL(ModelChecker mc, Model model, Expression expr, Vector labelDDs) throws PrismException
+ {
+ // Model check maximal state formulas
+ Expression ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelDDs);
+
+ SimpleLTL sltl = ltl.convertForJltl2ba();
+ // convert to positive normal form (negation only in front of APs)
+ sltl = sltl.toBasicOperators();
+ sltl = sltl.pushNegation();
+ if (sltl.hasNextStep()) {
+ // we have do add another atomic proposition
+ String stepLabel = "L" + labelDDs.size();
+ labelDDs.add(model.getReach().copy());
+ sltl = sltl.extendNextStepWithAP(stepLabel);
+ // mainLog.println("Adding step label " + stepLabel);
+ }
+
+ // Convert LTL formula to deterministic automaton, with Reach acceptance
+ LTL2WDBA ltl2wdba = new LTL2WDBA(this);
+ mainLog.println("\nBuilding deterministic finite automaton via LTL2WDBA construction (for " + sltl + ")...");
+ StopWatch timer = new StopWatch(getLog());
+ timer.start("constructing DFA");
+ DA dfa = ltl2wdba.cosafeltl2dfa(sltl);
+ timer.stop("DFA has " + dfa.size() + " states");
+
+ return dfa;
+ }
+
/**
* Construct a deterministic automaton (DA) for an LTL formula, having first extracted maximal state formulas
* and model checked them with the passed in model checker. The maximal state formulas are assigned labels