/*
 * CMatrix es asimetrico :
 *  si g1 es de entrelazamiento local o global => cs2p a su derecha
 *  si g2 es de entrelazamiento solo local     => cs1p a su izquierda
 *
 * Se consideran las pendientes a efectos de deteccion de contenidas
 */
/***********************************
  (C) Copyright 1990, 1991; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************
  $Log:  ITintexp.c,v $
  * Revision 1.3  92/05/20  15:36:46  lotos
  * date type included
  *
  * Revision 1.2  92/01/15  11:20:13  lotos
  * bug fixed: flag indicating initial termination
  *
  * Revision 1.1  92/01/14  13:07:14  lotos
  * Initial revision
  *
  ***********************************/

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

/***********************************

  Santiago Pavon Gomez
  David Larrabeiti Lopez

  Dec 18, 1992

  Optimized Interleaved Expansion.

  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:

  BEHASHDBG : trace stored behaviours
  IEXPDBG   : trace exploration in iexpansion

  ************************************/

/* LINTLIBRARY */


#include "itintexp.h"
#include "basynset.h"
#include "limisc.h"
#include "baattr.h"
#include "baprint.h"
#include "batables.h"
#include "balotosf.h"
#include "badefca.h"
#include "basust_v.h"
#include "expre_br.h"
#include "eximmed.h"
#include "exsynchr.h"
#include "exdupbeh.h"
#include "expostex.h"
#include "exexpans.h"

#define IEXP_BHT_SIZE 3072

static BehTyp  Cn();
static BehTyp  InsTC();
static BehTyp  CMatrix();
static BehTyp  Iexp();

/******************************************************************
 *                                                                *
 *     Verbose Mode Printing functions and variables              *
 *                                                                *
 *******************************************************************/

/* depth level */
#define DATLIN     5

/* prints depth every DELTADEPTH actions */
#define DELTADEPTH 20

static boolean verbose_mode;
static char    buff[50];
static int     contdepth, contactdepth, max_depth;
static int     num_trans, num_m_states;

static void Header()
{
  if (verbose_mode)
    printMsgs("                  Exploration Tree                           \n");
}

static void Leaf( depth )
     int depth;
{
  if (verbose_mode) {
    if (contdepth==DATLIN) {
      (void)sprintf(buff,"-%5d/ \n",depth,num_trans,num_m_states);
      if (runtimeConfig==TextMode) {
	printMsgs(buff);
      }
      else {
	printPos(buff,-1);
	flushTarget();
      }
      contdepth = 1;
    }
    else {
      (void)sprintf(buff,"-%5d/",depth);
      if (runtimeConfig==TextMode) {
	printMsgs(buff);
      }
      else {
	printPos(buff,-1);
	flushTarget();
      }
      contdepth++;
    }
    contactdepth = 1;
  }
}

static void Branch( depth )
     int depth;
{
  if (verbose_mode) {
    (void)sprintf(buff,"%5d", depth );
    if (runtimeConfig==TextMode) {
      printMsgs(buff);
    }
    else {
      printPos(buff,-1);
      flushTarget();
    }
  }
}


static void Digging( depth )
     int depth;
{
  if (verbose_mode)
    if ( contactdepth == DELTADEPTH ) {
      contactdepth = 1;
      if (runtimeConfig==TextMode) {
	(void)sprintf(buff,"(%7d)\b\b\b\b\b\b\b\b\b",depth);
	printMsgs(buff);
      }
      else {
	(void)sprintf(buff,"(%7d)",depth);
	printPos("",printPos(buff,-1)-9);
	flushTarget();
      }
    }
    else
      contactdepth = contactdepth + 1;
}


/******************************************************************
 *                                                                *
 *     Duplicate Behaviour Detection Aux. vars & functions        *
 *                                                                *
 *******************************************************************/

static boolean       plain_dbd, param_dbd;
static BehHashTabTyp sbhtd;              /* external beh hash table */
static ITContListTyp iexpanded, pending;

/*
 * While i-expanding a continuation <c>Bc , if there is a continuation with
 * the same label <c>Bc' already iexpanded ( their csets are different )
 * there is no need to generate duplicated process definitions since <c>Bc
 * will be discarded at the end.
 */
static boolean generate_dupproc;


/* KJT 22/01/23: added "int" type */
static  int InitIexpFlags( dup, param )
     boolean dup, param;
{
  param_dbd        = param;
  plain_dbd        = dup;
  if ( param ){
    expansion_flags = DUPLICATE_EXP | PARAMETERIZED_EXP;
  }
  else
    if ( dup ){
      expansion_flags = DUPLICATE_EXP;
    }
    else
      expansion_flags = 0;
  generate_dupproc = IS_DUPLICATE_EXP;
}


/* iexp_link_beh
 */
static void iexp_link_beh( here, eq_here, pdbl, cs, gsap )
     BehTyp           here, eq_here, *cs;
     PDupBehListsTyp  pdbl;
     PSyncGateSetTyp  gsap;
{
  BehTyp        inst2, def, beh, inst1, it;
  DescriptorTyp name;
  GateSetTyp    gs;
  GateListTyp   gl;
  PAttrTyp      gla;

  it  = LookArgB( eq_here, 1 );
  *cs = CopyUntilActB( LookArgB( it, 2 ) );/**/
  beh = LookArgB( it, 1 );

  /* iexpanding a duplicated continuation */

  if ( !generate_dupproc ){
    GlueB( here, CopyB(beh) );
    /* the cset is shared */
    return;
  }

  if ( LookTypeB(beh) == ContSetC ){
    ToMake("contset");
  }

  /*
   *   Avoid processes with a termination for behaviour
   *
   *   NOT IMPLEMENTED. PROBLEMS with free variables.
   *   IT IS VERY TRICKY : see abracadabra protocol i -p and doc's
   *
   */
  /*
     if ( LookTypeB(beh) == TerminationC ){
     .....
     }
     */

  if ( LookTypeB(beh) != ProcessInstC ) {
    name  = Declare_proc( NameDupProc(), (BehTyp)NULL, NOTCALCULATEDF );
    inst1 = MakeB( name, ProcessInstC );
    def   = MakeB( name, ProcessDefC );
    PutP_def( name, def );
    PutArgB( inst1, def, 1 );
    /* PutArgB( def, CopyUntilActB(beh), 1 ); */
    PutArgB( def, CopyOperB(beh), 1 ); /**/
    gs = GetGates( LookArgB(eq_here,2) );
    if ( !IsEmptyGS(gs) ) {
      gl  = GateSet_to_GateList( gs );
      gla = MakeA( (AttrValueTyp)gl, GLA );
      PutA( inst1, gla );
      PutA( def, gla );
    }
    FreeGS( gs );
    if ( pdbl->DupBehForVL != NULL ) {
      PutA( def, MakeA( (AttrValueTyp)(pdbl->DupBehForVL),ELA) );
      PutA( inst1, MakeA( (AttrValueTyp)(pdbl->DupBehActEL2),ELA) );
    }
  }
  else {
    inst1 = beh;
    name  = LookNameB( inst1 );
    FreeEL( pdbl->DupBehForVL );
    FreeEL( pdbl->DupBehActEL2 );
  }
  GlueB( beh, inst1 );
  inst2 = MakeB( name, ProcessInstC );
  GlueB( here, inst2 );
  gla = LookA( beh, GLA );
  if ( gla!=NULL )
    PutA( here, gla );
  if ( pdbl->DupBehForVL != NULL )
    PutA( here, MakeA( (AttrValueTyp)(pdbl->DupBehActEL1), ELA ) );
}



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

static DescriptorTyp successEvent=0;

/* IsSuccessfulState
 * Determines whether the success event is offered at the LOTOS behaviour b
 * This is a condition for the interleaved expansion to stop.
 */
