diff --git a/prism/.classpath b/prism/.classpath index a02649b1..ec6c29c5 100644 --- a/prism/.classpath +++ b/prism/.classpath @@ -5,6 +5,7 @@ + diff --git a/prism/etc/scripts/hoa-ltl2dstar-with-ltl2ba-for-prism b/prism/etc/scripts/hoa-ltl2dstar-with-ltl2ba-for-prism new file mode 100755 index 00000000..b81389a2 --- /dev/null +++ b/prism/etc/scripts/hoa-ltl2dstar-with-ltl2ba-for-prism @@ -0,0 +1,23 @@ +#! /bin/bash + +# Interface wrapper for calling ltl2dstar with ltl2ba as the LTL->NBA tool +# Invoke from PRISM with +# -ltl2datool hoa-ltl2dstar-with-ltl2ba-for-prism -ltl2dasyntax lbt +# +# Expects ltl2dstar and ltl2ba executables on the PATH, otherwise +# specify their location using +# export LTL2DSTAR=path/to/ltl2dstar +# export LTL2BA=path/to/ltl2ba + + +# Take ltl2dstar executable from the LTL2DSTAR environment variable +# Otherwise, default to "ltl2dstar", which will search the PATH +LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar} + +# Take the ltl2ba executable from the LTL2BA environment variable +# Otherwise, default to "ltl2ba", which will search the PATH +LTL2BA_BIN=${LTL2BA-ltl2ba} + +# --output=automaton = we want the automaton +# --output-format=hoa = ... in HOA +$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL2BA_BIN" "$@" diff --git a/prism/etc/scripts/hoa-ltl2dstar-with-ltl2tgba-for-prism b/prism/etc/scripts/hoa-ltl2dstar-with-ltl2tgba-for-prism new file mode 100755 index 00000000..753ba8c0 --- /dev/null +++ b/prism/etc/scripts/hoa-ltl2dstar-with-ltl2tgba-for-prism @@ -0,0 +1,25 @@ +#! /bin/bash + +# Interface wrapper for calling ltl2dstar with Spot's ltl2tgba as the LTL->NBA tool +# Invoke from PRISM with +# -ltl2datool hoa-ltl2dstar-with-ltl2tgba-for-prism -ltl2dasyntax lbt +# +# Expects ltl2dstar and ltl2tgba executables on the PATH, otherwise +# specify their location using +# export LTL2DSTAR=path/to/ltl2dstar +# export LTL2TGBA=path/to/ltl2tgba + + +# Take ltl2dstar executable from the LTL2DSTAR environment variable +# Otherwise, default to "ltl2dstar", which will search the PATH +LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar} + +# Take the ltl2tgba executable from the LTL2TGBA environment variable +# Otherwise, default to "ltl2tgba", which will search the PATH +LTL2TGBA_BIN=${LTL2TGBA-ltl2tgba} + +# --output=automaton = we want the automaton +# --output-format=hoa = ... in HOA +# --ltl2nba = with ltl2tgba as LTL->NBA +# -s -B = as Spin neverclaim, NBA output +$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:${LTL2TGBA_BIN}@-s -B" "$@" diff --git a/prism/etc/scripts/hoa-ltl2dstar-with-ltl3ba-for-prism b/prism/etc/scripts/hoa-ltl2dstar-with-ltl3ba-for-prism new file mode 100755 index 00000000..fcb8f12f --- /dev/null +++ b/prism/etc/scripts/hoa-ltl2dstar-with-ltl3ba-for-prism @@ -0,0 +1,36 @@ +#! /bin/bash + +# Interface wrapper for calling ltl2dstar with ltl3ba as the LTL->NBA tool +# Invoke from PRISM with +# -ltl2datool hoa-ltl2dstar-with-ltl3ba-for-prism -ltl2dasyntax lbt +# +# Expects ltl2dstar and ltl3ba executables on the PATH, otherwise +# specify their location using +# export LTL2DSTAR=path/to/ltl2dstar +# export LTL3BA=path/to/ltl3ba +# +# If ltl3ba is not statically compiled, you can specify the path +# to the Buddy library using +# export BUDDY_LIB=path/to/library-dir + +# Take ltl2dstar executable from the LTL2DSTAR environment variable +# Otherwise, default to "ltl2dstar", which will search the PATH +LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar} + +# Take the ltl3ba executable from the LTL3BA environment variable +# Otherwise, default to "ltl3ba", which will search the PATH +LTL3BA_BIN=${LTL3BA-ltl3ba} + +# If BUDDY_LIB environment variable is set, add to appropriate path +if [ ! -z "$BUDDY_LIB" ]; then + if [ "$(uname)" == "Darwin" ]; then + export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" + else + export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" + fi +fi + +# --output=automaton = we want the automaton +# --output-format=hoa = ... in HOA +# --ltl2nba = with ltl3ba as LTL->NBA +$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL3BA_BIN" "$@" diff --git a/prism/etc/scripts/hoa-ltl3dra-dra-for-prism b/prism/etc/scripts/hoa-ltl3dra-dra-for-prism new file mode 100755 index 00000000..a9335b40 --- /dev/null +++ b/prism/etc/scripts/hoa-ltl3dra-dra-for-prism @@ -0,0 +1,30 @@ +#! /bin/bash + +# Interface wrapper for calling ltl3dra (state-based DRA) +# Invoke from PRISM with +# -ltl2datool hoa-ltl3dra-dra-for-prism -ltl2dasyntax spin +# +# Expects the ltl3dra on the PATH, otherwise +# specify its location using +# export LTL3DRA=path/to/ltl3dra +# +# Expects the dynamic buddy library to be in the library PATH, otherwise +# specify its location using +# export BUDDY_LIB=path/to/buddy-lib-dir + + +# Take ltl3dra executable from the LTL3DRA environment variable +# Otherwise, default to "ltl3dra", which will search the PATH +LTL3DRA_BIN=${LTL3DRA-ltl3dra} + +# If BUDDY_LIB environment variable is set, add to appropriate path +if [ ! -z "$BUDDY_LIB" ]; then + if [ "$(uname)" == "Darwin" ]; then + export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" + else + export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" + fi +fi + +# -H3 = output deterministic state-based Rabin in HOA format +$LTL3DRA_BIN -H3 -F "$1" > "$2" diff --git a/prism/etc/scripts/hoa-ltl3dra-tgdra-for-prism b/prism/etc/scripts/hoa-ltl3dra-tgdra-for-prism new file mode 100644 index 00000000..aeb502c2 --- /dev/null +++ b/prism/etc/scripts/hoa-ltl3dra-tgdra-for-prism @@ -0,0 +1,30 @@ +#! /bin/bash + +# Interface wrapper for calling ltl3dra (transition-based DRA) +# Invoke from PRISM with +# -ltl2datool hoa-ltl3dra-tgdra-for-prism -ltl2dasyntax spin +# +# Expects the ltl3dra on the PATH, otherwise +# specify its location using +# export LTL3DRA=path/to/ltl3dra +# +# Expects the dynamic buddy library to be in the library PATH, otherwise +# specify its location using +# export BUDDY_LIB=path/to/buddy-lib-dir + + +# Take ltl3dra executable from the LTL3DRA environment variable +# Otherwise, default to "ltl3dra", which will search the PATH +LTL3DRA_BIN=${LTL3DRA-ltl3dra} + +# If BUDDY_LIB environment variable is set, add to appropriate path +if [ ! -z "$BUDDY_LIB" ]; then + if [ "$(uname)" == "Darwin" ]; then + export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" + else + export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" + fi +fi + +# -H2 = output deterministic transition-based Rabin in HOA format +$LTL3DRA_BIN -H2 -F "$1" > "$2" diff --git a/prism/etc/scripts/hoa-rabinizer3-dgra-for-prism b/prism/etc/scripts/hoa-rabinizer3-dgra-for-prism new file mode 100755 index 00000000..40db41d1 --- /dev/null +++ b/prism/etc/scripts/hoa-rabinizer3-dgra-for-prism @@ -0,0 +1,17 @@ +#! /bin/bash + +# Interface wrapper for calling Rabinizer3 (state-based DGRA) +# Invoke from PRISM with +# -ltl2datool hoa-rabinizer3-dra-for-prism -ltl2dasyntax rabinizer +# +# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise +# specify its location using +# export RABINIZER3=path/to/rabinizer.jar + +# Take location of the jar file from RABINIZER3 environment variable +# Otherwise, default to current directory +RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} + +# -hoa = output HOA +# -gen-states = output state-based generalized Rabin +java -jar $RABINIZER3_JAR -hoa -gen-states "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa-rabinizer3-dra-for-prism b/prism/etc/scripts/hoa-rabinizer3-dra-for-prism new file mode 100755 index 00000000..b264778a --- /dev/null +++ b/prism/etc/scripts/hoa-rabinizer3-dra-for-prism @@ -0,0 +1,17 @@ +#! /bin/bash + +# Interface wrapper for calling Rabinizer3 (state-based DRA) +# Invoke from PRISM with +# -ltl2datool hoa-rabinizer3-dra-for-prism -ltl2dasyntax rabinizer +# +# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise +# specify its location using +# export RABINIZER3=path/to/rabinizer.jar + +# Take location of the jar file from RABINIZER3 environment variable +# Otherwise, default to current directory +RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} + +# -hoa = output HOA +# -rabin-states = output state-based DRA +java -jar $RABINIZER3_JAR -hoa -rabin-states "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa-rabinizer3-tdra-for-prism b/prism/etc/scripts/hoa-rabinizer3-tdra-for-prism new file mode 100644 index 00000000..f7feb58c --- /dev/null +++ b/prism/etc/scripts/hoa-rabinizer3-tdra-for-prism @@ -0,0 +1,17 @@ +#! /bin/bash + +# Interface wrapper for calling Rabinizer3 (transition-based DRA) +# Invoke from PRISM with +# -ltl2datool hoa-rabinizer3-tdra-for-prism -ltl2dasyntax rabinizer +# +# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise +# specify its location using +# export RABINIZER3=path/to/rabinizer.jar + +# Take location of the jar file from RABINIZER3 environment variable +# Otherwise, default to current directory +RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} + +# -hoa = output HOA +# -rabin-edges = output transition-based Rabin +java -jar $RABINIZER3_JAR -hoa -rabin-edges "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa-rabinizer3-tgdra-for-prism b/prism/etc/scripts/hoa-rabinizer3-tgdra-for-prism new file mode 100644 index 00000000..1bb8b3f8 --- /dev/null +++ b/prism/etc/scripts/hoa-rabinizer3-tgdra-for-prism @@ -0,0 +1,17 @@ +#! /bin/bash + +# Interface wrapper for calling Rabinizer3 (transition-based DGRA) +# Invoke from PRISM with +# -ltl2datool hoa-rabinizer3-tgdra-for-prism -ltl2dasyntax rabinizer +# +# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise +# specify its location using +# export RABINIZER3=path/to/rabinizer.jar + +# Take location of the jar file from RABINIZER3 environment variable +# Otherwise, default to current directory +RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} + +# -hoa = output HOA +# -gen-edges = output transition-based generalized Rabin +java -jar $RABINIZER3_JAR -hoa -gen-edges "$1" && mv "$1.hoa" "$2" diff --git a/prism/lib/jhoafparser-1.1.0-rc3.jar b/prism/lib/jhoafparser-1.1.0-rc3.jar new file mode 100644 index 00000000..938b72e8 Binary files /dev/null and b/prism/lib/jhoafparser-1.1.0-rc3.jar differ diff --git a/prism/src/acceptance/AcceptanceGenRabin.java b/prism/src/acceptance/AcceptanceGenRabin.java new file mode 100644 index 00000000..5ce9c6c2 --- /dev/null +++ b/prism/src/acceptance/AcceptanceGenRabin.java @@ -0,0 +1,293 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// 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 acceptance; + +import java.util.ArrayList; +import java.util.BitSet; + +import jdd.JDDVars; + +/** + * A Generalized Rabin acceptance condition (based on BitSet state sets) + * This is a list of GenRabinPairs, which can be manipulated with the usual List interface. + *
+ * Semantics: Each Generalized Rabin pair has state sets L and K_1,...,K_n and is accepting iff + * L is not visited infinitely often and all K_j are visited infinitely often: + * (F G !"L") & (G F "K_1") & ... & (G F "K_n"). + * + * The Generalized Rabin condition is accepting if at least one of the pairs is accepting. + */ +@SuppressWarnings("serial") +public class AcceptanceGenRabin + extends ArrayList + implements AcceptanceOmega +{ + + /** + * A pair in a Generalized Rabin acceptance condition, i.e., with + * (F G !"L") & (G F "K_1") & ... & (G F "K_n"). + **/ + public static class GenRabinPair { + /** State set L (should be visited only finitely often) */ + private BitSet L; + + /** State sets K_j (should all be visited infinitely often) */ + private ArrayList K_list; + + /** Constructor with L and K_j state sets */ + public GenRabinPair(BitSet L, ArrayList K_list) { + this.L = L; + this.K_list = K_list; + } + + /** Get the state set L */ + public BitSet getL() + { + return L; + } + + /** Get the number of K_j sets */ + public int getNumK() + { + return K_list.size(); + } + + /** Get the state set K_j */ + public BitSet getK(int j) + { + return K_list.get(j); + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this pair. + */ + public boolean isBSCCAccepting(BitSet bscc_states) + { + if (L.intersects(bscc_states)) { + // there is some state in bscc_states that is + // forbidden by L + return false; + } + + for (BitSet K_j : K_list) { + if (!K_j.intersects(bscc_states)) { + // there is some state in bscc_states that is + // contained in K -> infinitely often visits to K + return false; + } + } + + return true; + } + + /** Generate signature for this Rabin pair and the given state. + * If the state is a member of L, returns "-pairIndex". + * If the state is a member of K, returns "+pairIndex". + * @param stateIndex the state index + * @param pairIndex the index of this Rabin pair + **/ + public String getSignatureForState(int stateIndex, int pairIndex) + { + // TODO: (What is the correct syntax here?) + /*if (L.get(stateIndex)) { + return "-"+pairIndex; + } else if (K.get(stateIndex)) { + return "+"+pairIndex; + } else { + return ""; + }*/ + return "?"; + } + + @Override + public GenRabinPair clone() + { + ArrayList newK_list = new ArrayList(); + for (BitSet K_j : K_list) + newK_list.add((BitSet) K_j.clone()); + return new GenRabinPair((BitSet)L.clone(), newK_list); + } + + public AcceptanceGeneric toAcceptanceGeneric() + { + AcceptanceGeneric genericL = new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet) L.clone()); + if (getNumK() == 0) { + return genericL; + } + AcceptanceGeneric genericKs = null; + for (BitSet K : K_list) { + AcceptanceGeneric genericK = new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet) K.clone()); + if (genericKs == null) { + genericKs = genericK; + } else { + genericKs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericKs, genericK); + } + } + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericL, genericKs); + } + + /** Returns a textual representation of this Generalized Rabin pair. */ + @Override + public String toString() { + String s = "(" + L; + for (BitSet K_j : K_list) + s += "," + K_j; + s += ")"; + return s; + } + } + + /** Make a copy of the acceptance condition. */ + public AcceptanceGenRabin clone() + { + AcceptanceGenRabin result = new AcceptanceGenRabin(); + for (GenRabinPair pair : this) { + result.add(pair.clone()); + } + + return result; + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this Rabin condition, + * i.e., there is a pair that accepts for bscc_states. + */ + public boolean isBSCCAccepting(BitSet bscc_states) + { + for (GenRabinPair pair : this) { + if (pair.isBSCCAccepting(bscc_states)) { + return true; + } + } + + return false; + } + + @Override + public void lift(LiftBitSet lifter) { + for (GenRabinPair pair : this) { + pair.L = lifter.lift(pair.L); + int n = pair.K_list.size(); + for (int j = 0; j < n; j++) + pair.K_list.set(j, lifter.lift(pair.K_list.get(j))); + } + } + + /** + * Returns a new Generalized Rabin acceptance condition that corresponds to the disjunction + * of this and the other Generalized Rabin acceptance condition. The GenRabinPairs are cloned, i.e., + * not shared with the argument acceptance condition. + * @param other the other GeneralizedRabin acceptance condition + * @return new AcceptanceGenRabin, disjunction of this and other + */ + public AcceptanceGenRabin or(AcceptanceGenRabin other) + { + AcceptanceGenRabin result = new AcceptanceGenRabin(); + for (GenRabinPair pair : this) { + result.add((GenRabinPair) pair.clone()); + } + for (GenRabinPair pair : other) { + result.add((GenRabinPair) pair.clone()); + } + return result; + } + + @Override + public AcceptanceGenRabinDD toAcceptanceDD(JDDVars ddRowVars) + { + return new AcceptanceGenRabinDD(this, ddRowVars); + } + + @Override + public AcceptanceGeneric toAcceptanceGeneric() + { + if (size() == 0) { + return new AcceptanceGeneric(false); + } + AcceptanceGeneric genericPairs = null; + for (GenRabinPair pair : this) { + AcceptanceGeneric genericPair = pair.toAcceptanceGeneric(); + if (genericPairs == null) { + genericPairs = genericPair; + } else { + genericPairs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, genericPairs, genericPair); + } + } + return genericPairs; + } + + /** + * Get the acceptance signature for state stateIndex. + **/ + public String getSignatureForState(int stateIndex) + { + String result = ""; + + for (int pairIndex=0; pairIndex (TU Dresden) +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// 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 acceptance; + +import java.util.ArrayList; + +import common.IterableBitSet; + +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * A Generalized Rabin acceptance condition (based on JDD state sets) + * This is a list of GenRabinPairs, which can be manipulated with the usual List interface. + *
+ * Semantics: Each Generalized Rabin pair has state sets L and K_1,...,K_n and is accepting iff + * L is not visited infinitely often and all K_j are visited infinitely often: + * (F G !"L") & (G F "K_1") & ... & (G F "K_n"). + * + * The Generalized Rabin condition is accepting if at least one of the pairs is accepting. + */ +@SuppressWarnings("serial") +public class AcceptanceGenRabinDD + extends ArrayList + implements AcceptanceOmegaDD +{ + + /** + * A pair in a Generalized Rabin acceptance condition, i.e., with + * (F G !"L") & (G F "K_1") & ... & (G F "K_n"). + **/ + public static class GenRabinPairDD { + /** State set L (should be visited only finitely often) */ + private JDDNode L; + + /** State sets K_j (should all be visited infinitely often) */ + private ArrayList K_list; + + /** + * Constructor with L and K_j state sets. + * Becomes owner of the references of L and K_j's. + */ + public GenRabinPairDD(JDDNode L, ArrayList K_list) + { + this.L = L; + this.K_list = K_list; + } + + /** Clear resources of the state sets */ + public void clear() + { + if (L!=null) JDD.Deref(L); + for (JDDNode K_j : K_list) + JDD.Deref(K_j); + } + + /** Get a referenced copy of the state set L. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getL() + { + JDD.Ref(L); + return L; + } + + /** Get the number of K_j sets */ + public int getNumK() + { + return K_list.size(); + } + + /** Get a referenced copy of the state set K_j. + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getK(int j) + { + JDD.Ref(K_list.get(j)); + return K_list.get(j); + } + + /** Returns true if the bottom strongly connected component + * given by bscc_states is accepting for this pair. + *
[ REFS: none, DEREFS: none ] + */ + public boolean isBSCCAccepting(JDDNode bscc_states) + { + if (JDD.AreInterecting(L, bscc_states)) { + // there is some state in bscc_states that is + // forbidden by L + return false; + } + + for (JDDNode K_j : K_list) { + if (!JDD.AreInterecting(K_j, bscc_states)) { + // there is some state in bscc_states that is + // contained in K_j -> infinitely often visits to K_j + return false; + } + } + + return true; + } + + /** Returns a textual representation of this Rabin pair. */ + @Override + public String toString() + { + String s = "(" + L; + for (JDDNode K_j : K_list) + s += "," + K_j; + s += ")"; + return s; + } + } + + /** + * Constructor, from a BitSet-based AcceptanceGenRabin. + * + * @param acceptance the BitSet-based acceptance condition + * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bit set + */ + public AcceptanceGenRabinDD(AcceptanceGenRabin acceptance, JDDVars ddRowVars) + { + for (AcceptanceGenRabin.GenRabinPair pair : acceptance) { + // get BDD based newL and newK from the bit sets + JDDNode newL = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(pair.getL())) { + newL = JDD.SetVectorElement(newL, ddRowVars, i, 1.0); + } + + ArrayList newK_list = new ArrayList(); + int n = pair.getNumK(); + for (int j = 0; j < n; j++) { + JDDNode newK_j = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(pair.getK(j))) { + newK_j = JDD.SetVectorElement(newK_j, ddRowVars, i, 1.0); + } + newK_list.add(newK_j); + } + + GenRabinPairDD newPair = new GenRabinPairDD(newL, newK_list); + this.add(newPair); + } + } + + @Override + public boolean isBSCCAccepting(JDDNode bscc_states) + { + for (GenRabinPairDD pair : this) { + if (pair.isBSCCAccepting(bscc_states)) { + return true; + } + } + return false; + } + + @Override + public void clear() + { + for (GenRabinPairDD pair : this) { + pair.clear(); + } + super.clear(); + } + + /** Returns a textual representation of this acceptance condition. */ + @Override + public String toString() + { + String result = ""; + for (GenRabinPairDD pair : this) { + result += pair.toString(); + } + return result; + } + + @Override + public String getSizeStatistics() + { + return size() + " Generalized Rabin pairs"; + } + + @Override + public AcceptanceType getType() + { + return AcceptanceType.GENERALIZED_RABIN; + } + + @Override + public String getTypeAbbreviated() + { + return "GR"; + } + + @Override + public String getTypeName() + { + return "Generalized Rabin"; + } +} diff --git a/prism/src/acceptance/AcceptanceGeneric.java b/prism/src/acceptance/AcceptanceGeneric.java new file mode 100644 index 00000000..f6b662c3 --- /dev/null +++ b/prism/src/acceptance/AcceptanceGeneric.java @@ -0,0 +1,275 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// 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 acceptance; + +import java.util.BitSet; + +import jdd.JDDVars; + +/** + * A generic acceptance condition (based on BitSet state sets). + * This is an AST of a boolean formula (conjunction and disjunction) over + * atoms of the form Inf(states), Inf(!states), Fin(states) and Fin(!states). + *
+ * Semantics: + * Inf(states) <=> G F states + * Inf(!states) <=> G F !states + * Fin(states) <=> F G !states + * Fin(!states) <=> F G states + */ +public class AcceptanceGeneric implements AcceptanceOmega { + + /** The types of elements in the AST */ + public enum ElementType { + FALSE, + TRUE, + + OR, + AND, + + INF, + FIN, + INF_NOT, + FIN_NOT; + } + + /** The type of this node in the AST */ + private ElementType kind; + + /** The left child (if it exists) */ + private AcceptanceGeneric left = null; + + /** The right child (if it exists) */ + private AcceptanceGeneric right = null; + + /** The set of states (if this is one of INF, FIN, INF_NOT, FIN_NOT) */ + private BitSet states = null; + + /** + * Constructor for TRUE or FALSE + * @param value true or false? + */ + public AcceptanceGeneric(boolean value) { + kind = value ? ElementType.TRUE : ElementType.FALSE; + } + + /** + * Constructor for an INF, FIN, INF_NOT or FIN_NOT element. + */ + public AcceptanceGeneric(ElementType kind, BitSet states) { + this.kind = kind; + + this.states = states; + } + + /** + * Constructor for a binary operator (AND/OR). + * @param kind + * @param left + * @param right + */ + public AcceptanceGeneric(ElementType kind, AcceptanceGeneric left, AcceptanceGeneric right) { + this.kind = kind; + this.left = left; + this.right = right; + } + + /** Get the ElementType of this AST element */ + public ElementType getKind() { + return kind; + } + + /** Get the left child of this AST element */ + public AcceptanceGeneric getLeft() { + return left; + } + + /** Get the right child of this AST element */ + public AcceptanceGeneric getRight() { + return right; + } + + /** Get the state set of this element (if kind is one of INF, FIN, INF_NOT, FIN_NOT). + */ + public BitSet getStates() { + return states; + } + + @Override + public boolean isBSCCAccepting(BitSet bscc) { + switch(kind) { + case TRUE: return true; + case FALSE: return false; + case AND: return left.isBSCCAccepting(bscc) && right.isBSCCAccepting(bscc); + case OR: return left.isBSCCAccepting(bscc) || right.isBSCCAccepting(bscc); + case INF: + // bscc |= G F states? + // there exists a state in bscc and states + return bscc.intersects(states); + case INF_NOT: { + // bscc_state |= G F !states? + // the BSCC does not consist only of states + BitSet bs = (BitSet) bscc.clone(); + bs.andNot(states); + return !bs.isEmpty(); + } + case FIN: { + // bscc |= F G !states? + // <=> there exists no states state in BSCC + return !bscc.intersects(states); + } + case FIN_NOT: { + // bscc |= F G states? + // the BSCC consists entirely of states + BitSet bs = (BitSet) bscc.clone(); + bs.and(states); + return bs.equals(bscc); + } + } + return false; + } + + @Override + public String getSignatureForState(int i) { + return ""; + } + + @Override + public String getSizeStatistics() { + return "generic acceptance with " + countAcceptanceSets() + " acceptance sets"; + } + + @Override + public AcceptanceType getType() { + return AcceptanceType.GENERIC; + } + + @Override + public String getTypeAbbreviated() { + return ""; + } + + @Override + public String getTypeName() { + return "generic"; + } + + @Override + public AcceptanceGeneric clone() { + switch (kind) { + case FIN: + case FIN_NOT: + case INF: + case INF_NOT: + return new AcceptanceGeneric(kind, states); + case AND: + case OR: + return new AcceptanceGeneric(kind, left.clone(), right.clone()); + case FALSE: + return new AcceptanceGeneric(false); + case TRUE: + return new AcceptanceGeneric(true); + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition"); + } + + @Override + public void lift(LiftBitSet lifter) { + switch(kind) { + case TRUE: + case FALSE: + return; + case INF: + case INF_NOT: + case FIN: + case FIN_NOT: + states = lifter.lift(states); + return; + case AND: + case OR: + left.lift(lifter); + right.lift(lifter); + return; + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition"); + } + + /** Count the number of state sets in this acceptance condition */ + public int countAcceptanceSets() { + switch(kind) { + case FALSE: + case TRUE: + return 0; + case INF: + case FIN: + case INF_NOT: + case FIN_NOT: + return 1; + case OR: + case AND: + return left.countAcceptanceSets() + right.countAcceptanceSets(); + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance condition"); + } + + @Override + public AcceptanceOmegaDD toAcceptanceDD(JDDVars ddRowVars) { + return new AcceptanceGenericDD(this, ddRowVars); + } + + @Override + public AcceptanceGeneric toAcceptanceGeneric() + { + return this.clone(); + } + + @Override + public String toString() { + switch(kind) { + case TRUE: + return "true"; + case FALSE: + return "false"; + case AND: + return "(" + left.toString() + " & " + right.toString() + ")"; + case OR: + return "(" + left.toString() + " | " + right.toString() + ")"; + case INF: + return "Inf(" + states.toString() + ")"; + case FIN: + return "Fin(" + states.toString() + ")"; + case INF_NOT: + return "Inf(!" + states.toString() + ")"; + case FIN_NOT: + return "Fin(!" + states.toString() + ")"; + default: + return null; + } + } + +} diff --git a/prism/src/acceptance/AcceptanceGenericDD.java b/prism/src/acceptance/AcceptanceGenericDD.java new file mode 100644 index 00000000..3c7e7c67 --- /dev/null +++ b/prism/src/acceptance/AcceptanceGenericDD.java @@ -0,0 +1,206 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// 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 acceptance; + +import common.IterableBitSet; +import acceptance.AcceptanceGeneric.ElementType; +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; + +/** + * A generic acceptance condition (based on JDD state sets). + * This is an AST of a boolean formula (conjunction and disjunction) over + * atoms of the form Inf(states), Inf(!states), Fin(states) and Fin(!states). + *
+ * Semantics: + * Inf(states) <=> G F states + * Inf(!states) <=> G F !states + * Fin(states) <=> F G !states + * Fin(!states) <=> F G states + */ +public class AcceptanceGenericDD implements AcceptanceOmegaDD { + + private ElementType kind; + private AcceptanceGenericDD left = null; + private AcceptanceGenericDD right = null; + private JDDNode states = null; + + public AcceptanceGenericDD(AcceptanceGeneric acceptance, JDDVars ddRowVars) + { + switch(acceptance.getKind()) { + case AND: + case OR: + kind = acceptance.getKind(); + left = (AcceptanceGenericDD) acceptance.getLeft().toAcceptanceDD(ddRowVars); + right = (AcceptanceGenericDD) acceptance.getRight().toAcceptanceDD(ddRowVars); + return; + case TRUE: + kind = ElementType.TRUE; + return; + case FALSE: + kind = ElementType.FALSE; + return; + case INF: + case INF_NOT: + case FIN: + case FIN_NOT: + kind = acceptance.getKind(); + states = JDD.Constant(0); + for (int i : IterableBitSet.getSetBits(acceptance.getStates())) { + states = JDD.SetVectorElement(states, ddRowVars, i, 1.0); + } + return; + } + throw new UnsupportedOperationException("Unsupported operatator in generic acceptance condition"); + } + + /** Get the ElementType of this AST element */ + public ElementType getKind() + { + return kind; + } + + /** Get the left child of this AST element */ + public AcceptanceGenericDD getLeft() + { + return left; + } + + /** Get the right child of this AST element */ + public AcceptanceGenericDD getRight() + { + return right; + } + + /** Get a referenced copy of the state sets (if kind is one of INF, FIN, INF_NOT, FIN_NOT). + *
[ REFS: result, DEREFS: none ] + */ + public JDDNode getStates() + { + if (states != null) { + JDD.Ref(states); + } + return states; + } + + @Override + public boolean isBSCCAccepting(JDDNode bscc) + { + switch(kind) { + case TRUE: + return true; + case FALSE: + return false; + case AND: + return left.isBSCCAccepting(bscc) && right.isBSCCAccepting(bscc); + case OR: + return left.isBSCCAccepting(bscc) || right.isBSCCAccepting(bscc); + case INF: + // bscc |= G F states? + // there exists a state in bscc and states + return JDD.AreInterecting(states, bscc); + case INF_NOT: + // bscc_state |= G F !states? + // the BSCC intersects Not(states) + JDD.Ref(states); + return JDD.AreInterecting(JDD.Not(states), bscc); + case FIN: + // bscc |= F G !states? + // the BSCC consists only of !states + return !JDD.AreInterecting(states, bscc); + case FIN_NOT: + // bscc |= F G states? + // the BSCC consists entirely of states + JDD.Ref(states); + return !JDD.AreInterecting(JDD.Not(states), bscc); + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression"); + } + + @Override + public String getSizeStatistics() { + return "generic acceptance with " + countAcceptanceSets() + " acceptance sets"; + } + + @Override + public AcceptanceType getType() { + return AcceptanceType.GENERIC; + } + + @Override + public String getTypeAbbreviated() { + return ""; + } + + @Override + public String getTypeName() { + return "generic"; + } + + @Override + public void clear() { + switch (kind) { + case TRUE: + case FALSE: + return; + case AND: + case OR: + left.clear(); + right.clear(); + return; + case INF_NOT: + case FIN: + case FIN_NOT: + case INF: + if (states != null) JDD.Deref(states); + states = null; + return; + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression"); + } + + /** Count the number of state sets in this acceptance condition */ + public int countAcceptanceSets() { + switch(kind) { + case FALSE: + case TRUE: + return 0; + case INF: + case FIN: + case INF_NOT: + case FIN_NOT: + return 1; + case OR: + case AND: + return left.countAcceptanceSets() + right.countAcceptanceSets(); + } + throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression"); + } + +} diff --git a/prism/src/acceptance/AcceptanceOmega.java b/prism/src/acceptance/AcceptanceOmega.java index d5bf48ca..e55b1cbf 100644 --- a/prism/src/acceptance/AcceptanceOmega.java +++ b/prism/src/acceptance/AcceptanceOmega.java @@ -82,4 +82,9 @@ public interface AcceptanceOmega extends Cloneable * @param ddRowVars JDDVars of the row variables corresponding to the bits in the bitset */ public AcceptanceOmegaDD toAcceptanceDD(JDDVars ddRowVars); + + /** + * Convert this acceptance condition to an AcceptanceGeneric condition. + */ + public AcceptanceGeneric toAcceptanceGeneric(); } diff --git a/prism/src/acceptance/AcceptanceRabin.java b/prism/src/acceptance/AcceptanceRabin.java index 7c855c41..94f42b48 100644 --- a/prism/src/acceptance/AcceptanceRabin.java +++ b/prism/src/acceptance/AcceptanceRabin.java @@ -96,6 +96,16 @@ public class AcceptanceRabin return false; } + public AcceptanceGeneric toAcceptanceGeneric() + { + AcceptanceGeneric genericL = new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet)L.clone()); + AcceptanceGeneric genericK = new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet)K.clone()); + + // F G ! "L" & G F "K" + // <=> Fin(L) & Inf(K) + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericL, genericK); + } + /** Generate signature for this Rabin pair and the given state. * If the state is a member of L, returns "-pairIndex". * If the state is a member of K, returns "+pairIndex". @@ -204,6 +214,24 @@ public class AcceptanceRabin return new AcceptanceRabinDD(this, ddRowVars); } + @Override + public AcceptanceGeneric toAcceptanceGeneric() + { + if (size() == 0) { + return new AcceptanceGeneric(false); + } + AcceptanceGeneric genericPairs = null; + for (RabinPair pair : this) { + AcceptanceGeneric genericPair = pair.toAcceptanceGeneric(); + if (genericPairs == null) { + genericPairs = genericPair; + } else { + genericPairs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, genericPairs, genericPair); + } + } + return genericPairs; + } + /** * Get the acceptance signature for state stateIndex. **/ diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java index b657bfd2..035b6a9b 100644 --- a/prism/src/acceptance/AcceptanceRabinDD.java +++ b/prism/src/acceptance/AcceptanceRabinDD.java @@ -98,6 +98,7 @@ public class AcceptanceRabinDD /** Returns true if the bottom strongly connected component * given by bscc_states is accepting for this pair. + *
[ REFS: none, DEREFS: none ] */ public boolean isBSCCAccepting(JDDNode bscc_states) { @@ -149,10 +150,7 @@ public class AcceptanceRabinDD } } - /** Returns true if the bottom strongly connected component - * given by bscc_states is accepting for this Rabin condition, - * i.e., there is a pair that accepts for bscc_states. - */ + @Override public boolean isBSCCAccepting(JDDNode bscc_states) { for (RabinPairDD pair : this) { diff --git a/prism/src/acceptance/AcceptanceReach.java b/prism/src/acceptance/AcceptanceReach.java index 96774472..74af4192 100644 --- a/prism/src/acceptance/AcceptanceReach.java +++ b/prism/src/acceptance/AcceptanceReach.java @@ -28,8 +28,6 @@ package acceptance; import java.util.BitSet; -import acceptance.AcceptanceRabin.RabinPair; - import jdd.JDDVars; /** @@ -91,6 +89,12 @@ public class AcceptanceReach implements AcceptanceOmega return new AcceptanceReachDD(this, ddRowVars); } + @Override + public AcceptanceGeneric toAcceptanceGeneric() + { + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet) goalStates.clone()); + } + @Override public String getSignatureForState(int i) { diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java index 18c85c85..134525ec 100644 --- a/prism/src/acceptance/AcceptanceReachDD.java +++ b/prism/src/acceptance/AcceptanceReachDD.java @@ -1,9 +1,9 @@ -package acceptance; //============================================================================== // //Copyright (c) 2014- //Authors: -//* Joachim Klein (TU Dresden) +// * Joachim Klein (TU Dresden) +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -25,6 +25,8 @@ package acceptance; // //============================================================================== +package acceptance; + import common.IterableBitSet; import jdd.JDD; import jdd.JDDNode; diff --git a/prism/src/acceptance/AcceptanceStreett.java b/prism/src/acceptance/AcceptanceStreett.java index 51dae747..852ea066 100644 --- a/prism/src/acceptance/AcceptanceStreett.java +++ b/prism/src/acceptance/AcceptanceStreett.java @@ -98,6 +98,17 @@ public class AcceptanceStreett } } + public AcceptanceGeneric toAcceptanceGeneric() + { + AcceptanceGeneric genericR = new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, (BitSet)R.clone()); + AcceptanceGeneric genericG = new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, (BitSet)G.clone()); + // G F "R" -> G F "G" + // <=> ! G F "R" | G F "G" + // <=> F G ! "R" | G F "G" + // <=> Fin(R) | Inf(G) + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, genericR, genericG); + } + /** Generate signature for this Streett pair and the given state. * If the state is a member of R, returns "-pairIndex". * If the state is a member of G, returns "+pairIndex". @@ -206,6 +217,24 @@ public class AcceptanceStreett return new AcceptanceStreettDD(this, ddRowVars); } + @Override + public AcceptanceGeneric toAcceptanceGeneric() + { + if (size() == 0) { + return new AcceptanceGeneric(true); + } + AcceptanceGeneric genericPairs = null; + for (StreettPair pair : this) { + AcceptanceGeneric genericPair = pair.toAcceptanceGeneric(); + if (genericPairs == null) { + genericPairs = genericPair; + } else { + genericPairs = new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, genericPairs, genericPair); + } + } + return genericPairs; + } + /** * Get the acceptance signature for state stateIndex. **/ diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java index b2075d93..a643f022 100644 --- a/prism/src/acceptance/AcceptanceStreettDD.java +++ b/prism/src/acceptance/AcceptanceStreettDD.java @@ -98,6 +98,7 @@ public class AcceptanceStreettDD /** Returns true if the bottom strongly connected component * given by bscc_states is accepting for this pair. + *
[ REFS: none, DEREFS: none ] */ public boolean isBSCCAccepting(JDDNode bscc_states) { diff --git a/prism/src/acceptance/AcceptanceType.java b/prism/src/acceptance/AcceptanceType.java index a3d53730..2901f1dd 100644 --- a/prism/src/acceptance/AcceptanceType.java +++ b/prism/src/acceptance/AcceptanceType.java @@ -3,6 +3,7 @@ // Copyright (c) 2014- // Authors: // * Joachim Klein (TU Dresden) +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -32,7 +33,9 @@ package acceptance; public enum AcceptanceType { RABIN, STREETT, - REACH; + REACH, + GENERALIZED_RABIN, + GENERIC; /** * Check whether an array of AcceptanceTypes contains a specific element. diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index a524d3a7..fd010195 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -76,7 +76,8 @@ public class DTMCModelChecker extends ProbModelChecker // Build product of Markov chain and automaton AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, - AcceptanceType.REACH + AcceptanceType.REACH, + AcceptanceType.GENERIC }; product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest, allowedAcceptance); diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index ca15a933..cb6cce1b 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -54,6 +54,7 @@ import prism.PrismFileLog; import prism.PrismLangException; import prism.PrismLog; import prism.PrismNotSupportedException; +import acceptance.AcceptanceGenRabin; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; import acceptance.AcceptanceType; @@ -594,6 +595,8 @@ public class LTLModelChecker extends PrismComponent { if (acceptance instanceof AcceptanceRabin) { return findAcceptingECStatesForRabin(model, (AcceptanceRabin) acceptance); + } else if (acceptance instanceof AcceptanceGenRabin) { + return findAcceptingECStatesForGeneralizedRabin(model, (AcceptanceGenRabin) acceptance); } throw new PrismNotSupportedException("Computing end components for acceptance type '"+acceptance.getTypeName()+"' currently not supported (explicit engine)."); } @@ -634,6 +637,53 @@ public class LTLModelChecker extends PrismComponent return allAcceptingStates; } + /** + * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Generalized Rabin acceptance condition. + * @param model The model + * @param acceptance The acceptance condition + */ + public BitSet findAcceptingECStatesForGeneralizedRabin(NondetModel model, AcceptanceGenRabin acceptance) throws PrismException + { + BitSet allAcceptingStates = new BitSet(); + int numStates = model.getNumStates(); + + // Go through the GR acceptance pairs (L_i, K_i_1, ..., K_i_n) + for (int i = 0; i < acceptance.size(); i++) { + + // Find model states *not* satisfying L_i + BitSet bitsetLi = acceptance.get(i).getL(); + BitSet statesLi_not = new BitSet(); + for (int s = 0; s < numStates; s++) { + if (!bitsetLi.get(s)) { + statesLi_not.set(s); + } + } + // Skip pairs with empty !L_i + if (statesLi_not.cardinality() == 0) + continue; + // Compute maximum end components (MECs) in !L_i + ECComputer ecComputer = ECComputer.createECComputer(this, model); + ecComputer.computeMECStates(statesLi_not); + List mecs = ecComputer.getMECStates(); + // Check which MECs contain a state from each K_i_j + int n = acceptance.get(i).getNumK(); + for (BitSet mec : mecs) { + boolean allj = true; + for (int j = 0; j < n; j++) { + if (!mec.intersects(acceptance.get(i).getK(j))) { + allj = false; + break; + } + } + if (allj) { + allAcceptingStates.or(mec); + } + } + } + + return allAcceptingStates; + } + /** Lift the acceptance condition from the automaton to the product states. */ private AcceptanceOmega liftAcceptance(final LTLProduct product, AcceptanceOmega acceptance) { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index b40413d6..3931ec70 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -84,6 +84,7 @@ public class MDPModelChecker extends ProbModelChecker AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, + AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH }; diff --git a/prism/src/jltl2ba/APSet.java b/prism/src/jltl2ba/APSet.java index fdc8ec68..1d215c3f 100644 --- a/prism/src/jltl2ba/APSet.java +++ b/prism/src/jltl2ba/APSet.java @@ -45,7 +45,7 @@ public class APSet implements Iterable { * @param name the name of the AP * @return the index of the added AP */ - int addAP(String name) { + public int addAP(String name) { int i = vector.indexOf(name); if (i == -1) { diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java index 2585417f..08c24c26 100644 --- a/prism/src/jltl2ba/SimpleLTL.java +++ b/prism/src/jltl2ba/SimpleLTL.java @@ -587,7 +587,49 @@ public class SimpleLTL { } return rv; } - + + /** + * Returns an equivalent SimpleLTL formula with a + * basic set of operators: + * AP, TRUE, FALSE, AND, OR, NOT, UNTIL, FINALLY, GLOBALLY, NEXT + */ + public SimpleLTL toBasicOperators() { + switch (kind) { + case AP: + case TRUE: + case FALSE: + return this; + case AND: + case OR: + case UNTIL: + return new SimpleLTL(kind, left.toBasicOperators(), right.toBasicOperators()); + case FINALLY: + case GLOBALLY: + case NEXT: + case NOT: + return new SimpleLTL(kind, left.toBasicOperators()); + case EQUIV: { + SimpleLTL newLeft = left.toBasicOperators(); + SimpleLTL newRight = right.toBasicOperators(); + SimpleLTL bothTrue = new SimpleLTL(LTLType.AND, newLeft, newRight); + SimpleLTL bothFalse = new SimpleLTL(LTLType.AND, + new SimpleLTL(LTLType.NOT, newLeft), + new SimpleLTL(LTLType.NOT, newRight)); + return new SimpleLTL(LTLType.OR, bothTrue, bothFalse); + } + case IMPLIES: { + SimpleLTL newLeft = new SimpleLTL(LTLType.NOT, left.toBasicOperators()); + return new SimpleLTL(LTLType.OR, newLeft, right.toBasicOperators()); + } + case RELEASE: { + SimpleLTL newLeft = new SimpleLTL(LTLType.NOT, left.toBasicOperators()); + SimpleLTL newRight = new SimpleLTL(LTLType.NOT, right.toBasicOperators()); + return new SimpleLTL(LTLType.UNTIL, newLeft, newRight); + } + } + throw new UnsupportedOperationException("Unknown operator in SimpleLTL"); + } + public SimpleLTL negate() { return new SimpleLTL(LTLType.NOT, this); } @@ -937,6 +979,202 @@ public class SimpleLTL { } } + /** + * Renames the atomic propositions apparing in the formula that + * start with {@code prefixFrom}. For these, the prefix is replaced + * by prefixTo. For example, with prefixFrom = "L" and prefixTo = "p", + * "L3" will be renamed to "p3", but "T2" will be left as-is. + */ + public void renameAP(String prefixFrom, String prefixTo) + { + switch (kind) { + case AP: + if (ap.startsWith(prefixFrom)) { + ap = prefixTo + ap.substring(prefixFrom.length()); + } + return; + case AND: + case OR: + case EQUIV: + case IMPLIES: + case RELEASE: + case UNTIL: + left.renameAP(prefixFrom, prefixTo); + right.renameAP(prefixFrom, prefixTo); + return; + case FINALLY: + case GLOBALLY: + case NEXT: + case NOT: + left.renameAP(prefixFrom, prefixTo); + return; + case TRUE: + case FALSE: + return; + } + throw new UnsupportedOperationException("Unknown operator in SimpleLTL formula: "+this); + } + + /** + * Render this LTL formula in LBT syntax, i.e., in prefix notation. + */ + public String toStringLBT() + { + String rv = ""; + + switch (kind) { + case OR: + rv = "| " + left.toStringLBT() + " " + right.toStringLBT(); + break; + case AND: + rv = "& " + left.toStringLBT() + " " + right.toStringLBT(); + break; + case UNTIL: + rv = "U " + left.toStringLBT() + " " + right.toStringLBT(); + break; + case RELEASE: + rv = "V " + left.toStringLBT() + " " + right.toStringLBT(); + break; + case IMPLIES: + rv = "i " + left.toStringLBT() + " " + right.toStringLBT(); + break; + case EQUIV: + rv = "e " + left.toStringLBT() + " " + right.toStringLBT(); + break; + case NEXT: + rv = "X " + left.toStringLBT(); + break; + case FINALLY: + rv = "F " + left.toStringLBT(); + break; + case GLOBALLY: + rv = "G " + left.toStringLBT(); + break; + case NOT: + rv = "! " + left.toStringLBT(); + break; + case FALSE: + rv = "f"; + break; + case TRUE: + rv = "t"; + break; + case AP: + rv = ap; + break; + default: + rv = null; + } + return rv; + } + + /** + * Render this LTL formula in Spin syntax. + */ + public String toStringSpin() + { + String rv = ""; + + switch (kind) { + case OR: + rv = "(" + left.toStringSpin() + ") || (" + right.toStringSpin() + ")"; + break; + case AND: + rv = "(" + left.toStringSpin() + ") && (" + right.toStringSpin() + ")"; + break; + case UNTIL: + rv = "(" + left.toStringSpin() + ") U (" + right.toStringSpin() + ")"; + break; + case RELEASE: + rv = "(" + left.toStringSpin() + ") V (" + right.toStringSpin() + ")"; + break; + case IMPLIES: + rv = "(" + left.toStringSpin() + ") -> (" + right.toStringSpin() + ")"; + break; + case EQUIV: + rv = "(" + left.toStringSpin() + ") <-> (" + right.toStringSpin() + ")"; + break; + case NEXT: + rv = "X (" + left.toStringSpin() + ")"; + break; + case FINALLY: + rv = "<> (" + left.toStringSpin() + ")"; + break; + case GLOBALLY: + rv = "[] (" + left.toStringSpin() + ")"; + break; + case NOT: + rv = "! (" + left.toStringSpin() + ")"; + break; + case FALSE: + rv = "false"; + break; + case TRUE: + rv = "true"; + break; + case AP: + rv = ap; + break; + default: + rv = null; + } + return rv; + } + + + /** + * Render this LTL formula in Spot syntax. + */ + public String toStringSpot() + { + String rv = ""; + + switch (kind) { + case OR: + rv = "(" + left.toStringSpot() + ") | (" + right.toStringSpot() + ")"; + break; + case AND: + rv = "(" + left.toStringSpot() + ") & (" + right.toStringSpot() + ")"; + break; + case UNTIL: + rv = "(" + left.toStringSpot() + ") U (" + right.toStringSpot() + ")"; + break; + case RELEASE: + rv = "(" + left.toStringSpot() + ") R (" + right.toStringSpot() + ")"; + break; + case IMPLIES: + rv = "(" + left.toStringSpot() + ") -> (" + right.toStringSpot() + ")"; + break; + case EQUIV: + rv = "(" + left.toStringSpot() + ") <-> (" + right.toStringSpot() + ")"; + break; + case NEXT: + rv = "X (" + left.toStringSpot() + ")"; + break; + case FINALLY: + rv = "F (" + left.toStringSpot() + ")"; + break; + case GLOBALLY: + rv = "G (" + left.toStringSpot() + ")"; + break; + case NOT: + rv = "! (" + left.toStringSpot() + ")"; + break; + case FALSE: + rv = "false"; + break; + case TRUE: + rv = "true"; + break; + case AP: + rv = ap; + break; + default: + rv = null; + } + return rv; + } + public NBA toNBA(APSet apset) throws PrismException { Alternating a = new Alternating(this, apset); diff --git a/prism/src/jltl2dstar/APMonom.java b/prism/src/jltl2dstar/APMonom.java index 79fde85d..1ea35a78 100644 --- a/prism/src/jltl2dstar/APMonom.java +++ b/prism/src/jltl2dstar/APMonom.java @@ -67,7 +67,8 @@ public class APMonom { */ public boolean isSet(int index) throws PrismException { if (!isNormal()) { - throw new PrismException("Can't get AP, is either TRUE/FALSE!"); + // TRUE / FALSE -> the bit is not set + return false; } return bits_set.get(index); } @@ -77,7 +78,7 @@ public class APMonom { * @param index index of AP * @return true if AP is true */ - boolean getValue(int index) throws PrismException { + public boolean getValue(int index) throws PrismException { if (!isNormal()) { throw new PrismException("Can't get AP, is either TRUE/FALSE!"); } diff --git a/prism/src/prism/DA.java b/prism/src/prism/DA.java index 7bd0ff80..70d61c03 100644 --- a/prism/src/prism/DA.java +++ b/prism/src/prism/DA.java @@ -5,6 +5,7 @@ // * Dave Parker (University of Oxford) // * Hongyang Qu (University of Oxford) // * Joachim Klein (TU Dresden) +// * David Mueller (TU Dresden) // //------------------------------------------------------------------------------ // @@ -31,7 +32,11 @@ package prism; import java.io.PrintStream; import java.util.*; +import jltl2ba.APElement; +import jltl2ba.APElementIterator; import acceptance.AcceptanceOmega; +import acceptance.AcceptanceRabin; +import acceptance.AcceptanceType; /** * Class to store a deterministic automata of some acceptance type Acceptance. @@ -107,6 +112,14 @@ public class DA this.start = start; } + /** + * Returns true if the automaton has an edge for {@code src} and {@label}. + */ + public boolean hasEdge(int src, Symbol label) + { + return edges.get(src).contains(label); + } + /** * Add an edge */ @@ -200,6 +213,53 @@ public class DA } out.println("}"); } + + /** + * Print the DRA in ltl2dstar v2 format to the output stream. + * @param out the output stream + */ + public static void printLtl2dstar(DA dra, PrintStream out) throws PrismException { + AcceptanceRabin acceptance = dra.getAcceptance(); + + if (dra.getStartState() < 0) { + // No start state! + throw new PrismException("No start state in DA!"); + } + + out.println("DRA v2 explicit"); + out.println("States: " + dra.size()); + out.println("Acceptance-Pairs: " + acceptance.size()); + out.println("Start: " + dra.getStartState()); + + // Enumerate APSet + out.print("AP: " + dra.getAPList().size()); + for (String ap : dra.getAPList()) { + out.print(" \"" + ap + "\""); + } + out.println(); + + out.println("---"); + + for (int i_state = 0; i_state < dra.size(); i_state++) { + out.println("State: " + i_state); + + out.print("Acc-Sig:"); + for (int pair = 0; pair < acceptance.size(); pair++) { + if (acceptance.get(pair).getL().get(i_state)) { + out.print(" -"+pair); + } else if (acceptance.get(pair).getK().get(i_state)) { + out.print(" +"+pair); + } + } + out.println(); + + APElementIterator it = new APElementIterator(dra.apList.size()); + while (it.hasNext()) { + APElement edge = it.next(); + out.println(dra.getEdgeDestByLabel(i_state, edge)); + } + } + } /** * Print automaton to a PrismLog in a specified format ("dot" or "txt"). diff --git a/prism/src/prism/HOAF2DA.java b/prism/src/prism/HOAF2DA.java new file mode 100644 index 00000000..78230c16 --- /dev/null +++ b/prism/src/prism/HOAF2DA.java @@ -0,0 +1,548 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Joachim Klein (TU Dresden) +// * David Mueller (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.ArrayList; +import java.util.BitSet; +import java.util.List; +import java.util.Set; + +import jhoafparser.ast.AtomAcceptance; +import jhoafparser.ast.AtomLabel; +import jhoafparser.ast.BooleanExpression; +import jhoafparser.consumer.HOAConsumer; +import jhoafparser.consumer.HOAConsumerException; +import jhoafparser.util.ImplicitEdgeHelper; +import jltl2ba.APElement; +import jltl2ba.APSet; +import jltl2dstar.APMonom; +import jltl2dstar.APMonom2APElements; +import acceptance.AcceptanceGenRabin; +import acceptance.AcceptanceGenRabin.GenRabinPair; +import acceptance.AcceptanceGeneric; +import acceptance.AcceptanceOmega; +import acceptance.AcceptanceRabin; +import acceptance.AcceptanceRabin.RabinPair; + +/** + * A HOAConsumer for jhoafparser that constructs a prism.DA from the parsed automaton. + */ +public class HOAF2DA implements HOAConsumer { + + public class TransitionBasedAcceptanceException extends HOAConsumerException { + public TransitionBasedAcceptanceException(String e) {super(e);} + } + + private DA da; + private APSet aps = new APSet(); + + /** Size, i.e. number of states */ + private int size; + private boolean knowSize = false; + + /** Start state (index) */ + private int startState; + private boolean knowStartState = false; + + private BooleanExpression accExpr = null; + private String accName; + private List extraInfo; + + private List acceptanceSets = null; + // set of acceptance set indizes where state membership has to be inverted + private Set negateAcceptanceSetMembership = null; + private List apList; + + ImplicitEdgeHelper implicitEdgeHelper = null; + + public void clear() { + aps = new APSet(); + + implicitEdgeHelper = null; + + size = 0; + knowSize = false; + + startState = 0; + knowStartState = false; + + accExpr = null; + accName = null; + extraInfo = null; + + acceptanceSets = null; + negateAcceptanceSetMembership = null; + apList = null; + } + + public HOAF2DA() { + } + + @Override + public boolean parserResolvesAliases() { + return true; + } + + @Override + public void notifyHeaderStart(String version) throws HOAConsumerException { + // NOP + } + + @Override + public void setNumberOfStates(int numberOfStates) + throws HOAConsumerException { + size = numberOfStates; + knowSize = true; + } + + @Override + public void addStartStates(List stateConjunction) + throws HOAConsumerException { + if(stateConjunction.size() > 1 || knowStartState) { + throw new HOAConsumerException("Not a deterministic automaton: More then one Start state"); + } + startState = stateConjunction.get(0).intValue(); + knowStartState = true; + } + + @Override + public void addAlias(String name, BooleanExpression labelExpr) + throws HOAConsumerException { + // NOP, aliases are already resolved + } + + @Override + public void setAPs(List aps) throws HOAConsumerException { + apList = aps; + + for (String ap : aps) { + this.aps.addAP(ap); + } + } + + @Override + public void setAcceptanceCondition(int numberOfSets, + BooleanExpression accExpr) + throws HOAConsumerException { + this.accExpr = accExpr; + } + + @Override + public void provideAcceptanceName(String name, List extraInfo) + throws HOAConsumerException { + accName = name; + this.extraInfo = extraInfo; + } + + @Override + public void setName(String name) throws HOAConsumerException { + // NOP + } + + @Override + public void setTool(String name, String version) throws HOAConsumerException { + // NOP + } + + @Override + public void addProperties(List properties) + throws HOAConsumerException { + if(!properties.contains("deterministic")) { + // we don't know yet whether the automaton is actually deterministic... + } + if(properties.contains("univ-branch")) { + throw new HOAConsumerException("A HOAF with universal branching is not deterministic"); + } + + if(properties.contains("state-labels")) { + throw new HOAConsumerException("Can't handle state labelling"); + } + } + + @Override + public void addMiscHeader(String name, List content) + throws HOAConsumerException { + if (name.substring(0,1).toUpperCase().equals(name.substring(0,1))) { + throw new HOAConsumerException("Unknown header "+name+" potentially containing semantic information, can not handle"); + } + } + + @Override + public void notifyBodyStart() throws HOAConsumerException { + if (!knowSize) { + throw new HOAConsumerException("Can currently only parse automata where the number of states is specified in the header"); + } + if (!knowStartState) { + throw new HOAConsumerException("Not a deterministic automaton: No initial state specified (Start header)"); + } + if (startState >= size) { + throw new HOAConsumerException("Initial state "+startState+" is out of range"); + } + + da = new DA(size); + da.setStartState(startState); + + if (apList == null) { + // no call to setAPs + apList = new ArrayList(0); + } + da.setAPList(apList); + implicitEdgeHelper = new ImplicitEdgeHelper(apList.size()); + + DA.switchAcceptance(da, prepareAcceptance()); + } + + /** + * Prepare an acceptance condition for the parsed automaton. + * Called in notifyBodyStart() + **/ + private AcceptanceOmega prepareAcceptance() throws HOAConsumerException + { + if (accName != null) { + if (accName.equals("Rabin")) { + return prepareAcceptanceRabin(); + } else if (accName.equals("generalized-Rabin")) { + return prepareAcceptanceGenRabin(); + } + } + + acceptanceSets = new ArrayList(); + return prepareAcceptanceGeneric(accExpr); + } + + /** + * Prepare a generic acceptance condition for the parsed automaton. + **/ + private AcceptanceGeneric prepareAcceptanceGeneric(BooleanExpression expr) throws HOAConsumerException + { + switch (expr.getType()) { + case EXP_TRUE: + return new AcceptanceGeneric(true); + case EXP_FALSE: + return new AcceptanceGeneric(false); + case EXP_AND: + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.AND, + prepareAcceptanceGeneric(expr.getLeft()), + prepareAcceptanceGeneric(expr.getRight())); + case EXP_OR: + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.OR, + prepareAcceptanceGeneric(expr.getLeft()), + prepareAcceptanceGeneric(expr.getRight())); + case EXP_NOT: + throw new HOAConsumerException("Boolean negation not allowed in acceptance expression"); + case EXP_ATOM: { + int index = expr.getAtom().getAcceptanceSet(); + while (index >= acceptanceSets.size()) { + // ensure that the acceptanceSets array is large enough + acceptanceSets.add(null); + } + if (acceptanceSets.get(index) == null) { + // this acceptance set index has not been seen yet, create BitSet + acceptanceSets.set(index, new BitSet()); + } + BitSet acceptanceSet = acceptanceSets.get(index); + switch (expr.getAtom().getType()) { + case TEMPORAL_FIN: + if (expr.getAtom().isNegated()) { + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN_NOT, acceptanceSet); + } else { + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.FIN, acceptanceSet); + } + case TEMPORAL_INF: + if (expr.getAtom().isNegated()) { + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF_NOT, acceptanceSet); + } else { + return new AcceptanceGeneric(AcceptanceGeneric.ElementType.INF, acceptanceSet); + } + } + } + } + + throw new UnsupportedOperationException("Unknown operator in acceptance condition: "+expr); + } + + /** + * Prepare a Rabin acceptance condition from the acc-name header. + */ + private AcceptanceRabin prepareAcceptanceRabin() throws HOAConsumerException + { + if (extraInfo.size() != 1 || + !(extraInfo.get(0) instanceof Integer)) { + throw new HOAConsumerException("Invalid acc-name: Rabin header"); + } + + int numberOfPairs = (Integer)extraInfo.get(0); + AcceptanceRabin acceptanceRabin = new AcceptanceRabin(); + acceptanceSets = new ArrayList(numberOfPairs*2); + for (int i = 0; i< numberOfPairs; i++) { + BitSet L = new BitSet(); + BitSet K = new BitSet(); + + acceptanceSets.add(L); // 2*i = Fin(L) = F G !L + acceptanceSets.add(K); // 2*i+1 = Inf(K) = G F K + + acceptanceRabin.add(new RabinPair(L,K)); + } + + return acceptanceRabin; + } + + /** + * Prepare a Generalized Rabin acceptance condition from the acc-name header. + */ + private AcceptanceGenRabin prepareAcceptanceGenRabin() throws HOAConsumerException + { + if (extraInfo.size() < 1 || + !(extraInfo.get(0) instanceof Integer)) { + throw new HOAConsumerException("Invalid acc-name: generalized-Rabin header"); + } + + int numberOfPairs = (Integer)extraInfo.get(0); + if (extraInfo.size() != numberOfPairs + 1) { + throw new HOAConsumerException("Invalid acc-name: generalized-Rabin header"); + } + int numberOfKs[] = new int[numberOfPairs]; + for (int i = 0; i < numberOfPairs; i++) { + if (!(extraInfo.get(i + 1) instanceof Integer)) { + throw new HOAConsumerException("Invalid acc-name: generalized-Rabin header"); + } + numberOfKs[i] = (Integer) extraInfo.get(i + 1); + } + + AcceptanceGenRabin acceptanceGenRabin = new AcceptanceGenRabin(); + acceptanceSets = new ArrayList(numberOfPairs*2); + for (int i = 0; i< numberOfPairs; i++) { + BitSet L = new BitSet(); + acceptanceSets.add(L); // Fin(L) = F G !L + ArrayList K_list = new ArrayList(); + for (int j = 0; j < numberOfKs[i]; j++) { + BitSet K_j = new BitSet(); + K_list.add(K_j); + acceptanceSets.add(K_j); // Inf(K_j) = G F K_j + } + acceptanceGenRabin.add(new GenRabinPair(L, K_list)); + } + + return acceptanceGenRabin; + } + + @Override + public void addState(int id, String info, + BooleanExpression labelExpr, List accSignature) + throws HOAConsumerException { + implicitEdgeHelper.startOfState(id); + + if(labelExpr != null) { + throw new HOAConsumerException("State "+id+" has a state label, currently only supports labels on transitions"); + } + + if (id >= size) { + throw new HOAConsumerException("Illegal state index "+id+", out of range"); + } + + if (accSignature != null) { + for (int index : accSignature) { + if (index >= acceptanceSets.size()) { + // acceptance set index not used in acceptance condition, ignore + } + BitSet accSet = acceptanceSets.get(index); + if (accSet == null) { + // acceptance set index not used in acceptance condition, ignore + } else { + accSet.set(id); + } + } + } + } + + @Override + public void addEdgeImplicit(int stateId, List conjSuccessors, + List accSignature) throws HOAConsumerException { + if (conjSuccessors.size() != 1) { + throw new HOAConsumerException("Not a DA, state "+stateId+" has transition with conjunctive target"); + } + + if (accSignature != null) { + throw new TransitionBasedAcceptanceException("DA has transition-based acceptance (state "+stateId+", currently only state-labeled acceptance is supported"); + } + + int to = conjSuccessors.get(0); + + BitSet edge = new BitSet(); + long tmp = implicitEdgeHelper.nextImplicitEdge(); + int index = 0; + while (tmp != 0) { + if (tmp % 2 == 1) { + edge.set(index); + } + tmp = tmp >> 1L; + index++; + } + da.addEdge(stateId, edge, to); + } + + /** + * Returns a list of APMonoms for the expression. The expression currently has to be in + * disjunctive normal form. Returns one APMonom for each clause of the DNF. + */ + private List labelExpressionToAPMonom(BooleanExpression expr) throws HOAConsumerException { + List result = new ArrayList(); + + switch (expr.getType()) { + case EXP_AND: + case EXP_ATOM: + case EXP_NOT: { + APMonom monom = new APMonom(); + labelExpressionToAPMonom(expr, monom); + result.add(monom); + return result; + } + case EXP_TRUE: + result.add(new APMonom(true)); + return result; + case EXP_FALSE: + result.add(new APMonom(false)); + case EXP_OR: + result.addAll(labelExpressionToAPMonom(expr.getLeft())); + result.addAll(labelExpressionToAPMonom(expr.getRight())); + return result; + } + throw new UnsupportedOperationException("Unsupported operator in label expression: "+expr); + } + + + /** + * Returns a single APMonom for a single clause of the overall DNF formula. + * Modifies APMonom result such that in the end it is correct. + */ + private void labelExpressionToAPMonom(BooleanExpression expr, APMonom result) throws HOAConsumerException { + try { + switch (expr.getType()) { + case EXP_TRUE: + case EXP_FALSE: + case EXP_OR: + throw new HOAConsumerException("Complex transition labels are not yet supported, only disjunctive normal form: "+expr); + + case EXP_AND: + labelExpressionToAPMonom(expr.getLeft(), result); + labelExpressionToAPMonom(expr.getRight(), result); + return; + case EXP_ATOM: { + int apIndex = expr.getAtom().getAPIndex(); + if (result.isSet(apIndex) && result.getValue(apIndex)!=true) { + throw new HOAConsumerException("Complex transition labels are not yet supported, transition label evaluates to false"); + } + result.setValue(apIndex, true); + return; + } + case EXP_NOT: { + if (!expr.getLeft().isAtom()) { + throw new HOAConsumerException("Complex transition labels are not yet supported, only conjunction of (negated) labels"); + } + int apIndex = expr.getLeft().getAtom().getAPIndex(); + if (result.isSet(apIndex) && result.getValue(apIndex)!=false) { + throw new HOAConsumerException("Complex transition labels are not yet supported, transition label evaluates to false"); + } + result.setValue(apIndex, false); + return; + } + } + } catch (PrismException e) { + throw new HOAConsumerException("While parsing, APMonom exception: "+e.getMessage()); + } + } + + @Override + public void addEdgeWithLabel(int stateId, + BooleanExpression labelExpr, + List conjSuccessors, List accSignature) + throws HOAConsumerException { + + if (conjSuccessors.size() != 1) { + throw new HOAConsumerException("Not a DA, state "+stateId+" has transition with conjunctive target"); + } + + if (accSignature != null) { + throw new TransitionBasedAcceptanceException("DA has transition-based acceptance (state "+stateId+", currently only state-labeled acceptance is supported"); + } + + if (labelExpr == null) { + throw new HOAConsumerException("Missing label on transition"); + } + + int to = conjSuccessors.get(0); + + for (APMonom monom : labelExpressionToAPMonom(labelExpr)) { + APMonom2APElements it = new APMonom2APElements(aps, monom); + while(it.hasNext()) { + APElement el = it.next(); + if (da.hasEdge(stateId, el)) { + throw new HOAConsumerException("Not a deterministic automaton, non-determinism detected (state "+stateId+")"); + } + da.addEdge(stateId, el, to); + } + } + } + + @Override + public void notifyEndOfState(int stateId) throws HOAConsumerException + { + implicitEdgeHelper.endOfState(); + } + + @Override + public void notifyEnd() throws HOAConsumerException { + // flip acceptance sets that need negating + if (negateAcceptanceSetMembership != null) { + for (int index : negateAcceptanceSetMembership) { + acceptanceSets.get(index).flip(0, size); + } + } + + clear(); + } + + @Override + public void notifyAbort() { + clear(); + + } + + public DA getDA() { + return da; + } + + @Override + public void notifyWarning(String warning) throws HOAConsumerException + { + // warnings are fatal + throw new HOAConsumerException(warning); + } + +} diff --git a/prism/src/prism/LTL2DA.java b/prism/src/prism/LTL2DA.java index 11680d4f..b980fca6 100644 --- a/prism/src/prism/LTL2DA.java +++ b/prism/src/prism/LTL2DA.java @@ -27,11 +27,24 @@ package prism; +import java.io.File; +import java.io.FileInputStream; +import java.io.FileWriter; +import java.io.IOException; +import java.io.InputStream; +import java.util.ArrayList; import java.util.BitSet; +import java.util.List; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; import acceptance.AcceptanceType; +import jhoafparser.consumer.HOAIntermediateStoreAndManipulate; +import jhoafparser.parser.HOAFParser; +import jhoafparser.parser.generated.ParseException; +import jhoafparser.transformations.ToStateAcceptance; +import jltl2ba.APSet; +import jltl2ba.SimpleLTL; import jltl2dstar.LTL2Rabin; import parser.Values; import parser.ast.Expression; @@ -70,7 +83,15 @@ public class LTL2DA extends PrismComponent public DA convertLTLFormulaToDA(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException { DA result = null; - if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) { + + boolean useExternal = useExternal(); + boolean containsTemporalBounds = Expression.containsTemporalTimeBounds(ltl); + if (containsTemporalBounds) { + useExternal = false; + } + + if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN) && + !useExternal) { // If we may construct a Rabin automaton, check the library first try { result = LTL2RabinLibrary.getDRAforLTL(ltl, constants); @@ -84,9 +105,13 @@ public class LTL2DA extends PrismComponent } // 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 && !containsTemporalBounds) { + if (useExternal) { + result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance); + } else { + // use jltl2dstar LTL2DA + result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance); + } } if (result == null) { @@ -97,4 +122,186 @@ public class LTL2DA extends PrismComponent return result; } + + public DA convertLTLFormulaToDAWithExternalTool(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException + { + String ltl2daTool = getSettings().getString(PrismSettings.PRISM_LTL2DA_TOOL); + + SimpleLTL ltlFormula = ltl.convertForJltl2ba(); + + // switch from the L0, L1, ... APs of PRISM to the + // safer p0, p1, ... APs for the external tool + SimpleLTL ltlFormulaSafeAP = ltlFormula.clone(); + ltlFormulaSafeAP.renameAP("L", "p"); + + DA result = null; + + try { + + String syntax = getSettings().getString(PrismSettings.PRISM_LTL2DA_SYNTAX); + if (syntax == null || syntax.isEmpty()) { + throw new PrismException("No LTL syntax option provided"); + } + String ltlOutput; + switch (syntax) { + case "LBT": + ltlOutput = ltlFormulaSafeAP.toStringLBT(); + break; + case "Spin": + ltlOutput = ltlFormulaSafeAP.toStringSpin(); + break; + case "Spot": + ltlOutput = ltlFormulaSafeAP.toStringSpot(); + break; + case "Rabinizer": + ltlFormulaSafeAP = ltlFormulaSafeAP.toBasicOperators(); + ltlOutput = ltlFormulaSafeAP.toStringSpot(); + break; + default: + throw new PrismException("Unknown LTL syntax option \""+syntax+"\""); + } + + File ltl_file=File.createTempFile("prism-ltl-external-", ".ltl", null); + File da_file=File.createTempFile("prism-ltl-external-",".hoa", null); + File tool_output=File.createTempFile("prism-ltl-external-",".output", null); + + FileWriter ltlWriter = new FileWriter(ltl_file); + ltlWriter.write(ltlOutput); + ltlWriter.close(); + + List arguments = new ArrayList(); + arguments.add(ltl2daTool); + + getLog().print("Calling external LTL->DA tool: "); + for (String s : arguments) { + getLog().print(" " + s); + } + getLog().println(); + + getLog().print("LTL formula (in "+syntax+" syntax): "); + getLog().println(ltlOutput); + getLog().println(); + + arguments.add(ltl_file.getAbsolutePath()); + arguments.add(da_file.getAbsolutePath()); + + + ProcessBuilder builder = new ProcessBuilder(arguments); + builder.redirectOutput(tool_output); + builder.redirectErrorStream(true); + + Process p = builder.start(); + p.getInputStream().close(); + + int rv; + while (true) { + try { + rv = p.waitFor(); + break; + } catch (InterruptedException e) { + } + } + if (rv != 0) { + throw new PrismException("Call to external LTL->DA tool failed, return value = "+rv+".\n" + +"To investigate, please consult the following files:" + +"\n LTL formula: "+ltl_file.getAbsolutePath() + +"\n Automaton output: "+da_file.getAbsolutePath() + +"\n Tool output (stdout and stderr): "+tool_output.getAbsolutePath() + +"\n"); + } + + tool_output.delete(); + + + try { + try { + HOAF2DA consumerDA = new HOAF2DA(); + + InputStream input = new FileInputStream(da_file); + HOAFParser.parseHOA(input, consumerDA); + result = consumerDA.getDA(); + } catch (HOAF2DA.TransitionBasedAcceptanceException e) { + // try again, this time transforming to state acceptance + getLog().println("Automaton with transition-based acceptance, automatically converting to state-based acceptance..."); + HOAF2DA consumerDA = new HOAF2DA(); + HOAIntermediateStoreAndManipulate consumerTransform = new HOAIntermediateStoreAndManipulate(consumerDA, new ToStateAcceptance()); + + InputStream input = new FileInputStream(da_file); + HOAFParser.parseHOA(input, consumerTransform); + result = consumerDA.getDA(); + } + + if (result == null) { + throw new PrismException("Could not construct DA"); + } + checkAPs(ltlFormulaSafeAP, result.getAPList()); + + // rename back from safe APs, i.e., p0, p1, ... to L0, L1, ... + List automatonAPList = result.getAPList(); + for (int i = 0; i < automatonAPList.size(); i++) { + if (automatonAPList.get(i).startsWith("p")) { + String renamed = "L" + automatonAPList.get(i).substring("p".length()); + automatonAPList.set(i, renamed); + } + } + } catch (ParseException e) { + throw new PrismException("Parse error: "+e.getMessage()+".\n" + +"To investigate, please consult the following files:\n" + +" LTL formula: "+ltl_file.getAbsolutePath() + +"\n Automaton output: "+da_file.getAbsolutePath() + +"\n"); + } catch (PrismException e) { + throw new PrismException(e.getMessage()+".\n" + +"To investigate, please consult the following files:" + +"\n LTL formula: " +ltl_file.getAbsolutePath() + +"\n Automaton output: "+da_file.getAbsolutePath() + +"\n"); + } + + da_file.delete(); + ltl_file.delete(); + } catch (IOException e) { + throw new PrismException(e.getMessage()); + } + + AcceptanceOmega acceptance = result.getAcceptance(); + if (AcceptanceType.contains(allowedAcceptance, acceptance.getType())) { + return result; + } else if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) { + // The specific acceptance type is not allowed, but GENERIC is allowed + // -> transform to generic acceptance and switch acceptance condition + DA.switchAcceptance(result, acceptance.toAcceptanceGeneric()); + return result; + } else { + throw new PrismException("The external LTL->DA tool returned an automaton with "+acceptance.getTypeName()+" acceptance, which is not yet supported for model checking this model / property"); + } + } + + /** Check whether we should use an external LTL->DA tool */ + private boolean useExternal() + { + String ltl2da_tool = getSettings().getString(PrismSettings.PRISM_LTL2DA_TOOL); + if (ltl2da_tool!=null && !ltl2da_tool.isEmpty()) { + return true; + } + return false; + } + + 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+"\""); + } + } + } + + + } diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 2b3e0e9d..0f58c6bb 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -32,6 +32,7 @@ import java.util.BitSet; import java.util.List; import java.util.Vector; +import acceptance.AcceptanceGenRabinDD; import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; @@ -708,6 +709,8 @@ public class LTLModelChecker extends PrismComponent switch (acceptance.getType()) { case RABIN: return findAcceptingECStatesForRabin((AcceptanceRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness); + case GENERALIZED_RABIN: + return findAcceptingECStatesForGeneralizedRabin((AcceptanceGenRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness); default: throw new PrismNotSupportedException("Computing the accepting EC states for "+acceptance.getTypeName()+" acceptance is not yet implemented (symbolic engine)"); } @@ -852,6 +855,61 @@ public class LTLModelChecker extends PrismComponent return allAcceptingStates; } + /** + * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Generalized Rabin acceptance condition. + * @param acceptance the Generalized Rabin acceptance condition + * @param model The model + * @param draDDRowVars BDD row variables for the DRA part of the model + * @param draDDColVars BDD column variables for the DRA part of the model + * @param fairness Consider fairness? + * @return A referenced BDD for the union of all states in accepting MECs + */ + public JDDNode findAcceptingECStatesForGeneralizedRabin(AcceptanceGenRabinDD acceptance, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) + throws PrismException + { + + if (fairness) { + throw new PrismException("Accepting end-component computation for generalized Rabin is currently not supported with fairness"); + } + + JDDNode allAcceptingStates; + + allAcceptingStates = JDD.Constant(0); + + // Go through the GR acceptance pairs (L_i, K_i_1, ..., K_i_n) + for (int i = 0; i < acceptance.size(); i++) { + + // Filter out L_i states from the model and find the MECs + JDDNode notL = JDD.Not(acceptance.get(i).getL()); + JDD.Ref(model.getTrans01()); + JDD.Ref(notL); + JDDNode candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), notL); + notL = JDD.PermuteVariables(notL, draDDRowVars, draDDColVars); + candidateStates = JDD.Apply(JDD.TIMES, candidateStates, notL); + candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars()); + candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars()); + List mecs = findMECStates(model, candidateStates); + JDD.Deref(candidateStates); + + // Check which MECs are accepting for this pair, calculate union + JDDNode acceptingStates = JDD.Constant(0); + for (int k = 0; k < mecs.size(); k++) { + // Is the induced BSCC by this MEC accepting? + // (note we only really need to check K_i_1, ..., K_i_n here, not L too, + // but this should not really affect efficiency) + if (acceptance.get(i).isBSCCAccepting(mecs.get(k))) { + acceptingStates = JDD.Or(acceptingStates, mecs.get(k)); + } else { + JDD.Deref(mecs.get(k)); + } + } + // Add to the set of accepting states for all pairs + allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates); + } + + return allAcceptingStates; + } + public JDDNode findMultiAcceptingStates(DA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness, List allecs, List statesH, List statesL) throws PrismException { diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 594337ea..fce4a4ad 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1007,6 +1007,7 @@ public class NondetModelChecker extends NonProbModelChecker LTL2DA ltl2da = new LTL2DA(prism); AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, + AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH }; da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index b8ccc7ba..618ce634 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -113,6 +113,9 @@ public class PrismSettings implements Observer public static final String PRISM_PARETO_EPSILON = "prism.paretoEpsilon"; public static final String PRISM_EXPORT_PARETO_FILENAME = "prism.exportParetoFileName"; + public static final String PRISM_LTL2DA_TOOL = "prism.ltl2daTool"; + public static final String PRISM_LTL2DA_SYNTAX = "prism.ltl2daSyntax"; + public static final String PRISM_PARAM_ENABLED = "prism.param.enabled"; public static final String PRISM_PARAM_PRECISION = "prism.param.precision"; public static final String PRISM_PARAM_SPLIT = "prism.param.split"; @@ -304,6 +307,13 @@ public class PrismSettings implements Observer { STRING_TYPE, PRISM_EXPORT_ADV_FILENAME, "Adversary export filename", "3.3", "adv.tra", "", "Name of file for MDP adversary export (if enabled)" }, + // LTL2DA TOOLS + { STRING_TYPE, PRISM_LTL2DA_TOOL, "Use external LTL->DA tool", "4.2.1", "", null, + "If non-empty, the path to the executable for the external LTL->DA tool."}, + + { STRING_TYPE, PRISM_LTL2DA_SYNTAX, "LTL syntax for external LTL->DA tool", "4.2.1", "LBT", "LBT,Spin,Spot,Rabinizer", + "The syntax for LTL formulas passed to the external LTL->DA tool."}, + // PARAMETRIC MODEL CHECKING { BOOLEAN_TYPE, PRISM_PARAM_ENABLED, "Do parametric model checking", "4.1", new Boolean(false), "", "Perform parametric model checking." }, @@ -1265,6 +1275,40 @@ public class PrismSettings implements Observer } } + // LTL2DA TOOLS + + else if (sw.equals("ltl2datool")) { + if (i < args.length - 1) { + String filename = args[++i]; + set(PRISM_LTL2DA_TOOL, filename); + System.out.println(getString(PRISM_LTL2DA_TOOL)); + } else { + throw new PrismException("The -" + sw + " switch requires one argument (path to the executable)"); + } + } + else if (sw.equals("ltl2dasyntax")) { + if (i < args.length - 1) { + String syntax = args[++i]; + switch (syntax) { + case "lbt": + set(PRISM_LTL2DA_SYNTAX, "LBT"); + break; + case "spin": + set(PRISM_LTL2DA_SYNTAX, "Spin"); + break; + case "spot": + set(PRISM_LTL2DA_SYNTAX, "Spot"); + case "rabinizer": + set(PRISM_LTL2DA_SYNTAX, "Rabinizer"); + break; + default: + throw new PrismException("Unrecognised option for -" + sw + " switch (options are: lbt, spin, spot, rabinizer)"); + } + } else { + throw new PrismException("The -" + sw + " switch requires one argument (options are: lbt, spin, spot, rabinizer)"); + } + } + // PARAMETRIC MODEL CHECKING: else if (sw.equals("param")) { @@ -1567,6 +1611,9 @@ public class PrismSettings implements Observer mainLog.println("-pathviaautomata ............... Handle all path formulas via automata constructions"); mainLog.println("-exportadv .............. Export an adversary from MDP model checking (as a DTMC)"); mainLog.println("-exportadvmdp ........... Export an adversary from MDP model checking (as an MDP)"); + mainLog.println("-ltl2datool ............. Run executable to convert LTL formulas to deterministic automata"); + mainLog.println("-ltl2dasyntax .............. Specify output format for -ltl2datool switch (lbt, spin, spot, rabinizer)"); + mainLog.println(); mainLog.println("MULTI-OBJECTIVE MODEL CHECKING:"); mainLog.println("-linprog (or -lp) .............. Use linear programming for multi-objective model checking"); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 8224a6ef..8f3601d0 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -541,7 +541,8 @@ public class ProbModelChecker extends NonProbModelChecker LTL2DA ltl2da = new LTL2DA(prism); AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, - AcceptanceType.REACH + AcceptanceType.REACH, + AcceptanceType.GENERIC }; da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance); mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + ".");