// Transition class -*- c++ -*-

#ifndef TRANSITION_H_
# define TRANSITION_H_
# ifdef __GNUC__
#  pragma interface
# endif // __GNUC__

# include <string.h>
# include <assert.h>
# include <map>
# include <list>

# include "util.h"
# include "Error.h"

/** @file Transition.h
 * Transition in an algebraic system net
 */

/* Copyright  1998-2003,2005 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA 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, or (at your option)
   any later version.

   MARIA 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.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

/** Transition class */
class Transition
{
public:
  /** Kind of the transition */
  enum Kind {
    tNormal = 0,	//< Regular transition
    tUndefined,		//< A safety assertion that does not abort analysis
    tFatal		//< A safety assertion that aborts the analysis
  };
  /** Actions for unifiability test */
  enum Unif {
    uNormal = 0,//< Report variables that cannot be unified
    uIgnore,	//< Ignore gates and outputs
    uRemove	//< Remove gates depending on un-unifiable variables
  };
  /** List of gate expressions */
  typedef std::list<class Expression*> GateList;
  /** Map from names to variables defined in the transition */
  typedef std::map<const char*,class VariableDefinition*,
    struct ltstr> VariableMap;
  /** Iterator to the variable name map */
  typedef VariableMap::iterator iterator;
  /** Constant iterator to the variable name map */
  typedef VariableMap::const_iterator const_iterator;
  /** Map from names to functions defined in the transition */
  typedef std::map<const char*,class Function*,struct ltstr> FunctionMap;

  /** Constructor for anonymous transitions */
  Transition ();
  /** Constructor
   * @param net		the net this transition belongs to
   * @param i		index number of the transition (in the net)
   * @param name	name of the transition
   */
  Transition (class Net& net,
	      unsigned i,
	      char* name);
private:
  /** Copy constructor */
  Transition (const class Transition& old);
  /** Assignment operator */
  class Transition& operator= (const class Transition& old);
public:
  /** Destructor */
  ~Transition ();

  /** Get the net of the transition */
  const class Net* getNet () const { return myNet; }
  /** Get the index number of the transition in the local net */
  unsigned getLocalIndex () const { return myLocalIndex; }
  /** Get the index number of the transition in the root net */
  unsigned getRootIndex () const { return myRootIndex; }
  /** Set the index number of the transition in the root net */
  void setRootIndex (unsigned root) { myRootIndex = root; }
  /** Get the name of the transition */
  const char* getName () const { return myName; }

  /** Get the number of parents (0 if this is not a sync transition) */
  unsigned getNumParents () const { return myNumParents; }
  /** Get a parent of this transition by index number */
  const class Transition& getParent (unsigned i) const {
    assert (i < myNumParents);
    return *myParents[i];
  }

# ifndef NDEBUG
  /** Determine whether the transition has a specific parent
   * @param parent	parent transition to look for
   */
  bool hasParent (const class Transition& parent) const;
  /** Determine whether the transition has a specific child
   * @param child	child transition to look for
   */
  bool hasChild (const class Transition& child) const;
# endif // NDEBUG

  /** Change the parent transition to indicate synchronisation label
   * @param old		the old parent transition
   * @param fused	the new (fused) parent transition
   */
  void changeParent (const class Transition& old,
		     const class Transition& fused);
  /** Get the number of children the transition has */
  unsigned getNumChildren () const { return myNumChildren; }
  /** Get a child transition by index number */
  const class Transition& getChild (unsigned i) const {
    assert (i < myNumChildren);
    return *myChildren[i];
  }
  /** Register a sync transition in a child net
   * @param child	the child transition
   */
  void addChild (class Transition& child);

  /** Get the priority level (0=none) */
  unsigned getPriority () const { return myPriority; }
  /** Set the priority level (0=none) */
  void setPriority (unsigned priority) { myPriority = priority; }

  /** Get the kind of the transition */
  enum Kind getKind () const { return myKind; }
  /** Flag the transition an assertion
   * @param fatal	flag: is this a fatal assertion?
   */
  void setAssertion (bool fatal);