static boolean IsSuccessfulState( b )
     BehTyp b;
{
  int n,i;

  while ( b!=NULL )
    switch( LookTypeB(b) )
      {
      case GateC:
	return LookNameB(b)==successEvent;

      case IC:
	b = NULL;
	break;

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

      default:
	for ( n=NumArgB(b), i=2; i<=n; i++ ) {
	  if ( IsSuccessfulState( LookArgB(b,i) ) )
	    return TRUE;
	}
	b = LookArgB(b,1);
	break;
      }
  return FALSE;
}



/******************************************************************
 *                                                                *
 *              Continuation sets operations                      *
 *                                                                *
 *******************************************************************/


/* JoinContSets
 * Collapse two csets into one.
 * cs1 and cs2 may have duplicate continuations with dbd
 * ( example : a;b;stop [] c;b;stop |[b]| ... => {<1>b;stop U <1>b;stop} )
 */
static BehTyp JoinContSets( cs1, cs2 )
     BehTyp cs1,cs2;
{
  ITContListTyp cs1cs,cs2cs,aux,l,eitcn;
  PAttrTyp      itcla;
  PITContTyp    itc,itc2;
  ListTyp       csl1,csl2;

  LASSERT(LookTypeB(cs1)==ContSetC&&LookTypeB(cs2)==ContSetC);

  /*
     PrintBeh(cs1,1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
     printf("------ U -----\n");
     PrintBeh(cs2,1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
     */

  if ( LookA(cs2,ITCLA)!=NULL ){
    UnshareA(cs2,ITCLA);
    itcla = LookA(cs2,ITCLA);
    cs2cs = (ITContListTyp)GetAInfo(itcla);
  }
  else {
    FreeB(cs2);
    return cs1;
  }


  if ( LookA(cs1,ITCLA)!=NULL ){
    UnshareA(cs1,ITCLA);
    itcla = LookA(cs1,ITCLA);
    cs1cs = (ITContListTyp)GetAInfo(itcla);
  }
  else {
    PutAInfo( itcla, (AttrValueTyp)cs2cs );
    FreeB(cs1);
    return cs2;
  }

  FreeB(cs2);

  for ( aux = Create_list(), l = cs1cs; l!=NULL; l=Next_list(l) ){
    itc    = (PITContTyp)GetInfo_list(l);
    eitcn  = cs2cs;
    while ( (eitcn=LookForNodeITCL( eitcn, itc->label ))!=NULL )
      {
	itc2 = (PITContTyp)LookInfo_list(eitcn);
	/* solve duplication */
	csl1 = csl2 = NULL;
	if ( itc->cset_labels==NULL ){
	  csl1 = CSets_Labels_in_Beh( itc->b );
	  Apply_Func_list( csl1, (DataListTyp(*)())ShareB );
	  if ( csl1!=NULL )
	    itc->cset_labels = Insert_list( (DataListTyp)csl1, itc->cset_labels );
	}
	else
	  csl1 = (ListTyp)LookInfo_list(itc->cset_labels);
	if ( itc2->cset_labels==NULL ){
	  csl2 = CSets_Labels_in_Beh( itc2->b );
	  Apply_Func_list( csl2, (DataListTyp(*)())ShareB );
	  if ( csl2!=NULL )
	    itc2->cset_labels = Insert_list( (DataListTyp)csl2, itc2->cset_labels );
	}
	else
	  csl2 = (ListTyp)LookInfo_list(itc2->cset_labels);
	/*
	   PrintLabel( itc->label, printTarget );
	   (void)printf(" : ");
	   Print_LL( printTarget,  (ListTyp)LookInfo_list(itc->cset_labels) );
	   (void)printf("\nU\n");
	   PrintLabel( itc2->label, printTarget );
	   (void)printf(" : ");
	   Print_LL( printTarget,  (ListTyp)LookInfo_list(itc2->cset_labels) );
	   (void)printf("\n=\n");
	   */
	if ( SubSet_LL( csl1, csl2 ) ){
	  /* 1 in 2 */
	  /*
	     (void)printf(" collide \n");
	     PrintLabel( itc2->label, printTarget );
	     (void)printf(" : ");
	     Print_LL( printTarget,  (ListTyp)LookInfo_list(itc2->cset_labels) );
	     (void)printf("\n");
	     PrintBeh(itc->b,-1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
	     (void)printf("-------1 up 2 down ------------\n");
	     PrintBeh(itc2->b,-1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
	     */
	  FreeITC(itc);
	  break; /* while */
	}
	else
	  if ( SubSet_LL( csl2, csl1 ) ){
	    /* 2 in 1 */
	    /*
	       (void)printf(" collide \n");
	       PrintLabel( itc->label, printTarget );
	       (void)printf(" : ");
	       Print_LL( printTarget,  (ListTyp)LookInfo_list(itc->cset_labels) );
	       (void)printf("\n");
	       PrintBeh(itc->b,-1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
	       (void)printf("-------1 up 2 down ------------\n");
	       PrintBeh(itc2->b,-1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
	       */
	    FreeITC((PITContTyp)GetInfo_list(eitcn));
	    cs2cs = DeleteNode_list( eitcn, cs2cs );
	    aux   = Insert_list( (DataListTyp)itc, aux );
	    break; /* while */
	  }
	eitcn = Next_list(eitcn);
      }
    if ( eitcn==NULL ){
      aux = Insert_list( (DataListTyp)itc, aux );
      /*        (void)printf("the same\n"); */
    }


  }
  Disp_list(cs1cs);

  cs1cs = Join_list( aux, cs2cs );
  LASSERT( cs1cs!=NULL );
  PutAInfo( itcla, (AttrValueTyp)cs1cs );
  /*
     printf("------ =  -----\n");
     PrintBeh(cs1,1,NO_PROC,FALSE,"",printTarget,TRUE,FALSE);
     printf("------ end  -----\n");
     */
  return cs1;

}


/******************************************************************
 *                                                                *
 *              Cn                                                *
 *                                                                *
 *******************************************************************/

static BehTyp Cn( A, b )
     PSyncGateSetTyp A;
     BehTyp          b;
{
  int    i,n;
  BehTyp res,bi,choice,guard;

  switch( LookTypeB(b) )
    {
    case StopC:
      res = MakeB( 0, StopC );
      break;

    case ChoiceC:
      bi     = Cn( A, LookArgB(b,1) );
      choice = CopyOperB(b);
      (void)GetArgB(choice,1);
      AddArgB(choice,bi);
      res = Distribute_Choice( choice );
      break;

    case GuardC:
      bi    = Cn( A, LookArgB(b,1) );
      guard = CopyOperB(b);
      (void)GetArgB(guard,1);
      AddArgB(guard,bi);
      res = Distribute_Guard( guard );
      break;

    case IC:
    case ExitC:
    case GateC:
      if ( GateInSS(b,A) ){
	res = CopyUntilActB(b);
      }
      else {
	res = MakeB( 0, StopC );
      }
      break;

    case AlternativeC:
      res = NULL;
      for ( n=NumArgB(b), i=1; i<=n; i++ ) {
	res = AppendUB( res, Cn(A,LookArgB(b,i)) );
      }
      res = Pre_Branch_Stop(Pre_Branch_Alt(res));
      break;


    case EnablingC:
    case RelabellingC:
    case HidingC:
    case DisablingC:
    case ParallelC:
      res = MakeB( 0, StopC );
      break;

      /* necessary cause InsTC(cs) calls Cn to know
	 if a termination must be inserted */

    case ContSetC:
      res = MakeB( 0, StopC );
      break;

    default:
      Error("Cn: unexpected cell type");
    }

  return res;
}


/* SplitGC
 * Take as input a guarded choice and make a copy until acts of the
 * synchronization actions and interleaving actions separately.
 * return the synchronization part.
 */
