prism-accumulation/prism/src/explicit/LTSNBAProduct.java

//==============================================================================
//	
//	Copyright (c) 2016-
//	Authors:
//	* 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.ArrayList;
import java.util.BitSet;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Stack;
import java.util.Vector;

import prism.PrismLog;
import common.IterableBitSet;
import common.IterableStateSet;
import jltl2ba.APElement;
import jltl2ba.APSet;
import jltl2dstar.NBA;
import jltl2dstar.NBA_State;

/**
 * Construction and storage for the product
 * of the underlying labeled transition system
 * of a model (i.e., the edge relation defined
 * by getSuccessorsIterator()) and a non-deterministic
 * Büchi automaton (NBA).
 */
public class LTSNBAProduct extends Product<Model>
{
	/** A product state */
	private static class ProductState {
		/** The model state */
		private int modelState;
		/** The automaton state */
		private int automatonState;

		/** Constructor */
		public ProductState(int modelState, int automatonState)
		{
			this.modelState = modelState;
			this.automatonState = automatonState;
		}

		/** Get model state */
		public int getModelState()
		{
			return modelState;
		}

		/** Get automaton state */
		public int getAutomatonState()
		{
			return automatonState;
		}
		
		public String toString() {
			return "(" + getModelState() + "," + getAutomatonState() +")";
		}

		@Override
		public int hashCode()
		{
			final int prime = 31;
			int result = 1;
			result = prime * result + automatonState;
			result = prime * result + modelState;
			return result;
		}

		@Override
		public boolean equals(Object obj)
		{
			if (this == obj)
				return true;
			if (obj == null)
				return false;
			if (!(obj instanceof ProductState))
				return false;
			ProductState other = (ProductState) obj;
			if (automatonState != other.automatonState)
				return false;
			if (modelState != other.modelState)
				return false;
			return true;
		}
	}

	/** Map state in product -> product state information */
	private ArrayList<ProductState> productStates;
	/** Accepting Büchi states in the product */
	private BitSet acceptingStates;

	/** Constructor for storing the product */
	private LTSNBAProduct(LTS productModel, Model originalModel, ArrayList<ProductState> productStates, BitSet acceptingStates)
	{
		super(productModel, originalModel);
		this.productStates = productStates;
		this.acceptingStates = acceptingStates;
	}

	@Override
	public int getModelState(int productState)
	{
		return productStates.get(productState).modelState;
	}

	@Override
	public int getAutomatonState(int productState)
	{
		return productStates.get(productState).automatonState;
	}

	/** Print the mapping between product state indizes and product states */
	public void printStateMapping(PrismLog log)
	{
		for (int i =0; i < productStates.size(); i++) {
			log.println(i + ": " + productStates.get(i) + (acceptingStates.get(i) ? " !":""));
		}
	}

	/** Get the Büchi states for the product */
	public BitSet getAcceptingStates()
	{
		return acceptingStates;
	}

	/**
	 * Construct the product.
	 *
	 * @param model the model
	 * @param nba the nondeterministic Büchi automaton
	 * @param statesOfInterest the states in the model that serve as the starting point for the product
	 * @param labelBS vector of state sets for the atomic propositions L0, L1, ... in the automaton
	 */
	public static LTSNBAProduct doProduct(Model model, NBA nba, BitSet statesOfInterest, Vector<BitSet> labelBS)
	{
		// map state index in product automaton -> ProductState
		ArrayList<ProductState> productIdToProductState = new ArrayList<ProductState>();
		// map ProductState -> state index in product automaton
		HashMap<ProductState, Integer> productStateToProductId = new HashMap<ProductState, Integer>();

		// storage for the product model
		LTSExplicit productModel = new LTSExplicit();
		// the accepting states in the product model
		BitSet acceptingStates = new BitSet();

		// the stack of product ids that potentially have to be expanded
		Stack<Integer> todo = new Stack<Integer>();

		// product state ids that have already been expanded
		BitSet expanded = new BitSet();

		// Note: In contrast to the deterministic automaton product elsewhere in
		// PRISM, the automaton step delta(q,l(s)) is done when leaving the product
		// state, not when entering. As we are only interested in the infinite behaviour,
		// this doesn't change acceptance at all:
		//
		//     <s,q> -> <s',q'>  where s->s' in the model and q' in delta(q, l(s))
		//
		// Thus, the initial states in the product are <s, q_0> for s in the states of interest
		// of the model and q_0 the initial state of the NBA.

		NBA_State nbaStart = nba.getStartState();
		if (nbaStart == null) {
			// no start state = rejecting
			// to simplify treatment, add a dummy start state
			// with no outgoing transitions
			nbaStart = nba.newState();
			nba.setStartState(nbaStart);
		}

		// Note: As the NBA currently is guaranteed to have a single initial state,
		// the product has exactly one initial product state per model state of interest.
		// This allows the use of the "normal" projection back from the product result to
		// the original model. For multiple initial NBA states, it would be necessary
		// to aggregate the results over all initial NBA states when projecting back to
		// the original model.

		// for each model state of interest ...
		for (int modelState : new IterableStateSet(statesOfInterest, model.getNumStates())) {
			// ... construct a product state (modelState, nbaStart)
			ProductState p = new ProductState(modelState, nbaStart.getName());

			productIdToProductState.add(p);
			int id = productModel.addState();
			productModel.addInitialState(id);
			assert ( id == productIdToProductState.size()-1 );
			productStateToProductId.put(p, id);
			todo.push(id);
			if (nbaStart.isFinal()) {
				acceptingStates.set(id);
			}
		}
		
		final APSet nbaAPSet = nba.getAPSet();

		while (!todo.isEmpty()) {
			int fromId = todo.pop();
			if (expanded.get(fromId))
				continue;

			ProductState from = productIdToProductState.get(fromId);

			// construct edge label from the labeling of the model state
			APElement label = new APElement(nbaAPSet.size());
			for (int k = 0; k < nbaAPSet.size(); k++) {
				label.set(k, labelBS.get(Integer.parseInt(nbaAPSet.getAP(k).substring(1))).get(from.getModelState()));
			}

			// the current state in the NBA
			NBA_State fromNBA = nba.get(from.getAutomatonState());
			// the successors in the NBA for the label corresponding to the model state
			BitSet nbaSuccessors = fromNBA.getEdge(label);
			// for each successor of the model state ...
			for (Iterator<Integer> it = model.getSuccessorsIterator(from.getModelState()); it.hasNext(); ) {
				Integer modelTo = it.next();
				// ... and NBA successor ...
				for (Integer nbaSuccessor : IterableBitSet.getSetBits(nbaSuccessors)) {
					// ... construct product state
					ProductState successor = new ProductState(modelTo, nbaSuccessor);
					Integer successorID = productStateToProductId.get(successor);
					if (successorID == null) {
						// newly discovered, add as state to the product model
						productIdToProductState.add(successor);
						successorID = productModel.addState();
						assert ( successorID == productIdToProductState.size()-1 );
						productStateToProductId.put(successor, successorID);
						// mark as todo
						todo.push(successorID);
						boolean isAccepting = nba.get(nbaSuccessor).isFinal();
						if (isAccepting) {
							acceptingStates.set(successorID);
						}
					}

					// add the edge
					productModel.addEdge(fromId, successorID);
				}

				// fromId is fully expanded in the product
				expanded.set(fromId);
			}
		}

		return new LTSNBAProduct(productModel, model, productIdToProductState, acceptingStates);
	}
}