  /** Determine if a transition instance should be hidden
   * @param valuation	the valuation
   */
  bool isHidden (const class Valuation& valuation) const;

  /** Add an enabling condition (conjunct with existing condition)
   * @param gate	the enabling condition
   */
  void addGate (class Expression& gate);

  /** Add a hide condition (disjunct with existing condition)
   * @param qualifier	the hiding condition
   */
  void addHide (class Expression& qualifier);

  /** Add a fairness constraint
   * @param qualifier	transition instance qualifier expression
   * @param id		identifier of the fairness set
   * @param isStrong	flag: is this a strong fairness constraint
   * @return		number of fairness constraints
   */
  unsigned addFairness (class Expression& qualifier,
			unsigned id,
			bool isStrong);
  /** Add an enabledness constraint
   * @param qualifier	transition instance qualifier expression
   * @param id		identifier of the enabledness set
   * @return		number of fairness constraints
   */
  unsigned addEnabledness (class Expression& qualifier,
			   unsigned id);

  /** Get a variable by name
   * @param name	Name of the variable
   * @return		the VariableDefinition object; NULL if there is none
   */
  const class VariableDefinition* getVariable (const char* name) const {
    const_iterator i = myVariables.find (name);
    return i != myVariables.end () ? i->second : NULL;
  }

  /** Determine whether a variable is present on any of the input arcs
   * @param variable	variable to look for (NULL=PlaceContents)
   * @return		true if it is an input variable
   */
  bool isInput (const class VariableDefinition* variable) const;

  /** Determine whether a variable is present on any of the output arcs
   * @param variable	variable to look for (NULL=PlaceContents)
   * @return		true if it is an output variable
   */
  bool isOutput (const class VariableDefinition* variable) const;

  /** Determine whether a variable is present on a gate expression
   * @param variable	variable to look for (NULL=PlaceContents)
   * @return		true if the variable is used in a gate expression
   */
  bool isGate (const class VariableDefinition* variable) const;

  /** @name Accessors to the variable map */
  /*@{*/
  const_iterator begin () const { return myVariables.begin (); }
  const_iterator end () const { return myVariables.end (); }
  iterator begin () { return myVariables.begin (); }
  iterator end () { return myVariables.end (); }
  size_t size () const { return myVariables.size (); }
  /*@}*/
  /** @name Accessors to the gate expression list */
  /*@{*/
  GateList::const_iterator beginG () const { return myGates.begin (); }
  GateList::const_iterator endG () const { return myGates.end (); }
  /*@}*/

  /** Add an output variable
   * @param type	Type of the variable
   * @param name	Name of the variable (may be NULL)
   * @param expr	Condition expression for the quantification
   * @return		reference to the VariableDefinition object
   */
  const class VariableDefinition& addOutputVariable (const class Type& type,
						     char* name,
						     class Expression* expr);

  /** Get the quantifier list for the output variables of the transition */
  const class QuantifierList* getOutputVariables () const {
    return myOutputVariables;
  }

  /** Add a variable
   * @param name	Name of the variable
   * @param type	Type of the variable
   * @param aggregate	flag: is this an output variable (quantifier)?
   * @param hidden	flag: should the variable be hidden?
   * @return		reference to the VariableDefinition object
   */
  const class VariableDefinition& addVariable (char* name,
					       const class Type& type,
					       bool aggregate,
					       bool hidden);

  /** Get a function definition by name
   * @param name	Name of the function
   * @return		The function definition
   */
  class Function* getFunction (const char* name) {
    FunctionMap::const_iterator i = myFunctions.find (name);
    return i == myFunctions.end () ? NULL : i->second;
  }

  /** Add a function definition
   * @param function	The function
   */
  void addFunction (class Function& function);

  /** Check the gates
   * @param valuation	Valuation for evaluating the gate expressions
   * @param err		error code to accept (typically errVar or errNone)
   * @return		true if the gates allow the transition to be fired
   */
  bool checkGates (const class Valuation& valuation,
		   enum Error err = errVar) const;