static BehTyp SplitGC( A, b, int_part )
     PSyncGateSetTyp A;
     BehTyp          b, *int_part;
{
  BehTyp sync_part;
  int    n,i;

  sync_part = *int_part = NULL;
  for ( n=NumArgIB(b), i=1; i<=n; i++ ) {
    if ( GateInSS( LookActionArgIB(b,i), A ) )
      sync_part = AppendUB( sync_part, CopyUntilActB(LookArgIB(b,i)) );
    else
      *int_part = AppendUB( *int_part, CopyUntilActB(LookArgIB(b,i)) );
  }
  return sync_part;
}

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

/* Look_IexpPreProc_Token
 * First occurrence of either of the following operators found in a UB :
 *  gate | i | stop | exit | termination | [> | >> | |A| | hide | relabelling
 */
static BehTyp Look_IexpPreProc_Token( b )
     BehTyp b;
{

  LASSERT( b!=NULL );
  for (;;) {
    switch(LookTypeB(b))
      {
      case GateC:
      case StopC:
      case ExitC:
      case IC:

      case EnablingC:      /* note : on behalf of Iexp .... */
      case DisablingC:
      case HidingC:
      case RelabellingC:
      case ProcessInstC:
      case ParallelC:
      case TerminationC:
	return b;
      default:
	b = LookArgB( b, 1 );
	LASSERT(b!=NULL);
      }
  }
}


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

/* number of nodes analysed */

/* KJT 22/01/23: added "int" type */
static int num_states = 0;

/* InsTC
 * Apply Iexp and insert termination if needed.
 * Duplicate Behaviour Detection generation ( when IS_DUPLICATE_EXP ).
 * dupf disables duplicate behaviour detection in the first state.
 */
static BehTyp InsTC( gsap, rfl, b, cs, bhtd, dupf )
     PSyncGateSetTyp  gsap;
     RelabFuncListTyp rfl;
     BehTyp           b, *cs;
     BehHashTabTyp    bhtd;
     boolean          dupf;
{
  BehTyp         pp_b,iz,izres,cont,cn,wia,dupb,it,stop,cset,termination;
  int            term;
  PITContTyp     itc;
  ITContListTyp  itcl;
  DupBehListsTyp dbl;
  ExprListTyp    vl;

  pp_b  =  Iexp_Pre_Proc ( GetUntilActB(b) );

  /* Begin Duplicate Behaviour Detection ------------ */

  wia = NULL;
  if (     !dupf && IS_DUPLICATE_EXP /* ( plain_dbd || param_dbd ) */ &&
      LookTypeB(pp_b)!=StopC /* WRONG v1.lot  && LookTypeB(pp_b)!=ExitC */
      && LookTypeB(pp_b)!=ContSetC  ){

    wia = MakeB(0,BehaviourC);
    PutArgB( wia, CopyUntilActB(pp_b), 2 );/**/

    dupb = GetHashBehDef( bhtd, wia, &dbl );
    if ( dupb!=NULL ) {
#ifdef BEHASHDBG
      (void)printf("\n--------- duplicated state %d -------- node # %d \n",
		   LookNameB(wia), num_states );
      printMsgs("\n list 1: \n\n");
      DrawEL(dbl.DupBehActEL1,printMsgs);

      printMsgs("\n list 2: \n\n");
      DrawEL(dbl.DupBehActEL2,printMsgs);
      PBeh( LookArgB(wia,2) );
#endif
      iexp_link_beh( wia, dupb, &dbl, cs, gsap );
      FreeB(pp_b);
      return wia;
    }
    else {
#ifdef BEHASHDBG
      (void)printf("\n--------- new state %d -------- node # %d \n",
		   LookNameB(wia), num_states );
      PBeh( LookArgB(wia,2) );
#endif
      num_states++;
      it = MakeB( 0, InterleavedC ); /* auxiliary */
      PutArgB( it, stop=MakeB(0,StopC), 1 );
      PutArgB( it, cset=MakeB(0,ContSetC), 2 );
      PutArgB( wia, it, 1 );
    }
  }

  /* End Duplicate Behaviour Detection ------------------ */

  izres   = NULL;
  cont    = MakeB(0,ContSetC);

  cn    = Cn( gsap, pp_b );

  /*
   * if ( IsT( gsap, pp_b ) )
   *
   */
  if ( LookTypeB(cn)!=StopC ){
    term        = NewTerm();
    termination = MakeB( term, TerminationC );
    izres       = termination;
    vl          = GetFreeVarsBehSV( cn );
    if ( vl!=NULL )
      PutA( termination, MakeA((AttrValueTyp)vl,ELA) );
    itc        = NewITC();
    itc->label = ShareB(InsertLabel( CopyB(termination),
				    (LabelTyp)NULL )
			);
    itc->b     = ShareB( cn );
    itcl       = Insert_list( (DataListTyp)itc, Create_list() );
    PutA( cont, MakeA((AttrValueTyp)itcl,ITCLA) );
  }
  else
    FreeB( cn );


  iz  = Iexp( gsap, rfl, pp_b, cs, bhtd );


  izres = AppendUB( izres, iz );
  izres = Pre_Branch_Stop( izres );
  *cs   = JoinContSets( *cs, cont );

  if ( wia!=NULL ){ /* dbd */

    if ( LookTypeB(stop)==ProcessInstC ){
      iz = LookArgB( LookArgB(stop,1), 1 ); /* Fetch the definition */
    }
    else
      iz = stop;
    GlueB( iz, izres );
    izres = stop;

    GlueB( cset, /**/ CopyUntilActB /**/ (*cs) ); /* se pierde *cs */

  }

  return izres;
}



/******************************************************************
 *                                                                *
 *              CMat                                              *
 *                                                                *
 *******************************************************************/


/* ResolveVarCollisions
 * Redefine duplicated free variables in csets.
 * Example :  ResolveVarCollisions( <1(x),2(z,t)>, <3(z)> ) =>
 *                                  <1(x),2(z,t)>, <3(z')>
 */
static void ResolveVarCollisions( cs1, cs2 )
     BehTyp cs1, cs2;
{
  ExprListTyp      vl;         /* cs1 var list */
  ExprListTyp      vl2;        /* vl of each termination */
  ListTyp          cvl,cvlh;   /* collision var list */
  ITContListTyp    itcl;
  PITContTyp       pit;
  LabelTyp         lab;
  SVdescriptorTyp  td;
  DescriptorTyp    name;
  ExprTyp          var,nv;
  BehTyp           itc_b;

  vl  = Create_list();
  itcl = (ITContListTyp)LookAInfo(LookA(cs1,ITCLA));
  for ( ; itcl!=NULL; itcl = Next_list(itcl) ) {
    pit = (PITContTyp)LookInfo_list(itcl);
    for ( lab = pit->label; lab!=NULL; lab = LookArgB(lab,1) ){
      vl2 = (ExprListTyp)LookAInfo(LookA(lab,ELA));
      for ( ; vl2!=NULL; vl2 = Next_list(vl2) )
	vl = InsertEL((ExprTyp)LookInfo_list(vl2),vl);
    }
  }
  UnshareA( cs2, ITCLA );
  itcl = (ITContListTyp)LookAInfo(LookA(cs2,ITCLA));
  for ( ; itcl!=NULL; itcl = Next_list(itcl) ) {
    cvl  = Create_list();
    pit = (PITContTyp)LookInfo_list(itcl);
    for ( lab = pit->label; lab!=NULL; lab = LookArgB(lab,1) ){
      vl2 = (ExprListTyp)LookAInfo(LookA(lab,ELA));
      for ( ; vl2!=NULL; vl2 = Next_list(vl2) ){
	if ( InEL((ExprTyp)LookInfo_list(vl2),vl) )
	  cvl = InsertEL((ExprTyp)LookInfo_list(vl2),cvl);
      }
    }
    if ( cvl!=NULL){
      td   = CreateSV();
      for ( cvlh=cvl; cvl!=NULL; cvl=Next_list(cvl) ){
	var  = (ExprTyp)LookInfo_list(cvl);
	name = LookNameE(var);
	nv   = CopyE( var );             /* including parameterized value */
	ChangeNameE( nv, EqualV_entry(name) );
	InsertSV( name, nv, &td );
      }
      for ( lab = pit->label; lab!=NULL; lab = LookArgB(lab,1) )
	SubstBehSV( lab, &td );
      itc_b = CopyB(pit->b);    /* SubstBehSV affects the whole behavior  */
      SubstBehSV( itc_b, &td ); /* CopyB until plet would be enough       */
      FreeB(UnshareB(pit->b));
      pit->b = ShareB(itc_b);
      FreeSV( &td );
      FreeEL(cvlh);
    }
  }
  FreeEL(vl);
}

