code: //==============================================================================
  //	
  //	Copyright (c) 2002-
  //	Authors:
  //	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
  //	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (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 explicit;
  
  import java.util.BitSet;
  import java.util.Iterator;
  import java.util.Vector;
  
  import automata.LTL2NBA;
  import jltl2dstar.NBA;
  import common.IterableBitSet;
  import common.IterableStateSet;
  import parser.ast.Expression;
  import parser.ast.ExpressionExists;
  import parser.ast.ExpressionForAll;
  import parser.ast.ExpressionTemporal;
  import parser.ast.ExpressionUnaryOp;
  import prism.PrismComponent;
  import prism.PrismException;
  import prism.PrismNotSupportedException;
  import prism.PrismSettings;
  
  /**
   * Explicit-state, non-probabilistic model checker.
   */
  public class NonProbModelChecker extends StateModelChecker
  {
  	/**
  	 * Create a new NonProbModelChecker, inherit basic state from parent (unless null).
  	 */
  	public NonProbModelChecker(PrismComponent parent) throws PrismException
  	{
  		super(parent);
  	}
  	
  	@Override
  	public StateValues checkExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
  	{
  		StateValues res;
  
  		// E operator
  		if (expr instanceof ExpressionExists) {
  			return checkExpressionExists(model, ((ExpressionExists)expr).getExpression(), statesOfInterest);
  		}
  		// A operator
  		else if (expr instanceof ExpressionForAll) {
  			return checkExpressionForAll(model, ((ExpressionForAll)expr).getExpression(), statesOfInterest);
  		}
  		// Otherwise, use the superclass
  		else {
  			res = super.checkExpression(model, expr, statesOfInterest);
  		}
  
  		return res;
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ expr ].
  	 * <br>
  	 * 'expr' has to be a simple path formula.
  	 *
  	 * @param model the model
  	 * @param expr the expression for 'expr'
  	 * @param statesOfInterest the states of interest ({@code null} = all states)
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ expr ]
  	 */
  	protected StateValues checkExpressionExists(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
  	{
  		// Check whether we have to use LTL path formula handling
  		if (getSettings().getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA)
  		    || !expr.isSimplePathFormula() ) {
  			return checkExistsLTL(model, expr, statesOfInterest);
  		}
  
  		// We have a simple path formula, convert to either
  		// (1) a U b
  		// (2) !(a U b)
  		// (3) X a
  		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
  
  		// next-step (3)
  		if (expr instanceof ExpressionTemporal &&
  		    ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_X) {
  			if (((ExpressionTemporal)expr).hasBounds()) {
  				throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported");
  			}
  			return checkExistsNext(model, ((ExpressionTemporal) expr).getOperand2(), statesOfInterest);
  		}
  
  		// until
  		boolean negated = false;
  		if (Expression.isNot(expr)) {
  			// (2) !(a U b)
  			negated = true;
  			expr = ((ExpressionUnaryOp)expr).getOperand();
  		}
  
  		ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
  		assert (exprTemp.getOperator() == ExpressionTemporal.P_U);
  
  		if (exprTemp.hasBounds()) {
  			throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported");
  		}
  
  		StateValues result;
  
  		if (negated) {
  			// compute E[ !a R !b ] instead of E[ !(a U b) ]
  			result = checkExistsRelease(model,
  			                            Expression.Not(exprTemp.getOperand1()),
  			                            Expression.Not(exprTemp.getOperand2()));
  		} else {
  			// compute E[ a U b ]
  			result = checkExistsUntil(model, exprTemp.getOperand1(), exprTemp.getOperand2());
  		}
  
  		return result;
  	}
  
  	/**
  	 * Compute the set of states satisfying A[ expr ].
  	 * <br>
  	 * This is computed by determining the set of states not satisfying E[ !expr ].
  	 * 'expr' has to be a simple path formula.
  	 *
  	 * @param model the model
  	 * @param expr the expression for 'expr'
  	 * @param statesOfInterest the states of interest ({@code null} = all states)
  	 * @return a boolean StateValues, with {@code true} for all states satisfying A[ expr ]
  	 */
  	protected StateValues checkExpressionForAll(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
  	{
  		StateValues result = checkExpressionExists(model, Expression.Not(expr), statesOfInterest);
  		result.complement();
  
  		return result;
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ X expr ].
  	 * @param model the model
  	 * @param expr the expression for 'expr'
  	 * @param statesOfInterest the states of interest ({@code null} = all states)
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ X expr ]
  	 */
  	protected StateValues checkExistsNext(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
  	{
  		BitSet target = checkExpression(model, expr, null).getBitSet();
  		BitSet result = computeExistsNext(model, target, statesOfInterest);
  
  		return StateValues.createFromBitSet(result, model);
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ X "target" ].
  	 * @param model the model
  	 * @param target the BitSet of states for target
  	 * @param statesOfInterest the states of interest ({@code null} = all states)
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ X "target" ]
  	 */
  	public BitSet computeExistsNext(Model model, BitSet target, BitSet statesOfInterest) throws PrismException
  	{
  		BitSet result = new BitSet();
  
  		for (int s : new IterableStateSet(statesOfInterest, model.getNumStates())) {
  			// for each state of interest, check whether there is a transition to the 'target'
  			if (model.someSuccessorsInSet(s, target)) {
  				result.set(s);
  			}
  		}
  
  		return result;
  	}
  
  	/**
  	 * Compute the set of states satisfying A[ X expr ].
  	 * @param model the model
  	 * @param expr the expression for 'expr'
  	 * @param statesOfInterest the states of interest ({@code null} = all states)
  	 * @return a boolean StateValues, with {@code true} for all states satisfying A[ X expr ]
  	 */	
  	protected StateValues checkForAllNext(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
  	{
  		BitSet target = checkExpression(model, expr, null).getBitSet();
  		BitSet result = new BitSet();
  
  		for (int s : new IterableStateSet(statesOfInterest, model.getNumStates())) {
  			// for each state of interest, check whether all transitions go to 'target'
  			if (model.allSuccessorsInSet(s, target)) {
  				result.set(s);
  			}
  		}
  
  		return StateValues.createFromBitSet(result, model);
  	}
  
  	/**
  	 * Compute the set of states satisfying A[ X "target" ].
  	 * @param model the model
  	 * @param target the BitSet of states in target
  	 * @param statesOfInterest the states of interest ({@code null} = all states)
  	 * @return a boolean StateValues, with {@code true} for all states satisfying A[ X "target" ]
  	 */
  	public BitSet computeForAllNext(Model model, BitSet target, BitSet statesOfInterest) throws PrismException
  	{
  		BitSet result = new BitSet();
  
  		for (int s : new IterableStateSet(statesOfInterest, model.getNumStates())) {
  			// for each state of interest, check whether all transitions go to 'target'
  			if (model.allSuccessorsInSet(s, target)) {
  				result.set(s);
  			}
  		}
  
  		return result;
  	}
  
  	
  	/**
  	 * Compute the set of states satisfying E[ a U b ].
  	 * @param model the model
  	 * @param exprA the expression for 'a'
  	 * @param exprB the expression for 'b'
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ a U b ]
  	 */
  	protected StateValues checkExistsUntil(Model model, Expression exprA, Expression exprB) throws PrismException {
  		// the set of states satisfying exprA
  		BitSet A = checkExpression(model, exprA, null).getBitSet();
  		// the set of states satisfying exprB
  		BitSet B = checkExpression(model, exprB, null).getBitSet();
  
  		BitSet result = computeExistsUntil(model, A, B);
  
  		return StateValues.createFromBitSet(result, model);
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ "a" U "b" ].
  	 * @param model the model
  	 * @param A the BitSet of states for "a"
  	 * @param B the BitSet of states for "b"
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ "a" U "b" ]
  	 */
  	public BitSet computeExistsUntil(Model model, BitSet A, BitSet B) throws PrismException
  	{
   		PredecessorRelation pre = model.getPredecessorRelation(this, true);
   		return pre.calculatePreStar(A, B, B);
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ G a ].
  	 * @param model the model
  	 * @param exprA the expression for 'a'
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ G a ]
  	 */
  	protected StateValues checkExistsGlobally(Model model, Expression exprA) throws PrismException
  	{
  		return checkExistsRelease(model, Expression.False(), exprA);
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ G "a" ].
  	 * @param model the model
  	 * @param A the BitSet of states for "a"
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ G "a" ]
  	 */
  	public BitSet computeExistsGlobally(Model model, BitSet A) throws PrismException
  	{
  		return computeExistsRelease(model, new BitSet(), A);
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ a R b ], i.e., from which there
  	 * exists a path satisfying G b or b U (a&b)
  	 * @param model the model
  	 * @param exprA the expression for 'a'
  	 * @param exprB the expression for 'b'
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ a R b ]
  	 */
  	protected StateValues checkExistsRelease(Model model, Expression exprA, Expression exprB) throws PrismException
  	{
  		// the set of states satisfying exprA
  		BitSet A = checkExpression(model, exprA, null).getBitSet();
  		// the set of states satisfying exprB
  		BitSet B = checkExpression(model, exprB, null).getBitSet();
  
  		PredecessorRelation pre = model.getPredecessorRelation(this, true);
  
  		// the intersection of A and B
  		// these states surely satisfy E[ a R b ]
  		BitSet AandB = (BitSet) A.clone();
  		AandB.and(B);
  
  		// The set T contains all states for which E[ a R b ] has not yet been disproven
  		// Initially, this contains all 'B' states
  		BitSet T = (BitSet) B.clone();
  
  		// the set E contains all states that have not yet been visited
  		// and for which we have proven that they do not satisfy E[ a R b ]
  		// Initially, it contains the complement of 'T'
  		BitSet E = (BitSet) T.clone();
  		E.flip(0, model.getNumStates());
  
  		// NOTE: The correctness relies on the fact that both
  		// getSuccessorsIterator and pre.getPre are exactly the two sides
  		// of the underlying edge relation, i.e., that the number of entries
  		// is consistent. If the PredecessorRelation semantics are changed
  		// later on, we have to adapt here as well...
  
  		// for all states s in T \ AandB, we compute count[s], the number of successors
  		// according to getSuccessorsIterator
  		int count[] = new int[model.getNumStates()];
  		for (int s : IterableBitSet.getSetBits(T)) {
  			if (AandB.get(s)) continue;
  
  			int i=0;
  			for (Iterator<Integer> it = model.getSuccessorsIterator(s); it.hasNext(); it.next()) {
  				i++;
  			}
  			count[s]=i;
  		}
  		
  		while (!E.isEmpty()) {
  			// get the first element of E
  			int t = E.nextSetBit(0);
  			// and mark it as processed
  			E.clear(t);
  
  			// We know that t does not satisfy E[ a R b ].
  			// Any predecessor s of t can be shown to not satisfy E[ a R b ]
  			// if there are no remaining successors into T, i.e, if count[s]==0
  
  			// For all predecessors s of t....
  			for (int s : pre.getPre(t)) {
  				// ... ignore if we have already proven that it does not satisfy E[ a R b ]
  				if (!T.get(s)) continue;
  
  				// decrement count, because s can not use t to stay in T
  				count[s]--;
  				if (count[s] == 0 && !AandB.get(s)) {
  					// the count is zero and s is not safe because it's in AandB
  					//  -> remove from T and add to E
  					T.clear(s);
  					E.set(s);
  				}
  			}
  		}
  
  		return StateValues.createFromBitSet(T, model);
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ "a" R "b" ], i.e., from which there
  	 * exists a path satisfying G "b" or "b" U ("a&b")
  	 * @param model the model
  	 * @param A the BitSet for the states in "a"
  	 * @param A the BitSet for the states in "a"
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ "a" R "b" ]
  	 */
  	public BitSet computeExistsRelease(Model model, BitSet A, BitSet B) throws PrismException
  	{
  		PredecessorRelation pre = model.getPredecessorRelation(this, true);
  
  		// the intersection of A and B
  		// these states surely satisfy E[ a R b ]
  		BitSet AandB = (BitSet) A.clone();
  		AandB.and(B);
  
  		// The set T contains all states for which E[ a R b ] has not yet been disproven
  		// Initially, this contains all 'B' states
  		BitSet T = (BitSet) B.clone();
  
  		// the set E contains all states that have not yet been visited
  		// and for which we have proven that they do not satisfy E[ a R b ]
  		BitSet E = new BitSet();
  		// Initially, it contains the complement of 'T'
  		E.set(0, model.getNumStates(), true);
  		E.andNot(T);
  
  		// TODO: Important: The correctness relies on the fact that
  		// the number of predecessors provided by pre.getPre()
  		// and the number of successors provided by getSuccessorsIterator()
  		// mirror each other. If PredecessorRelation is changed later on,
  		// take this into account...
  
  		// for all states s in T \ AandB, we compute count[s], the number of (unique) successors
  		int count[] = new int[model.getNumStates()];
  		for (int s : IterableBitSet.getSetBits(T)) {
  			if (AandB.get(s)) continue;
  
  			int i=0;
  			for (Iterator<Integer> it = model.getSuccessorsIterator(s); it.hasNext(); it.next()) {
  				i++;
  			}
  			count[s]=i;
  		}
  
  		while (!E.isEmpty()) {
  			// get the first element of E
  			int t = E.nextSetBit(0);
  			// and mark it as processed
  			E.clear(t);
  
  			// We know that t does not satisfy E[ a R b ].
  			// Any predecessor s of t can be shown to not satisfy E[ a R b ]
  			// if there are no remaining successors into T, i.e, if count[s]==0
  
  			// For all predecessors s of t....
  
  			for (int s : pre.getPre(t)) {
  				// ... ignore if we have already proven that it does not satisfy E[ a R b ]
  				if (!T.get(s)) continue;
  
  				// decrement count, because s can not use t to stay in T
  				count[s]--;
  				if (count[s] == 0 && !AandB.get(s)) {
  					// the count is zero and s is not safe because it's in AandB
  					//  -> remove from T and add to E
  					T.clear(s);
  					E.set(s);
  				}
  			}
  		}
  
  		return T;
  	}
  
  	/**
  	 * Compute the set of states satisfying E[ phi ] for an LTL formula phi.
  	 * The LTL formula can have nested P or R operators, as well as nested CTL formulas.
  	 * @param model the model
  	 * @param expr the LTL formula
  	 * @param statesofInterest the states of interest
  	 * @return a boolean StateValues, with {@code true} for all states satisfying E[ phi ]
  	 */
  	protected StateValues checkExistsLTL(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
  	{
  		if (Expression.containsTemporalTimeBounds(expr)) {
  			throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
  		}
  
  		LTLModelChecker ltlMC = new LTLModelChecker(this);
  		Vector<BitSet> labelBS = new Vector<BitSet>();
  		expr = ltlMC.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelBS);
  
  		// We are doing existential LTL checking:
  		//  - Construct an NBA for the LTL formula
  		//  - Construct product M' = M x NBA
  		//  - Search for an accepting lasso in M', i.e., a reachable cycle
  		//    that visits F infinitely often
  
  		mainLog.println("Non-probabilistic LTL model checking for E[ " +expr + " ]");
  		mainLog.print("Constructing NBA...");
  		mainLog.flush();
  		LTL2NBA ltl2nba = new LTL2NBA(this);
  		NBA nba = ltl2nba.convertLTLFormulaToNBA(expr, this.getConstantValues());
  		mainLog.println(" NBA has " + nba.size() + " states");
  
  		// If we only care about a few states in the model,
  		// it would make sense to do a nested DFS and construct the product on the fly.
  		// But for now it's easier to rely on the existing infrastructure,
  		// construct the full product and just compute the SCCs.
  		mainLog.print("Constructing " + model.getModelType()+ "-NBA product as LTS...");
  		mainLog.flush();
  		LTSNBAProduct product = LTSNBAProduct.doProduct(model, nba, statesOfInterest, labelBS);
  		mainLog.println(" "+product.getProductModel().infoString()+", "+product.getAcceptingStates().cardinality()+" states accepting");
  
  		// Note: As the NBA is not guaranteed to be complete, the product may contain
  		// terminal states. The SCC computer can correctly deal with that.
  
  		if (product.getAcceptingStates().isEmpty()) {
  			mainLog.print("None of the states in the product are accepting, skipping further computations");
  			// If there are no accepting states, there is no accepting run, return all-false result
  			// Note: In the dual case, where all states are accepting, we nevertheless have to do the
  			// SCC analysis below, as there is no guarantee that there is actually a cycle (i.e., when
  			// eventually all runs reach terminal states in the product)
  			return StateValues.createFromBitSet(new BitSet(), model);
  		}
  
  		mainLog.print("Searching for non-trivial, accepting SCCs in product LTS...");
  		mainLog.flush();
  		SCCConsumerStore sccConsumerStore = new SCCConsumerStore();
  		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, product.getProductModel(), sccConsumerStore);
  		sccComputer.computeSCCs();
  
  		// We determine the SCCs that intersect F, as those are guaranteed to
  		// have at least one accepting cycle. This crucially relies on the fact
  		// that the SCC computer returns only non-trivial SCCs.
  		int accepting = 0;
  		int sccs = 0;
  		BitSet acceptingSCCs = new BitSet();
  		for (BitSet scc : sccConsumerStore.getSCCs()) {
  			sccs++;
  			if (scc.intersects(product.getAcceptingStates())) {
  				acceptingSCCs.or(scc);
  				accepting++;
  			}
  		}
  		mainLog.println(" "+accepting+" of "+sccs+" non-trivial SCCs are accepting");
  
  		BitSet allStates = new BitSet();
  		allStates.set(0, product.getProductModel().getNumStates());
  
  		// compute the set of states that can reach an accepting cycle,
  		// i.e., satisfy E[ true U acceptingSCCs ], using the CTL checker
  		mainLog.println("Computing reachability of accepting SCCs...");
  		BitSet resultProduct = computeExistsUntil(product.getProductModel(), allStates, acceptingSCCs);
  		StateValues svProduct = StateValues.createFromBitSet(resultProduct, product.getProductModel());
  
  		// we project to the original model
  		StateValues result = product.projectToOriginalModel(svProduct);
  
  		return result;
  	}
  
  }
  
  