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

/***********************************
  
  
  Miguel Angel Palomares Ortega
  
  11-11-1992
  
  This module implements an expansion algorithm that
  removes no determinism in each analized state.
  
  
  ************************************/


#ifdef INVEXP


#include "eximmed.h"
#include "exdupbeh.h"
#include "expre_br.h"
#include "babeh.h"
#include "batables.h"
#include "badefca.h"
#include "listack.h"
#include "limisc.h"
#include "balotosf.h"
#include "expostex.h"
#include "lilists.h"
#include "listdout.h"
#include "lihash.h"
#include "licell.h"
#include "baexpr.h"
#include "baattr.h"
#include "excomp.h"
#include "baprint.h"
#include "ievcdeex.h"
#include "iefunc.h"


/* List used for storing analized states */

static ListTyp behlist;



/*********************************************************************
 *
 *
 *          BEHAVIOUR LIST FUNCTIONS
 *
 *
 *********************************************************************/



/* CompareBehaviour
 * Returns if b1 and b2 offers the same actions (if they are equivalents).
 */
static boolean CompareBehaviour( b1, b2 )
     BehTyp b1,b2;
{
  boolean equal;
  
  if ( LookNameB(b1)!=LookNameB(b2) )
    return FALSE;
  
  equal = Call_Cmp_Rec_Beh( LookB2(b1), LookB2(b2) ); 
  
  
  return equal;
}



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



/* InitBehList
 * Inits the behaviour list.
 */
static void InitBehList()
{
  behlist = Create_list();
}



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



/* LookForBehList
 * If a equivalent behaviour is found in the behaviour list then
 * returns it , else returns NULL.
 */
static BehTyp LookForBehList(beh)
     BehTyp beh;
     
{
  ListTyp l;
  
  
  l = LookFor_list((DataListTyp)beh,behlist,CompareBehaviour);
  if (l == NULL)
    return (BehTyp)NULL;
  else 
    return (BehTyp)LookInfo_list(l);
}



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



/* AddBehList
 * Adds "beh" to behaviour list.
 */
static void AddBehList(beh)
     BehTyp beh;
     
{
  behlist = Insert_list((DataListTyp)beh,behlist);
}



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



/* FreeBehList
 * Frees the behaviour list.
 * It must be called when the expansion has finished.
 */
static void FreeBehList()
{
  Disp_list(behlist);
}



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



/* GetBehDef
 * Looks for a duplicated behaviour of beh in the behaviour list.
 * If it does exist then returns the duplicated behaviour. 
 * If beh has not a duplicated behaviour it is inserted in the behaviour
 * list and NULL is returned.
 */
static BehTyp GetBehDef( beh )
     BehTyp beh;
     
{
  BehTyp dupBeh;
  
  
  LASSERT( LookTypeB(beh)==BehaviourC );
  
  PutNameB( beh, (DescriptorTyp)0 );
  dupBeh = LookForBehList(beh);
  if ( dupBeh == NULL ) 
    AddBehList(beh);
  
  return dupBeh;
}




/******************************************************************
 *                                                              
 *                       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;
}

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

static void PrintStat()
{
  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");
}




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




static BehTyp alt_processing ( here )
     BehTyp here;
{
  BehTyp  t1 , t2 , t3 , t4 ;
  
  t1 = here;
  while ( t1 != NULL ) {
    t3 = LookActionUB( t1 );
    if  (LookType(t3)==GateC) {
      t2 = MakeB( 1, BehaviourC );
      PutCopy( t2, 1 );
      t4 = LookB1( t3 );
      PutB1( t3, t2 );
      PutB2( t2, t4 );
    }
    t1 = LookB2( 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;
}

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

/* ExpanOneLevel
 *
 */ 
static void ExpanOneLevel( here )
     BehTyp here;
{
  BehTyp the_copy;
  
  the_copy = CopyB( LookB2(here) );
  switch ( LookType(the_copy) )
    {
    case AlternativeC: 
      the_copy = alt_processing( the_copy );
      break;
      
    case GateC: 
      the_copy = gate_processing( the_copy );
      break;
      
    case StopC: 
      break;
      
    default:
      Error("Expan_one_level: Unexpected cell type.");
    }
  
  PutArgB( here , the_copy, 1 );
  
}


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


static boolean verbose_mode;

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



/******************************************************************
 *
 *           Removes no determinism 
 *
 *******************************************************************/




/* Rec_DE
 * Removes no determinism from behaviour "b" until processes instantiations.
 */
