New intermediate class to store DRAs, small efficiency improvements in LTL due to hard-coded DRAs + easier decoupling of GPLed LTL-to-DRA libraries, if needed.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4269 bbc10eb1-c90d-0410-af57-cb519fbb1720

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 <j.klein@ltl2dstar.de>
  * 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<APElement, DA_State> transition : cur_state.edges().entrySet()) {
+				out.println("	" + i_state + " -> " + transition.getValue().getName() + 
+						" [label=\"" + transition.getKey().toString(_ap_set, true) + "\"]");
+			}
+		}
+		out.println("}");
+		
+	}
 }

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 <j.klein@ltl2dstar.de>
  * 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<BitSet> createPrismDRA() throws PrismException
+	{
+		int i, k, numLabels, numStates, src, dest;
+		List<String> apList;
+		BitSet bitset, bitset2;
+		RabinAcceptance acc;
+		prism.DRA<BitSet> draNew;
+		
+		numLabels = getAPSize();
+		numStates = size();
+		draNew = new prism.DRA<BitSet>(numStates);
+		// Copy AP set
+		apList = new ArrayList<String>(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<APElement, DA_State> 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,

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 <j.klein@ltl2dstar.de>
  * 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<BitSet> 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 {

prism/src/prism/DRA.java

@@ -0,0 +1,245 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	* Hongyang Qu <hongyang.qu@comlab.ox.ac.uk> (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<Symbol>
+{
+	/** AP list */
+	private List<String> apList;
+	/** Size, i.e. number of states */
+	private int size;
+	/** Start state (index) */
+	private int start;
+	/** Edges of DRA */
+	private List<List<Edge>> edges;
+	/** Sets L_i of acceptance condition pairs (L_i,K_i), stored as BitSets */
+	private List<BitSet> acceptanceL;
+	/** Sets K_i of acceptance condition pairs (L_i,K_i), stored as BitSets */
+	private List<BitSet> 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<List<Edge>>(size);
+		for (int i = 0; i < size; i++) {
+			edges.add(new ArrayList<Edge>());
+		}
+		acceptanceL = new ArrayList<BitSet>();
+		acceptanceK = new ArrayList<BitSet>();
+	}
+
+	// TODO: finish/tidy this
+	public void setAPList(List<String> apList)
+	{
+		this.apList = apList;
+	}
+	
+	public List<String> 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;
+	}
+}

prism/src/prism/LTL2RabinLibrary.java

@@ -0,0 +1,255 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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<String> labels;
+
+	private static HashMap<String, String> dras;
+	static {
+		// Hard-coded DRA descriptions for various LTL formulas 
+		dras = new HashMap<String, String>();
+		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<BitSet> convertLTLFormulaToDRA(Expression ltl) throws PrismException
+	{
+		// Get list of labels appearing
+		labels = new ArrayList<String>();
+		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<BitSet> createDRAFromString(String s, List<String> labels) throws PrismException
+	{
+		int ptr = 0, i, j, k, n, from, to;
+		String bs;
+		prism.DRA<BitSet> draNew;
+
+		try {
+			// Num states
+			j = s.indexOf("states", ptr);
+			n = Integer.parseInt(s.substring(0, j).trim());
+			draNew = new prism.DRA<BitSet>(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<BitSet> draForNotFaCb(String l0, String l1) throws PrismException
+	{
+		int numStates;
+		List<String> apList;
+		prism.DRA<BitSet> 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<BitSet>(numStates);
+		// AP set
+		apList = new ArrayList<String>(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<BitSet> dra1 = jltl2dstar.LTL2Rabin.ltl2rabin(expr.convertForJltl2ba());
+			System.out.println(dra1);
+			DRA<BitSet> 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);
+		}
+	}
+}

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<BitSet> 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<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, JDDVars draDDColVars)
+	public JDDNode buildTransMask(DRA<BitSet> dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, JDDVars draDDColVars)
 	{
-		Iterator<DA_State> 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<APElement, DA_State> 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<JDDNode> labelDDs, JDDVars draDDRowVars)
+	public JDDNode buildStartMask(DRA<BitSet> dra, Vector<JDDNode> 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<APElement, DA_State> 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<BitSet> 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);
 				}
 			}

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.");

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<JDDNode> labelDDs;
-		DRA dra;
+		DRA<BitSet> 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.");