/******************************************************************
 *  (C) Copyright 1994; dit/upm
 *  Distributed under the conditions stated in the
 *  TOPO General Public License (see file LICENSE)
 ******************************************************************
 *  $Log$
 ******************************************************************/

#ifndef lint
static char rcsid[]= "$Id$";
#endif

/******************************************************************
 *
 *  Santiago Pavon Gome
 *
 *  18 Apr 1990
 *
 *  Substitution of formal variables with actual expressions.
 *
 *  COMPILATION FLAGS:
 *
 *  LOG:
 *     10/07/92. santiago.
 *     The implementation of the SV tables has been changed to BST.
 *     Note that now it is necessary to pass a pointer to the SV table
 *     to the functions.
 *
 *     26/04/93. dlarra.
 *     GetFreeVarsBehSV modified in order to include parameterized
 *     values.
 *
 ******************************************************************/

/* LINTLIBRARY */

/* KJT 12/02/12: Added */
#include <stdlib.h>
#include "limisc.h"
#include "lihash.h"
#include "libst.h"
#include "baattr.h"
#include "basust_v.h"
#include "badefca.h"
#include "batyperw.h"
#include "balotosf.h"
#include "batables.h"

/* KJT 22/01/23: added function prototypes */
boolean IsFalse(ExprTyp ve);
boolean IsTrue(ExprTyp ve);
int GetFalse();
int GetTrue();

/*
 *  auxiliar variables
 */
static SVdescriptorTyp auxtd;
static ListTyp         ld;  /* List of copy cells. */


/******************************************************************
 *                                                                *
 *    Definition of the SVEntries, and functions to manage them   *
 *                                                                *
 ******************************************************************/

typedef struct SVEntryTyp {
			   int      var;
			   ExprTyp  exp;
			   } *PSVEntryTyp;

/*----------------------------------------------------------------*/

/* NewSVEntry
 * Allocate memory for an SV table entry.
 */
#define NewSVEntry() (PSVEntryTyp)Emalloc2Words()

/*----------------------------------------------------------------*/

/* DispSVEntry
 * Dispose the memory used by the entry n.
 */
static void DispSVEntry( n )
     PSVEntryTyp n;
{
  FreeE(UnshareE(n->exp));
  Free2Words((void*)n);
}

/*----------------------------------------------------------------*/

/* PrintSVEntry
 * Print a SV table entry.
 * pstr is the function used to print strings.
 */
static void PrintSVEntry( n, pstr )
     PSVEntryTyp n;
     void       (*pstr)();
{
  char *l;

  pstr(" < ");
  pstr(l=SPrintV(n->var,TRUE));
  (void)free(l);
  pstr(" , ");
  PrintE(n->exp,pstr);
  pstr(" > \n");
}

/*----------------------------------------------------------------*/

/* KeySVEntry
 * Return a key for an SV table entry.
 */
static int KeySVEntry( n )
     PSVEntryTyp n;
{
  return n->var;
}

/*----------------------------------------------------------------*/

/* CmpSVEntryVar
 * TRUE if n1->var is equal to n2->var.
 */
static boolean CmpSVEntryVar( n1,n2 )
     PSVEntryTyp n1,n2;
{
  return n1->var == n2->var;
}


/******************************************************************
 *                                                                *
 *   Definition of the SV tables, and functions to manage them    *
 *                                                                *
 ******************************************************************/

/* CreateSV
 * Create a SV table.
 */
SVdescriptorTyp CreateSV()
{
  return (SVdescriptorTyp)CreateBST();
}

/*----------------------------------------------------------------*/

/* FreeSV
 * Free a SV table.
 */
void FreeSV( td )
     SVdescriptorTyp* td ;
{
  FreeBST( (BstTyp)*td , DispSVEntry );
  *td = NULL;
}

/*----------------------------------------------------------------*/

/* IsEmptySV
 * Return TRUE if the SV table is empty.
 */
boolean IsEmptySV( td )
     SVdescriptorTyp td;
{
  return td==NULL;
}

/*----------------------------------------------------------------*/

/* InsertSV
 * Insert a formal variable and an actual expression in the table td.
 */
void InsertSV( v, e, td )
     int		  v;
     ExprTyp	      e;
     SVdescriptorTyp *td;
{
  PSVEntryTyp n;

  n	 = NewSVEntry();
  n->var = v;
  n->exp = ShareE(e);
  *td	 = (SVdescriptorTyp)InsertBST((DataBstTyp)n, (BstTyp)*td, KeySVEntry);
}

/*----------------------------------------------------------------*/

/* GetActExp_SV
 * Return the actual expression associated to the formal variable v.
 * It must be copied.
 */
ExprTyp GetActExp_SV(v, td)
     int	      v;
     SVdescriptorTyp  *td;
{
  struct SVEntryTyp sve;
  BstTyp t;

  sve.var = v;
  t	  = LookForBST((DataBstTyp)&sve,(BstTyp)*td,KeySVEntry,CmpSVEntryVar);
  return t==NULL ? NULL : ((PSVEntryTyp)(t->dat))->exp;
}

