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

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

  Santiago Pavon Gomez

  22 January 1991

  Expansion functions

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

  SDEBUG : activate debugging mode
  BEHASHDBG : activate state tracing

  21-July-1992 David
  MAY PASS tests are aborted by default when a MAY condition is matched

  01 June 1994 Rabay

  Calls to AsapT function included
  ************************************/


/* KJT 12/02/12: Added */
#include <stdlib.h>
#include "eximmed.h"
#include "exdupbeh.h"
#include "exexpans.h"
#include "expre_br.h"
#include "babeh.h"
#include "batables.h"
#include "badefca.h"
#include "listack.h"
#include "limisc.h"
#include "listdout.h"
#include "balotosf.h"
#include "expostex.h"
#include "exrmparm.h"
#include "baprint.h"
#include "exsucces.h"
#include "itintexp.h"

/* KJT 22/01/23: added function prototypes */
void gl_cleanup();


#define BEHHASHTABSIZE 32767


/******************************************************************
 *
 *           Statistics.
 *
 *******************************************************************/


static int num_states;
static int num_trans;
static int num_dupproc;
static int num_stops;

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

static void InitStat()
{
  num_states  = 0;
  num_trans   = 0;
  num_dupproc = 0;
  num_stops   = 0;
}

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

#ifdef STATISTIC
#define EVERY_STATES 1000
#endif

static void PrintStat()
{
#ifdef STATISTIC
  if ( num_states%EVERY_STATES==0 ){
#endif
    printMsgs(  "    Analysed states       = ");
    PrintInt(printMsgs,num_states);
    printMsgs("\n    Generated transitions = ");
    PrintInt(printMsgs,num_trans);
    printMsgs("\n    Duplicated states     = ");
    PrintInt(printMsgs,num_dupproc);
    printMsgs("\n    Deadlocks             = ");
    PrintInt(printMsgs,num_stops);
    printMsgs("\n\n");
#ifdef STATISTIC
    PrintUsageMemoTime();
  }
#endif
}


/******************************************************************
 *
 *               Expand one level
 *
 *******************************************************************/


static BehTyp alt_processing ( here )
     BehTyp here;
{
  BehTyp  t1 , t2 , t3 , t4 ;

  t1 = here;
  while ( t1 != NULL ) {
    t3 = LookActionUB( t1 );
    if ( (LookTypeB(t3)==GateC) || (LookTypeB(t3)==IC) ) {
      t2 = MakeB( 1, BehaviourC );
      PutCopy( t2, 1 );
      t4 = LookB1( t3 );
      PutB1( t3, t2 );
      PutB2( t2, t4 );
    }
    t1 = LookB2( t1 );
  }
  return here;
}

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

static BehTyp guard_processing ( here )
     BehTyp here;
{
  BehTyp  t1 , t2 , t3;

  t2 = LookActionUB( here );
  if ( (LookTypeB(t2)==GateC) || (LookTypeB(t2)==IC) ) {
    t1 = MakeB( 1, BehaviourC );
    PutCopy( t1, 1 );
    t3 = LookB1( t2 );
    PutB2( t1, t3 );
    PutB1( t2, t1 );
  }
  return here;
}

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

static BehTyp gate_processing ( here )
     BehTyp here;
{
  BehTyp  t2;

  t2 = MakeB( 1, BehaviourC );
  PutCopy( t2, 1 );
  PutB2( t2, LookB1(here) );
  PutB1( here, t2 );
  return here;
}

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

static BehTyp i_processing( here )
     BehTyp here;
{
  BehTyp  t2;

  t2 = MakeB( 1, BehaviourC );
  PutCopy( t2, 1 );
  PutB2( t2, LookB1(here) );
  PutB1( here, t2 );
  return here;
}

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

static BehTyp sum_processing( here )
     BehTyp here;
{
  BehTyp  t1 , t2 , t3;

  t2 = LookActionUB(here);
  if ( (LookTypeB(t2)==GateC) || (LookTypeB(t2)==IC) ) {
    t1 = MakeB( 1, BehaviourC );
    PutCopy( t1, 1 );
    t3 = LookB1( t2 );
    PutB2( t1, t3 );
    PutB1( t2, t1 );
  }
  return here;
}

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

/* ExpanOneLevel
 *
 */
static void ExpanOneLevel( here )
     BehTyp here;
{
  BehTyp the_copy;


  if ( LookNameB(here)==-1 )
    the_copy = GetUntilActB(GetArgB( here, 2 ));
  else
    the_copy = CopyUntilActB( LookB2(here) );
  switch ( LookTypeB(the_copy) )
    {
    case AlternativeC:
      the_copy = alt_processing( the_copy );
      break;

    case GuardC:
      the_copy = guard_processing( the_copy );
      break;

    case GateC:
      the_copy = gate_processing( the_copy );
      break;

    case IC:
      the_copy = i_processing( the_copy );
      break;

    case ChoiceC:
      the_copy = sum_processing( the_copy );
      break;

    case ExitC:
    case StopC:
      break;

    default:
      Error("Expan_one_level: Unexpected cell type.");
    }

  PutArgB( here , the_copy, 1 );

}


/* ExpanOneLevel_2
 *
 */
static void ExpanOneLevel_2( here )
     BehTyp here;
{
  BehTyp the_copy;

  the_copy = GetArgB( here, 2 );
  switch ( LookTypeB(the_copy) )
    {
    case AlternativeC:
      the_copy = alt_processing( the_copy );
      break;

    case GuardC:
      the_copy = guard_processing( the_copy );
      break;

    case GateC:
      the_copy = gate_processing( the_copy );
      break;

    case IC:
      the_copy = i_processing( the_copy );
      break;

    case ChoiceC:
      the_copy = sum_processing( the_copy );
      break;

    case ExitC:
    case StopC:
      break;

    default:
      Error("Expan_one_level_2: Unexpected cell type.");
    }
  PutArgB( here , the_copy, 1 );
}


/******************************************************************
 *
 *      VERBOSE MODE
 *
 *******************************************************************/

/* depth level */
#define DATLIN     5

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

static boolean verbose_mode;

static int  contdepth, contactdepth, verbose_level;

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

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


/******************************************************************
 *
 *      EXPAND - VAR EXPAND - FREE EXPAND
 *
 *******************************************************************/

static StackTyp pathStack, depthStack, varStack;

/* counter for the duplicated behaviours. */
static int num_produp = 0;


/* wactd123
 * prints current depth.
 */
