// Net class -*- c++ -*-

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

# include <assert.h>
# include <string.h>
# include <map>
# include <list>
# include "util.h"
# include "BitBuffer.h"

/** @file Net.h
 * Nested modular algebraic system net
 */

/* Copyright  1998-2003 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. */

/** Nested modular algebraic system net */
class Net
{
public:
  /** Map from names to functions */
  typedef std::map<const char*,class Function*,struct ltstr> FunctionMap;
  /** Map from names to places */
  typedef std::map<const char*,class Place*,struct ltstr> PlaceMap;
  /** Map from names to transitions */
  typedef std::map<const char*,class Transition*,struct ltstr> TransitionMap;
  /** Map from names to data types */
  typedef std::map<const char*,class Type*,struct ltstr> TypeMap;
  /** List of all data types (named and nameless ones) */
  typedef std::list<class Type*> TypeList;

  /** Constructor
   * @param ix		index number (0 for root net)
   * @param parent	parent net (optional)
   * @param parentix	the child index number in the parent net
   * @param name	the name of the net (optional)
   */
  Net (
# ifdef EXPR_COMPILE
       unsigned ix = 0,
# endif // EXPR_COMPILE
       class Net* parent = 0,
       unsigned parentix = 0,
       char* name = 0);
private:
  /** Copy constructor */
  Net (const class Net& old);
  /** Assignment operator */
  class Net& operator= (const class Net& old);
public:
  /** Destructor */
  ~Net ();

# ifdef EXPR_COMPILE
  /** Get the index number of this net */
  unsigned getIndex () const { return myIndex; }
  /** Get the number of callee transitions in this net */
  unsigned getNumCallees () const { return myNumCallees; }
  /** Get a callee transition by number */
  class Transition& getCallee (unsigned i) const {
    assert (i < myNumCallees); return *myCallees[i];
  }
  /** Get the number of compiled transitions */
  unsigned getNumCompiled () const { return myNumCompiled; }
  /** Set the number of compiled transitions */
  void setNumCompiled (unsigned n) const {
    assert (n >= myNumAllTransitions); myNumCompiled = n;
  }
# endif // EXPR_COMPILE

  /** Get the optional name of this net */
  const char* getName () const { return myName; }
  /** Get the parent of this net (0 if this is not a child net) */
  class Net* getParent () { return myParent; }
  /** Get the parent of this net (0 if this is not a child net) */
  const class Net* getParent () const { return myParent; }
  /** Get the index number of a child net in its parent */
  unsigned getParentIndex () const { return myParentIndex; }
  /** Get the number of children in the net */
  unsigned getNumChildren () const { return myNumChildren; }
  /** Get a child net by index */
  const class Net& getChild (unsigned i) const {
    assert (i < myNumChildren); return *myChildren[i];
  }

  /** Add a child net to this net
   * @param name	optional name of the child net
   * @return		a reference to the newly created subnet
   */
  class Net& addChild (char* name);
private:
  /** Import needed places from parent nets
   * @param t		the transition to be processed
   */
  void addPlaces (const class Transition& t);
public:
  /** Get the highest available priority level */
  unsigned getMaxPriority () { return --myMaxPriority; }

  /** 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 = myFunctionMap.find (name);
    return i == myFunctionMap.end () ? NULL : i->second;
  }

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

  /** Fairness or enabledness constraint kind */
  enum CKind { Weak, Strong, Enabled };

  /** Add a fairness or enabledness constraint
   * @param qualifier	transition qualifier expression
   * @param kind	type of the constraint
   * @return		true if everything succeeded
   */
  bool addConstraint (class Expression& qualifier,
		      enum CKind kind);

  /** Add a fairness or an enabledness constraint to a transition
   * @param qualifier	transition instance qualifier expression
   * @param transition	the transition
   * @param kind	type of the constraint
   * @return		true if everything succeeded
   */
  bool addConstraint (class Expression& qualifier,
		      class Transition& transition,
		      enum CKind kind);

