//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	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 prism;

import java.io.*;
import java.util.*;

import jdd.*;
import odd.*;
import parser.*;

public interface Model
{
	ModelType getModelType();

	int getNumModules();
	String[] getModuleNames();
	String getModuleName(int i);
	
	int getNumVars();
	VarList getVarList();
	String getVarName(int i);
	int getVarIndex(String n);
	int getVarModule(int i);
	int getVarLow(int i);
	int getVarHigh(int i);
	int getVarRange(int i);
	Values getConstantValues();
	List<String> getSynchs();

	/**
	 * Returns the JDDNode for the state set (over the row variables)
	 * associated with the given label.
	 *
	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
	 * @param label the label
	 * @returns JDDNode for the label, {@code null} if none is stored
	 */
	JDDNode getLabelDD(String label);

	/**
	 * Returns true if a JDDNode state set for the given label
	 * is stored in the model.
	 */
	default boolean hasLabelDD(String label)
	{
		return getLabels().contains(label);
	}

	/**
	 * Get the (read-only) set of label names
	 * that are (optionally) stored in the model.
	 * Returns an empty set if there are none.
	 */
	Set<String> getLabels();

	/**
	 * Add a label with corresponding state set, ensuring a unique, non-existing label.
	 * The label will be either "X" or "X_i" where X is the content of the {@code prefix} argument
	 * and i is a non-negative integer.
	 * <br>
	 * Optionally, a set of defined label names can be passed so that those labels
	 * can be avoided. This can be obtained from the model checker via {@code getDefinedLabelNames()}.
	 * <br>
	 * Note that a stored label takes precedence over the on-the-fly calculation
	 * of an ExpressionLabel, cf. {@link explicit.StateModelChecker#checkExpressionLabel}
	 * <br>[ STORES: labelDD, deref on later call to clear() ]
	 *
	 * @param prefix the prefix for the unique label
	 * @param labelDD the JDDNode with the state set for the label
	 * @param definedLabelNames set of names (optional, may be {@code null}) to check for existing labels
	 * @return the generated unique label
	 */
	public String addUniqueLabelDD(String prefix, JDDNode labelDD, Set<String> definedLabelNames);

	String globalToLocal(long x);
	int globalToLocal(long x, int l);
	State convertBddToState(JDDNode dd);
	int convertBddToIndex(JDDNode dd) throws PrismNotSupportedException;

	StateList getReachableStates();
	
	/**
	 * Get a StateList storing the set of states that are/were deadlocks.
	 * (Such states may have been fixed at build-time by adding self-loops)
	 */
	StateList getDeadlockStates();
	
	StateList getStartStates();
	int getNumRewardStructs();
	long getNumStates();
	long getNumTransitions();
	long getNumStartStates();
	String getNumStatesString();
	String getNumTransitionsString();
	String getNumStartStatesString();

	JDDNode getTrans();
	JDDNode getTrans01();
	JDDNode getStart();
	JDDNode getReach();
	
	/**
	 * Get a BDD storing the underlying transition relation of the model.
	 * If it is not stored already, it will be computed.
	 */
	JDDNode getTransReln();
	
	/**
	 * Get a BDD storing the set of states that are/were deadlocks.
	 * (Such states may have been fixed at build-time by adding self-loops)
	 */
	JDDNode getDeadlocks();
	
	JDDNode getStateRewards();
	JDDNode getStateRewards(int i);
	JDDNode getStateRewards(String s);
	JDDNode getTransRewards();
	JDDNode getTransRewards(int i);
	JDDNode getTransRewards(String s);
	JDDNode getTransActions();
	JDDNode[] getTransPerAction();
	JDDVars[] getVarDDRowVars();
	JDDVars[] getVarDDColVars();
	JDDVars getVarDDRowVars(int i);
	JDDVars getVarDDColVars(int i);
	JDDVars[] getModuleDDRowVars();
	JDDVars[] getModuleDDColVars();
	JDDVars getModuleDDRowVars(int i);
	JDDVars getModuleDDColVars(int i);
	JDDVars getAllDDRowVars();
	JDDVars getAllDDColVars();
	int getNumDDRowVars();
	int getNumDDColVars();
	int getNumDDVarsInTrans();
	Vector<String> getDDVarNames();

	/** Get the information about the model variables */
	ModelVariablesDD getModelVariables();

	ODDNode getODD();

	void setSynchs(List<String> synchs);

	/**
	 * Stores a JDDNode state set (over the row variables)
	 * for the given label.<br>
	 * If the label already exists, the old state set is dereferenced
	 * and overwritten.
	 * <br>
	 * Note that a stored label takes precedence over the on-the-fly calculation
	 * of an ExpressionLabel, cf. {@link prism.StateModelChecker#checkExpressionLabel}
	 *
	 * <br>[ STORES: labelDD, deref on later call to clear() ]
	 * @param label the label name
	 * @param labelDD the JDDNode with the state set for the label
	*/
	void addLabelDD(String label, JDDNode labelDD);

	void resetTrans(JDDNode trans);
	void resetTransRewards(int i, JDDNode transRewards);
	void doReachability() throws PrismException;
	void skipReachability() throws PrismException;
	void setReach(JDDNode reach) throws PrismException;
	void setTransActions(JDDNode transActions); // MDPs only
	void setTransPerAction(JDDNode[] transPerAction); // D/CTMCs only
	void filterReachableStates();
	
	/**
	 * Find all deadlock states and store this information in the model.
	 * If requested (if fix=true) and if needed (i.e. for DTMCs/CTMCs),
	 * fix deadlocks by adding self-loops in these states.
	 * The set of deadlocks (before any possible fixing) can be obtained from {@link #getDeadlocks()}.
	 */
	void findDeadlocks(boolean fix);
	
	void printTrans();
	void printTrans01();
	public void printTransInfo(PrismLog log);
	public void printTransInfo(PrismLog log, boolean extra);
	void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException;
	
	/**
	 * Export (non-zero) state rewards for one reward structure of the model.
	 * @param r Index of reward structure to export (0-indexed)
	 * @param exportType The format in which to export
	 * @param file File to export to (if null, print to the log instead)
	 */
	void exportStateRewardsToFile(int r, int exportType, File file) throws FileNotFoundException, PrismException;
	
	@Deprecated
	String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException;
	
	/**
	 * Export (non-zero) transition rewards for one reward structure of the model.
	 * @param r Index of reward structure to export (0-indexed)
	 * @param exportType The format in which to export
	 * @param ordered Do the entries need to be printed in order?
	 * @param file File to export to (if null, print to the log instead)
	 */
	void exportTransRewardsToFile(int r, int exportType, boolean ordered, File file) throws FileNotFoundException, PrismException;

	@Deprecated
	String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException;

	void exportStates(int exportType, PrismLog log);

	void clear();
}

//------------------------------------------------------------------------------