static void wactd123(a_depth)
     int a_depth;
{
  char buff[50];

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

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

/* is_leaf123
 * says if a behaviour is a leaf according to the depth and depth limit
 */
static boolean is_leaf123( h1, the_depth, pa_depth )
     BehTyp  h1;
     int     the_depth,*pa_depth;
{
  BehTyp aux;

  if ( LookTypeB(h1)==ProcessInstC )
    return TRUE;
  else {
    aux = LookActionUB( h1 );
    if ( (LookTypeB(aux)==StopC) || (LookTypeB(aux)==ExitC) )
      return TRUE;
    else if ( the_depth==(*pa_depth)+1 ) {
      *pa_depth = *pa_depth + 1;

      if (!IS_DUPLICATE_EXP) {
	aux = LookArgB(aux,1);
	if (LookTypeB(aux)==BehaviourC)
	  GlueArgB( aux , 2 );
      }

      return TRUE;
    }
    else
      return FALSE;
  }
}

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

/* after_leaf123
 *
 */
static BehTyp after_leaf123( pa_depth )
     int *pa_depth;
{
  BehTyp pre_ord;
  char buff[15];

  if ( IsEmpty_Stack(pathStack) ) {
    *pa_depth = 0;
    if (verbose_mode) {
      if (runtimeConfig==TextMode) {
	printMsgs(".\n\n");
      }
      else {
	printPos(".\n\n",-1);
	flushTarget();
      }
    }
    return NULL;
  }
  else {
    pre_ord = (BehTyp) Look_Stack( pathStack );
    while ( (IsEmpty_Stack(pathStack)==FALSE) && (LookB2(pre_ord)==NULL) ){
      (void)Get_Stack( &pathStack );
      (void)Get_Stack( &depthStack );
      if ( IsEmpty_Stack(pathStack)==FALSE ) {
	pre_ord = (BehTyp) Look_Stack( pathStack );
	*pa_depth = (int) Look_Stack( depthStack );
      }
    }
    if ( IsEmpty_Stack(pathStack)==TRUE ) {
      *pa_depth = 0;
      if (verbose_mode) {
	if (runtimeConfig==TextMode) {
	  printMsgs(".\n\n");
	}
	else {
	  printPos(".\n\n",-1);
	  flushTarget();
	}
      }
      return NULL;
    }
    else {
      (void)Get_Stack( &pathStack );
      pre_ord = LookB2( pre_ord );
      pathStack = Save_Stack( (DataStackTyp)pre_ord, pathStack );
      *pa_depth = (int) Look_Stack( depthStack );
      if (verbose_mode) {
	(void)sprintf(buff,"%5d", *pa_depth );
	if (runtimeConfig==TextMode) {
	  printMsgs(buff);
	}
	else {
	  printPos(buff,-1);
	  flushTarget();
	}
      }
      return LookActionUB( pre_ord );
    }
  }
}

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

/* next_wia_123
 *
 */
BehTyp next_wia_123 ( here, the_depth, pa_depth )
     BehTyp here;
     int the_depth, *pa_depth;
{
  char buff[50];

  while ( (here!=NULL) && is_leaf123(here,the_depth,pa_depth) ) {
    if (verbose_mode) {
      if (contdepth==DATLIN) {
	(void)sprintf(buff,"-%5d/ |%8d|%8d\n",*pa_depth,num_trans,num_states);
	if (runtimeConfig==TextMode) {
	  printMsgs(buff);
	}
	else {
	  printPos(buff,-1);
	  flushTarget();
	}
	contdepth = 1;
      }
      else {
	(void)sprintf(buff,"-%5d/",*pa_depth);
	if (runtimeConfig==TextMode) {
	  printMsgs(buff);
	}
	else {
	  printPos(buff,-1);
	  flushTarget();
	}
	contdepth = contdepth + 1;
      }
      contactdepth = 1;
    }
    here = after_leaf123( pa_depth );
  }
  if ( here!=NULL ) {
    while ( LookTypeB(here)!=BehaviourC )
      here = LookB1( here );
    *pa_depth = *pa_depth +1;
  }
  if (verbose_mode) {
    wactd123( *pa_depth );
  }
  return here;
}

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

/* expand_free
 * return the free expansion of the_beh until the_depth
 */
BehTyp expand_free( the_beh, the_depth, i_remove, wbcontext )
     BehTyp  the_beh;
     int     the_depth;
     boolean i_remove, wbcontext;
{
  BehTyp        where_i_am;
  int           a_depth;
  int           i_depth, i_rm_depth, *i_rm_depthPt, cero=0;
  char buff[15];

  if ( the_depth != 0 ) {
    InitStat();
    if (verbose_mode) {
      (void)sprintf(buff,"%5d",0);
      if (runtimeConfig==TextMode) {
	printMsgs(buff);
      }
      else {
	printPos(buff,-1);
	flushTarget();
      }
      contdepth    = 1;
      contactdepth = 1;
    }
    if ( i_remove ) {
      expansion_flags = SHARED_EXP | WEAK_EQUIV_EXP;
      i_depth         = MAXDEPTH_I_RMV;
    }
    else {
      expansion_flags = SHARED_EXP;
      i_depth         = 0;
    }
    pathStack  = Create_Stack();
    depthStack = Create_Stack();
    where_i_am = MakeB(0,BehaviourC);
    PutArgB( where_i_am, the_beh, 2 );
    the_beh = where_i_am;
    a_depth = 0;
    while ( where_i_am != NULL ) {
      num_states += 1;
#ifdef STATISTIC
      PrintStat();
#endif
      /*
	 pba = GetArgB( where_i_am, 2 );
	 pba = Pre_Branch( pba, &i_rm_depth );
	 PutArgB( where_i_am, pba, 2 );
	 */
      i_rm_depth   = i_depth;
      i_rm_depthPt = (!wbcontext && num_states==1) ? &cero: &i_rm_depth;
      Pre_Branch_2( LookArgB(where_i_am,2), i_rm_depthPt );

#ifdef TIME
#ifdef ASAP
     (void) AsapT( LookArgB(where_i_am,2));
#endif
#endif
      PutNameB( where_i_am , -1 );
      ExpanOneLevel_2( where_i_am );
      GlueCellB1( where_i_am );
      num_trans += NumArgB( where_i_am );
      if ( LookTypeB(where_i_am)==StopC )
	num_stops++;
      if ( LookTypeB(where_i_am)==ExitC )
	num_trans++;
      if ( LookTypeB(where_i_am)==AlternativeC ) {
	pathStack = Save_Stack( (DataStackTyp)where_i_am, pathStack );
	depthStack = Save_Stack( (DataStackTyp)a_depth, depthStack );
      }
      where_i_am = next_wia_123( where_i_am, the_depth, &a_depth );
    }
    Free_Stack( pathStack, (void(*)())NULL );
    Free_Stack( depthStack, (void(*)())NULL );
    /*    ClearBeh( the_beh ); */
    /* rm_alt_stop(the_beh); */
    /* DupProcTab_Func( last_proc+1 );*/
    /* for relabel to process */
  }
  return the_beh;
}

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

/* NameDupProc
 * returns a new name for a new duplicated process.
 */
char * NameDupProc()
{
  char * s;

  s = (char*)emalloc(18);
  do {
    (void)sprintf(s,"duplicate%d",num_produp);
    LASSERT(strlen(s)<18);
    num_produp++;
  }
  while ( FindP(s)!=0 );
  return s;
}

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

/* IsLoopBehDef
 * says if BehaviourC here is reached from eq_here
 * travelling only through alternatives, processes and behaviour cells.
 */
static boolean IsLoopBehDef( here , eq_here )
     BehTyp here,eq_here;
{
  boolean    result;
  BehTyp  mark;

  result = FALSE;
  mark   = eq_here;
  switch (LookTypeB(mark))
    { case ProcessInstC:
      case ProcessDefC:
	result = IsLoopBehDef( here, LookB1(mark) );
	break;
      case BehaviourC :
	if ( mark == here )
	  result = TRUE;
	else
	  if ( LookB1(mark)!=NULL )
	    result = IsLoopBehDef( here, LookB1(mark) );
	break;
      case AlternativeC :
	while ( (mark!=NULL) && (result==FALSE) ) {
	  result = IsLoopBehDef( here, LookB1(mark) );
	  mark = LookB2( mark );
	}
	break;
      }
  return result;
}

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

/* link_beh
 * Takes a BehDef (here) and its duplicated BehDef (eq_here).
 * If they only differ in alternatives, processes and behaviour cells,
 * then a stop behaviour is returned
 * else a duplicated process.
 */
/* KJT 22/01/23: added "int" type */
static int link_beh( here, eq_here, pdbl )
     BehTyp here, eq_here;
     PDupBehListsTyp pdbl;
{
  BehTyp aux, t0, t1 , t2 ;
  DescriptorTyp name;
  GateSetTyp gs;
  GateListTyp gl;
  PAttrTyp gla;

  /*
     if ( IsLoopBehDef(here,eq_here) ) {
     aux = MakeB( 0, StopC );
     GlueB( here, aux );
     }
     else
     */
  LASSERT( ! IsLoopBehDef(here,eq_here) );
  {
    t1 = LookB1( eq_here );
    if ( LookTypeB(t1) != ProcessInstC ) {
      name = Declare_proc( NameDupProc(), (BehTyp)NULL, NOTCALCULATEDF );
      t2 = MakeB( name, ProcessInstC );
      PutB1( eq_here, t2 );
      t2 = ShareB( t2 );
      t0 = MakeB( name, ProcessDefC );
      PutP_def( name, t0 );
      PutB1( t2, ShareB(t0) );
      PutB1( t0, t1 );
      gs = GetGates( LookB2(eq_here) );
      if ( !IsEmptyGS(gs) ) {
	gl  = GateSet_to_GateList( gs );
	gla = MakeA( (AttrValueTyp)gl, GLA );
	PutA( t2, gla );
	PutA( t0, gla );
      }
      FreeGS( gs );
      if ( pdbl->DupBehForVL != NULL ) {
	PutA( t0, MakeA( (AttrValueTyp)(pdbl->DupBehForVL),ELA) );
	PutA( t2, MakeA( (AttrValueTyp)(pdbl->DupBehActEL2),ELA) );
      }
    }
    else {
      t2 = t1;
      name = LookNameB( t2 );
      FreeEL( pdbl->DupBehForVL );
      FreeEL( pdbl->DupBehActEL2 );
    }
    aux = MakeB( name, ProcessInstC );
    GlueB( here, aux );
    gla = LookA( t2, GLA );
    if ( gla!=NULL )
      PutA( here, gla );
    if ( pdbl->DupBehActEL1 != NULL )
      PutA( here, MakeA( (AttrValueTyp)(pdbl->DupBehActEL1), ELA ) );
  }
}

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

/* expand_exp
 * return the expansion of the_beh until the_depth with duplicated beheviour
 * detection.
 */
BehTyp expand_exp( the_beh, the_depth, i_remove, wbcontext )
     BehTyp  the_beh;
     int     the_depth;
     boolean i_remove, wbcontext;
{
  BehTyp         where_i_am, dupb, b2;
  int            a_depth;
  DupBehListsTyp dbl;
  DescriptorTyp  last_proc;
  int            i_depth, i_rm_depth, *i_rm_depthPt, cero=0;
  char           buff[15];
  BehHashTabTyp  bhtd;

  if ( the_depth != 0 ) {
    InitStat();
    if (verbose_mode) {
      (void)sprintf(buff,"%5d",0);
      if (runtimeConfig==TextMode) {
	printMsgs(buff);
      }
      else {
	printPos(buff,-1);
	flushTarget();
      }
      contdepth      = 1;
      contactdepth   = 1;
    }
    if ( i_remove ) {
      expansion_flags = DUPLICATE_EXP | WEAK_EQUIV_EXP;
      i_depth = MAXDEPTH_I_RMV;
    }
    else {
      expansion_flags = DUPLICATE_EXP;
      i_depth = 0;
    }
    last_proc      = LastTableP();
    bhtd           = InitHashBehDef(BEHHASHTABSIZE,FALSE);
    pathStack  = Create_Stack();
    depthStack = Create_Stack();
    where_i_am = MakeB(0,BehaviourC);
    PutArgB( where_i_am, the_beh, 2 );
    the_beh = where_i_am;
    a_depth = 0;

    while ( where_i_am != NULL ) {
      i_rm_depth   = i_depth;
      i_rm_depthPt = (!wbcontext && num_states==1) ? &cero: &i_rm_depth;
      b2 = Pre_Branch( GetArgB(where_i_am,2), i_rm_depthPt );
#ifdef TIME
#ifdef ASAP
      b2 = AsapT(b2);
#endif
#endif
      PutArgB( where_i_am, b2, 2 );

      if ( LookTypeB(LookArgB(where_i_am,2))==StopC )
	dupb = NULL;
      else
	dupb = GetHashBehDef( bhtd, where_i_am, &dbl );
      if ( dupb!=NULL ) {

#ifdef BEHASHDBG
	(void)printf("\n--------- duplicated state %d -------- # node %d\n",
		     LookNameB(where_i_am), num_states );
	printMsgs("lista 1:  ");
	PrintEL(dbl.DupBehActEL1,printMsgs);

	printMsgs("\nlista 2:  ");
	PrintEL(dbl.DupBehActEL2,printMsgs);
	printMsgs("\n\n");
	PBeh( LookArgB(where_i_am,2) );
#endif

	num_dupproc += 1;
	link_beh( where_i_am, dupb, &dbl );
      }
      else {
	num_states += 1;
#ifdef STATISTIC
      PrintStat();
#endif
#ifdef BEHASHDBG
	(void)printf("\n--------- state %d -------- # node %d\n",
		     LookNameB(where_i_am), num_states );
	PBeh( LookArgB(where_i_am,2) );
#endif
	ExpanOneLevel( where_i_am );
	where_i_am = LookB1( where_i_am );
	num_trans += NumArgB( where_i_am );
	if ( LookTypeB(where_i_am)==StopC )
	  num_stops++;
	if ( LookTypeB(where_i_am)==ExitC )
	  num_trans++;
	if ( LookTypeB(where_i_am)==AlternativeC ) {
	  pathStack = Save_Stack( (DataStackTyp)where_i_am, pathStack );
	  depthStack = Save_Stack( (DataStackTyp)a_depth, depthStack );
	}
      }
      where_i_am = next_wia_123( where_i_am, the_depth, &a_depth );
    }

    /*   (void)printf("\n\n");
	 PrintHashBehDef(bhtd); */
#ifdef SDEBUG
    StatHashBehDef(bhtd);
    printMsgs("\n");
#endif
    FreeHashBehDef(bhtd);
    PrintStat();
    Free_Stack( pathStack, (void(*)())NULL );
    Free_Stack( depthStack, (void(*)())NULL );
    ClearBeh( the_beh );
    DupProcTab_Func( last_proc+1 );
    RmParameters( the_beh, last_proc+1 );
  }
  return the_beh;
}

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

/* expand_var
 * return the parameterized expansion of the_beh until the_depth
 */
BehTyp expand_var( the_beh, the_depth, i_remove, wbcontext )
     BehTyp  the_beh;
     int     the_depth;
     boolean i_remove, wbcontext;
{
  BehTyp         where_i_am, dupb, b2;
  int            a_depth;
  DupBehListsTyp dbl;
  DescriptorTyp  last_proc;
  int            i_depth, i_rm_depth, *i_rm_depthPt, cero=0;
  char           buff[15];
  BehHashTabTyp  bhtd;

  if (the_depth != 0 ) {
    InitStat();
    if (verbose_mode) {
      (void)sprintf(buff,"%5d",0);
      if (runtimeConfig==TextMode) {
	printMsgs(buff);
      }
      else {
	printPos(buff,-1);
	flushTarget();
      }
      contdepth      = 1;
      contactdepth   = 1;
    }
    if ( i_remove ) {
      expansion_flags = DUPLICATE_EXP | PARAMETERIZED_EXP | WEAK_EQUIV_EXP;
      i_depth         = MAXDEPTH_I_RMV;
    }
    else {
      expansion_flags = DUPLICATE_EXP | PARAMETERIZED_EXP;
      i_depth         = 0;
    }
    last_proc  = LastTableP();
    bhtd       = InitHashBehDef(BEHHASHTABSIZE,FALSE);
    pathStack  = Create_Stack();
    depthStack = Create_Stack();
    where_i_am = MakeB( 0, BehaviourC );
    PutArgB( where_i_am, the_beh, 2 );
    the_beh = where_i_am;
    a_depth = 0;

    while ( where_i_am != NULL ) {
      i_rm_depth   = i_depth;
      i_rm_depthPt = (!wbcontext && num_states==1) ? &cero: &i_rm_depth;
      b2 = Pre_Branch( GetArgB(where_i_am,2), i_rm_depthPt );

#ifdef TIME
#ifdef ASAP
      b2 = AsapT(b2);
#endif
#endif
     PutArgB( where_i_am, b2, 2 );

      if ( LookTypeB(LookArgB(where_i_am,2)) == StopC )
	dupb = NULL;
      else
	dupb = GetHashBehDef( bhtd, where_i_am, &dbl );
      if (dupb!=NULL) {
#ifdef BEHASHDBG
	(void)printf("\n--------- duplicated state %d -------- # node %d\n",
		     LookNameB(where_i_am), num_states );
	PBeh( LookArgB(where_i_am,2) );
#endif
	/*
	   printMsgs("\n list 1: \n\n");
	   DrawEL(dbl.DupBehActEL1,printMsgs);

	   printMsgs("\n list 2: \n\n");
	   DrawEL(dbl.DupBehActEL2,printMsgs);
	   */
	num_dupproc += 1;
	link_beh( where_i_am, dupb, &dbl );
      }
      else {
	num_states += 1;
#ifdef STATISTIC
      PrintStat();
#endif
#ifdef BEHASHDBG
	(void)printf("\n--------- state %d -------- # node %d\n",
		     LookNameB(where_i_am), num_states );
	PBeh( LookArgB(where_i_am,2) );
#endif
	ExpanOneLevel( where_i_am );
	where_i_am = LookB1( where_i_am );
	num_trans += NumArgB( where_i_am );
	if ( LookTypeB(where_i_am)==StopC )
	  num_stops++;
	if ( LookTypeB(where_i_am)==ExitC )
	  num_trans++;
	if ( LookTypeB(where_i_am)==AlternativeC ) {
	  pathStack = Save_Stack( (DataStackTyp)where_i_am, pathStack );
	  depthStack = Save_Stack( (DataStackTyp)a_depth, depthStack );
	}
      }
      where_i_am = next_wia_123( where_i_am, the_depth, &a_depth );
    }

    /*   printMsgs(void)("\n\n");
	 PrintHashBehDef(bhtd); */
#ifdef SDEBUG
    StatHashBehDef(bhtd);
    printMsgs("\n");
#endif
    FreeHashBehDef(bhtd);
    PrintStat();
    Free_Stack( pathStack,(void(*)())NULL );
    Free_Stack( depthStack,(void(*)())NULL );
    /*
       PrintBeh(the_beh ,-1,ALL_PROC,FALSE,"2  ",printTarget,FALSE,FALSE);
       */
    PClearBeh( the_beh, last_proc );
    DupProcTab_Func( last_proc+1 );
    RmParameters( the_beh, last_proc+1 );
  }
  return the_beh;
}

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

static ExprListTyp newvl;

/* Instantiate
 * return an instantiation of process definition b with new variables.
 * leave in newvl a copy the new variable list.
 */
static BehTyp Instantiate(b)
     BehTyp b;
{
  BehTyp      inst;
  ExprTyp     e;
  ExprListTyp vl;
  PAttrTyp    a;

  inst  = MakeB( LookNameB(b), ProcessInstC );
  if ( (a=LookA( b, GLA ))!=NULL )
    PutA( inst, a );
  vl = (ExprListTyp)LookAInfo(LookA(b,ELA));
  if ( vl!=NULL ) {
    newvl = CreateEL();
    for ( ; vl!=NULL; vl=Next_list(vl) ) {
      e = MakeE( EqualV_entry(LookNameE((ExprTyp)LookInfo_list(vl))),
		VariableC );
      newvl = AddEL( e, newvl );
    }
    PutA( inst, MakeA( (AttrValueTyp)newvl, ELA ) );
    newvl = CopyEL( newvl );
  }

  return inst;
}

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

/* FreeExpand
 * Free expansion of b until depth d.
 */
void FreeExpand( b, d, verbose, i_remove, wbcontext )
     BehTyp b;
     int    d;
     boolean verbose, i_remove, wbcontext;
{
  BehTyp aux;

  verbose_mode = verbose;
  Header();
  if ( (LookTypeB(b)==ProcessDefC) || (LookTypeB(b)==SpecificationC) )
    b = LookArgB( b, 1 );
  aux = expand_free( b, d, i_remove, wbcontext );
  GlueB( b, aux );
  PrintStat();
}

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

/* StepExpand
 * Free expansion of b of depth 1.
 * debug_info is TRUE if debugging information is computed.
 */
BehTyp StepExpand( b, debug_info )
     BehTyp  b;
     boolean debug_info;
{
  int d;
  BehTyp res;

  LASSERT((LookTypeB(b)!=ProcessDefC) & (LookTypeB(b)!=SpecificationC));
  if ( debug_info )
    expansion_flags = STEP_EXP;
  else
    expansion_flags = 0;
  d = 0;
  res = Pre_Branch(b,&d);
  return res;
}

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

/* Expand
 * Expansion of b until depth d.
 */
void Expand( b, d, verbose, i_remove, wbcontext )
     BehTyp  b;
     int     d;
     boolean verbose, i_remove, wbcontext;
{
  BehTyp   aux, beh, inst;
  PAttrTyp a;

  verbose_mode = verbose;
  Header();
  if ( d!=0 && LookTypeB(b)==ProcessDefC ) {
    inst   = Instantiate( b );
    aux    = expand_exp( inst, d, i_remove, wbcontext );
    beh    = GetArgB( b, 1 );
    FreeB( beh );
    AddArgB( b, aux );
    if ( (a=LookA(b,ELA))!=NULL ) {
      FreeEL( (ExprListTyp)GetAInfo(a) );
      PutAInfo( a, (AttrValueTyp)newvl );
    }
  }
  else {
    if ( LookTypeB(b)==SpecificationC )
      b = LookArgB( b, 1 );
    aux = expand_exp( b, d, i_remove, wbcontext );
    GlueB( b, aux );
  }
}

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

/* VarExpand
 * Parameterized Expansion of b until depth d.
 */
void VarExpand( b, d, verbose, i_remove, wbcontext )
     BehTyp b;
     int       d;
     boolean verbose, i_remove, wbcontext;
{
  BehTyp   aux, beh, inst;
  PAttrTyp a;

  verbose_mode = verbose;
  Header();
  if ( d!=0 && LookTypeB(b)==ProcessDefC ) {
    inst   = Instantiate( b );
    aux    = expand_var( inst, d, i_remove, wbcontext );
    beh    = GetArgB( b, 1 );
    FreeB( beh );
    AddArgB( b, aux );
    if ( (a=LookA(b,ELA))!=NULL ) {
      FreeEL( (ExprListTyp)GetAInfo(a) );
      PutAInfo( a, (AttrValueTyp)newvl );
    }
  }
  else {
    if ( LookTypeB(b)==SpecificationC )
      b = LookArgB( b, 1 );
    aux = expand_var( b, d, i_remove, wbcontext );
    GlueB( b, aux );
  }
}


/******************************************************************
 *
 *             TEST EXPANSION
 *
 *******************************************************************/


/* test expansion : options, number of terminations, success event*/
static boolean optiona, options, optione, optiond, optionx, optiont;
static int termd, terma, terme, terms;
static DescriptorTyp sevent, test_proc;

#define UnsuccessfulTerms ((termd!=0)||(terms!=0)||(terme!=0))

/*
 * True if the current test is going to be MAY and there were no
 * debug options (-asde) in the command line.
 */
#define IsMay() ( (terma!=0) && UnsuccessfulTerms )


/* nonSolvedPred
 * This variable indicates if the test process is valid or not.
 * A test is not valid when there are guard or selection predicates
 * unresolved.
 */
static boolean nonSolvedPred;


/* CheckNonSolvedPred
 * Checks if the immediate behaviour b has unresolved guards or
 * selection predicates.
 * It sets the variable nonSolvedPred.
 */
static void CheckNonSolvedPred( b )
     BehTyp b;
{
  int i,n;
  BehTyp b1;

  if (nonSolvedPred == TRUE)
    return;
  n = NumArgB(b);
  for ( i=1; i<=n; i++ ) {
    b1 = LookPreActionUB( LookArgIB(b,i) );
    if ( (b1!=NULL) && (LookTypeB(b1)==GuardC) ) {
      nonSolvedPred = TRUE;
      return;
    }
    b1 =  LookActionArgIB( b, i );
    if ( (LookTypeB(b1)==GateC) && (LookA(b1,PA)!=NULL) ) {
      nonSolvedPred = TRUE;
      return;
    }
  }
}

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

/* IsSuccess
 * Returns TRUE if the behaviour b is the success event.
 */
static boolean IsSuccess( b )
     BehTyp b;
{
  LASSERT(b!=NULL);
  return  ((LookTypeB(b)==GateC) && (LookNameB(b)==sevent));
}

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

/* RmIfSuccess
 * Check if the immediate behaviour b can offer the success event.
 * If it is offered then all the other actions in alternative are removed.
 */
static BehTyp RmIfSuccess( b, is_success )
     BehTyp   b;
     boolean *is_success;
{
  BehTyp  ub, nb;
  boolean cont;
  int     n,i;

  *is_success = FALSE;
  if ( LookTypeB(b) == AlternativeC ) {
    cont = TRUE;
    n    = NumArgIB(b);
    i    = 1;
    while ( (i<=n) && cont ) {
      ub = LookArgIB( b, i );
      cont = ! IsSuccess( LookActionUB(ub) );
      i++;
    }
    if ( !cont ) {
      *is_success = TRUE;
      nb = NULL;
      for ( i=1 ; i<=n ; i++ ) {
	ub = GetArgIB( b, i );
	if ( IsSuccess(LookActionUB(ub)) )
	  nb = AppendUB( nb, ub );
	else
	  FreeB( ub );
      }
      FreeB( b );
      LASSERT(nb!=NULL);
      return nb;
    }
    else
      return b;
  }
  else
    *is_success = IsSuccess(LookActionUB(b));
  return b;
}

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

static int test_response, expected_response;

/* Unexpected Test Response
 */
#define UTR() ( optionx &&\
	       ( (expected_response==MUST) && ( terme!=0 || terms!=0 || termd!=0 ) )\
	       ||\
	       ( (expected_response==REJECT) && ( terma!=0 ) )\
	       )

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