/* FilterSync
 * Take in a cset and make its continuation w.r.t. gsa.
 */
static BehTyp FilterSync( cs, gsa )
     BehTyp          cs;
     PSyncGateSetTyp gsa;
{
  ITContListTyp itclres,itcl;
  PITContTyp    itc;
  BehTyp        res,contres;

  itcl = (ITContListTyp)LookAInfo(LookA(cs,ITCLA));

  itclres = Create_list();
  for ( ; itcl!=NULL; itcl=Next_list(itcl) ){
    itc = (PITContTyp)LookInfo_list(itcl);
    contres = Cn( gsa, itc->b );

    /*
       contres = NULL;
       for ( n=NumArgIB(itc->b); i<=n; i++ ) {
       if ( GateInSS( gsa, LookActionArgIB(itc->b,i) ) )
       contres = AppendUB( contres, CopyUntilActB(LookArgIB(itc->b,i)) );
       }

       if ( contres!=NULL )
       */
    if ( LookTypeB(contres)!=StopC )
      itclres = InsertITCL( itclres,
			   CopyLabel(LookLabelITC(itc)), contres, itc->n_label );
    else
      FreeB( contres );
  }
  res   = MakeB( 0, ContSetC );
  if ( itclres!=NULL )
    PutA( res, MakeA((AttrValueTyp)itclres,ITCLA) );

  return res;
}

static boolean PureInt( gsap, b )
     PSyncGateSetTyp gsap;
     BehTyp b;
{
  int n;

  for ( n=NumArgIB(b); n>0; n-- ) {
    if ( GateInSS( LookActionArgIB(b,n), gsap ) )
      break;
  }
  return n==0;
}


/*
 * clean sync_b part in an itcl.
 * if hard clean then free the int_b part too.
 */
static void CleanAuxInfo( itcl1, hard )
     ITContListTyp itcl1;
     boolean       hard;
{
  PITContTyp      itc1;

  for ( ; itcl1!=NULL; itcl1= Next_list(itcl1) ) {
    itc1 = (PITContTyp)LookInfo_list(itcl1);
    if ( itc1->sync_b!=NULL )
      FreeB(itc1->sync_b);
    itc1->sync_b = NULL;
    if ( hard && itc1->int_b!=NULL )
      FreeB(itc1->int_b);
    itc1->int_b  = NULL;
  }
}


/* CMatrix
 * b is the parallel and cs1 and cs2 are its operands
 * A' = A' U A
 */
static BehTyp CMatrix( b, cs1, cs2, gsap )
     BehTyp          b, cs1, cs2;
     PSyncGateSetTyp gsap;
{
  PSyncGateSetTyp gsa;
  ITContListTyp   itcl,itcl1,itcl2,itcl1h,itcl2h;
  BehTyp          gate,b1_int,b2_int,b1_sync,b2_sync,par,
  bc_sync,res,cs1p,cs2p,bi;
  PITContTyp      itc1,itc2,itc,nitc1,nitc2;
  LabelTyp        label1,label2,newlabel;
  int             i,n;
  boolean         firstTime,balloon1,balloon2;

  res    = MakeB( 0, ContSetC );
  itcl1h = itcl1 = (ITContListTyp)LookAInfo(LookA(cs1,ITCLA));
  itcl2h = itcl2 = (ITContListTyp)LookAInfo(LookA(cs2,ITCLA));

  if ( itcl1 == NULL && itcl2 == NULL ) {
    return res;
  }

  itcl   = Create_list();

  cs1p  = FilterSync( cs1, gsap );
  cs2p  = FilterSync( cs2, gsap );

  /* Prepare Aux. info */

  gsa    = Parallel_to_SS( b );
  balloon1 = itcl1!=NULL;
  balloon2 = FALSE;
  for ( itcl1=itcl1h; itcl1!=NULL; itcl1= Next_list(itcl1) ) {
    itc1 = (PITContTyp)LookInfo_list(itcl1);
    itc1->sync_b = SplitGC( gsa, itc1->b, &(itc1->int_b) );
    balloon1 = balloon1 && itc1->sync_b==NULL && ( itc1->int_b!=NULL ) &&
      PureInt( gsap, itc1->int_b );
  }
  if ( !balloon1 ){
    balloon2 = itcl2!=NULL;
    for ( itcl2=itcl2h; itcl2!=NULL; itcl2= Next_list(itcl2) ) {
      itc2 = (PITContTyp)LookInfo_list(itcl2);
      itc2->sync_b = SplitGC( gsa, itc2->b, &(itc2->int_b) );
      balloon2 = balloon2 && itc2->sync_b==NULL && (itc2->int_b!=NULL) &&
	PureInt( gsap, itc2->int_b );
    }
  }
  FreeSS(gsa);

  /* End prepare ----- */


  /*
     balloon1 = balloon2 = FALSE;
     */

  itcl1 = itcl1h;
  itcl2 = itcl2h;

  if ( itcl1==NULL || balloon2 ){
#ifdef IEXPDBG
    if ( balloon2 )
      (void)printf("\nballoon (2)\n");
#endif
    for ( itcl2 = itcl2h; itcl2!=NULL; itcl2 = Next_list(itcl2) ) {

      itc2 = (PITContTyp)LookInfo_list(itcl2);
      label2  = LookLabelITC( itc2 );
      b2_sync = itc2->sync_b;
      b2_int  = itc2->int_b;

      if ( b2_int != NULL ) {
	for ( n=NumArgIB(b2_int), i=1; i<=n; i++ ) {
	  gate = LookActionArgIB(b2_int,i);
	  bi   = GetArgB( gate, 1 );
	  par  = CopyOperB( b );
	  AddArgB( par, cs1 );
	  AddArgB( par, bi );
	  AddArgB( gate, par );
	}
	nitc2        = NewITC();
	nitc2->label = ShareB(CopyLabel(label2));
	nitc2->b     = ShareB(b2_int);
	itcl         = Add_list( (DataListTyp)nitc2, itcl );
      }

      if (b2_sync!=NULL){
	LASSERT(!balloon2);
	FreeB(b2_sync);
	itc2->sync_b = NULL;
	itc2->int_b  = NULL;
      }

    }

    if ( itcl!=NULL )
      PutA(res,MakeA((AttrValueTyp)itcl,ITCLA));

    CleanAuxInfo( itcl1h, TRUE );

    FreeB(cs1p);
    FreeB(cs2p);
    return res;
  }


  if ( itcl2==NULL || balloon1 ){
#ifdef IEXPDBG
    if ( balloon1 )
      (void)printf("\nballoon (1)\n");
#endif
    for ( itcl1 = itcl1h; itcl1!=NULL; itcl1= Next_list(itcl1) ) {

      itc1    = (PITContTyp)LookInfo_list(itcl1);
      b1_sync = itc1->sync_b;
      b1_int  = itc1->int_b;
      label1  = LookLabelITC( itc1 );

      if ( b1_int != NULL ) {
	for ( n=NumArgIB(b1_int), i=1; i<=n; i++ ) {
	  gate = LookActionArgIB(b1_int,i);
	  bi  = GetArgB( gate, 1 );
	  par = CopyOperB( b );
	  AddArgB( par, bi );
	  AddArgB( par, cs2 );
	  AddArgB( gate, par );
	}
	nitc1        = NewITC();
	nitc1->label = ShareB(CopyLabel(label1));
	nitc1->b     = ShareB(b1_int);
	itcl         = Add_list( (DataListTyp)nitc1, itcl );
      }
      if ( b1_sync!=NULL ){
	LASSERT(!balloon1);
	FreeB(b1_sync);
	itc1->sync_b = NULL;
	itc1->int_b  = NULL;
      }
    }
    if ( itcl!=NULL )
      PutA(res,MakeA((AttrValueTyp)itcl,ITCLA));

    FreeB(cs1p);
    FreeB(cs2p);
    return res;
  }

  for ( firstTime=TRUE, itcl1=itcl1h; itcl1!=NULL; itcl1 = Next_list(itcl1) ) {
    itc1    = (PITContTyp)LookInfo_list(itcl1);
    label1  = LookLabelITC(itc1);
    b1_int  = itc1->int_b;
    b1_sync = itc1->sync_b;

    if ( b1_int != NULL && !balloon2 ) {
      for ( n=NumArgIB(b1_int), i=1; i<=n; i++ ) {
	gate = LookActionArgIB(b1_int,i);
	bi   = GetArgB( gate, 1 );
	par  = CopyOperB( b );
	AddArgB( par, bi );
	AddArgB( par, cs2p );
	AddArgB( gate, par );
      }
      itc1        = NewITC();
      itc1->label = ShareB(CopyLabel(label1));
      itc1->b     = ShareB(b1_int);
      itcl        = Add_list( (DataListTyp)itc1, itcl );
    }

    for ( itcl2 = itcl2h; itcl2!=NULL; itcl2 = Next_list(itcl2) ) {
      itc2    = (PITContTyp)LookInfo_list(itcl2);
      label2  = LookLabelITC(itc2);
      b2_sync = itc2->sync_b;
      b2_int  = itc2->int_b;
      if ( b1_sync!=NULL && b2_sync!=NULL ){
	newlabel = JoinLabel( CopyLabel(label1), CopyLabel(label2) );
	/*
	 * NOT VALID (example: e1.lot) :
	 *  if ( LookForITCL( pending, newlabel ) != NULL )
	 *   FreeLabel(newlabel);
	 *  else
	 *
	 */
	{
	  par = CopyOperB( b );
	  AddArgB( par, CopyUntilActB(b1_sync) );
	  AddArgB( par, CopyUntilActB(b2_sync) );
	  bc_sync = Par_Expand( par, (BehTyp)NULL,(BehTyp)NULL, FALSE, FALSE );
	  if ( LookTypeB(bc_sync) != StopC ) {
	    itc        = NewITC();
	    itc->label = ShareB(newlabel);
	    itc->b     = ShareB(bc_sync);
	    itcl       = Add_list( (DataListTyp)itc, itcl );
	  }
	  else {
	    FreeB(bc_sync);
	    FreeLabel(newlabel);
	  }
	}
      }
      if ( firstTime && b2_int != NULL && !balloon1 ) {
	for ( n=NumArgIB(b2_int),i=1; i<=n; i++ ) {
	  gate = LookActionArgIB(b2_int,i);
	  bi  = GetArgB( gate, 1 );
	  par = CopyOperB( b );
	  if ( GateInSS( gate, gsap ) )
	    AddArgB( par, cs1p );
	  else
	    AddArgB( par, cs1 ); /**/
	  AddArgB( par, bi );
	  AddArgB( gate, par );
	}
	itc2        = NewITC();
	itc2->label = ShareB(CopyLabel(label2));
	itc2->b     = ShareB(b2_int);
	itcl        = Add_list( (DataListTyp)itc2, itcl );
      }
    }
    firstTime = FALSE;
  }

  /* Clean auxiliary info  */

  CleanAuxInfo( itcl1h, FALSE );
  CleanAuxInfo( itcl2h, FALSE );

  /* End Clean ------------ */


  if ( itcl!=NULL )
    PutA(res,MakeA((AttrValueTyp)itcl,ITCLA));

  FreeB(cs1p);
  FreeB(cs2p);
  return res;
}



