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

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

/******************************************************************
 *  
 *  Santiago Pavon Gomez
 *  David Larrabeiti Lopez
 *
 *  17 Dec 1992
 *
 *  Management of Interleaved Expansion Continuations (ITC)
 *
 *         <n1,n2,...,nm> B   or <c> Bc 
 *
 *  and Interleaved Continuations lists (ITCL), representing
 *  Continuation Sets { <c1>Bc1, ..., <cm>Bcm }.
 * 
 *  COMPILATION FLAGS:
 *  
 *  LOG:
 *
 ******************************************************************/

/* LINTLIBRARY */

#include "baattr.h"
#include "baprint.h"
#include "listdh.h"
#include "limisc.h"
#include "badefca.h"
#include "lilists.h"


/******************************************************************
 *                                                                *
 *                  Termination Counter                           *
 *                                                                *
 ******************************************************************/

/*
 * Global Termination counter
 *
 */
static int aux_tercont = 1, tercont = 1 ;

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

/* InitTerm
 * Reset to 1 the termination counter.
 */
int InitTerm()
{
  aux_tercont  = 1;
  tercont      = 1;
}

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

/* NewTerm
 *  Return a new termination value.
 */
int NewTerm()
{
  return tercont++;
}

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

/* CurrentTerm
 * Return the current termination value.
 */
int CurrentTerm()
{
  return tercont;
}

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

/* SetTerm
 *  Set temporarily the termination counter to n.
 */
void SetTerm( n )
     int n;
{
  aux_tercont = MAX(aux_tercont,tercont);
  tercont = n;
}

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

/* ResetTerm
 * Reset the termination counter to a brandnew value, after having been
 * set to a temporary value.
 */
void ResetTerm()
{
  if ( aux_tercont > tercont )
    tercont = aux_tercont;
}

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

/* DisposeTerm
 *  Release the last termination value. ( decrement term-counter ).
 */
void DisposeTerm()
{
  tercont -= 1;
}


/******************************************************************
 *                                                                 *
 *               Labels                                            *
 *                                                                 *
 *        A label is a concatenation of termination cells sorted   *
 *        by name and joined by their first argument               *
 *                                                                 *
 *        Example :                                                *
 *                                                                 *
 *        < 3(x:s), 11, 24(z:s,w:s2), 3847 >                       *
 *                                                                 *
 *                                                                 *
 *                                                                 *
 *                                                                 *
 *******************************************************************/


/* FreeLabel
 * Free a label
 */
void FreeLabel( label )
     LabelTyp label;
{
  FreeB( label );
}

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

/* EqualLabel
 * Decide whether 2 labels are equal. Only numbers are compared.
 */
boolean EqualLabel( label1, label2 )
     LabelTyp label1, label2;
{
  LASSERT(label1!=NULL&&label2!=NULL);
  for ( ;
       label1!=NULL && label2!=NULL;
       label1 = LookArgB(label1,1), label2 = LookArgB(label2,1)
       ){
    LASSERT(LookTypeB(label1)==TerminationC &&
	    LookTypeB(label2)==TerminationC);
    if ( LookNameB(label1)!=LookNameB(label2) )
      return FALSE;
  }
  return label1==NULL && label2==NULL;
}

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

/* InsertLabel
 * Append a termination to a label in a sorted way.
 * Example : InsertLabel( 3, <1,4,9> ) = <1,3,4,9>
 */
LabelTyp InsertLabel( t, label )
     BehTyp   t;
     LabelTyp label;
{
  LabelTyp n,last;
  
  if (label==NULL)
    return t;
  
  LASSERT( LookCopy(label)==0 );
  for ( last=n=label; n!=NULL; last=n, n=LookArgB(n,1) ){
    LASSERT((int)LookNameB(n)!=LookNameB(t));
    if ( (int)LookNameB(n) > LookNameB(t) ){
      if ( last==n ){
	AddArgB(t,last);
	return t;
      }
      else{
	n = GetArgB(last,1);
	AddArgB(last,t);
	AddArgB(t,n);
	return label;
      }
    }
  }
  LASSERT( n==NULL && last!=NULL );
  AddArgB( last, t);
  return label;
}

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