/*
 * random number generator
 */

#define MODULO 2976203
#define PROD 139

static unsigned act_seed;

/* NextSeed
 * Returns the next ramdon value.
 */
static int NextSeed()
{
  return (act_seed * PROD) % MODULO;
}

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

/*
 * Partial Test Expansion variables and functions
 *
 */

typedef struct { unsigned bit_set; } SlotTyp;

static boolean  partial_test_expansion, vevents_first;
static int      exploration_percentage, bsht_slots;
static SlotTyp *bsht;
static StackTyp hash_stack;

static void InitPartialTestExpand( percent, seed, bhsize)
     int percent, seed, bhsize;
{
  int i;

  exploration_percentage = percent;
  act_seed               = seed;
  hash_stack             = Create_Stack();
  if ( bhsize != UNDEFINED ){
    bsht_slots = bhsize*1024*(1024/WORDBYTES);
    bsht       = (SlotTyp*)emalloc(bsht_slots*WORDBYTES);
    for ( i=0; i<bsht_slots; i++ )
      bsht[i].bit_set = (unsigned)NULL;
  }
  else {
    bsht       = (SlotTyp*)NULL;
    bsht_slots = 0;
  }
}

static void EndPartialTestExpand()
{
  if ( bsht != NULL ){
    (void)free((char*)bsht);
    bsht =  (SlotTyp*)NULL;
    LASSERT(hash_stack==NULL);
    Free_Stack( hash_stack, (void(*)())NULL );
  }
}


