Logo Search packages:      
Sourcecode: maria version File versions

Transition.h

Go to the documentation of this file.
// Transition class -*- c++ -*-

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

# include <string.h>
# include <assert.h>
# include <map>
# include "s_list.h"

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

/** @file Transition.h
 * Transition in an 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. */

/** Transition class */
00042 class Transition
{
public:
  /** Kind of the transition */
00046   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 */
00052   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 */
00058   typedef slist<class Expression*> GateList;
  /** Map from names to variables defined in the transition */
  typedef std::map<const char*,class VariableDefinition*,
00061     struct ltstr> VariableMap;
  /** Iterator to the variable name map */
00063   typedef VariableMap::iterator iterator;
  /** Constant iterator to the variable name map */
00065   typedef VariableMap::const_iterator const_iterator;
  /** Map from names to functions defined in the transition */
00067   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 */
00089   const class Net* getNet () const { return myNet; }
  /** Get the index number of the transition in the local net */
00091   unsigned getLocalIndex () const { return myLocalIndex; }
  /** Get the index number of the transition in the root net */
00093   unsigned getRootIndex () const { return myRootIndex; }
  /** Set the index number of the transition in the root net */
00095   void setRootIndex (unsigned root) { myRootIndex = root; }
  /** Get the name of the transition */
00097   const char* getName () const { return myName; }

  /** Get the number of parents (0 if this is not a sync transition) */
00100   unsigned getNumParents () const { return myNumParents; }
  /** Get a parent of this transition by index number */
00102   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 */
00125   unsigned getNumChildren () const { return myNumChildren; }
  /** Get a child transition by index number */
00127   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) */
00137   unsigned getPriority () const { return myPriority; }
  /** Set the priority level (0=none) */
00139   void setPriority (unsigned priority) { myPriority = priority; }

  /** Get the kind of the transition */
00142   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
   */
00184   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 */
00232   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
   */
00252   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 */
00281   bool hasInputs () const { return myNumInputs != 0; }
  /** Determine whether the transition has output arcs */
00283   bool hasOutputs () const { return myNumOutputs != 0; }

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

  /** Determine the number of weak fairness sets the transition belongs to */
00303   unsigned getNumWeaklyFair () const { return myNumWeaklyFair; }
  /** Determine the number of strong fairness sets the transition belongs to */
00305   unsigned getNumStronglyFair () const { return myNumStronglyFair; }
  /** Determine the number of enabledness sets the transition belongs to */
00307   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 */
00322   unsigned getNumConstants () const { return myNumConstants; }

  /** Get the name of a constant
   * @param i           index number of the constant
   * @return            the name of the constant
   */
00328   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
   */
00337   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 slist<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 */
00450   class Net* myNet;
  /** Index number of the transition in myNet */
00452   unsigned myLocalIndex;
  /** Index number of the transition in the root net */
00454   unsigned myRootIndex;
  /** Name of the transition */
00456   char* myName;
  /** Number of parent transitions */
00458   unsigned myNumParents;
  /** Parent transitions (for transitions in child nets) */
00460   const class Transition** myParents;
  /** Number of child transitions */
00462   unsigned myNumChildren;
  /** Child transitions in child nets */
00464   const class Transition** myChildren;
  /** Priority level (0=none) */
00466   unsigned myPriority;
  /** Kind of the transition */
00468   enum Kind myKind;
  /** Number of input arcs */
00470   unsigned myNumInputs;
  /** Input arcs */
00472   class Arc** myInputs;
  /** Number of output arcs */
00474   unsigned myNumOutputs;
  /** Output arcs */
00476   class Arc** myOutputs;
  /** Flag: do the outputs depend on the input marking? */
00478   bool myOutputMarking;

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

  /** Number of weak fairness sets */
00484   unsigned myNumWeaklyFair;
  /** Number of strong fairness sets */
00486   unsigned myNumStronglyFair;
  /** Number of enabledness sets */
00488   unsigned myNumEnabled;
  /** Weak fairness conditions */
00490   class Expression** myWeaklyFairCond;
  /** Strong fairness conditions */
00492   class Expression** myStronglyFairCond;
  /** Enabledness conditions */
00494   class Expression** myEnabledCond;
  /** Weak fairness sets */
00496   unsigned* myWeaklyFairSet;
  /** Strong fairness sets */
00498   unsigned* myStronglyFairSet;
  /** Enabledness sets */
00500   unsigned* myEnabledSet;

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

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

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

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

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

#endif // TRANSITION_H_

Generated by  Doxygen 1.6.0   Back to index