/******************************************************************
 *                                                                *
 *                Iexp                                            *
 *                                                                *
 *  Put into cs the continuation set and return the interleaved   *
 *  part iz.                                                      *
 *                                                                *
 *                                                                *
 *******************************************************************/


static PSyncGateSetTyp SyncSet_U_rfl_1_SyncSet( egsap, rfl )
     PSyncGateSetTyp  egsap;
     RelabFuncListTyp rfl;
{
  GateSetTyp      gsapUrfl_1gsap,rfl_1gsap,gsap;
  PSyncGateSetTyp newSyncSet;

  if ( !IsPartialSyncSS(egsap) )    /* || or ||| */
    return CopySS(egsap);

  gsap = egsap->gs;

  if ( rfl!=NULL ) {
    rfl_1gsap = InvApplyRFL( rfl, gsap );
    gsapUrfl_1gsap = JunctionGS( gsap, rfl_1gsap );
    FreeGS( rfl_1gsap );
  }
  else
    gsapUrfl_1gsap = CopyGS(gsap);

  newSyncSet = GateSet_to_SS( gsapUrfl_1gsap);

  return newSyncSet;
}


/* Iexp
 * transforms until actions
 */
static BehTyp Iexp( gsap, rfl, b, cs, bhtd )
     PSyncGateSetTyp  gsap;
     RelabFuncListTyp rfl;
     BehTyp           b, *cs;
     BehHashTabTyp    bhtd;
{
  BehTyp           b1,b2,bi,csi,res,cs1,cs2,term,
  choice,guard,hide,relab,enab,disab,
  itc_b,gate,bp;
  int              n,i;
  LabelTyp         label;
  DescriptorTyp    name;
  PAttrTyp         itcla;
  ITContListTyp    itcl;
  PITContTyp       itc;
  PSyncGateSetTyp  gsas,gsa;
  RelabFuncListTyp rfls;
  BehHashTabTyp    bhtd1, bhtd2;

  switch(LookTypeB(b)) {

  case StopC:
    *cs  = MakeB( 0, ContSetC );
    res  = b;
    break;

  case GateC:
  case IC:
  case ExitC:
    if ( !GateInSS(b,gsap) ){
      PutArgB( b, InsTC( gsap, rfl, GetArgB(b,1), cs, bhtd, FALSE ), 1 );
      if ( LookTypeB(b)==GateC ) {
	name = ActualRFL( rfl, LookNameB(b) );
	if ( name!=(DescriptorTyp)NULL )
	  PutNameB( b, name );
      }
      res = b;
    }
    else {
      *cs  = MakeB( 0, ContSetC );
      res  = MakeB( 0, StopC );
      FreeB(b); /**/
    }
    break;

  case AlternativeC:
    *cs  = MakeB( 0, ContSetC );
    n = NumArgB(b);
    for ( i=1; i<=n; i++ ) {
      bi = GetArgB( b, i );
      PutArgB( b, Iexp( gsap, rfl, bi, &csi, bhtd ), i );
      *cs = JoinContSets(*cs,csi);
    }
    res = Pre_Branch_Stop(b);
    break;

  case ParallelC:
    /* dbd */
    bhtd1 = LookAInfo(LookA(b,BHT1A));
    bhtd2 = LookAInfo(LookA(b,BHT2A));
    if ( IS_DUPLICATE_EXP /* (param_dbd || plain_dbd) */ &&  bhtd1==NULL ){
      LASSERT( bhtd2==NULL );
      bhtd1 = InitHashBehDef( IEXP_BHT_SIZE, TRUE );
      PutA(b,MakeA((AttrValueTyp)bhtd1,BHT1A));
      bhtd2 = InitHashBehDef( IEXP_BHT_SIZE, TRUE );
      PutA(b,MakeA((AttrValueTyp)bhtd2,BHT2A));
    }
    /*
     * Par_Iexp
     *
     */
    gsa   = Parallel_to_SS( b );
    gsas  = JunctionSS( gsap, gsa );
    bp = CopyOperB(b);
    (void)GetArgB( bp, 1 );
    (void)GetArgB( bp, 2 );
    PutNameB( b, INTER_SYNC );
    if ( LookA(b,GSA)!=NULL ) {
      UnshareA( b, GSA );
      FreeA( GetA( b, GSA ) );
    }
    b1 = GetArgB( b, 1 );
    PutArgB( b, InsTC( gsas, rfl, b1, &cs1, bhtd1, FALSE), 1 );
    b2 = GetArgB( b, 2 );
    PutArgB( b, InsTC( gsas, rfl, b2, &cs2, bhtd2, FALSE), 2 );
    ResolveVarCollisions( cs1, cs2 );
    *cs = CMatrix( bp, cs1, cs2, gsas );

    FreeB(bp);
    /*
       OLD SEMANTICS
       if ( LookTypeB(LookArgB(b,1))==StopC )
       GlueArgB(b,2);
       else
       if ( LookTypeB(LookArgB(b,2))==StopC )
       GlueArgB(b,1);
       */

    /* NEW SEMANTICS */
    if ( LookTypeB(LookArgB(b,1))==ContSetC )
      GlueArgB(b,2);
    else
      if ( LookTypeB(LookArgB(b,2))==ContSetC )
	GlueArgB(b,1);
    res = b;
    FreeB(cs1);
    FreeB(cs2);
    FreeSS( gsas );
    FreeSS( gsa );
    break;


  case ContSetC:
    /* NEW SEMANTICS */
    res  = MakeB( 0, ContSetC );
    /* OLD SEMANTICS */
    /* res  = MakeB( 0, StopC ); */
    *cs  = b;
    break;

  case ChoiceC:
    b1 = GetArgB( b, 1 );
    b1 = Iexp( gsap, rfl, b1, &cs1, bhtd );
    /* EYE */
    term = Look_IexpPreProc_Token( LookArgIB( b1, 1 ) );
    if ( LookTypeB(term)==TerminationC && LookA(cs1,ITCLA)!=NULL ) {
      label = CopyB(term);
      UnshareA( cs1, ITCLA );
      itcla = LookA(cs1,ITCLA);
      itcl = (ITContListTyp)LookAInfo(itcla);
      for ( ; itcl!=NULL; itcl=Next_list(itcl) ){
	itc = (PITContTyp)LookInfo_list(itcl);
	if ( EqualLabel( label, itc->label ) ){
	  choice = CopyOperB(b);
	  AddArgB( choice, UnshareB(itc->b) );
	  itc->b = ShareB( Distribute_Choice(choice) );
	  break;
	}
      }
      LASSERT( itcl!=NULL );
      FreeLabel(label);
    }
    PutArgB( b, b1, 1 );
    res = Distribute_Choice( b );
    *cs  = cs1;
    break;

  case GuardC:
    b1 = GetArgB( b, 1 );
    b1 = Iexp( gsap, rfl, b1, &cs1, bhtd );
    /* EYE */
    term = Look_IexpPreProc_Token( LookArgIB( b1, 1 ) );
    if ( LookTypeB(term)==TerminationC && LookA(cs1,ITCLA)!=NULL ) {
      label = CopyB(term);
      UnshareA( cs1, ITCLA );
      itcla = LookA(cs1,ITCLA);
      itcl = (ITContListTyp)LookAInfo(itcla);
      for ( ; itcl!=NULL; itcl=Next_list(itcl) ){
	itc = (PITContTyp)LookInfo_list(itcl);
	if ( EqualLabel( label, itc->label ) ){
	  guard = CopyOperB(b);
	  AddArgB( guard, UnshareB(itc->b) );
	  itc->b = ShareB( Distribute_Guard(guard) );
	  break;
	}
      }
      LASSERT( itcl!=NULL );
      FreeLabel(label);
    }
    PutArgB( b, b1, 1 );
    res = Distribute_Guard( b );
    *cs  = cs1;
    break;

  case EnablingC:
    b1  = GetArgB( b, 1 );
    b2  = GetArgB( b, 2 );
    res = Iexp( gsap, rfl, b1, &cs1, bhtd );   /* ULL : old InsTC */
    if ( LookA(cs1,ITCLA)!=NULL ) {
      UnshareA( cs1, ITCLA );
      itcla = LookA(cs1,ITCLA);
      itcl = (ITContListTyp)LookAInfo(itcla);
      for ( ; itcl!=NULL; itcl=Next_list(itcl) ) {
	enab = CopyOperB(b);
	b2   = CopyUntilActB(b2);                      /* >>B2 */
	itc  = (PITContTyp)LookInfo_list(itcl);
	PutArgB( enab, UnshareB(itc->b), 1 );
	PutArgB( enab, b2, 2 );
	itc->b = ShareB( Enabling_Expand(enab) );
      }
    }
    FreeB(b);
    *cs = cs1;
    break;

  case DisablingC:
    /* dbd */
    /*
       bhtd1 = LookAInfo(LookA(b,BHT1A));
       bhtd2 = LookAInfo(LookA(b,BHT2A)); disdcd4.lot
       if ( IS_DUPLICATE_EXP &&  bhtd1==NULL ){
       LASSERT( bhtd2==NULL );
       bhtd1 = InitHashBehDef( IEXP_BHT_SIZE, TRUE );
       PutA(b,MakeA((AttrValueTyp)bhtd1,BHT1A));
       bhtd2 = InitHashBehDef( IEXP_BHT_SIZE, TRUE );
       PutA(b,MakeA((AttrValueTyp)bhtd2,BHT2A));
       }
       b1 = GetArgB( b, 1 );
       b2 = GetArgB( b, 2 );
       b1 = InsTC( gsap, rfl, b1, &cs1, bhtd1 );
       b2 = InsTC( gsap, rfl, b2, &cs2, bhtd2 );
       */
    bhtd1 = LookAInfo(LookA(b,BHT1A));
    if ( IS_DUPLICATE_EXP /* (param_dbd || plain_dbd) */ &&  bhtd1==NULL ){
      bhtd1 = InitHashBehDef( IEXP_BHT_SIZE, TRUE );
      PutA(b,MakeA((AttrValueTyp)bhtd1,BHT1A));
    }
    b1 = GetArgB( b, 1 );
    b2 = GetArgB( b, 2 );
    b1 = InsTC( gsap, rfl, b1, &cs1, bhtd1, FALSE );
    b2 = InsTC( gsap, rfl, b2, &cs2, bhtd, TRUE );
    if ( LookA(cs1,ITCLA)!=NULL ) {
      UnshareA( cs1, ITCLA );
      itcla = LookA(cs1,ITCLA);
      itcl  = (ITContListTyp)LookAInfo(itcla);
      for ( ; itcl!=NULL; itcl=Next_list(itcl) ){
	itc   = (PITContTyp)LookInfo_list(itcl);
	itc_b = itc->b;
	for ( n=NumArgIB(itc_b), i=1; i<=n; i++ ){
	  gate = LookActionArgIB(itc_b,i);
	  LASSERT(LookTypeB(gate) == GateC ||
		  LookTypeB(gate) == IC ||
		  LookTypeB(gate) == ExitC );
	  if ( ( LookTypeB(gate)==IC || LookTypeB(gate)==GateC) &&
	      LookA(cs2,ITCLA)!=NULL ){
	    bi   = GetArgB(gate,1);
	    disab = CopyOperB(b);       /* sharing bhtd's */
	    AddArgB( disab, bi );
	    AddArgB( disab, CopyB(cs2) );
	    AddArgB( gate, disab );
	  }
	}
      }
    }
    if ( LookTypeB(b2)==ContSetC ){
      LASSERT(LookA(b2,ITCLA)==NULL); /* standby */
      FreeB(b);
      FreeB(b2);
      res = b1;
    }
    else {
      PutArgB( b, b1, 1 );
      PutArgB( b, b2, 2 );
      res = b;
    }
    *cs = JoinContSets( cs1, cs2 );
    break;


  case RelabellingC:
    rfls = JunctionRFL( CopyRFL(rfl),
		       CopyRFL((RelabFuncListTyp)LookAInfo(LookA(b,RFLA)))
		       );
    gsas = SyncSet_U_rfl_1_SyncSet( gsap, rfls );
    b1    = GetArgB( b, 1 );
    res   = Iexp( gsas, rfls, b1, &cs1, bhtd );
    if ( LookA(cs1,ITCLA)!=NULL ) {
      UnshareA( cs1, ITCLA );
      itcla = LookA(cs1,ITCLA);
      itcl = (ITContListTyp)LookAInfo(itcla);
      for ( ; itcl!=NULL; itcl=Next_list(itcl) ) {
	relab = CopyOperB(b);
	itc   = (PITContTyp)LookInfo_list(itcl);
	PutArgB( relab, UnshareB(itc->b), 1 );
	/*      itc->b = ShareB( Iexp_Relabel_Proc(relab) ); */
	itc->b = ShareB( Iexp_Pre_Proc(relab) );
      }
    }
    FreeB(b);
    FreeRFL( rfls );
    FreeSS( gsas );
    *cs = cs1;
    break;


  case HidingC:
    b1    = GetArgB( b, 1 );
    res   = Iexp( gsap, rfl, b1, &cs1, bhtd );
    if ( LookA(cs1,ITCLA)!=NULL ) {
      UnshareA( cs1, ITCLA );
      itcla = LookA(cs1,ITCLA);
      itcl = (ITContListTyp)LookAInfo(itcla);
      for ( ; itcl!=NULL; itcl=Next_list(itcl) ) {
	hide  = CopyOperB(b);
	itc   = (PITContTyp)LookInfo_list(itcl);
	PutArgB( hide, UnshareB(itc->b), 1 );
	/*      itc->b = ShareB( Iexp_Hide_Proc(hide) ); */
	itc->b = ShareB( Iexp_Pre_Proc(hide) );
      }
    }
    FreeB(b);
    *cs = cs1;
    break;


  default:
    Error("Iexp : Unexpected cell type.");

  }

  return res;
}


