(HOA path) Add support in LTLModelCheckers (ex/sym) to support HOA path specifications

Additionally, protect multi-objective model checking and checkRewardCoSafeLTL against HOA path specifications.
Later on, we can add handling for that.

prism/src/explicit/LTLModelChecker.java

@@ -55,6 +55,7 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismNotSupportedException;
+import prism.PrismPaths;
 import prism.PrismUtils;
 import acceptance.AcceptanceBuchi;
 import acceptance.AcceptanceGenRabin;
@@ -129,6 +130,7 @@ public class LTLModelChecker extends PrismComponent
 		if (!expr.isPathFormula(true)) {
 			return false;
 		}
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (modelType.continuousTime()) {
 				// Only support temporal bounds for discrete time models
@@ -140,6 +142,10 @@ public class LTLModelChecker extends PrismComponent
 				return false;
 			}
 		}
+
+		if (Expression.isHOA(expr))
+			return true;
+
 		return true;
 	}
 
@@ -236,14 +242,33 @@ public class LTLModelChecker extends PrismComponent
 			}
 		}
 
-		// Model check maximal state formulas
-		ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS);
+		if (Expression.isHOA(expr)) {
+			LTL2DA ltl2da = new LTL2DA(this);
+			time = System.currentTimeMillis();
+			mainLog.println("Parsing and constructing HOA automaton for "+expr);
+			PrismPaths paths = new PrismPaths(mc.getModulesFile(),
+			                                   mc.getPropertiesFile());
+			Vector<Expression> apExpressions = new Vector<Expression>();
+			da = ltl2da.fromExpressionHOA(expr, paths, apExpressions, allowedAcceptance);
+
+			mainLog.println("Determining states satisfying atomic proposition labels of the automaton...");
+			for (int i=0; i<da.getAPList().size(); i++) {
+				Expression apExpression = apExpressions.get(i);
+				apExpression.typeCheck();
+				BitSet labelStates = mc.checkExpression(model, apExpression, null).getBitSet();
+				labelBS.add(labelStates);
+				da.getAPList().set(i, "L"+i);
+			}
+		} else {
+			// Model check maximal state formulas
+			ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS);
 
-		// Convert LTL formula to deterministic automaton
-		mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
-		time = System.currentTimeMillis();
-		LTL2DA ltl2da = new LTL2DA(this);
-		da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
+			// Convert LTL formula to deterministic automaton
+			mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
+			time = System.currentTimeMillis();
+			LTL2DA ltl2da = new LTL2DA(this);
+			da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
+		}
 		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
 		da.checkForCanonicalAPs(labelBS.size());
 		time = System.currentTimeMillis() - time;

prism/src/parser/ast/Expression.java

@@ -991,6 +991,10 @@ public abstract class Expression extends ASTElement
 	 */
 	public static boolean isCoSafeLTLSyntactic(Expression expr, boolean convert)
 	{
+		if (Expression.isHOA(expr)) {
+			return false;
+		}
+
 		// Convert to or check for positive normal form
 		if (convert) {
 			expr = BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy());

prism/src/prism/LTLModelChecker.java

@@ -181,6 +181,11 @@ public class LTLModelChecker extends PrismComponent
 				return false;
 			}
 		}
+
+		if (Expression.isHOA(expr)) {
+			return true;
+		}
+
 		return true;
 	}
 
@@ -302,14 +307,14 @@ public class LTLModelChecker extends PrismComponent
 	 * (L0, L1, etc.) which become the atomic propositions in the resulting DA. JDDNodes giving the states which
 	 * satisfy each label are put into the vector {@code labelBS}, which should be empty when this function is called.
 	 *
-	 * @param mc a ModelChecker, used for checking maximal state formulas
+	 * @param mc a StateModelChecker, used for checking maximal state formulas
 	 * @param model the model
 	 * @param expr a path expression, i.e. the LTL formula
 	 * @param labelBS empty vector to be filled with JDDNodes for subformulas 
 	 * @param allowedAcceptance the allowed acceptance types
 	 * @return the DA
 	 */
