//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Christian von Essen <christian.vonessen@imag.fr> (Verimag, Grenoble)
//	* 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.ArrayDeque;
import java.util.Arrays;
import java.util.BitSet;
import java.util.Deque;
import java.util.function.IntPredicate;

import prism.PrismComponent;
import prism.PrismException;

/**
 * Tarjan's SCC algorithm operating on a Model object, implemented
 * without recursion, i.e., using an explicit stack. This allows to
 * deal with deep models without exhausting the Java stack.
 */
public class SCCComputerTarjanIterative extends SCCComputer
{
	/* The model to compute (B)SCCs for */
	private Model model;
	/* Number of nodes (model states) */
	private int numNodes;

	/* Next index to give to a node */
	private int index = 0;
	/* Stack of nodes */
	private Deque<Integer> stack = new ArrayDeque<Integer>();
	/* Nodes currently on the stack. */
	private BitSet onStack = new BitSet();

	/** The lowlink information for the nodes (states) */
	private int[] nodeLowlink;
	/** The index information for the nodes (states) */
	private int[] nodeIndex;

	/** The stack for simulating the recursive calls of Tarjan's algorithm */
	private Deque<StackFrame> recursionStack = new ArrayDeque<>();

	/**
	 * Set to remember those states that had a direct self loop
	 * (to distinguish between trivial and non-trivial single state SCCs
	 * if we have to filter the former).
	 */
	private BitSet statesWithSelfloop;

	/** Should we filter trivial SCCs? */
	private boolean filterTrivialSCCs;

	/**
	 * (optional) A predicate to restrict the explored state space
	 * and transition relation to those states that satisfy restrict
	 */
	private IntPredicate restrict;

	/**
	 * Build (B)SCC computer for a given model.
	 */
	public SCCComputerTarjanIterative(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException
	{
		super(parent, consumer);
		this.model = model;
		this.numNodes = model.getNumStates();
		nodeLowlink = new int[numNodes];
		Arrays.fill(nodeLowlink, -1);
		nodeIndex = new int[numNodes];
		Arrays.fill(nodeIndex, -1);
	}

	// Methods for SCCComputer interface

	@Override
	public void computeSCCs(boolean filterTrivialSCCs, IntPredicate restrict) throws PrismException
	{
		this.filterTrivialSCCs = filterTrivialSCCs;
		if (filterTrivialSCCs)
			statesWithSelfloop = new BitSet();
		consumer.notifyStart(model);
		this.restrict = restrict;
		tarjan();
		consumer.notifyDone();
	}

	// SCC Computation

	/**
	 * Execute Tarjan's algorithm. Determine maximal strongly connected components
	 * (SCCS) for the graph of the model and report to the consumer.
	 */
	public void tarjan() throws PrismException
	{
		for (int i = 0; i < numNodes; i++) {
			if (restrict != null && !restrict.test(i))
				continue; // skip state if not one of the relevant states
			if (nodeLowlink[i] == -1) {
				beginVisit(i);
				loop();
			}
		}
	}

	/**
	 * Begin the visit to node i.
	 */
	private void beginVisit(int i)
	{
		// initialise index and lowindex
		nodeIndex[i] = index;
		nodeLowlink[i] = index;
		index++;
		// push on Tarjan stack
		stack.push(i);
		onStack.set(i);
		// push corresponding frame (state and successor iterator) on the recursion stack
		recursionStack.push(new StackFrame(i, model.getSuccessors(i)));
	}

	/** Main loop, process the recursion stack until empty */
	private void loop() throws PrismException
	{
		while (!recursionStack.isEmpty()) {
			StackFrame frame = recursionStack.peek();
			// the current node
			int v = frame.getNode();

			if (frame.hasPending()) {
				// first, finish the visit of the previous edge, if there was one
				int w = frame.getPending();
				nodeLowlink[v] = Math.min(nodeLowlink[v], nodeLowlink[w]);
			}

			final int w = frame.nextSuccessor(restrict);
			if (w != -1) {
				if (v == w) {
					// a self loop
					if (statesWithSelfloop != null)
						statesWithSelfloop.set(v);

					// ignore this edge, continue with loop
					frame.clearPending();
					continue;
				}

				if (nodeIndex[w] == -1) {
					// setup visit of successor w, then continue with loop
					beginVisit(w);
					continue;
				} else if (onStack.get(w)) {
					// back edge, update lowlink, don't explore successor
					nodeLowlink[v] = Math.min(nodeLowlink[v], nodeIndex[w]);
				}
				// the current edge v->w is not actually explored,
				// so we clear the pending successor (w) in the frame
				// and continue with the loop
				frame.clearPending();
				continue;
			}

			// no more successors for this frame, remove from recursion stack
			recursionStack.pop();

			// finished exploring node v, perform necessary steps
			if (nodeLowlink[v] == nodeIndex[v]) {
				// we have found the root node of an SCC

				// this is a singleton SCC if the top of the stack equals i
				boolean singletonSCC = (stack.peek() == v);
				if (singletonSCC && filterTrivialSCCs) {
					if (!statesWithSelfloop.get(v)) {
						// singleton SCC & no selfloop -> trivial
						// ignore this SCC and cleanup the Tarjan stack
						stack.pop();
						onStack.set(v, false);
						continue;
					}
				}

				int n;
				consumer.notifyStartSCC();
				do {
					n = stack.pop();
					onStack.set(n, false);
					consumer.notifyStateInSCC(n);
				} while (n != v);
				consumer.notifyEndSCC();
			}
		}
	}

	/**
	 * The stack frame with all the information for Tarjan's algorithm
	 * (current node, successor iterator, currently explored edge).
	 */ 
	private static class StackFrame {
		/** The current 'from' node */
		int node;
		/** The iterator over the successors */
		private SuccessorsIterator it;
		/** The successor that is currently explored (-1 = none) */
		private int pending = -1;

		/** Constructor */
		StackFrame(int node, SuccessorsIterator it) {
			this.node = node;
			this.it = it;
		}

		/** Get the current node */
		public int getNode()
		{
			return node;
		}

		/**
		 * Returns the next successor. If there is none, returns {@code -1}.
		 * If restrict is non-null, only those successors that satisfy restrict are returned.
		 */
		public int nextSuccessor(IntPredicate restrict)
		{
			while (it.hasNext()) {
				int i = it.nextInt();
				if (restrict != null && !restrict.test(i))
					// skip
					continue;

				pending = i;
				return i;
			}
			return -1;
		}

		/** Do we have a successor whose edge is currently explored? */
		public boolean hasPending()
		{
			return pending != -1;
		}

		/** Return (and clear) the current pending successor */
		public int getPending() {
			int p = pending;
			pending = -1;
			return p;
		}

		/** Clear the current pending successor */
		public void clearPending()
		{
			pending = -1;
		}

	}

}