  /** Determine the number of weak fairness sets */
  unsigned getNumWeaklyFair () const { return myNumWeaklyFair; }
  /** Determine the number of strong fairness sets */
  unsigned getNumStronglyFair () const { return myNumStronglyFair; }
  /** Determine the maximum number of fairness constraints per transition */
  unsigned getNumMaxFair () const { return myNumMaxFair; }
  /** Determine the number of enabledness sets */
  unsigned getNumEnabled () const { return myNumEnabled; }

  /** Add a reject condition (assertion)
   * @param expr	the reject condition
   */
  void addReject (class Expression& expr);

  /** Add a deadlock monitor condition
   * @param expr	the deadlock condition
   */
  void addDeadlock (class Expression& expr);

  /** Get the reject condition */
  class Expression* getReject () const { return myReject; }
  /** Get the deadlock condition */
  class Expression* getDeadlock () const { return myDeadlock; }

  /** Get the number of places in the net */
  unsigned getNumPlaces () const { return myNumPlaces; }
  /** Get a place
   * @param i		Index number of the place
   */
  const class Place* getPlace (unsigned i) const {
    assert(i < myNumPlaces); return myPlaces[i];
  }
  /** Get a place
   * @param name	Name of the place
   */
  const class Place* getPlace (const char* name) const {
    PlaceMap::const_iterator i = myPlaceMap.find (name);
    return i == myPlaceMap.end () ? NULL : i->second;
  }

  /** Get the number of local transitions in the net */
  unsigned getNumTransitions () const { return myNumTransitions; }
  /** Get the number of local and flattened transitions in the net */
  unsigned getNumAllTransitions () const { return myNumAllTransitions; }
  /** Get a transition
   * @param i		Index number of the transition
   */
  const class Transition& getTransition (unsigned i) const {
    assert(i < myNumAllTransitions); return *myTransitions[i];
  }
  /** Get a transition
   * @param name	Name of the transition
   */
  class Transition* getTransition (const char* name) {
    TransitionMap::const_iterator i = myTransitionMap.find (name);
    return i == myTransitionMap.end () ? NULL : i->second;
  }
  /** Get a callee
   * @param name	name of the transition
   * @param except	do not return this transition, search in parent instead
   * @return		the transition, or 0 if not found
   */
  class Transition* getCallee (const char* name,
			       const class Transition* except) {
    for (const class Net* net = this;;) {
      TransitionMap::const_iterator i = net->myCalleeMap.find (name);
      if (i != net->myCalleeMap.end () && i->second != except)
	return i->second;
      else if (except && net == this && myParent)
	net = myParent;
      else
	break;
    }
    return 0;
  }

  /** Get a type
   * @param name	Name of the type
   */
  const class Type* getType (const char* name) const {
    TypeMap::const_iterator i = myTypeMap.find (name);
    return i == myTypeMap.end () ? NULL : i->second;
  }
  /** @name Accessors to the type list */
  /*@{*/
  TypeList::const_iterator begin () const { return myTypeList.begin (); }
  TypeList::const_iterator end () const { return myTypeList.end (); }
  /*@}*/
  /** Determine whether the net contains a type
   * @param type	Type to be sought
   * @return		true if the net contains the type
   */
  bool hasType (const class Type& type) const {
    for (TypeList::const_iterator i = begin (); i != end (); i++)
      if ((*i) == &type)
	return true;
    return false;
  }
  /** @name Accessors to the type name map */
  /*@{*/
  TypeMap::const_iterator beginTypename () const { return myTypeMap.begin (); }
  TypeMap::const_iterator endTypename () const { return myTypeMap.end (); }
  /*@}*/

  /** Get the initial marking of the net */
  const class GlobalMarking* getInitMarking () const { return myInitMarking; }
  /** Get the initial marking of the net */
  class GlobalMarking* getInitMarking () { return myInitMarking; }