/* CopyLabel
 * Copy a label
 */
LabelTyp CopyLabel( label )
     LabelTyp  label;
{
  return CopyB( label );
}

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

/* JoinLabel
 * Join 2 labels in a sorted way. ( label1 & label2 no longer exist ).
 * Example : JoinLabel( <3,7>, <1,4,9> ) = <1,3,4,7,9>
 */
LabelTyp JoinLabel( label1, label2 )
     LabelTyp  label1, label2;
{
  LabelTyp n,nn;
  
  LASSERT(label1!=NULL||label2!=NULL);
  for ( n=label1; n!=NULL; n=LookArgB(n,1) ){
    nn = CopyOperB(n);
    if ( LookArgB(nn,1)!=NULL )
      (void)GetArgB(nn,1);
    label2 = InsertLabel( nn, label2 );
  }
  FreeB( label1 );
  return label2;
}

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

/* HashKeyLabel
 * hash value for a label
 */
int HashKeyLabel( p )
     LabelTyp p;
{
  int res = 0;
  for ( ; p!=NULL; p = LookArgB(p,1) )
    res +=LookNameB(p);
  return res;
}

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

/* PrintLabel
 * Print a label with pstr ( only descriptors ).
 */
void PrintLabel( label, pstr )
     LabelTyp label;
     void (*pstr)();
{
  LabelTyp l;
  
  pstr("<");
  for ( l=label; l!=NULL; l=LookArgB(l,1) ){
    PrintInt(pstr,(int)LookNameB(l));
    if ( LookArgB(l,1)!=NULL )
      pstr(",");
  } 
  pstr(">");
}

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

/* LookForLabel
 * Determine whether a termination belongs to a label.
 * return a pointer to the matched termination in the label
 */
LabelTyp LookForLabel( t, label )
     int       t;
     LabelTyp  label;
{
  for ( ; label!=NULL; label=LookArgB(label,1) ){
    if ( (int)LookNameB(label) == t )
      return label;
    if ( (int)LookNameB(label) > t )
      return NULL;
  }
  return NULL;
}

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

/* SubLabel
 * Determine whether label sl is a sublabel of label.
 * Only descriptors are taken into account.
 */
boolean SubLabel( sl, label )
     LabelTyp sl, label;
{
  LabelTyp n;
  
  for ( ; sl!=NULL; sl = LookArgB(sl,1)){
    for ( n=label; n!=NULL; n=LookArgB(n,1) )
      if ( LookNameB(n)==LookNameB(sl) )
	break;
    if ( n == NULL )
      return FALSE;
  }
  return sl==NULL;
}


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

/* SubLabelList
 * Determine whether a label is a sublabel of the label made by
 * the list of integers tl.
 */
boolean SubLabelList( label, tl )
     LabelTyp label;
     ListTyp  tl;
{
  ListTyp n;
  
  for ( ; label!=NULL; label=LookArgB(label,1) ){
    for ( n = tl; n!=NULL; n = Next_list(n) )
      if ( LookNameB(label)==(DescriptorTyp)LookInfo_list(n) )
	break;
    if ( n == NULL )
      return FALSE;
  }
  return label==NULL;
}


/******************************************************************
 *                                                                 *
 *               Label lists                                       *
 *                                                                 *
 *******************************************************************/


/* Free_LL
 * Free a list of labels
 */
void Free_LL( labl )
     ListTyp labl;
{
#ifdef SDEBUG
  ListTyp n;
  for ( n=labl; n!=NULL; n=Next_list(n) ){
    LASSERT( LookCopy((BehTyp)LookInfo_list(n))==1 );
  }
#endif
  Apply_Func_list( labl, (DataListTyp(*)())UnshareB );
  Free_list( labl, FreeLabel );
}

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

/* Copy_LL
 * Copy a label list
 */