/* SelectTransitions
 * Selection of some transitions from an alternative of transitions.
 * If no transitions are selected ( forced leaf ) then return TRUE
 * else return FALSE.
 *
 * It depends on the caller being careful not to feed this function with
 * successful states !
 */
static boolean SelectTransitions( b )
     BehTyp *b;
{
  BehTyp   invis;
  int      to_remove,n,ni,bit_position,hash_number;


  /* skip stops and exits */
  n = NumArgB(*b);
  if ( n==0 )
    return FALSE;

  /* bit state hashing ------- */

  if ( bsht!=NULL ){

    hash_number = BehHashKey(*b)%bsht_slots;
    hash_number = hash_number <0 ? -hash_number : hash_number;

    if ( !In_list( (DataListTyp)hash_number,
		  Stack_to_list(hash_stack), (boolean (*) ())NULL ) ){
      bit_position = ( hash_number & 03700 ) >> 6;
      LASSERT(bit_position<WORDLENGTH && bit_position>=0);
      if ( ( bsht[hash_number].bit_set & ( 01 << bit_position ) )!=(int)NULL ){
	/* busy slot */
#ifdef THASHDBG
	(void)printf("\n------ probably duplicated state %d --- # node %d\n",
		     hash_number, num_states );
	PBeh( *b );
#endif
	return TRUE;
      }
      else {
#ifdef THASHDBG
	(void)printf("\n------ new state %d --- # node %d\n",
		     hash_number, num_states );
	PBeh( *b );
#endif
	bsht[hash_number].bit_set =  bsht[hash_number].bit_set |
	  ( 01 << bit_position );
      }
    }
    hash_stack = Save_Stack( (DataStackTyp)hash_number,   hash_stack  );
  }

  /* end bit state -------- */


  /* select a percentage of transitions */

  n = NumArgIB(*b);
  if ( n>1 ){

    /* ( exploration_percentage == 0 ) => equivalent to One Expand */

    to_remove = n - (int)(( exploration_percentage*n )/100) - 1;
    if ( (exploration_percentage!=0) && exploration_percentage*n % 100 == 0 )
      to_remove++;

    if ( vevents_first ){
      invis = ExtractIB( b, IC );  /* split b into internal and visible */
      ni    = invis!=NULL ? NumArgIB(invis) : 0;
      n     = n-ni;
      if ( ni<to_remove ){ /* still necessary to remove some visible actions */
	for ( to_remove -= ni ; to_remove>0; to_remove--, n-- ){
	  act_seed = NextSeed();
	  FreeArgB( *b, (int)(act_seed%n)+1 );
	}
      }
      else {                             /* add some internal actions */
	for (  ; ni>to_remove; ni-- ){
	  act_seed = NextSeed();
	  *b = AppendUB( *b, SubtractUB( &invis, (int)(act_seed%ni)+1 ) );
	}
      }
      if ( invis!=NULL )
	FreeB(invis);
    }
    else {
      LASSERT( to_remove<n && to_remove>=0);
      for ( ; to_remove>0; to_remove--, n-- ){
	act_seed = NextSeed();
	FreeArgB( *b, (int)(act_seed%n)+1 );
      }
    }

  }
  /* end select a percentage */

  return FALSE;
}

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


