/* version nueva semantica */
/***********************************
  (C) Copyright 1990, 1991; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************
  $Log:  EXit_processing.c,v $
  * Revision 1.1  92/05/20  15:36:55  lotos
  * Initial revision
  * 
  * Revision 1.1  92/01/14  13:07:22  lotos
  * Initial revision
  * 
  ***********************************/

#ifndef lint
static char rcsid[]= "$Id: EXit_processing.c,v 1.1 92/05/20 15:36:55 lotos Exp Locker: lotos $";
#endif

/***********************************
  
  David Larrabeiti Lopez
  
  Oct 29, 1993
  
  Free & Test expansion of a behaviour expressed in the
  Interleaved Expanded form .
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  (none)
  
  ************************************************/

/* LINTLIBRARY */

#include "basynset.h"
#include "expre_br.h"
#include "badefca.h"
#include "baattr.h"
#include "batables.h"
#include "balotosf.h"
#include "limisc.h" 
#include "eximmed.h" 
#include "excomp.h" 
#include "listack.h" 
#include "baprint.h" 


static ITContListTyp CopyPath();
static BehTyp ApplyITC();
static boolean verbose_mode;

/*
 * stop ||| B := B
 */
static void GlueStop( b )
     BehTyp b;
{
  LASSERT( LookTypeB(b)==ParallelC );
  if ( LookTypeB(LookArgB(b,1))==StopC )
    GlueArgB( b, 2 );
  else
    if ( LookTypeB(LookArgB(b,2))==StopC )
      GlueArgB( b, 1 );
}


/* OfferedTerms
 * OT = Offered Terminations
 * -------------------------
 * 
 * OT( B1[]B2 )    = n                 if ( B1=n ) 
 *                 = OT(B1) U OT(B2)   otherwise (* OT(B1) = emptyset or
 *                                                  OT(B2) = emptyset     *)
 * OT( B1|||B2 )   = OT(B1) U OT(B2)
 * OT( B1[>B2 )    = OT(B1) U OT(B2)
 * OT( n )         = n
 * OT( stop )      = emptyset
 * OT( g;B )       = emptyset
 * OT( pi :=B )    = OT( B )
 * OT( otherwise ) = emptyset
 */
ListTyp OfferedTerms( b )
     BehTyp  b;
{
  BehTyp     bi;
  int        i,n;
  ListTyp    tlres, tl1h,tl2h,tli;
  
  tlres = Create_list();
  switch ( LookTypeB(b) )
    {
    case ProcessInstC:
      tlres = OfferedTerms( LookArgB(GetP_def(LookNameB(b)),1) );
      break;
      
    case DisablingC:
    case ParallelC:
      tl1h = OfferedTerms( LookArgB(b,1) );
      tl2h = OfferedTerms( LookArgB(b,2) );
      tlres = Join_list( tl1h, tl2h );
      break;
      
    case ChoiceC:
    case GuardC:
      tlres = OfferedTerms( LookArgB(b,1) );
      break;
      
    case AlternativeC:
      for ( n=NumArgB(b),i=1; i<=n; i++ ) {
        bi = LookArgB(b,i);
        if ( LookTypeB(bi)!=TerminationC ){
          tli   = OfferedTerms( bi );
          tlres = Join_list( tlres, tli );
        }
        else
          tlres = Insert_list( (DataListTyp)LookNameB(bi), tlres );
      }
      break;
      
    case TerminationC:
      tlres = Insert_list( (DataListTyp)LookNameB(b), tlres );
      break;
      
    case IC:
    case GateC:
    case ExitC: 
    case StopC:
    case ContSetC:         /* NEW SEM */
    case EnablingC:
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case GateChoiceC:
    case ParC:
    case InterleavedC:         /* NEW SEM */
      break;
      
    default:
      Error("OfferedTerms : Unexpected cell type");
    }
  
  return tlres;
}


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

/* TerminalTerms
 * TT = Terminal Terminations
 * -------------------------
 * 
 * TT( B1[]B2 )    = TT(B2)            if ( B1=n ) 
 *                 = TT(B1) U TT(B2)   otherwise 
 * TT( B1[>B2 )    = TT(B1) U TT(B2)                   REVISAR !!!!!
 * TT( B1|||B2 )   = TT(B1) U TT(B2)
 * TT( n )         = n
 * TT( stop )      = emptyset
 * TT( g;B )       = TT( B )
 * TT( otherwise ) = error
 */
ListTyp TerminalTerms( b )
     BehTyp  b;
{
  BehTyp     bi;
  int        i,n;
  ListTyp    tlres, tl1h,tl2h,tli;
  
  tlres = Create_list();
  switch ( LookTypeB(b) )
    {
      
    case DisablingC:
    case ParallelC:
      tl1h = TerminalTerms( LookArgB(b,1) );
      tl2h = TerminalTerms( LookArgB(b,2) );
      tlres = Join_list( tl1h, tl2h );
      break;
      
    case ChoiceC:
    case GuardC:
    case IC:
    case GateC:
      tlres = TerminalTerms( LookArgB(b,1) );
      break;
      
    case ExitC: 
    case StopC:
      break;
      
    case AlternativeC:
      for ( n=NumArgB(b),i=1; i<=n; i++ ) {
        bi = LookArgB(b,i);
        if ( LookTypeB(bi)!=TerminationC ){
          tli   = TerminalTerms( bi );
          tlres = Join_list( tlres, tli );
        }
      }
      break;
      
    case TerminationC:
      tlres = Insert_list( (DataListTyp)LookNameB(b), tlres );
      break;
      
    case ContSetC:         /* NEW SEM */
    case EnablingC:
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case GateChoiceC:
    case ParC:
    case InterleavedC:         /* NEW SEM */
    case ProcessInstC:
    default:
      Error("TerminalTerms : Unexpected cell type");
    }
  
  return tlres;
}


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

/* SplitPrefix
 * Split a prefix into its hard , soft & terminations parts :
 * CH1CH2G1g1-CH3g2-G4g3-CH5G6-plet1plet2-n1n2n3n4 =>
 * CH1CH2G1g1-CH3g2-G4g3 , CH5G6plet1plet2, n1n2n3n4
 */
static BehTyp SplitPrefix( prefix, soft_prefix, terms )
     BehTyp prefix, *soft_prefix, *terms;
{
  BehTyp hard, gate, cursor, preterms;
  
  hard         = NULL;
  *soft_prefix = NULL;
  *terms       = NULL;
  
  for ( ;; ){
    gate   = LookActionUB( prefix );
    if ( LookTypeB(gate)!=TerminationC ){
      cursor = GetArgB( gate, 1 );
      hard   = ConcatUB( hard, prefix );
      prefix = cursor;
    }
    else {
      *soft_prefix = prefix;
      break;
    }
  }
  
  preterms = LookPreActionUB(*soft_prefix);
  if ( preterms == NULL ){
    *soft_prefix = NULL;
    *terms       = gate;
  }
  else
    *terms = GetArgB(preterms,1);
  
  
  return hard;
  
}


/* Sort_ChGT
 * example :
 *  Sort_ChGT( Ch1G1 val1 n1;n2 , Ch2G2 val2 n3;n4;n5 ) =
 *   = Ch1Ch2G1G2 val1Uval2 n1;n2;n3;n4
 */  
