//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham)
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	* Vincent Nimal <vincent.nimal@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 userinterface.properties.computation;

import java.util.*;
import javax.swing.*;

import parser.*;
import parser.ast.*;
import prism.*;
import simulator.method.SimulationMethod;
import userinterface.*;
import userinterface.util.*;
import userinterface.properties.*;

/**
 * Thread that executes approximate (simulation-based) model checking of a property via PRISM.
 * Model should have been loaded into PRISM already. Supplied are:
 * properties file (constants defined), list of properties to
 * be (approximately) verified and initial state (default/random if null).
 */
public class SimulateModelCheckThread extends GUIComputationThread
{
	private GUIMultiProperties parent;
	private PropertiesFile pf;
	private ArrayList<GUIProperty> guiProps;
	private Values definedPFConstants;
	private long maxPathLength;
	private SimulationInformation info;

	/** Creates a new instance of SimulateModelCheckThread */
	public SimulateModelCheckThread(GUIMultiProperties parent, PropertiesFile prFi, ArrayList<GUIProperty> guiProps,
			Values definedPFConstants, SimulationInformation info)
	{
		super(parent);
		this.parent = parent;
		this.pf = prFi;
		this.guiProps = guiProps;
		this.definedPFConstants = definedPFConstants;
		this.info = info;
		this.maxPathLength = info.getMaxPathLength();
	}

	public void run()
	{
		boolean allAtOnce = prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS);

		SimulationMethod method = info.createSimulationMethod();

		//Notify user interface of the start of computation
		SwingUtilities.invokeLater(new Runnable()
		{
			public void run()
			{
				parent.startProgress();
				parent.setTaskBarText("Checking properties using simulation...");
				parent.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_START, parent));
			}
		});

		//Set icon for all properties to be verified to a clock
		for (int i = 0; i < guiProps.size(); i++) {
			GUIProperty gp = guiProps.get(i);
			gp.setStatus(GUIProperty.STATUS_DOING);
			parent.repaintList();
		}

		// do all at once if requested
		if (allAtOnce) {
			Result results[] = null;
			Exception resultError = null;
			ArrayList<Expression> properties = new ArrayList<Expression>();
			ArrayList<IconThread> clkThreads = new ArrayList<IconThread>();
			for (int i = 0; i < guiProps.size(); i++) {
				GUIProperty gp = guiProps.get(i);
				properties.add(gp.getProperty());
				IconThread ict = new IconThread(gp);
				ict.start();
				clkThreads.add(ict);
			}

			try {
				// convert initial Values -> State
				// (remember: null means use default or pick randomly)
				parser.State initialState;
				if (info.getInitialState() == null) {
					initialState = null;
				} else {
					initialState = new parser.State(info.getInitialState(), prism.getPRISMModel());
				}
				// do simulation
				results = prism.modelCheckSimulatorSimultaneously(pf, properties, definedPFConstants, initialState, maxPathLength, method);
				method.reset();
			} catch (Exception e) {
				// in the case of an error which affects all props, store/report it
				resultError = e;
				error(e);
			} catch (StackOverflowError e) {
				// in the case of an error which affects all props, store/report it
				// convert to a PrismException for result
				resultError = new PrismException("Stack overflow");
				error(e);
			}
			//after collecting the results stop all of the clock icons
			for (int i = 0; i < clkThreads.size(); i++) {
				IconThread ict = (IconThread) clkThreads.get(i);
				ict.interrupt();
				while (!ict.canContinue) {
					try {
						Thread.sleep(10);
					} catch (InterruptedException e) {
						return;
					}
				}
			}

			// store results
			ModelType currentModelType = prism.getModelType();
			String methodString = "Simulation";
			if (currentModelType.nondeterministic() && currentModelType.removeNondeterminism() != currentModelType) {
				methodString += " (nondeterminism in " + currentModelType.name() + " resolved uniformly)";
			}

			for (int i = 0; i < guiProps.size(); i++) {
				GUIProperty gp = guiProps.get(i);
				gp.setResult((results == null) ? new Result(resultError) : results[i]);
				gp.setMethodString(methodString);
				gp.setNumberOfWarnings(prism.getMainLog().getNumberOfWarnings());
			}
		}
		// do each property individually
		else {
			Result result = null;
			for (int i = 0; i < pf.getNumProperties(); i++) {
				// get property
				GUIProperty gp = guiProps.get(i);
				// animate it's clock icon
				IconThread ict = new IconThread(gp);
				ict.start();
				// do model checking
				try {
					// convert initial Values -> State
					// (remember: null means use default or pick randomly)
					parser.State initialState;
					if (info.getInitialState() == null) {
						initialState = null;
					} else {
						initialState = new parser.State(info.getInitialState(), prism.getPRISMModel());
					}
					// do simulation
					result = prism.modelCheckSimulator(pf, pf.getProperty(i), definedPFConstants, initialState, maxPathLength, method);
					method.reset();
				} catch (Exception e) {
					result = new Result(e);
					error(e);
				} catch (StackOverflowError e) {
					// store as PrismException in result
					result = new Result(new PrismException("Stack overflow"));
					error(e);
				}
				ict.interrupt();
				while (!ict.canContinue) {
					try {
						Thread.sleep(10);
					} catch (InterruptedException e) {
						return;
					}
				}
				gp.setResult(result);
				gp.setMethodString("Simulation");

				parent.repaintList();
			}
		}
		SwingUtilities.invokeLater(new Runnable()
		{
			public void run()
			{
				parent.stopProgress();
				parent.setTaskBarText("Checking properties using simulation... done.");
				parent.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, parent));
				parent.notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.VERIFY_END));
			}
		});
	}

	class IconThread extends Thread
	{
		GUIProperty gp;
		ImageIcon[] images;
		boolean canContinue = false;

		public IconThread(GUIProperty gp)
		{
			this.gp = gp;
			images = new ImageIcon[8];
			images[0] = GUIPrism.getIconFromImage("smallClockAnim1.png");
			images[1] = GUIPrism.getIconFromImage("smallClockAnim2.png");
			images[2] = GUIPrism.getIconFromImage("smallClockAnim3.png");
			images[3] = GUIPrism.getIconFromImage("smallClockAnim4.png");
			images[4] = GUIPrism.getIconFromImage("smallClockAnim5.png");
			images[5] = GUIPrism.getIconFromImage("smallClockAnim6.png");
			images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png");
			images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png");
		}

		public void run()
		{
			try {
				int counter = 0;
				while (!interrupted() && gp != null) {
					//System.out.println("counter = " + counter);
					counter++;
					counter = counter % 8;
					gp.setDoingImage(images[counter]);
					parent.repaintList();
					sleep(150);
				}
			} catch (InterruptedException e) {
			} finally {
				canContinue = true;
			}
		}
	}
}
