/******************************************************************
 *  (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 Gomez
 *  David Larrabeiti Lopez
 *
 *  29 Aug 1991
 *
 *  Some general functions to manage LOTOS expressions.
 *
 *  Brief description
 *
 *  COMPILATION FLAGS:
 *     SDEBUG : debugging checks
 *
 *  LOG:
 *     20/07/92. dlarra.
 *     New function that simplifies predicates and offer lists:
 *     SimplifyPredAndOL.
 *
 ******************************************************************/

/* LINTLIBRARY */


#include "babeh.h"
#include "limisc.h"
#include "balotosf.h"
#include "badefca.h"
#include "listdh.h"
#include "baattr.h"
#include "batyperw.h"
#include "basust_v.h"
#include "licell.h"
#include "baattr.h"
#include "batables.h"

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

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

/* TrfStop
 * Transform the behaviour b into stop, using the same memory place.
 */
void TrfStop( b )
     BehTyp b;
{
  BehTyp stop;

  stop = MakeB(0,StopC);
  GlueB(b,stop);
}

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

/* SolvePredicate
 * Rewrite the predicate of a visible action or guard, if it exists.
 * SolvePredicate returns 't', 'f' or 'i' depending on the result.
 * If there is no predicate, return 'T'.
 * Guards have always predicates.
 */
char SolvePredicate( g )
     BehTyp  g;
{
  PredicateTyp  p;
  char     r;
  PAttrTyp a;

  a = LookA(g,PA);
  if (a!=NULL) {
    p = (PredicateTyp)GetAInfo(a);
    r = Evaluate(&p);
    PutAInfo(a,(AttrValueTyp)p);
    return r;
  }
  else
    return 't';
}

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

/* SolvePredicateBeh
 * Take as input an action prefix like g[e];B or a guarded behaviour [e]->B.
 * SolvePredicateBeh transforms those behaviours
 *  into stop                    if predicate e is false ,
 * or
 *  into g;B and B, respectively if e is true.
 * Leave the behaviour unchanged if the predicate is not true nor false.
 * The predicate is not rewritten, it must have already been rewritten.
 */
void SolvePredicateBeh( g )
     BehTyp  g;
{
  PredicateTyp p;
  PAttrTyp     a;
  ExprTyp      e;

  a = LookA(g,PA);
  if (a!=NULL) {
    p = (PredicateTyp)LookAInfo(a);
    LASSERT(p != NULL);
    e = LookRwPred(p);
    if (IsFalse(e))
      TrfStop(g);
    else if (IsTrue(e))
      if (LookType(g)==GateC)
	FreeA(GetA(g,PA));
      else
	GlueCellB1(g);
  }
}

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

/* LookPredicate
 * Look at the predicate of the gate or guard b and returns 'i','f' or 't'
 * depending on the contents of the rewritten predicate :
 * undetermined, false or true respectively.
 */
char LookPredicate( b )
     BehTyp b;
{
  PredicateTyp p;
  PAttrTyp     a;
  ExprTyp      e;

  a = LookA(b,PA);
  if (a!=NULL) {
    p = (PredicateTyp)LookAInfo(a);
    e = LookRwPred(p);
    if (IsFalse(e))
      return 'f';
    else
      if (IsTrue(e))
	return 't';
      else
	return 'i';
  }
  else
    return 't';
}

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

/* GateInPar
 * Say whether gate g is in the gate set of the parallel operator b.
 */
boolean GateInPar( g, b )
     BehTyp g,b;
{
  GateSetTyp    gs;
  DescriptorTyp gd;

  switch( LookNameB(b) )
    {
    case INTER_SYNC:
      return FALSE;
    case FULL_SYNC:
      return TRUE;
    case PART_SYNC:
      gs = (GateSetTyp) LookAInfo(LookA(b,GSA));
      gd = LookName(g);
      return GateInGS(gd,gs);
    default:
      Error("GateInPar: Unexpected synchronization type");
      return FALSE; /*lint*/
    }
}

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

/* GateInHide
 * Say whether gate g is in the gate set of the hide operator b.
 */
boolean GateInHide( g, b )
     BehTyp       g, b;
{
  GateSetTyp      gs;
  DescriptorTyp   gd;

  gs = (GateSetTyp) LookAInfo(LookA(b,GSA));
  gd = LookName(g);
  return GateInGS(gd,gs);
}

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