static void Rec_DE(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,j;
  BehTyp baux,baux2;
  DescriptorTyp name;
  boolean rde;  
  
  
  LASSERT(b!=NULL);
  type=LookTypeB(b);
  if (type == ProcessDefC)
    {
      b = LookArgB(b,1);
      type=LookTypeB(b);
    }
  if (type == ProcessInstC)
    return;
  
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      Rec_DE(LookArgB(b,1));
      return;
      
    case AlternativeC:
      b=Pre_Branch_Stop(b);
      if (LookTypeB(b) != AlternativeC)
        {
          Rec_DE(b);
          return;
        }
      
      i=1;
      while((i<NumArgB(b)) && (LookTypeB(b) == AlternativeC)) {
        rde=FALSE;
        for(j=i+1 ; ((j<=NumArgB(b)) && (LookTypeB(b) == AlternativeC)) ;++j)
          if ((LookTypeB(LookArgB(b,i)) == GateC) && (LookTypeB(LookArgB(b,j)) == GateC))
            {
              name=LookNameB(LookArgB(b,i));
              if ( name == LookNameB(LookArgB(b,j)) )  
                {
                  rde=TRUE;
                  baux=GetArgB(LookArgB(b,j),1);
                  baux2=GetArgB(LookArgB(b,i),1);
                  FreeArgB(b,j);
                  baux2=AppendUB(baux2,baux);
                  if (LookTypeB(b) == AlternativeC) {
                    baux=LookArgB(b,i);
                    PutArgB(baux,baux2,1);
                    Rec_DE(LookArgB(LookArgB(b,i),1));
                  }
                  else {
                    PutArgB(b,baux2,1);
                    Rec_DE(LookArgB(b,1));
                  }
                  --j;
                }  /* if ( ( name == LookName ... */
            }   /* if (LookTypeB(LookArgB ... */
	
	if (rde == FALSE)
	  if (LookTypeB(LookArgB(b,i)) == GateC)
	    Rec_DE(LookArgB(LookArgB(b,i),1));
	++i;
      }  /* while ... */
      
      if (NumArgB(b) == i)
        if (LookTypeB(LookArgB(b,i)) == GateC)
          Rec_DE(LookArgB(LookArgB(b,i),1));
      
      return;
      
    default:
      Error("Invalid Lotos Operator for Inverse Expansion");
      break;
    }
}




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




/* RmPletC
 * Removes "PletC" cells from behaviour "b".
 */
static void RmPletC(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,num;
  
  
  LASSERT(b != NULL);
  
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      RmPletC(LookArgB(b,1));
      return;
      
    case AlternativeC:
      num = NumArgB(b);
      for (i = 1 ; i <= num ; i++)
        RmPletC(LookArgB(b,i));
      return;
      
    case ProcessInstC:
      return;
      
    case PletC:
      GlueB(b,GetB(LookArgB(b,1)));
      RmPletC(b);
      return;
      
    default:
      Error("Invalid cell type");
      break;
    }
}




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




/* RmvAltSameP
 * Removes from alternatives instantiations of the same process.
 */
static void RmvAltSameP(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,j,num;
  BehTyp beh1,beh2;
  
  
  LASSERT( b != NULL);
  
  type = LookTypeB(b);
  if (type == ProcessDefC)
    {
      b = LookArgB(b,1);
      type = LookTypeB(b);
    }
  
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      RmvAltSameP(LookArgB(b,1));
      return;
      
    case AlternativeC:
      i = 1;
      while ((i <= NumArgB(b)) && (LookTypeB(b) == AlternativeC))
        {
          beh1 = LookArgB(b,i);
          if (LookTypeB(beh1) == ProcessInstC)
            for (j = i + 1 ; ((j <= NumArgB(b)) && (LookTypeB(b) == AlternativeC)) ; j++)
              {
                beh2 = LookArgB(b,j);
                if (LookTypeB(beh2) == ProcessInstC)
                  if (LookNameB(beh1) == LookNameB(beh2))
                    {
                      FreeArgB(b,j);
                      j--;
                    }
              }
          i++;
        }
      
      if (LookTypeB(b) == AlternativeC)
        {
          num = NumArgB(b);
          for (i=1 ; i<=num ; i++)
            RmvAltSameP(LookArgB(b,i));
        }
      else
        RmvAltSameP(b);
      
      return;
      
    case ProcessInstC:
      return;
      
    default:
      Error("invalid cell");
      break;
    }
  
}



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





/* RmNoDet
 * Removes no determinism from "b" until processes instantiations.
 */
static BehTyp RmNoDet(b)
     BehTyp b;
     
{
  
  LASSERT(b!=NULL);
  
  b = GetB(b); 
  
  RmPletC(b);
  
  Rec_DE(b);  
  
  b = RmAltStopInBeh(b);
  RmvAltSameP(b);
  
  
  return b;
  
}



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


