From ac63f5b0ef5ba5bd060f7d5affadf291a3d91b91 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Feb 2016 14:42:27 +0000
Subject: [PATCH] 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           | 23 +++++++------
 prism/src/automata/LTL2RabinLibrary.java | 41 ++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 10 deletions(-)

diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java
index e19811da..e06882fe 100644
--- a/prism/src/automata/LTL2DA.java
+++ b/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");
 			}
 		}
 
diff --git a/prism/src/automata/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java
index c8f30ad8..4173888c 100644
--- a/prism/src/automata/LTL2RabinLibrary.java
+++ b/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>