/*----------------------------------------------------------------*/

/* In_SV
 * True if the variable v is in the table td.
 */
boolean In_SV( v, td )
     int	      v;
     SVdescriptorTyp *td ;
{
  return GetActExp_SV(v,td)!=NULL;
}

/******************************************************************
 *								  *
 *	 Redefinition of the variables in the attributes	  *
 *								  *
 ******************************************************************/


/* RedefVarList
 * To redefine the variables defined in a variable list.
 */
static void RedefVarList( v )
     ExprTyp  v;
{
  ExprTyp newv;
  int	  dv;

  dv   = LookNameE(v);
  newv = MakeE(EqualV_entry(dv),VariableC);
  InsertSV(dv,newv,&auxtd);
}

/*----------------------------------------------------------------*/

/* RedefOfferList
 * To redefine the variables defined in a offer list.
 */
static void RedefOfferList( ol )
     OfferListTyp  ol;
{
  ExprTyp newv;
  int	  dv;

  for ( ; ol!=NULL; ol=MvNextOffer(ol) )
    if ( LookKindOffer(ol)==QUESTION ){
      dv   = LookNameE( LookExprOffer(ol) );
      newv = MakeE(EqualV_entry(dv),VariableC);
      InsertSV(dv,newv,&auxtd);
    }
}

/*----------------------------------------------------------------*/

/* RedefVarAssignList
 * To redefine the variables defined in a var assign list.
 */
static void RedefVarAssignList( va )
     PVarAssignTyp  va;
{
  ExprTyp newv;
  int	  dv;

  dv   = va->varFor;
  newv = MakeE(EqualV_entry(dv),VariableC);
  InsertSV(dv,newv,&auxtd);
}

/*----------------------------------------------------------------*/

/* IDSV
 * Auxiliar function of InsertBehDefSV
 */
static void IDSV( b )
     BehTyp b;
{
  ITContListTyp itcl;
  PITContTyp	itc;
  LabelTyp	lab;

  while ( b!=NULL ) {
    if (SharedB(b))
      if( In_list((DataListTyp)b,ld,EqInt) )
	return;
      else
	ld = Insert_list((DataListTyp)b,ld);
    switch ( LookType(b) )
      { case IC:
	case GuardC:
	case HidingC:
	case RelabellingC:
	case ParC:
	case GateChoiceC:
	  b =  LookB1(b);
	  break;

	case ProcessInstC:
	case PletC:
	case StopC:
	case TerminationC:
	  b =  NULL;
	  break;

	case AlternativeC:
	  while ( b!=NULL )
	    { IDSV(LookB1(b));
	      b = LookB2(b);
	    }
	  break;

	case DisablingC:
	case ParallelC:
	  IDSV(LookB1(b));
	  b = LookB2(b);
	  break;
	case ProcessDefC:
	case EnablingC:
	case ChoiceC:
	  Apply_Proc_list((ListTyp)LookAInfo(LookA(b,ELA)),RedefVarList);
	  b =  LookB1(b);
	  break;

	case GateC:
	case ExitC:
	  RedefOfferList((OfferListTyp)LookAInfo(LookA(b,OLA)));
	  b =  LookB1(b);
	  break;

	case LetC:
	  Apply_Proc_list((ListTyp)LookAInfo(LookA(b,VALA)),
			  RedefVarAssignList);
	  b =  LookB1(b);
	  break;

	case ContSetC:
	  itcl = (ITContListTyp)LookAInfo(LookA(b,ITCLA));
	  while (itcl!=NULL) {
	    itc = (PITContTyp)LookInfo_list(itcl);
	    for ( lab = itc->label; lab!=NULL; lab=LookArgB(lab,1) )
	      IDSV(lab);
	    itcl = Next_list(itcl);
	  }
	  b =  NULL;
	  break;

	case InterleavedC:
	  IDSV(LookB2(b));
	  b = LookB1(b);
	  break;

	default :
	  Error("InsertBehDefSV: unexpected cell.");
	}
  }
}

/*----------------------------------------------------------------*/

/* InsertBehDefSV
 * Insert in the table td the definition variables in the behaviour b,
 * in order to redefine them.
 * Stop when plet or instantation are reached.
 */
void InsertBehDefSV( b, td )
     BehTyp	      b;
     SVdescriptorTyp *td ;
{
  auxtd = *td;
  ld	=  Create_list();
  IDSV( b );
  Disp_list( ld );
  *td = auxtd;
}


/******************************************************************
 *								  *
 *		   Create a SV table from a VAL			  *
 *								  *
 ******************************************************************/


/* Insert_VA_SV
 * Insert in the table a variable assignment.
 */
static void Insert_VA_SV( va )
     PVarAssignTyp  va;
{
  /*
   * discard void variable assignment : plet x:s=x
   *
   */
  if (!IsVariableE(va->expAct) || va->varFor!=LookNameE(va->expAct))
    InsertSV(va->varFor,CopyE(va->expAct),&auxtd);  /*mse*/
}

/*----------------------------------------------------------------*/