ListTyp Copy_LL( labl )
     ListTyp labl;
{
  ListTyp res;
  
  res = Copy_list( labl, (DataListTyp(*)())CopyLabel );
  Apply_Func_list( res, (DataListTyp(*)())ShareB );
  
  return res;
}

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

/* Print_LL
 * Print a list of labels
 */
void Print_LL( pstr, labl )
     void    (*pstr)(); 
     ListTyp labl;
{
  printTarget("{");
  for ( ;labl!=NULL; labl=Next_list(labl) ){
    PrintLabel( (LabelTyp)LookInfo_list(labl), pstr );
    if ( Next_list(labl)!=NULL )
      printTarget(",");
  }
  printTarget("}");
}

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

/* HashF_LL
 * Label list hash function. Only descriptors are considered.
 */
int HashF_LL( labl )
     ListTyp labl;
{
  LabelTyp label;
  int      res = 0;
  int      n   = 1;
  
  for ( ;labl!=NULL; labl=Next_list(labl), n++ ){
    label = (LabelTyp)LookInfo_list(labl);
    for ( ;label!=NULL; label=LookArgB(label,1) )
      res += (int)LookNameB(label)+n;
  }
  return res;
}

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

/* Equal_LL
 * Label list equality.
 */
boolean Equal_LL( labl1, labl2 )
     ListTyp labl1, labl2;
{
  
  if ( Length_list(labl1)!=Length_list(labl2) )
    return FALSE;
  for ( ; labl1!=NULL; labl1=Next_list(labl1) )
    if ( !In_list( LookInfo_list(labl1),labl2,EqualLabel) )
      return FALSE;
  return TRUE;
}

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

/* SubSet_LL
 * Say whether labl1 is a subset of labl2.
 */
boolean SubSet_LL( labl1, labl2 )
     ListTyp labl1, labl2;
{
  for ( ; labl1!=NULL; labl1=Next_list(labl1) )
    if ( !In_list( LookInfo_list(labl1),labl2,EqualLabel) )
      return FALSE;
  return TRUE;
}

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

/* Insert_LL
 * Insert a label into a label list
 */
ListTyp Insert_LL( label, labl )
     LabelTyp label;
     ListTyp  labl;
{
  LASSERT( LookCopy(label)==0 );
  return Insert_list( (DataListTyp)ShareB(label), labl);
}


/******************************************************************
 *                                                                 *
 *                     IT Continuations                            *
 *                                                                 *
 *******************************************************************/


static int new_itc_count      = 0;
static int released_itc_count = 0;
static int max_itc_count      = 0;

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

/* InitITC
 * Init the ITC module
 */
void InitITC()
{
#ifdef SDEBUG
  new_itc_count      = 0;
  released_itc_count = 0;
  max_itc_count      = 0;
#endif
}

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

/* NewITC
 * Get memory for a new interleaved continuation.
 */
PITContTyp NewITC()
{
  PITContTyp p;
  
#ifdef SDEBUG
  new_itc_count++;
  max_itc_count = MAX( max_itc_count, new_itc_count-released_itc_count );
#endif
  p                 = (PITContTyp) NewCellM(sizeof(ITContTyp));
  p->label          = NULL;
  p->b              = NULL;
  p->n_label        = 0;
  p->cset_labels    = NULL;
  p->cset_labels_ht = NULL;
  p->isDeadlock     = TRUE;
  p->deadlocks      = NULL;
  p->path           = NULL;
  p->int_b          = NULL;
  p->sync_b         = NULL;
  return p;
}

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

/* DispITC
 * Free memory used by the PITContTyp struct.
 */
void DispITC( itc )
     PITContTyp itc; 
{
#ifdef SDEBUG
  released_itc_count++;
#endif
  FreeCellM( (void*)itc, sizeof(ITContTyp) );
}

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

/* FreeITC
 *  Deallocate the memory used by the interleaved continuation itc.
 */
