/***********************************
  (C) Copyright 1992-1993; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************/

/***********************************
  
  Santiago Pavon Gomez
  David Larrabeti Lopez
  
  8 February 1991
  
  Pre_branch
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  (none)
  
  ************************************/


#include "limisc.h"
#include "lilists.h"
#include "badefca.h"
#include "babeh.h"
#include "balotosf.h"
#include "eximmed.h"
#include "expre_br.h"
#include "exsucces.h"
#include "exdiver.h"
#include "excomp.h"


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

/* InitEX
 * Initialization of the interface EXpansion
 */
void InitEX()
{
  InitVP();
}

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

/* expansion_flags
 *
 * These flags indicate the type of expansion to make.
 */
int expansion_flags = 0;

/******************************************************************
 *                                                                *
 *            i filtering-off according to                        *
 *            weak bisimulation equivalence                       *
 *                                                                *
 *******************************************************************/

static boolean CompareBehavior( b1, b2 )
     BehTyp b1,b2;
{
  boolean     equal;
  
  Init_VPTable();
  equal = Comp_Beh( b1, b2 );
  Init_VPTable();
  return equal;
}

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

static boolean IsRmvble_i_Branch( b )
     BehTyp b;
{
  
  if ( LookTypeB(b)==AlternativeC || LookTypeB(b)==ChoiceC )
    return FALSE;
  if ( LookTypeB(LookActionUB(b))==IC )
    return TRUE;
  return FALSE;
}

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

/* Filter_i
 * Transformation i;B = B
 * return the condition : extra processing is needed after filtering.
 */
boolean Filter_i( b, i_rm_depth )
     BehTyp b;
     int   *i_rm_depth;
{
  int     count, entry_rm_depth;
  BehTyp  curr, up;
  ListTyp behl;
  boolean res;

  LASSERT(*i_rm_depth>=0);
  
  if ( !IsRmvble_i_Branch(b) )
    return FALSE;
  res = LookTypeB(b)!=IC;  /* extra processing is needed after Filter_i */

  entry_rm_depth = *i_rm_depth;
  behl           = Create_list();
  for ( count = MAX_ICANCEL, up = curr = b ; count >0; count-- ) {
    behl = Insert_list( (DataListTyp)CopyUntilActB(up), behl );
    
    up   = LookActionUB(up);
    curr = GetArgB(up,1);
    if ( *i_rm_depth > 0 )
      (*i_rm_depth)--;
    curr = Pre_Branch( curr, i_rm_depth );
    AddArgB( up, curr );
    if ( IsRmvble_i_Branch(curr) ) {
      GlueB( up,curr);
      if ( In_list( (DataListTyp)up, behl, CompareBehavior ) ){  
	
	/* i-loop detected => =~= i;stop =~wbe~= stop */
	
	GlueB( b, MakeB(0,StopC) );
	Free_list( behl, FreeB );
	*i_rm_depth = entry_rm_depth;    /* restore i_rm_depth */
	return res;
      }
    }
    else {  /*  no more i transitions */
      GlueB( up, curr );
      break;
    }
  }
  
  Free_list( behl, FreeB );
  return res;
}

/******************************************************************
 *                                                                *
 *     Pre_Branch                                                 *
 *                                                                *
 *     Original function for one level expansion                  *
 *     The behaviour is unshared until actions and                *
 *     then transformed                                           *
 *                                                                *
 *******************************************************************/

/* Pre_Branch_Choice
 * Distribute a value choice into a behaviour choice
 * choice v:s [] ( B1[]B2 ) = (choice v:s [] B1) [] (choice v:s [] B2)
 */