static BehTyp Sort_ChGT( prefix1, prefix2 )
     BehTyp prefix1, prefix2;
{
  VarAssignListTyp val;
  BehTyp           choices, guards, terms, plet, plets, pletsh,
  hard_prefix1, hard_prefix2,
  soft_prefix1, soft_prefix2, terms1, terms2;
  
  if ( prefix1==NULL )
    return prefix2;
  else
    if ( prefix2==NULL )
      return prefix1;
  
  hard_prefix1 = SplitPrefix( prefix1, &soft_prefix1, &terms1 );
  hard_prefix2 = SplitPrefix( prefix2, &soft_prefix2, &terms2 );
  
  guards  = ExtractUB( soft_prefix1, soft_prefix2, GuardC );
  choices = ExtractUB( soft_prefix1, soft_prefix2, ChoiceC );
  plets   = ExtractUB( soft_prefix1, soft_prefix2, PletC );
  terms   = ExtractUB( terms1, terms2, TerminationC );
  
  if ( soft_prefix1 )
    FreeB( soft_prefix1 );
  if ( soft_prefix2 )
    FreeB( soft_prefix2 );
  FreeB( terms1 );
  FreeB( terms2 );
  
  /* unify plets */
  plet = NULL;
  val  = Create_list(); 
  for ( pletsh=plets; plets!=NULL; plets = LookArgB(plets,1) )
    val = Join_list( val,
		    CopyVAL((VarAssignListTyp)LookAInfo(LookA(plets,VALA))) );
  if ( pletsh != NULL ){
    LASSERT( val!=NULL );
    FreeB( pletsh );
    plet = MakeB( 0, PletC );
    PutA( plet, MakeA((AttrValueTyp)val,VALA) );
  }
  
  return ConcatUB( hard_prefix1,
		  ConcatUB( hard_prefix2,
			   ConcatUB( choices,
				    ConcatUB( guards,
					     ConcatUB( plet,
						      terms ) ) ) ) );
}

static boolean HARD_EXIT;

/* Remainder
 * returns the result of extracting from b1 the terminations given by label.
 * Variable prefix will contain the chain of choices and guards that must
 * precede the transitions enabled.
 *
 * Example :
 *
 * Remainder( choice x:s[](1|||2[]B|||B2), <1,2>, &prefix ) =>
 *                                            B2, prefix = choice x:s[](1;2)
 *             
 */
BehTyp Remainder( b1, label, prefix )
     BehTyp   b1,*prefix;
     LabelTyp label;
{
  int              n,i;
  BehTyp           remp,rem,choice,guard,
  rem1,rem2,remi,prefix1,prefix2,prefixi,plet,gate;
  LabelTyp         lab;
  ExprListTyp      el,vl;
  VarAssignListTyp val;
  
  /* the occurrence of a termination of label in an operand is denoted by
     a non-null prefix */
  
  switch ( LookTypeB(b1) )
    {
      
    case TerminationC:
      if( (lab = LookForLabel( LookNameB(b1), label ))!=NULL ){
        rem     = MakeB( 0, StopC );
        *prefix = CopyOperB(lab);
	if ( LookArgB(*prefix,1)!=NULL )
	  (void)GetArgB(*prefix,1);
	el = (ExprListTyp)LookAInfo(LookA(b1,ELA));
	vl = (ExprListTyp)LookAInfo(LookA(lab,ELA));
	LASSERT(Length_list(el)==Length_list(vl));
	if ( el!=NULL ){
	  el   = CopyEL(el); 
	  val  = Mk_VLEL_VAL( vl, el );
	  plet = MakeB( 0, PletC );
	  PutA(plet,MakeA((AttrValueTyp)val,VALA));
	  AddArgB(plet,*prefix);
	  *prefix = plet;
	}
      }
      else {
        rem    = CopyOperB(b1);
        *prefix = NULL;
      }
      break;
      
    case StopC:
    case ExitC:
      rem = CopyOperB(b1);
      *prefix = NULL;
      break;
      
    case GateC:
    case IC:
      if ( HARD_EXIT ){
        rem1 = rem = Remainder( LookArgB(b1,1), label, prefix );
        if ( *prefix==NULL ){
          rem = CopyOperB(b1);
          (void)GetArgB(rem,1);
          AddArgB( rem, rem1 );
        }
	else {
	  gate = CopyOperB(b1);
	  (void)GetArgB(gate,1);
	  PutArgB(gate,*prefix,1);
	  *prefix = gate;
	}
      }
      else {
        rem = CopyOperB(b1);
        *prefix = NULL;
      }
      break;
      
    case ChoiceC:
      choice = CopyOperB(b1);
      (void)GetArgB(choice,1);
      rem = Remainder( LookArgB(b1,1), label, prefix );
      if ( *prefix!=NULL )
        *prefix = Pre_Branch_Choice( ConcatUB(choice,*prefix) );
      else
        rem = Distribute_Choice( ConcatUB(choice,rem) );
      break;
      
    case GuardC:
      guard = CopyOperB(b1);
      (void)GetArgB(guard,1);
      rem = Remainder( LookArgB(b1,1), label, prefix );
      if ( *prefix!=NULL )
        *prefix = Pre_Branch_Guard( ConcatUB(guard,*prefix) );
      else
        rem = Distribute_Guard( ConcatUB(guard,rem) );
      break;
      
    case ParallelC: 
      rem1    = Remainder( LookArgB(b1,1), label, &prefix1 );
      rem2    = Remainder( LookArgB(b1,2), label, &prefix2 );
      *prefix = Sort_ChGT( prefix1, prefix2 );
      if ( LookTypeB(rem1)==StopC )            /* stop|||B == stop */
        rem = rem2;
      else
        if ( LookTypeB(rem2)==StopC )
          rem = rem1;
        else {
          rem = CopyOperB( b1 );
          (void)GetArgB(rem,1);
          (void)GetArgB(rem,2);
          AddArgB( rem, rem1 );
          AddArgB( rem, rem2 );
        }
      break;
      
      
    case DisablingC:
      remp    = CopyOperB(b1);
      (void)GetArgB(remp,1);
      (void)GetArgB(remp,2);
      *prefix = NULL; 
      for ( n=2, i=1; i<=n; i++ ){
        remi = Remainder( LookArgB(b1,i), label, &prefixi );
        if ( prefixi!=NULL ){
          rem     = remi;
          *prefix = prefixi;
          break;
        }
        else
          PutArgB( remp, remi, i );
      }
      if ( *prefix!=NULL )
        FreeB(remp );
      else
        rem = remp;
      break;
      
      
      
    case AlternativeC:
      remp    = NULL;
      *prefix = NULL; 
      for ( n=NumArgB(b1),i=1; i<=n; i++ ){
        remi = Remainder( LookArgB(b1,i), label, &prefixi );
        if ( prefixi!=NULL ){
          rem = remi;
          *prefix = prefixi;
          break;
        }
        else
          remp = AppendUB( remp, remi );
      }
      if ( *prefix!=NULL ){
        if ( remp!=NULL )
          FreeB(remp );
      }
      else
        rem = remp;
      break;
      
      
      
    case ProcessInstC:
    case EnablingC:  
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case ProcessDefC:
    case SpecificationC:
    case GateChoiceC:
    case ParC:
    case BehaviourC:
    case InterleavedC:
    default:
      Error("Remainder : unexpected cell type");
      break;
      
    }
  LASSERT(rem!=NULL);
  return rem;
}


/* ConnectPrefix
 * Take out the terminations from a prefix and distribute the soft part
 * into the choice.
 * Still leave hard prefix apart.
 */