void FreeITC( itc )
     PITContTyp itc; 
{
  if ( itc==NULL )
    return;
  if ( itc->label!=NULL ){
    LASSERT( LookCopy(itc->label)>=1 );
    FreeLabel( UnshareB(itc->label) );
    itc->label = NULL;
  }
  Free_list( itc->deadlocks, FreeLabel );
  itc->deadlocks = NULL;
  Free_list( itc->cset_labels, Free_LL );
  itc->cset_labels = NULL;
  if ( itc->cset_labels_ht!=NULL ){
    Free_HT( itc->cset_labels_ht ); 
    itc->cset_labels_ht = NULL;
  }
  if (itc->b!=NULL) {
    itc->b = UnshareB(itc->b);
    FreeB(itc->b);
    itc->b = NULL;
  }
  if ( itc->path!=NULL ){
    FreeLabel( UnshareB(itc->path) );
    itc->path = NULL;
  }
  DispITC(itc);
}

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

/* CopyITC
 * Copy the interleaved continuation itc, copying its behaviour until actions.
 * The cset_labels hash table is not copied.
 */
PITContTyp CopyITC( itc )    
     PITContTyp itc;
{
  PITContTyp n;
  
  n              = NewITC();
  n->label       = itc->label ? ShareB(CopyLabel(itc->label)) : NULL;
  n->b           = ShareB(CopyUntilActB(itc->b));
  n->n_label     = itc->n_label;
  n->isDeadlock  = itc->isDeadlock;
  n->deadlocks   = Copy_list( itc->deadlocks, (DataListTyp (*)())CopyLabel );
  n->cset_labels = Copy_list( itc->cset_labels, (DataListTyp (*)())Copy_LL );
  n->cset_labels_ht = NULL;
  n->path        = itc->path ? ShareB(CopyLabel(itc->path)) : NULL;
  
  return n;
}

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

/* CopyShareITC
 * Make a new continuation sharing all shareable contents of itc
 */
PITContTyp CopyShareITC( itc )    
     PITContTyp itc;
{
  PITContTyp n;
  
  n              = NewITC();
  n->label       = itc->label ? ShareB(itc->label) : NULL;
  n->b           = ShareB(itc->b);
  n->n_label     = itc->n_label;
  n->isDeadlock  = itc->isDeadlock;
  n->deadlocks   = Copy_list( itc->deadlocks, (DataListTyp (*)())CopyLabel );
  n->cset_labels = Copy_list( itc->cset_labels, (DataListTyp (*)())Copy_LL );
  n->cset_labels_ht = NULL;
  n->path        = itc->path ? ShareB(itc->path) : NULL;
  
  return n;
}

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

/* StatITC
 * new      : number of cell queries the system has granted this module with.
 * released : number of cell releases.
 * max      : max number of cells hold on by this module till now.
 */
void StatITC( new, released, max )
     int * new, *released, *max;
{
  *new      = new_itc_count;
  *released = released_itc_count;
  *max      = max_itc_count;
}

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

/* LookLabelITC
 * Look at an itc label.
 */
LabelTyp LookLabelITC( itc )
     PITContTyp itc;
{
  return itc->label;
}

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

/* GetLabelITC
 * Get an itc label.
 */
LabelTyp GetLabelITC( itc )
     PITContTyp itc;
{
  LabelTyp label;
  label      = UnshareB(itc->label);
  itc->label = NULL;
  return label;
}

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

/* LookBehITC
 * Look at an itc behaviour.
 */
BehTyp LookBehITC( itc )
     PITContTyp itc;
{
  return itc->b;
}

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

/* PrintITC
 * Print the interleaved continuation itc.
 * pstr is the function used to print strings.
 */
void PrintITC( itc , pstr )
     PITContTyp itc;
     void (*pstr)(); 
{
  PrintLabel( itc->label, pstr );
  pstr("\n");
  PrintBeh(itc->b,-1,NO_PROC,FALSE,"",pstr,TRUE,FALSE);
}

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

/* FreeITCL
 * Deallocate the memory used by the interleaved continuation list itcl.
 */
void FreeITCL( itcl )
     ITContListTyp itcl; 
{
  Free_list(itcl,FreeITC);
}

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

/* CopyITCL
 * Copy the interleaved continuation list itcl.
 */