/* JoinHides
 * Transform :  hide GS1 in hide GS2 in B
 * into      :  hide GS1 U GS2 in B.
 */
BehTyp JoinHides( h )
     BehTyp  h;
{
  BehTyp     h2;
  PAttrTyp   a1,a2;
  GateSetTyp gs1,gs2;

  LASSERT(h!=NULL);
  LASSERT(LookTypeB(h)==HidingC);
  h2 = GetArgB(h,1);
  LASSERT(h2!=NULL);
  LASSERT(LookTypeB(h2)==HidingC);
  a1 = LookA(h,GSA);
  a2 = LookA(h2,GSA);
  gs1 = (GateSetTyp) GetAInfo(a1);
  gs2 = (GateSetTyp) LookAInfo(a2);
  PutAInfo(a1,(AttrValueTyp)JunctionGS(gs1,gs2));
  PutArgB(h,LookArgB(h2,1),1);
  FreeB(h2);
  FreeGS(gs1);
  return h;
}

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

/* Replaceable
 * determine whether ( mequality = " v = f({xi}) " ) where v in vdol,
 *                                                        {xi} not in vdol
 */
static boolean Replaceable( mequality, vdol )
     ExprTyp     mequality;
     ExprListTyp vdol;
{
  ExprListTyp vl, vlAux;
  ExprTyp e1,e2;

  e1 = LookArgE( mequality, 1 );
  e2 = LookArgE( mequality, 2 );
  if ( IsOperationE( e1 ) || !InEL( e1, vdol ) )
    return FALSE;
  vl = (ExprListTyp)VarsInE(e2);
  for ( vlAux = vl; vlAux!=NULL; vlAux=Next_list(vlAux) )
    if ( InEL( (ExprTyp)LookInfo_list(vlAux), vdol ) ) {
      FreeEL(vl);
      return FALSE;
    }
  FreeEL(vl);
  return TRUE;
}

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

static ExprTyp ReverseMBEq( mbe )
     ExprTyp mbe;
{
  ExprTyp e1,e2;

  LASSERT( IsEqual(mbe) );
  e1 = GetArgE( mbe, 1 );
  e2 = GetArgE( mbe, 2 );
  PutArgE( mbe, e2, 1 );
  PutArgE( mbe, e1, 2 );

  return mbe;
}

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

#ifdef SDEBUG
static boolean CheckOut( e )
     ExprTyp e;
{
  if ( IsOperationE(e) )
    return !IsMetaBool(LookNameE(e));
  return TRUE;
}
#endif

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

/* SimplifyPredAndOL
 * Simplify the predicate and offer list of a gate.
 *  Example :
 *
 *        g ?x1 ?x2 ?x3 ?x4 [ x1=v, x2=opn, x3=g(x4) , f(x1,x2,x3,x4) ]
 *
 *    <=> g !v !opn ?x3 ?x4 [ x3=g(x4) , f(v,opn,x3,x4) ]
 *
 *  These subtitutions are also done in the behaviour after the action.
 */
void SimplifyPredAndOL( g )
     BehTyp g;
{
  OfferListTyp    ol, offer;
  ListTyp         pl;
  PredNodeTyp     pn;
  ExprListTyp     vdol;        /*list of variables defined at the offer list */
  ExprTyp         mbe,         /* metaboolean expression */
  expr, var;
  PAttrTyp        pa;          /* predicate attribute */
  SVdescriptorTyp sv;
  PredicateTyp    newpred;

  ol = (OfferListTyp)LookAInfo(LookA(g,OLA));
  pa = LookA( g, PA );
  if ( ol==NULL || pa==NULL )
    return ;
  pl = (ListTyp)LookAInfo( pa );
  newpred = NULL;
  vdol    = VarsDefinedInOL( ol );
  sv      = CreateSV();

  /* transformation */

  while ( pl != NULL ) {
    pn  = (PredNodeTyp)LookInfo_list( pl );
    mbe = pn->rewritten;
    LASSERT( IsEqual(mbe) );
    if ( Replaceable( mbe, vdol ) || Replaceable( ReverseMBEq(mbe), vdol ) ) {
      var  = LookArgE( mbe, 1 );
      expr = LookArgE( mbe, 2 );
      LASSERT( CheckOut(expr) );
      InsertSV( LookNameE( var ), CopyE(expr), &sv );
      offer = LookForVarOL( LookNameE(var), ol );
      FreeE( GetExprOffer(offer) );
      PutKindOffer( offer, EXCLAMATION );
      PutExprOffer( offer, CopyE(expr) );
    }
    else {
      newpred = AddPremisePred(newpred,
			       CopyE(ReverseMBEq(mbe)),   /*mse*/
			       pn->original!=NULL ?
			       CopyE(pn->original) : NULL);
    }
    pl = Next_list(pl);
  }

  /* update predicate  */

  if ( newpred != NULL ) {
    FreePred( (PredicateTyp)GetAInfo( pa ) );
    (void)SubstPredSV( &newpred, &sv );
    PutAInfo( pa,(AttrValueTyp)newpred);
  }
  else
    FreeA( GetA(g,PA) );   /* free pa */

  /* update behaviour after action */
  if (!IsEmptySV(sv))
    SubstBehSV( LookArgB(g,1) , &sv );

  FreeEL( vdol );
  FreeSV( &sv );
}

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

