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

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

   Santiago Pavon Gomez
   Francisco Monfort Martin
   David Larrabeiti Lopez

   25-07-1990

   Commands

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

 /* LINTLIBRARY */

/* KJT 22/01/23: added header */
#include <unistd.h>

/* KJT 12/02/12: Added */
#include <stdlib.h>
#include <sys/stat.h>
#include "listdh.h"
#include "listdout.h"
#include "limisc.h"
#include "ligetlin.h"
#include "batables.h"
#include "baprint.h"
#include "incomm.h"
#include "bainit.h"
#include "bamove.h"
#include "exexpans.h"
#include "ststep.h"
#include "babeh.h"
#include "badefca.h"
#include "instat.h"
#include "batyperw.h"
#include "balotosf.h"
#include "itintexp.h"
#include "batransl.h"
#include "exdiver.h"
#include "expre_br.h"
#include "eximmed.h"
#include "basust_v.h"
#include "ie_vc.h"
#include "ie_nrec.h"
#include "ie_k.h"
#include "inparser.h"

/******************************************************************
 *
 *  Common variables, functions,...
 *
 *******************************************************************/

/* KJT 18/05/02: defined NUL */

#define NUL '\0'

/* output file */
static  FILE *stfd;


/* PrintStrInFD
 * Prints the string "s" into "stfd".
 */
static void PrintStrInFD(s)
     char* s;
{
  (void)fprintf(stfd,"%s",s);
}

/******************************************************************
 *
 *  Depuration Information.
 *
 *     This information is used in the Step mode, but it is removed
 *     if any transformation is done.
 *
 *******************************************************************/

static boolean NeverRemovedDepInfo = TRUE;

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

static void RmvDepInfo(b)
     BehTyp b;
{
  int i;

  while ( b!=NULL ) {
    if ( VisitedB( b ) )
      return;
    switch ( LookTypeB(b) )
      { case GateC:
	 case IC:
	 case ExitC:
	 case ProcessInstC:
	   if ( LookA(b,STA)!=NULL )
	     FreeA( GetA(b,STA) );
	   if ( LookA(b,SSLA)!=NULL )
	     FreeA( GetA(b,SSLA) );
	   break;
	 }
    for ( i=NumArgB(b); i>1; i-- )
      RmvDepInfo(LookArgB(b,i));
    b = LookArgB(b,1);
  }
}

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

/* RemoveDepurationInfo
 * Remove from the specification all the depuration info in order to
 * save up memory.
 */
static void RemoveDepurationInfo()
{
  int i, lastProc;

  if ( NeverRemovedDepInfo ) {
    lastProc = LastTableP();
    Begin_VisitB();
    for ( i=1 ; i<=lastProc; i++ )
      RmvDepInfo( LookArgB(GetP_def(i),1) );
    End_VisitB();
    NeverRemovedDepInfo = FALSE;
  }
}

/* IsRemovedDepInfo
 * return TRUE if the depuration attributes have been deleted
 */
boolean IsRemovedDepInfo()
{
  return !NeverRemovedDepInfo;
}

/******************************************************************
 *
 *  Command: load
 *
 *******************************************************************/

extern char* getenv();

#define SIZESTR 100

static char nspec[SIZESTR] = "\0";
static char nlibr[SIZESTR] = "\0";

static char nspeclsf[SIZESTR];

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

static int make_lsf()
{
  char cmd1[500];
#ifdef TOPOIFC
  static char * argv1[] = { "toposet", nspec, "-v", "-l", nlibr };
  static char * argv2[] = { "topo", nspec, "-v", "-plola"};
  int    argc1 = sizeof(argv1)/sizeof(argv1[0]);
  int    argc2 = sizeof(argv2)/sizeof(argv2[0]);
#endif

  if (nlibr[0]!='\0') {
#ifdef MSDOS
    (void)sprintf(cmd1,"toposet %s -v -l %s",nspec,nlibr);
#else
    (void)sprintf(cmd1,"toposet %s -l %s 2>&1",nspec,nlibr);
#endif

#ifdef TOPOIFC
    toposetmain(argc1,argv1);
#else
    if (System(cmd1)!=0)
      (void)printf("\nWARNING: problems updating the library %s.\n\n",nlibr);
#endif
  }
#ifdef MSDOS
  (void)sprintf(cmd1,"topo %s -v -plola",nspec );
#else
  (void)sprintf(cmd1,"topo %s -plola 2>&1",nspec );
#endif

#ifdef TOPOIFC
  topomain(argc2,argv2);
#else
  if (System(cmd1)!=0)
    return -1;
#endif
  return 0;
}

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

/*
 * RmExt
 */
static void RmExt(id)
     char *id;
{
  char *c;

  c = strrchr ( id,'.' ) ;
  *c = '\0';
}

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

/* is_lot
 * Returns true if id ends in ".lot"
 */
static boolean is_lot (id)
     char * id;
{
  char *c;

  if ((c = strrchr ( id,'.' )) != NULL)
    if (strcmp(c,".lot") == 0)
      return TRUE;
  return FALSE;
}

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

/* is_cr
 * Returns true if id ends in ".cr"
 */
static boolean is_cr (id)
     char * id;
{
  char *c;

  if ((c = strrchr ( id,'.' )) != NULL)
    if (strcmp(c,".cr") == 0)
      return TRUE;
  return FALSE;
}

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

/* check_name_load
 * Removes .lot or .cr extensions.
 * Sets nspec, nlibr and nspeclsf.
 * Returns FALSE if there is an error.
 */