BehTyp Pre_Branch_Choice( b )
     BehTyp b;
{
  BehTyp c, a, b1 ;
  int n, i;
  
  LASSERT(LookCopy(b)==0);
  a = GetArgB( b, 1 );
  LASSERT(LookCopy(a)==0 );
  switch ( LookTypeB(a) )
    {
    case AlternativeC:
      n = NumArgB( a );
      for ( i=1; i<=n; i++ ) {
	b1 = GetArgB( a, i );
	c = CopyB( b );
	AddArgB( c, b1 );
	PutArgB( a, c, i );
      }
      FreeB( b );
      return a;
      
    case ChoiceC:
    case GuardC:
    case IC:
    case GateC:
    case ExitC:
      PutArgB( b, a, 1 );
      return b;
      
    case StopC:
      FreeB( b );
      return a;
      
    default:
      Error("Pre_Branch_Choice: unexpected cell.");
    }
  return NULL;
}

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

/* Pre_Branch_Alt
 * Flatten a 2-level alternative tree.
 * b1 [] ( b2 [] b3) [] b4 = b1 [] b2 [] b3 [] b4
 */
BehTyp Pre_Branch_Alt( b )
     BehTyp b;
{
  BehTyp res,a,aa;
  int i,j,nb,na;
  
  LASSERT(OwnersB(b)==0);
  res = MakeB( 0, AlternativeC );
  nb  = NumArgB( b );
  for ( i=1; i<=nb; i++ ) {
    a = GetArgB( b, i );
    if ( LookTypeB(a)==AlternativeC ) {
      na = NumArgB( a );
      for ( j=1; j<=na; j++ ) {
	aa = LookArgB( a, j );
	AddArgB( res, aa );
      } 
      FreeB( a );  
    }
    else 
      AddArgB( res, a ); 
  }
  FreeB( b );
  return res;
}

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

/* Pre_Branch_Guard
 * Distribute a guard into a behaviour choice
 * [ BE ]-> ( B1[]B2 ) = ([ BE ]-> B1) [] ([ BE ]-> B2)
 */
BehTyp Pre_Branch_Guard( b )
     BehTyp b;
{
  BehTyp g, a, b1, b2;
  int n, i;
  
  LASSERT(LookCopy(b)==0);
  a = GetArgB( b, 1 );
  LASSERT(LookCopy(a)==0);
  switch ( LookTypeB(a) )
    {
    case AlternativeC:
      n = NumArgB( a );
      for ( i=1 ; i<=n ; i++ ) {
	b2 = LookArgB( a, i );
	if ( LookTypeB(b2)!=ChoiceC ) {
	  b2 = GetArgB( a, i );
	  g = CopyB( b );
	  AddArgB( g, b2 );
	  PutArgB( a, g, i );
	}
	else {
	  b1 = LookArgB( b2, 1 );
	  while ( LookTypeB(b1)==ChoiceC ) {
	    b2 = b1;
	    b1 = LookArgB( b2, 1 );
	  }
	  b1 = GetArgB( b2, 1 );
	  g  = CopyB( b );
	  AddArgB( g, b1 );
	  PutArgB( b2, g, 1 );
	}
      }
      FreeB( b );
      return a;
      
    case ChoiceC:
      b2 = a;
      b1 = LookArgB( b2, 1 );
      while ( LookTypeB(b1)==ChoiceC ) {
	b2 = b1;
	b1 = LookArgB( b2, 1 );
      }
      b1 = GetArgB( b2, 1 );
      AddArgB( b, b1 );
      PutArgB( b2, b, 1 );
      return a;
      
    case GuardC:
    case IC:
    case GateC:
    case ExitC:
      PutArgB( b, a, 1 );
      return b;
      
    case StopC:
      FreeB( b );
      return a;
      
    default :
      Error("Pre_Branch_Guard: unexpected cell.");
    }
  return NULL;
}

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

/* Pre_Branch_Stop
 * Transforms ...[]B1[]stop[]B2[]... into ...[]B1[]B2...
 */
BehTyp Pre_Branch_Stop( b )
     BehTyp b;
{
  int n,i;
  
  if ( LookTypeB(b) == AlternativeC ) {
    n = NumArgB( b );
    for ( i=1; i<=n; ) {
      if ( LookTypeB(b)==AlternativeC )
        if ( LookTypeB(LookActionUB(LookArgB(b,i)))==StopC ) {
          FreeArgB( b, i );
          n--;
        }       
        else
          i++;
      else
        i++;  
    }
  }
  return b;
}