static BehTyp ConnectPrefix( prefix, itc_b, hard_prefix, terms )
     BehTyp prefix, itc_b, *hard_prefix, *terms; 
{
  int    n,i;
  BehTyp res,soft_prefix;
  
  *hard_prefix = NULL;
  if ( prefix==NULL )
    return itc_b;
  
  *hard_prefix = SplitPrefix( prefix, &soft_prefix, terms );
  
  if ( soft_prefix==NULL )
    return itc_b ;
  
  n = NumArgIB(itc_b);
  if ( n==1 )
    return ConcatUB(soft_prefix,itc_b);
  
  res = NULL;
  for ( i=1; i<n; i++ ) 
    res = AppendUB( res, ConcatUB(CopyB(soft_prefix),GetArgB(itc_b,i)) );
  res = AppendUB( res, ConcatUB(soft_prefix,GetArgB(itc_b,n)) );
  FreeB( itc_b );
  
  return res ;
  
}


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

/* Exits
 * return the alternative of transitions offered only by the continuations
 * of the IT "it" .
 * The first operand (b1) must have been iexp_pre_processed to get rid of
 * process instantiations.
 * if all==TRUE then return the continuations to all the terminations
 * of b1.                                        ---
 */
BehTyp Exits( it, all )
     BehTyp  it;
     boolean all;
{
  ListTyp       tl;
  ITContListTyp itcl;
  PITContTyp    itc;
  BehTyp        itc_b,arg,gate,out,b1,bi,itb,par,rem,prefix,
  hard_prefix, terms;
  int           n,i;
  
  
  HARD_EXIT = all;
  
  out   = NULL;
  b1    = LookArgB(it,1);
  if ( HARD_EXIT )
    /* tl    = TerminalTerms( b1 ); */
    tl  = GetTerminations( b1 );
  else
    tl  = OfferedTerms( b1 );
  
  if ( tl==NULL )
    return NULL;
  
  itcl  = (ITContListTyp)LookAInfo(LookA(LookArgB(it,2),ITCLA));
  for ( ; itcl!=NULL; itcl = Next_list(itcl) ){
    itc = (PITContTyp)LookInfo_list(itcl);
    if ( SubLabelList( itc->label, tl ) ){
      itc_b  = Iexp_Pre_Proc( CopyUntilActB(itc->b) );     /* instantiations */
      rem    = Remainder( b1, itc->label, &prefix );
      itc_b  = ConnectPrefix( prefix, itc_b, &hard_prefix, &terms );
      FreeB(terms);
      /**/ /* AMMEND */
      if ( hard_prefix!=NULL )
	FreeB( hard_prefix );
      
      itc_b  = Iexp_Pre_Proc( itc_b );                   /* advance new plet */
      for ( n = NumArgIB(itc_b), i=1 ; i<=n ; i++ ) {
        arg  = LookArgIB(itc_b,i); 
        gate = LookActionUB(arg);
        LASSERT( LookTypeB(gate)==GateC || LookTypeB(gate)==IC ||
		LookTypeB(gate)==ExitC ||
		LookTypeB(gate)==StopC    /* only due to plet assignations */
		); 
        if ( LookTypeB(gate)==GateC || LookTypeB(gate)==IC ){
          bi   = GetArgB(gate,1);
          par  = MakeB( INTER_SYNC, ParallelC );
          AddArgB( par, CopyUntilActB(rem) );    /* prevent GlueStop effects */
          AddArgB( par, bi );
          GlueStop( par );
          itb  = CopyOperB(it);
          (void)GetArgB( itb, 1 ); 
          PutArgB( itb, par, 1 );
          PutArgB( gate, itb, 1 );
        }
	if ( LookTypeB(gate)!=StopC )
	  out = AppendUB( out, arg );
      }
      FreeB(rem);
    }
  }
  return out;
}

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

/* OldIT_Processing
 * Extract the first actions that an IT can offer
 */
BehTyp OldIT_Processing( b )
     BehTyp b;
{
  BehTyp        b1,out, gate, bi, bb, arg, b1p, exits;
  int           n,i,i_rm_depth,flagsbkup;
  
  b               = GetUntilActB(b);  /* to avoid SHARED_EXP effect */
  b1              = LookArgB( b, 1 ); 
  out             = NULL;
  i_rm_depth      = 0;
  b1              = Iexp_Pre_Proc( GetArgB(b,1) );
  PutArgB( b, b1, 1 );
  flagsbkup       = expansion_flags;
  expansion_flags = NOT_PRE_PROC_EXP;
  b1p             = Pre_Branch( b1, &i_rm_depth );
  expansion_flags = flagsbkup;
  n  = NumArgIB( b1p );
  for ( i=1 ; i<=n; i++ ) {
    arg  = CopyUntilActB( LookArgIB( b1p, i ) );
    gate = LookActionUB(arg);
    switch( LookTypeB(gate) )
      {
      case IC:
      case GateC:
        out = AppendUB ( out, arg );
        bi = GetArgB(gate,1);
        bb = CopyOperB(b);
        (void)GetArgB( bb, 1 ); 
        PutArgB( bb, bi, 1 );
        PutArgB( gate, bb, 1 );
        break;
	
      case ExitC:
        out = AppendUB ( out, arg );
        break;
	
      case TerminationC:
      case StopC:
        FreeB(arg);
        break;
	
      default:
        Error( "IT_Processing: unexpected cell type");
        break;
	
      }
  }
  FreeB(b1p);
  
  exits     = Exits( b, FALSE );
  out       = AppendUB ( out, exits );
  
  if ( out==NULL )
    out = MakeB( 0, StopC );
  
  FreeB( b ); 
  
  return out;
  
}

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


/******************************************************************
 *                                                                *
 *              Testing Aux. functions                            *
 *                                                                *
 *******************************************************************/

static int termd, terma, terme, terms;
static DescriptorTyp successEvent=0;
static ITContListTyp sitcl;
static boolean nonSolvedPred;

/* TestResult
 * Prints the result of the test analysis.
 */
static void TestResult(proc)
     DescriptorTyp proc;
{
  char buff[55];
  
  if ( proc!=(DescriptorTyp)NULL ) {
    printTarget("\n    Process Test = ");
    PrintP( proc, printTarget  );
  }
  printTarget("\n    Test result  = ");
  if ( terma==0 )
    printTarget("REJECT.\n");
  else if ( (terme==0) && (termd==0) && (terms==0) )
    printTarget("MUST PASS.\n");
  else {
    printTarget("MAY PASS.\n\n    ");
    /*
       PrintInt(printTarget,terma+terms+termd+terme);
       printTarget(" executions analysed: \n");
       */
  }
  (void)sprintf(buff,"\n");
  printTarget(buff);
  (void)sprintf(buff,"        succesful situations = %1d\n",terma);
  printTarget(buff);
  (void)sprintf(buff,"         deadlock situations = %1d\n",terms);
  printTarget(buff);
  (void)sprintf(buff,"                       exits = %1d\n",terme);
  printTarget(buff);
  (void)sprintf(buff,"               cuts by depth = %1d\n",termd);
  printTarget(buff);
  if ( nonSolvedPred==TRUE ) {
    Warning("Invalid test. There are unresolved predicates or guards.\n");
  }
  printTarget("\n");
}

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

