From fe95ece34204b6d98657f2e900cb86290aa9a811 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 13 Jul 2015 14:35:48 +0000 Subject: [PATCH] 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 | 38 +++++++++++++++++++++++++ prism/src/automata/LTL2DA.java | 12 +++----- prism/src/explicit/LTLModelChecker.java | 1 + prism/src/prism/NondetModelChecker.java | 1 + prism/src/prism/ProbModelChecker.java | 1 + 5 files changed, 45 insertions(+), 8 deletions(-) diff --git a/prism/src/automata/DA.java b/prism/src/automata/DA.java index d3bab963..e97f8513 100644 --- a/prism/src/automata/DA.java +++ b/prism/src/automata/DA.java @@ -323,4 +323,42 @@ public class DA // 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. + *
+ * 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. + *
+ * 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. + } } diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java index cc77562c..c3e57fc2 100644 --- a/prism/src/automata/LTL2DA.java +++ b/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 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 } - - } diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 32b33f0c..ce11fea6 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/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 diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index a657bbb3..1c8e1f6e 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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."); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 59691de4..4ce2c813 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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.");