/* Insert_VAL_SV
 * Insert in the table td a variable assignment List.
 * Ignore void assignments ( x:s=x ).
 */
void Insert_VAL_SV( val, td )
     VarAssignListTyp  val;
     SVdescriptorTyp  *td;
{
  auxtd = *td;
  Apply_Proc_list( val, Insert_VA_SV );
  *td = auxtd;
}


/******************************************************************
 *								  *
 *	       Creates a VAL from a SV table			  *
 *								  *
 ******************************************************************/

static VarAssignListTyp val_mk;

static void Add_VAL_mk(d)
     DataBstTyp d;
{
  val_mk = InsertVAL(val_mk,((PSVEntryTyp)d)->var,
		     CopyE(((PSVEntryTyp)d)->exp)); /*mse*/
}

/*----------------------------------------------------------------*/

/* Make_VAL_SV
 * Makes a attribute VAL from the table td.
 */
VarAssignListTyp Make_VAL_SV(td)
     SVdescriptorTyp *td ;
{
  val_mk = Create_list();
  OrdenBST( (BstTyp)*td , Add_VAL_mk );
  return val_mk;
}


/******************************************************************
 *								  *
 *		 Substitution functions				  *
 *								  *
 ******************************************************************/

static ListTyp vars_in_expr;
static ListTyp replaced_vars;
static boolean changeSubstExpr;


static boolean SubstExprSVaux ( e, td )
     ExprTyp	      e;
     SVdescriptorTyp *td ;
{
  ExprTyp aux;
  boolean rewrite;
  int	  n,i;

  /*
     LASSERT(OwnersE(e)==0);
     */
  if ( IsVariableE(e) ) {
    aux = GetActExp_SV(LookNameE(e),td);
    if (aux!=NULL) {
      GlueE(e,aux);
      changeSubstExpr = TRUE;
      if (IsVariableE(aux)) {
	if ( In_list((DataListTyp)LookNameE(aux),replaced_vars,EqInt) )
	  return TRUE;
	replaced_vars = Insert_list((DataListTyp)LookNameE(aux),replaced_vars);
	if ( ! In_list((DataListTyp)LookNameE(aux),vars_in_expr,EqInt) )
	  return FALSE;
      }
      return TRUE;
    }
    else {
      vars_in_expr = Insert_list((DataListTyp)LookNameE(e),vars_in_expr);
      return In_list((DataListTyp)LookNameE(e),replaced_vars,EqInt);
    }
  }
  else {
    rewrite = FALSE;
    n = NumArgE(e);
    for (i=1 ; i<=n ; i++) {
      if (SubstExprSVaux(LookArgE(e,i),td))
	rewrite = TRUE;
    }
    if (rewrite) {
      (void) One_Rewrite(&e);
      return TRUE ;
    }
  }
  return FALSE;
}

/*----------------------------------------------------------------*/

/* SubstExprSV
 * Makes the replacement indicated in the table td in the expression
 * pointed by pe.
 * Returns true if any replacement is done.
 */
boolean SubstExprSV( pe, td )
     ExprTyp         *pe;
     SVdescriptorTyp *td ;
{
  changeSubstExpr = FALSE;
  vars_in_expr    = Create_list();
  replaced_vars   = Create_list();
  (void) SubstExprSVaux ( *pe, td );
  Disp_list(vars_in_expr);
  Disp_list(replaced_vars);
  return changeSubstExpr;
}

/*----------------------------------------------------------------*/

/* SubstPredSV
 * Makes the replacement indicated in the table td in the predicate p.
 * Returns true if any replacement is done.
 */
boolean SubstPredSV( pp, td )
     PredicateTyp    *pp;
     SVdescriptorTyp *td ;
{
  boolean       changes;
  ExprListTyp   vl1,vl2;
  ExprTyp       eo,er;
  PredNodeTyp   pn;
  PredicateTyp  p,newp;

  changes = FALSE;
  newp    = NULL;
  p       = *pp;
  while (p != NULL) {
    pn = (PredNodeTyp)LookInfo_list(p);
    LASSERT(OwnersE(pn->rewritten)==1);
    er = UnshareE(pn->rewritten);
    if (SubstExprSV(&er,td)) {
      changes = TRUE;
      /*
       * er = FalseIfConst(er);
       */
      LASSERT((!IsConstE(er))||(!IsEqual(er)));

      pn->rewritten = ShareE(er);
      if (IsFalse(er)) {
	FreePred(*pp);
	FreePred(newp);
	*pp = NewPred(MakeE(GetFalse(),OperationC),(ExprTyp)NULL);
	return TRUE;
      }
      else if (!IsTrue(er)) {
	if (pn->original!=NULL) {
	  eo = UnshareE(pn->original);
	  (void)SubstExprNoRwSV(&eo,td);
	  pn->original = ShareE(eo);

	  vl1 = VarsInE(er);
	  vl2 = VarsInE(eo);
	  if (Length_list(vl1)!=Length_list(vl2)) {
	    FreeE(UnshareE(pn->original));
	    pn->original = NULL;
	  }
	  FreeEL(vl1);
	  FreeEL(vl2);
	}
	newp = AddPremisePred(newp,pn->rewritten,pn->original);
      }
    }
    else {
      pn->rewritten = ShareE(er);
      newp          = AddPremisePred(newp,er,pn->original);
    }
    p = Next_list(p);
  }
  FreePred(*pp);
  if (newp != NULL) {
    if (changes)
      *pp = RemoveEqualExprPred(newp);
    else
      *pp = newp;
  }
  else
    *pp = NewPred(MakeE(GetTrue(),OperationC),(ExprTyp)NULL);
  return changes;
}

