// Multi-set filter -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Submarking.h"
#include "VariableDefinition.h"
#include "Valuation.h"
#include "PlaceMarking.h"
#include "Substitution.h"
#include "Variable.h"
#include "LeafValue.h"
#include "Printer.h"

/** @file Submarking.C
 * Multi-set filter
 */

/* Copyright  1999-2002 Marko Mkel (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. */

Submarking::Submarking (class VariableDefinition& variable,
			class Expression& marking,
			class Expression& condition) :
  myVariable (&variable), myMarking (&marking), myCondition (&condition)
{
  assert (myVariable && myCondition);
  assert (myMarking && myMarking->getType ());
  assert (!myMarking->isTemporal () && myCondition->isBasic ());
  assert (myCondition->getKind () != Expression::eConstant);
  setType (*myMarking->getType ());
}

Submarking::~Submarking ()
{
  delete myVariable;
  myMarking->destroy ();
  myCondition->destroy ();
}

class PlaceMarking*
Submarking::meval (const class Valuation& valuation) const
{
  if (class PlaceMarking* p = myMarking->meval (valuation)) {
    p->setPlace (NULL);
    class Valuation v (valuation);
    for (PlaceMarking::iterator i = p->begin (); i != p->end (); i++) {
      v.setValue (*myVariable, *PlaceMarking::getValue (i).copy ());
      if (class Value* val = myCondition->eval (v)) {
	assert (val->getKind () == Value::vLeaf);
	bool pass = bool (static_cast<class LeafValue&>(*val));
	delete val;
	if (!pass)
	  p->remove (i);
      }
      else {
	delete p;
	valuation.copyErrors (v);
	return NULL;
      }
    }
    return p;
  }
  return NULL;
}

/** Create a Submarking, substituting the iterator variable
 * @param variable	the old iterator variable
 * @param marking	the marking expression
 * @param condition	the condition expression (iterator substituted)
 * @return		the corresponding Submarking expression
 */
static class Submarking*
newSubmarking (const class VariableDefinition& variable,
	       class Expression& marking,
	       class Expression& condition)
{
  class VariableDefinition& v = *new class VariableDefinition (variable);
  class Substitution s;
  s.setExpr (variable, *(new class Variable (v))->cse ());
  class Expression* cond = condition.substitute (s);
  assert (!!cond);
  condition.destroy ();
  return static_cast<class Submarking*>
    ((new class Submarking (v, marking, *cond))->cse ());
}

class Expression*
Submarking::ground (const class Valuation& valuation,
		    class Transition* transition,
		    bool declare)
{
  class Expression* marking =
    myMarking->ground (valuation, transition, declare);
  if (!marking) return NULL;
  class Expression* condition =
    myCondition->ground (valuation, transition, declare);
  if (!condition) { marking->destroy (); return NULL; }

  assert (valuation.isOK ());

  if (marking == myMarking && condition == myCondition) {
    marking->destroy ();
    condition->destroy ();
    return copy ();
  }
  else
    return newSubmarking (*myVariable, *marking, *condition);
}

class Expression*
Submarking::substitute (class Substitution& substitution)
{
  class Expression* marking = myMarking->substitute (substitution);
  class Expression* condition = myCondition->substitute (substitution);

  if (!marking || !condition) {
    marking->destroy ();
    condition->destroy ();
    return NULL;
  }
  if (marking == myMarking && condition == myCondition) {
    marking->destroy ();
    condition->destroy ();
    return copy ();
  }
  else
    return newSubmarking (*myVariable, *marking, *condition);
}

bool
Submarking::depends (const class VariableSet& vars,
		     bool complement) const
{
  return
    myMarking->depends (vars, complement) ||
    myCondition->depends (vars, complement);
}

bool
Submarking::forExpressions (bool (*operation)
			    (const class Expression&,void*),
			    void* data) const
{
  return
    (*operation) (*this, data) &&
    myMarking->forExpressions (operation, data) &&
    myCondition->forExpressions (operation, data);
}

#ifdef EXPR_COMPILE
# include "CExpression.h"

void
Submarking::compileMset (class CExpression& cexpr,
			 unsigned indent,
			 const char* resulttype,
			 const char* result,
			 const class VariableSet* vars) const
{
  /** the multi-set iterator */
  char* iter = cexpr.getLabel ();
  /** the multi-set */
  char* mset;
  /** the filtering condition */
  char* cond;
  /** the item iterator */
  char* var = cexpr.getIterator (*myVariable);
  cexpr.getVariable (*myCondition, cond);
  if (cexpr.getVariable (*myMarking, mset))
    myMarking->compileMset (cexpr, indent, 0, mset, vars);
  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent);
  out.append (result), out.append ("=copy"), getType ()->appendIndex (out);
  out.append (" (");
  if (resulttype)
    out.append (resulttype);
  out.append (result);
  out.append (", "), out.append (mset), out.append (");\n");
  out.indent (indent), out.append ("{\n");
  out.indent (indent + 2);
  getType ()->appendMSetName (out), out.append ("* "), out.append (iter);
  out.append ("=");
  if (resulttype)
    out.append (resulttype);
  out.append (result), out.append (";\n");
  out.indent (indent + 2);
  out.append ("FIRST ("), out.append (iter), out.append (");\n");
  out.indent (indent + 2);
  out.append ("while ("), out.append (iter), out.append (") {\n");
  out.indent (indent + 4);
  out.append ("if ("), out.append (iter), out.append ("->count) {\n");
  out.indent (indent + 6);
  myVariable->getType ().appendName (out);
  out.append (" "), out.append (var), out.append ("=");
  out.append (iter), out.append ("->item;\n");
  myCondition->compile (cexpr, indent + 6, cond, vars);
  out.indent (indent + 6);
  out.append ("if (!"), out.append (cond), out.append (") ");
  out.append (iter), out.append ("->count=0;\n");
  out.indent (indent + 4), out.append ("}\n");
  out.indent (indent + 4);
  out.append ("NEXT ("), out.append (iter), out.append (");\n");
  out.indent (indent + 2), out.append ("}\n");
  out.indent (indent), out.append ("}\n");

  delete[] var;
  delete[] cond;
  delete[] mset;
  delete[] iter;
}

#endif // EXPR_COMPILE

void
Submarking::display (const class Printer& printer) const
{
  printer.printRaw ("subset");
  printer.delimiter (' ');
  printer.print (myVariable->getName ());
  printer.delimiter ('{')++;
  myMarking->display (printer);
  --printer.delimiter ('}');
  printer.delimiter ('(')++;
  myCondition->display (printer);
  --printer.delimiter (')');
}