/******************************************************************
 *                                                                *
 *          Interleaved Expansion                                 *
 *                                                                *
 *******************************************************************/


/* Start
 * Iexpansion of the first state of a behaviour or global continuation.
 * Filter out exit alternatives and Iexpand the rest.
 *   If depth == 0 then return Iexp_Pre_Proc(b)
 *   b_itc is the itc whose itc->b is b. ( it is NULL for the root behaviour ).
 *  *current_term contains the value of the termination counter after computing
 *   InsTC on the continuation to be iexpanded.
 */
static BehTyp Start( gsap, rfl, b, b_itc, cs, depth, isDeadlock, deadlocks )
     PSyncGateSetTyp  gsap;
     RelabFuncListTyp rfl;
     BehTyp           b, *cs;
     PITContTyp       b_itc;
     int              depth;
     boolean          *isDeadlock;
     ListTyp          *deadlocks;
{
  BehTyp         b1,b2p,pp_b,pp_b_filtered,pp_bi,res,itc_b/*,gate*/;
  int            i,n,cti,ctf;
  PAttrTyp       itcla;
  ITContListTyp  itcl,itclh,itclh2;
  PITContTyp     itc,dupitc,iexp_itc,itcc,pend_itc;
  ListTyp        csl,paux;
  boolean        first;

  res           = NULL;
  pp_b          = Iexp_Pre_Proc( GetUntilActB(b) );

  /*
     PrintBeh(pp_b,-1,TRUE,FALSE,"",printTarget,TRUE,FALSE);
     */

  /* Success Event stop condition ---------------------------- */

  if ( successEvent!=0 ){
    if ( b_itc!=NULL ){
      for ( i=1,n=NumArgIB(pp_b); i<=n; i++ ){
	/*
	 * Delete successful state to save up memory and
	 * cause the exploration to stop.
	 *
	 */
	/*
	   gate = LookActionArgIB(pp_b,i);
	   if ( ( LookTypeB(gate)==GateC || LookTypeB(gate)==IC )
	   && IsSuccessfulState( LookArgB(gate,1))
	   ){
	   FreeB(GetArgB(gate,1));
	   succ = MakeB( successEvent, GateC );
	   AddArgB( succ, MakeB(0,StopC) );
	   AddArgB( gate, succ );
	   }
	   */
      }
    }
    else
      if ( IsSuccessfulState( pp_b ) ) {
	/*
	 * Delete successful state to save up memory and
	 * cause the exploration to stop.
	 *
	 */
	FreeB( pp_b );
	pp_b = MakeB( successEvent, GateC );
	AddArgB( pp_b, MakeB(0,StopC) );
      }
  }

  /* End Success Event stop condition -------------------------------*/

  /* Depth stop condition ------------------------------------ */

  if ( depth == 0 ) {
    *cs = MakeB( 0, ContSetC );
    Leaf( max_depth <0 ? -(depth+1) : max_depth-depth );
    return pp_b;
  }
  else
    Digging( max_depth <0 ? -(depth+1) : max_depth-depth );

  /* End depth stop condition --------------------------------------- */


  /* Extract the exits from pp_b ------------------------------------ */

  pp_b_filtered = NULL;
  for ( n=NumArgIB(pp_b), i=1; i<=n; i++ ) {
    pp_bi = LookArgIB(pp_b,i);
    if ( LookTypeB(Look_IexpPreProc_Token(pp_bi))==ExitC ) {
      res = AppendUB( res, CopyUntilActB(pp_bi) );
    }
    else {
      pp_b_filtered = AppendUB( pp_b_filtered, CopyUntilActB(pp_bi) );
    }
  }
  FreeB( pp_b );

  /* End Extract ----------------------------------------------------- */

  if ( pp_b_filtered==NULL ){           /* pp_b == Sumi CHi Gi exit */
    *cs    = MakeB( 0, ContSetC );
    if ( b_itc!=NULL ){
      FreeB(UnshareB(b_itc->b));
      b_itc->b  = ShareB(res);

      dupitc = LookForITCL( iexpanded, LookLabelITC(b_itc) );

      /* Update Iexpanded conts list */

      if ( dupitc==NULL ){
	iexp_itc  = CopyShareITC(b_itc);
	iexpanded = Insert_list( (DataListTyp)iexp_itc, iexpanded );
	num_m_states++;
      }
      /* End Update ---------------- */

    }
#ifdef IEXPDBG
    (void)printf("\n-----------------------------------------------\n");
#endif
  }
  else {   /* hay bacalao que cortar (sic) */

    if ( b_itc!=NULL ){

      /* n(m) for iexpanding the itc with the right termination counter */

      dupitc = LookForITCL( iexpanded, LookLabelITC(b_itc) );
      if ( !IS_DUPLICATE_EXP )
	if ( dupitc==NULL || dupitc->n_label==0 ){
	  ResetTerm();
	}
	else {
	  SetTerm(dupitc->n_label);
	}
      generate_dupproc = dupitc==NULL;
    }

    /* Iexpansion ------------------ */

    cti = CurrentTerm();
    b1  = InsTC( gsap, CreateRFL(), pp_b_filtered, cs, sbhtd, FALSE );
    ctf = CurrentTerm();

#ifdef IEXPDBG
    if ( b_itc ){
      (void)printf("\n");
      PrintLabel( b_itc->label, printTarget );
      if ( dupitc )
	(void)printf("-> current : %d first : %d , last : %d",dupitc->n_label,cti,ctf);
      else
	(void)printf("-> current : NO first : %d , last : %d",cti,ctf);
    }
#endif

    res = AppendUB( res, b1 );
    /*
       PrintBeh(res,-1,TRUE,FALSE,"",printTarget,TRUE,FALSE);
       */
#ifdef IEXPDBG
    (void)printf("\n-----------------------------------------------\n");
#endif

    /* End Iexpansion -------------- */


    if ( b_itc!=NULL ){

      FreeB(UnshareB(b_itc->b));
      b_itc->b  = ShareB(res);

      /* Update Iexpanded conts list */

      if ( dupitc==NULL ){
	num_m_states++;
	iexp_itc  = CopyShareITC(b_itc);
	iexpanded = Insert_list( (DataListTyp)iexp_itc, iexpanded );
	/**/
	pend_itc = LookFor_IdenticalITCL( pending, b_itc );
	LASSERT(pend_itc!=NULL );
	paux = LookFor_list( (DataListTyp)pend_itc, pending, EqInt );
	LASSERT(paux!=NULL );
	pending   = DeleteNode_list( paux, pending );
      }
      else
	iexp_itc = dupitc;

      /* End Update ---------------- */

      /* Update Iexpanded conts list */

      /*
       * first expenditure of terminations in this continuation
       */
      if ( iexp_itc->n_label==0 && (cti != ctf) )
	iexp_itc->n_label = cti;
    }

    /* End Update ---------------- */


    if ( LookA(*cs,ITCLA)==NULL ) {
      Leaf( max_depth <0 ? -(depth+1) : max_depth-depth );
    }
    else {
      /* Iexpansion of the continuations produced */

      UnshareA( *cs, ITCLA );
      itcla   = LookA( *cs, ITCLA );
      itclh   = (ITContListTyp)GetAInfo(itcla);

      /*
       * Select those "iexpanded & identical" continuations.
       * Be careful not to rule out equal continuations in this level
       *
       */

      for ( itclh2 = itcl = itclh , itclh = Create_list();
	   itcl != NULL; itcl = Next_list(itcl) ) {
	itc = (PITContTyp)LookInfo_list(itcl);
	if ( itc->cset_labels==NULL ){
	  csl = CSets_Labels_in_Beh( itc->b );
	  Apply_Func_list( csl, (DataListTyp(*)())ShareB );/**/
	  if ( csl!=NULL )
	    itc->cset_labels = Insert_list( (DataListTyp)csl, itc->cset_labels );
	}
	/* dupitc  = LookFor_Update_IdenticalITCL( iexpanded, itc ); */

	/**/
	dupitc  = LookFor_IncluderITCL( pending, itc );
	if ( dupitc!=NULL ){
#ifdef IEXPDBG
	  (void)printf("-");
#endif
	}
	else {
	  dupitc  = LookFor_Update_IncluderITCL( iexpanded, itc );
	  if ( dupitc!=NULL ){
#ifdef IEXPDBG
	    (void)printf("(-)");
#endif
	  }
	  else {
	    itcc = CopyShareITC(itc);
	    itclh = Add_list( (DataListTyp)itcc, itclh );
	    pending = Insert_list( (DataListTyp)CopyShareITC(itcc), pending );
	  }
	}
#ifdef IEXPDBG
	PrintLabel( itc->label, printTarget );
	(void)printf(" : ");
	Print_LL( printTarget,  (ListTyp)LookInfo_list(itc->cset_labels) );
	(void)printf("\n");
#endif
      }
      FreeITCL(itclh2);
      /* End Select ---------------------------------------------------- */

      first = TRUE;
      for ( itcl = itclh; itcl!=NULL; itcl=Next_list(itcl) ) {
	if ( !first )
	  Branch( max_depth <0 ? -(depth+1) : max_depth-depth );
	itc = (PITContTyp)LookInfo_list(itcl);

	/* Iexpansion (even duplicated ones) */
	itc_b  = itc->b;
	(void)
	  ( Start( gsap, CreateRFL(), itc_b, itc, &b2p, depth-1,
		  &(itc->isDeadlock), &(itc->deadlocks) )
	   );
	FreeB( b2p );
	first = FALSE;
	/* End Iexpansion of this continuation */

      }

      /*
       * the return of *cs can be ruled out in the future for efficiency sake
       */
      if ( itclh!=NULL )
	PutAInfo( itcla, (AttrValueTyp)itclh );
      else {
	Leaf( max_depth <0 ? -(depth+1) : max_depth-depth );
	FreeA(GetA(*cs,ITCLA));
      }
    }
  }

  return res;
}