/* TestResult
 * Print the result of the test expansion.
 * partial_result is TRUE when the exploration is not complete.
 */
static void TestResult( proc, partial_result )
     DescriptorTyp proc;
     boolean       partial_result;
{
  char buff[55];

  if ( proc!=(DescriptorTyp)NULL ) {
    printTarget("    Process Test = ");
    PrintP( proc,printTarget  );
  }
  if ( partial_result )
    printTarget("\n          Status = ");
  else
    printTarget("\n    Test result  = ");
  if ( (terma==0) && (terme==0) && (termd==0) && (terms==0) ){
    test_response = UNDEFINED;
    printTarget("NO ANALYSED EXECUTION.\n");
  }
  else if ( terma==0 ){
    test_response = REJECT;
    if ( partial_result )
      printTarget("ALL ANALYSED EXECUTIONS WERE REJECTED.\n");
    else
      printTarget("REJECT.\n");
  }
  else if ( (terme==0) && (termd==0) && (terms==0) ){
    test_response = MUST;
    if ( partial_result )
      printTarget("ALL ANALYSED EXECUTIONS WERE SUCCESSFUL.\n");
    else
      printTarget("MUST PASS.\n");
  }
  else {
    test_response = MAY;
    printTarget("MAY PASS.\n\n    ");
    PrintInt(printTarget,terma+terms+termd+terme);
    printTarget(" executions analysed: \n");
  }
  (void)sprintf(buff,"\n");
  printTarget(buff);
  (void)sprintf(buff,"                   successes = %1d\n",terma);
  printTarget(buff);
  (void)sprintf(buff,"                       stops = %1d\n",terms);
  printTarget(buff);
  (void)sprintf(buff,"                       exits = %1d\n",terme);
  printTarget(buff);
  (void)sprintf(buff,"               cuts by depth = %1d\n",termd);
  printTarget(buff);
  if ( nonSolvedPred==TRUE ) {
    Warning("Invalid test. There are unresolved predicates or guards.\n");
  }
  printTarget("\n");
}

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

static float iut, ist;
static long int imem;

static void InitReport()
{
  UsageMemoTime( &iut, &ist, &imem );
}

