Refactor LTL-to-deterministic automaton generation, introduce LTL2DA and use LTL2RabinLibrary only for hard-coded and specially crafted DRA. [Joachim Klein]

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

prism/src/explicit/LTLModelChecker.java

@@ -41,7 +41,6 @@ import java.util.Vector;
 import acceptance.AcceptanceRabin;
 import common.IterableStateSet;
 import parser.State;
-import parser.Values;
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionLabel;
@@ -50,7 +49,7 @@ import parser.ast.ExpressionUnaryOp;
 import parser.type.TypeBool;
 import parser.type.TypePathBool;
 import prism.DA;
-import prism.LTL2RabinLibrary;
+import prism.LTL2DA;
 import prism.ModelType;
 import prism.PrismComponent;
 import prism.PrismException;
@@ -103,18 +102,6 @@ public class LTLModelChecker extends PrismComponent
 		super(parent);
 	}
 
-	/**
-	 * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
-	 * in which atomic propositions are represented by ExpressionLabel objects.
-	 * @param ltl the LTL formula
-	 * @param constantValues values for constants in the formula
-	 */
-	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constantValues) throws PrismException
-	{
-		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl, constantValues);
-	}
-	
-	
 	/**
 	 * Returns {@code true} if expression {@code expr} is a formula that can be handled by
 	 * LTLModelChecker for the given ModelType.
@@ -234,7 +221,8 @@ public class LTLModelChecker extends PrismComponent
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		time = System.currentTimeMillis();
-		dra = convertLTLFormulaToDRA(ltl, mc.getConstantValues());
+		LTL2DA ltl2da = new LTL2DA(this);
+		dra = ltl2da.convertLTLFormulaToDRA(ltl, mc.getConstantValues());
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
 		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
@@ -422,7 +410,8 @@ public class LTLModelChecker extends PrismComponent
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		time = System.currentTimeMillis();
-		dra = convertLTLFormulaToDRA(ltl, mc.getConstantValues());
+		LTL2DA ltl2da = new LTL2DA(this);
+		dra = ltl2da.convertLTLFormulaToDRA(ltl, mc.getConstantValues());
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
 		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");

prism/src/prism/LTL2DA.java

@@ -0,0 +1,98 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package prism;
+
+import java.util.BitSet;
+
+import acceptance.AcceptanceOmega;
+import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceType;
+import jltl2dstar.LTL2Rabin;
+import parser.Values;
+import parser.ast.Expression;
+
+/**
+ * Infrastructure for constructing deterministic automata for LTL formulas.
+ */
+public class LTL2DA extends PrismComponent
+{
+
+	public LTL2DA(PrismComponent parent) throws PrismException {
+		super(parent);
+	}
+
+	/**
+	 * Convert an LTL formula into a deterministic Rabin automaton.
+	 * The LTL formula is represented as a PRISM Expression,
+	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the formula
+	 * @param constantValues the values of constants, may be {@code null}
+	 */
+	@SuppressWarnings("unchecked")
+	public DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constantValues) throws PrismException
+	{
+		return (DA<BitSet, AcceptanceRabin>) convertLTLFormulaToDA(ltl, constantValues, AcceptanceType.RABIN);
+	}
+
+	/**
+	 * Convert an LTL formula into a deterministic automaton.
+	 * The LTL formula is represented as a PRISM Expression,
+	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the formula
+	 * @param constantValues the values of constants, may be {@code null}
+	 * @param allowedAcceptance the AcceptanceTypes that are allowed to be returned
+	 */
+	public DA<BitSet,? extends AcceptanceOmega> convertLTLFormulaToDA(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException
+	{
+		DA<BitSet, ? extends AcceptanceOmega> result = null;
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			// If we may construct a Rabin automaton, check the library first
+			try {
+				result = LTL2RabinLibrary.getDRAforLTL(ltl, constants);
+				if (result != null) {
+					getLog().println("Taking deterministic Rabin automaton from library...");
+				}
+			} catch (Exception e) {
+				getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
+				getLog().println(" "+e.getMessage());
+			}
+		}
+
+		// TODO (JK): support generation of DSA for simple path formula with time bound
+		if (result == null && !Expression.containsTemporalTimeBounds(ltl)) {
+			// use jltl2dstar LTL2DA
+			result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+		}
+
+		if (result == null) {
+			throw new PrismException("Could not convert LTL formula to deterministic automaton");
+		}
+
+		return result;
+	}
+}

prism/src/prism/LTL2RabinLibrary.java

