diff --git a/prism/src/automata/LTL2WDBA.java b/prism/src/automata/LTL2WDBA.java new file mode 100644 index 00000000..8290a9ec --- /dev/null +++ b/prism/src/automata/LTL2WDBA.java @@ -0,0 +1,604 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * 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 automata; + +import java.io.PrintStream; +import java.util.ArrayList; +import java.util.BitSet; +import java.util.HashMap; +import java.util.LinkedList; +import java.util.Queue; +import java.util.Stack; + +import jltl2ba.APElement; +import jltl2ba.LTLFragments; +import jltl2ba.MyBitSet; +import jltl2ba.SimpleLTL; +import jltl2dstar.NBA; +import prism.PrismComponent; +import prism.PrismDevNullLog; +import prism.PrismException; +import acceptance.AcceptanceBuchi; +import acceptance.AcceptanceOmega; +import acceptance.AcceptanceReach; + +import common.IterableBitSet; + +import explicit.LTS; +import explicit.LTSExplicit; +import explicit.NonProbModelChecker; +import explicit.SCCComputer; + +/** + *

+ * Construction of weak Deterministic Büchi Automata for + * a fragment of LTL, based on the algorithm presented in + * Christian Dax, Jochen Eisinger, Felix Klaedtke: + * + * "Mechanizing the Powerset Construction for Restricted + * Classes of omega-Automata", + * ATVA 2007, LNCS 4762. + *

+ *

+ * The approach works as follows: First, we construct a + * DBA via a standard power set construction of the NBA + * for the LTL formula. Then, for the suitable fragment of LTL, + * it is guaranteed that either all states in a SCC in the DA + * can be made accepting or all can be made non-accepting (the + * "weakness" property of the DBA). + *

+ *

+ * Using the algorithm described in + * Christof Löding: + * + * "Efficient minimization of deterministic weak omega-automata", + * Inf. Process. Lett. 79(3), 2001, + * it is then possible to obtain a minimal automaton for the language + * via a DFA-based minimisation. + *

+ *

+ * This minimisation step is not yet included, but will + * be added in the future. Currently, we are using this + * construction to obtain DAs with AcceptanceReach that + * are suitable for the model checking of co-safety rewards. + * For further details, see Sec. 4 of + * Joachim Klein et al: + * + * "Advances in probabilistic model checking with PRISM: + * variable reordering, quantiles and weak deterministic + * Büchi automata", International Journal on Software + * Tools for Technology Transfer, 2017. + *

+ *

TODO: Optimise for performance

+ */ +public class LTL2WDBA extends PrismComponent +{ + /** Constructor */ + public LTL2WDBA(PrismComponent parent) + { + super(parent); + } + + /** + * For a co-safe LTL formula, construct a DFA (i.e., a DA with AcceptanceReach) + * with the additional property that every state that accepts the full language + * is accepting, i.e., that state s in F iff s |= Sigma^omega. + *
+ * Note: Does not check if the formula is actually syntactically cosafe, it is the responsibility + * of the caller to ensure that the formula corresponds to a cosafe language. + * @param ltl the ltl formula, has to + * @return a DA with AcceptanceReach + */ + public DA cosafeltl2dfa(SimpleLTL ltl) throws PrismException + { + // construct DBA using the powerset-based construction + DA wdba = ltl2wdba(ltl); + + BitSet F = wdba.getAcceptance().getAcceptingStates(); + BitSet notF = (BitSet) F.clone(); + notF.flip(0, wdba.size()); + + // Now, to satisfy that s in F iff s |= Sigma^omega, we determine + // the set of states that can not avoid reaching an F state, as + // those are the states that will accept any word + LTS lts = new LTSFromDA(wdba); + NonProbModelChecker ctlMC = new NonProbModelChecker(this); + ctlMC.setLog(new PrismDevNullLog()); // quietly + BitSet canAvoidF = ctlMC.computeExistsGlobally(lts, notF); + BitSet canNotAvoidF = (BitSet)canAvoidF.clone(); + canNotAvoidF.flip(0, wdba.size()); + + // As the result, we construct the DFA on the transition structure + // of the wdba, with goal states = canNotAvoidF + DA dfa = toDFA(wdba, canNotAvoidF); + //dfa.printDot(System.out); + return dfa; + } + + /** + * For an LTL formula in the obligation fragment, return a WDBA. + * @param ltl the LTL formula + * @return a weak deterministic Büchi automaton + */ + public DA obligation2wdba(SimpleLTL ltl) throws PrismException + { + return ltl2wdba(ltl); + } + + /** + * Generate DFA (i.e., DA with AcceptanceReach) with the underlying transition + * structure of {@code da}. The set of goal states should be upward closed, + * i.e., once a goal state has been reached, all successor states should + * be goal states as well. + *
+ * Note: {@code da} is destroyed during the transformation + * and should not be used afterwards. + * @param da the DA + * @param goalStates the set of goalStates for the DFA. + * @return + */ + @SuppressWarnings("unchecked") + private DA toDFA(DA da, BitSet goalStates) + { + AcceptanceReach reach = new AcceptanceReach(goalStates); + DA.switchAcceptance(da, reach); + return (DA) da; + } + + /** + * Perform the power set construction as described in + * "Mechanizing the Powerset Construction for Restricted Classes of omega-Automata", + * and determine whether the SCCs of the resulting automaton should be accepting + * or non-accepting. + *
+ * The resulting WDBA is only equivalent to the language of the LTL formula + * if the language of the LTL formula is WDBA-realizable. + * @param ltl the LTL formula. + * @return a weak deterministich Büchi automaton. + */ + private DA ltl2wdba(SimpleLTL ltl) throws PrismException + { + ltl = ltl.simplify(); + + NBA nba = ltl.toNBA(); + PowersetDA P = powersetConstruction(nba); + determineF(P); + + return P.da; + } + + /** + * Storage for a DA resulting from the powerset + * construction on an NBA; + */ + private static class PowersetDA + { + /** The original NBA */ + public NBA nba; + + /** The DBA */ + public DA da; + + /** + * The set of states in the DBA where at least + * one of the corresponding NBA states is accepting. + */ + public MyBitSet powersetOneF; + + /** + * The set of states in the DBA where all + * of the corresponding NBA states are accepting. + */ + public MyBitSet powersetAllF; + + /** Mapping DBA state index to the set of NBA states */ + public ArrayList idToState; + + /** The accepting states of the DBA */ + public BitSet F = new BitSet(); + } + + /** Perform powerset construction on the NBA */ + private PowersetDA powersetConstruction(NBA nba) throws PrismException + { + //System.out.println("--- NBA ---"); + //nba.print_hoa(System.out); + DA da = new DA(); + da.setAcceptance(new AcceptanceBuchi()); + + HashMap stateToId = new HashMap(); + ArrayList idToState = new ArrayList(); + + MyBitSet nbaF = nba.getFinalStates(); + MyBitSet powersetOneF = new MyBitSet(); + MyBitSet powersetAllF = new MyBitSet(); + + Queue todo = new LinkedList(); + BitSet initialState = new BitSet(); + initialState.set(nba.getStartState().getName()); + int initialId = da.addState(); + stateToId.put(initialState, initialId); + idToState.add(initialState); + todo.add(initialId); + da.setStartState(initialId); + da.setAPList(new ArrayList(nba.getAPSet().asList())); + + if (initialState.intersects(nbaF)) { + powersetOneF.set(initialId); + } + if (nbaF.containsAll(initialState)) { + powersetAllF.set(initialId); + } + + //System.out.println("new: "+initialId+" "+initialState); + + BitSet visited = new BitSet(); + while (!todo.isEmpty()) { + int curId = todo.poll(); + if (visited.get(curId)) continue; + + BitSet cur = idToState.get(curId); + //System.out.println("Expand "+curId+" "+cur); + + for (APElement e : nba.getAPSet().elements()) { + BitSet to = new BitSet(); + for (int f : IterableBitSet.getSetBits(cur)) { + to.or(nba.get(f).getEdge(e)); + } + + Integer toId = stateToId.get(to); + if (toId == null) { + toId = da.addState(); + stateToId.put(to, toId); + idToState.add(to); + todo.add(toId); + + //System.out.println("new: "+toId+" "+to); + + if (to.intersects(nbaF)) { + powersetOneF.set(toId); + } + if (nbaF.containsAll(to)) { + powersetAllF.set(toId); + } + } + + //System.out.println(" delta(" + curId + ", " + e + ") = " + toId); + da.addEdge(curId, e, toId); + } + } + + //da.printHOA(System.out); + + PowersetDA result = new PowersetDA(); + result.nba = nba; + result.da = da; + result.idToState = idToState; + result.powersetOneF = powersetOneF; + result.powersetAllF = powersetAllF; + //System.out.println("powersetOneF = "+powersetOneF); + //System.out.println("powersetAllF = "+powersetAllF); + + return result; + } + + /** + * Analyse the SCCs of the DA obtained by the power set construction, + * whether they should be accepting or rejecting. + * @param P the DA + */ + private void determineF(final PowersetDA P) throws PrismException + { + LTS daLTS = new LTSFromDA(P.da); + + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, daLTS); + sccComputer.computeSCCs(); + for (BitSet scc : sccComputer.getSCCs()) { + if (hasAcceptingCycle(P, scc)) { + // mark all SCC states as final in powerset automaton + P.F.or(scc); + } + } + + // construct acceptance + P.da.getAcceptance().setAcceptingStates(P.F); + } + + /** + * Check whether the given SCC of the DBA has an accepting cycle + * in the underlying NBA. + * @param P the powerset DBA + * @param scc an SCC of P + */ + private boolean hasAcceptingCycle(PowersetDA P, BitSet scc) throws PrismException + { + //System.out.println("hasAcceptingCycle "+scc+"?"); + if (!scc.intersects(P.powersetOneF)) { + // none of the NBA states in this powerset SCC are final + //System.out.println(" -> no (none final)"); + return false; + } + if (P.powersetAllF.containsAll(scc)) { + // all NBA states in this powerset SCC are final + //System.out.println(" -> yes (all final)"); + return true; + } + + // first, construct an arbitrary lasso in P, remaining + // in the SCC + Lasso lasso = findLasso(P, scc); + //System.out.println(cycle); + + // second, construct the NBA fragment corresponding to the + // lasso + final BuchiLTS buchilts = buildLTSforLasso(P, lasso); + // String name = "lts"+scc+".dot"; + // buchilts.lts.exportToDotFile(name, p.F); + //System.out.println("DOT: "+name); + + // perform cycle check + // TODO: use nested-DFS? + boolean hasCycleViaF = false; + SCCComputer sccComputer = SCCComputer.createSCCComputer(this, buchilts.lts); + sccComputer.computeSCCs(); + for (BitSet subSCC : sccComputer.getSCCs()) { + if (subSCC.intersects(buchilts.F)) { + hasCycleViaF = true; + break; + } + } + + //System.out.println(hasCycleViaF ? " -> yes" : " -> no"); + return hasCycleViaF; + } + + /** A lasso, i.e., an infinite word uw^omega */ + private static class Lasso { + LinkedList word; + /** start of the w fragment */ + int cycleStart; + + public String toString() + { + String s = "Cycle starting at "+cycleStart+" with "; + s+= word.toString(); + return s; + } + } + + /** Construct an arbitrary lasso inside the SCC of the DA */ + private Lasso findLasso(PowersetDA P, BitSet scc) throws PrismException + { + // pick a start state + int R = scc.nextSetBit(0); + + Stack states = new Stack(); + Stack letters = new Stack(); + BitSet onStack = new BitSet(); + + states.push(R); + onStack.set(R); + + final DA da = P.da; + + while (true) { + int cur = states.peek(); + // find first letter that allows remaining in SCC + int n = da.getNumEdges(cur); + boolean found = false; + int to = -1; + for (int i=0; i(); + cycle.cycleStart = cycleStart; + + do { + APElement label = new APElement(); + label.or(letters.pop()); + cycle.word.addFirst(label); + states.pop(); + } while (states.peek() != to); + + return cycle; + } + } + + private static class LassoLTSState + { + int nbaState; + int cyclePos; + + LassoLTSState(int nbaState, int cyclePos) + { + this.nbaState = nbaState; + this.cyclePos = cyclePos; + } + + public String toString() + { + return "("+nbaState+","+cyclePos+")"; + } + + @Override + public int hashCode() + { + final int prime = 31; + int result = 1; + result = prime * result + cyclePos; + result = prime * result + nbaState; + return result; + } + + @Override + public boolean equals(Object obj) + { + if (this == obj) + return true; + if (obj == null) + return false; + LassoLTSState other = (LassoLTSState) obj; + if (cyclePos != other.cyclePos) + return false; + if (nbaState != other.nbaState) + return false; + return true; + } + } + + private static class BuchiLTS + { + LTS lts; + BitSet F; + } + + /** Build an LTS for the NBA fragment corresponding to the lasso in the DBA. */ + private BuchiLTS buildLTSforLasso(PowersetDA p, Lasso lasso) + { + HashMap stateToIndex = new HashMap(); + ArrayList indexToState = new ArrayList(); + + Stack todo = new Stack(); + BitSet expanded = new BitSet(); + BitSet F = new BitSet(); + + LTSExplicit lts = new LTSExplicit(); + + for (int startNBA : IterableBitSet.getSetBits(p.idToState.get(lasso.cycleStart))) { + int i = lts.addState(); + todo.push(i); + LassoLTSState s = new LassoLTSState(startNBA, 0); + stateToIndex.put(s, i); + indexToState.add(s); + if (p.nba.get(startNBA).isFinal()) { + F.set(i); + } + + //System.out.println("new: " + i + " = "+ s); + } + + while (!todo.isEmpty()) { + int curProd = todo.pop(); + if (expanded.get(curProd)) continue; + + LassoLTSState cur = indexToState.get(curProd); + // expand + //System.out.println("Expand "+curProd+" = "+cur); + APElement letter = lasso.word.get(cur.cyclePos); + MyBitSet toSet = p.nba.get(cur.nbaState).getEdge(letter); + int cyclePos = (cur.cyclePos+1) % lasso.word.size(); + + for (int to : toSet) { + LassoLTSState toProd = new LassoLTSState(to, cyclePos); + Integer prodTo = stateToIndex.get(toProd); + if (prodTo == null) { + prodTo = lts.addState(); + todo.push(prodTo); + stateToIndex.put(toProd, prodTo); + indexToState.add(toProd); + + if (p.nba.get(to).isFinal()) { + F.set(prodTo); + } + + //System.out.println("new: " + prodTo + " = " +toProd); + } + + lts.addEdge(curProd, prodTo); + //System.out.println(" " + curProd +" -> " +prodTo); + } + } + + BuchiLTS result = new BuchiLTS(); + result.lts = lts; + result.F = F; + return result; + } + + + /** + * Simple test method: convert LTL formula (in LBT format) to HOA/Dot/txt + */ + public static void main(String args[]) + { + try { + // Usage: + // * ... 'X p1' + // * ... 'X p1' da.hoa + // * ... 'X p1' da.hoa hoa + // * ... 'X p1' da.dot dot + // * ... 'X p1' - hoa + // * ... 'X p1' - txt + + // Convert to Expression (from LBT format) + SimpleLTL sltl = SimpleLTL.parseFormulaLBT(args[0]); + + // Build/export DA + PrismComponent parent = new PrismComponent(); + parent.setLog(new PrismDevNullLog()); + LTL2WDBA ltl2wdba = new LTL2WDBA(parent); + LTLFragments tl = LTLFragments.analyse(sltl); + + DA da; + if (tl.isSyntacticGuarantee()) { + da = ltl2wdba.cosafeltl2dfa(sltl); + } else if (tl.isSyntacticObligation()) { + da = ltl2wdba.obligation2wdba(sltl); + } else { + throw new Exception("Can not construct an automaton for " + sltl +", not syntactically co-safe or obligation"); + } + PrintStream out = (args.length < 2 || "-".equals(args[1])) ? System.out : new PrintStream(args[1]); + String format = (args.length < 3) ? "hoa" : args[2]; + da.print(out, format); + + } catch (Exception e) { + e.printStackTrace(); + System.err.println("Error: " + e + "."); + } + } +}