static void CurrentReport()
{
  char  buff[256];
  float ut, st;
  long int   mem;

  if ( (verbose_level>0) && num_states%verbose_level==0 ){
    printTarget("-------------------------  exploration status  ---------------------------\n\n");
    PrintStat();
    TestResult( test_proc, TRUE );
    UsageMemoTime( &ut, &st, &mem );
    (void)sprintf(buff,"\n Memory: %ld Kbytes. ", mem );
    printTarget(buff);
    (void)sprintf(buff,"CPU Time: %1.2f sec. ", ut+st );
    printTarget(buff);
#ifdef SDEBUG
    (void)sprintf(buff,"Speed: %1.2f states/sec.\n",
		  ((float)num_states)/(ut+st-iut-ist));
    printTarget(buff);
#endif
    printTarget("\n--------------------------------------------------------------------------\n");
  }
}

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

/* wactd4
 * prints current depth.
 */
static void wactd4( a_depth )
     int a_depth;
{
  wactd123( a_depth );
}

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

/* Eliminate
 * Remove the first alternative from the behaviour on top of the stack.
 */
static void Eliminate()
{
  BehTyp aux1;

  aux1 = (BehTyp)Look_Stack( pathStack );
  if ( LookB1(aux1)!=NULL )
    FreeB( GetArgB(aux1,1) );
  if ( LookTypeB(aux1)!=AlternativeC ) {
    TrfStop( aux1 );
  }
}

/*----------------------------------------------------------------*/
static BehTyp  root;
static void PrintTrace(b)
     BehTyp b;
{
  BehTyp aux;
  int pdepth = 1;

  aux = root;
  do {
    if ( LookTypeB(aux) == AlternativeC ){
      while ( LookB1(aux)==NULL )
	aux = LookB2(aux);
      aux = LookB1(aux);
    }
    /*
    pdepth = (LookTypeB(b)==GateC) && (LookNameB(b)==sevent) ? 2 : 1;
    */
    PrintBeh(aux,pdepth,NO_PROC,FALSE,"",printTarget,FALSE,FALSE);
    aux = LookActionUB(aux);
    if ( aux==b )
      break;
    aux = LookB1(aux);
  }
  while ( 1 );

  printTarget("\n");
}

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

/* is_leaf4
 * if the branch b is a leaf :
 *    update success, deadlocks, exits & cuts-by-depth counters ;
 *    if the leaf must not be preserved : free this branch;
 *    return TRUE;
 * else :
 *    return FALSE;
 */
static boolean is_leaf4( b, the_depth, pa_depth, forced_leaf )
     BehTyp  b;
     int     the_depth,*pa_depth;
     boolean forced_leaf;
{
  BehTyp aux1;

  b = LookActionUB( b );

  if ( forced_leaf ){           /* partial test expansion forced leaf */
    LASSERT( LookTypeB(b)!=StopC && LookTypeB(b)!=ExitC );
    aux1 = GetArgB( b, 1 );
    LASSERT(LookTypeB(aux1)==BehaviourC);
    PutArgB( b, GetArgB(aux1,2), 1 );
    FreeB( aux1 );
    Eliminate();
    return TRUE;
  }

  if ( LookTypeB(b) == StopC ) {
    aux1 = LookActionUB( (BehTyp)Look_Stack(pathStack) );
    if ( b!=aux1 || Count_Stack(pathStack)==1 )
      terms++;
    if ( !options && !optiont ){
      PrintTrace(b);
      Eliminate();
    }
    else
      if ( options )
	Eliminate();
  }
  else if ( (LookTypeB(b)==GateC) && (LookNameB(b)==sevent) ) {
    terma++;
    FreeB( GetArgB(b,1) );
    aux1 = MakeB( 0, StopC );
    PutArgB( b, aux1, 1 );
    if ( !optiona && !optiont ){
      PrintTrace(b);
      Eliminate();
    }
    else
      if ( optiona )
	Eliminate();
  }
  else if ( LookTypeB(b)==ExitC ) {
    terme++;
    if ( !optione && !optiont ){
      PrintTrace(b);
      Eliminate();
    }
    else
      if ( optione )
	Eliminate();
  }
  else if ( the_depth==*pa_depth ) {
    termd++;
    aux1 = GetArgB( b, 1 );
    LASSERT(LookTypeB(aux1)==BehaviourC);
    PutArgB( b, GetArgB(aux1,2), 1 );
    FreeB( aux1 );
    if ( !optiond && !optiont ){
      PrintTrace(b);
      Eliminate();
    }
    else
      if ( optiond )
	Eliminate();
  }
  else
    return FALSE;
  return TRUE;
}


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

/* AddStop
 * Goes to the first alternative found below b.
 * If all its arguments are null then
 *   the first argument of b is removed;
 *   If b is not an alternative then it becomes stop;
 * else
 *   the null arguments become stops.
 * The memory address of b is not modified.
 */
static void AddStop( b )
     BehTyp b;
{
  BehTyp aux, p0;

  p0 = LookB1(b);
  while ( (p0!=NULL) && (LookTypeB(p0)!=AlternativeC) )
    p0 = LookB1(p0);
  if ( p0!=NULL ) {
    aux = p0;
    while ( (aux!=NULL) && (LookB1(aux)==NULL) )
      aux = LookB2( aux );
    if ( aux!=NULL ) {
      aux = p0;
      while ( aux!=NULL ) {
	if ( LookB1(aux)==NULL )
	  PutArgB( aux, MakeB(0,StopC), 1 ); /**/
	aux = LookB2( aux );
      }
    }
    else                                    /* all args are null */
      if ( LookTypeB(b)==AlternativeC ) {
	FreeB( GetArgB(b,1) );
      }
      else {
	TrfStop( b );
      }
  }
}

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

static void UpdateHashStack( stack, depth )
     StackTyp *stack;
     int depth;
{
  int hsl = Count_Stack( *stack);
  while (depth<=hsl){
    hsl--;
    (void)Get_Stack( stack );
  }
}


/* after_leaf4
 * after a leaf is found, this function removes from the stack and cleans
 * the path that led to the leaf until an unexplored alternative
 * the leaf had stemed from is found.
 * returns and pushes onto the stack this new alternative to be explored,
 * preoder : left - right
 */
static BehTyp after_leaf4( pa_depth )
     int *pa_depth;
{
  BehTyp        pre_ord;
  DescriptorTyp lastVar;

  pre_ord   = (BehTyp)Get_Stack( &pathStack );
  *pa_depth =    (int)Get_Stack( &depthStack );
  lastVar   = (DescriptorTyp)Get_Stack( &varStack );
  if ( bsht!=NULL )
    UpdateHashStack( &hash_stack, *pa_depth );

  while ( (!IsEmpty_Stack(pathStack)) && (LookB2(pre_ord)==NULL) ){
    pre_ord   = (BehTyp)Get_Stack( &pathStack );
    *pa_depth = (int)   Get_Stack( &depthStack );
    lastVar   = (DescriptorTyp)Get_Stack( &varStack );
    AddStop( pre_ord );
  }
  if ( bsht!=NULL )
    UpdateHashStack( &hash_stack, *pa_depth );
  if ( IsEmpty_Stack(pathStack) ) {
    *pa_depth = 0;
    if (verbose_mode)
      if (runtimeConfig==TextMode) {
	printMsgs(".\n\n");
      }
      else {
	printPos(".\n\n",-1);
	flushTarget();
      }
    return NULL;
  }
  else {
    pre_ord    = LookB2( pre_ord );
    pathStack  = Save_Stack( (DataStackTyp)pre_ord,   pathStack  );
    depthStack = Save_Stack( (DataStackTyp)*pa_depth, depthStack );
    varStack   = Save_Stack( (DataStackTyp)lastVar,   varStack );
    if ( !optiont || (optiona && options && optiond && optione) )
      /* the variable descriptors can be re-utilized */
      ReleaseRangeTableV( lastVar );

    *pa_depth = *pa_depth + 1;
    return pre_ord;
  }
}

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

