jltl2dstar: support generation of Rabin and Streett automata. [Joachim Klein]

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

prism/src/jltl2dstar/DRA.java

@@ -26,7 +26,9 @@ import java.io.FileWriter;
 import java.io.PrintStream;
 import java.util.*;
 
+import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceStreett;
 import jltl2ba.APElement;
 import jltl2ba.APSet;
 import prism.PrismException;
@@ -144,28 +146,54 @@ public class DRA extends DA {
 	}
 
 	/**
-	 * Convert the DRA from jltl2dstar to PRISM data structures.  
+	 * Convert this jltl2dstar deterministic automaton to PRISM data structures.
 	 */
-	public prism.DA<BitSet,AcceptanceRabin> createPrismDRA() throws PrismException
+	public prism.DA<BitSet,? extends AcceptanceOmega> createPrismDA() throws PrismException
+	{
+		int numStates = size();
+		if (!isStreett()) {
+			// Rabin
+			prism.DA<BitSet, AcceptanceRabin> draNew;
+
+			draNew = new prism.DA<BitSet, AcceptanceRabin>(numStates);
+			createPrismDA(draNew);
+			AcceptanceRabin accNew = createRabinAcceptance();
+			draNew.setAcceptance(accNew);
+
+			return draNew;
+		} else {
+			// Streett
+			prism.DA<BitSet, AcceptanceStreett> dsaNew;
+
+			dsaNew = new prism.DA<BitSet, AcceptanceStreett>(numStates);
+			createPrismDA(dsaNew);
+			AcceptanceStreett accNew = createStreettAcceptance();
+			dsaNew.setAcceptance(accNew);
+
+			return dsaNew;
+		}
+	}
+
+	/**
+	 * Convert the state and transition structure of this jltl2dstar deterministic automaton
+	 * to the PRISM data structures.
+	 */
+	private void createPrismDA(prism.DA<BitSet, ?> da) throws PrismException
 	{
 		int i, k, numLabels, numStates, src, dest;
 		List<String> apList;
 		BitSet bitset;
-		RabinAcceptance acc;
-		prism.DA<BitSet,AcceptanceRabin> draNew;
-		AcceptanceRabin accNew = new AcceptanceRabin();
 		
 		numLabels = getAPSize();
 		numStates = size();
-		draNew = new prism.DA<BitSet,AcceptanceRabin>(numStates);
 		// Copy AP set
 		apList = new ArrayList<String>(numLabels);
 		for (i = 0; i < numLabels; i++) {
 			apList.add(getAPSet().getAP(i));
 		}
-		draNew.setAPList(apList);
+		da.setAPList(apList);
 		// Copy start state
-		draNew.setStartState(getStartState().getName());
+		da.setStartState(getStartState().getName());
 		// Copy edges
 		for (i = 0; i < numStates; i++) {
 			DA_State cur_state = get(i);
@@ -176,23 +204,51 @@ public class DRA extends DA {
 				for (k = 0; k < numLabels; k++) {
 					bitset.set(k, transition.getKey().get(k));
 				}
-				draNew.addEdge(src, bitset, dest);
+				da.addEdge(src, bitset, dest);
 			}
 		}
+	}
+
+	/**
+	 * Create an AcceptanceRabin acceptance condition from the acceptance condition
+	 * of this jltl2dstar deterministic automaton.
+	 */
+	private AcceptanceRabin createRabinAcceptance() throws PrismException {
+		AcceptanceRabin accNew = new AcceptanceRabin();
+
 		// Copy acceptance pairs
-		acc = acceptance(); 
-		for (i = 0; i < acc.size(); i++) {
+		RabinAcceptance acc = acceptance();
+		for (int i = 0; i < acc.size(); i++) {
 			// Note: Pairs (U_i,L_i) become (L_i,K_i) in PRISM's notation
 			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);
 		}
+		return accNew;
+	}
+
+	/**
+	 * Create an AcceptanceStreett acceptance condition from the acceptance condition
+	 * of this jltl2dstar deterministic automaton.
+	 */
+	private AcceptanceStreett createStreettAcceptance() throws PrismException {
+		AcceptanceStreett accNew = new AcceptanceStreett();
 		
-		draNew.setAcceptance(accNew);
+		// Copy acceptance pairs, interpreting the RabinAcceptance from this automaton
+		// as Streett acceptance
+		RabinAcceptance acc = acceptance();
+		for (int i = 0; i < acc.size(); i++) {
+			// Note: Pairs (U_i,L_i) become (G_i,R_i) in PRISM's notation
+			BitSet newR = (BitSet)acc.getAcceptance_L(i).clone();
+			BitSet newG = (BitSet)acc.getAcceptance_U(i).clone();
+			AcceptanceStreett.StreettPair pair = new AcceptanceStreett.StreettPair(newR, newG);
 
-		return draNew;
+			accNew.add(pair);
+		}
+		return accNew;
 	}