/******************************************************************
 *                                                                *
 *     Pre_Processing                                             *
 *                                                                *
 *     Original function to pre_process operators not allowed     *
 *     in the guarded choice representation.                      *
 *     The behaviour is supposed to be unshared until actions.    *
 *                                                                *
 *******************************************************************/


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

/* CanGlueNextBeh
 * Returns:
 *   3 -> "b" offers any visible actions, so it can not be glued by its 
 *  .     father.
 *   2 -> "b" only offers internal actions preeceded by guards, so
 *        it can not be glued by its father.
 *   1 -> "b" only offers one internal action. It is glued by its father.
 *         Note that Filter_i has removed all the internal actions 
 *         (a sequence) until the maximum allowed depth. 
 *         then a i-loop can exist.
 *   0 -> "b" only offers several internal actions (or one internal
 *         action preceeded by a choice), so it can be glued by its father.
 */ 
static int CanGlueNextBeh(b)
     BehTyp b;
{
  int n,i,res;
  BehTyp b0,b1,b2;
  
  res = 2;
  n = NumArgIB(b);
  for (i=1 ; i<=n ; i++) {
    b0 = b1 = LookArgIB(b,i);
    while (LookTypeB(b1)==ChoiceC) b1 = LookArgB(b1,1); /* skip choices */
    b2 = b1;
    while (LookTypeB(b2)==GuardC) b2 = LookArgB(b2,1); /* skip guards */
    if (LookType(b2)!=IC) return 3; /* gate or exit is offered */
    if (b1==b2)  /* internal actions not preceeded by guard */
      if ((n==1)&&(b0==b1)) /* only one internal action */
	res =  1 ; 
      else 
	res = 0;
  }
  return res;
}

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

static boolean GlueInternalActionsAux(b,i_rm_depth)
     BehTyp b;
     int    *i_rm_depth;
{
  int n,i,irmdepthmin,i_rm_depth_2;
  BehTyp aux,b1;
  boolean res;
  
  n = NumArgIB(b);
  irmdepthmin = *i_rm_depth;
  res = TRUE;
  for (i=1 ; i<=n ; i++) {
    i_rm_depth_2 = *i_rm_depth - 1;
    aux = LookActionArgIB( b, i );
    PutArgB( aux, b1 = Pre_Branch(GetArgB(aux,1),&i_rm_depth_2), 1 );
    if (CanGlueNextBeh(b1) < 2) {
      GlueB(aux,b1);
      if ((i_rm_depth_2<1) || !GlueInternalActionsAux(aux,&i_rm_depth_2))
	res = FALSE;
    }
    else 
      i_rm_depth_2++;
    irmdepthmin = MIN(i_rm_depth_2,irmdepthmin);
  }
  *i_rm_depth = irmdepthmin;
  return res;
}


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

#define MAX_GIA 5

/* GlueInternalActions
 * The behaviour after the actions offered by the branch "branch" of "b"
 * (* LookArgB(b,branch) *) is expanded (only for testing); and if
 * it can be glued according to "CanGlueNextBeh" then it is glued.
 * This process ends when a visible action or a exit statement is offered,
 * or "i_rm_depth" reach the value zero.
 * Returns TRUE when i_rm_depth does not reach the value 0.
 */
static boolean GlueInternalActions(b,branch,i_rm_depth)
     BehTyp b;
     int    branch,*i_rm_depth;
{
  boolean res;
  int zero = 0;
  static int flag = 0; /* limits the recursion */
  BehTyp b1;
  
  if (IS_TEST_EQUIV_EXP) {
    if ((*i_rm_depth>0) && (flag < MAX_GIA)) {
      flag++;
      b1 = GetArgB(b,branch);
      if (CanGlueNextBeh(b1) < 2) {
	res = GlueInternalActionsAux(b1,i_rm_depth);
	b1 = Pre_Branch(b1,&zero);
      }
      else
	res = FALSE;
      PutArgB( b, b1 , branch);
      flag--;
      return res;
    }
  }
  return FALSE;
}

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