static boolean check_name_load (spec,libr)
     char *spec, *libr;
{
  nlibr[0] = NUL;				/* KJT 18/05/02: NULL -> NUL */
  if (spec[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
    (void)sprintf(nspec,"%s",spec);
    if (is_cr(nspec) || is_lot(nspec))
      RmExt(nspec);
    (void)sprintf(nspeclsf,"%s.lsf",nspec);

    if (libr[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
      (void)sprintf(nlibr,"%s",libr);
      if (is_lot(nlibr))
	 RmExt(nlibr);
    }
  }
  else
    if (libr[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
      printError("      The specification file name is empty.\n\n");
      return FALSE;
    }
  return TRUE;
}

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

/* echo_load_files
 *
 */
/* KJT 22/01/23: added "int" type */
static int echo_load_files()
{
  if ( nspec[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
    printMsgs("  Loading specification from ");
    printMsgs(nspec);
    printMsgs(".\n");
  }
  if ( nlibr[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
    printMsgs("  Loading library from ");
    printMsgs(nlibr);
    printMsgs(".\n");
  }
  printMsgs("\n");
}

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

/* ECload
 * Executes the command load.
 * spec is the filename of the specification.
 * libr is the library file name.
* returns -1 if there is an error.
*/
int ECload(spec,libr)
    char *spec, *libr;
{
 printMsgs("load\n\n");
 if (check_name_load(spec,libr)) {
   echo_load_files();
    if (nspec[0]!=NUL) {			/* KJT 18/05/02: NULL -> NUL */
     FreeMove();
     InitDiver();
     if (make_lsf()==0){
       printMsgs("\n  Restoring ");
       printMsgs(nspeclsf);
       printMsgs(".\n");
	InitBA();
	InitEX();
	InitIT();
       if (LoadSpec(nspeclsf)){
	 InitMove(1);
	InitIT();
#ifdef TIME
	(void) InitT();
#endif
	  NeverRemovedDepInfo = TRUE;
	 printMsgs("\n");
	 return 0;
       }
     }
     else {
       printError("\n      I can not process the file ");
       printError(nspec);
       printError(".\n");
     }
   }
   else
     printError("      A specification file name must be given.\n");
   printError("\n");
 }
 return -1;
}

/******************************************************************
*
*  Command: print
*
*******************************************************************/

static boolean opcionA, opcionC, opcionP, opcionT;

static void check_opcion_print(contopcio,lst_opcio)
    char *lst_opcio;
    int contopcio;
{
 int i;

 opcionP = (boolean)Default("print_proc");
 opcionT = (boolean)Default("print_types");
 opcionA = FALSE;
 opcionC = FALSE;
 for (i=0 ; i != contopcio ; i++) {
   if (lst_opcio[i]=='p')
     opcionP = TRUE;
   else if (lst_opcio[i]=='t')
     opcionT = TRUE;
   else if (lst_opcio[i]=='c')
     opcionC = TRUE;
   else if (lst_opcio[i]=='a')
     opcionA = TRUE;
 }
}


static void echo_print(num,ident)
    int num;
    char * ident;
{
 printMsgs("print ");
 if (opcionP == TRUE) printMsgs("-p ");
 if (opcionT == TRUE) printMsgs("-t ");
 if (opcionA == TRUE) printMsgs("-a ");
 if (opcionC == TRUE) printMsgs("-c ");
 PrintInt(printMsgs,num); printMsgs(" ");
 if (ident[0]!=NUL)			/* KJT 18/05/02: NULL -> NUL */
   printMsgs(ident);
 printMsgs("\n\n");
}

#ifndef MSDOS
#define NAMETMP "lolaprinttmp"

/* RmLolaPrintTmp
* Removes auxiliar files
*/
static void RmLolaPrintTmp()
{
 char command1[500];

 (void)sprintf(command1,"/bin/rm -f %s.* > /dev/null\n",NAMETMP );
 if (System(command1)!=0)
   printError("      /bin/rm error.\n\n");
}
#endif


/* ECprint
* Executes the command print.
* contopcio is the number of options in lst_opcio.
* lst_opcio is the list of options.
* depth is the depth of the print.
* outfile is the output file.
* "pstr" is a function to print strings (if outfile is "")
*/
void ECprint( contopcio, lst_opcio, depth, outfile, pstr )
    int   depth,contopcio;
    char *outfile, *lst_opcio;
    void (*pstr)();
{
 BehTyp p;
 char nametmp[20];
 char command1[500];
 int  proc;

 check_opcion_print(contopcio,lst_opcio);
 if ( depth==UNDEFINED )
   depth = (int)Default("print_depth");
 echo_print(depth,outfile);
 if ((p = GetCursor()) != NULL) {

#ifndef MSDOS
   if (opcionC == TRUE) {
     (void)sprintf(nametmp,"%s.lot",NAMETMP);
     if ((stfd = fopen(nametmp,"w")) == NULL) {
       printError("      Open file error.\n\n");
       return;
     }
     PrintBeh(GetP_def(1),-1,ALL_PROC,TRUE,"",PrintStrInFD,TRUE,FALSE);
     (void)fflush(stfd);
     (void)close((int)stfd);

     (void)sprintf(command1,
		   "$LITEDIR/$LITEARCH/bin/topo %s -cr 2>&1",NAMETMP);
     if (System(command1)!=0)
       printError("      I cannot generate CR.\n");
     else {
       if (outfile[0]==NUL)			/* KJT 18/05/02: NULL -> NUL */
	 (void)sprintf(command1,"/bin/cat %s.cr 2>&1",NAMETMP);
       else
	 if (is_cr(outfile))
	   (void)sprintf(command1,"/bin/cat %s.cr > %s 2>&1",NAMETMP,outfile);
	 else
	   (void)sprintf(command1,"/bin/cat %s.cr >%s.cr 2>&1",NAMETMP,outfile);
       if (System(command1)!=0)
	 printError("      /bin/cat error.\n");
     }
     RmLolaPrintTmp();
     printError("\n");
     return;
   }
#else
   if (opcionC == TRUE) {
     printError("      Error: Common Representation format can only be\n");
     printError("             generated inside LITE.\n\n");
     return;
   }
#endif

   if (opcionA==TRUE) {
     proc = ALL_PROC;
     p = GetP_def(1);
     depth = -1;
     opcionT = TRUE;
   }
   else if (opcionP==TRUE)
     proc = USED_PROC;
   else
     proc = NO_PROC;

   if (outfile[0]!=NUL)			/* KJT 18/05/02: NULL -> NUL */
     if ((stfd = fopen(outfile,"w")) == NULL) {
       printError("      I can't open file ");
       printError(outfile);
       printError("\n");
       return;
     }
     else
       pstr = PrintStrInFD;

   PrintBeh(p,depth,proc,opcionT,"",pstr,TRUE,FALSE);
   pstr("\n");

   if (outfile[0]!=NUL) {			/* KJT 18/05/02: NULL -> NUL */
     (void)fflush(stfd);
     (void)close((int)stfd);
   }
 }
 else
   printError("      There is not any tree to print.\n\n");
}


/******************************************************************
*
*  Command: Save
*
*******************************************************************/

static void echo_save(ident)
    char *ident;
{
 printMsgs("save ");
  if (ident[0]!=NUL)				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(ident);
 printMsgs("\n\n");
}


/* ECsave
* Executes the execution of the command save.
* outfile is the output file.
* "pstr" is a function to print strings (if outfile is "")
*/
void ECsave(outfile,pstr)
    char *outfile;
    void (*pstr)();
{
 BehTyp p;

 echo_save(outfile);
 if ((p = GetCursor()) != NULL) {
   if (outfile[0]!=NUL)			/* KJT 18/05/02: NULL -> NUL */
     if ((stfd = fopen(outfile,"w")) == NULL) {
       printError("      I can't open file ");
       printError(outfile);
       printError("\n\n");
       return;
     }
     else
       pstr = PrintStrInFD;

   DrawB(p,pstr);
   pstr("\n");

    if (outfile[0]!=NUL) {			/* KJT 18/05/02: NULL -> NUL */
     (void)fflush(stfd);
     (void)close((int)stfd);
   }
 }
 else
   printError("      There is not any tree to save.\n\n");
}

/******************************************************************
*
*  Command: Data
*
*******************************************************************/

/* ECdata
* Executes the command dataTable.
* table indicates the table to print (g, v, o, p or s).
* l and h are the first and the last positions to print.
*/
void ECdata(table,l,h)
    char table;
    int l,h;
{
 char buff[50];

 if (l<=0)
   l = 1;
 switch (table)
   { case 'g':
     case 'G':
       if (h == 0)
	 h = LastTableG();
       (void)sprintf(buff,"data -%c %d %d\n",table,l,h);
       printMsgs(buff);
       PrintTable(GateTable,l,h,printTarget);
       break;
     case 'v':
     case 'V':
       if (h == 0)
	 h = LastTableV();
       (void)sprintf(buff,"data -%c %d %d\n",table,l,h);
       printMsgs(buff);
       PrintTable(VarTable,l,h,printTarget);
       break;
     case 'o':
     case 'O':
       if (h == 0)
	 h = LastTableO();
       (void)sprintf(buff,"data -%c %d %d\n",table,l,h);
       printMsgs(buff);
       PrintTable(OperTable,l,h,printTarget);
       break;
     case 'p':
     case 'P':
       if (h == 0)
	 h = LastTableP();
       (void)sprintf(buff,"data -%c %d %d\n",table,l,h);
       printMsgs(buff);
       PrintTable(ProcTable,l,h,printTarget);
       break;
     case 's':
     case 'S':
       if (h == 0)
	 h = LastTableS();
       (void)sprintf(buff,"data -%c %d %d\n",table,l,h);
       printMsgs(buff);
       PrintTable(SortTable,l,h,printTarget);
       break;
     }
 printMsgs("\n");
}


/******************************************************************
*
*  Command: Expand.
*
*******************************************************************/


static boolean opcVexp, opcIexp;

static void echo_expand(depth,contopcio,lst_opcio)
    int depth,contopcio;
    char *lst_opcio;
{
 int i;

 opcVexp = (boolean)Default("verbose");
 opcIexp = (boolean)Default("expand_i_removal");
 if ( depth==UNDEFINED )
   depth = (int)Default("exploration_depth");
 printMsgs("expand  ");
 PrintInt(printMsgs,depth);
 for (i=0 ; i != contopcio ; i++){
   if (lst_opcio[i]=='v') {
     opcVexp = TRUE;
   }
   if (lst_opcio[i]=='i') {
     opcIexp = TRUE;
   }
 }
 if ( opcVexp )
   printMsgs(" -v");
 if ( opcIexp )
   printMsgs(" -i");
 printMsgs("\n");
}



/* ECexpand
* Executes the command expand.
* depth is the expansion depth.
* contopcio is the number of options in lst_opcio.
* lst_opcio is the list of options.
*/
void ECexpand( depth,contopcio,lst_opcio )
    int depth,contopcio;
    char *lst_opcio;
{
 BehTyp b, root;
 DescriptorTyp dp;

 echo_expand(depth,contopcio,lst_opcio );

 b = GetCursor();
 if (b!=NULL) {
   Rw_Spec();
   Expandable( (boolean)Default("divergence_check"),
		(boolean)Default("unguarded_proc_check") );
   RemoveDepurationInfo();

   root = GetRoot();
   if ((LookTypeB(root)==ProcessDefC) && (b!=root)) {
     dp = LookNameB( root );
     PutP_def( dp, CopyMovePath() );
     Expand( b, depth, opcVexp, opcIexp,
	    (opcIexp ? IsCursorAt_WBE_Context() : FALSE) );
     FreeB( UnshareB(GetP_def(dp)) );
     PutP_def( dp, UnshareB(root) );
   }
   else
     Expand( b, depth, opcVexp, opcIexp,
	    (opcIexp ? IsCursorAt_WBE_Context() : FALSE) );
 }
 else
   printError("      There is not any behaviour to expand.\n\n");
}


/******************************************************************
*
*  Command: Free Expand.
*
*******************************************************************/

static boolean opcVfree, opcIfree;

static void echo_free(depth,contopcio,lst_opcio)
    int depth,contopcio;
    char *lst_opcio;
{
 int i;

 opcVfree = (boolean)Default("verbose");
 opcIfree = (boolean)Default("expand_i_removal");
 printMsgs("free  ");
 if ( depth==UNDEFINED )
   depth = (int)Default("exploration_depth");
 PrintInt(printMsgs,depth);
 for (i=0 ; i != contopcio ; i++){
   if (lst_opcio[i]=='v') {
     opcVfree = TRUE;
   }
   if (lst_opcio[i]=='i') {
     opcIfree = TRUE;
   }
 }
 if ( opcVfree )
   printMsgs(" -v");
 if ( opcIfree )
   printMsgs(" -i");
 printMsgs("\n\n");
}

static void AddPletBelowCursor()
{
 BehTyp           plet,cursor;
 ExprListTyp      hel,el;
 VarAssignListTyp val;
 ExprTyp          e;
 int              n;

 cursor = GetCursor();
 if ( LookArgB(cursor,1)!=NULL) {
   n =  LookTypeB(cursor)==InterleavedC ? 1 : NumArgB(cursor);
   for ( ; n>0 ; n-- ) {
     hel  = GetFreeVarsBehSV(LookArgB(cursor,n));
     plet = MakeB(0,PletC);
     val  = NULL;
     if (hel!=NULL) {
       for ( el = hel ; el!=NULL ; el=Next_list(el) ) {
	 e   = UnshareE((ExprTyp)GetInfo_list(el));
	 val = InsertVAL(val,LookNameE(e),e);
       }
       PutA(plet,MakeA((AttrValueTyp)val,VALA));
       Disp_list(hel);
     }
     AddArgB(plet,GetArgB(cursor,n));
     PutArgB(cursor,plet,n);
   }
 }
}


/* ECfree
* Executes the command freeExpand.
* depth is the expansion depth.
* contopcio is the number of options in lst_opcio.
* lst_opcio is the list of options.
*/
void ECfree( depth,contopcio,lst_opcio )
    int depth,contopcio;
    char *lst_opcio;
{
 BehTyp b, root;
 DescriptorTyp dp;

 echo_free(depth,contopcio,lst_opcio );

 b = GetCursor();
 if (b!=NULL) {
   Rw_Spec();
   Expandable((boolean)Default("divergence_check"),
	       (boolean)Default("unguarded_proc_check"));
   RemoveDepurationInfo();

   root = GetRoot();
   if (LookTypeB(root)==ProcessDefC) {
     dp = LookNameB(root);
     PutP_def(dp,CopyMovePath());
     AddPletBelowCursor();
     FreeExpand( b, depth, opcVfree, opcIfree,
		(opcIfree?IsCursorAt_WBE_Context():FALSE) );
     FreeB(UnshareB(GetP_def(dp)));
     PutP_def(dp,UnshareB(root));
   }
   else
     FreeExpand( b, depth, opcVfree, opcIfree,
		(opcIfree?IsCursorAt_WBE_Context():FALSE) );
 }
 else
   printError("      There is not any behaviour to expand.\n\n");
}

/******************************************************************
*
*  Command: Var Expand.
*
*******************************************************************/

static boolean opcVvar, opcIvar;


static void echo_var(depth,contopcio,lst_opcio)
    int depth,contopcio;
    char *lst_opcio;
{
 int i;

 opcVvar = (boolean)Default("verbose");
 opcIvar = (boolean)Default("expand_i_removal");
 if ( depth==UNDEFINED )
   depth = (int)Default("exploration_depth");
 printMsgs("var  ");
 PrintInt(printMsgs,depth);
 for (i=0 ; i != contopcio ; i++) {
   if (lst_opcio[i]=='v') {
     opcVvar = TRUE;
   }
   if (lst_opcio[i]=='i') {
     opcIvar = TRUE;
   }
 }
 if ( opcVvar )
   printMsgs(" -v");
 if ( opcIvar )
   printMsgs(" -i");
 printMsgs("\n\n");
}


/* ECvar
* Executes the command varExpand.
* depth is the expansion depth.
* contopcio is the number of options in lst_opcio.
* lst_opcio is the list of options.
*/
void ECvar( depth,contopcio,lst_opcio )
    int depth,contopcio;
    char *lst_opcio;
{
 BehTyp b, root;
 DescriptorTyp dp;

 echo_var(depth,contopcio,lst_opcio );

 b = GetCursor();
 if (b!=NULL) {
   Rw_Spec();
   Expandable((boolean)Default("divergence_check"),
	       (boolean)Default("unguarded_proc_check"));
   RemoveDepurationInfo();

   root = GetRoot();
   if ((LookTypeB(root)==ProcessDefC) && (b!=root)) {
     dp = LookNameB(root);
     PutP_def(dp,CopyMovePath());
     VarExpand(b,depth,opcVvar,opcIvar,
	       (opcIvar? IsCursorAt_WBE_Context() : FALSE) );
     FreeB(UnshareB(GetP_def(dp)));
     PutP_def(dp,UnshareB(root));
   }
   else
     VarExpand( b, depth, opcVvar, opcIvar,
	       (opcIvar? IsCursorAt_WBE_Context() : FALSE) );
 }
 else
   printError("      There is not any behaviour to expand.\n\n");
}

/******************************************************************
*
*  Command:   Test Expand.
*
*******************************************************************/

static boolean ParseInt();
static boolean ParseResp();
static boolean ParseSwitch();
static boolean ParseString();
static char *  SPInt();
static char * SPResp();
static char * SPSwitch();
static char * SPString();


static boolean TestOptionA, TestOptionE, TestOptionD, TestOptionS, TestOptionV,
TestOptionY, TestOptionI, TestOptionQ, TestOptionX, TestOptionT;

static boolean PartOptionP, PartOptionB, PartOptionG;

static void check_opcion_test(contopcio,lst_opcio)
    char *lst_opcio;
    int contopcio;
{
 int i;

 TestOptionT = FALSE;
 TestOptionA = FALSE;
 TestOptionS = FALSE;
 TestOptionD = FALSE;
 TestOptionE = FALSE;
 TestOptionV = (boolean)Default("verbose");
 TestOptionY = !(boolean)Default("quit_exploration_on_may_response");
 TestOptionI = !(boolean)Default("test_i_removal");
 TestOptionX = (int)Default("expected_response")!=UNDEFINED;
 TestOptionQ = (boolean)Default("quit_lola_on_unexpected_response");
 PartOptionP = FALSE;
 PartOptionG = FALSE;
 PartOptionB = FALSE;
 for (i=0 ; i != contopcio ; i++) {
   if (lst_opcio[i]=='t')
     TestOptionT = TRUE;
   else if (lst_opcio[i]=='a')
     TestOptionA = TRUE;
   else if (lst_opcio[i]=='s')
     TestOptionS = TRUE;
   else if (lst_opcio[i]=='e')
     TestOptionE = TRUE;
   else if (lst_opcio[i]=='d')
     TestOptionD = TRUE;
   else if (lst_opcio[i]=='v')
     TestOptionV = TRUE;
   else if (lst_opcio[i]=='y')
     TestOptionY = TRUE;
   else if (lst_opcio[i]=='i')
     TestOptionI = TRUE;
   else if (lst_opcio[i]=='x')
     TestOptionX = TRUE;
   else if (lst_opcio[i]=='q')
     TestOptionQ = TRUE;
   else if (lst_opcio[i]=='p')
     PartOptionP = TRUE;
   else if (lst_opcio[i]=='g')
     PartOptionG = TRUE;
   else if (lst_opcio[i]=='b')
     PartOptionB = TRUE;
 }
}


static void echo_test(command,num,ident,process,x_resp,percent,seed,bhsize,vl)
    int num;
    char * command, * ident, * process;
    int x_resp,percent,seed,bhsize,vl;
{
 printMsgs(command);
 printMsgs(" ");
 PrintInt(printMsgs,num);
 printMsgs(" ");
  if (ident[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(ident);
   printMsgs(" ");
 }
  if (process[0]!=NUL) {			/* KJT 18/05/02: NULL -> NUL */
   printMsgs(process);
   printMsgs(" ");
 }
 if (TestOptionT == TRUE)
   printMsgs("-t ");
 if (TestOptionA == TRUE)
   printMsgs("-a ");
 if (TestOptionD == TRUE)
   printMsgs("-d ");
 if (TestOptionE == TRUE)
   printMsgs("-e ");
 if (TestOptionS == TRUE)
   printMsgs("-s ");
 if (TestOptionV == TRUE){
   printMsgs("-v ");
   PrintInt(printMsgs,vl);
   printMsgs(" ");
 }
 if (TestOptionY == TRUE)
   printMsgs("-y ");
 if (TestOptionI == TRUE)
   printMsgs("-i ");
 if (TestOptionX == TRUE){
   printMsgs("-x ");
   printMsgs(SPResp(x_resp));
   printMsgs(" ");
 }
 if (TestOptionQ == TRUE)
   printMsgs("-q ");
 if (PartOptionP){
   printMsgs("-p ");
   PrintInt(printMsgs,percent);
   printMsgs(" ");
   PrintInt(printMsgs,seed);
   printMsgs(" ");
   if (PartOptionG)
     printMsgs("-g ");
 }
 if (PartOptionB){
   printMsgs("-b ");
   PrintInt(printMsgs,bhsize);
   printMsgs(" ");
 }
 printMsgs("\n\n");
}




/* ECtest
* Executes the command TestExpand.
* depth is the expansion depth.
* success is the name of the success event.
* process is the name of the test process.
* n_opt is the number of options and opt_lst is the list of options.
* exp_resp is the expected response.
* vl is the verbose level
*
* bhtsz,seed,percent correspond to a partial testexpansion when
* bhtsz!=0 or percent!=100%
* bhtsz (Mb) is the size of the table for bit state hashing
* percent is the % of alternatives to be explored in every state
* seed is the random generator seed when percent<100%
*/
void ECtest(n_opt,depth,success,process,opt_lst,exp_resp,bhtsz,seed,percent,vl)
    int   n_opt, depth, bhtsz, seed, percent, vl;
    char *success, *process, *opt_lst, *exp_resp;
{
 BehTyp        b, bb, root;
 DescriptorTyp dp, sed,proc;
 int           expected_response;

 check_opcion_test(n_opt,opt_lst);
 if ( depth==UNDEFINED )
   depth = (int)Default("exploration_depth");
 if ( success[0]=='\0' )
   success = (char*)Default("success_event");
 if ( exp_resp[0]=='\0' )
   expected_response = (int)Default("expected_response");
 else
   if (!ParseResp(exp_resp,&expected_response) ){
     printError("\n      Wrong Test Response\n");
     return;
   }
 if ( PartOptionB )
   if ( bhtsz==UNDEFINED )
     bhtsz = (int)Default("msize");
   else
     bhtsz = bhtsz<0? -bhtsz:bhtsz;

 percent = percent<0 ? -percent:percent;
 percent = percent>100 ? 100: percent;

 echo_test("testexpand",depth,success,process,expected_response,
	   percent,seed,bhtsz,vl);


 if ( TestOptionX && expected_response==UNDEFINED ){
   printError("\n      Missing Test Response\n\n");
   return;
 }

 sed = GetSuccessEvent(success);
 if ( sed ==-1 )
   return;
 if ( sed==0 ){
   printError("      A success event must be defined either as a TestExpand parameter\n");
   printError("      or by means of the Set command ( e.g. lola> set success_event test_ok ).\n\n");
   return;
 }
 if ((proc=GetTestProcess(process))==-1 )
   return;
 b = MvCursorBeh();
 if (b!=NULL) {
   Rw_Spec();
   Expandable((boolean)Default("divergence_check"),
	       (boolean)Default("unguarded_proc_check"));
   RemoveDepurationInfo();

   if ( process[0]!=NUL ) {			/* KJT 18/05/02: NULL -> NUL */
     printMsgs("  Composing behaviour and test :\n\n");
     bb = Compose_b_with_Test(b,proc,sed);
     if ( bb==NULL ) {
       return;
     }
     PrintBeh(bb,-1,NO_PROC,FALSE,"   ",printTarget,TRUE,FALSE);
     printTarget("\n");
   }
   else
     bb = CopyB(b);
   root = GetRoot();
   if ((LookTypeB(root)==ProcessDefC) && !TestOptionT &&
       (TestOptionA || TestOptionD || TestOptionE || TestOptionS)) {
     dp = LookNameB(root);
     PutP_def(dp,CopyMovePath());
     TestExpand(bb,depth,sed,TestOptionT,TestOptionA,TestOptionD,TestOptionE,
		TestOptionS,proc,TestOptionV,
		TestOptionY,!TestOptionI,
		(TestOptionI ? FALSE : IsCursorAt_WBE_Context()),
		expected_response, TestOptionQ,
		percent, seed, bhtsz, PartOptionG,
		vl );
     FreeB(UnshareB(GetP_def(dp)));
     PutP_def(dp,UnshareB(root));
   }
   else {
     TestExpand(bb,depth,sed,TestOptionT,TestOptionA,TestOptionD,TestOptionE,
		TestOptionS,proc,TestOptionV,
		TestOptionY,!TestOptionI,
		(TestOptionI ? FALSE : IsCursorAt_WBE_Context()),
		expected_response, TestOptionQ,
		percent, seed, bhtsz, PartOptionG,
		vl );
   }
   if ( !TestOptionT &&
	(TestOptionA || TestOptionD || TestOptionE || TestOptionS ) )
     GlueB( b, bb );
   else {
     FreeB( bb );
   }
 }
}



/******************************************************************
*
*  Command: One Expand.
*
*******************************************************************/

static boolean opcVone,opcIone;


static void echo_one(depth,success,process,seed,contopcio,lst_opcio,execs)
    int  depth,seed,contopcio,execs;
    char *success,*lst_opcio,*process;
{
 int i;

 opcVone = (boolean)Default("verbose");
 opcIone = (boolean)Default("expand_i_removal");
 if ( depth==UNDEFINED )
   depth = (int)Default("exploration_depth");
 if (success[0]!=NUL)				/* KJT 18/05/02: NULL -> NUL */
   success = (char*)Default("success_event");
 printMsgs("oneexpand ");
 PrintInt(printMsgs,depth);
 printMsgs(" ");
 if (success[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(success);
   printMsgs(" ");
 }
 if (process[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(process);
   printMsgs(" ");
 }
 PrintInt(printMsgs,seed);
 printMsgs(" ");
 PrintInt(printMsgs,execs);
 for (i=0 ; i != contopcio ; i++) {
   if (lst_opcio[i]=='v') {
     opcVone = TRUE;
   }
   if (lst_opcio[i]=='i') {
     opcIone = TRUE;
   }
 }
 if ( opcVone )
   printMsgs(" -v");
 if ( opcIone )
   printMsgs(" -i");
 printMsgs("\n\n");
}



/* ECone
* Executes the command oneExpand.
* depth is the expansion depth.
* success is the name of the success event.
* process is the name of the test process.
* seed is the seed for a ramdon number generator.
* contopcio is the number of options in lst_opcio.
* lst_opcio is the list of options.
*
* return the random number generated by the seed
*/
int ECone( depth,success,process,seed,contopcio,lst_opcio,execs )
    int  depth,seed,contopcio,execs;
    char *success,*lst_opcio,*process;
{
 BehTyp b;
 DescriptorTyp sed,proc;

 if ( success[0]=='\0' )
   success = (char*)Default("success_event");

 echo_one(depth,success,process,seed,contopcio,lst_opcio,execs);

 sed = GetSuccessEvent(success);
 if ( sed ==-1 )
   return seed;

 if ( sed==0 && process[0]!='\0' ){
   printError("\n      \nMissing argument success event or test.\n");
   printError("A success event can be defined either as a OneExpand parameter\n");
   printError("      or by means of the Set command ( e.g. lola> set success_event test_ok ).\n\n");
   return seed;
 }
 if ((proc=GetTestProcess(process))==-1 )
   return seed;
 if ( sed>0 && proc==0){ /* xlola case */
   printError("\nWith a success event, a test process is compulsory.\n");
   return seed;
 }
 if (GetCursor()==NULL) {
   printError("      A Specification must be loaded first.\n\n");
   return seed;
 }
 b = MvCursorBeh();
 Rw_Spec();
 Expandable((boolean)Default("divergence_check"),
	     (boolean)Default("unguarded_proc_check"));
 RemoveDepurationInfo();

 if (sed==0) {
   b = ShareB(CopyB(b));
 }
 else {
   printMsgs("  Composing behaviour and test : \n\n");
   b = Compose_b_with_Test(b,proc,sed);
   if ( b==NULL ) {
     return seed;
   }
   PrintBeh(b,-1,NO_PROC,FALSE,"   ",printTarget,TRUE,FALSE);
   printTarget("\n");
   b = ShareB(b);
 }

 seed = OneExpand( b, depth, sed, proc, seed, opcVone, !opcIone,
		  (opcIone ? FALSE : IsCursorAt_WBE_Context()) );
 printTarget("\n");
 FreeB(UnshareB(b));

 return seed;
}




/******************************************************************
*
*  Command: Interleaved Expansion.
*
*******************************************************************/

static boolean ITopcionDup, ITopcionParam, ITopcionVerb;

static void check_opcion_iexpand(contopcio,lst_opcio)
    int contopcio;
    char *lst_opcio;
{
 int i;

 ITopcionDup   = FALSE;
 ITopcionParam = FALSE;
 ITopcionVerb  = (boolean)Default("verbose");
 for (i=0 ; i != contopcio ; i++) {
   if (lst_opcio[i]=='d')
     ITopcionDup = TRUE;
   if (lst_opcio[i]=='p')
     ITopcionParam = TRUE;
   if (lst_opcio[i]=='v')
     ITopcionVerb = TRUE;
 }

}



static void echo_iexpand(num,ident,process)
    int num;
    char * ident, * process;
{
 printMsgs("InterExpand ");
 PrintInt(printMsgs,num);
 printMsgs(" ");
 if (ident[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(ident);
   printMsgs(" ");
 }
 if (process[0]!=NUL) {			/* KJT 18/05/02: NULL -> NUL */
   printMsgs(process);
   printMsgs(" ");
 }
 if (ITopcionParam)
   printMsgs("-p ");
 if (ITopcionDup)
   printMsgs("-d ");
 if (ITopcionVerb)
   printMsgs("-v ");

 printMsgs("\n\n");
}


/* ECit
* Executes the command interleaved expansion.
* depth is the iexpansion depth in synchronizations depth.
* success is the name of the success event.
* process is the name of the test process.
* contopcio is the number of options and lst_opcio is the list
* of options.
*/
void ECit(contopcio,depth,success,process,lst_opcio)
    int contopcio,depth;
    char *success, *process, *lst_opcio;
{
 BehTyp b,bb, root;
 DescriptorTyp dp, sed,proc;

 check_opcion_iexpand(contopcio,lst_opcio);
 if ( depth==UNDEFINED )
   depth = (int)Default("exploration_depth");
 echo_iexpand(depth,success,process);
 if ((sed=GetSuccessEvent(success))==-1)
   return;
 if ((proc=GetTestProcess(process))==-1 )
   return;
 b = MvCursorBeh();
 if (b!=NULL) {
   Rw_Spec();
   Expandable((boolean)Default("divergence_check"),
	       (boolean)Default("unguarded_proc_check"));
   RemoveDepurationInfo();

   if (process[0]!=NUL) {			/* KJT 18/05/02: NULL -> NUL */
     printMsgs("  Composing behaviour and test :\n\n");
     bb = Compose_b_with_Test(b,proc,sed);
     if ( bb==NULL ) {
       return;
     }
     PrintBeh(bb,-1,NO_PROC,FALSE,"   ",printTarget,TRUE,FALSE);
     printTarget("\n");
   }
   else
     bb = CopyB(b);
   root = GetRoot();
   if ((LookTypeB(root)==ProcessDefC) &&
       (TestOptionA || TestOptionD || TestOptionE || TestOptionS)) {
     dp = LookNameB(root);
     PutP_def(dp,CopyMovePath());
     InterExpand( bb, depth, sed, proc, ITopcionDup, ITopcionParam,
		 ITopcionVerb);
     FreeB(UnshareB(GetP_def(dp)));
     PutP_def(dp,UnshareB(root));
   }
   else
     InterExpand( bb, depth, sed, proc, ITopcionDup, ITopcionParam,
		 ITopcionVerb);
   /*    if ( TestOptionA || TestOptionD || TestOptionE || TestOptionS ) */
   GlueB( b, bb );
   /*    else {
	 FreeB( bb );
	 }
	 */
 }
 else
   printError("      There is not any tree to iexpand.\n\n");
}


/******************************************************************
*
*  Command: Statistic.
*
*******************************************************************/


/* ECstat
* Executes the command statistic.
*/
void ECstat()
{
 printTarget("statistics\n\n");
 Statistic();
}

/******************************************************************
*
*  Command: Quit.
*
*******************************************************************/

/* ECquit
* Executes the command quit.
*/
void ECquit()
{
 printTarget("quit\n\n");
 gl_cleanup();
 EXITLOLA(NORMALQUIT);
}

/******************************************************************
*
*  Command: Rewrite.
*
*******************************************************************/

/* ECrewrite
* Executes the command eval.
* expr is a data value expression.
*/
void ECrewrite( expr )
    ExprTyp expr;
{
 if (expr!=NULL) {
   Rw_Rules();
   printTarget("  rewrite ");
   PrintE(expr,printTarget);
   printTarget("\n\n");
   expr = Rewrite(expr);
   PrintE(expr,printTarget);
   FreeE(expr);
   printTarget("\n\n");
 }
}

/******************************************************************
*
*  Command: Set.
*
*******************************************************************/


/*  EnvVarNameTyp
*  Pairs var name and value.
*/
typedef struct Cell_EnvVar { char *  env_var;       /* var name              */
			    void *  value;         /* current var value     */
			    void *  default_value; /* initial value         */
			    char *  (*sprint)();   /* value sprint function */
			    boolean (*parse)();    /* value check function  */
			  } EnvVarTyp;

static char str[128];

#define MAXENVTAB 14

/* EnvVariableTable
*
*/
static EnvVarTyp EnvVarTable[] = {
 "divergence_check",       (void*)OFF, (void*)OFF,  SPSwitch, ParseSwitch,
 "unguarded_proc_check",   (void*) ON, (void*) ON,  SPSwitch, ParseSwitch,
 "print_depth",            (void*)  4, (void*)  4,  SPInt,    ParseInt,
 "print_types",            (void*)OFF, (void*)OFF,  SPSwitch, ParseSwitch,
 "print_proc",             (void*)OFF, (void*)OFF,  SPSwitch, ParseSwitch,

 "verbose",                (void*)OFF, (void*)OFF,  SPSwitch, ParseSwitch,
 "expand_i_removal",       (void*)OFF, (void*)OFF,  SPSwitch, ParseSwitch,
 "exploration_depth",      (void*) -1, (void*) -1,  SPInt,    ParseInt,
 "success_event", (void*)ALIGN(""), (void*)ALIGN(""),  SPString, ParseString,
 "test_i_removal",         (void*) ON, (void*) ON,  SPSwitch, ParseSwitch,
 "quit_exploration_on_may_response",
 (void*) ON, (void*) ON,   SPSwitch, ParseSwitch,
 "expected_response",
 (void*)UNDEFINED,(void*)UNDEFINED, SPResp, ParseResp,
 "quit_lola_on_unexpected_response",
 (void*)OFF, (void*)OFF, SPSwitch, ParseSwitch,
 "memory_size",             (void*)  1, (void*)  1, SPInt,    ParseInt
};

/* LookUpEnvVar
* return the position of var in the env var table
* return -1 if var is not in the table
*/
static int LookUpEnvVar(var)
    char * var;
{
 int i;

 for ( i=MAXENVTAB-1; i>=0; i-- )
   if ( strcmp(EnvVarTable[i].env_var,var)==0 )
     break;
 return i;
}

/* SPString
* sprints a string into str.
*/
static char * SPString( s )
    char *s;
{
 (void)sprintf(str,"%s",s);
 return str;
}

/* SPInt
* sprints the integer "i" into str.
*/
static char * SPInt( i )
    int    i;
{
 (void)sprintf(str,"%d",i);
 return str;
}

/* SPSwitch
* sprints a boolean into str
*/
static char * SPSwitch( i )
    boolean    i;
{
 if ( i )
   (void)sprintf(str,"ON");
 else
   (void)sprintf(str,"OFF");
 return str;
}


/* SPResp
* sprints a test response into str.
*/
static char * SPResp( tr )
    int tr;
{
 switch ( tr ){
 case MUST:
   (void)sprintf(str,"MUST");
   break;
 case MAY:
   (void)sprintf(str,"MAY");
   break;
 case REJECT:
   (void)sprintf(str,"REJECT");
   break;
 case UNDEFINED:
   (void)sprintf(str,"");
   break;
 default:
   Error("unexpected variable value");
 }
 return str;
}


/* ParseSwitch
* leave *value unchanged if the value is not right and return FALSE
*/
static boolean ParseSwitch( s, value )
    char * s;
    boolean *value;
{
 LowerString(s);
 if ( strcmp(s,"on")==0 ){
   *value = ON;
   return TRUE;
 }
 else
   if ( strcmp(s,"off")==0 ){
     *value = OFF;
     return TRUE;
   }
   else
     return FALSE;
}

/* ParseString
* leave *value unchanged if the value is not right and return FALSE
*/
static boolean ParseString( s, value )
    char * s;
    char **value;
{
 LowerString(s);
 *value = s;
 return TRUE;
}

/* ParseInt
* leave *value unchanged if the value is not right and return FALSE
*/
static boolean ParseInt( s, value )
    char * s;
    int *value;
{
 if ( sscanf(s,"%d\0",value) == 0 )		/* KJT 18/05/02: NULL -> 0 */
   return FALSE;
 else
   return TRUE;
}


/* ParseResp
* leave *value unchanged if the value is not right and return FALSE
*/
static boolean ParseResp( s, value )
    char * s;
    int *value;
{
 LowerString(s);
 if ( strcmp(s,"must")==0 ){
   *value = MUST;
   return TRUE;
 }
 else
   if ( strcmp(s,"may")==0 ){
     *value = MAY;
     return TRUE;
   }
   else
     if ( strcmp(s,"reject")==0 ){
       *value = REJECT;
       return TRUE;
     }
     else
       if ( s[0]=='\0' ){
	 *value = UNDEFINED;
	 return TRUE;
       }
 return FALSE;
}


static void SetVariableEnv( var, value )
    char * var, * value;
{
 int i;

 i = LookUpEnvVar(var);
 if ( i<0 ){
   printError("\n      ");
   printError(var);
   printError(" : Unknown variable name.\n\n");
   return;
 }
 if ( !EnvVarTable[i].parse( value, &EnvVarTable[i].value ) ) {
   printError("\n      ");
   printError( value );
   printError(" : Invalid variable value.\n\n");
   return;
 }
}

static void     DisplayEnv( pstr )
    void (*pstr)();
{
 int i,j;

 for ( i=0; i<MAXENVTAB; i++ ){
   pstr("\n   ");
   pstr(EnvVarTable[i].env_var);
   for ( j=strlen(EnvVarTable[i].env_var); j<=50; j++)
     pstr(" ");
   pstr(EnvVarTable[i].sprint(EnvVarTable[i].value));
 }
 pstr("\n");
}

/* ResetVariableEnv
* reset a variable to its initialization value
*/
static void     ResetVariableEnv( var )
    char *var;
{
 int i;

 i = LookUpEnvVar(var);
 if ( i<0 ){
   printError("\n      ");
   printError(var);
   printError(" : Unknown variable name.\n\n");
   return;
 }
 else {
   EnvVarTable[i].value = EnvVarTable[i].default_value;
 }
}

static void echo_set(var,value)
    char * var, * value;
{
 printMsgs("set ");
 if (var[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(var);
   printMsgs(" ");
 }
 if (value[0]!=NUL) {				/* KJT 18/05/02: NULL -> NUL */
   printMsgs(value);
 }
 printMsgs("\n");
}

/* Default
* return the defult value being given by the environment variables
*/
void * Default( var )
    char * var;
{
 int i = LookUpEnvVar(var);
 if ( i<0 )
   Error("Unknown variable");
 return EnvVarTable[i].value;
}

/* ECset
* Executes the command Set.
* Set a LoLa customization variable to a value.
*/
void ECset( var, value )
    char *var, *value;
{
 echo_set( var, value );
 if ( var[0]=='\0' )
   DisplayEnv( printMsgs );
 else
   if ( value[0]=='\0' )
     ResetVariableEnv( var );
   else
     SetVariableEnv( var, value );
 printMsgs("\n");
}


/******************************************************************
*
*  command: Command : read a LOLA command file
*
*******************************************************************/

static void echo_cmd( file_name )
    char * file_name;
{
 printMsgs("command ");
 printMsgs(file_name);
 printMsgs("\n");
}


/* ECcmd
* Executes the command Cmd which executes a file cmd_file.
*/
void ECcmd( cmd_file )
    char *cmd_file;
{
 FILE *cfd;
 char line[BUF_SIZE];

 echo_cmd( cmd_file );

 if ((cfd = fopen(cmd_file,"r")) == NULL ) {
   printError("\n      I can not open file <");
   printError(cmd_file);
   printError(">.\n");
   return;
 }

 while ( fgets(line,BUF_SIZE-1,cfd) != NULL ) {
   CommandLineInt( line );
 }

}


#ifdef INVEXP

/******************************************************************
*
*  command: Visible Communication Inverse Expansion.
*
*******************************************************************/



/* Echo_vis_co
* Echoes the command line.
*/
static void Echo_vis_com( lgl1, gl1, lgl2, gl2 )
    char   *gl1[], *gl2[];
    int    lgl1, lgl2;
{
 int i;

 printMsgs("vc ");
 for (i=0 ; i<lgl1 ; i++) {
   printMsgs(gl1[i]);
   printMsgs(" ");
 }
 printMsgs(", ");
 for (i=0 ; i<lgl2 ; i++) {
   printMsgs(gl2[i]);
   printMsgs(" ");
 }
 printMsgs("\n\n");
}


/* ECvis_com
* Executes the command for visible communication decomposition.
*/
void ECvis_com( lgl1, gl1, lgl2, gl2 )
    char   *gl1[], *gl2[];
    int    lgl1, lgl2;
{
 GateSetTyp gs1,gs2,gsb,gsjunct;
 int i;
 DescriptorTyp gd;
 BehTyp b;

 Echo_vis_com( lgl1, gl1, lgl2, gl2 );
 gs1 = NewGS();
 gs2 = NewGS();
 gsb = NewGS();

 for (i=0 ; i<lgl1 ; i++) {
   gd = FindG( gl1[i] );
   if (gd==0) {
     printError("\n      ");
     printError(gl1[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs1);
     FreeGS(gs2);
     FreeGS(gsb);
     return;
   }
   else
     gs1 = AddGS(gs1,gd);
 }
 for (i=0 ; i<lgl2 ; i++) {
   gd = FindG( gl2[i] );
   if (gd==0) {
     printError("\n      ");
     printError(gl2[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs2);
     FreeGS(gs1);
     FreeGS(gsb);
     return;
   }
   else
     gs2 = AddGS(gs2,gd);
 }

 b = GetCursor();
 LASSERT(b != NULL);
 if ( (LookTypeB(b)==SpecificationC) || (LookTypeB(b)==ProcessDefC) )
   b = LookArgB(b,1);

 gsjunct=JunctionGS(gs1,gs2);
 gsb = GetGates(b);
 if (!SubSetGS(gsb,gsjunct)) {
   printError("\n      There are not all the gates.\n\n");
   FreeGS(gs1);
   FreeGS(gs2);
   FreeGS(gsb);
   FreeGS(gsjunct);
   return;
 }
 FreeGS(gsb);
 FreeGS(gsjunct);

 Rw_Spec();
 Expandable(Default("divergence_check"),Default("unguarded_proc_check"));
 RemoveDepurationInfo();

 Rec_InvExp( b,gs1,gs2 );

 FreeGS(gs1);
 FreeGS(gs2);
}



/******************************************************************
*
*  command: Non Recursive Visible Communication Inverse Expansion.
*
*******************************************************************/



/* ECvc_nrec
* Executes the command for non recursive visible communication decomposition.
*/
void ECvc_nrec( lgl1, gl1, lgl2, gl2 )
    char   *gl1[], *gl2[];
    int    lgl1, lgl2;
{
 GateSetTyp gs1,gs2,gsb,gsjunct;
 int i;
 DescriptorTyp gd;
 BehTyp b;

 Echo_vis_com( lgl1, gl1, lgl2, gl2 );
 gs1 = NewGS();
 gs2 = NewGS();
 gsb = NewGS();

 for (i=0 ; i<lgl1 ; i++) {
   gd = FindG( gl1[i] );
   if (gd==0) {
     printError("\n      ");
     printError(gl1[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs1);
     FreeGS(gs2);
     FreeGS(gsb);
     return;
   }
   else
     gs1 = AddGS(gs1,gd);
 }
 for (i=0 ; i<lgl2 ; i++) {
   gd = FindG( gl2[i] );
   if (gd==0) {
     printError("\n      ");
     printError(gl2[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs1);
     FreeGS(gs2);
     FreeGS(gsb);
     return;
   }
   else
     gs2 = AddGS(gs2,gd);
 }

 b = GetCursor();
 LASSERT(b != NULL);
 if ( (LookTypeB(b)==SpecificationC) || (LookTypeB(b)==ProcessDefC) )
   b = LookArgB(b,1);

 gsjunct=JunctionGS(gs1,gs2);
 gsb = GetGates(b);
 if (!SubSetGS(gsb,gsjunct)) {
   printError("\n      There are not all the gates.\n\n");
   FreeGS(gs1);
   FreeGS(gs2);
   FreeGS(gsb);
   FreeGS(gsjunct);
   return;
 }
 FreeGS(gsb);
 FreeGS(gsjunct);

 Rw_Spec();
 Expandable(Default("divergence_check"),Default("unguarded_proc_check"));
 RemoveDepurationInfo();

 VC_nrec( b,gs1,gs2 );

 FreeGS(gs2);
 FreeGS(gs1);
}

/******************************************************************
*
*  command: K - Inverse Expansion.
*
*******************************************************************/



/* ECk
* Executes the command for k - decomposition.
*/
void ECk( lgl1, gl1, lgl2, gl2 )
    char   *gl1[], *gl2[];
    int    lgl1, lgl2;
{
 GateSetTyp gs1,gs2,gsb,gsjunct;
 int i;
 DescriptorTyp gd;
 BehTyp b;

 Echo_vis_com( lgl1, gl1, lgl2, gl2 );
 gs1 = NewGS();
 gs2 = NewGS();
 gsb = NewGS();

 for (i=0 ; i<lgl1 ; i++) {
   gd = FindG( gl1[i] );
   if (gd==0) {
     printError("\n      ");
     printError(gl1[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs1);
     FreeGS(gs2);
     FreeGS(gsb);
     return;
   }
   else
     gs1 = AddGS(gs1,gd);
 }
 for (i=0 ; i<lgl2 ; i++) {
   gd = FindG( gl2[i] );
   if (gd==0) {
     printError("\n      ");
     printError(gl2[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs1);
     FreeGS(gs2);
     FreeGS(gsb);
     return;
   }
   else
     gs2 = AddGS(gs2,gd);
 }

 b = GetCursor();
 LASSERT(b != NULL);
 if ( (LookTypeB(b)==SpecificationC) || (LookTypeB(b)==ProcessDefC) )
   b = LookArgB(b,1);

 gsjunct=JunctionGS(gs1,gs2);
 gsb = GetGates(b);
 if (!SubSetGS(gsb,gsjunct)) {
   printError("\n       There are not all the gates.\n\n");
   FreeGS(gs1);
   FreeGS(gs2);
   FreeGS(gsb);
   FreeGS(gsjunct);
   return;
 }
 FreeGS(gsb);
 FreeGS(gsjunct);

 Rw_Spec();
 Expandable(Default("divergence_check"),Default("unguarded_proc_check"));
 RemoveDepurationInfo();

 Kdecomp( b,gs1,gs2 );

 FreeGS(gs2);
 FreeGS(gs1);
}


/******************************************************************
*
*  Command: Pure Interleaving Inverse Communication.
*
*******************************************************************/

/* Echo_pure_int
* Echoes the command line.
*/
static void Echo_pure_int( lgl, gl )
    char   *gl[];
    int    lgl;
{
 int i;

 printMsgs("pi ");
 for (i=0 ; i<lgl ; i++) {
   printMsgs(gl[i]);
   printMsgs(" ");
 }
 printMsgs("\n\n");
}


/* ECpure_int
* Executes the command for pure interleaving decomposition.
*/
void ECpure_int( lgl,gl )
    char * gl[];
    int    lgl;
{
 GateSetTyp gs1;
 int i;
 DescriptorTyp gd;
 BehTyp b;

 Echo_pure_int( lgl, gl );
 gs1 = NewGS();
 for (i=0 ; i<lgl ; i++) {
   gd = FindG(gl[i]);
   if (gd==0) {
     printError("\n      ");
     printError(gl[i]);
     printError(": Unknown gate name.\n\n");
     FreeGS(gs1);
     return;
   }
   else
     gs1 = AddGS(gs1,gd);
 }

 b = GetCursor();
 LASSERT(b != NULL);
 if  (LookTypeB(b)==SpecificationC)
   b = LookArgB(b,1);
 if  (LookTypeB(b)==ProcessDefC)
   b = LookArgB(b,1);


 Rw_Spec();
 Expandable(Default("divergence_check"),Default("unguarded_proc_check"));
 RemoveDepurationInfo();

 PI_nrec( b,gs1 );

 FreeGS(gs1);
}


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

#endif /* INVEXP */