+
 	
 	//	public DRA calculateUnionStuttered(DRA other,
 	//			StutterSensitivenessInformation stutter_information,

prism/src/jltl2dstar/LTL2Rabin.java

@@ -27,16 +27,46 @@ import prism.PrismException;
 
 import java.util.BitSet;
 
+import prism.DA;
+import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceStreett;
+import acceptance.AcceptanceType;
 
 public class LTL2Rabin {
+
+	@SuppressWarnings("unchecked")
+	public static prism.DA<BitSet,AcceptanceRabin> ltl2rabin(SimpleLTL ltlFormula) throws PrismException
+	{
+		DA<BitSet, ? extends AcceptanceOmega> result;
+		result = ltl2da(ltlFormula, AcceptanceType.RABIN);
+		return (DA<BitSet, AcceptanceRabin>)result;
+	}
+
+	@SuppressWarnings("unchecked")
+	public static prism.DA<BitSet, AcceptanceStreett> ltl2streett(SimpleLTL ltlFormula) throws PrismException
+	{
+		DA<BitSet, ? extends AcceptanceOmega> result;
+		result = ltl2da(ltlFormula, AcceptanceType.STREETT);
+		return (DA<BitSet, AcceptanceStreett>)result;
+	}
 	
-	public static prism.DA<BitSet,AcceptanceRabin> ltl2rabin(SimpleLTL ltlFormula) throws PrismException {
+	public static prism.DA<BitSet, ? extends AcceptanceOmega> ltl2da(SimpleLTL ltlFormula, AcceptanceType... allowedAcceptance) throws PrismException
+	{
 		SimpleLTL ltl = ltlFormula.simplify();
-		return ltl2rabin(ltl, ltl.getAPs()).createPrismDRA();
+
+		boolean allowRabin=AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN);
+		boolean allowStreett=AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT);
+
+		if (allowRabin && allowStreett) {
+			// currently, disable opportunistic generation of either Rabin or Streett automaton
+			allowStreett = false;
+		}
+
+		return ltl2da(ltl, ltl.getAPs(), allowRabin, allowStreett).createPrismDA();
 	}
-	
-	private static DRA ltl2rabin(SimpleLTL ltl, APSet apset) throws PrismException {
+
+	private static DRA ltl2da(SimpleLTL ltl, APSet apset, boolean allowRabin, boolean allowStreett) throws PrismException {
 		DRA dra = null;
 		Options_LTL2DRA opt_ltl2rabin = new Options_LTL2DRA();
 		
@@ -57,7 +87,16 @@ public class LTL2Rabin {
 		// opt_ltl2dstar.scheck_path="";
 		// stuttercheck_timekeep = true;
 		// stuttercheck_print = false;
-		opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.RABIN;
+		if (allowRabin) {
+			if (allowStreett)
+				opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.RABIN_AND_STREETT;
+			else
+				opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.RABIN;
+		} else if (allowStreett) {
+			opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.STREETT;
+		} else {
+			throw new PrismException("Can not generate deterministic automata if neither Rabin nor Streett is allowed.");
+		}
 		opt_ltl2rabin.detailed_states = false;
 		opt_ltl2rabin.verbose_scheduler = false;
 		opt_ltl2rabin.opt_safra.opt_accloop = true;