From f644011ba28abcb3c047ad6047adb841b4eaba65 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 14:46:15 +0000 Subject: [PATCH] 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 | 21 ++--- prism/src/prism/LTL2DA.java | 98 +++++++++++++++++++++++ prism/src/prism/LTL2RabinLibrary.java | 30 ++++--- prism/src/prism/LTLModelChecker.java | 12 --- prism/src/prism/MultiObjModelChecker.java | 3 +- prism/src/prism/NondetModelChecker.java | 3 +- prism/src/prism/ProbModelChecker.java | 3 +- 7 files changed, 130 insertions(+), 40 deletions(-) create mode 100644 prism/src/prism/LTL2DA.java diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 374c4bdf..c2ad1668 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/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 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."); diff --git a/prism/src/prism/LTL2DA.java b/prism/src/prism/LTL2DA.java new file mode 100644 index 00000000..0619edd5 --- /dev/null +++ b/prism/src/prism/LTL2DA.java @@ -0,0 +1,98 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// * Joachim Klein (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 convertLTLFormulaToDRA(Expression ltl, Values constantValues) throws PrismException + { + return (DA) 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 convertLTLFormulaToDA(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException + { + DA 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; + } +} diff --git a/prism/src/prism/LTL2RabinLibrary.java b/prism/src/prism/LTL2RabinLibrary.java index 278ff961..c3344437 100644 --- a/prism/src/prism/LTL2RabinLibrary.java +++ b/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 + *
    + *
  1. hard-coded DRA for special formulas
    2. + *
  2. direct translation into DRA for simple path formulas with temporal bounds
    3. + *
*/ 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: + *
    + *
  • First, look up hard-coded DRA from the DRA map.
    • + *
  • Second, if the formula is a simple path formula with temporal bounds, use the special + * constructions {@code constructDRAFor....} + *
+ * Return {@code null} if the automaton can not be constructed using the library. + *
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 convertLTLFormulaToDRA(Expression ltl, Values constants) throws PrismException - { + public static DA getDRAforLTL(Expression ltl, Values constants) throws PrismException { // Get list of labels appearing labels = new ArrayList(); 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 dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba()); System.out.println(dra1); - DA dra2 = convertLTLFormulaToDRA(expr, null); + DA 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"))); diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index da44ab29..14a0340f 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/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 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 diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index b3305e10..b4c3154c 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/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."); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index d9776710..70d7b99a 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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."); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 19fc6503..339a4cab 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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.");