More jltl2ba and jltl2dstar bug fixes from Joachim Klein.

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

prism/src/jltl2ba/SimpleLTL.java

@@ -947,6 +947,13 @@ public class SimpleLTL {
 		// b.print_spin(System.out, apset);
 		NBA nba = b.toNBA(apset);
 		// nba.print(System.out);
+
+		// jltl2ba should never produce disjoint NBA,
+		// i.e., where some states are not reachable
+		// from the intial state, so we want to fail
+		// later if the NBA is discovered to be disjoint:
+		nba.setFailIfDisjoint(true);
+
 		return nba;
 	}
 	

prism/src/jltl2dstar/GraphAlgorithms.java

@@ -90,14 +90,14 @@ public class GraphAlgorithms {
 				return;
 			}
 
-			if (!disjoint) {
-				int start_idx = start_state.getName();
-				visit(start_idx);
-			} else {
+			int start_idx = start_state.getName();
+			visit(start_idx);
+			if (disjoint) {
 				// The Graph may be disjoint -> restart DFS on every not yet visited state 
 				for (int v = 0; v < _graph.size(); ++v) {
 					if (_dfs_data.get(v) == null) {
-						// not yet visited
+						// not yet visited, i.e., not reachable from the start state
+						_result.setGraphIsDisjoint();
 						visit(v);
 					}
 				}

prism/src/jltl2dstar/NBA.java

@@ -55,6 +55,12 @@ public class NBA implements Iterable<NBA_State> {
 	  /** The states that are accepting (final) */
 	  private MyBitSet _final_states;
 
+	  /**
+	   * Flag, telling whether to fail later on if the NBA is discovered
+	   * to be disjoint, as this is indicative of a malfunctioning
+	   * NBA generator.
+	   */
+	  private boolean _fail_if_disjoint = false;
 	
 	/**
 	 * Constructor.
@@ -260,6 +266,18 @@ public class NBA implements Iterable<NBA_State> {
 		return _state_count;
 	}
 	
+	/** Set fail_if_disjoint flag */
+	public void setFailIfDisjoint(boolean value)
+	{
+		_fail_if_disjoint = value;
+	}
+	
+	/** Get fail_if_disjoint flag */
+	public boolean getFailIfDisjoint()
+	{
+		return _fail_if_disjoint;
+	}
+	
 	/** 
 	 * Create a new state.
 	 * @return the index of the new state

prism/src/jltl2dstar/NBAAnalysis.java

@@ -108,6 +108,14 @@ public class NBAAnalysis {
 		return _nba.getFinalStates();
 	}
 
+	/**
+	 * Returns true if the NBA is disjoint, i.e., there are states
+	 * that are not reachable from the initial state
+	 */
+	public boolean isNBADisjoint() {
+		return getSCCs().getGraphIsDisjoint();
+	}
+	
 	/** Get the reachability analysis for the NBA
 	 * @return vector of BitSets representing the set of state which are reachable from a given state.
 	 */

prism/src/jltl2dstar/SCCs.java

@@ -37,6 +37,7 @@ public class SCCs {
 	public Vector<MyBitSet> _dag;
 	public Vector<Integer> _topological_order;
 	public Vector<MyBitSet> _reachability;
+	public boolean _graph_is_disjoint;
 
 
 	/** Constructor */
@@ -46,6 +47,7 @@ public class SCCs {
 		_dag = new Vector<MyBitSet>();
 		_topological_order = new Vector<Integer>();
 		_reachability = new Vector<MyBitSet>();
+		_graph_is_disjoint = false;
 	}
 	
 	/** Get the states that are in SCC scc_index */
@@ -131,4 +133,14 @@ public class SCCs {
 		}
 		_state_to_scc.set(state, new Integer(scc));
 	}
+
+	/** Set flag that the graph was discovered to be disjoint */
+	public void setGraphIsDisjoint() {
+		_graph_is_disjoint = true;
+	}
+	
+	/** Get flag wether the graph was discovered to be disjoint */
+	public boolean getGraphIsDisjoint() {
+		return _graph_is_disjoint;
+	}
 }

prism/src/jltl2dstar/SafrasAlgorithm.java

@@ -51,10 +51,18 @@ public class SafrasAlgorithm {
 	 * @param nba The NBA
 	 * @param options The options for Safra's algorithm
 	 */
-	public SafrasAlgorithm(NBA nba, Options_Safra options) {
+	public SafrasAlgorithm(NBA nba, Options_Safra options) throws PrismException {
 		_options = options; 
 		_nba_analysis = new NBAAnalysis(nba);
 		_nba = nba;
+		
+		if (_nba.getFailIfDisjoint() && _nba_analysis.isNBADisjoint()) {
+			throw new PrismException("The NBA generated for the LTL formula was discovered to be disjoint,\n"
+			                       + "i.e., some states were not reachable from the initial state. This likely\n"
+			                       + "indicates a problem in the translation. Please report the formula to the\n"
+			                       + "PRISM developers");
+		}
+		
 		_NODES = 2 * nba.getStateCount();
 		stv_reorder = null; 
 		_next = new Vector<MyBitSet>();
@@ -462,7 +470,7 @@ public class SafrasAlgorithm {
 				_node_order[child.getID()] = i++;
 
 				MyBitSet label_this = child.getLabeling();
-				for (int setbit = label_this.nextSetBit(0); i >= 0; i = label_this.nextSetBit(i+1)) {
+				for (int setbit = label_this.nextSetBit(0); setbit >= 0; setbit = label_this.nextSetBit(setbit+1)) {
 					reachable_this.or(_nba_reachability.get(setbit));
 				}
 				//      std::cerr << "reachability_this: "<<reachable_this << std::endl;