Deterministic automata: Better checking of atomic propositions

- Loosen check in LTL2DA for external automata, as the automata
  having less APs than expected is fine
- Add generic checking in automata.DA, will catch problems no
  matter the source of the automaton (jltl2dstar, HOA, LTL2RabinLibrary...)


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

prism/src/automata/DA.java

@@ -323,4 +323,42 @@ public class DA<Symbol, Acceptance extends AcceptanceOmega>
 		// as Java generics are only compile time, we can change the AcceptanceType
 		da.acceptance = newAcceptance;
 	}
+
+	/**
+	 * Validates that the atomic propositions of this automaton
+	 * conform to the standard values that PRISM expects:
+	 *   L0, ..., Ln-1 (in arbitrary order)
+	 * if there are {@code n} expected atomic propositions.
+	 * <br/>
+	 * The automaton may actually have less atomic propositions than expected,
+	 * e.g., if the given atomic proposition does not influence the acceptance
+	 * of a run in the automaton.
+	 * <br/>
+	 * If there is an error, throws a {@code PrismException} detailing the problem.
+	 * @param expectedNumberOfAPs the expected number of atomic propositions
+	 */
+	public void checkForCanonicalAPs(int expectedNumberOfAPs) throws PrismException {
+		BitSet seen = new BitSet();
+		for (String ap : apList) {
+			if (!ap.substring(0,1).equals("L")) {
+				throw new PrismException("In deterministic automaton, unexpected atomic proposition "+ap+", expected L0, L1, ...");
+			}
+			try {
+				int index = Integer.parseInt(ap.substring(1));
+				if (seen.get(index)) {
+					throw new PrismException("In deterministic automaton, duplicate atomic proposition "+ap);
+				}
+				if (index < 0) {
+					throw new PrismException("In deterministic automaton, unexpected atomic proposition "+ap+", expected L0, L1, ...");
+				}
+				if (index >= expectedNumberOfAPs) {
+					throw new PrismException("In deterministic automaton, unexpected atomic proposition "+ap+", expected highest index to be "+(expectedNumberOfAPs-1));
+				}
+				seen.set(index);
+			} catch (NumberFormatException e) {
+				throw new PrismException("In deterministic automaton, unexpected atomic proposition "+ap+", expected L0, L1, ...");
+			}
+		}
+		// We are fine with an empty apList or an apList that lacks some of the expected Li.
+	}
 }

prism/src/automata/LTL2DA.java

@@ -290,22 +290,18 @@ public class LTL2DA extends PrismComponent
 		}
 		return false;
 	}
-	
+
+	/** Check the atomic propositions of the (externally generated) automaton */
 	private void checkAPs(SimpleLTL ltl, List<String> automatonAPs) throws PrismException
 	{
 		APSet ltlAPs = ltl.getAPs();
-		for (String ap : ltlAPs) {
-			if (!automatonAPs.contains(ap)) {
-				throw new PrismException("Generated automaton misses atomic proposition \""+ap+"\"");
-			}
-		}
 		for (String ap : automatonAPs) {
 			if (!ltlAPs.hasAP(ap)) {
 				throw new PrismException("Generated automaton has extra atomic proposition \""+ap+"\"");
 			}
 		}
+		// It's fine for the automaton to not have APs that occur in the formula, e.g., for
+		// p0 | !p0, the external tool could simplify to 'true' and omit all APs
 	}
 
-	
-	
 }

prism/src/explicit/LTLModelChecker.java

@@ -242,6 +242,7 @@ public class LTLModelChecker extends PrismComponent
 		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;
 		mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds.");
 		// If required, export DA

prism/src/prism/NondetModelChecker.java

@@ -1013,6 +1013,7 @@ public class NondetModelChecker extends NonProbModelChecker
 				AcceptanceType.REACH
 		};
 		da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
+		da.checkForCanonicalAPs(labelDDs.size());
 		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");

prism/src/prism/ProbModelChecker.java

@@ -547,6 +547,7 @@ public class ProbModelChecker extends NonProbModelChecker
 				AcceptanceType.GENERIC
 		};
 		da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
+		da.checkForCanonicalAPs(labelDDs.size());
 		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");
 		l = System.currentTimeMillis() - l;
 		mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");