-	public DA<BitSet,? extends AcceptanceOmega> constructDAForLTLFormula(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs, AcceptanceType... allowedAcceptance) throws PrismException
+	public DA<BitSet,? extends AcceptanceOmega> constructDAForLTLFormula(StateModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs, AcceptanceType... allowedAcceptance) throws PrismException
 	{
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
@@ -321,14 +326,36 @@ public class LTLModelChecker extends PrismComponent
 			}
 		}
 		
-		// Model check maximal state formulas
-		Expression ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelDDs);
+		long time;
+		DA<BitSet, ? extends AcceptanceOmega> da;
 
-		// Convert LTL formula to deterministic automaton (DA)
-		mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
-		long time  = System.currentTimeMillis();
-		LTL2DA ltl2da = new LTL2DA(this);
-		DA<BitSet, ? extends AcceptanceOmega> da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
+		if (Expression.isHOA(expr)) {
+			LTL2DA ltl2da = new LTL2DA(this);
+			time = System.currentTimeMillis();
+			mainLog.println("Parsing and constructing HOA automaton for "+expr);
+			PrismPaths paths = new PrismPaths(mc.getModulesFile(),
+			                                  mc.getPropertiesFile());
+			Vector<Expression> apExpressions = new Vector<Expression>();
+			da = ltl2da.fromExpressionHOA(expr, paths, apExpressions, allowedAcceptance);
+
+			mainLog.println("Determining states satisfying atomic proposition labels of the automaton...");
+			for (int i=0; i<da.getAPList().size(); i++) {
+				Expression apExpression = apExpressions.get(i);
+				apExpression.typeCheck();
+				JDDNode labelStates = mc.checkExpressionDD(apExpression, model.getReach().copy());
+				labelDDs.add(labelStates);
+				da.getAPList().set(i, "L"+i);
+			}
+		} else {
+			// Model check maximal state formulas
+			Expression ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelDDs);
+
+			// Convert LTL formula to deterministic automaton (DA)
+			mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
+			time  = System.currentTimeMillis();
+			LTL2DA ltl2da = new LTL2DA(this);
+			da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance);
+		}
 		da.checkForCanonicalAPs(labelDDs.size());
 		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
 		time = System.currentTimeMillis() - time;
@@ -344,7 +371,6 @@ public class LTLModelChecker extends PrismComponent
 		return da;
 	}
 
-
 	/**
 	 * Construct the product of a DA and a DTMC/CTMC, starting from a given set
 	 * of states of interest. The corresponding states in the product become

prism/src/prism/MultiObjModelChecker.java

@@ -74,6 +74,11 @@ public class MultiObjModelChecker extends PrismComponent
 	{
 
 		// TODO (JK): Adapt to support simple path formulas with bounds via DRA construction
+		// TODO (JK): Adapt to support HOA automata
+
+		if (Expression.isHOA(ltl)) {
+			throw new PrismNotSupportedException("Multi-objective model checking with HOA automata currently not supported");
+		}
 
 		// Model check maximal state formulas
 		Vector<JDDNode> labelDDs = new Vector<JDDNode>();

prism/src/prism/NondetModelChecker.java

@@ -1517,6 +1517,10 @@ public class NondetModelChecker extends NonProbModelChecker
 			throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
 		}
 
+		if (Expression.isHOA(expr)) {
+			throw new PrismNotSupportedException("Co-safety rewards with HOA automata not supported yet");
+		}
+
 		// For LTL model checking routines
 		mcLtl = new LTLModelChecker(prism);
 

prism/src/prism/ProbModelChecker.java

@@ -988,6 +988,10 @@ public class ProbModelChecker extends NonProbModelChecker
 			throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
 		}
 
+		if (Expression.isHOA(expr)) {
+			throw new PrismNotSupportedException("Co-safety rewards with HOA automata not supported yet");
+		}
+
 		// For LTL model checking routines
 		mcLtl = new LTLModelChecker(prism);