/* InterleavedExpansion
 * Returns the interleaved expansion of the behaviour b.
 * The exploration stops after a depth d of synchronizations or when
 * the success event se is offered by the continuation.
 * If dup (or param), the explorations also stops when a duplicate state
 * (or a parameterized duplicated state) is found.
 */
BehTyp InterleavedExpansion( b, d, se, proc, dup, param, verb )
     BehTyp        b;
     int           d;
     DescriptorTyp se, proc;
     boolean       dup, param, verb;
{
  BehTyp           b1,b2,res;
  PSyncGateSetTyp  gsap;
  PAttrTyp         itcla;
  boolean          isDeadlock;
  ListTyp          deadlocks;
  DescriptorTyp    last_proc;

#ifdef IEXPDBG
  printTarget("\n\n Optimized Interleaved Expansion.\n");
  printTarget(" Version for full LOTOS under development.\n");
#endif


  max_depth    = (d<0)? -1 : d;
  num_m_states = 1;
  num_trans    = 0;
  successEvent = se;
  verbose_mode = verb;
  last_proc    = LastTableP();
  InitTerm();
  InitIexpFlags( dup, param );
  iexpanded = Create_list();
  pending   = Create_list();
  gsap      = CreateSS();
  sbhtd = NULL;
  if ( IS_DUPLICATE_EXP /* dup || param */ ){
    sbhtd = InitHashBehDef( IEXP_BHT_SIZE, TRUE );
  }
  Header();
  if (verbose_mode) {
    (void)sprintf(buff,"%5d",0);
    if (runtimeConfig==TextMode) {
      printMsgs(buff);
    }
    else {
      printPos(buff,-1);
      flushTarget();
    }
    contdepth    = 1;
    contactdepth = 1;
  }

  b1   = Start( gsap, CreateRFL(), b,
	       (PITContTyp)NULL, &b2, d, &isDeadlock, &deadlocks );

  if (verbose_mode)
    if (runtimeConfig==TextMode) {
      printMsgs(".\n\n");
    }
    else {
      printPos(".\n\n",-1);
      flushTarget();
    }

  res  = MakeB( 0, InterleavedC );
  PutArgB( res, b1, 1 );
  PutArgB( res, b2, 2 );
  if ( LookA(b2,ITCLA)!=NULL ) {
    UnshareA( b2, ITCLA );
    itcla = LookA(b2,ITCLA);
    FreeITCL( (ITContListTyp)GetAInfo(itcla) );
    PutAInfo( itcla, (AttrValueTyp)iexpanded );
  }
  FreeSS( gsap );

  if ( sbhtd!=NULL ){
    printTarget("\n Post processing...");
    FreeHashBehDef( sbhtd );
    if ( param )
      PClearBeh( res, last_proc );
    else
      ClearBeh( res );

    DupProcTab_Func( last_proc+1 );
    /*
       RmParameters( res, last_proc+1 );
       */
    printTarget("done\n\n");
  }
  if ( se!=(DescriptorTyp)NULL ){
    IT_Testing( res, se, proc, verb );
  }
  return res;
}

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

/* InitIT
 * Initialization of the interface InTerleaved
 */
void InitIT()
{
  InitITC();
  InitSS();
}

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