static boolean IsSuccessfulState( b )
     BehTyp b;
{
  int n,i;
  
  while ( b!=NULL )
    switch( LookTypeB(b) )
      {
      case GateC:
        return LookNameB(b)==successEvent;
	
      case ExitC:
	terme++; /**/
      case IC:
      case TerminationC:
      case StopC:
        b = NULL;
        break;
	
      case GuardC:
        nonSolvedPred = TRUE;
      case ChoiceC:
      case DisablingC:
      case ParallelC:
      case AlternativeC:
        for ( n=NumArgB(b), i=2; i<=n; i++ ) {
          if ( IsSuccessfulState( LookArgB(b,i) ) )
            return TRUE;
        }
        b = LookArgB(b,1);
        break;
	
      default:
        Error("IsSuccessfulState: unexpected cell type");
        break;
	
      }
  return FALSE;
}


/* DeadTerms
 * may_succeed : the success event is in the current behaviour.
 * stop_deadlock : there is at least one g;stop|exit down here.
 *                  => DT( g;stop|||B ) = DT(B)
 */
static ListTyp DeadTerms( b, stop_deadlock, may_succeed )
     BehTyp  b;
     boolean *stop_deadlock, *may_succeed;
{
  BehTyp     bi,b1,b2;
  int        i,n;
  ListTyp    dlres, dl1h,dl1,dl2h,dl2,dli;
  LabelTyp   d1,d2,d1_d2,new_label;
  boolean    stop_deadlock1, stop_deadlock2, may_succeed1, may_succeed2;
  PITContTyp itc;
  
  dlres = Create_list();
  *may_succeed = FALSE;
  
  switch ( LookTypeB(b) )
    {
    case ParallelC:
      b1             = LookArgB(b,1);
      dl1h           = DeadTerms( b1, &stop_deadlock1, &may_succeed1 );
      b2             = LookArgB(b,2);
      dl2h           = DeadTerms( b2, &stop_deadlock2, &may_succeed2 );
      *stop_deadlock = stop_deadlock1 && stop_deadlock2;
      *may_succeed    = may_succeed1 || may_succeed2;
      /*
	 if ( *may_succeed ){
	 Free_LL( dl1h );
	 Free_LL( dl2h );
	 break;
	 }
	 */
      for ( dl1=dl1h; dl1!=NULL; dl1=Next_list(dl1) ) {
        d1 = (LabelTyp)LookInfo_list(dl1);
        for ( dl2=dl2h; dl2!=NULL; dl2=Next_list(dl2) ){
          d2 = CopyLabel((LabelTyp)LookInfo_list(dl2));
          d1_d2 = JoinLabel( CopyLabel(d1), d2 );
          itc = LookFor_SubSet_ITCL(sitcl,d1_d2);
          if ( itc==NULL /* || (itc!=NULL && itc->isDeadlock ) */ ){
            dlres = Insert_LL( d1_d2, dlres );
	  }
          else {
            FreeLabel( d1_d2 );
          }
        }
      }
      if ( stop_deadlock2 )
        dlres = Join_list( dlres, dl1h );
      else
        Free_LL( dl1h );
      if ( stop_deadlock1 )
        dlres = Join_list( dlres, dl2h );
      else
        Free_LL( dl2h );
      break;
      
    case DisablingC:
      if ( IsSuccessfulState(b) ){
        *may_succeed = TRUE;
        *stop_deadlock = FALSE;
        break;
      }
      bi = LookArgB(b,1);
      dli   = DeadTerms( bi, &stop_deadlock1, &may_succeed1 );
      dlres = Join_list( dlres, dli );
      bi = LookArgB(b,2);
      if ( LookTypeB(bi)!=TerminationC ){
	dli   = DeadTerms( bi, &stop_deadlock2, &may_succeed2 );
	dlres = Join_list( dlres, dli );
      }
      *stop_deadlock = stop_deadlock2;
      *may_succeed   = may_succeed1 || may_succeed2;
      break;
      
      
    case AlternativeC:
      if ( IsSuccessfulState(b) ){
        *may_succeed = TRUE;
        *stop_deadlock = FALSE;
        break;
      }
      *stop_deadlock = FALSE;
      *may_succeed    = FALSE;
      for ( n=NumArgB(b),i=1; i<=n; i++ ) {
        bi = LookArgB(b,i);
        if ( LookTypeB(bi)!=TerminationC ){
          dli   = DeadTerms( bi, &stop_deadlock1, &may_succeed1 );
          /* if ( !may_succeed1 )*/
          dlres = Join_list( dlres, dli );
          *stop_deadlock = *stop_deadlock || stop_deadlock1;
          /* *may_succeed = *may_succeed && may_succeed1; */
          *may_succeed   = *may_succeed || may_succeed1;
        }
      }
      break;
      
    case TerminationC:
      new_label = InsertLabel(MakeB(LookNameB(b),TerminationC),
			      (LabelTyp)NULL);
      itc = LookFor_SubSet_ITCL(sitcl,new_label);
      if ( itc==NULL ){
        dlres = Insert_LL( new_label, dlres );
      }
      else{
        FreeLabel( new_label );
      }
      *stop_deadlock = FALSE;
      *may_succeed   = FALSE;
      break;
      
    case GateC:
      if ( LookNameB(b)==successEvent ){
        LASSERT( dlres == NULL );
        *stop_deadlock = FALSE;
        *may_succeed    = TRUE;
        return dlres;
      }
      else {
        dlres         = DeadTerms( LookArgB(b,1), stop_deadlock, may_succeed );
        nonSolvedPred = LookA(b,PA)!=NULL;
      }
      break;
      
    case GuardC:
      nonSolvedPred = TRUE;
    case ChoiceC:
    case IC:
      dlres = DeadTerms( LookArgB(b,1), stop_deadlock, may_succeed );
      break;
      
    case ExitC:
    case StopC:
      *stop_deadlock = TRUE;
      *may_succeed   = FALSE;
      break;
      
    case ContSetC:
    case EnablingC:
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case ProcessInstC:
    case GateChoiceC:
    case ParC:
    default:
      Error("DeadTerms : Unexpected cell type");
    }
  
  return dlres;
}



/* Is_Deadlock
 */
boolean Is_Deadlock( b, cs, ll )
     BehTyp  b,cs;
     ListTyp *ll;
{
  boolean stop_deadlock, may_succeed;
  
  stop_deadlock = FALSE;
  sitcl         = (ITContListTyp)LookAInfo(LookA(cs,ITCLA));
  *ll           = DeadTerms( b, &stop_deadlock, &may_succeed );
  if ( may_succeed ){
    terma++;
  }
  if ( stop_deadlock || *ll!=NULL ){
    terms++;
    return TRUE;
  }
  return FALSE;
}



/* ApplicableConts
 * return a list of pointers to the itc's enabled by B1 in IT( B1, UcBc )
 * The first operand (b1) must have been iexp_pre_processed to get rid of
 * process instantiations.
 * if all==TRUE then return the continuations to all the terminations
 * of b1, including those not offered yet.       ---
 */