/*----------------------------------------------------------------*/

/* Subst_OL_SV
 * Make the replacement indicated in the table td in the offer list ol.
 */
void Subst_OL_SV( ol, td )
     OfferListTyp     ol;
     SVdescriptorTyp  *td;
{
  ExprTyp e;

  while (ol!=NULL)
    { e = GetExprOffer(ol);
      (void) SubstExprSV(&e,td);
      PutExprOffer(ol,e);
      ol = MvNextOffer(ol);
    }
}

/*----------------------------------------------------------------*/

/* Subst_EL_SV
 * Make the replacement indicated in the table td in the expression list el.
 */
void Subst_EL_SV( el, td )
     ExprListTyp      el;
     SVdescriptorTyp *td;
{
  ExprTyp e;

  while (el!=NULL) {
    e = UnshareE((ExprTyp)el->info);
    (void) SubstExprSV(&e,td);
    el->info = (DataListTyp) ShareE(e);
    el = Next_list(el);
  }
}

/*----------------------------------------------------------------*/

/* Subst_VAL_RightSide_SV
 * Make the replacement indicated by the table td
 * in the right side of the var assign list val.
 */
void Subst_VAL_RightSide_SV( val, td )
     VarAssignListTyp  val;
     SVdescriptorTyp   *td;
{
  ExprTyp e;

  while ( val!=NULL ) {
    e = GetExprVAL(val);
    (void)SubstExprSV(&e,td);
    PutExprVAL(val,e);
    val = Next_list(val);
  }
}

/*----------------------------------------------------------------*/

/* Subst_VAL_BothSides_SV
 * Make the replacement indicated by the table td
 * in both sides of the var assign list val.
 */
void Subst_VAL_BothSides_SV( val, td )
     VarAssignListTyp  val;
     SVdescriptorTyp   *td;
{
  ExprTyp       e;
  DescriptorTyp v;

  while (val!=NULL)
    { e = GetExprVAL(val);
      (void) SubstExprSV(&e,td);
      PutExprVAL(val,e);

      v = GetVarVAL(val);
      if (In_SV(v,td)) {
	e = GetActExp_SV(v,td);
	LASSERT(IsVariableE(e));
	PutVarVAL(val,LookNameE(e));
      }
      else
	PutVarVAL(val,v);
      val = Next_list(val);
    }
}

/*----------------------------------------------------------------*/

/* Var_in_Expr_SV
 * Return TRUE if the expression e contains any formal variable that is
 * in the table td.
 */
boolean Var_in_Expr_SV( e, td )
     ExprTyp          e;
     SVdescriptorTyp *td;
{
  boolean found;
  int     n,i;
  ExprTyp a;

  if (IsVariableE(e))
    return In_SV(LookNameE(e),td);
  else
    { found = FALSE;
      n = NumArgE(e);
      for (i=1 ; (i<=n) && !found ; i++) {
	a = LookArgE(e,i);
	found = Var_in_Expr_SV(a,td);
      }
      return found;
    }
}

/*----------------------------------------------------------------*/

/* Var_in_Pred_SV
 * Returns true if the predicate p contains any formal variable that is
 * in the table td.
 */
boolean Var_in_Pred_SV( p, td )
     PredicateTyp      p;
     SVdescriptorTyp *td;
{
  LASSERT(OwnersE(LookRwPred(p))!=0);
  for ( ; p!=NULL ; p=Next_list(p) )
    if (Var_in_Expr_SV( LookRwPred(p), td ))
      return TRUE;
  return FALSE;
}

/*----------------------------------------------------------------*/

/* Var_in_EL_SV
 * Return true if the expression list el contains any formal variable
 * that is in the table td.
 */
boolean Var_in_EL_SV( el,td )
     ExprListTyp       el;
     SVdescriptorTyp  *td;
{
  boolean  found;

  found = FALSE;
  while ((!found) && (el!=NULL))
    { found = Var_in_Expr_SV((ExprTyp)LookInfo_list(el),td);
      el = Next_list(el);
    }
  return found;
}

/*----------------------------------------------------------------*/

/* Var_in_VAL_RightSide_SV
 * Return true if the right hand side of the var assign list val
 * contains any formal variable that is in the table td.
 */
boolean Var_in_VAL_RightSide_SV( val,td )
     VarAssignListTyp  val;
     SVdescriptorTyp  *td;
{
  boolean  found;

  found = FALSE;
  while ((!found) && (val!=NULL)){
    found = Var_in_Expr_SV(LookExprVAL(val),td);
    val = Next_list(val);
  }
  return found;
}