/* GetGates
 * Return a set with the visible gates of a behaviour.
 */
GateSetTyp GetGates( b )
     BehTyp b;
{
  RelabFuncListTyp rfl;
  PITContTyp       pit;
  GateDecListTyp   gdl;
  boolean          cont;
  ITContListTyp    itcl;
  ListTyp          auxl,lastl;
  GateSetTyp       gs,s1,sa,sf,s1bk,s2bk,gsbk,intbk,diffbk,ggbk,rngbk,imgbk;

  cont = TRUE;
  gs   = NewGS();
  while ( cont )
    switch ( LookType(b) )
      {
      case HidingC :
	cont = FALSE;
	gs   = JunctionGS( gsbk=gs,
			  diffbk=DiffGS( ggbk=GetGates(LookB1(b)),
					(GateSetTyp)LookAInfo(LookA(b,GSA))
					)
			  );
	FreeGS(gsbk);
	FreeGS(diffbk);
	FreeGS(ggbk);
	break;

      case RelabellingC :
	cont = FALSE;
	s1   = GetGates(LookB1(b));
	rfl  = (RelabFuncListTyp) LookAInfo(LookA(b,RFLA));
	s1   = DiffGS(s1bk=s1,rngbk=RangeRFL(rfl));
	s1   = JunctionGS(s2bk=s1,imgbk=ImageRFL(rfl));
	gs   = JunctionGS(gsbk=gs,s1);
	FreeGS(s1);
	FreeGS(rngbk);
	FreeGS(imgbk);
	FreeGS(s1bk);
	FreeGS(s2bk);
	FreeGS(gsbk);
	break;

      case GuardC :
      case IC :
      case LetC :
      case PletC :
      case ChoiceC :
	b = LookB1(b);
	break;

      case BehaviourC :
	if (LookB1(b)!=NULL)
	  b = LookB1(b);
	else
	  b = LookB2(b);
	break;

      case ExitC :
      case StopC :
      case TerminationC:
	cont = FALSE;
	break;

      case GateC :
	gs = AddGS(gs,LookName(b));
	b  = LookB1(b);
	break;

      case GateChoiceC:
	s1    = GetGates(LookB1(b));
	gdl   = (GateDecListTyp)LookAInfo(LookA(b,GDLA));
	lastl = NULL;
	do
	  { auxl = gdl;
	    while (Next_list(auxl) != lastl)
	      auxl = Next_list(auxl);
	    lastl = auxl;
	    sf = ((PGateDecTyp)LookInfo_list(auxl))->fgs;
	    intbk = IntersGS(s1,sf);
	    if ( !IsEmptyGS(intbk) ) {
	      s1 = DiffGS(s1bk=s1,sf);
	      sa = GateList_to_GateSet(((PGateDecTyp)
					LookInfo_list(auxl))->agl);
	      s1 = JunctionGS(s2bk=s1,sa);
	      FreeGS(s1bk);
	      FreeGS(s2bk);
	      FreeGS(sa);
	    }
	    FreeGS(intbk);
	  } while (gdl!=lastl);
	gs = JunctionGS(gsbk=gs,s1);
	FreeGS(gsbk);
	FreeGS(s1);
	cont = FALSE;
	break;

      case ParC:
	s1 = GetGates(LookB1(b));
	gdl = (GateDecListTyp)LookAInfo(LookA(b,GDLA));
	lastl = NULL;
	do {
	  auxl = gdl;
	  while (Next_list(auxl) != lastl)
	    auxl = Next_list(auxl);
	  lastl = auxl;
	  sf = ((PGateDecTyp)LookInfo_list(auxl))->fgs;
	  intbk = IntersGS(s1,sf);
	  if (!IsEmptyGS(intbk)) {
	    s1 = DiffGS(s1bk=s1,sf);
	    sa = GateList_to_GateSet(((PGateDecTyp)LookInfo_list(auxl))->agl);
	    s1 = JunctionGS(s2bk=s1,sa);
	    FreeGS(s1bk);
	    FreeGS(s2bk);
	    FreeGS(sa);
	  }
	  FreeGS(intbk);
	} while (gdl!=lastl);
	if ( LookNameB(b)==PART_SYNC )
	  s1 = JunctionGS(s1bk=s1,(GateSetTyp)LookAInfo(LookA(b,GSA)));
	gs = JunctionGS(gsbk=gs,s1);
	FreeGS(s1bk);
	FreeGS(gsbk);
	FreeGS(s1);
	cont = FALSE;
	break;

      case ParallelC :
	gs = JunctionGS(gsbk=gs,ggbk=GetGates(LookB1(b)));
	FreeGS(gsbk);
	FreeGS(ggbk);
	if ( LookNameB(b)==PART_SYNC ) {
	  gs = JunctionGS(gsbk=gs,(GateSetTyp)LookAInfo(LookA(b,GSA)));
	  FreeGS(gsbk);
	}
	b = LookB2(b);
	break;

      case EnablingC :
      case DisablingC :
	gs = JunctionGS( gsbk=gs, ggbk=GetGates(LookB1(b)) );
	FreeGS(gsbk);
	FreeGS(ggbk);
	b = LookB2(b);
	break;

      case AlternativeC:
	while (LookB2(b)!=NULL) {
	  gs = JunctionGS( gsbk=gs, ggbk=GetGates(LookB1(b)) );
	  FreeGS(gsbk);
	  FreeGS(ggbk);
	  b = LookB2(b);
	}
	b = LookB1(b);
	break;

      case ProcessInstC :
      case ProcessDefC :
	sa = GateList_to_GateSet((GateListTyp) LookAInfo(LookA(b,GLA)));
	gs = JunctionGS(gsbk=gs,sa);
	FreeGS(sa);
	FreeGS(gsbk);
	cont = FALSE;
	break;

      case InterleavedC:
	gs = JunctionGS( gsbk=gs, ggbk=GetGates(LookArgB(b,1)) );
	FreeGS(gsbk);
	FreeGS(ggbk);
	b = LookArgB(b,2);
	break;

      case ContSetC:
	itcl = (ITContListTyp)LookAInfo(LookA(b,ITCLA));
	for (; itcl!=NULL ; itcl = Next_list(itcl)) {
	  pit = (PITContTyp)LookInfo_list(itcl);
	  gs  = JunctionGS( gsbk=gs, ggbk=GetGates(pit->b) );
	  FreeGS(gsbk);
	  FreeGS(ggbk);
	}
	cont = FALSE;
	break;

      default :
	Error("GetGates: Unexpected cell.");
      }
  return gs;
}

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