ITContListTyp CopyITCL( itcl )    
     ITContListTyp itcl; 
{
  return Copy_list(itcl,(DataListTyp(*)())CopyITC);
}

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

/* InsertITCL
 * Insert a itc in a list
 */
ITContListTyp InsertITCL( itcl, label, b, n_m ) 
     ITContListTyp itcl;
     LabelTyp      label;
     BehTyp        b;
     int           n_m;
{
  PITContTyp n;
  
  n          = NewITC();
  n->label   = ShareB(label);
  n->b       = ShareB(b);
  n->n_label = n_m;
  return Insert_list( (DataListTyp)n, itcl );
}

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

/* PrintITCL
 * Print the interleaved continuation list itcl.
 * pstr is the function used to print strings.
 */
void PrintITCL( itcl , pstr )
     ITContListTyp itcl;
     void (*pstr)(); 
{
  while (itcl!=NULL) {
    PrintITC((PITContTyp)LookInfo_list(itcl),pstr);
    itcl = Next_list(itcl);
  }
}

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

/* StatisticITC
 * Return the number of itc nodes (itcn) and list nodes (ln),
 * used in the interleaved continuation list itcl.
 * Return also a list of behaviours to be processed by StatSpecification()
 */
ListTyp StatisticITC( itcl, itcn, ln )
     ITContListTyp itcl;
     int          *ln, *itcn;
{
  ITContListTyp l;
  PITContTyp    itc;
  ListTyp       ll,ll2,res;
  
  res = Create_list();
  *ln = *itcn = Length_list(itcl);
  for ( l=itcl; l!=NULL; l = Next_list(l) ) {
    itc = (PITContTyp)LookInfo_list(l);
    res = Insert_list( (DataListTyp)itc->label, res );
    if ( itc->path!=NULL )
      res = Insert_list( (DataListTyp)itc->path, res );
    for ( ll=itc->cset_labels; ll!=NULL; ll=Next_list(ll) ){
      (*ln)++;
      for ( ll2=(ListTyp)LookInfo_list(ll); ll2!=NULL; ll2=Next_list(ll2) ){
	(*ln)++;
	res = Insert_list( (DataListTyp)LookInfo_list(ll2), res );
      }
    }
    for ( ll=itc->deadlocks; ll!=NULL; ll=Next_list(ll) )
      *ln += Length_list((ListTyp)LookInfo_list(ll));
  }
  res = Join_list( res, Copy_list( itcl, (DataListTyp(*)())LookBehITC ) );
  return res;
}

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

/* LookForITCL
 * Look for a continuation labelled <label> in an itcl.
 * NULL if <label> does not belong to itcl.
 */
PITContTyp LookForITCL( itcl, label )
     ITContListTyp itcl;
     LabelTyp      label;
{
  PITContTyp pit;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( EqualLabel( pit->label, label ) )
      break;
  }
  if (itcl!=NULL) {
    return pit;
  }
  else
    return NULL;
  
}
/*----------------------------------------------------------------*/

/* LookForNodeITCL
 * Look for a continuation labelled <label> in an itcl.
 * return the list node of that continuation
 * NULL if <label> does not belong to itcl.
 */
ListTyp LookForNodeITCL( itcl, label )
     ITContListTyp itcl;
     LabelTyp      label;
{
  PITContTyp pit;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( EqualLabel( pit->label, label ) )
      break;
  }
  return (ListTyp)itcl;
}

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

/* LookFor_SubSet_ITCL
 * Look for a continuation labelled <c> in itcl subset of <label>.
 * NULL if there is not such a <c> in itcl.
 */
PITContTyp LookFor_SubSet_ITCL( itcl, label )
     ITContListTyp itcl;
     LabelTyp      label;
{
  PITContTyp pit;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( SubLabel( pit->label, label ) )
      break;
  }
  if (itcl!=NULL) {
    return pit;
  }
  else
    return NULL;
  
}

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