/*----------------------------------------------------------------*/

/* Var_in_VAL_BothSides_SV
 * Returns true if the var assign list val contains any formal variable
 * that is in the table td.
 */
boolean Var_in_VAL_BothSides_SV( val, td )
     VarAssignListTyp  val;
     SVdescriptorTyp  *td;
{
  boolean found;

  found = FALSE;
  while ((!found) && (val!=NULL)){
    found = In_SV(LookVarVAL(val),td);
    if (!found)
      found = Var_in_Expr_SV(LookExprVAL(val),td);
    val = Next_list(val);
  }
  return found;
}

/*----------------------------------------------------------------*/

/* Var_in_OfferList_SV
 * Returns true if the offer list ol contains any formal variable
 * that is in the table td.
 */
boolean Var_in_OL_SV( ol, td )
     OfferListTyp      ol;
     SVdescriptorTyp  *td;
{
  boolean  found;

  found = FALSE;
  while ((!found) && (ol!=NULL))
    { found = Var_in_Expr_SV(LookExprOffer(ol),td);
      ol = MvNextOffer(ol);
    }
  return found;
}

/*----------------------------------------------------------------*/

/* SubstBehSV
 * Make the replacement indicated in the table td in all the
 * expressions of the behaviour b.
 */
void SubstBehSV( b, td )
     BehTyp            b;
     SVdescriptorTyp  *td;
{
  PredicateTyp     p;
  ExprListTyp      el;
  OfferListTyp     ol;
  VarAssignListTyp val;
  PAttrTyp         a;
  ITContListTyp    itcl;
  PITContTyp       itc;
  char             r;
  LabelTyp         lab;
#ifdef TIME
  PTimeTyp         time;
#endif

  while ( b!=NULL )
    switch ( LookTypeB(b) )
      {
      case IC:
#ifdef TIME
	time = (PTimeTyp) LookAInfo(LookA(b,TA));
	UnshareA(b,TA);
	a  = GetA(b,TA);
	time = (PTimeTyp)GetAInfo(a);
	if ( Var_in_TA_SV(time,td) ){
	  Subst_TA_SV(time,td);
	  if (LookNameE(time->lower_bound)==FindO_time("neg"))
	    ChangeNameE(time->lower_bound,FindO_time("0"));
	}
	PutAInfo(a,(AttrValueTyp)time);
	PutA(b,a);

#endif

      case HidingC:
      case RelabellingC:
      case ParC:
      case GateChoiceC:
	b =  LookB1(b);
	break;

      case StopC:
	b =  NULL;
	break;

      case ChoiceC:
      case ProcessDefC:
	if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),td) )
	  { UnshareA(b,ELA);
	    a  = GetA(b,ELA);
	    el = (ExprListTyp)GetAInfo(a);
	    Subst_EL_SV(el,td);
	    PutAInfo(a,(AttrValueTyp)el);
	    PutA(b,a);
	  }
	b = LookB1(b);
	break;

      case TerminationC:
      case ProcessInstC:
	if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),td) )
	  { UnshareA(b,ELA);
	    a  = GetA(b,ELA);
	    el = (ExprListTyp)GetAInfo(a);
	    Subst_EL_SV(el,td);
	    PutAInfo(a,(AttrValueTyp)el);
	    PutA(b,a);
	  }
	b = NULL;
	break;

      case GuardC:
	if ( Var_in_Pred_SV((PredicateTyp)LookAInfo(LookA(b,PA)),td) )
	  { UnshareA(b,PA);
	    a = GetA(b,PA);
	    p = (PredicateTyp)GetAInfo(a);
	    (void)SubstPredSV(&p,td);
	    PutAInfo(a,(AttrValueTyp)p);
	    PutA(b,a);
	  }
	r = LookPredicate(b);
	SolvePredicateBeh(b);
	if (r=='i')
	  b = LookB1( b);
	break;

      case GateC:
#ifdef TIME

      time = (PTimeTyp) LookAInfo(LookA(b,TA));

      UnshareA(b,TA);
      a  = GetA(b,TA);
      time = (PTimeTyp)GetAInfo(a);
      if ( Var_in_TA_SV(time,td) ){
	Subst_TA_SV(time,td);
	if (LookNameE(time->lower_bound)==FindO_time("neg"))
	  ChangeNameE(time->lower_bound,FindO_time("0"));
      }
      PutAInfo(a,(AttrValueTyp)time);
      PutA(b,a);

