Logo Search packages:      
Sourcecode: maria version File versions

Marking.h

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

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

# include "Expression.h"
# include <assert.h>

/** @file Marking.h
 * Basic multi-set constructor operation
 */

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

/** Marking (basic multi-set) expression */
00037 class Marking : public Expression
{
public:
  /** Result of a check */
00041   enum Result { undefined, pass, fail };

  /** Constructor
   * @param place the place the marking is associated with
   * @param child child marking
   */
  Marking (const class Place* place, class Marking* child = 0);
private:
  /** Copy constructor */
  Marking (const class Marking& old);
  /** Assignment operator */
  class Marking& operator= (const class Marking& old);
protected:
  /** Destructor */
  ~Marking ();
public:

  /** Determine the type of the expression */
00059   enum Expression::Kind getKind () const { return eMarking; }

  /** Get the child marking */
00062   const class Marking* getChild () const { return myChild; }
  /** Get the parent marking */
00064   const class Marking* getParent () const { return myParent; }

  /** Set the place associated with this marking (and its neighbours) */
  void setPlace (const class Place* place);
  /** Get the place associated with this marking */
00069   const class Place* getPlace () const { return myPlace; }

  /** Set the multiplicity associated with this marking */
  void setMultiplicity (class Expression* multiplicity);
  /** Get the multiplicity associated with this marking */
00074   const class Expression* getMultiplicity () const { return myMultiplicity; }
  /** Get the multiplicity expression associated with this marking */
00076   class Expression* getMultiplicity () { return myMultiplicity; }

  /** Set the token value expression associated with this marking */
  void setToken (class Expression* token);
  /** Get the token value expression associated with this marking */
00081   class Expression* getToken () const { return myToken; }

  /** Get the next marking in the list */
00084   const class Marking* getNext () const { return myNext; }

  /**
   * Determine whether this is a basic expression containing
   * no temporal logic or set operations
   * @return      true if this is a basic expression
   */
00091   bool isBasic () const { return true; }
  /**
   * Determine whether this is a temporal logic expression
   * @return      true if this is a temporal logic expression
   */
00096   bool isTemporal () const { return false; }
  /**
   * Determine whether this is a multiset-valued expression
   * @return      true if this is a multiset-valued expression
   */
00101   bool isSet () const { return true; }

  /** Set the type of the expression and its subexpressions */
  void setType (const class Type& type);

  /** Equality comparison operator */
  bool operator== (const class Marking& other) const;

  /** Ordering comparison operator */
  bool operator< (const class Marking& other) const;

  /** Partially evaluate the expression using a valuation
   * @param valuation   Variable substitutions
   * @param transition  Transition for registering quantified variables
   * @param declare     flag: declare new variables if required
   * @return            grounded expression, or NULL in case of error
   */
  class Expression* ground (const class Valuation& valuation,
                      class Transition* transition,
                      bool declare);

  /** Partially evaluate the marking using a valuation
   * @param valuation   variable substitutions
   * @param transition  transition for registering quantified variables
   * @param declare     flag: declare new variables if required
   * @param result      placeholder for the grounded markings
   * @param count initial multiplicity
   * @return            true if the operation was successful
   */
  bool ground (const class Valuation& valuation,
             class Transition* transition,
             bool declare,
             class ExpressionMSet& result,
             card_t count);

  /** Substitute some variables in the expression with expressions
   * @param substitution      Variable substitutions
   * @return                  substituted expression
   */
  class Expression* substitute (class Substitution& substitution);

  /** Determine whether the expression depends on a set of variables
   * @param vars  the set of variables
   * @param complement  flag: treat the set as its complement
   */
  bool depends (const class VariableSet& vars,
            bool complement) const;

  /** Perform an operation on all variables of the expression
   * @param operation   operation to be performed (return false on failure)
   * @param data  parameters to be passed to the operation
   * @return            true if all operations succeeded
   */
  bool forVariables (bool (*operation)
                 (const class Expression&,void*),
                 void* data) const;

  /** Evaluate the marking and add it to or remove it from a PlaceMarking
   * @param source      the PlaceMarking object whose tokens are to be removed
   * @param target      the PlaceMarking object to receive the tokens
   * @param count token multiplier
   * @param valuation   variable substitutions
   * @return            true if everything evaluated ok; false otherwise
   */
  bool eval (class PlaceMarking* const source,
           class PlaceMarking* const target,
           const card_t count,
           const class Valuation& valuation) const;
  /** Evaluate the marking and add it to a PlaceMarking
   * @param target      the PlaceMarking object to receive the tokens
   * @param count token multiplier
   * @param valuation   variable substitutions
   * @return            true if everything evaluated ok; false otherwise
   */
00175   bool add (class PlaceMarking& target,
          const card_t count,
          const class Valuation& valuation) const {
    return eval (NULL, &target, count, valuation);
  }
  /** Evaluate the marking and remove it from a PlaceMarking
   * @param source      the PlaceMarking object whose tokens are to be removed
   * @param count token multiplier
   * @param valuation   variable substitutions
   * @return            true if everything evaluated ok; false otherwise
   */
00186   bool remove (class PlaceMarking& source,
             const card_t count,
             const class Valuation& valuation) const {
    return eval (&source, NULL, count, valuation);
  }

  /** Evaluate the marking expression
   * @param valuation   variable substitutions
   * @return            a PlaceMarking object, or NULL
   */
  class PlaceMarking* meval (const class Valuation& valuation) const;

  /** Calculate the multiplicity of the marking
   * @param valuation   Valuation for evaluating the expressions
   * @return            the multiplicity (0 in case of an error)
   */
  card_t getMultiplicity (const class Valuation& valuation) const;

  /** Append a marking to the list of markings
   * @param expr  Marking to be appended
   */
00207   void append (class Marking& expr) {
    class Marking* m = this;
    assert (&expr != this);
    while (m->myNext) {
      assert (&expr != m->myNext);
      assert (m->myParent == myParent);
      m = m->myNext;
    }
    m->myNext = &expr, m->myParent = myParent;
  }

  /** Get first marking expression */
00219   const class Marking* first () const {
    const class Marking* m = this;
    while (m->myChild) m = m->myChild;
    return m;
  }
  /** Get next marking expression */
00225   const class Marking* next () const {
    for (const class Marking* m = this; m; m = m->myParent)
      if (m->myNext)
      return m->myNext->first ();
    return 0;
  }

  /** Quantify the marking
   * @param valuation   variable substitutions (mainly for error reporting)
   * @param transition  transition for registering quantified variables
   * @param variable    the quantifier variable
   * @param condition   quantification condition (optional)
   * @param declare     flag: declare new variables if required
   * @return            a corresponding multi-set expression, or NULL
   */
  class Expression* quantify (const class Valuation& valuation,
                        class Transition* transition,
                        class VariableDefinition& variable,
                        class Expression* condition,
                        bool declare);

  /** Determine if a marking expression has a non-constant multiplicity
   * @return      whether the marking expression has a variable multiplicity
   */
  bool hasVariableMultiplicity () const;

# ifdef EXPR_COMPILE
  /** Generate C code for evaluating the expression */
  void compile (class CExpression&,
            unsigned,
            const char*,
            const class VariableSet*) const {
    assert (false);
  }

  /** Determine if a marking expression is associated with a multiplicity
   * @return      whether the marking expression has a multiplicity
   */
  bool hasMultiplicity () const;

  /** Generate C code for evaluating a multi-set expression as a scalar
   * @param cexpr the compilation
   * @param indent      indentation level
   * @param result      scalar to assign the multi-set to (must be singleton)
   * @param vars  the variables that have been assigned a value
   * @param check flag: check for result overflow
   */
  void compileScalarMset (class CExpression& cexpr,
                    unsigned indent,
                    const char* result,
                    const class VariableSet* vars,
                    bool check) const;

  /** Generate C code for evaluating the multi-set expression
   * @param cexpr the compilation
   * @param indent      indentation level
   * @param resulttype  type of result (optional typecast qualifier)
   * @param result      multi-set to add items to
   * @param vars  the variables that have been assigned a value
   */
  void compileMset (class CExpression& cexpr,
                unsigned indent,
                const char* resulttype,
                const char* result,
                const class VariableSet* vars) const;

  /** Generate C code for evaluating the multiplicity
   * @param cexpr the compilation
   * @param indent      indentation level
   * @param result      placeholder for the result
   * @param vars  the variables that have been assigned a value
   */
  void compileMultiplicity (class CExpression& cexpr,
                      unsigned indent,
                      const char* result,
                      const class VariableSet* vars) const;
# endif // EXPR_COMPILE

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

  /** Display the token
   * @param printer     the printer object
   */
  void displayToken (const class Printer& printer) const;

private:
  /** The child marking */
00315   class Marking* myChild;
  /** The parent marking (of a child marking) */
00317   const class Marking* myParent;
  /** The sibling marking */
00319   class Marking* myNext;
  /** The place associated with the marking */
00321   const class Place* myPlace;
  /** The multiplicity of the marking */
00323   class Expression* myMultiplicity;
  /** The token expression of the marking */
00325   class Expression* myToken;
};

#endif // MARKING_H_

Generated by  Doxygen 1.6.0   Back to index