  /** Add a place to the net
   * @param name	Name of the place
   * @param capacity	Capacity constraint of the place
   * @param type	Type of the place
   * @return		reference to the place
   */
  class Place& addPlace (char* name, class Constraint* capacity,
			 const class Type& type);

  /** Add a transition to the net
   * @param name	Name of the transition
   * @param callee	Flag: is this a callee transition?
   * @return		reference to the transition
   */
  class Transition& addTransition (char* name, bool callee);

  /** Add a type to the net
   * @param type	Type to be added
   * @param name	Name of the type
   */
  void addType (class Type& type, char* name = 0);

  /** Add a state proposition
   * @param name	name of the state proposition
   * @param prop	the state proposition
   * @return		true if the proposition had a unique name
   */
  bool addProp (char* name, class Expression& prop);

  /** Check the state propositions in a state
   * @param m		the state
   * @param operation	operation to invoke on propositions that hold
   * @param data	extra data to pass to the operation
   * @return		true if all operations succeeded
   */
  bool checkProps (const class GlobalMarking& m,
		   bool (*operation) (unsigned, const void*),
		   const void* data) const;

  /** Get the number of state propositions */
  unsigned getNumProps () const { return myNumProps; }

  /** Get the name of a state proposition
   * @param i		index number of the state proposition
   * @return		the name of the state proposition
   */
  const char* getPropName (unsigned i) const {
    assert (i < myNumProps);
    return myPropNames[i];
  }

  /** Get a state proposition
   * @param i		index number of the state proposition
   * @return		the state proposition
   */
  const class Expression& getProp (unsigned i) const {
    assert (i < myNumProps);
    return *myProps[i];
  }

  /** 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];
  }

private:
  /** Create fused transitions for all sync transitions in all subnets
   * @param printer	The printer object for diagnostic output
   * @return		true if the operation succeeded
   */
  bool addSyncTrans (const class Printer& printer);

  /** Add local transitions to the flattened root net
   * @param root	the root net
   */
  void addLocalTransitions (class Net& root) const;

public:
  /** Prepare a modular net for analysis
   * @param printer	The printer object for diagnostic output
   * @return		true if the system was successfully translated
   */
  bool prepareModular (const class Printer& printer);

  /** Compute the initial marking of the net (@see getInitMarking)
   * @param printer	The printer object for diagnostic output
   * @return		true if the operation succeeded
   */
  bool computeInitMarking (const class Printer& printer);

  /** Get the boolean type */
  static const class BoolType& getBoolType ();
  /** Get the signed integer type */
  static const class IntType& getIntType ();
  /** Get the unsigned integer type */
  static const class CardType& getCardType ();
  /** Get the character type */
  static const class CharType& getCharType ();

  /** Rejection or deadlock status */
  enum Status {
    OK = 0,	//< No error
    Error,	//< Non-fatal error (report and continue the search)
    Fatal	//< Fatal error (abort the search)
  };

  /** Determine whether a state is rejected
   * @param m		the state
   * @param flattened	flag: consider the reject statements in subnets
   * @return		true if the state is rejected
   */
  enum Status isReject (const class GlobalMarking& m,
			bool flattend) const;

  /** Check and whethera a deadlock state should be reported
   * @param m		the deadlock state
   * @param flattened	flag: consider the deadlock statements in subnets
   * @return		true if the deadlock should be reported
   */
  enum Status isDeadlock (const class GlobalMarking& m,
			  bool flattened) const;

  /** Determine whether a type is predefined
   * @param type	type to be checked
   * @return		true if the type is predefined
   */
  static bool isPredefinedType (const class Type& type);

  /** Encode a transition instance
   * @param buf		buffer for the encoded data
   * @param transition	the high-level transition
   * @param valuation	variable definitions
   * @param flattened	consider the flattened net
   */
  void encode (class BitPacker& buf,
	       const class Transition& transition,
	       const class Valuation& valuation,
	       bool flattened) const;