#endif

       if ( Var_in_OL_SV((OfferListTyp)LookAInfo(LookA(b,OLA)),td) )
	  { UnshareA(b,OLA);
	    a  = GetA(b,OLA);
	    ol = (OfferListTyp)GetAInfo(a);
	    Subst_OL_SV(ol,td);
	    PutAInfo(a,(AttrValueTyp)ol);
	    PutA(b,a);
	  }
	p = (PredicateTyp)LookAInfo(LookA(b,PA));
	if (p!=NULL)
	  if ( Var_in_Pred_SV(p,td) )
	    { UnshareA(b,PA);
	      a = GetA(b,PA);
	      p = (PredicateTyp)GetAInfo(a);
	      (void)SubstPredSV(&p,td);
	      PutAInfo(a,(AttrValueTyp)p);
	      PutA(b,a);
	    }
	r = LookPredicate(b);
	SolvePredicateBeh(b);
	b = LookB1(b);
	break;

      case ExitC:
	if ( Var_in_OL_SV((OfferListTyp)LookAInfo(LookA(b,OLA)),td) )
	  { UnshareA(b,OLA);
	    a  = GetA(b,OLA);
	    ol = (OfferListTyp)GetAInfo(a);
	    Subst_OL_SV(ol,td);
	    PutAInfo(a,(AttrValueTyp)ol);
	    PutA(b,a);
	  }
	b = NULL;
	break;

      case PletC:
	val = (VarAssignListTyp)LookAInfo(LookA(b,VALA));
	if ( Var_in_VAL_RightSide_SV(val,td) )
	  { UnshareA(b,VALA);
	    a   = GetA(b,VALA);
	    val = (VarAssignListTyp)GetAInfo(a);
	    Subst_VAL_RightSide_SV(val,td);
	    PutAInfo(a,(AttrValueTyp)val);
	    PutA(b,a);
	  }
	b = NULL;
	break;

      case LetC:
	if ( Var_in_VAL_BothSides_SV((VarAssignListTyp)LookAInfo(LookA(b,VALA)),td) )
	  { UnshareA(b,VALA);
	    a   = GetA(b,VALA);
	    val = (VarAssignListTyp)GetAInfo(a);
	    Subst_VAL_BothSides_SV(val,td);
	    PutAInfo(a,(AttrValueTyp)val);
	    PutA(b,a);
	  }
	b = LookB1(b);
	break;
      case AlternativeC:
      case  DisablingC:
      case ParallelC:
	SubstBehSV(LookB1(b),td);
	b =  LookB2(b);
	break;
      case EnablingC:
	if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),td) )
	  { UnshareA(b,ELA);
	    a  = GetA(b,ELA);
	    el = (ExprListTyp)GetAInfo(a);
	    Subst_EL_SV(el,td);
	    PutAInfo(a,(AttrValueTyp)el);
	    PutA(b,a);
	  }
	SubstBehSV(LookB1(b),td);
	b = LookB2(b);
	break;

      case InterleavedC:
	SubstBehSV(LookB1(b),td);
	b = LookB2(b);
	break;

      case ContSetC:
	itcl = (ITContListTyp)LookAInfo(LookA(b,ITCLA));
	while (itcl!=NULL) {
	  itc = (PITContTyp)LookInfo_list(itcl);
	  for ( lab = itc->label; lab!=NULL; lab=LookArgB(lab,1) )
	    SubstBehSV(lab,td);
	  SubstBehSV(itc->b,td);
	  itcl = Next_list(itcl);
	}
	b = NULL;
	break;

      default :
	Error("SubstBehSV: unexpected cell.");
      }
}


/******************************************************************
 *                                                                *
 *           Get the free variables of a behaviour                *
 *                                                                *
 ******************************************************************/


#define DVHASH 100

static ExprListTyp  fvl;    /* copy of free variables */
static HashDTyp     dvht;   /* defined variables */

/*----------------------------------------------------------------*/

static void StoreDVHT( n )
     DescriptorTyp n;
{
  if (!In_HT( dvht, (DataHashTyp)n ) )
    Insert_HT( dvht, (DataHashTyp)n );
}

/*----------------------------------------------------------------*/

static void GetVFreeExpr( e )
     ExprTyp e;
{
  ExprListTyp fvln;
  int         n,i;

  if (e!=NULL)
    if (IsOperationE(e)) {
      n = NumArgE(e);
      for (i=1 ; i<=n ; i++) {
	GetVFreeExpr(LookArgE(e,i));
      }
    }
    else
      if ( !In_HT( dvht, (DataHashTyp)LookNameE(e) ) ){

	/* add if not in list */
	for ( fvln=fvl; fvln!=NULL; fvln=Next_list(fvln) )
	  if ( LookNameE(e) ==
	      LookNameE((ExprTyp)LookInfo_list(fvln)) )
	    break;
	if (fvln==NULL)
	  fvl = InsertEL(CopyE(e),fvl); /*mse*/
      }
}

/*----------------------------------------------------------------*/

static void GetVFreePred( p )
     PredicateTyp p;
{
  if (p!=NULL)
    GetVFreeExpr(((PredNodeTyp)LookInfo_list(p))->rewritten);
}

/*----------------------------------------------------------------*/

static void GetVDefExpr( e )
     ExprTyp e;
{
  int i,n;

  if (e!=NULL)
    if (IsOperationE(e)){
      n = NumArgE(e);
      for (i=1 ; i<=n ; i++) {
	GetVDefExpr(LookArgE(e,i));
      }
    }
    else
      StoreDVHT(LookNameE(e));
}

/*----------------------------------------------------------------*/