/* LookFor_IncluderITCL
 * Look for a continuation with the same label and cset label included
 * in the cset_labels of an itcl.
 * There can be several candidates.
 * NULL if <label> does not belong to itcl.
 */
PITContTyp LookFor_IncluderITCL( itcl, itc )
     ITContListTyp itcl;
     PITContTyp    itc;
{
  PITContTyp pit;
  ListTyp    csl;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( EqualLabel( pit->label, itc->label ) ){
      if ( itc->cset_labels==NULL )
	return pit;
      for ( csl=pit->cset_labels; csl!=NULL; csl=Next_list(csl) )
	if ( SubSet_LL( (ListTyp)LookInfo_list(itc->cset_labels),
		       (ListTyp)LookInfo_list(csl)) )
	  return pit;
      
    }
  }
  return NULL;
}


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

/* LookFor_IdenticalITCL
 *  Look for a continuation with the same label and cset labels in an itcl.
 *  NULL if <label> does not belong to itcl.
 */
PITContTyp LookFor_IdenticalITCL( itcl, itc )
     ITContListTyp itcl;
     PITContTyp    itc;
{
  PITContTyp pit;
  boolean    dup;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( EqualLabel( pit->label, itc->label ) ){
      dup = Equal_list( itc->cset_labels, pit->cset_labels, Equal_LL );
      if (dup)
	return pit;
    }
  }
  return NULL;
}

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

/* LookFor_Update_IdenticalITCL
 * Look for a continuation with the same label and cset labels in an itcl.
 * return NULL if <label> does not belong to itcl.
 * if found then
 *  if its cset labels is already registered in the duplicated
 *    return the duplicate pit
 *  else
 *    return NULL
 */
PITContTyp LookFor_Update_IdenticalITCL( itcl, itc )
     ITContListTyp itcl;
     PITContTyp    itc;
{
  PITContTyp pit;
  ListTyp    csl;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( EqualLabel( pit->label, itc->label ) ){
      break;
    }
  }
  if (itcl!=NULL){
    if ( itc->cset_labels==NULL )
      return pit;
    for ( csl=pit->cset_labels; csl!=NULL; csl=Next_list(csl) )
      if ( Equal_LL( (ListTyp)LookInfo_list(csl),
		    (ListTyp)LookInfo_list(itc->cset_labels) ) )
	return pit;
    
    pit->cset_labels = Join_list( pit->cset_labels,
				 Copy_list(itc->cset_labels,
					   (DataListTyp(*)())Copy_LL) );
  }
  return NULL;
}

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

/* LookFor_Update_IncluderITCL
 * Look for a continuation with the same label and cset labels in an itcl.
 * return NULL if <label> does not belong to itcl.
 * if found then
 *  if its cset labels is already registered in a subset of the duplicated
 *    return the duplicate pit
 *  else
 *    return NULL
 */
PITContTyp LookFor_Update_IncluderITCL( itcl, itc )
     ITContListTyp itcl;
     PITContTyp    itc;
{
  PITContTyp pit;
  ListTyp    csl;
  
  for ( ; itcl !=NULL; itcl=itcl->next ){
    pit = (PITContTyp) LookInfo_list( itcl );
    if ( EqualLabel( pit->label, itc->label ) ){
      break;
    }
  }
  if (itcl!=NULL){
    if ( itc->cset_labels==NULL )
      return pit;
    for ( csl=pit->cset_labels; csl!=NULL; csl=Next_list(csl) )
      if ( SubSet_LL( (ListTyp)LookInfo_list(itc->cset_labels),
		     (ListTyp)LookInfo_list(csl)) )
	return pit;
    
    pit->cset_labels = Join_list( pit->cset_labels,
				 Copy_list(itc->cset_labels,
					   (DataListTyp(*)())Copy_LL) );
  }
  return NULL;
}

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

static ListTyp ll;

/* CSetLbls
 * CSets_Labels auxiliary function
 */