/* Pre_Processing
 * Pre_Processing of a non-immediate behaviour.
 * Returns a behaviour whose first operator is either
 * alternative, choice, guard, gate, i, stop or exit.
 */
BehTyp Pre_Processing( b, i_rm_depth )
     BehTyp b;
     int    *i_rm_depth;
{
  BehTyp b1,b1p,b2,b2p,out;
  int    i_rm_depth_2, cero=0;
  
  LASSERT ( OwnersB( b )>=0);
  LASSERT( (*i_rm_depth)>=0 );
  
  switch( LookTypeB(b) )
    {
    case HidingC:
      out = Hide_Expand( b, i_rm_depth );
      break;
      
    case RelabellingC:
      out = Relabel_Expand( b,i_rm_depth );
      break;
      
    case DisablingC:
      PutArgB( b, Pre_Branch(GetArgB(b,1),i_rm_depth), 1 );
      b2 = GetArgB(b,2);
      b2p = IS_NOT_PRE_PROC_EXP ? CopyUntilActB(b2) : NULL ;
      PutArgB( b, Pre_Branch(b2,&cero), 2 );
      out = Disabling_Expand( b, b2p );
      break;
      
    case EnablingC:
      PutArgB( b, Pre_Branch(GetArgB(b,1),i_rm_depth), 1 );
      out = Enabling_Expand( b );
      break;
      
    case ParallelC:{
      boolean res1,res2;
	
      i_rm_depth_2 = *i_rm_depth;
      b1  = GetArgB(b,1);
      b1p = IS_NOT_PRE_PROC_EXP ? CopyUntilActB(b1) : NULL ;
      if (IS_TEST_EQUIV_EXP) {
	ParUpdateSuccessStack(b);
	PutArgB( b, Pre_Branch(b1,&i_rm_depth_2), 1 );
	PopSuccessStack();
	}
      else
	PutArgB( b, Pre_Branch(b1,&i_rm_depth_2), 1 );
       res1 = GlueInternalActions(b,1,&i_rm_depth_2);
      
      b2 = GetArgB(b,2);
      b2p = IS_NOT_PRE_PROC_EXP ? CopyUntilActB(b2) : NULL ;
      if (IS_TEST_EQUIV_EXP) {
	ParUpdateSuccessStack(b);
	PutArgB( b, Pre_Branch(b2,i_rm_depth), 2 );
	PopSuccessStack();
      }
      else
	PutArgB( b, Pre_Branch(b2,i_rm_depth), 2 );
      res2 = GlueInternalActions(b,2,i_rm_depth);
      
      *i_rm_depth = MIN( *i_rm_depth, i_rm_depth_2 );
      if (IS_TEST_EQUIV_EXP && Par_to_Success(b)) { 
	out = b;
      }
      else { 
	out = Par_Expand( b , b1p, b2p, res1 , res2 );
      }
      break;
    }
      
    case ProcessInstC:
      out = Inst_Processing( b );
      break;
      
    case LetC:
      out = Let_Processing( b );
      break;
      
    case PletC:
      out = Plet_Processing( b );
      break;
      
    case GateChoiceC:
      out = Sum_Expr_Processing( b );
      break;
      
    case ParC:
      out = Par_Expr_Processing( b );
      break;
      
    case InterleavedC:
      out = IT_Processing( b );
      break;
      
    default:
      Error("Pre_Processing: Unexpected Cell Type");
      break;
    }
  
  LASSERT ( OwnersB( out )>=0);
  
  return out;
  
}

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

/* Pre_Branch
 * Transforms a behaviour b into a 1_immediate behaviour.
 * If *i_rm_depth > 0 then apply Weak Bisimulation Congruence.
 */
