Logo Search packages:      
Sourcecode: maria version File versions

Net.h

Go to the documentation of this file.
// 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 Mäkelä (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 */
00041 class Net
{
public:
  /** Map from names to functions */
00045   typedef std::map<const char*,class Function*,struct ltstr> FunctionMap;
  /** Map from names to places */
00047   typedef std::map<const char*,class Place*,struct ltstr> PlaceMap;
  /** Map from names to transitions */
00049   typedef std::map<const char*,class Transition*,struct ltstr> TransitionMap;
  /** Map from names to data types */
00051   typedef std::map<const char*,class Type*,struct ltstr> TypeMap;
  /** List of all data types (named and nameless ones) */
00053   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 */
00095   const char* getName () const { return myName; }
  /** Get the parent of this net (0 if this is not a child net) */
00097   class Net* getParent () { return myParent; }
  /** Get the parent of this net (0 if this is not a child net) */
00099   const class Net* getParent () const { return myParent; }
  /** Get the index number of a child net in its parent */
00101   unsigned getParentIndex () const { return myParentIndex; }
  /** Get the number of children in the net */
00103   unsigned getNumChildren () const { return myNumChildren; }
  /** Get a child net by index */
00105   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 */
00121   unsigned getMaxPriority () { return --myMaxPriority; }

  /** Get a function definition by name
   * @param name  Name of the function
   * @return            The function definition
   */
00127   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 */
00138   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 */
00159   unsigned getNumWeaklyFair () const { return myNumWeaklyFair; }
  /** Determine the number of strong fairness sets */
00161   unsigned getNumStronglyFair () const { return myNumStronglyFair; }
  /** Determine the maximum number of fairness constraints per transition */
00163   unsigned getNumMaxFair () const { return myNumMaxFair; }
  /** Determine the number of enabledness sets */
00165   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 */
00178   class Expression* getReject () const { return myReject; }
  /** Get the deadlock condition */
00180   class Expression* getDeadlock () const { return myDeadlock; }

  /** Get the number of places in the net */
00183   unsigned getNumPlaces () const { return myNumPlaces; }
  /** Get a place
   * @param i           Index number of the place
   */
00187   const class Place* getPlace (unsigned i) const {
    assert(i < myNumPlaces); return myPlaces[i];
  }
  /** Get a place
   * @param name  Name of the place
   */
00193   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 */
00199   unsigned getNumTransitions () const { return myNumTransitions; }
  /** Get the number of local and flattened transitions in the net */
00201   unsigned getNumAllTransitions () const { return myNumAllTransitions; }
  /** Get a transition
   * @param i           Index number of the transition
   */
00205   const class Transition& getTransition (unsigned i) const {
    assert(i < myNumAllTransitions); return *myTransitions[i];
  }
  /** Get a transition
   * @param name  Name of the transition
   */
00211   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
   */
00220   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
   */
00237   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
   */
00250   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 */
00263   const class GlobalMarking* getInitMarking () const { return myInitMarking; }
  /** Get the initial marking of the net */
00265   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 */
00307   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
   */
00313   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
   */
00322   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 */
00340   unsigned getNumConstants () const { return myNumConstants; }

  /** Get the name of a constant
   * @param i           index number of the constant
   * @return            the name of the constant
   */
00346   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
   */
00355   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 */
00395   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) */
00506   char* const myName;
  /** Parent net (for child nets) */
00508   class Net* const myParent;
  /** Index in the parent (for child nets) */
00510   const unsigned myParentIndex;
  /** Number of child nets */
00512   unsigned myNumChildren;
  /** Child nets */
00514   class Net** myChildren;

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

  /** Number of places in the net */
00520   unsigned myNumPlaces;
  /** Places in the net */
00522   class Place** myPlaces;
  /** Number of transitions in the net */
00524   unsigned myNumTransitions;
  /** Number of flattened transitions in the net */
00526   unsigned myNumAllTransitions;
  /** Transitions in the net */
00528   class Transition** myTransitions;
  /** Number of callee transitions in the net */
00530   unsigned myNumCallees;
  /** Callee transitions in the net */
00532   class Transition** myCallees;

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

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

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

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

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

#endif // NET_H_

Generated by  Doxygen 1.6.0   Back to index