Logo Search packages:      
Sourcecode: maria version File versions

Variable.C

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

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Variable.h"
#include "Valuation.h"
#include "Value.h"
#include "VariableDefinition.h"
#include "VariableSet.h"
#include "Constant.h"
#include "Substitution.h"
#include "Printer.h"
#include "Transition.h"
#include "util.h"
#include "Printer.h"

#include <assert.h>

/** @file Variable.C
 * Variable reference
 */

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

00044 Variable::Variable (const class VariableDefinition& variable,
                bool pred) :
  Expression (),
  myVariable (&variable), myPred (pred)
{
  setType (myVariable->getType ());
  assert (!pred || myVariable->getFather ());
}

00053 Variable::~Variable ()
{
}

void
00058 Variable::setType (const class Type& type)
{
  assert (myVariable->getType ().isAlwaysAssignable (type));
  Expression::setType (type);
}

class Value*
00065 Variable::do_eval (const class Valuation& valuation) const
{
  const class Value* v = valuation.getValue (*myVariable);
  myVariable->flagReferenced (true);
  assert (!v || v->getType ().isAssignable (*getType ()));
  if (v)
    return constrain (valuation, v->copy ());
  else {
    valuation.flag (errVar, *this);
    return NULL;
  }
}

class Expression*
00079 Variable::ground (const class Valuation& valuation,
              class Transition* transition,
              bool declare)
{
  if (myVariable->isAggregate ()) {
    const class Value* v = valuation.getValue (*myVariable);
    assert (!v || v->getType ().isAssignable (*getType ()));
    return v ? (new class Constant (*v->copy ()))->cse () : copy ();
  }
  else if (const class VariableDefinition* father = myVariable->getFather ()) {
    if (!transition)
      return 0;
    if (const class Value* v = valuation.getValue (*father)) {
      class StringBuffer buf;
      buf.append (myVariable->getName ());
      buf.append ("[");
      class Printer printer;
      printer.setOutput (&buf);
      if (myPred) {
      class Value* vp = v->copy ();
      vp->decrement ();
      vp->display (printer);
      delete vp;
      }
      else
      v->display (printer);
      buf.append ("]");
      const char* name = buf.getString ();
      if (const class VariableDefinition* var =
        transition->getVariable (name)) {
      if (&var->getType () != getType ())
        return 0;
      return (new class Variable (*var))->cse ();
      }
      else if (declare)
      return (new class Variable (transition->addVariable
                            (newString (name), *getType (),
                             false, false)))->cse ();
      else
      return 0;
    }
  }
  return copy ();
}

class Expression*
00125 Variable::substitute (class Substitution& substitution)
{
  class Expression* e = substitution.getExpr (*myVariable);
  assert (!e || e->isAssignable (*getType ()));

  return e ? e : copy ();
}

bool
00134 Variable::depends (const class VariableSet& vars,
               bool complement) const
{
  return vars.contains (*myVariable) ? !complement : complement;
}

bool
00141 Variable::forVariables (bool (*operation)
                  (const class Expression&,void*),
                  void* data) const
{
  return operation (*this, data);
}

bool
00149 Variable::isCompatible (const class Value& value,
                  const class Valuation& valuation) const
{
  assert (&value.getType () == getType ());
  if (const class Value* v = valuation.getValue (*myVariable))
    return *v == value;
  else
    return true;
}

void
00160 Variable::getLvalues (const class Value& value,
                  class Valuation& valuation,
                  const class VariableSet& vars) const
{
  assert (&value.getType () == getType ());
  if (vars.contains (*myVariable) &&
      !valuation.getValue (*myVariable))
    valuation.setValue (*myVariable, *value.copy ());
}

void
00171 Variable::getLvalues (const class VariableSet& rvalues,
                  class VariableSet*& lvalues) const
{
  if (!rvalues.contains (*myVariable)) {
    if (!lvalues)
      lvalues = new class VariableSet;
    lvalues->insert (*myVariable);
  }
}

#ifdef EXPR_COMPILE
# include "CExpression.h"

void
Variable::compileLvalue (class CExpression& cexpr,
                   unsigned indent,
                   const class VariableSet& vars,
                   const char* lvalue) const
{
  assert (myVariable->getNumber () && lvalue);
  if (!vars.contains (*myVariable))
    return;
  class StringBuffer& out = cexpr.getOut ();
  if (myVariable->isUndefined ()) {
    out.indent (indent);
    out.append ("ASSIGN (vars, ");
    out.append (myVariable->getNumber () - 1);
    out.append (");\n");
  }
  char* name;
  cexpr.getVariable (*this, name);
  out.indent (indent);
  out.append (name);
  out.append ("=");
  out.append (lvalue);
  out.append (";\n");
  delete[] name;
}

void
Variable::compileCompatible (class CExpression& cexpr,
                       unsigned indent,
                       const class VariableSet& vars,
                       const char* value) const
{
  if (!vars.contains (*myVariable))
    return;
  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent);
  out.append ("if (");
  if (myVariable->isUndefined ()) {
    out.append ("ASSIGNED (");
    out.append (cexpr.getValuation ());
    out.append (", ");
    out.append (myVariable->getNumber () - 1);
    out.append (")&&\n");
  }
  char* name;
  cexpr.getVariable (*this, name);
  if (!getType ()->compileEqual (out, indent + 4, name, value,
                         false, !myVariable->isUndefined (),
                         true, false))
    out.append ("0");
  out.append (")\n");
  cexpr.compileError (indent + 2, errComp);
}

void
Variable::compile (class CExpression& cexpr,
               unsigned indent,
               const char* lvalue,
               const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();
  char* rvalue = cexpr.isIterator (*myVariable);
  if (rvalue) goto gotName;
  assert (myVariable->getNumber ());
  if (!vars || vars->contains (*myVariable)) {
    if (myVariable->isUndefined ()) {
      out.indent (indent);
      out.append ("if (!ASSIGNED (");
      out.append (cexpr.getValuation ());
      out.append (", ");
      out.append (myVariable->getNumber () - 1);
      out.append ("))\n");
      cexpr.compileError (indent + 2, errVar);
    }
    cexpr.getVariable (*this, rvalue);
  gotName:
    if (strcmp (lvalue, rvalue)) {
      out.indent (indent);
      out.append (lvalue);
      out.append ("=");
      out.append (rvalue);
      out.append (";\n");
    }
    delete[] rvalue;
  }
  else
    cexpr.compileError (indent, errVar);
}

#endif // EXPR_COMPILE

void
00276 Variable::display (const class Printer& printer) const
{
  if (const class VariableDefinition* father = myVariable->getFather ()) {
    printer.delimiter (myPred ? ':' : '.');
    printer.print (myVariable->getName ());
    printer.delimiter (' ');
    printer.print (father->getName ());
  }
  else
    printer.print (myVariable->getName ());
}

Generated by  Doxygen 1.6.0   Back to index