/* next_wia_4
 * Applies after_leaf4 until an effective (i.e. not leaf) alternative is found.
 * returns the next BehaviourC to be explored.
 */
BehTyp next_wia_4 ( here, the_depth, pa_depth, forced_leaf )
     BehTyp  here;
     int     the_depth, *pa_depth;
     boolean forced_leaf;
{
  char buff[50];

  if ( is_leaf4(here,the_depth,pa_depth,forced_leaf) )
    do {
      if (verbose_mode) {
	if (contdepth==DATLIN) {
	  (void)sprintf(buff,"-%5d/ |%8d|%8d\n",*pa_depth,num_trans,num_states);
	  if (runtimeConfig==TextMode) {
	    printMsgs(buff);
	  }
	  else {
	    printPos(buff,-1);
	    flushTarget();
	  }
	  contdepth = 1;
	}
	else {
	  (void)sprintf(buff,"-%5d/",*pa_depth);
	  if (runtimeConfig==TextMode) {
	    printMsgs(buff);
	  }
	  else {
	    printPos(buff,-1);
	    flushTarget();
	  }
	  contdepth = contdepth + 1;
	}
	contactdepth = 1;
      }
      here = after_leaf4(pa_depth);
      if (verbose_mode && (here!=NULL)) {
	(void)sprintf(buff,"%5d",(*pa_depth)-1);
	if (runtimeConfig==TextMode) {
	  printMsgs(buff);
	}
	else {
	  printPos(buff,-1);
	  flushTarget();
	}
      }
    } while ( (here!=NULL) && is_leaf4(here,the_depth,pa_depth,FALSE) );
  if ( here!=NULL ) {
    while ( LookTypeB(here)!=BehaviourC )
      here = LookB1( here );
  }
  if (verbose_mode) {
    wactd4( *pa_depth );
  }
  return here;
}

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

static BehTyp NullArgs_to_Stop( the_beh )
     BehTyp the_beh;
{
  BehTyp aux;

  if ( LookTypeB(the_beh)==AlternativeC )
    for( aux=the_beh; aux!=NULL; aux=LookB2(aux) )
      if ( LookB1(aux)==NULL )
	PutArgB( aux, MakeB( 0, StopC ), 1 );

  return the_beh;
}

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

static boolean force_complete_exploration;

/* expand_test
 * test expansion of the_beh until the_depth
 */
static BehTyp expand_test( the_beh, the_depth, i_remove, wbcontext )
     BehTyp  the_beh;
     int     the_depth;
     boolean i_remove,wbcontext;
{
  BehTyp  where_i_am,b2;
  int     a_depth;
  int     i_depth, i_rm_depth,*i_rm_depthPt,cero=0;
  boolean mayEsc, utrEsc, forced_leaf, is_success;
  char buff[15];

  if ( verbose_level>0 )
    InitReport();
  mayEsc      = FALSE;
  utrEsc      = FALSE;
  forced_leaf = FALSE;
  if ( i_remove ) {
    expansion_flags = WEAK_EQUIV_EXP | TEST_EQUIV_EXP;
    i_depth         = MAXDEPTH_I_RMV;
  }
  else {
    expansion_flags = 0;
    i_depth         = 0;
  }
  if ( the_depth != 0 ) {
    InitStat();
    if (verbose_mode) {
      (void)sprintf(buff,"%5d",0);
      if (runtimeConfig==TextMode) {
	printMsgs(buff);
      }
      else {
	printPos(buff,-1);
	flushTarget();
      }
      contdepth    = 1;
      contactdepth = 1;
    }
    terma = terms = terme = termd = 0;
    pathStack    = Create_Stack();
    depthStack   = Create_Stack();
    varStack     = Create_Stack();
    where_i_am   = MakeB( 0, BehaviourC );
    PutArgB( where_i_am, the_beh, 2 );
    the_beh = where_i_am;
    a_depth = 0;
    root = where_i_am;
    pathStack  = Save_Stack( (DataStackTyp)where_i_am,   pathStack );
    depthStack = Save_Stack( (DataStackTyp)a_depth,      depthStack );
    varStack   = Save_Stack( (DataStackTyp)((int)LastTableV()+1), varStack );

    while ( where_i_am != NULL &&
	   ( force_complete_exploration ||
	    (!(mayEsc=IsMay()) && !(utrEsc=UTR())) ) ) {
      num_states  += 1;
#ifdef STATISTIC
      PrintStat();
#endif
      i_rm_depth   = i_depth;
      i_rm_depthPt = (!wbcontext && num_states==1) ? &cero: &i_rm_depth;

#ifdef ASAP
      PutArgB( where_i_am,
	      AsapT(Pre_Branch(GetArgB(where_i_am,2), i_rm_depthPt)),
	      2 );
#else
      PutArgB( where_i_am,
	      Pre_Branch(GetArgB(where_i_am,2), i_rm_depthPt),
	      2 );
#endif
      /*
       * (-) CPU TIME (+) MEMORY :
       * Pre_Branch_2( LookArgB(where_i_am,2), i_rm_depthPt );
       *
       */
#ifdef BEHASHDBG
      (void)printf("\n--------- state %d -------- # node %d\n",
		   LookNameB(where_i_am), num_states );
      PBeh( LookArgB(where_i_am,2) );
#endif

      b2 = RmIfSuccess(GetArgB(where_i_am,2),&is_success);

      if ( LookTypeB(b2)==StopC )
	num_stops++;
      if ( partial_test_expansion && !is_success )
	forced_leaf = SelectTransitions( &b2 );

      PutNameB( where_i_am, -1 );
      PutArgB( where_i_am, b2, 2 );
      ExpanOneLevel( where_i_am );
      GlueArgB( where_i_am, 1 );

      if (!forced_leaf){
	num_trans += NumArgB(where_i_am);
	if ( LookTypeB(where_i_am)==ExitC )
	  num_trans++;
	CheckNonSolvedPred( where_i_am );
	if ( LookTypeB(where_i_am)==AlternativeC ) {
	  pathStack  = Save_Stack( (DataStackTyp)where_i_am, pathStack  );
	  depthStack = Save_Stack( (DataStackTyp)a_depth,    depthStack );
	  varStack   = Save_Stack( (DataStackTyp)((int)LastTableV()+1),
				  varStack );
	}
      }
      a_depth++;
      where_i_am = next_wia_4( where_i_am, the_depth, &a_depth, forced_leaf );
      CurrentReport();
    }

    if ( mayEsc || utrEsc ){
      where_i_am = (BehTyp) Look_Stack( pathStack );
      if ( where_i_am!=NULL /* && where_i_am!=the_beh */ ) {
	do {
	  LASSERT( LookTypeB(where_i_am)==AlternativeC );
	  if ( LookB1(where_i_am)!=NULL )
	    GlueB( LookArgB(where_i_am,1), MakeB(0,StopC) );
	  if ( LookB2(where_i_am)!=NULL )
	    FreeB(GetArgB(where_i_am,2));
	}
	while ( ( where_i_am = after_leaf4(&a_depth) )!= NULL );
      }
    }
    Free_Stack( pathStack, (void(*)())NULL );
    Free_Stack( depthStack, (void(*)())NULL );
    Free_Stack( varStack, (void(*)())NULL );
    the_beh = NullArgs_to_Stop( the_beh);
    the_beh = RmAltStopInBeh( the_beh );

  }
  return the_beh;
}

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

/* TestExpand
 * Test Expansion of b.
 * d is the depth of the exploration.
 * se is the name of the sucess event.
 * opta, optd, opte and opts are output control options.
 * proc is the name of the test process.
 * mayc forces MAY tests to be thoroughly tested.
 * i_removal removes some redundant internal actions.
 * wbcontext says whether b is in a context suitable for i-removal.
 * x_resp is the expected test response ( MUST,MAY,REJECT or UNDEFINED ).
 * optq flag forces LOLA to quit on unexpected response.
 *
 * percentage, seed, bhsize are PartialExpand parameters
 * Default ( 100%, 0, UNDEFINED ) is equivalent to an exhaustive TestExpansion
 *
 */