  /** Add an arc
   * @param arc		The arc to be added
   */
  void addArc (class Arc& arc);
  /** Determine whether the transition has an arc from/to a place
   * @param output	specifies the type of arcs to look for
   * @param place	identifies the place
   * @return		the arc, or NULL
   */
  class Arc* getArc (bool output, const class Place& place);
  /** Determine whether the transition has input arcs */
  bool hasInputs () const { return myNumInputs != 0; }
  /** Determine whether the transition has output arcs */
  bool hasOutputs () const { return myNumOutputs != 0; }

  /** Determine the number of input arcs */
  unsigned getNumInputs () const { return myNumInputs; }
  /** Determine the number of output arcs */
  unsigned getNumOutputs () const { return myNumOutputs; }
  /** Get an input arc
   * @param i	index number of the arc
   */
  const class Arc& getInput (unsigned i) const {
    assert (i < myNumInputs); return *myInputs[i];
  }
  /** Get an output arc
   * @param i	index number of the arc
   */
  const class Arc& getOutput (unsigned i) const {
    assert (i < myNumOutputs); return *myOutputs[i];
  }

  /** Determine the number of weak fairness sets the transition belongs to */
  unsigned getNumWeaklyFair () const { return myNumWeaklyFair; }
  /** Determine the number of strong fairness sets the transition belongs to */
  unsigned getNumStronglyFair () const { return myNumStronglyFair; }
  /** Determine the number of enabledness sets the transition belongs to */
  unsigned getNumEnabled () const { return myNumEnabled; }

  /** Add a constant
   * @param name	name of the constant
   * @param constant	the constant
   * @return		true if the constant had a unique name
   */
  bool addConstant (char* name, class Constant& constant);
  /** Retrieve a constant by name
   * @param name	name of the constant
   * @return		the constant, or NULL if none found
   */
  const class Constant* getConstant (const char* name) const;

  /** Get the number of constants */
  unsigned getNumConstants () const { return myNumConstants; }

  /** Get the name of a constant
   * @param i		index number of the constant
   * @return		the name of the constant
   */
  const char* getConstantName (unsigned i) const {
    assert (i < myNumConstants);
    return myConstantNames[i];
  }

  /** Get a constant
   * @param i		index number of the constant
   * @return		the constant
   */
  const class Constant& getConstant (unsigned i) const {
    assert (i < myNumConstants);
    return *myConstants[i];
  }

  /** Fuse a callee transition to this one
   * @param callee	the transition to be fused
   * @param printer	the printer object for diagnostics
   * @param warn	flag: issue warnings
   * @return		true if the operation was successful
   */
  bool fuse (const class Transition& callee,
	     const class Printer& printer,
	     bool warn);

  /** Determine whether the transition can be unified
   * @param action	additional actions to take
   * @param printer	the printer object for diagnostics
   * @return		true if the transition can be unified
   */
  bool isUnifiable (enum Unif action,
		    const class Printer& printer);

  /** Determine all enabled instances of the transition for a marking
   * @param m		the marking to be analyzed
   * @param reporter	the interface for reporting successors or errors
   */
  void analyze (class GlobalMarking& m,
		class StateReporter& reporter) const;

  /** Report a rejected successor state
   * @param valuation	the transition binding
   * @param marking	the erroneous successor state
   * @param reason	reason for failure (optional)
   * @param place	the place whose marking could not be encoded (optional)
   * @param printer	the output stream for the message
   */
  void report (const class Valuation& valuation,
	       const class GlobalMarking& marking,
	       const char* reason,
	       const class Place* place,
	       const class Printer& printer) const;

  /** Display an edge to a successor state
   * @param valuation	the transition binding
   * @param marking	the successor state
   * @param printer	the output stream for the message
   */
  void displayEdge (const class Valuation& valuation,
		    const class GlobalMarking& marking,
		    const class Printer& printer) const;