static void GetVDefVFreeVAL( val )
     VarAssignListTyp val;
{
  PVarAssignTyp va;

  for ( ; val!=NULL; val=Next_list(val) ){
    /* strictly compulsory precedence */
    va = (PVarAssignTyp)LookInfo_list(val);
    if (!IsVariableE(va->expAct) || va->varFor!=LookNameE(va->expAct))
      StoreDVHT(va->varFor);
    GetVFreeExpr(va->expAct);
  }
}

/*----------------------------------------------------------------*/

static void GetVDefVFreeOL( ol )
     OfferListTyp ol;
{
  for ( ; ol!=NULL; ol=MvNextOffer(ol) )
    if (LookKindOffer(ol)==EXCLAMATION)
      GetVFreeExpr(LookExprOffer(ol));
    else
      StoreDVHT(LookNameE(LookExprOffer(ol)));
}

/*----------------------------------------------------------------*/

/* GFVB
 * Auxiliar function of GetFreeVarsBeh
 */
static void GFVB( b )
     BehTyp   b;
{
  ITContListTyp itcl;
  PITContTyp    pit;
  LabelTyp      lab;

  while ( b!=NULL ) {
    if (VisitedB(b))
      return;
    switch ( LookTypeB(b) )
      {
      case IC:
      case HidingC:
      case RelabellingC:
      case ParC:
      case GateChoiceC:
	b =  LookB1(b);
	break;

      case StopC:
	b =  NULL;
	break;

      case LetC:     /* example :  let x:s = x, y:s = inc(z)  => free=(x,z)  */
	GetVDefVFreeVAL((VarAssignListTyp)LookAInfo(LookA(b,VALA)));
	b =  LookB1(b);
	break;

      case PletC:   /* example :  plet x:s = x, y:s = inc(z)  => free=(x,z)  */
	GetVDefVFreeVAL((VarAssignListTyp)LookAInfo(LookA(b,VALA)));
	b = NULL;
	break;

      case AlternativeC:
	while ( b!=NULL )
	  { GFVB(LookB1(b));
	    b= LookB2(b);
	  }
	break;

      case DisablingC:
      case ParallelC:
	GFVB(LookB1(b));
	b= LookB2(b);
	break;

      case ProcessInstC:
	Apply_Proc_list((ListTyp)LookAInfo(LookA(b,ELA)),GetVFreeExpr);
	b = NULL;
	break;

      case ProcessDefC:
	Apply_Proc_list((ListTyp)LookAInfo(LookA(b,ELA)),GetVDefExpr);
	b = NULL;
	break;

      case EnablingC:  /* example :  >> accept x:s ,y:s in   => def = (x,y)  */
      case ChoiceC:
	Apply_Proc_list((ListTyp)LookAInfo(LookA(b,ELA)),GetVDefExpr);
	b =  LookB1(b);
	break;

	/*
	 * strictly compulsory precedence
	 *
	 */
      case GateC:   /* example : g !x ?y:s [f(y,z)]; => free=(x,z), def=(y)  */
	GetVDefVFreeOL((OfferListTyp)LookAInfo(LookA(b,OLA)));
      case GuardC:
	GetVFreePred((PredicateTyp)LookAInfo(LookA(b,PA)));
	b =  LookB1(b);
	break;

      case ExitC:
	GetVDefVFreeOL((OfferListTyp)LookAInfo(LookA(b,OLA)));
	b =  NULL;
	break;

      case InterleavedC:
	b = LookArgB(b,1);
	break;

      case ContSetC:
	itcl = (ITContListTyp)LookAInfo(LookA(b,ITCLA));
	for ( ; itcl!=NULL; itcl= Next_list(itcl) ) {
	  pit = (PITContTyp)LookInfo_list(itcl);
	  for ( lab=pit->label; lab!=NULL; lab=LookArgB(lab,1) )
	    Apply_Proc_list((ListTyp)LookAInfo(LookA(lab,ELA)),GetVDefExpr);
	}
	b = NULL;
	break;

      case TerminationC:
	Apply_Proc_list((ListTyp)LookAInfo(LookA(b,ELA)),
			GetVFreeExpr);
	b = NULL;
	break;

      default :
	Error("GetFreeVarsBehSV: unexpected cell.");
      }
  }
}

/*----------------------------------------------------------------*/

/* GetFreeVarsBehSV
 * return a list of free variables in b, including its parameterized value.
 * ( variables undefined in b ).
 */
ExprListTyp GetFreeVarsBehSV( b )
     BehTyp b;
{

  /* copies of free variables (until plet obviously)*/
  fvl  = CreateEL();

  /* defined variables (until plet) */
  dvht = Create_HT( DVHASH, (void(*)())EchoInt, EchoInt, EqInt, PrintInt );

  Begin_VisitB();
  GFVB( b );
  End_VisitB();
  Free_HT( dvht );

  return fvl;
}

/*----------------------------------------------------------------*/

/* IsUsedVAB
 * auxiliary function for IsUsedVALInBeh
 */
