diff --git a/prism/src/jltl2dstar/DA.java b/prism/src/jltl2dstar/DA.java index 981fd659..31f30540 100644 --- a/prism/src/jltl2dstar/DA.java +++ b/prism/src/jltl2dstar/DA.java @@ -3,6 +3,7 @@ * (http://www.ltl2dstar.de/) for PRISM (http://www.prismmodelchecker.org/) * Copyright (C) 2005-2007 Joachim Klein * Copyright (c) 2007 Carlos Bederian + * Copyright (c) 2011- Hongyang Qu * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License version 2 as @@ -294,4 +295,57 @@ public class DA { } } } + + /** + * Print the DA in dot format to the output stream. + * This functions expects that the DA is compact. + * @param da_type a string specifying the type of automaton ("DRA", "DSA"). + * @param out the output stream + * + * @author Hongyang Qu + */ + public void printDot(String da_type, PrintStream out) throws PrismException { + // Ensure that this DA is compact... + if (!this.isCompact()) { + throw new PrismException("DA is not compact!"); + } + + if (this.getStartState() == null) { + // No start state! + throw new PrismException("No start state in DA!"); + } + + int start_state = this.getStartState().getName(); + + out.println("digraph model {"); + for (int i_state = 0; i_state < _index.size(); i_state++) { + if(i_state == start_state) + out.println(" " + i_state + " [label=\"" + i_state + "\", shape=ellipse]"); + else { + boolean isAcceptance = false; + for (int ap_i = 0; ap_i < _acceptance.size(); ap_i++) { + if(_acceptance.isStateInAcceptance_L(ap_i, i_state)) { + out.println(" " + i_state + " [label=\"" + i_state + "\", shape=doublecircle]"); + isAcceptance = true; + break; + } else if(_acceptance.isStateInAcceptance_U(ap_i, i_state)) { + out.println(" " + i_state + " [label=\"" + i_state + "\", shape=box]"); + isAcceptance = true; + break; + } + } + if(!isAcceptance) + out.println(" " + i_state + " [label=\"" + i_state + "\", shape=circle]"); + } + } + for (int i_state = 0; i_state < _index.size(); i_state++) { + DA_State cur_state = _index.get(i_state); + for (Map.Entry transition : cur_state.edges().entrySet()) { + out.println(" " + i_state + " -> " + transition.getValue().getName() + + " [label=\"" + transition.getKey().toString(_ap_set, true) + "\"]"); + } + } + out.println("}"); + + } } diff --git a/prism/src/jltl2dstar/DRA.java b/prism/src/jltl2dstar/DRA.java index e67935a8..371711f6 100644 --- a/prism/src/jltl2dstar/DRA.java +++ b/prism/src/jltl2dstar/DRA.java @@ -3,6 +3,7 @@ * (http://www.ltl2dstar.de/) for PRISM (http://www.prismmodelchecker.org/) * Copyright (C) 2005-2007 Joachim Klein * Copyright (c) 2007 Carlos Bederian + * Copyright (c) 2011- David Parker, Hongyang Qu * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License version 2 as @@ -20,9 +21,12 @@ package jltl2dstar; +import java.io.FileNotFoundException; +import java.io.FileWriter; import java.io.PrintStream; -import java.util.Iterator; +import java.util.*; +import jltl2ba.APElement; import jltl2ba.APSet; import prism.PrismException; @@ -85,6 +89,18 @@ public class DRA extends DA { this.print(typeID(), out); } + + /** + * Print the DRA/DSA in dot format to the output stream. + * This function can compact the automaton, which may invalidate iterators! + */ + public void printDot(PrintStream out) throws PrismException { + if (!this.isCompact()) { + this.makeCompact(); + } + + this.printDot(typeID(), out); + } /** * Print the DRA/DSA in DOT format to the output stream. @@ -127,6 +143,55 @@ public class DRA extends DA { return DAUnionAlgorithm.calculateUnion(this, other, trueloop_check, detailed_states); } + /** + * Convert the DRA from jltl2dstar to PRISM data structures. + */ + public prism.DRA createPrismDRA() throws PrismException + { + int i, k, numLabels, numStates, src, dest; + List apList; + BitSet bitset, bitset2; + RabinAcceptance acc; + prism.DRA draNew; + + numLabels = getAPSize(); + numStates = size(); + draNew = new prism.DRA(numStates); + // Copy AP set + apList = new ArrayList(numLabels); + for (i = 0; i < numLabels; i++) { + apList.add(getAPSet().getAP(i)); + } + draNew.setAPList(apList); + // Copy start state + draNew.setStartState(getStartState().getName()); + // Copy edges + for (i = 0; i < numStates; i++) { + DA_State cur_state = get(i); + src = cur_state.getName(); + for (Map.Entry transition : cur_state.edges().entrySet()) { + dest = transition.getValue().getName(); + bitset = new BitSet(); + for (k = 0; k < numLabels; k++) { + bitset.set(k, transition.getKey().get(k)); + } + draNew.addEdge(src, bitset, dest); + } + } + // Copy acceptance pairs + acc = acceptance(); + for (i = 0; i < acc.size(); i++) { + bitset = new BitSet(); + bitset.or(acc.getAcceptance_U(i)); + bitset2 = new BitSet(); + bitset2.or(acc.getAcceptance_L(i)); + // Note: Pairs (U_i,L_i) become (L_i,K_i) in PRISM's notation + draNew.addAcceptancePair(bitset, bitset2); + } + + return draNew; + } + // public DRA calculateUnionStuttered(DRA other, // StutterSensitivenessInformation stutter_information, // boolean trueloop_check, diff --git a/prism/src/jltl2dstar/LTL2Rabin.java b/prism/src/jltl2dstar/LTL2Rabin.java index f8296817..a2babc38 100644 --- a/prism/src/jltl2dstar/LTL2Rabin.java +++ b/prism/src/jltl2dstar/LTL2Rabin.java @@ -3,6 +3,7 @@ * (http://www.ltl2dstar.de/) for PRISM (http://www.prismmodelchecker.org/) * Copyright (C) 2005-2007 Joachim Klein * Copyright (c) 2007 Carlos Bederian + * Copyright (c) 2011- David Parker * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License version 2 as @@ -24,11 +25,13 @@ import jltl2ba.APSet; import jltl2ba.SimpleLTL; import prism.PrismException; +import java.util.BitSet; + public class LTL2Rabin { - public static DRA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { + public static prism.DRA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { SimpleLTL ltl = ltlFormula.simplify(); - return ltl2rabin(ltl, ltl.getAPs()); + return ltl2rabin(ltl, ltl.getAPs()).createPrismDRA(); } private static DRA ltl2rabin(SimpleLTL ltl, APSet apset) throws PrismException { diff --git a/prism/src/prism/DRA.java b/prism/src/prism/DRA.java new file mode 100644 index 00000000..63db1f29 --- /dev/null +++ b/prism/src/prism/DRA.java @@ -0,0 +1,245 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// * Hongyang Qu (University of 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 prism; + +import java.io.PrintStream; +import java.util.*; + +/** + * Class to store a deterministic Rabin automata (DRA). + * States are 0-indexed integers; class is parameterised by edge labels (Symbol). + */ +public class DRA +{ + /** AP list */ + private List apList; + /** Size, i.e. number of states */ + private int size; + /** Start state (index) */ + private int start; + /** Edges of DRA */ + private List> edges; + /** Sets L_i of acceptance condition pairs (L_i,K_i), stored as BitSets */ + private List acceptanceL; + /** Sets K_i of acceptance condition pairs (L_i,K_i), stored as BitSets */ + private List acceptanceK; + + /** Local class to represent DRA edge */ + class Edge + { + private Symbol label; + private int dest; + + public Edge(Symbol label, int dest) + { + this.label = label; + this.dest = dest; + } + } + + /** + * Construct a DRA of fixed size (i.e. fixed number of states). + */ + public DRA(int size) + { + apList = null; + this.size = size; + this.start = -1; + edges = new ArrayList>(size); + for (int i = 0; i < size; i++) { + edges.add(new ArrayList()); + } + acceptanceL = new ArrayList(); + acceptanceK = new ArrayList(); + } + + // TODO: finish/tidy this + public void setAPList(List apList) + { + this.apList = apList; + } + + public List getAPList() + { + return apList; + } + + // Mutators + + /** + * Set the start state (index) + */ + public void setStartState(int start) + { + this.start = start; + } + + /** + * Add an edge + */ + public void addEdge(int src, Symbol label, int dest) + { + edges.get(src).add(new Edge(label, dest)); + } + + /** + * Add an acceptance pair (L_i,K_i) + */ + public void addAcceptancePair(BitSet l, BitSet k) + { + acceptanceL.add(l); + acceptanceK.add(k); + } + + // Accessors + + /** + * Get the size (number of states). + */ + public int size() + { + return size; + } + + /** + * Get the start state (index) + */ + public int getStartState() + { + return start; + } + + /** + * Get the number of edges from state i + */ + public int getNumEdges(int i) + { + return edges.get(i).size(); + } + + /** + * Get the destination of edge j from state i + */ + public int getEdgeDest(int i, int j) + { + return edges.get(i).get(j).dest; + } + + /** + * Get the label of edge j from state i. + */ + public Symbol getEdgeLabel(int i, int j) + { + return edges.get(i).get(j).label; + } + + /** + * Get the number of pairs (L_i,K_i) in the acceptance condition. + */ + public int getNumAcceptancePairs() + { + return acceptanceL.size(); + } + + /** + * Get the states in set L_i for acceptance condition pair (L_i,K_i). + * @param Pair index (0-indexed) + */ + public BitSet getAcceptanceL(int i) + { + return acceptanceL.get(i); + } + + /** + * Get the states in set K_i for acceptance condition pair (L_i,K_i). + * @param Pair index (0-indexed) + */ + public BitSet getAcceptanceK(int i) + { + return acceptanceK.get(i); + } + + /** + * Print DRA in DOT format to an output stream. + */ + public void printDot(PrintStream out) throws PrismException + { + int i, j, n; + out.println("digraph model {"); + for (i = 0; i < size; i++) { + if (i == start) + out.println(" " + i + " [label=\"" + i + "\", shape=ellipse]"); + else { + boolean isAcceptance = false; + n = getNumAcceptancePairs(); + for (j = 0; j < n; j++) { + if (acceptanceK.get(j).get(i)) { + out.println(" " + i + " [label=\"" + i + "\", shape=doublecircle]"); + isAcceptance = true; + break; + } else if (acceptanceL.get(j).get(i)) { + out.println(" " + i + " [label=\"" + i + "\", shape=box]"); + isAcceptance = true; + break; + } + } + if (!isAcceptance) + out.println(" " + i + " [label=\"" + i + "\", shape=circle]"); + } + } + for (i = 0; i < size; i++) { + for (Edge e : edges.get(i)) { + out.println(" " + i + " -> " + e.dest + " [label=\"" + e.label + "\"]"); + } + } + } + + // Standard methods + + @Override + public String toString() + { + String s = ""; + int i, n; + s += size + " states (start " + start + ")"; + if (apList != null) + s += ", " + apList.size() + " labels"; + s += ":"; + for (i = 0; i < size; i++) { + for (Edge e : edges.get(i)) { + s += " " + i + "-" + e.label + "->" + e.dest; + } + } + n = acceptanceL.size(); + s += "; " + n + " acceptance pairs:"; + for (i = 0; i < n; i++) { + s += " (" + acceptanceL.get(i) + "," + acceptanceK.get(i) + ")"; + } + return s; + } +} diff --git a/prism/src/prism/LTL2RabinLibrary.java b/prism/src/prism/LTL2RabinLibrary.java new file mode 100644 index 00000000..8739f013 --- /dev/null +++ b/prism/src/prism/LTL2RabinLibrary.java @@ -0,0 +1,255 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of 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 prism; + +import java.io.*; +import java.util.*; + +import jltl2dstar.*; +import parser.ast.*; +import parser.visitor.ASTTraverse; +import parser.visitor.ASTTraverseModify; + +/** + * LTL-to-DRA conversion. + */ +public class LTL2RabinLibrary +{ + private static ArrayList labels; + + private static HashMap dras; + static { + // Hard-coded DRA descriptions for various LTL formulas + dras = new HashMap(); + dras.put("F \"L0\"", "2 states (start 0), 1 labels: 0-{}->0 0-{0}->1 1-{}->1 1-{0}->1; 1 acceptance pairs: ({},{1})"); + dras.put("G \"L0\"", "2 states (start 0), 1 labels: 0-{}->1 0-{0}->0 1-{}->1 1-{0}->1; 1 acceptance pairs: ({1},{0})"); + dras.put("G F \"L0\"", "2 states (start 0), 1 labels: 0-{0}->1 0-{}->0 1-{0}->1 1-{}->0; 1 acceptance pairs: ({},{1})"); + dras.put("!(G F \"L0\")", "2 states (start 0), 1 labels: 0-{}->1 0-{0}->0 1-{}->1 1-{0}->0; 1 acceptance pairs: ({0},{1})"); + dras.put("F G \"L0\"", "2 states (start 0), 1 labels: 0-{0}->1 0-{}->0 1-{0}->1 1-{}->0; 1 acceptance pairs: ({0},{1})"); + dras.put("!(F G \"L0\")", "2 states (start 0), 1 labels: 0-{}->1 0-{0}->0 1-{}->1 1-{0}->0; 1 acceptance pairs: ({},{1})"); + //dras.put("F (\"L0\"&(X \"L1\"))", "3 states (start 2), 2 labels: 0-{1}->0 0-{0, 1}->0 0-{}->0 0-{0}->0 1-{1}->0 1-{0, 1}->0 1-{}->2 1-{0}->1 2-{1}->2 2-{0, 1}->1 2-{}->2 2-{0}->1; 1 acceptance pairs: ({},{0})"); + //dras.put("!(F (\"L0\"&(X \"L1\")))", "4 states (start 3), 2 labels: 0-{1}->0 0-{0, 1}->1 0-{}->0 0-{0}->1 1-{1}->2 1-{0, 1}->2 1-{}->0 1-{0}->1 2-{1}->2 2-{0, 1}->2 2-{}->2 2-{0}->2 3-{1}->0 3-{0, 1}->1 3-{}->0 3-{0}->1; 1 acceptance pairs: ({2},{0, 1})"); + //dras.put("(X \"L0\")=>(G \"L1\")", "6 states (start 5), 2 labels: 0-{1}->0 0-{0, 1}->0 0-{}->0 0-{0}->0 1-{1}->0 1-{0, 1}->3 1-{}->0 1-{0}->4 2-{1}->0 2-{0, 1}->4 2-{}->0 2-{0}->4 3-{1}->3 3-{0, 1}->3 3-{}->4 3-{0}->4 4-{1}->4 4-{0, 1}->4 4-{}->4 4-{0}->4 5-{1}->1 5-{0, 1}->1 5-{}->2 5-{0}->2; 1 acceptance pairs: ({4},{0, 1, 2, 3})"); + //dras.put("!((X \"L0\")=>(G \"L1\"))", "6 states (start 5), 2 labels: 0-{1}->0 0-{0, 1}->0 0-{}->0 0-{0}->0 1-{1}->1 1-{0, 1}->1 1-{}->1 1-{0}->1 2-{1}->2 2-{0, 1}->2 2-{}->0 2-{0}->0 3-{1}->1 3-{0, 1}->0 3-{}->1 3-{0}->0 4-{1}->1 4-{0, 1}->2 4-{}->1 4-{0}->0 5-{1}->4 5-{0, 1}->4 5-{}->3 5-{0}->3; 1 acceptance pairs: ({1},{0})"); + //dras.put("(G !\"b\")&(G F \"a\")", "5 states (start 4), 2 labels: 0-{1}->0 0-{0, 1}->2 0-{}->1 0-{0}->2 1-{1}->3 1-{0, 1}->2 1-{}->4 1-{0}->2 2-{1}->2 2-{0, 1}->2 2-{}->2 2-{0}->2 3-{1}->0 3-{0, 1}->2 3-{}->1 3-{0}->2 4-{1}->3 4-{0, 1}->2 4-{}->4 4-{0}->2; 1 acceptance pairs: ({2},{0, 1})"); + //dras.put("(G \"L0\")&(G F \"L1\")", "5 states (start 4), 2 labels: 0-{1}->2 0-{0, 1}->0 0-{}->2 0-{0}->1 1-{1}->2 1-{0, 1}->3 1-{}->2 1-{0}->4 2-{1}->2 2-{0, 1}->2 2-{}->2 2-{0}->2 3-{1}->2 3-{0, 1}->0 3-{}->2 3-{0}->1 4-{1}->2 4-{0, 1}->3 4-{}->2 4-{0}->4; 1 acceptance pairs: ({2},{0, 1})"); + //dras.put("(G (\"L0\"=>(F \"L1\")))&(F G \"L2\")", "7 states (start 3), 3 labels: 0-{1, 2}->1 0-{0, 1, 2}->1 0-{2}->0 0-{0, 2}->0 0-{1}->3 0-{0, 1}->3 0-{}->4 0-{0}->4 1-{1, 2}->6 1-{0, 1, 2}->6 1-{2}->6 1-{0, 2}->5 1-{1}->3 1-{0, 1}->3 1-{}->3 1-{0}->4 2-{1, 2}->1 2-{0, 1, 2}->1 2-{2}->1 2-{0, 2}->0 2-{1}->3 2-{0, 1}->3 2-{}->3 2-{0}->4 3-{1, 2}->2 3-{0, 1, 2}->2 3-{2}->2 3-{0, 2}->4 3-{1}->3 3-{0, 1}->3 3-{}->3 3-{0}->4 4-{1, 2}->2 4-{0, 1, 2}->2 4-{2}->4 4-{0, 2}->4 4-{1}->3 4-{0, 1}->3 4-{}->4 4-{0}->4 5-{1, 2}->1 5-{0, 1, 2}->1 5-{2}->0 5-{0, 2}->0 5-{1}->3 5-{0, 1}->3 5-{}->4 5-{0}->4 6-{1, 2}->6 6-{0, 1, 2}->6 6-{2}->6 6-{0, 2}->5 6-{1}->3 6-{0, 1}->3 6-{}->3 6-{0}->4; 1 acceptance pairs: ({2, 3, 4},{5, 6})"); + //dras.put("!((G \"L0\")&(G F \"L1\"))", "4 states (start 3), 2 labels: 0-{1}->1 0-{0, 1}->3 0-{}->1 0-{0}->0 1-{1}->1 1-{0, 1}->1 1-{}->1 1-{0}->1 2-{1}->1 2-{0, 1}->3 2-{}->1 2-{0}->0 3-{1}->1 3-{0, 1}->3 3-{}->1 3-{0}->2; 2 acceptance pairs: ({},{1}) ({1, 2, 3},{0})"); + } + + /** + * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression, + * in which atomic propositions are represented by ExpressionLabel objects. + */ + public static DRA convertLTLFormulaToDRA(Expression ltl) throws PrismException + { + // Get list of labels appearing + labels = new ArrayList(); + ltl.accept(new ASTTraverse() + { + public Object visit(ExpressionLabel e) throws PrismLangException + { + labels.add(e.getName()); + return null; + } + }); + + // On a copy of formula, rename labels to "L0", "L1", "L2", ... + // (for looking up LTL formula in table of strings) + Expression ltl2 = ltl.deepCopy(); + ltl2.accept(new ASTTraverseModify() + { + public Object visit(ExpressionLabel e) throws PrismLangException + { + int i = labels.indexOf(e.getName()); + //char letter = (char) ('a' + i); + return new ExpressionLabel("L" + i); + } + }); + + // See if we have a hard-coded DRA to return + String draString = dras.get(ltl2.toString()); + if (draString != null) + return createDRAFromString(draString, labels); + + // If none, convert using jltl2dstar library + return LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); + } + + /** + * Create a DRA from a string, e.g.: + * "2 states (start 0), 1 labels: 0-{0}->1 0-{}->0 1-{0}->1 1-{}->0; 1 acceptance pairs: ({},{1})" + */ + private static DRA createDRAFromString(String s, List labels) throws PrismException + { + int ptr = 0, i, j, k, n, from, to; + String bs; + prism.DRA draNew; + + try { + // Num states + j = s.indexOf("states", ptr); + n = Integer.parseInt(s.substring(0, j).trim()); + draNew = new prism.DRA(n); + draNew.setAPList(labels); + // Start state + i = s.indexOf("start", j) + 6; + j = s.indexOf(")", i); + n = Integer.parseInt(s.substring(i, j).trim()); + draNew.setStartState(n); + // Edges + i = s.indexOf("labels", j) + 8; + j = s.indexOf("-{", i); + while (j != -1) { + from = Integer.parseInt(s.substring(i, j).trim()); + i = j + 2; + j = s.indexOf("}", i); + bs = s.substring(i, j); + i = j + 3; + j = Math.min(s.indexOf(";", i), s.indexOf(" ", i)); + to = Integer.parseInt(s.substring(i, j).trim()); + draNew.addEdge(from, createBitSetFromString(bs), to); + i = j + 1; + j = s.indexOf("-{", i); + } + // Acceptance pairs + i = s.indexOf("({", i); + while (i != -1) { + j = s.indexOf("},{", i); + k = s.indexOf("})", j); + draNew.addAcceptancePair(createBitSetFromString(s.substring(i + 2, j)), createBitSetFromString(s.substring(j + 3, k))); + i = s.indexOf("({", k); + } + } catch (NumberFormatException e) { + throw new PrismException("Error in DRA string format"); + } + + return draNew; + } + + /** + * Create a BitSet from a string, e.g. "0,3,4". + */ + private static BitSet createBitSetFromString(String s) throws PrismException + { + int i, n; + BitSet bs = new BitSet(); + String ss[] = s.split(","); + n = ss.length; + for (i = 0; i < n; i++) { + s = ss[i].trim(); + if (s.length() == 0) + continue; + bs.set(Integer.parseInt(s)); + } + return bs; + } + + // Example: manual creation of DRA for: !(F ("L0"&(X "L1"))) + public static DRA draForNotFaCb(String l0, String l1) throws PrismException + { + int numStates; + List apList; + prism.DRA draNew; + + // 4 states (start 3), 2 labels: 0-{1}->0 0-{0, 1}->1 0-{}->0 0-{0}->1 1-{1}->2 1-{0, 1}->2 1-{}->0 1-{0}->1 2-{1}->2 2-{0, 1}->2 2-{}->2 2-{0}->2 3-{1}->0 3-{0, 1}->1 3-{}->0 3-{0}->1; 1 acceptance pairs: ({2},{0, 1}) + numStates = 4; + draNew = new prism.DRA(numStates); + // AP set + apList = new ArrayList(2); + apList.add(l0); + apList.add(l1); + draNew.setAPList(apList); + // Start state + draNew.setStartState(3); + // Bitsets for edges + BitSet bitset = new BitSet(); // {} + BitSet bitset0 = new BitSet(); // {0} + bitset0.set(0); + BitSet bitset1 = new BitSet(); // {1} + bitset1.set(1); + BitSet bitset01 = new BitSet(); // {0, 1} + bitset01.set(0); + bitset01.set(1); + // Edges + // 3-{}->0 3-{0}->1; 1 acceptance pairs: ({2},{0, 1}) + draNew.addEdge(0, bitset1, 0); + draNew.addEdge(0, bitset01, 1); + draNew.addEdge(0, bitset, 0); + draNew.addEdge(0, bitset0, 1); + draNew.addEdge(1, bitset1, 2); + draNew.addEdge(1, bitset01, 2); + draNew.addEdge(1, bitset, 0); + draNew.addEdge(1, bitset0, 1); + draNew.addEdge(2, bitset1, 2); + draNew.addEdge(2, bitset01, 2); + draNew.addEdge(2, bitset, 2); + draNew.addEdge(2, bitset0, 2); + draNew.addEdge(3, bitset1, 0); + draNew.addEdge(3, bitset01, 1); + draNew.addEdge(3, bitset, 0); + draNew.addEdge(3, bitset0, 1); + // Acceptance pairs + BitSet bitsetL = new BitSet(); + bitsetL.set(2); + BitSet bitsetK = new BitSet(); + bitsetK.set(01); + bitsetK.set(1); + draNew.addAcceptancePair(bitsetL, bitsetK); + + return draNew; + } + + // To run: + // PRISM_MAINCLASS=prism.LTL2RabinLibrary bin/prism 'G F "L0"' + public static void main(String args[]) + { + try { + String ltl = args.length > 0 ? args[0] : "G F \"L0\""; + + // Convert to Expression + String pltl = "P=?[" + ltl + "]"; + PropertiesFile pf = Prism.getPrismParser().parsePropertiesFile(new ModulesFile(), new ByteArrayInputStream(pltl.getBytes())); + Prism.releasePrismParser(); + Expression expr = pf.getProperty(0); + expr = ((ExpressionProb) expr).getExpression(); + + System.out.println(ltl); + System.out.println(expr.toString()); + System.out.println(ltl.equals(expr.toString())); + DRA dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba()); + System.out.println(dra1); + DRA dra2 = convertLTLFormulaToDRA(expr); + System.out.println(dra2); + System.out.println(dra1.toString().equals(dra2.toString())); + //dra2.printDot(new PrintStream(new File("dra"))); + + } catch (Exception e) { + System.err.print("Error: " + e); + } + } +} diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index d495f19d..ff671da2 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -50,6 +50,15 @@ public class LTLModelChecker mainLog = prism.getMainLog(); } + /** + * Convert an LTL formula into a DRA. The LTL formula is represented as a PRISM Expression, + * in which atomic propositions are represented by ExpressionLabel objects. + */ + public static DRA convertLTLFormulaToDRA(Expression ltl) throws PrismException + { + return LTL2RabinLibrary.convertLTLFormulaToDRA(ltl); + } + /** * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result @@ -528,28 +537,25 @@ public class LTLModelChecker * * @return a referenced mask BDD over trans */ - public JDDNode buildTransMask(DRA dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, JDDVars draDDColVars) + public JDDNode buildTransMask(DRA dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, JDDVars draDDColVars) { - Iterator it; - DA_State state; JDDNode draMask, label, exprBDD, transition; - int i, n; + int i, j, k, numAPs, numStates, numEdges; + numAPs = dra.getAPList().size(); draMask = JDD.Constant(0); // Iterate through all (states and) transitions of DRA - for (it = dra.iterator(); it.hasNext();) { - state = it.next(); - for (Map.Entry edge : state.edges().entrySet()) { + numStates = dra.size(); + for (i = 0; i < numStates; i++) { + numEdges = dra.getNumEdges(i); + for (j = 0; j < numEdges; j++) { // Build a transition label BDD for each edge - // System.out.println(state.getName() + " to " + edge.getValue().getName() + " through " + - // edge.getKey().toString(dra.getAPSet(), false)); label = JDD.Constant(1); - n = dra.getAPSize(); - for (i = 0; i < n; i++) { - // Get the expression BDD for label i - exprBDD = labelDDs.get(Integer.parseInt(dra.getAPSet().getAP(i).substring(1))); + for (k = 0; k < numAPs; k++) { + // Get the expression BDD for AP k (via label "Lk") + exprBDD = labelDDs.get(Integer.parseInt(dra.getAPList().get(k).substring(1))); JDD.Ref(exprBDD); - if (!edge.getKey().get(i)) { + if (!dra.getEdgeLabel(i, j).get(k)) { exprBDD = JDD.Not(exprBDD); } label = JDD.And(label, exprBDD); @@ -557,7 +563,7 @@ public class LTLModelChecker // Switch label BDD to col vars label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars); // Build a BDD for the edge - transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge.getValue().getName(), 1); + transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, i, dra.getEdgeDest(i, j), 1); // Now get the conjunction of the two transition = JDD.And(transition, label); // Add edge BDD to the DRA transition mask @@ -574,27 +580,31 @@ public class LTLModelChecker * * @return a referenced mask BDD over start */ - public JDDNode buildStartMask(DRA dra, Vector labelDDs, JDDVars draDDRowVars) + public JDDNode buildStartMask(DRA dra, Vector labelDDs, JDDVars draDDRowVars) { JDDNode startMask, label, exprBDD, dest, tmp; + int i, j, k, numAPs, numEdges; + numAPs = dra.getAPList().size(); startMask = JDD.Constant(0); - for (Map.Entry edge : dra.getStartState().edges().entrySet()) { + // Iterate through all transitions of start state of DRA + i = dra.getStartState(); + numEdges = dra.getNumEdges(i); + for (j = 0; j < numEdges; j++) { // Build a transition label BDD for each edge - // System.out.println("To " + edge.getValue().getName() + " through " + - // edge.getKey().toString(dra.getAPSet(), false)); label = JDD.Constant(1); - for (int i = 0; i < dra.getAPSize(); i++) { - exprBDD = labelDDs.get(Integer.parseInt(dra.getAPSet().getAP(i).substring(1))); + for (k = 0; k < numAPs; k++) { + // Get the expression BDD for AP k (via label "Lk") + exprBDD = labelDDs.get(Integer.parseInt(dra.getAPList().get(k).substring(1))); JDD.Ref(exprBDD); - if (!edge.getKey().get(i)) { + if (!dra.getEdgeLabel(i, j).get(k)) { exprBDD = JDD.Not(exprBDD); } - label = JDD.Apply(JDD.TIMES, label, exprBDD); + label = JDD.And(label, exprBDD); } // Build a BDD for the DRA destination state dest = JDD.Constant(0); - dest = JDD.SetVectorElement(dest, draDDRowVars, edge.getValue().getName(), 1); + dest = JDD.SetVectorElement(dest, draDDRowVars, dra.getEdgeDest(i, j), 1); // Now get the conjunction of the two tmp = JDD.And(dest, label); @@ -611,7 +621,7 @@ public class LTLModelChecker * * @returns a referenced BDD of the union of all the accepting sets */ - public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model) throws PrismException + public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model) throws PrismException { SCCComputer sccComputer; JDDNode acceptingStates, allAcceptingStates; @@ -629,23 +639,25 @@ public class LTLModelChecker // for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i // and compute the BSCCs in H'_i - for (i = 0; i < dra.acceptance().size(); i++) { + for (i = 0; i < dra.getNumAcceptancePairs(); i++) { // build the acceptance vectors H_i and L_i JDDNode acceptanceVector_H = JDD.Constant(0); JDDNode acceptanceVector_L = JDD.Constant(0); for (j = 0; j < dra.size(); j++) { /* - * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that H_i contains Inf(ρ) The intersection of - * Inf(ρ) and L_i is non-empty + * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that + * H_i contains Inf(\rho) and the intersection of Inf(K) and L_i is non-empty * - * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that The intersection of U_i and - * Inf(ρ) is empty (H_i = S - U_i) The intersection of L_i and Inf(ρ) is non-empty + * OTOH PRISM's DRAs (via ltl2dstar use pairs (L_i, K_i) such that + * the intersection of L_i and Inf(\rho) is empty + * and the intersection of K_i and Inf(\rho) is non-empty + * So: L_i = K_i, H_i = S - L_i */ - if (!dra.acceptance().isStateInAcceptance_U(i, j)) { + if (!dra.getAcceptanceL(i).get(j)) { acceptanceVector_H = JDD.SetVectorElement(acceptanceVector_H, draDDRowVars, j, 1.0); } - if (dra.acceptance().isStateInAcceptance_L(i, j)) { + if (dra.getAcceptanceK(i).get(j)) { acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0); } } @@ -699,7 +711,7 @@ public class LTLModelChecker // for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i // and compute the maximal ECs in H'_i - for (i = 0; i < dra.acceptance().size(); i++) { + for (i = 0; i < dra.getNumAcceptancePairs(); i++) { // build the acceptance vectors H_i and L_i JDDNode acceptanceVector_H = JDD.Constant(0); @@ -712,10 +724,10 @@ public class LTLModelChecker * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that The intersection of U_i and * Inf(ρ) is empty (H_i = S - U_i) The intersection of L_i and Inf(ρ) is non-empty */ - if (!dra.acceptance().isStateInAcceptance_U(i, j)) { + if (!dra.getAcceptanceL(i).get(j)) { acceptanceVector_H = JDD.SetVectorElement(acceptanceVector_H, draDDRowVars, j, 1.0); } - if (dra.acceptance().isStateInAcceptance_L(i, j)) { + if (dra.getAcceptanceK(i).get(j)) { acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0); } } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index c95714e2..96d3cea5 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -431,14 +431,14 @@ public class NondetModelChecker extends NonProbModelChecker // Convert LTL formula to deterministic Rabin automaton (DRA) // For min probabilities, need to negate the formula // (But check fairness setting since this may affect min/max) - mainLog.println("\nBuilding deterministic Rabin automaton (for " + (min && !fairness ? "!" : "") + ltl + ")..."); - l = System.currentTimeMillis(); + // (add parentheses to allow re-parsing if required) if (min && !fairness) { - dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba().negate()); - } else { - dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); + ltl = Expression.Not(Expression.Parenth(ltl)); } - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.acceptance().size() + " pairs."); + mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + l = System.currentTimeMillis(); + dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); + mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); // dra.print(System.out); l = System.currentTimeMillis() - l; mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 3f1ae658..118971de 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -28,11 +28,10 @@ package prism; import java.io.File; import java.io.FileNotFoundException; +import java.util.BitSet; import java.util.Vector; import jdd.*; -import jltl2dstar.DRA; -import jltl2dstar.LTL2Rabin; import dv.*; import mtbdd.*; import sparse.*; @@ -51,6 +50,9 @@ public class ProbModelChecker extends NonProbModelChecker // Options (in addition to those inherited from StateModelChecker): // Use 0,1 precomputation algorithms? + // if 'precomp' is false, this disables all (non-essential) use of prob0/prob1 + // if 'precomp' is true, the values of prob0/prob1 determine what is used + // (currently prob0/prob are not under user control) protected boolean precomp; protected boolean prob0; protected boolean prob1; @@ -588,7 +590,7 @@ public class ProbModelChecker extends NonProbModelChecker StateValues probsProduct = null, probs = null; Expression ltl; Vector labelDDs; - DRA dra; + DRA dra; ProbModel modelProduct; ProbModelChecker mcProduct; JDDNode startMask; @@ -624,8 +626,8 @@ public class ProbModelChecker extends NonProbModelChecker // Convert LTL formula to deterministic Rabin automaton (DRA) mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); l = System.currentTimeMillis(); - dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.acceptance().size() + " pairs."); + dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); + mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); // dra.print(System.out); l = System.currentTimeMillis() - l; mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds.");