Add LTL2RabinLibrary.getDAforLTL, now supports generation of DA with Streett and generic acceptance from the library

In particular, we can now construct DSA or generic DA for simple path formulas with bounds.


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

prism/src/automata/LTL2DA.java

@@ -97,12 +97,12 @@ public class LTL2DA extends PrismComponent
 			useExternal = false;
 		}
 
-		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN) && !useExternal) {
-			// If we may construct a Rabin automaton, check the library first
+		if (!useExternal) {
 			try {
-				result = LTL2RabinLibrary.getDRAforLTL(ltl, constants);
+				// checking the library first
+				result = LTL2RabinLibrary.getDAforLTL(ltl, constants, allowedAcceptance);
 				if (result != null) {
-					getLog().println("Taking deterministic Rabin automaton from library...");
+					getLog().println("Taking "+result.getAutomataType()+" from library...");
 				}
 			} catch (Exception e) {
 				if (containsTemporalBounds) {
@@ -118,13 +118,16 @@ public class LTL2DA extends PrismComponent
 			}
 		}
 
-		// TODO (JK): support generation of DSA for simple path formula with time bound
-		if (result == null && !containsTemporalBounds) {
-			if (useExternal) {
-				result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
+		if (result == null) {
+			if (!containsTemporalBounds) {
+				if (useExternal) {
+					result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
+				} else {
+					// use jltl2dstar LTL2DA
+					result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+				}
 			} else {
-				// use jltl2dstar LTL2DA
-				result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+				throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton, formula had time-bounds");
 			}
 		}
 

prism/src/automata/LTL2RabinLibrary.java

@@ -30,8 +30,10 @@ package automata;
 import java.io.*;
 import java.util.*;
 
+import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceRabin.RabinPair;
+import acceptance.AcceptanceType;
 import parser.Values;
 import parser.ast.*;
 import parser.visitor.ASTTraverse;
@@ -73,6 +75,45 @@ public class LTL2RabinLibrary
 		//dras.put("!((G \"L0\")&(G F \"L1\"))", "4 states (start 3), 2 labels: 0-{1}->1 0-{0, 1}->3 0-{}->1 0-{0}->0 1-{1}->1 1-{0, 1}->1 1-{}->1 1-{0}->1 2-{1}->1 2-{0, 1}->3 2-{}->1 2-{0}->0 3-{1}->1 3-{0, 1}->3 3-{}->1 3-{0}->2; 2 acceptance pairs: ({},{1}) ({1, 2, 3},{0})"); 
 	}
 
+	/**
+	 * Attempts to convert an LTL formula into a deterministic omega-automaton (with
+	 * one of the allowed acceptance conditions) by direct translation methods of the library:
+	 *
+	 * Relies on getDRAForLTL, with appropriate pre/post-processing for acceptance types
+	 * that are not Rabin.
+	 *
+	 * Return {@code null} if the automaton can not be constructed using the library.
+	 * <br> The LTL formula is represented as a PRISM Expression,
+	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the LTL formula
+	 * @param constants values for constants in the formula (may be {@code null})
+	 */
+	public static DA<BitSet, ? extends AcceptanceOmega> getDAforLTL(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException {
+		// first try Rabin ...
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return getDRAforLTL(ltl, constants);
+		}
+
+		// ..., then Streett (via negation and complementation at the acceptance level)
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			Expression negatedLtl = Expression.Not(ltl);
+			DA<BitSet, AcceptanceRabin> da = getDRAforLTL(negatedLtl, constants);
+			if (da != null) {
+				DA.switchAcceptance(da, da.getAcceptance().complementToStreett());
+				return da;
+			}
+		}
+
+		// ..., and then generic acceptance
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			DA<BitSet, AcceptanceRabin> da = getDRAforLTL(ltl, constants);
+			DA.switchAcceptance(da, da.getAcceptance().toAcceptanceGeneric());
+			return da;
+		}
+
+		return null;
+	}
+
 	/**
 	 * Attempts to convert an LTL formula into a DRA by direct translation methods of the library:
 	 * <ul>