BehTyp Pre_Branch( b, i_rm_depth )
     BehTyp b;
     int    *i_rm_depth;
{
  boolean cont;
  int     i,n,cero=0;
  
  LASSERT(*i_rm_depth>=0);
  
  b = GetUntilActB( b );
  
  cont = TRUE;
  while (cont) {
    switch (LookTypeB(b)) 
      { 
      case ProcessInstC:
      case LetC:
      case PletC:
      case HidingC:
      case RelabellingC:
      case ParC:
      case GateChoiceC:
      case InterleavedC:
	b = Pre_Processing( b, i_rm_depth );
	break;
	
      case DisablingC:
      case ParallelC:
	b = Pre_Processing( b, i_rm_depth );
	b = Pre_Branch_Stop( b ); 
	if ( (*i_rm_depth)>0 )
	  cont = Filter_i( b, i_rm_depth );
	else
	  cont = FALSE;
	break;
	
      case EnablingC:
	b = Pre_Processing( b, i_rm_depth );
	if ( (*i_rm_depth)>0 )
	  cont = Filter_i( b, i_rm_depth );
	else
	  cont = FALSE;
	break;
	
      case GateC:
	SolvePredicateBeh( b );
	cont = FALSE;
	break;
	
      case IC:
	if ( (*i_rm_depth)>0 )
	  (void)Filter_i( b, i_rm_depth );
	cont = FALSE;
	break;
	
      case ExitC:
      case StopC: 
      case TerminationC:
	cont = FALSE;
	break;
	
      case ChoiceC:
	PutArgB( b, Pre_Branch(GetArgB(b,1),&cero), 1 );
	b = Pre_Branch_Choice( b );
	cont = FALSE;
	break;
	
      case AlternativeC:
	n = NumArgB( b );
	for ( i=1; i<=n; i++ ) 
	  PutArgB( b, Pre_Branch(GetArgB(b,i),&cero), i );
	b = Pre_Branch_Alt( b );
	b = Pre_Branch_Stop( b ); 
	if ( (*i_rm_depth)>0 )
	  cont = Filter_i( b, i_rm_depth );
	else
	  cont = FALSE;
	break;
	
      case GuardC:
	
	LASSERT(LookPredicate(b) == 'i' );
	
	if ( LookPredicate(b) != 'i' )
	  SolvePredicateBeh( b );
	else {
	  PutArgB( b, Pre_Branch(GetArgB(b,1),i_rm_depth), 1 );
	  b = Pre_Branch_Guard( b );
	  cont = FALSE;
	}
	break;
	
      default:           
	Error("Pre_Branch : unexpected cell.");
      }
  }
  return b;
}


/******************************************************************
 *                                                                *
 *     Pre_Branch_2                                               *
 *                                                                *
 *     Function for one level expansion IN SITU                   *
 *     The behaviour is pre_processed before unsharing, then      *
 *     is unshared until actions and finally gets transformed     *
 *                                                                *
 *******************************************************************/

/* Filter_i_2
 * Transformation i;B = B using Pre_Branch_2
 */
boolean Filter_i_2( b, i_rm_depth )
     BehTyp  b;
     int    *i_rm_depth;
{
  int     count, entry_rm_depth;
  BehTyp  curr,up;
  ListTyp behl;
  boolean res;
  
  if ( !IsRmvble_i_Branch(b) )
    return FALSE;
  res = LookTypeB(b)!=IC;  /* extra processing is needed after Filter_i_2 */

  entry_rm_depth = *i_rm_depth;
  behl = Create_list();
  for ( count = MAX_ICANCEL, up=curr = b ; count >0; count-- ) {
    behl = Insert_list( (DataListTyp)CopyB(up), behl );
    
    up   = LookActionUB(up);
    curr = LookArgB(up,1);
    if ( *i_rm_depth > 0 )
      (*i_rm_depth)--;
    Pre_Branch_2( curr, i_rm_depth );
    if ( IsRmvble_i_Branch(curr) ) {
      GlueB( up,curr);
      if ( In_list( (DataListTyp)up, behl, CompareBehavior ) ){
	
	/* i-loop detected =~= i;stop =~wbe~= stop */
	
	GlueB( b, MakeB(0,StopC) );
	Free_list( behl, FreeB );
	*i_rm_depth = entry_rm_depth;    /* restore i_rm_depth */
	return res;
      }
    }
    else {  /*  no more i transitions */
      GlueB( up,curr);
      break;
    }
  }
  
  Free_list( behl, FreeB );
  return res;
}

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