static StackTyp ApplicableConts( it, all )
     BehTyp  it;
     boolean all;
{
  ListTyp       tl;
  StackTyp      res;
  ITContListTyp itcl;
  PITContTyp    itc;
  BehTyp        b1;
  
  HARD_EXIT = all;
  
  b1    = LookArgB(it,1);
  if ( HARD_EXIT )
    tl  = GetTerminations( b1 );
  else
    tl  = OfferedTerms( b1 );
  
  if ( tl==NULL )
    return NULL;
  
  res = Create_Stack();
  itcl  = (ITContListTyp)LookAInfo(LookA(LookArgB(it,2),ITCLA));
  for ( ; itcl!=NULL; itcl = Next_list(itcl) ){
    itc = (PITContTyp)LookInfo_list(itcl);
    if ( SubLabelList( itc->label, tl ) ){
      res = Save_Stack( (DataStackTyp)itc, res );
    }
  }
  return res;
}



/* OldApplyITC
 * return the result of escaping from b1 through the continuation itc of IT
 */
static BehTyp OldApplyITC( it, b1, itc, hard_prefix, actual_label )
     BehTyp     it, b1, *hard_prefix;
     LabelTyp  *actual_label;
     PITContTyp itc;
{
  BehTyp        itc_b,arg,gate,out,bi,itb,par,rem,prefix,term,next;
  int           n,i;
  
  out    = NULL;
  itc_b  = Iexp_Pre_Proc( CopyUntilActB(itc->b) );     /* instantiations */
  rem    = Remainder( b1, itc->label, &prefix );
  itc_b  = ConnectPrefix( prefix, itc_b, hard_prefix, &term ); 
  itc_b  = Iexp_Pre_Proc( itc_b );                   /* advance new plet */
  for ( n = NumArgIB(itc_b), i=1 ; i<=n ; i++ ) {
    arg  = LookArgIB(itc_b,i); 
    gate = LookActionUB(arg);
    LASSERT( LookTypeB(gate)==GateC || LookTypeB(gate)==IC ||
	    LookTypeB(gate)==ExitC ||
	    LookTypeB(gate)==StopC    /* only due to plet assignations */
	    ); 
    if ( LookTypeB(gate)==GateC || LookTypeB(gate)==IC ){
      bi   = GetArgB(gate,1);
      par  = MakeB( INTER_SYNC, ParallelC );
      AddArgB( par, CopyUntilActB(rem) );    /* prevent GlueStop effects */
      AddArgB( par, bi );
      GlueStop( par );
      itb  = CopyOperB(it);
      (void)GetArgB( itb, 1 ); 
      PutArgB( itb, par, 1 );
      PutArgB( gate, itb, 1 );
    }
    if ( LookTypeB(gate)!=StopC )
      out = AppendUB( out, arg );
  }
  FreeB(rem);
  
  *actual_label = (LabelTyp)NULL;
  for ( ; term!=NULL; term=next ){
    LASSERT(LookTypeB(term)==TerminationC);
    next = LookArgB(term,1);
    if ( next!=NULL )
      next = GetArgB(term,1);
    *actual_label = InsertLabel( term, *actual_label ); 
  }
  return out;
}


static boolean Success( b1 )
     BehTyp b1;
{
  if ( IsSuccessfulState( b1 ) ){
    terma++;
    return TRUE;
  }
  return FALSE;
}


/* Deadlock
 * Static Deadlock Analysis.
 * If deadlock print tracing information.
 * path_stk is the stack with the applied actual itc's label path.
 * path_stk->int_b is the hard_prefixes stack for those itcs.
 * path_stk->sync_b is the gate being explored of those itcs.
 */
static boolean Deadlock( b1, cs, path_stk )
     BehTyp   b1,cs;
     StackTyp path_stk;
{
  ListTyp    ll, path,pathh;
  PITContTyp itc;
  BehTyp     cursor;
  
  if ( Is_Deadlock( b1, cs, &ll ) ){
    
    if ( verbose_mode ){
      printTarget("\nPath:\n");
      pathh = Reverse_list( Stack_to_list(Copy_Stack(path_stk,EchoInt)) );
      for ( path = pathh; path!=NULL; path = Next_list(path) ){
	itc    = (PITContTyp)LookInfo_list(path);
	if ( itc!=NULL ){
	  cursor = itc->int_b;
	  while ( cursor!=NULL ){
	    PrintBeh(cursor,1,NO_PROC,FALSE," ",printTarget,FALSE,FALSE);
	    cursor = LookArgB(cursor,1);
	  }
	  PrintLabel( itc->label, printTarget );
	  printTarget("\n");
	  PrintBeh(itc->sync_b,1,NO_PROC,FALSE," ",printTarget,FALSE,FALSE);
	}
      }
      Disp_list( pathh );
      printTarget("Deadlock:");
      Print_LL( printTarget, ll );
      printTarget("\n");
      PrintBeh(b1,-1,NO_PROC,FALSE," ",printTarget,FALSE,FALSE);
      printTarget("\n");
    }
    return TRUE;                  /**/ /* MUST I GO ON ? */
  }
  return FALSE;
}

static HashDTyp paths;



/* IT_Deadlock
 * analyse whether an IT has deadlocks i.e.
 * all branches are stop | n1 , or have a subbranch with format : g;n2 | g;stop
 */