@@ -32,14 +32,17 @@ import java.util.*;
 
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceRabin.RabinPair;
-import jltl2dstar.*;
 import parser.Values;
 import parser.ast.*;
 import parser.visitor.ASTTraverse;
 import parser.visitor.ASTTraverseModify;
 
 /**
- * LTL-to-DRA conversion.
+ * LTL-to-DRA conversion via
+ * <ol>
+ *  <li> hard-coded DRA for special formulas </li>
+ *  <li> direct translation into DRA for simple path formulas with temporal bounds</li>
+ * </ol>
  */
 public class LTL2RabinLibrary
 {
@@ -66,13 +69,19 @@ public class LTL2RabinLibrary
 	}
 
 	/**
-	 * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression,
+	 * Attempts to convert an LTL formula into a DRA by direct translation methods of the library:
+	 * <ul>
+	 * <li>First, look up hard-coded DRA from the DRA map.</li>
+	 * <li>Second, if the formula is a simple path formula with temporal bounds, use the special
+	 *     constructions {@code constructDRAFor....}
+	 * </ul>
+	 * 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,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException
-	{
+	public static DA<BitSet, AcceptanceRabin> getDRAforLTL(Expression ltl, Values constants) throws PrismException {
 		// Get list of labels appearing
 		labels = new ArrayList<String>();
 		ltl.accept(new ASTTraverse()
@@ -118,12 +127,12 @@ public class LTL2RabinLibrary
 			    ((ExpressionTemporal)ltl).getOperator() == ExpressionTemporal.P_U) {
 				return constructDRAForSimpleUntilFormula((ExpressionTemporal)ltl, constants, negated);				
 			} else {
-				throw new PrismException("Unsupported LTL formula: "+ltl);
+				throw new PrismException("Unsupported LTL formula with time bounds: "+ltl);
 			}
 		}
 		
-		// No time-bounded operators, convert using jltl2dstar library
-		return LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba());
+		// No time-bounded operators, do not convert using the library
+		return null;
 	}
 	
 	/**
@@ -588,7 +597,10 @@ public class LTL2RabinLibrary
 			System.out.println(ltl.equals(expr.toString()));
 			DA<BitSet,AcceptanceRabin> dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba());
 			System.out.println(dra1);
-			DA<BitSet,AcceptanceRabin> dra2 = convertLTLFormulaToDRA(expr, null);
+			DA<BitSet,AcceptanceRabin> dra2 = getDRAforLTL(expr, null);
+			if (dra2 == null) {
+			    dra2 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba());
+			}
 			System.out.println(dra2);
 			System.out.println(dra1.toString().equals(dra2.toString()));
 			//dra2.printDot(new PrintStream(new File("dra")));

prism/src/prism/LTLModelChecker.java

@@ -36,7 +36,6 @@ import acceptance.AcceptanceRabin;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
-import parser.Values;
 import parser.VarList;
 import parser.ast.Declaration;
 import parser.ast.DeclarationInt;
@@ -84,17 +83,6 @@ public class LTLModelChecker extends PrismComponent
 		return true;
 	}
 
-	/**
-	 * Convert an LTL formula into a DRA. 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, may be {@code null}
-	 */
-	public static DA<BitSet,AcceptanceRabin> convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException
-	{
-		return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl, constants);
-	}
-
 	/**
 	 * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and
 	 * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result

prism/src/prism/MultiObjModelChecker.java

@@ -82,7 +82,8 @@ public class MultiObjModelChecker extends PrismComponent
 			ltl = Expression.Not(Expression.Parenth(ltl));
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		long l = System.currentTimeMillis();
-		dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues());
+		LTL2DA ltl2da = new LTL2DA(prism);
+		dra[i] = ltl2da.convertLTLFormulaToDRA(ltl, modelChecker.getConstantValues());
 		mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");

prism/src/prism/NondetModelChecker.java

@@ -999,7 +999,8 @@ public class NondetModelChecker extends NonProbModelChecker
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
-		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl, constantValues);
+		LTL2DA ltl2da = new LTL2DA(prism);
+		dra = ltl2da.convertLTLFormulaToDRA(ltl, constantValues);
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");

prism/src/prism/ProbModelChecker.java

@@ -535,7 +535,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		// Convert LTL formula to deterministic Rabin automaton (DRA)
 		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
 		l = System.currentTimeMillis();
-		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl, constantValues);
+		LTL2DA ltl2da = new LTL2DA(prism);
+		dra = ltl2da.convertLTLFormulaToDRA(ltl, constantValues);
 		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds.");