/* Pre_Branch_Choice_2
 * Distribute a value choice into a behaviour choice
 * choice v:s [] ( B1[]B2 ) = (choice v:s [] B1) [] (choice v:s [] B2)
 */
void Pre_Branch_Choice_2( b )
     BehTyp b;
{
  BehTyp c, a, b1 ;
  int n, i;
  
  a = GetArgB( b, 1 );
  switch ( LookTypeB(a) )
    {
    case AlternativeC:
      a = GetOperB(a);
      n = NumArgB( a );
      for ( i=1; i<=n; i++ ) {
	b1 = GetArgB( a, i );
	c = CopyB( b );
	AddArgB( c, b1 );
	PutArgB( a, c, i );
      }
      GlueB( b , a );
      return;
      
    case ChoiceC:
    case GuardC:
    case GateC:
    case IC:
    case ExitC:
      PutArgB( b, a, 1 );
      return ;
      
    case StopC:
      TrfStop( b );
      FreeB(a);
      return;
      
    default:
      Error("Pre_Branch_Choice_2: unexpected cell.");
    }
  return;
}

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

/* Pre_Branch_Alt_2
 * Flatten a 2-level alternative tree.
 * b1 [] ( b2 [] b3) [] b4 = b1 [] b2 [] b3 [] b4
 */
void Pre_Branch_Alt_2( b )
     BehTyp b;
{
  BehTyp res,a,aa;
  int i,j,nb,na;
  
  res = MakeB( 0, AlternativeC );
  nb  = NumArgB( b );
  for ( i=1; i<=nb; i++ ) {
    a = LookArgB( b, i );  /* i.o. GetArgB cause shared sub alts are allowed */
    if ( LookTypeB(a)==AlternativeC ) {
      na = NumArgB( a );
      for ( j=1; j<=na; j++ ) {
	aa = LookArgB( a, j );
	AddArgB( res, aa );
      } 
      /* FreeB( a );  same comment */
    }
    else 
      AddArgB( res, a ); 
  }
  GlueB(b,res);
  return;
}

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

/* Pre_Branch_Guard_2
 * Distribute a guard into a behaviour choice
 * [ BE ]-> ( B1[]B2 ) = ([ BE ]-> B1) [] ([ BE ]-> B2)
 */
void Pre_Branch_Guard_2( b )
     BehTyp b;
{
  BehTyp g, a, b1, b2;
  int n, i;
  
  a = GetArgB( b, 1 );
  switch ( LookTypeB(a) )
    {
    case AlternativeC:
      a = GetOperB( a );
      n = NumArgB( a );
      for ( i=1 ; i<=n ; i++ ) {
	b2 = LookArgB( a, i );
	if ( LookTypeB(b2)!=ChoiceC ) {
	  b2 = GetArgB( a, i );
	  g = CopyB( b );
	  AddArgB( g, b2 );
	  PutArgB( a, g, i );
	}
	else {
	  b1 = GetOperB( GetArgB(a,i) );
	  PutArgB( a, b1, i );
	  while ( LookTypeB(LookArgB(b1,1)) == ChoiceC ) {
	    b2 = GetOperB( GetArgB(b1,1) );
	    PutArgB( b1, b2, 1 );
	    b1 = b2;
	  }
	  b2 = GetArgB( b1, 1 );
	  g  = CopyB( b );
	  AddArgB( g, b2 );
	  PutArgB( b1, g, 1 );
	}
      }
      GlueB( b, a );
      break;
      
    case ChoiceC:
      a = GetOperB( a );
      b1 = a;
      while ( LookTypeB(LookArgB(b1,1))==ChoiceC ) {
	b2 = GetOperB(GetArgB(b1,1));
	PutArgB( b1, b2, 1 );
	b1 = b2;
      }
      b2 = GetArgB( b1, 1 );
      g = CopyB(b);
      AddArgB( b1, g );
      PutArgB( g, b2, 1 );
      GlueB( b, a );
      break;
      
    case GuardC:
    case GateC:
    case IC:
    case ExitC:
      PutArgB( b, a, 1 );
      break;
      
    case StopC:
      GlueB( b, a );
      break;
      
    default :
      Error("Pre_Branch_Guard_2: unexpected cell.");
    }
  
}

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

