Logo Search packages:      
Sourcecode: maria version File versions

Expression.h

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

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

# include "Type.h"
# include "Constraint.h"
# include "Value.h"
# include "Valuation.h"

/** @file Expression.h
 * Abstract base class for expressions
 */

/* 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. */

/** Abstract base class for expressions */
00039 class Expression
{
public:
  /** Expression kinds (@see getKind) */
00043   enum Kind {
    eVariable, eConstant, eUndefined,
    eStruct, eStructComponent, eStructAssign,
    eUnion, eUnionComponent, eUnionType,
    eVector, eVectorIndex, eVectorAssign, eVectorShift,
    eUnop, eBinop, eBooleanBinop, eNot, eRelop,
    eBuffer, eBufferUnop, eBufferRemove, eBufferWrite, eBufferIndex,
    eSet, eIfThenElse, eTemporalBinop, eTemporalUnop,
    eTypecast, eCardinality, eMarking, eTransitionQualifier,
    ePlaceContents, eSubmarking, eMapping, eEmptySet
  };

  /** Constructor */
  Expression ();

private:
  /** Copy constructor */
  Expression (const class Expression& old);
  /** Assignment operator */
  class Expression& operator= (const class Expression& old);
protected:
  /** Destructor */
  virtual ~Expression ();
public:
  /** Common subexpression elimination
   * @return      pointer to this, or to a similar object
   */
  class Expression* cse ();
  /** Get a shared copy of the expression */
00072   class Expression* copy () { myReferences++; return this; }
  /** Destructs Expression, provided that there aren't any references to it */
00074   void destroy () { if (this && !--myReferences) delete this; }
  /** Determine whether this is the last copy of an expression */
00076   bool isLastCopy () const { return myReferences == 1; }

  /** Determine the type of the expression */
  virtual enum Expression::Kind getKind () const = 0;

  /** Set the atomicity flag
   * @param atomic      specifies whether this should be treated
   *              as an atomic (non-temporal) expression
   */
00085   void setAtomic (bool atomic) { myIsAtomic = atomic; }

  /** Read the atomicity flag */
00088   bool isAtomic () const { return myIsAtomic; }

  /** Set the type of the expression
   * @param type  Type of the expression
   */
  virtual void setType (const class Type& type);

  /** Get the type associated with the expression */
00096   const class Type* getType () const { return myType; }

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

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

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

  /** Evaluate the expression
   * @param valuation   Variable substitutions
   * @return            Value of the expression, or NULL in case of error
   */
00125   class Value* eval (const class Valuation& valuation) const {
    return do_eval (valuation);
  }

  /** Evaluate the multiset expression
   * @param valuation   variable substitutions and the global marking
   * @return            a marking
   */
  virtual class PlaceMarking* meval (const class Valuation& valuation) const;

private:
  /** Evaluate the expression
   * @param valuation   Variable substitutions
   * @return            Value of the expression, or NULL in case of error
   */
  virtual class Value* do_eval (const class Valuation& valuation) const;

protected:
  /** Check the constraints of a value
   * @param valuation   Variable substitutions (for error reporting)
   * @param value the value to be checked
   * @return            value, or NULL in case of error
   */
00148   class Value* constrain (const class Valuation& valuation,
                    class Value* value) const {
    assert (!!value);
    if (const class Constraint* const constraint = myType->getConstraint ()) {
      if (!constraint->isConstrained (*value)) {
      valuation.flag (errConst, *this);
      delete value;
      return NULL;
      }
    }
    return value;
  }

public:
  /** Try to evaluate the expression using a valuation
   * @param valuation   Variable substitutions
   * @return            new pointer to this
   */
  class Expression* ground (const class Valuation& valuation);

  /** 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
   */
  virtual class Expression* ground (const class Valuation& valuation,
                            class Transition* transition,
                            bool declare) = 0;

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

  /** 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
   */
  virtual bool depends (const class VariableSet& vars,
                  bool complement) const = 0;

  /** 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
   */
  virtual bool forVariables (bool (*operation)
                       (const class Expression&,void*),
                       void* data) const = 0;

  /** Remove transition qualifiers from the expression
   * @param transition  the transition for which the expression is qualified
   * @return            the expession without qualifiers, or NULL
   */
  virtual class Expression* disqualify (const class Transition& transition);

  /** Determine whether the expression is assignable to the given data type
   * (perform static analysis)
   * @param type  Data type to be checked
   * @return            true if the expression is assignable to the type
   */
00211   bool isAssignable (const class Type& type) const {
    return myType->isAssignable (type);
  }

  /** Determine whether the expression is type compatible with the specified
   * value (whether it ever could evaluate to the value)
   */
  bool isTypeCompatible (const class Value& value) const;

  /** Determine whether the expression is compatible with the specified value,
   * neglecting subexpressions that cannot be evaluated
   * @param value value the expression will be compared to
   * @param valuation   variable substitutions
   * @return            true if the expression is compatible with the value
   */
  virtual bool isCompatible (const class Value& value,
                       const class Valuation& valuation) const;

  /** Unify variables from this expression
   * @param value the value the expression should evaluate to
   * @param valuation   variable substitutions
   * @param vars  the variables to unify
   */
  virtual void getLvalues (const class Value& value,
                     class Valuation& valuation,
                     const class VariableSet& vars) const;

  /** Determine which variables could be unified from this expression
   * @param rvalues     variables unified so far
   * @param lvalues     (output) variables that could be unified
   */
  virtual void getLvalues (const class VariableSet& rvalues,
                     class VariableSet*& lvalues) const;

  /** Translate the expression to a list of temporal logic connectives
   * and Boolean propositions
   * @param property    the property automaton
   * @return            the translated object
   */
  virtual class Ltl* toFormula (class Property& property);

# ifdef EXPR_COMPILE
  /** Generate lvalue gathering code
   * @param cexpr the compilation
   * @param indent      level of indentation
   * @param vars  the variables
   * @param lvalue      C expression referring to the value
   */
  virtual void compileLvalue (class CExpression& cexpr,
                        unsigned indent,
                        const class VariableSet& vars,
                        const char* lvalue) const;

  /** Generate compatibility check code
   * @param cexpr the compilation
   * @param indent      level of indentation
   * @param vars  the variables that have been assigned a value
   * @param value C expression referring to the desired value
   */
  virtual void compileCompatible (class CExpression& cexpr,
                          unsigned indent,
                          const class VariableSet& vars,
                          const char* value) const;

  /** Generate C code for evaluating the expression
   * @param cexpr the compilation
   * @param indent      indentation level
   * @param lvalue      C expression referring to the lvalue
   * @param vars  the variables that have been assigned a value
   */
  virtual void compile (class CExpression& cexpr,
                  unsigned indent,
                  const char* lvalue,
                  const class VariableSet* vars) const = 0;

  /** 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
   */
  virtual 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
   */
  virtual void compileMset (class CExpression& cexpr,
                      unsigned indent,
                      const char* resulttype,
                      const char* result,
                      const class VariableSet* vars) const;

  /** Generate C code for checking the constraint of this expression
   * @param cexpr the compilation
   * @param indent      indentation level
   * @param value C expression referring to the value
   */
  void compileConstraint (class CExpression& cexpr,
                    unsigned indent,
                    const char* value) const {
    if (const class Constraint* c = myType->getConstraint ())
      c->compileCheck (cexpr, indent, value);
  }
# endif // EXPR_COMPILE

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

private:
  /** Number of references to the expression */
00332   unsigned myReferences;
  /** Type of the expression */
00334   const class Type* myType;
  /** Flag: is this an atomic expression */
00336   bool myIsAtomic;
};

#endif // EXPRESSION_H_

Generated by  Doxygen 1.6.0   Back to index