LTLModelCheckers: constructDFAForCosafetyRewardLTL

This method constructs a DFA for a co-safe LTL formula
with appropriate semantics for co-safe LTL reward computations.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12064 bbc10eb1-c90d-0410-af57-cb519fbb1720

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.
+	 * <br>
+	 * 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.
+	 * <br>
+	 * 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<BitSet, AcceptanceReach> constructDFAForCosafetyRewardLTL(StateModelChecker mc, Model model, Expression expr, Vector<BitSet> 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<BitSet, AcceptanceReach> 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.

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.
+	 * <br>
+	 * 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.
+	 * <br>
+	 * 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<BitSet, AcceptanceReach> constructDFAForCosafetyRewardLTL(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> 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<BitSet, AcceptanceReach> 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