/* Pre_Branch_Stop_2
 * Transforms ...[]B1[]stop[]B2[]... into ...[]B1[]B2...
 */
void Pre_Branch_Stop_2( b )
     BehTyp b;
{
  int n,i;
  
  if ( LookTypeB(b) == AlternativeC ) {
    n = NumArgB( b );
    for ( i=1; i<=n; ) {
      if ( LookTypeB(b)==AlternativeC )
	if ( LookTypeB(LookActionUB(LookArgB(b,i)))==StopC ) {
	  FreeArgB( b, i );
	  n--;
	}       
	else
	  i++;
      else
	i++;  
    }
  }
}


/******************************************************************
 *                                                                *
 *     Pre_Processing_2                                           *
 *                                                                *
 *     Function to pre_process operators not allowed              *
 *     in the guarded choice representation.                      *
 *     The pre_processing of their operands (when necessary)      *
 *     is performed before unsharing until actions.               *
 *                                                                *
 *******************************************************************/

/* Pre_Processing_2
 * Pre_Processing of a non-immediate behaviour.
 * Returns a behaviour whose first operator is either
 * alternative, choice, guard, gate, i, stop or exit.
 */
void  Pre_Processing_2( b, i_rm_depth )
     BehTyp b;
     int    *i_rm_depth;
{
  BehTyp out, b1, b1p, b2, b2p, aux;
  int    i_rm_depth_2, cero=0;
  
  LASSERT ( OwnersB( b )>=0);
  
  switch( LookTypeB(b) )
    {
    case HidingC:
      b1 = CopyUntilActB(b);
      out = Hide_Expand( b1, i_rm_depth );
      break;
      
    case RelabellingC:
      b1 = CopyUntilActB(b);
      out = Relabel_Expand( b1, i_rm_depth );
      break;
      
    case DisablingC:
      b1 = LookArgB(b,1);
      Pre_Branch_2( b1, i_rm_depth );
      b2 = LookArgB(b,2);
      b2p = IS_NOT_PRE_PROC_EXP ? CopyUntilActB(b2) : NULL;
      Pre_Branch_2( b2, &cero );
      /**/ aux = GetArgB(b,2); /**/
      b1 = CopyUntilActB(b);
      /**/
      PutArgB(b,aux,2);
      PutArgB(b1,aux,2);
      /**/
      out = Disabling_Expand( b1, b2p );
      break;
      
    case EnablingC:
      Pre_Branch_2( b1=LookArgB(b,1), i_rm_depth );
      aux = GetArgB(b,2);
      b1 = CopyUntilActB(b);
      PutArgB(b,aux,2);
      PutArgB(b1,aux,2);
      out = Enabling_Expand( b1 );
      break;
      
    case ParallelC:
      i_rm_depth_2 = *i_rm_depth;
      b1 = LookArgB(b,1); 
      b1p = IS_NOT_PRE_PROC_EXP ? CopyUntilActB(b1) : NULL ;
      Pre_Branch_2( b1, &i_rm_depth_2 );
      b2 = LookArgB(b,2);
      b2p = IS_NOT_PRE_PROC_EXP ? CopyUntilActB(b2) : NULL ;
      Pre_Branch_2( b2, i_rm_depth );
      b1 = CopyUntilActB(b);
      out = Par_Expand( b1, b1p, b2p, FALSE, FALSE );
      *i_rm_depth = MIN( *i_rm_depth, i_rm_depth_2 );
      break;
      
    case ProcessInstC:
      b = ShareB(b);
      out = Inst_Processing( b );
      b = UnshareB(b);
      break;
      
    case LetC:
      
      
      /*    THIS COMMENT MUST NEVER BE REMOVED: Performance decreases a lot */
      /*      if ( LookCopy(LookArgB(b,1))>1 && ! UngProcBefAct(b)) {
	      Pre_Branch_2(b1=LookArgB(b,1),i_rm_depth);
	      }
	      */
      b1 = CopyUntilActB(b);
      out = Let_Processing( b1);
      break;
      
    case PletC:
      /*
	 
	 if (! UngProcBefAct(b))
	 Pre_Branch_2(LookArgB(b,1),????);  
	 */
      
      b = ShareB(b);
      out = Plet_Processing( b );
      b = UnshareB(b);
      break;
      
    case GateChoiceC:
      b = ShareB(b);
      out = Sum_Expr_Processing( b );
      b = UnshareB(b);
      break;
      
    case ParC:
      b = ShareB(b);
      out = Par_Expr_Processing( b );
      b = UnshareB(b);
      break;
      
    case InterleavedC:
      b = ShareB(b);
      out = IT_Processing( b );
      b = UnshareB(b);
      break;
      
    default:
      Error("Pre_Processing_2: Unexpected Cell Type");
      break;
    }
  
  LASSERT ( OwnersB( out )>=0);
  
  GlueB(b,out);
}

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