void IT_Deadlock( b )
     BehTyp b;
{
  BehTyp        it,b1,cs, gate, arg, exits, hard_prefix;
  LabelTyp      actual_label;
  int           n,i,num_args;
  StackTyp      arg_stk,b1_stk,aitc_stk_stk,path_stk,aitc_stk;
  PITContTyp    aitc,aitc2;
  
  LASSERT( LookTypeB(b)==InterleavedC );
  
  b1_stk       = Create_Stack();
  aitc_stk_stk = Create_Stack();
  path_stk     = Create_Stack();
  arg_stk      = Create_Stack();
  b1           = LookArgB( b, 1 ); 
  cs           = LookArgB( b, 2 ); 
  
  if ( !Success( b1 ) ) { 
    
    (void)Deadlock( b1, cs, path_stk );
    
    aitc_stk     = ApplicableConts( b, TRUE );
    aitc_stk_stk = Save_Stack( (DataStackTyp)aitc_stk, aitc_stk_stk );
    b1_stk       = Save_Stack( (DataStackTyp)b1,       b1_stk );
    arg_stk      = Save_Stack( (DataStackTyp)1,        arg_stk );
    
    while ( !IsEmpty_Stack(b1_stk) ){
      b1 = (BehTyp)Look_Stack(b1_stk);
      aitc_stk = (StackTyp)Look_Stack( aitc_stk_stk );
      
      if ( IsEmpty_Stack(aitc_stk) ){
	FreeB((BehTyp)Get_Stack(&b1_stk));
	(void)Get_Stack(&aitc_stk_stk);
	num_args = (int)Get_Stack(&arg_stk);
	if ( num_args > 1 )
	  arg_stk  = Save_Stack( (DataStackTyp)(num_args-1), arg_stk );
	else {
	  aitc2 = (PITContTyp)Get_Stack(&path_stk);
	  if ( aitc2!=NULL ){
	    if ( aitc2->int_b != NULL )
	      FreeB( aitc2->int_b );
	    aitc2->sync_b = NULL;
	    DispITC( aitc2 );
	  }
	  else {
	    aitc2 = aitc2;
	    /* LASSERT( Count_Stack(b1_stk) == 1 ); */
	  }
	}
      }
      else {
	aitc_stk     = (StackTyp)   Get_Stack(&aitc_stk_stk);
	aitc         = (PITContTyp) Get_Stack(&aitc_stk);
	aitc_stk_stk = Save_Stack( (DataStackTyp)aitc_stk, aitc_stk_stk );
	
	if ( Count_Stack(b1_stk) > 1 ){
	  aitc2         = (PITContTyp) Look_Stack(path_stk);
	  aitc2->sync_b = b1;
	  b1            = LookArgB(LookArgB(LookActionUB(b1),1),1);
	}
	exits = ApplyITC( b, b1, aitc, &hard_prefix, &actual_label );
	
	aitc2 = NewITC();
	aitc2->label = actual_label;
	aitc2->int_b = hard_prefix;
	
	path_stk = Save_Stack( (DataStackTyp)aitc2, path_stk );
	
	n       = NumArgIB(exits);
	arg_stk = Save_Stack( (DataStackTyp)n, arg_stk );
	for ( i=1; i<=n; i++ ){
	  arg     = GetArgIB( exits, i );
	  if ( SearchCellUntilActUB(arg,GuardC)!=NULL )
	    nonSolvedPred = TRUE;
	  gate = LookActionUB(arg);
	  switch( LookTypeB(gate) )
	    {
	    case GateC:
	      nonSolvedPred = LookA(gate,PA)!=NULL;
	    case IC:
	      aitc2         = (PITContTyp) Look_Stack(path_stk);
	      aitc2->sync_b = arg;
	      if ( In_HT( paths, (DataHashTyp)path_stk ) ){
		aitc_stk = NULL;
#ifdef IEXPDBG
		(void)printf("duplicado path\n");
#endif
	      }
	      else {
		Insert_HT( paths, (DataHashTyp)CopyPath(path_stk) );
		it            = LookArgB(gate,1);
		b1            = LookArgB(it,1);
		if ( !Success( b1 ) ){
		  (void)Deadlock( b1, cs, path_stk );
		  aitc_stk = ApplicableConts( it, TRUE );
		}
		else
		  aitc_stk = NULL;
	      }
	      aitc_stk_stk = Save_Stack( (DataStackTyp)aitc_stk,aitc_stk_stk );
	      b1_stk       = Save_Stack( (DataStackTyp)arg, b1_stk );
	      break;
	      
	    case ExitC:
	      terme++;
	    case StopC:
	      num_args = (int)Get_Stack(&arg_stk);
	      arg_stk  = Save_Stack( (DataStackTyp)(num_args-1), arg_stk );
	      break;
	      
	    default:
	      Error( "IT_Deadlock: unexpected cell type");
	      break;
	    }
	}
	if ( LookTypeB(exits)==AlternativeC )
	  FreeB(exits);
      }
      
    }
    LASSERT(IsEmpty_Stack(b1_stk));
    LASSERT(IsEmpty_Stack(aitc_stk_stk));
    LASSERT(IsEmpty_Stack(path_stk));
    LASSERT(IsEmpty_Stack(arg_stk));
  }
}


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

static void FreePath( itcl )    
     ITContListTyp itcl;
{
  PITContTyp itc;
  for ( ; itcl!=NULL; itcl = Next_list(itcl) ){
    itc  = (PITContTyp)LookInfo_list(itcl);
    FreeLabel(itc->label);
    if ( itc->int_b ){
      FreeB( itc->int_b );
      itc->int_b= NULL;
    }
    if ( itc->sync_b ){
      FreeB( itc->sync_b );
      itc->sync_b= NULL;
    }
    DispITC(itc);
  }
}

static ITContListTyp CopyPath( itcl )   
     ITContListTyp itcl;
{
  ITContListTyp  itclres;
  PITContTyp itc,itc2;
  
  itclres = Create_list();
  for ( ; itcl!=NULL; itcl = Next_list(itcl) ){
    itc  = (PITContTyp)LookInfo_list(itcl);
    itc2 = NewITC();
    itc2->label = CopyLabel(itc->label);
    if ( itc->int_b ){
      itc2->int_b = CopyB( itc->int_b );
    }
    if ( itc->sync_b ){
      itc2->sync_b = CopyB( itc->sync_b );
    }
    itclres = Add_list( (DataListTyp)itc2, itclres );
  }
  return itclres;
}


static boolean CompareBehaviorIEXP( b1, b2 )
     BehTyp b1,b2;
{
  boolean equal;
  
  if ( LookNameB(b1)!=LookNameB(b2) )
    return FALSE;
  Init_VPTable();
  equal = Comp_Beh( b1, b2 );
  
  return equal;
}

static boolean EqualPath( p1, p2 )
     ITContListTyp p1, p2;
{
  PITContTyp itc,itc2;
  
  if ( Length_list(p1)!=Length_list(p2) )
    return FALSE;
  
  for ( ; p1!=NULL; p1=Next_list(p1) ){
    itc  = (PITContTyp)LookInfo_list(p1);
    itc2 = LookForITCL( p2, itc->label );
    if ( itc2==NULL )
      return FALSE;
    /*
       if ( itc->int_b !=NULL && itc2->int_b==NULL )
       return FALSE;
       if ( itc2->int_b !=NULL && itc->int_b==NULL )
       return FALSE;
       if ( itc->int_b && itc2->int_b)
       if ( !CompareBehaviorIEXP( itc->int_b, itc2->int_b ) )
       return FALSE;
       */
    
    if ( itc->sync_b !=NULL && itc2->sync_b==NULL )
      return FALSE;
    if ( itc2->sync_b !=NULL && itc->sync_b==NULL )
      return FALSE;
    if ( itc->sync_b && itc2->sync_b)
      /*
	 if ( !CompareBehaviorIEXP( itc->sync_b, itc2->sync_b ) )
	 return FALSE;
	 */
      if ( LookNameB( LookActionUB(itc->sync_b) )
	  != LookNameB(LookActionUB(itc2->sync_b)) )
	return FALSE; /* chapuza */
  }
  return TRUE;
}


/* HashKeyPath
 */
static int HashKeyPath( p )
     ITContListTyp p;
{
  PITContTyp itc;
  int res = 0;
  
  for ( ; p!=NULL; p=Next_list(p) ){
    itc = (PITContTyp)LookInfo_list(p);
    res +=HashKeyLabel(itc->label);
  }
  return res;
}

/* IT_Testing
 */
void IT_Testing( b, success_event, proc, verb )
     BehTyp        b;
     DescriptorTyp success_event, proc;
     boolean       verb;
{
  printTarget("Test Response Analysis\n"); 
  paths = Create_HT( 3000, FreePath, HashKeyPath, EqualPath, (void(*) ())NULL );
  verbose_mode  = verb;
  nonSolvedPred = FALSE;
  successEvent  = success_event;
  termd = terma = terme = terms = 0;
  IT_Deadlock( b );
  successEvent = (DescriptorTyp)NULL;
  TestResult( proc );
  Free_HT( paths );
}


/***********************************************************************/
/*                                                                     */
/*                         NEW SEMANTICS                               */
/*                                                                     */
/***********************************************************************/


/* MakePrefix
 * 
 * As a side-effect leave in *l a list of pointers to the operators of b
 * directly envolved in the generation of the terminations in label.
 *
 * Example : TPO( 1[]B|||(B2|||2[]B3) , <1,2> ) => the following list :
 *                  ^  ^     ^ ^ ^
 * order            2  1     3 5 4
 * 
 */