static ListTyp pl;                   /* explored process definitions */
static ListTyp tl;                   /* terminations list output*/

/* FetchTerminations
 * Insert in tl the visible terminations of a behaviour.
 */
static void FetchTerminations( b )
     BehTyp b;
{
  boolean       cont;
  int           procName,term;

  cont = TRUE;
  while (cont)
    switch (LookType(b))
      {
      case HidingC :
      case RelabellingC :
      case GuardC :
      case IC :
      case LetC :
      case GateChoiceC:
      case ParC:
      case PletC :
      case GateC :
      case ChoiceC :
	b = LookB1(b);
	break;

      case BehaviourC :
	if (LookB1(b)!=NULL)
	  b = LookB1(b);
	else
	  b = LookB2(b);
	break;

      case ExitC :
      case StopC :
	cont = FALSE;
	break;

      case TerminationC:
	term = LookNameB(b);
	tl   = Add_IfNotIn_list( (DataListTyp)term, tl, EqInt );
	cont = FALSE;
	break;

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

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

      case ProcessInstC :
      case ProcessDefC :
	procName = LookNameB(b);
	if ( !In_list( (DataListTyp)procName, pl, EqInt ) ) {
	  pl = Insert_list( (DataListTyp)procName, pl );
	  b = LookArgB(GetP_def(procName),1);
	}
	else
	  cont=FALSE;
	break;

      case InterleavedC:
	cont = FALSE;    /* odd case */
	break;


      default :
	Error("GetTerminations: Unexpected cell.");
	break;
      }
}

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