  /** Decode a transition instance
   * @param buf		the encoded data buffer
   * @param transition	(output parameter) the transition
   * @param valuation	(output parameter) the variable bindings
   * @param flattened	consider the flattened net
   */
  void decode (class BitUnpacker& buf,
	       const class Transition*& transition,
	       class Valuation& valuation,
	       bool flattened) const;

# ifdef EXPR_COMPILE
  /** Compile an encoding function
   * @param cexpr	the compilation
   */
  void compileEncoder (class CExpression& cexpr) const;

  /** Compile an decoding function
   * @param cexpr	the compilation
   */
  void compileDecoder (class CExpression& cexpr) const;

  /** Compile a projection function
   * @param cexpr	the compilation
   */
  void compileProjection (class CExpression& cexpr) const;

  /** Compile the reject tester formula
   * @param cexpr	the compilation
   */
  void compileReject (class CExpression& cexpr) const;
  /** Compile the deadlock tester formula
   * @param cexpr	the compilation
   */
  void compileDeadlock (class CExpression& cexpr) const;

  /** Compile the state properties
   * @param cexpr	the compilation
   * @param operation	name of the "operation" parameter
   * @param data	name of the "data" parameter
   */
  void compileProps (class CExpression& cexpr,
		     const char* operation,
		     const char* data) const;

  /** Compile constant declarations
   * @param out		the output stream
   * @param ext		the "extern" prefix, or NULL if this not a header entry
   */
  void compileConstantDecl (class StringBuffer& out,
			    const char* ext) const;
  /** Compile constant initializations
   * @param out		the output stream
   */
  void compileConstantInit (class StringBuffer& out) const;
# endif // EXPR_COMPILE

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

private:
# ifdef EXPR_COMPILE
  /** Index number of the net (0=parent) */
  const unsigned myIndex;
  /** Number of descendent nets (for the root net) */
  unsigned myNumDescendents;
  /** Number of compiled transitions (at least myNumAllTransitions) */
  mutable unsigned myNumCompiled;
# endif // EXPR_COMPILE
  /** Name of the net (for child nets) */
  char* const myName;
  /** Parent net (for child nets) */
  class Net* const myParent;
  /** Index in the parent (for child nets) */
  const unsigned myParentIndex;
  /** Number of child nets */
  unsigned myNumChildren;
  /** Child nets */
  class Net** myChildren;

  /** Highest available priority level */
  unsigned myMaxPriority;

  /** Number of places in the net */
  unsigned myNumPlaces;
  /** Places in the net */
  class Place** myPlaces;
  /** Number of transitions in the net */
  unsigned myNumTransitions;
  /** Number of flattened transitions in the net */
  unsigned myNumAllTransitions;
  /** Transitions in the net */
  class Transition** myTransitions;
  /** Number of callee transitions in the net */
  unsigned myNumCallees;
  /** Callee transitions in the net */
  class Transition** myCallees;

  /** Functions indexed by name */
  FunctionMap myFunctionMap;
  /** Places indexed by name */
  PlaceMap myPlaceMap;
  /** Transitions indexed by name */
  TransitionMap myTransitionMap;
  /** Callee transitions indexed by name */
  TransitionMap myCalleeMap;
  /** Types indexed by name */
  TypeMap myTypeMap;
  /** All types in the net (also nameless ones) */
  TypeList myTypeList;
  /** Initial marking of the net */
  class GlobalMarking* myInitMarking;

  /** Condition for reject tester */
  class Expression* myReject;
  /** Condition for deadlock tester */
  class Expression* myDeadlock;

  /** Number of weak fairness sets */
  unsigned myNumWeaklyFair;
  /** Number of strong fairness sets */
  unsigned myNumStronglyFair;
  /** Maximum number of fairness constraints per transition */
  unsigned myNumMaxFair;
  /** Number of enabledness sets */
  unsigned myNumEnabled;

  /** Number of state propositions */
  unsigned myNumProps;
  /** Names of state propositions */
  char** myPropNames;
  /** State propositions */
  class Expression** myProps;

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

#endif // NET_H_