static void CSetLbls( b )
     BehTyp b;
{
  BehTyp        bi;
  int           i,n;
  PAttrTyp      itcla;
  ITContListTyp itcl;
  PITContTyp    itc;
  
  
  while ( b!=NULL )
    switch ( LookTypeB(b) )
      {
      case InterleavedC:  /* odd case */
        b = NULL;
        break;
	
      case DisablingC:
      case ParallelC:
        CSetLbls( LookArgB(b,1) );
        b  = LookArgB(b,2);
        break;
        
      case AlternativeC:
        for ( n=NumArgB(b),i=1; i<=n; i++ ) {
          bi = LookArgB(b,i);
	  /*
	   * if ( LookTypeB(bi)==TerminationC )
	   */
	  CSetLbls(bi);
        }
        b = NULL;
        break;
        
      case ContSetC:
        if ( (itcla=LookA(b,ITCLA))!=NULL ) {
          itcl = (ITContListTyp)LookAInfo(itcla);
          for ( ; itcl!=NULL; itcl=Next_list(itcl) ) {
            itc = (PITContTyp)LookInfo_list(itcl);
            ll  = Insert_list( (DataListTyp)CopyLabel(itc->label), ll );
	    /*
	     * CSetLbls(itc->b);
	     * s57.lot fails. I don't know exactly why.
	     *
             * discuss
	     *
	     */
          }
        }
        b = NULL;
        break;
	
      case ChoiceC:
      case GuardC:
      case GateC:
      case IC:
      case ExitC: 
      case StopC:
        b = LookArgB(b,1);  
        break;
        
      case EnablingC:
      case RelabellingC:
      case HidingC:
      case PletC:
      case LetC:
      case ProcessInstC:
      case GateChoiceC:
      case ParC:
        b = LookArgB(b,1);  
        break;
	
      default:
        Error("CSetLbls : Unexpected cell type");
      }
}

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

/* CSets_Labels_in_Beh
 *  return the list of labels of the subbehaviors of all the continuations sets
 *  of a behaviour
 */ 
ListTyp CSets_Labels_in_Beh( b )
     BehTyp b;
{
  ll = Create_list();
  CSetLbls( b );
  return ll;
}



/******************************************************************
 *                                                                 *
 *                          Paths                                  *
 *                                                                 *
 *          A path is a special label that behaves like            *
 *          an ordered set.                                        *
 *                                                                 *
 *          Example :                                              *
 *                                                                 *
 *          <3(x:s)> U < 3(x:s), 11(z:n) > = < 3(x:s), 11(z:n) >   *
 *                                                                 *
 *                                                                 *
 *                                                                 *
 *******************************************************************/


/* InsertPath
 * Append a termination into a path in a sorted and univocal way.
 * Example : InsertPath( 3, <1,3,4,9> ) = <1,3,4,9>
 */
LabelTyp InsertPath( t, label )
     BehTyp   t;
     LabelTyp label;
{
  LabelTyp n,last;
  
  if (label==NULL)
    return (LabelTyp)t;
  
  LASSERT( LookCopy(label)==0 );
  for ( n=last=label; n!=NULL; last=n, n=LookArgB(n,1) ){
    if ( LookNameB(n) == LookNameB(t) ){
      FreeB(t);
      return label;
    }
    if ( (int)LookNameB(n) > LookNameB(t) ){
      if ( last==n ){
	AddArgB(t,last);
	return t;
      }
      else{
	n = GetArgB(last,1);
	AddArgB(last,t);
	AddArgB(t,n);
	return label;
      }
    }
  }
  LASSERT( n==NULL && last!=NULL );
  AddArgB( last, t);
  return label;
  
}

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

/* JoinPath
 * Join 2 labels in a sorted way. ( label1 & label2 no longer exist ).
 * Example : JoinPath( <3,7>, <1,3,4,9> ) = <1,3,4,7,9>
 */
LabelTyp JoinPath( label1, label2 )
     LabelTyp  label1, label2;
{
  LabelTyp n;
  
  LASSERT(label1!=NULL||label2!=NULL);
  for ( n=label1; n!=NULL; n=LookArgB(n,1) ){
    label2 = InsertPath( n, label2 );
  }
  return label2;
}

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