  /** Unfold the transition with the help of a coverable marking
   * @param cover	(input/output) the coverable marking
   * @param lnet	the low-level net being generated
   * @param reporter	the reporting interface
   */
  void unfold (class GlobalMarking& cover,
	       class LNet& lnet,
	       class DummyReporter& reporter) const;

  /** Unfold the transition by iterating the variable domains
   * @param lnet	the low-level net being generated
   * @param reporter	the reporting interface
   */
  void unfold (class LNet& lnet,
	       class DummyReporter& reporter) const;

  /** Determine which weak fairness sets a transition instance belongs to
   * @param valuation	variable substitutions
   * @param sets	(output) sets[1..*sets]: weak fairness sets
   */
  void computeWeaklyFair (const class Valuation& valuation,
			  unsigned* sets) const;

  /** Determine which strong fairness sets a transition instance belongs to
   * @param valuation	variable substitutions
   * @param sets	(output) sets[1..*sets]: strong fairness sets
   */
  void computeStronglyFair (const class Valuation& valuation,
			    unsigned* sets) const;

  /** Log the enabled enabledness sets
   * @param valuation	variable substitutions
   * @param log		the enabledness sets
   */
  void logEnabled (const class Valuation& valuation,
		   char* log) const;

# ifdef EXPR_COMPILE
private:
  /** Compile transition instance analysis
   * @param cexpr	compilation output
   * @param inputPlaces	the input places
   * @param numOptVars	number of optional variables
   */
  void compileAnalysis (class CExpression& cexpr,
			const std::list<const class Place*>& inputPlaces,
			unsigned numOptVars) const;
public:
  /** Compile the expressions of the transition
   * @param out		the output stream
   */
  void compile (class StringBuffer& out) const;
# endif // EXPR_COMPILE

  /** Display the transition definition
   * @param printer	the printer object
   */
  void display (const class Printer& printer) const;

private:
  /** The net this transition belongs to */
  class Net* myNet;
  /** Index number of the transition in myNet */
  unsigned myLocalIndex;
  /** Index number of the transition in the root net */
  unsigned myRootIndex;
  /** Name of the transition */
  char* myName;
  /** Number of parent transitions */
  unsigned myNumParents;
  /** Parent transitions (for transitions in child nets) */
  const class Transition** myParents;
  /** Number of child transitions */
  unsigned myNumChildren;
  /** Child transitions in child nets */
  const class Transition** myChildren;
  /** Priority level (0=none) */
  unsigned myPriority;
  /** Kind of the transition */
  enum Kind myKind;
  /** Number of input arcs */
  unsigned myNumInputs;
  /** Input arcs */
  class Arc** myInputs;
  /** Number of output arcs */
  unsigned myNumOutputs;
  /** Output arcs */
  class Arc** myOutputs;
  /** Flag: do the outputs depend on the input marking? */
  bool myOutputMarking;

  /** List of tokens to be unified */
  struct unif* myUnif;

  /** Number of weak fairness sets */
  unsigned myNumWeaklyFair;
  /** Number of strong fairness sets */
  unsigned myNumStronglyFair;
  /** Number of enabledness sets */
  unsigned myNumEnabled;
  /** Weak fairness conditions */
  class Expression** myWeaklyFairCond;
  /** Strong fairness conditions */
  class Expression** myStronglyFairCond;
  /** Enabledness conditions */
  class Expression** myEnabledCond;
  /** Weak fairness sets */
  unsigned* myWeaklyFairSet;
  /** Strong fairness sets */
  unsigned* myStronglyFairSet;
  /** Enabledness sets */
  unsigned* myEnabledSet;

  /** Gate expressions */
  GateList myGates;
  /** Hiding condition */
  class Expression* myHide;

  /** Output variables */
  class QuantifierList* myOutputVariables;

  /** Transition variables indexed by name */
  VariableMap myVariables;

  /** Functions indexed by name */
  FunctionMap myFunctions;

  /** Number of constants */
  unsigned myNumConstants;
  /** Names of constants */
  char** myConstantNames;
  /** Constants */
  class Constant** myConstants;
};

#endif // TRANSITION_H_