static boolean IsUsedVAB( td, b )
     SVdescriptorTyp *td ;
     BehTyp           b;
{
  PredicateTyp p;

  while ( b!=NULL ) {
    if ( VisitedB(b) )
      return FALSE;
    switch ( LookTypeB(b) )
      {
      case IC:
#ifdef TIME
	if ( Var_in_TA_SV((PTimeTyp)LookAInfo(LookA(b,TA)),td) )
	  return TRUE;
#endif
      case HidingC:
      case RelabellingC:
      case ParC:
      case GateChoiceC:
	b =  LookArgB(b,1);
	break;

      case ContSetC:
      case StopC:
	b =  NULL;
	break;
      case ChoiceC:
      case ProcessInstC:
      case TerminationC:
	if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),td) )
	  return TRUE;
	b = LookArgB(b,1);
	break;
      case GuardC:
	if ( Var_in_Pred_SV((PredicateTyp)LookAInfo(LookA(b,PA)),td) )
	  return TRUE;
	b = LookArgB(b,1);
	break;
      case GateC:
	p = (PredicateTyp)LookAInfo(LookA(b,PA));
	if (p!=NULL)
	  if ( Var_in_Pred_SV(p,td) )
	    return TRUE;
#ifdef TIME
	if ( Var_in_TA_SV((PTimeTyp)LookAInfo(LookA(b,TA)),td) )
	  return TRUE;
#endif
      case ExitC:
	if ( Var_in_OL_SV((OfferListTyp)LookAInfo(LookA(b,OLA)),td) )
	  return TRUE;
	b = LookArgB(b,1);
	break;

      case PletC:
	if ( Var_in_VAL_RightSide_SV((VarAssignListTyp)LookAInfo(LookA(b,VALA)),td) )
	  return TRUE;
	b = NULL;
	break;

      case LetC:
	if ( Var_in_VAL_BothSides_SV((VarAssignListTyp)LookAInfo(LookA(b,VALA)),td) )
	  return TRUE;
	b = LookArgB(b,1);
	break;

      case EnablingC:
	if ( Var_in_EL_SV((ExprListTyp)LookAInfo(LookA(b,ELA)),td) )
	  return TRUE;
      case AlternativeC:
      case DisablingC:
      case ParallelC:
	if ( IsUsedVAB( td, LookArgB(b,1) ) )
	  return TRUE;
	b =  LookArgB(b,2);
	break;

      case InterleavedC:
	b =  LookArgB(b,1);
	break;

      default :
	Error("IsUsedVAB: unexpected cell.");
      }
  }
  return FALSE;
}

/*----------------------------------------------------------------*/

/* IsUsedInBehSV
 * Say if a VAL (in sv-format) is actually used in a behaviour b.
 * (i.e. b contains variables defined in VAL )
 */
boolean IsUsedInBehSV( td, b )
     SVdescriptorTyp *td ;
     BehTyp           b;
{
  boolean isUsed;

  Begin_VisitB();
  isUsed = IsUsedVAB( td, b );
  End_VisitB();

  return isUsed;
}

/*----------------------------------------------------------------*/

/* SubstExprNoRwSV
 * Make the replacement indicated in the table td in the expression
 * pointed by pe without rewriting.
 * Return TRUE if any replacement has been done.
 */
boolean SubstExprNoRwSV( pe, td )
     ExprTyp         *pe;
     SVdescriptorTyp *td ;
{
  ExprTyp a;
  boolean changes;
  int     n,i;

  LASSERT(OwnersE(*pe) == 0);
  if (IsVariableE(*pe)) {
    a = GetActExp_SV(LookNameE(*pe),td);
    if (a!=NULL) {
      FreeE(*pe);
      *pe = CopyE(a); /*mse*/
      return TRUE;
    }
  }
  else {
    changes = FALSE;
    n       = NumArgE(*pe);
    for ( i=1; i<=n; i++ ) {
      a = GetArgE(*pe,i);
      if (SubstExprNoRwSV(&a,td))
	changes = TRUE;
      PutArgE(*pe,a,i);
    }
    if (changes) {
      return TRUE ;
    }
  }
  return FALSE;
}

/*----------------------------------------------------------------*/
#ifdef TIME

/* Subst_TA_SV
 * Make the replacement indicated in the table td in the time attribute.
 */

void Subst_TA_SV( time, td )
     PTimeTyp     time;
     SVdescriptorTyp  *td;
{

  (void) SubstExprSV(& time->lower_bound,td);
  (void) SubstExprSV(& time->upper_bound,td);
  if (time -> tvar !=NULL)
    (void) SubstExprSV(& time->tvar,td);
}

/*----------------------------------------------------------------*/

/* Var_in_TA_SV
 * Returns true if the time attribute contains any formal variable
 * that is in the table td.
 */

boolean Var_in_TA_SV( time, td )
     PTimeTyp      time;
     SVdescriptorTyp  *td;
{
  boolean  found1,found2,found3;
  found1 = found2 = found3 = FALSE;
  found1 = Var_in_Expr_SV(time->lower_bound,td);
  found2 = Var_in_Expr_SV(time->upper_bound,td);
  if (time->tvar !=NULL)
    found3 = Var_in_Expr_SV(time->tvar,td);
  return (found1 || found2||found3);
}

#endif