void TestExpand( b,d,se,optt,opta,optd,opte,opts,proc,verbose,mayc,i_removal,wbcontext,x_resp,optq,percentage,seed,bhsize,gate_priority,vl )
     BehTyp        b;
     int           d;
     DescriptorTyp se;
     boolean optt,opta, optd, opte, opts, verbose, mayc,
     i_removal, wbcontext, optq, gate_priority;
     DescriptorTyp proc;
     int           x_resp, percentage, seed, bhsize, vl;
{
  BehTyp aux;

  verbose_level = vl;
  verbose_mode  = ( verbose_level>0 )? FALSE : verbose;
  Header();
  nonSolvedPred = FALSE;
  optiont = !optt;
  optiona = !opta;
  options = !opts;
  optiond = !optd;
  optione = !opte;
  optionx = x_resp!=UNDEFINED;
  expected_response = x_resp;
  sevent  = se;
  test_proc = proc;

  InitSuccessStack(se);

  force_complete_exploration = mayc;

  partial_test_expansion = bhsize!=UNDEFINED || percentage<100;
  vevents_first          = gate_priority;
  if ( partial_test_expansion )
    InitPartialTestExpand(percentage,seed,bhsize);

  b      = ShareB(b);
  aux    = expand_test( b, d, i_removal, wbcontext );
  PrintStat();
  TestResult( proc, partial_test_expansion );
  if ( optionx && (test_response!=x_resp) ){
    printMsgs("\n    Unexpected Test Response\n\n");
    if ( optq )
      EXITLOLA(UTRQUIT);
  }

  if ( partial_test_expansion )
    EndPartialTestExpand();

  PopSuccessStack();

  GlueB( b, aux );
  b = UnshareB(b);
}


/******************************************************************
 *
 *          ONE EXPANSION
 *
 *******************************************************************/


/*
 *  termination_event will be TRUE if the termination event is reached.
 */
static boolean termination_event;

/*
 * It is the length of the generated trace.
 */
static int trace_length;


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

/* Wact
 * prints current depth.
 */
static void Wact( a_depth )
     int a_depth;
{
  char buff[25];

  if (runtimeConfig==TextMode) {
    (void)sprintf(buff,"\b\b\b\b\b\b\b%7d",a_depth);
    printMsgs(buff);
  }
  else {
    (void)sprintf(buff,"%7d",a_depth);
    printPos(buff,printPos("",-1)-7);
    flushTarget();
  }
}

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

/* WactdOne
 * prints current depth when pcontactdepth reaches DELTADEPTH
 */
static void WactdOne(pcontactdepth,a_depth)
     int *pcontactdepth,a_depth;
{
  if (*pcontactdepth == DELTADEPTH) {
    *pcontactdepth = 1;
    Wact(a_depth);
  }
  else
    *pcontactdepth = *pcontactdepth + 1;
}


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


/* OneResult
 * Prints the result of a test that has been done with OneExpand.
 */
static void OneResult(proc,res,depth)
     DescriptorTyp proc;
     boolean       res;
     int           depth;
{
  char buff[100];

  if ( proc!=(DescriptorTyp)NULL ) {
    printTarget("\n    Process Test = ");
    PrintP( proc, printTarget );
  }
  printTarget("\n    Test result  = ");
  if ( !res )
    printTarget("REJECTED EXECUTION.\n");
  else
    printTarget("SUCCESSFUL EXECUTION.\n");


  if ( nonSolvedPred==TRUE ) {
    Warning("Invalid test. There are unresolved predicates or guards.\n");
  }
  (void)sprintf(buff,"\n       Transitions generated = %1d\n",depth);
  printTarget(buff);
}


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


/* expand_one
 * one-expansion of the_beh until the_depth
 */
static BehTyp expand_one( the_beh, the_depth, i_remove, wbcontext )
     BehTyp  the_beh;
     int     the_depth;
     boolean i_remove, wbcontext;
{
  BehTyp where_i_am, wia, b, b2;
  int    a_depth, i;
  char   indent[16];
  int    i_depth, i_rm_depth, *i_rm_depthPt, cero=0;

  if ( the_depth != 0 ) {
    if ( i_remove ) {
      expansion_flags = WEAK_EQUIV_EXP;
      i_depth         = MAXDEPTH_I_RMV;
    }
    else {
      expansion_flags = 0;
      i_depth         = 0;
    }
    a_depth      = 0;
    where_i_am   = MakeB(0,BehaviourC);
    PutArgB( where_i_am, the_beh, 2 );
    the_beh = where_i_am;
    while ( (where_i_am != NULL) && (the_depth != 0) ) {
      i_rm_depth   = i_depth;
      i_rm_depthPt = (!wbcontext && num_states==1) ? &cero: &i_rm_depth;
      b2 = Pre_Branch( GetArgB(where_i_am,2), i_rm_depthPt );
#ifdef TIME
#ifdef ASAP
      b2 = AsapT(b2);
#endif
#endif
      PutArgB( where_i_am, b2, 2 );
      PutNameB( where_i_am, -1 );
      ExpanOneLevel( where_i_am );
      GlueB( where_i_am, GetArgB(where_i_am,1) );
      CheckNonSolvedPred( where_i_am );
      if ( LookTypeB(where_i_am)==AlternativeC ) {
	i = 1 + (act_seed % NumArgB(where_i_am));
	b = GetArgB(where_i_am,i);
	GlueB( where_i_am, b );
	act_seed = NextSeed();
      }
      where_i_am = wia = LookActionUB( where_i_am );
      a_depth++;
      if ( LookTypeB(where_i_am)==IC ) {
	the_depth--;
      }
      else
	if ( LookTypeB(where_i_am)==GateC ) {
	  if ( LookNameB(where_i_am)==sevent ) {
	    termination_event = TRUE;
	    TrfStop( LookArgB(where_i_am,1) );
	    where_i_am = NULL;
	  }
	  else {
	    the_depth--;
	  }
	}

      if (verbose_mode) {
	(void)sprintf(indent," %4d  ",a_depth);
	PrintBeh(wia,1,NO_PROC,FALSE,indent,printTarget,FALSE,FALSE);
      }

      while ( (where_i_am!=NULL) && (LookTypeB(where_i_am)!=BehaviourC) )
	where_i_am = LookArgB( where_i_am, 1 );
    }

    trace_length = a_depth;
    ClearBeh( the_beh );
  }
  return the_beh;
}

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

/* OneExpand
 * One Expansion of b.
 * d is the depth of the exploration.
 * se is the name of an optional termination event.
 * proc is the name of the test process.
 *
 * return the next random value
 */
int OneExpand( b, d, se, proc, seed, verbose, i_remove, wbcontext )
     BehTyp        b;
     int           d,seed;
     DescriptorTyp se, proc;
     boolean       verbose, i_remove, wbcontext;
{
  BehTyp aux;

  termination_event = FALSE;
  verbose_mode   = verbose || (se==0);
  nonSolvedPred  = FALSE;
  sevent         = se;
  act_seed       = seed;
  act_seed       = NextSeed();

  aux            = expand_one( b, d, i_remove, wbcontext );
  /*
     if (verbose || (se==0)) {
     PrintBeh(aux,d,NO_PROC,FALSE,"   ",printTarget,TRUE,FALSE);
     printTarget("\n");
     }
     */
  if (se!=0) {
    OneResult(proc,termination_event,trace_length);
  }
  GlueB( b ,aux );

  return act_seed;
}

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




/* InterExpand
 * Interleaved Expansion of b.
 * d is the depth of the exploration.
 * se is the name of the sucess event.
 * proc is the name of the test process.
 */
void InterExpand( b, d, se, proc, dup, param, verbose )
     BehTyp        b;
     int           d;
     DescriptorTyp se, proc;
     boolean       dup, param, verbose;
{
  BehTyp aux;

  /*
     verbose_mode = verbose;
     Header();
     */
  nonSolvedPred = FALSE;
  b = ShareB(b);
  aux = InterleavedExpansion( b, d, se, proc, dup, param, verbose );
  /*
     PrintStat();
     TestResult( proc, FALSE );
     */
  GlueB( b, aux );
  b = UnshareB(b);
}