/* depth level */
#define DATLIN     5  

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

static int  contdepth, contactdepth;
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;
    (void)sprintf(buff,"(%7d)\b\b\b\b\b\b\b\b\b",a_depth);
    printMsgs(buff);
  }
  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) 
      return TRUE;
    else if ( the_depth==(*pa_depth)+1 ) {
      *pa_depth = *pa_depth + 1;
      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) printMsgs(".\n\n");
    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) printMsgs(".\n\n");
      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 );
	printMsgs(buff);
      }
      return LookActionUB( pre_ord );
    }
  }    
}

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

/* next_wia_123
 *
 */
static 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);
	printMsgs(buff);
	contdepth = 1;
      }
      else {
	(void)sprintf(buff,"-%5d/",*pa_depth);
	printMsgs(buff);
	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;
}

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

/* NameDupProc
 * returns a new name for a new duplicated process.
 */
static char * NameDupProc()
{
  char * s;
  
  s = (char*)emalloc(18);  
  do {
    (void)sprintf(s,"duplicate%d",num_produp);
    num_produp++;
  }
  while ( FindP(s)!=0 );
  return s;
}

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

/* 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.
 */
static link_beh( here, eq_here )
     BehTyp here, eq_here;
     
{
  BehTyp aux, t0, t1 , t2 ;
  DescriptorTyp name;
  GateSetTyp gs;
  GateListTyp gl;
  PAttrTyp gla;
  
  
  t1 = LookB1( eq_here );
  if ( LookType(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 );
  }
  else {
    t2 = t1;
    name = LookName( t2 );
  }
  aux = MakeB( name, ProcessInstC );
  GlueB( here, aux );
  gla = LookA( t2, GLA );
  if ( gla!=NULL )
    PutA( here, gla );
}

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

/* expand_exp
 * return the expansion of the_beh until the_depth with duplicated beheviour
 * detection.
 */
static BehTyp expand_exp( the_beh, the_depth )
     BehTyp the_beh;
     int the_depth;
{ 
  BehTyp         where_i_am, dupb, b2;
  int            a_depth;
  DescriptorTyp  last_proc; 
  int            cero=0;
  char buff[15];
  
  if ( the_depth != 0 ) {
    InitStat();
    if (verbose_mode) {
      (void)sprintf(buff,"%5d",0);
      printMsgs(buff);
      contdepth      = 1;
      contactdepth   = 1;
    }
    expansion_flags = DUPLICATE_EXP;
    last_proc      = LastTableP(); 
    InitBehList();
    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 ) {
      b2 = Pre_Branch( GetArgB(where_i_am,2), &cero );
      b2 = RmNoDet(b2);
      PutArgB( where_i_am, b2, 2 );
      
      if ( LookType(LookArgB(where_i_am,2))==StopC )
	dupb = NULL;
      else
	dupb = GetBehDef( where_i_am );
      if ( dupb!=NULL ) {
	num_dupproc += 1;
	link_beh( where_i_am, dupb );
      }
      else {
	num_states += 1;
	ExpanOneLevel( where_i_am );
	where_i_am = LookB1( where_i_am );
	num_trans += NumArgB( where_i_am );
	if ( LookType(where_i_am)==StopC ) 
	  num_stops++;
	if ( LookType(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 );
    }
    FreeBehList();
    PrintStat();
    Free_Stack( pathStack, (void(*)())NULL );
    Free_Stack( depthStack, (void(*)())NULL );
    ClearBeh( the_beh );
    DupProcTab_Func( last_proc+1 );
  }   
  return the_beh;
}

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


/* Instantiate
 * return an instantiation of process definition b.
 */
static BehTyp Instantiate(b)
     BehTyp b;
{
  BehTyp      inst;
  PAttrTyp    a;
  
  inst  = MakeB( LookNameB(b), ProcessInstC );
  if ( (a=LookA( b, GLA ))!=NULL )
    PutA( inst, a );
  return inst;
}


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




/* VC_DE_Expand
 * Expansion of b until depth d.
 */
void VC_DE_Expand( b, verbose )
     BehTyp  b;
     boolean verbose; 
{
  BehTyp   aux, beh, inst;
  
  
  verbose_mode = verbose;
  Header();
  if ( LookTypeB(b)==ProcessDefC ) {
    inst   = Instantiate( b );
    aux    = expand_exp( inst, -1 );
    beh    = GetArgB( b, 1 );
    FreeB( beh );
    AddArgB( b, aux );
  } 
  else {
    if ( LookTypeB(b)==SpecificationC )
      b = LookArgB( b, 1 );
    aux = expand_exp( b, -1);
    GlueB( b, aux );
  }
}


#endif /* INVEXP */