static BehTyp MakePrefix( b1, label, l )
     BehTyp   b1;
     LabelTyp label;
     ListTyp  *l;
{
  int              n,i;
  BehTyp           choice,guard,prefix,
  prefix1,prefix2,plet,gate;
  LabelTyp         lab;
  ExprListTyp      el,vl;
  VarAssignListTyp val;
  
  /* the occurrence of a termination of label in an operand is denoted by
     a non-null prefix */
  
  prefix = NULL;
  switch ( LookTypeB(b1) )
    {
      
    case TerminationC:
      if( (lab = LookForLabel( LookNameB(b1), label ))!=NULL ){
        prefix = CopyOperB(lab);
	if ( LookArgB(prefix,1)!=NULL )
	  (void)GetArgB(prefix,1);
	el = (ExprListTyp)LookAInfo(LookA(b1,ELA));
	vl = (ExprListTyp)LookAInfo(LookA(lab,ELA));
	LASSERT(Length_list(el)==Length_list(vl));
	if ( el!=NULL ){
	  el   = CopyEL(el); 
	  val  = Mk_VLEL_VAL( vl, el );
	  plet = MakeB( 0, PletC );
	  PutA(plet,MakeA((AttrValueTyp)val,VALA));
	  AddArgB(plet,prefix);
	  prefix = plet;
	}
      }
      else {
        prefix = NULL;
      }
      break;
      
    case StopC:
    case ExitC:
      prefix = NULL;
      break;
      
    case GateC:
    case IC:
      if ( HARD_EXIT ){
        prefix =  MakePrefix( LookArgB(b1,1), label, l );
        if ( prefix!=NULL ){
	  gate = CopyOperB(b1);
	  (void)GetArgB(gate,1);
	  PutArgB(gate,prefix,1);
	  prefix = gate;
	}
      }
      else {
        prefix = NULL;
      }
      break;
      
    case ChoiceC:
      prefix = MakePrefix( LookArgB(b1,1), label, l );
      if ( prefix!=NULL ){
	choice = CopyOperB(b1);
	(void)GetArgB(choice,1);
        prefix = Pre_Branch_Choice( ConcatUB(choice,prefix) );
      }
      break;
      
    case GuardC:
      prefix = MakePrefix( LookArgB(b1,1), label, l );
      if ( prefix!=NULL ){
	guard = CopyOperB(b1);
	(void)GetArgB(guard,1);
        prefix = Pre_Branch_Guard( ConcatUB(guard,prefix) );
      }
      break;
      
    case ParallelC: 
      prefix1 = MakePrefix( LookArgB(b1,1), label, l );
      prefix2 = MakePrefix( LookArgB(b1,2), label, l );
      prefix = Sort_ChGT( prefix1, prefix2 );
      break;
      
      
    case DisablingC:
      prefix = NULL; 
      for ( n=2, i=1; i<=n; i++ ){
        prefix = MakePrefix( LookArgB(b1,i), label, l );
	if ( prefix!=NULL )
	  break;
      }
      break;
      
      
      
    case AlternativeC:
      prefix = NULL; 
      for ( n=NumArgB(b1),i=1; i<=n; i++ ){
        prefix = MakePrefix( LookArgB(b1,i), label, l );
	if ( prefix!=NULL )
	  break;
      }
      break;
      
      
      
    case ProcessInstC:
    case EnablingC:  
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case ProcessDefC:
    case SpecificationC:
    case GateChoiceC:
    case ParC:
    case BehaviourC:
    case InterleavedC:
    default:
      Error("MakePrefix : unexpected cell type");
      break;
      
    }
  if ( prefix!=NULL )
    *l = Insert_list( (DataListTyp)b1, *l );
  return prefix;
}




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

/* MergeB1Bc
 * returns the result of merging B1 with Bci, where IT( B1, Uc<c>Sumi gi;Bci )
 * assuming that <c> is offered by B1.
 *
 * Example :
 *
 * MergeB1Bc( choice x:s[](1(35)|||2[]B|||B2), (B3|||B4), <1(y:s),2>, &prefix )
 *         = (B3|||B4|||B2) , prefix = (choice x:s[] plet y:s=35 in)
 *
 * Non destructive function.
 */
BehTyp MergeB1Bc( b1, b2, label, opl, exiting )
     BehTyp   b1, b2;
     LabelTyp label;
     ListTyp  opl;
     boolean  exiting;
{
  int              n,i;
  BehTyp           rem,bi,rem1,rem1b,rem2,rem2b;
  boolean          go1,go2;
  /*
  LabelTyp         lab;
  BehTyp           plet;
  ExprListTyp      el,vl;
  VarAssignListTyp val;
  */
  
  /* the occurrence of a termination of label in an operand is denoted by
     a non-null prefix */
  
  
  switch ( LookTypeB(b2) )
    {
    case ContSetC:
      LASSERT(LookA(b2,ITCLA)==NULL);
      return CopyUntilActB(b1);
      /*
	 case TerminationC:
	 case StopC:
	 case ExitC:
	 case GateC:
	 case IC:
	 case GuardC:
	 case ChoiceC:
	 case AlternativeC:
	 case DisablingC:
	 return CopyUntilActB(b2);
	 */
      
    case ProcessInstC:
    case EnablingC:  
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case ProcessDefC:
    case SpecificationC:
    case GateChoiceC:
    case ParC:
    case BehaviourC:
    case InterleavedC:
      Error("MergeB1Bc : unexpected cell type");
      break;
    }
  
  rem = NULL;
  switch ( LookTypeB(b1) )
    {
      
    case TerminationC:
      if( LookForLabel( LookNameB(b1), label )!=NULL ){
	rem     = CopyUntilActB(b2);
	/*
	   el      = (ExprListTyp)LookAInfo(LookA(b1,ELA));
	   vl      = (ExprListTyp)LookAInfo(LookA(lab,ELA));
	   LASSERT(Length_list(el)==Length_list(vl));
	   if ( el!=NULL ){
	   el   = CopyEL(el); 
	   val  = Mk_VLEL_VAL( vl, el );
	   plet = MakeB( 0, PletC );
	   PutA(plet,MakeA((AttrValueTyp)val,VALA));
	   AddArgB(plet,rem);
	   rem = plet;
	   }
	   */
      }
      break;
      
    case StopC:
    case ExitC:
      break;
      
    case GateC:
    case IC:
      if ( HARD_EXIT ){
        rem = MergeB1Bc( LookArgB(b1,1), b2, label, opl, exiting );
      }
      break;
      
    case ChoiceC:
      if ( In_list( (DataListTyp)b1, opl, EqInt ) )
	rem = MergeB1Bc( LookArgB(b1,1), b2, label, opl, exiting );
      break;
      
    case GuardC:
      if ( In_list( (DataListTyp)b1, opl, EqInt ) ){
	rem = MergeB1Bc( LookArgB(b1,1), b2, label, opl, exiting );
      }
      break;
      
    case ParallelC:
      go1  = In_list( (DataListTyp)LookArgB(b1,1), opl, EqInt );
      go2  = In_list( (DataListTyp)LookArgB(b1,2), opl, EqInt );
      rem1 = rem2 = NULL;
      
      if ( go1 && go2 ){
	if ( exiting )
	  rem = CopyB(b2);
	else
	  if ( LookTypeB(b2)==ParallelC ){
	    rem1 = MergeB1Bc( LookArgB(b1,1), LookArgB(b2,1), label, opl, exiting );
	    rem2 = MergeB1Bc( LookArgB(b1,2), LookArgB(b2,2), label, opl, exiting );
	    rem     = CopyOperB( b1 );
	    (void)GetArgB(rem,1);
	    (void)GetArgB(rem,2);
	    AddArgB( rem, rem1 );
	    AddArgB( rem, rem2 );
	  }
	/*
	   else */ /* Iexp_Pre_Proc simplification */
      }
      else
	if ( go1 ){
	  rem1    = MergeB1Bc( LookArgB(b1,1), b2, label, opl, exiting );
	  rem     = CopyOperB( b1 );
	  (void)GetArgB(rem,1);
	  rem2b = GetArgB(rem,2);
	  PutArgB( rem, rem1, 1 );
	  PutArgB( rem, CopyUntilActB(rem2b), 2 );
	}
	else
	  if ( go2 ){
	    rem2    = MergeB1Bc( LookArgB(b1,2), b2, label, opl, exiting );
	    rem     = CopyOperB( b1 );
	    rem1b = GetArgB(rem,1);
	    (void)GetArgB(rem,2);
	    PutArgB( rem, CopyUntilActB(rem1b), 1 );
	    PutArgB( rem, rem2, 2 );
	  }
      break;
      
      
    case DisablingC:
      LASSERT( In_list( (DataListTyp)b1, opl, EqInt ) );
      go1  = In_list( (DataListTyp)LookArgB(b1,1), opl, EqInt );
      go2  = In_list( (DataListTyp)LookArgB(b1,2), opl, EqInt );
      rem1 = rem2 = NULL;
      if ( go1 ){
	rem1    = MergeB1Bc( LookArgB(b1,1), b2, label, opl, exiting );
	if ( exiting )
	  rem = rem1;
	else {
	  rem     = CopyOperB( b1 );
	  (void)GetArgB(rem,1);
	  rem2b = GetArgB(rem,2);
	  AddArgB( rem, rem1 );
	  AddArgB( rem, CopyUntilActB(rem2b) );
	}
      }
      else
	if ( go2 ){
	  rem    = MergeB1Bc( LookArgB(b1,2), b2, label, opl, exiting );
	}
      break;
      
      
      
    case AlternativeC:
      LASSERT( In_list( (DataListTyp)b1, opl, EqInt ) );
      for ( n=NumArgB(b1),i=1; i<=n; i++ ){
	bi = LookArgB(b1,i);
        if ( In_list( (DataListTyp)bi, opl, EqInt ) ){
          rem = MergeB1Bc( bi, b2, label, opl, exiting );
          break;
        }
      }
      if ( i>n )
	Error("MergeB1Bc : unexpected cell type");
      break;
      
      
      
    case ProcessInstC:
    case EnablingC:  
    case RelabellingC:
    case HidingC:
    case PletC:
    case LetC:
    case ProcessDefC:
    case SpecificationC:
    case GateChoiceC:
    case ParC:
    case BehaviourC:
    case InterleavedC:
    default:
      break;
      
    }
  if (rem==NULL)
    Error("MergeB1Bc : unexpected cell type");
  return rem;
}



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