/* GetTerminations
 * Return a list with the visible terminations of a behaviour.
 */
ListTyp GetTerminations( b )
     BehTyp b;
{
  pl = Create_list();
  tl = Create_list();
  FetchTerminations(b);
  Disp_list(pl);

  return tl;

}

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

/* GetSuccessEvent
 * Return the descriptor of the success event gate.
 * If event success does not exist then return -1.
 * If event success is empty ("")  then return 0.
 */
DescriptorTyp GetSuccessEvent( success )
     char *success;
{
  DescriptorTyp sed;

  if (success[0]!='\0') {
    sed = FindG(success);
    if (sed==0) {
      printError("\n      ");
      printError(success);
      printError(": Unknown gate name.\n\n");
      return -1;
    }
    return  sed;
  }
  else
    return 0;
}

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

/* GetTestProcess
 * Return the descriptor of a process.
 * If process does not exist or it has parameters then return -1.
 * If process is empty ("")                       then return  0.
 */
DescriptorTyp GetTestProcess( process )
     char *process;
{
  DescriptorTyp proc;

  if (process[0]!='\0') {
    proc = FindP( process );
    if (proc==0) {
      printError("\n      ");
      printError(process);
      printError(": Unknown process name.\n\n");
      return -1;
    }
    if (LookA(GetP_def(proc),ELA)!=NULL) {
      printError("\n      Error: test processes can not have Data Value Parameters.\n\n");
      return -1;
    }
    return proc;
  }
  return 0;
}

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

/* Compose_b_with_Test
 * Replace b by the parallel composition of the behaviour b and the
 * test process proc, synchronizing in all their gates but success_event.
 *
 *         b[A1] |[A]| proc[A2,success_event],  where A = A1 + A2
 */
BehTyp Compose_b_with_Test( b, proc, success_event )
     BehTyp        b;
     DescriptorTyp proc, success_event;
{
  GateSetTyp  gset,bgset,gsetUbgset;
  GateMaskTyp successMask;
  BehTyp      par, def, inst, suc, enab;
  SortListTyp sl;
  ExprListTyp vl;
  int         func;
  char      * name;

  bgset = GetGates(b);
  if ( GateInGS( success_event, bgset ) ) {
    FreeGS( bgset );
    printError("      Error: the behaviour under test can not contain the success event\n\n");
    return NULL;
  }
  b    = CopyB( b );
  def  = GetArgB(GetP_def(proc),1);
  inst = CopyB(GetP_def(proc));
  PutType(inst,ProcessInstC);
  PutArgB(GetP_def(proc),def,1);

  par         = MakeB(PART_SYNC,ParallelC);
  gset        = GateList_to_GateSet((GateListTyp)LookAInfo(LookA(inst,GLA)));
  gsetUbgset  = JunctionGS( bgset, gset );
  successMask = Descr_to_Mask( success_event );
  PutA(par,MakeA((AttrValueTyp)DiffGS(gsetUbgset,successMask),GSA));
  FreeGS(bgset);
  FreeGS(gset);
  FreeGS(gsetUbgset);
  FreeGS(successMask);

  AddArgB( par, inst );
  AddArgB( par, b );

  if ( (func=GetP_func(proc)) > NOEXITF ) {
    suc = MakeB( success_event, GateC );
    AddArgB( suc, MakeB(0,StopC) );
    enab = MakeB( 0, EnablingC );
    AddArgB( enab, par );
    AddArgB( enab, suc );
    if ( func>EXITF ) {
      vl = CreateEL();
      for ( sl=GetF_sl(GetP_func(proc)); sl!=NULL; sl=Next_list(sl) ) {
	name = (char*)emalloc(3);
	(void)sprintf(name,"%s","nv");
	vl = AddEL( MakeE(Declare_var(name,
				      (DescriptorTyp)LookInfo_list(sl)),
			  VariableC),
		   vl );
      }
      PutA(enab,MakeA((AttrValueTyp)vl,ELA));
    }
    return enab;
  }
  else
    return par;

}

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