/* Pre_Branch_2
 * Transforms a behaviour b into a 1_immediate behaviour.
 * If *i_rm_depth > 0 then apply Weak Bisimulation Congruence.
 */
void Pre_Branch_2( b, i_rm_depth )
     BehTyp b;
     int    *i_rm_depth;
{
  boolean cont;
  int     i,n,cero=0;
  
  cont = TRUE;
  while (cont) {
    switch (LookTypeB(b)) 
      { 
      case ProcessInstC:
      case LetC:
      case PletC:
      case HidingC:
      case RelabellingC:
      case ParC:
      case GateChoiceC:
      case InterleavedC:
	Pre_Processing_2( b, i_rm_depth );
	break;
	
      case DisablingC:
      case ParallelC:
	Pre_Processing_2( b, i_rm_depth );
	Pre_Branch_Stop_2( b ); 
	if ( (*i_rm_depth)>0 )
	  cont = Filter_i_2( b, i_rm_depth );
	else
	  cont = FALSE;
	break;
	
      case EnablingC:
	Pre_Processing_2( b, i_rm_depth );
	if ( (*i_rm_depth)>0 )
	  cont = Filter_i_2( b, i_rm_depth );
	else
	  cont = FALSE;
	break;
	
      case GateC:
	SolvePredicateBeh( b );
	cont = FALSE;
	break;
	
      case IC:
	if ( (*i_rm_depth)>0 )
	  (void)Filter_i_2( b, i_rm_depth );
	cont = FALSE;
	break;
	
      case ExitC:
      case StopC: 
      case TerminationC:
	cont = FALSE;
	break;
	
      case ChoiceC:
        Pre_Branch_2( LookArgB(b,1), &cero);
	Pre_Branch_Choice_2( b );
	cont = FALSE;
	break;
	
      case AlternativeC:
	n = NumArgB( b );
	for ( i=1; i<=n; i++ ) 
	  Pre_Branch_2( LookArgB(b,i), &cero);
	Pre_Branch_Alt_2( b );
	Pre_Branch_Stop_2( b ); 
	if ( (*i_rm_depth)>0 )
	  cont = Filter_i_2( b, i_rm_depth );
	else
	  cont = FALSE;
	break;
	
      case GuardC:
	if ( LookPredicate(b) != 'i' )
	  SolvePredicateBeh( b );
	else {
	  Pre_Branch_2( LookArgB(b,1), i_rm_depth );
	  Pre_Branch_Guard_2( b );
	  cont = FALSE;
	}
	break;
	
      default:           
	Error("Pre_Branch_2 : unexpected cell.");
      }
  }
  
}

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