/* ApplyITC
 * return the result of escaping from b1 through the continuation itc of IT
 */
static BehTyp ApplyITC( it, b1, itc, hard_prefix, actual_label )
     BehTyp     it, b1, *hard_prefix;
     LabelTyp  *actual_label;
     PITContTyp itc;
{
  BehTyp        itc_b,arg,gate,out,bi,itb,rem,prefix,term,next,bib;
  int           n,i;
  ListTyp       opl;
  
  out    = NULL;
  itc_b  = Iexp_Pre_Proc( CopyUntilActB(itc->b) );     /* instantiations */
  
  opl    = Create_list();
  prefix = MakePrefix( b1, itc->label, &opl );
  itc_b  = ConnectPrefix( prefix, itc_b, hard_prefix, &term ); 
  itc_b  = Iexp_Pre_Proc( itc_b );
  
  for ( n = NumArgIB(itc_b), i=1 ; i<=n ; i++ ) {
    arg  = LookArgIB(itc_b,i); 
    gate = LookActionUB(arg);
    LASSERT( LookTypeB(gate)==GateC || LookTypeB(gate)==IC ||
	    LookTypeB(gate)==ExitC ||
	    LookTypeB(gate)==StopC    /* only due to plet assignations */
	    ); 
    if ( LookTypeB(gate)==GateC || LookTypeB(gate)==IC ){
      /* instantiations */
      bib    = GetArgB(gate,1);
      bi     = Iexp_Pre_Proc( CopyUntilActB(bib) );
      FreeB(bib);
      rem    = MergeB1Bc( b1, bi, itc->label, opl,
			 (LookTypeB(gate)==IC && LookNameB(gate)==-1) );
      itb    = CopyOperB(it);
      (void)GetArgB( itb, 1 );
      PutArgB( itb, rem, 1 );
      PutArgB( gate, itb, 1 );
    }
    if ( LookTypeB(gate)!=StopC )
      out = AppendUB( out, arg );
  }
  
  *actual_label = (LabelTyp)NULL;
  for ( ; term!=NULL; term=next ){
    LASSERT(LookTypeB(term)==TerminationC);
    next = LookArgB(term,1);
    if ( next!=NULL )
      next = GetArgB(term,1);
    *actual_label = InsertLabel( term, *actual_label ); 
  }
  
  Disp_list(opl);
  return out;
}


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

/* IT_Processing
 * Extract the first actions that an IT can offer
 */
BehTyp IT_Processing( b )
     BehTyp b;
{
  BehTyp        b1,out, gate, bi, bb, arg, b1p, exits,hard_prefix;
  int           n,i,i_rm_depth,flagsbkup;
  StackTyp      aitc_stk;
  PITContTyp    aitc;
  LabelTyp      actual_label;
  
  b               = GetUntilActB(b);  /* to avoid SHARED_EXP effect */
  b1              = LookArgB( b, 1 ); 
  out             = NULL;
  i_rm_depth      = 0;
  b1              = Iexp_Pre_Proc( GetArgB(b,1) );
  PutArgB( b, b1, 1 );
  flagsbkup       = expansion_flags;
  expansion_flags = NOT_PRE_PROC_EXP;
  b1p             = Pre_Branch( b1, &i_rm_depth );
  expansion_flags = flagsbkup;
  n  = NumArgIB( b1p );
  for ( i=1 ; i<=n; i++ ) {
    arg  = CopyUntilActB( LookArgIB( b1p, i ) );
    gate = LookActionUB(arg);
    switch( LookTypeB(gate) )
      {
      case IC:
      case GateC:
        out = AppendUB ( out, arg );
        bi = GetArgB(gate,1);
        bb = CopyOperB(b);
        (void)GetArgB( bb, 1 ); 
        PutArgB( bb, bi, 1 );
        PutArgB( gate, bb, 1 );
        break;
	
      case ExitC:
        out = AppendUB ( out, arg );
        break;
	
      case TerminationC:
      case StopC:
        FreeB(arg);
        break;
	
      default:
        Error( "IT_Processing: unexpected cell type");
        break;
	
      }
  }
  FreeB(b1p);
  
  aitc_stk  = ApplicableConts( b, FALSE );
  while ( !IsEmpty_Stack(aitc_stk) ){
    aitc  = (PITContTyp) Get_Stack(&aitc_stk);
    exits = ApplyITC( b, b1, aitc, &hard_prefix, &actual_label );
    FreeLabel( actual_label );
    out   = AppendUB ( out, exits );
  }
  
  if ( out==NULL )
    out = MakeB( 0, StopC );
  
  FreeB( b ); 
  
  return out;
  
}



