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

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

  Santiago Pavon Gomez

  16 October 1992

  Commands related with the STEP mode.

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

/* LINTLIBRARY */

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

/* KJT 12/02/12: Added */
#include <stdlib.h>
#include "batables.h"
#include "balotosf.h"
#include "baprint.h"
#include "ststep.h"
#include "bamove.h"
#include "incomm.h"
#include "exexpans.h"
#include "babeh.h"
#include "badefca.h"
#include "batyperw.h"
#include "exdiver.h"
#include "eximmed.h"
#include "expre_br.h"
#include "basust_v.h"
#include "basynset.h"

/* KJT 22/01/23: added function prototypes */
boolean ReadExpr(char * prompt, ExprTyp * pe, DescriptorTyp expSort);

/******************************************************************
 *                                                                *
 * STEP BY STEP mode.                                             *
 *                                                                *
 * Types and functions used to simulate a behaviour.              *
 *                                                                *
 *******************************************************************/

/* StepNodeTyp
 *
 * Nodes to store the behaviours and event simulated with the command STEP.
 *
 * init_beh -> Initial behaviour to simulate.
 * exp_beh  -> One level expanded behaviour
 * event    -> Chosen event.
 * event_num-> Chosen event branch.
 * nst      -> Alternative made with all the rejected synchronizations.
 */
typedef struct stepnode { BehTyp init_beh, exp_beh, event, nst;
			  int    event_num;
			} StepNodeTyp, *PStepNodeTyp;


/* step_nodes
 * Stack to store PStepNodeTyp.
 */
static StackTyp step_nodes = NULL;

/* stack_window
 * number of allowed undo's
 */
static int stack_window = -1;

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

/* Create_StepNode
 * Allocate memory for a new node.
 */
static PStepNodeTyp Create_StepNode()
{
  PStepNodeTyp pnn;

  pnn            = (PStepNodeTyp)emalloc(sizeof(StepNodeTyp));
  pnn->init_beh  = NULL ;
  pnn->exp_beh   = NULL ;
  pnn->event     = NULL ;
  pnn->nst       = NULL ;
  pnn->event_num = 0;
  return pnn;
}

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

/* Free_StepNode
 * Deallocate memory of node.
 */
static void Free_StepNode(pnn)
     PStepNodeTyp pnn;
{
  if (pnn->init_beh != NULL) {
    pnn->init_beh = UnshareB(pnn->init_beh);
    FreeB(pnn->init_beh);
  }
  if (pnn->exp_beh != NULL) {
    pnn->exp_beh = UnshareB(pnn->exp_beh);
    FreeB(pnn->exp_beh);
  }
  if (pnn->event != NULL) {
    pnn->event = UnshareB(pnn->event);
    FreeB(pnn->event);
  }
  if (pnn->nst != NULL) {
    pnn->nst = UnshareB(pnn->nst);
    FreeB(pnn->nst);
  }
  (void)free((char*)pnn);
}

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

/* Save_StepNode
 * Stores a node in the stack "step_nodes".
 */
#define Save_StepNode(n) {step_nodes = Save_Stack((DataStackTyp)n,step_nodes);}


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

/* StepOK
 * Returns TRUE if "n" is an existing option event.
 */
static boolean StepOK(b,n)
     BehTyp b;
     int n;
{
  if (LookTypeB(b) != AlternativeC)
    return n==1;
  else
    return ((n<=NumArgB(b)) && (n>0));
}


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

static int ReturnNameE(e)
     ExprTyp e;
{
  return LookNameE(e);
}

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

/* ReadValues
 * Read values (strings) for the variables in the list "dvl".
 * It also fills the table "*psv" with the read values.
 */
static void ReadValues(dvl,psv)
     ListTyp dvl;
     SVdescriptorTyp *psv;
{
  char *prompt, *strv;
  ListTyp hdvl;
  DescriptorTyp nv;
  ExprTyp e;

  LASSERT(dvl!=NULL);

  for (hdvl = dvl ; hdvl!=NULL ; hdvl = Next_list(hdvl)) {
    nv = (DescriptorTyp)LookInfo_list(hdvl);
    strv = SPrintV(nv,TRUE);
    prompt = (char*)emalloc(7+strlen(strv));
    (void)sprintf(prompt,"   %s = ",strv);
    (void)free(strv);
    while (!ReadExpr(prompt,&e,GetV_sort(nv)))
      ;
    free(prompt);
    if (e!=NULL)
      InsertSV(nv,Rewrite(e),psv);
  }
}



/******************************************************************
 *
 *  Start the StepByStep mode.
 *
 *******************************************************************/

static boolean StepOptionU; /* number of enabled undo's specified */
static boolean StepOptionT; /* trace disabled */
static boolean StepOptionD; /* debugging information disabled */

static void echo_step(success,process,contopcio,lst_opcio,undos)
     char *success,*process;
     int contopcio;
     char *lst_opcio;
     int undos;
{
  int i;

  StepOptionU = FALSE;
  StepOptionT = FALSE;
  StepOptionD = FALSE;
  for (i=0 ; i != contopcio ; i++)
    if (lst_opcio[i]=='u')
      StepOptionU = TRUE;
    else
      if (lst_opcio[i]=='t')
	StepOptionT = TRUE;
      else
	if (lst_opcio[i]=='d')
	  StepOptionD = TRUE;

  printMsgs("step ");
  if (success[0]!='\0') {
    printMsgs(success);
    printMsgs(" ");
    printMsgs(process);
    printMsgs(" ");
  }
 if (StepOptionU){
   printMsgs("-u ");
   PrintInt(printMsgs,undos);
   printMsgs(" ");
 }
 if (StepOptionD){
   printMsgs("-d ");
 }
 if (StepOptionT){
   printMsgs("-t ");
 }
  printMsgs("\n\n");
}

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

/* Append_Choice_Beh
 * Returns the behaviour of a specification or process definition preceeded
 * with a choice operator.
 * The choice operator will contain all the variable parameters definition
 * if they exist.
 */
static BehTyp Append_Choice_Beh(b)
     BehTyp b;
{
  BehTyp cho;
  PAttrTyp a;

  LASSERT(b!=NULL);
  LASSERT((LookType(b)==SpecificationC) || (LookType(b)==ProcessDefC));
  a = LookA(b,ELA);
  if (a!=NULL) {
    cho = MakeB(0,ChoiceC);
    PutA(cho,a);
    PutArgB(cho,LookArgB(b,1),1);
    return cho;
  }
  return LookArgB(b,1);
}

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

/* ECstep_start_CheckBehEventTest
 * This is the first function to invoke when switching LOLA into
 * the simulation mode.
 * This function checks that both the success event and the test process
 * exist, that a specification has been loaded.
 * Returns TRUE if these conditions are satisfied.
 * In "psed" and "pproc" returns the descriptors of the success event and
 * the test process.
 * It also calls to Rw_Spec() and Expandable().
 * undos is the number of undo's allowed during a simulation session.
 */
boolean ECstep_start_CheckBehEventTest( success, process, psed, pproc,
					contopcio, lst_opcio, undos )
     char *success, *process;
     DescriptorTyp *psed, *pproc;
     int contopcio;
     char *lst_opcio;
     int undos;
{

  echo_step(success,process,contopcio,lst_opcio,undos);

  if ( IsRemovedDepInfo() )
    /* KJT 16/03/98: message changed */
    Warning("Specification is not current. Use load to restore it.");

  /* Both success and process must be null or not null. */
  /*
     if ( (success[0]=='\0') && (process[0]!='\0') ) {
     printError("\n      Please, fill in the Success Event name.\n\n");
     return FALSE;
     }
     if ( (success[0]!='\0') && (process[0]=='\0') ) {
     printError("\n      Please, fill in the Test Process name.\n\n");
     return FALSE;
     }
     */

  if ( success[0]=='\0' && (process[0]!='\0') )
    success = (char*)Default("success_event");
  *psed = GetSuccessEvent(success);
  if ( *psed ==-1 )
    return FALSE;
  if ( *psed==0 && (process[0]!='\0') ){
    printError("\n      ");
    printError("A success event must be defined either as a Step parameter\n");
    printError("      or by means of the Set command ( e.g. lola> set success_event test_ok ).\n\n");
    return FALSE;
  }

  if ((*pproc=GetTestProcess(process))==-1 )
    return FALSE;

  if ((GetCursor())==NULL) {
    printError("      A Specification must be loaded first.\n\n");
    return FALSE;
  }

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

  return TRUE;
}

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

/* ECstep_start_GetUnassignedVars
 * If the current behaviour (cursor) is either a process definition or
 * a specification cell, then this function returns a list with all the
 * descriptors of the variables defined in the formal parameter list.
 * If not, returns NULL.
 */
ListTyp ECstep_start_GetUnassignedVars()
{
  BehTyp   b;
  PAttrTyp a;

  b = GetCursor();
  LASSERT(b!=NULL);

  if ((LookTypeB(b)==SpecificationC) || (LookTypeB(b)==ProcessDefC)) {
    a = LookA(b,ELA);
    if (a!=NULL) {
      return Join_list(Create_list(),
		       Copy_list((ListTyp)LookAInfo(a),
				 (DataListTyp(*)())ReturnNameE));
    }
  }
  return NULL;
}

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

/* ECstep_start_ReadParameters
 * Read values (strings) for the variables in the list "varList"
 * and fills the SVdescriptorTyp table "psv" with the values read.
 */
void ECstep_start_ReadParameters(varList,psv)
     ListTyp varList;
     SVdescriptorTyp *psv;
{
  if (varList!=NULL) {
    printMsgs("\n  Enter expressions for the variable definitions ");
    printMsgs("(CR for none):\n");
    ReadValues(varList,psv);
  }
}

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

/* ECstep_start_Behaviour
 * If "psv" is not empty then creates a "let" with the values in "psv"
 * and add the "let" operator before the current behaviour. Then returns
 * the behaviour: let + the current behaviour.
 * If it is empty then return the current behaviour.
 */
BehTyp ECstep_start_Behaviour(psv)
     SVdescriptorTyp *psv;
{
  VarAssignListTyp val;
  BehTyp let,b;

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

  val = Make_VAL_SV(psv);
  if (val!=NULL) {
    let = MakeB(0,LetC);
    PutA(let,MakeA((AttrValueTyp)val,VALA));
    AddArgB(let,b);
    b = let;
  }
  return b;
}

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

/* ECstep_start_ComposeWithTest
 * This function composes the behavior "b" with the test process
 * if it is specified. If the test process is not specified then it
 * returns "b".
 * If there is any problem the function returns NULL, otherwise
 * returns the behaviour to simulate.
 */
BehTyp ECstep_start_ComposeWithTest( b, sed, proc )
     BehTyp b;
     DescriptorTyp sed,proc;
{
  BehTyp b2;

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

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

/* ECstep_start_Expan
 * "b" is the behaviour in the first step of the simulation process.
 * This function calculates the first set of transitions offered.
 * undos_num is a limit to the number of undo's available during a simulation.
 */
void ECstep_start_Expan(b,undos_num)
     BehTyp b;
     int    undos_num;
{
  PStepNodeTyp pnn;

  stack_window = undos_num;
  Free_Stack( step_nodes , Free_StepNode );
  step_nodes = Create_Stack();
  pnn        = Create_StepNode();
  Save_StepNode(pnn);
  pnn->init_beh = ShareB(b);
  pnn->exp_beh = ShareB(StepExpand(b,!StepOptionD));

#ifdef TIME
#ifdef ASAP
     pnn->exp_beh   = AsapT( pnn->exp_beh);
#endif
#endif

  pnn->nst = GetRefusedSync();
}


/******************************************************************
 *                                                                *
 * ECstep_branch                                                  *
 *                                                                *
 *******************************************************************/

/* ValidBranch
 * Returns TRUE if "n" is a valid transition in the current state.
 */
static boolean ValidBranch(n)
     int n;
{
  PStepNodeTyp pnn;
  int          numArg;
  BehTyp       b;

  pnn = (PStepNodeTyp)Look_Stack(step_nodes);
  b   = pnn->exp_beh;

  if ( (b==NULL) || (LookTypeB(b)==StopC) ) {
    printMsgs("\n   DEADLOCK\n\n");
    return FALSE;
  }
  LASSERT(b!=NULL);
  numArg = NumArgIB(b);
  if ( (n<0) || (!StepOK(b,n)) ) {
    printError("\n      Invalid transition. ( Valid range: 1..");
    PrintInt(printError,numArg);
    printError(" )\n\n");
    return FALSE;
  }

  return TRUE;
}

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


/* ECstep_branch_GetUnassignedVars
 * Returns a list with all the descriptors of the unassigned variables in
 * the choices and gate operators of the branch "n".
 */
ListTyp ECstep_branch_GetUnassignedVars(n)
     int n;
{
  PStepNodeTyp pnn;
  ListTyp      dvl;
  OfferListTyp ol;
  BehTyp       b;
#ifdef TIME
  PTimeTyp t;
#endif
  pnn    = (PStepNodeTyp)Look_Stack(step_nodes);
  b      = pnn->exp_beh;

  if (LookTypeB(b)==AlternativeC)
    b = LookArgB(b,n);
  LASSERT(b!=NULL);

  dvl  = Create_list();   /* list of defined variables until the action */
  while ( b!=NULL ) {
    switch ( LookTypeB(b) ) {
    case IC:
#ifdef TIME
      t = (PTimeTyp) LookAInfo(LookA(b,TA)) ;
      if ( (t->tvar !=NULL) &&
	  (!IsConstE(t->tvar)))
	dvl = Add_list((DataListTyp)LookNameE(t->tvar),dvl);
      b =  NULL;
      break;
#endif
    case StopC:
    case ExitC:
      b =  NULL;
      break;
    case ChoiceC:
      dvl = Join_list(dvl,
		      Copy_list((ListTyp)LookAInfo(LookA(b,ELA)),
				(DataListTyp(*)())ReturnNameE));
      b =  LookB1(b);
      break;
    case GuardC:
      b =  LookB1(b);
      break;
    case GateC:
      for (ol = (OfferListTyp)LookAInfo(LookA(b,OLA)) ;
	   ol != NULL ;
	   ol = MvNextOffer(ol))
	if (LookKindOffer(ol)==QUESTION)
	  dvl = Add_list((DataListTyp)LookNameE(LookExprOffer(ol)),dvl);
#ifdef TIME
      t = (PTimeTyp) LookAInfo(LookA(b,TA)) ;
      if ( (t->tvar !=NULL) &&
	  (!IsConstE(t->tvar)))
	dvl = Add_list((DataListTyp)LookNameE(t->tvar),dvl);
#endif
      b =  NULL;
      break;
    default :
      Error("ECstep_branch_GetUnassignedVars: unexpected cell.");
    }
  }
  return dvl;
}

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


/* Clean_Var_Choice
 * Removes all the variables assigned in "*psv" from the sequence of
 * choices operators pointed by "c".
 */
static void Clean_Var_Choice(c,psv)
     BehTyp c;
     SVdescriptorTyp *psv;
{
  ExprTyp v;
  ExprListTyp nvl,vl,vlh;
  PAttrTyp a;

  while (LookTypeB(c)==ChoiceC) {
    UnshareA(c,ELA);
    a = LookA(c,ELA);
    LASSERT(a!=NULL);
    vlh = (ExprListTyp)GetAInfo(a);
    nvl = CreateEL();
    for (vl = vlh ; vl!=NULL ; vl = Next_list(vl)) {
      v = (ExprTyp)LookInfo_list(vl);
      if (GetActExp_SV(LookNameE(v),psv)==NULL)
	nvl = AddEL(CopyE(v),nvl);  /*mse*/
    }
    FreeEL(vlh);
    if (nvl==NULL)
      GlueArgB(c,1);
    else {
      PutAInfo(a,(AttrValueTyp)nvl);
      c = LookArgB(c,1);
    }
  }
}


/* Clean_Var_Gate
 * Removes all the variables assigned in "*psv" from the offer list of
 * the gate pointed by "c".
 */
static void Clean_Var_Gate( c, psv )
     BehTyp          c;
     SVdescriptorTyp *psv;
{
  ExprTyp      v;
  OfferListTyp ol;

  UnshareA(c,OLA);
  for (ol=(OfferListTyp)LookAInfo(LookA(c,OLA));ol!=NULL;ol=MvNextOffer(ol))
    if (LookKindOffer(ol)==QUESTION) {
      v = LookExprOffer(ol);
      if (GetActExp_SV(LookNameE(v),psv)!=NULL)
	PutKindOffer(ol,EXCLAMATION);
    }
}


/* AssignVar_Choice_Gate
 * Applies the table "sv" to the behaviour "b" until actions.
 */
static BehTyp AssignVar_Choice_Gate(b,sv)
     BehTyp b;
     SVdescriptorTyp sv;
{
  BehTyp           act,let;
  VarAssignListTyp val;
#ifdef TIME
  PTimeTyp t;
  BehTyp   gd;
#endif

  if (!IsEmptySV(sv)) {
    if (LookTypeB(b)==ChoiceC)
      Clean_Var_Choice(b,&sv);
    act = LookActionUB(b);
    if ((LookTypeB(act)==GateC )
#ifdef TIME
	||  (LookTypeB(act)==IC)
#endif
	){
      if (LookTypeB(act)==GateC)
	  Clean_Var_Gate(act,&sv);
#ifdef TIME

      gd = NULL;
      t = (PTimeTyp) LookAInfo(LookA(act,TA));
      if ((t->tvar !=NULL) && (!IsConstE(t->tvar))) {
	gd = ChoiceT(LookNameE(t->tvar),t->lower_bound,t->upper_bound);
       if (gd !=NULL)    AddArgB(LookLastUB(gd),b);
      }
#endif
    }
    val = Make_VAL_SV(&sv);
    let = MakeB(0,LetC);
    PutA(let,MakeA((AttrValueTyp)val,VALA));

#ifdef TIME
    if (gd !=NULL)
      AddArgB(let,gd);
    else
#endif
      AddArgB(let,b);

    b = StepExpand(let,!StepOptionD);
  }
  return ShareB(b);
}


/* ECstep_branch_exec
 * Executes the n-th transition of the current simulation behaviour.
 * "n" must be a valid transition.
 * The Table "sv" is applied to the transition.
 */
void ECstep_branch_exec(n,sv)
     int n;
     SVdescriptorTyp sv;
{
  PStepNodeTyp pnn;
  BehTyp       b,ev;

  pnn = (PStepNodeTyp)Look_Stack(step_nodes);
  b   = pnn->exp_beh;
  LASSERT(n<=NumArgIB(b));

  if (LookTypeB(b)==AlternativeC)
    b = LookArgB(b,n);
  LASSERT(b!=NULL);

  pnn->event = ev = AssignVar_Choice_Gate(GetUntilActB(b),sv);
  pnn->event_num = n;

  printMsgs("\n");
  PrintBeh(ev,1,NO_PROC,FALSE,"  ==> ",printTarget,FALSE,FALSE);
  printMsgs("\n---------------------------------------------------------------------------\n\n");

  pnn = Create_StepNode();
  if (LookArgB(LookActionUB(ev),1)!=NULL) {
    pnn->init_beh = ShareB(LookArgB(LookActionUB(ev),1));
    pnn->exp_beh  = ShareB(StepExpand(pnn->init_beh,!StepOptionD));

#ifdef TIME
#ifdef ASAP
     pnn->exp_beh   = AsapT( pnn->exp_beh);
#endif
#endif
    if (pnn->nst==NULL)
      pnn->nst = GetRefusedSync();
    else
      FreeB(UnshareB(GetRefusedSync()));
  }
  if ( StepOptionT ) {
    /* trace disabled : remove previous node */
    LASSERT(Length_list(step_nodes)==1);
    Free_StepNode((PStepNodeTyp)Get_Stack(&step_nodes));
  }
  Save_StepNode(pnn);
}

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

/* ECstep_branch
 * Executes the n-th transition of the current simulation behaviour.
 */
void ECstep_branch(n)
     int n;
{
  ListTyp         varList;
  SVdescriptorTyp sv;
  PStepNodeTyp pnn;

  if (ValidBranch(n)) {
    varList = ECstep_branch_GetUnassignedVars(n);
    sv = CreateSV();
    if (varList!=NULL) {
      printMsgs("\n  Enter expressions for the variable definitions ");
      printMsgs("(CR for none):\n");
      ReadValues(varList,&sv);
    }
    ECstep_branch_exec(n,sv);
    FreeSV(&sv);
    Disp_list(varList);
    /**/
    /* free exceeded undo's */
    if ( stack_window >= 0 ){
      pnn = (PStepNodeTyp)LookN_Stack(step_nodes, stack_window+2);
      if ( pnn!=NULL ){
	if (pnn->event != NULL) {
	  /* pnn->event not freed, just the debugging info */
	  if ( LookA(pnn->event,STA)!=NULL ){
	    FreeA(GetA(pnn->event,STA));
	  }
	}
	if (pnn->init_beh != NULL) {
	  FreeB(UnshareB(pnn->init_beh));
	  pnn->init_beh = NULL;
	}
	if (pnn->exp_beh != NULL) {
	  FreeB(UnshareB(pnn->exp_beh));
	  pnn->exp_beh = NULL;
	}
	if (pnn->nst != NULL) {
	  FreeB(UnshareB(pnn->nst));
	  pnn->nst = NULL;
	}
      }
    }
    /**/
  }
}


/******************************************************************
 *                                                                *
 * ECmenu                                                         *
 *                                                                *
 *******************************************************************/


/* PrintStep
 * Prints the transitions offered by the one level expanded behaviour "b".
 */
static void PrintStep(b)
     BehTyp b;
{
  int i,n;
  char prompt[12];

  if (LookTypeB(b)==AlternativeC) {
    n = NumArgB(b);
    for (i=1 ; i<=n ; i++) {
      (void)sprintf(prompt," [%3d]  ",i);
      PrintBeh(LookArgB(b,i),1,NO_PROC,FALSE,prompt,printCursor,FALSE,FALSE);
    }
  }
  else {
    (void)sprintf(prompt," [%3d]  ",1);
    PrintBeh(b,1,NO_PROC,FALSE,prompt,printCursor,FALSE,FALSE);
  }
  printCursor("\n");
}

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

/* KJT 16/03/98: ECstep_menu_aux
 * Return number of branches
 */
int ECstep_menu_aux()
{
  PStepNodeTyp pnn;
  BehTyp b;
  pnn = (PStepNodeTyp)Look_Stack(step_nodes);
  b = pnn->exp_beh;
  if ((b==NULL) || (LookTypeB(b)==13)) {
    printCursor("\n   DEADLOCK\n\n");
    return (0);
  }
  else {
    printCursor("\n");
    PrintStep(b);
    return (NumArgB (b));
  }
}

/* KJT 16/03/98:
 * ECstep_menu
 * Displays a menu with the possible transitions.
 */
void ECstep_menu()
{
  int n;
  do {
    n = ECstep_menu_aux();
    if (n == 1)
      ECstep_branch (1);
  } while (n == 1);
}

/* ECstep_menu
 * Displays a menu with the possible transitions.
 */
void ECstep_menu_original()
{
  PStepNodeTyp pnn;
  BehTyp b;

  pnn = (PStepNodeTyp)Look_Stack(step_nodes);
  b = pnn->exp_beh;

  if ((b==NULL) || (LookTypeB(b)==StopC)) {
    printCursor("\n   DEADLOCK\n\n");
  }
  else {
    printCursor("\n");
    PrintStep(b);
  }
}


/******************************************************************
 *                                                                *
 *  ECstep_refused                                                     *
 *                                                                *
 *******************************************************************/

/* ECstep_ExistRefused
 * Returns TRUE is there are any refused synchronizations.
 */
boolean ECstep_ExistRefused()
{
  PStepNodeTyp pnn;
  BehTyp       b;

  pnn  = (PStepNodeTyp)Look_Stack(step_nodes);
  b    = pnn->nst;
  return b!=NULL;
}

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

static void PrintPartner( b )
     BehTyp b;
{
  if ( LookTypeB(b)==ParallelC ) {
    PrintPartner( LookArgB(b,1) );
    printCursor(",");
    PrintPartner( LookArgB(b,2) );
  }
  else {
    if ( LookA(b,SSLA)!=NULL ) {
      PrintInt(printCursor,(int)LookAInfo(LookA(b,SSLA)));
    }
    else
      printCursor("?");
  }
}

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

static void PrintActName( b )
     BehTyp b;
{
  switch( LookTypeB(b) )
    {
    case GateC:
      printCursor(GetG_name(LookNameB(b)));
      break;
    case ExitC:
      printCursor("exit");
      break;
    default:
      Error("ECstep_refused : unexpected cell type");
    }
}

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

/* ECstep_refused
 * Display the synchronizations refused due to data values (the menu).
 */
void ECstep_refused()
{
  int          i,numArgs;
  PStepNodeTyp pnn;
  BehTyp       b;
  char buff[15];

  pnn  = (PStepNodeTyp)Look_Stack(step_nodes);
  b    = pnn->nst;
  if ( b!=NULL ){
    numArgs = NumArgIB(b);
    for (i=1 ; i<=numArgs ; i++) {
      (void)sprintf(buff," [%4d]  ",-i);
      printCursor(buff);
      PrintActName(LookActionArgIB(b,i));
      printCursor(" (at lines ");
      PrintPartner(LookArgIB(b,i));
      printCursor(")\n");
    }
    printCursor("\n");
  }
  else {
    printMsgs("\n  No unsuccessful synchronizations at the current state.\n\n");
  }
}


/******************************************************************
 *                                                                *
 * ECstep_undo                                                         *
 * Undo the last simulation step.                                 *
 *                                                                *
 *******************************************************************/

/* ECstep_undo
 * Undo the last simulation step.
 * Returns TRUE if there was a step to be undone.
 */
boolean ECstep_undo()
{
  PStepNodeTyp pnn;
  BehTyp       next_init_beh;

  LASSERT(step_nodes!=NULL);

  /**/
  next_init_beh = NULL;
  if ( Next_list(step_nodes)!=NULL
      &&
      (next_init_beh =
       ((PStepNodeTyp)LookInfo_list(Next_list(step_nodes)))->init_beh)!=NULL
      ) {
  /**/
    pnn = (PStepNodeTyp)Get_Stack(&step_nodes);
    Free_StepNode(pnn);
    pnn        = (PStepNodeTyp)Look_Stack(step_nodes);
    pnn->event = UnshareB(pnn->event);
    FreeB(pnn->event);
    pnn->event     = NULL;
    pnn->event_num = 0;
    printMsgs("\n   Last simulation step undone.\n\n");
    return TRUE;
  }
  else {
    pnn = (PStepNodeTyp)Look_Stack(step_nodes);
    /**/
    if ( Next_list(step_nodes)==NULL ) {
      LASSERT(pnn->event==NULL);
      printMsgs("\n   No simulation step to undo.\n\n");
    }
    else {
      /**/
      LASSERT(next_init_beh==NULL);
      printMsgs("\n   Number of specified undo's exceeded.\n\n");
    }
    return FALSE;
  }
}


/******************************************************************
 *                                                                *
 * ECstep_trace                                                        *
 * Displays the trace of simulated events.                        *
 *                                                                *
 *******************************************************************/

static char event[16];

static void PrintSimEvents(st)
     StackTyp st;
{
  PStepNodeTyp pnn;

  if (st!=NULL) {
    PrintSimEvents(st->next);
    pnn = (PStepNodeTyp)Look_Stack(st);
    if (pnn->event!=NULL){
      (void)sprintf( event, " [%3d] - ", pnn->event_num );
      PrintBeh(pnn->event,1,NO_PROC,FALSE,event,printTarget,FALSE,FALSE);
    }
  }
}

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

/* ECstep_trace
 * Displays all the simulated events.
 */
void ECstep_trace()
{
  LASSERT(step_nodes!=NULL);
  (void)printTarget("\n");
  PrintSimEvents(step_nodes);
  (void)printTarget("\n");
}

/******************************************************************
 *                                                                *
 * ECstep_sync                                                    *
 * Displays the synchronization tree of a menu option or          *
 * the refused-synchronization tree of the -menu option.          *
 *                                                                *
 *******************************************************************/


/* GetProcess
 * Returns the descriptor of the process called "process".
 * If the process does not exist then it returns -1.
 * If "process" is empty then it returns 0.
 */
static DescriptorTyp GetProcess(process)
     char *process;
{
  DescriptorTyp proc;

  if (process[0]!='\0') {
    proc = FindP( process );
    if (proc==0) {
      printError("\n      ");
      printError(process);
      printError(": Unknown process name.\n\n");
      return -1;
    }
    return proc;
  }
  else
    return 0;
}


/* ECstep_sync
 * Displays the synchronization tree of a menu option or
 * the refused-synchronization tree of the -menu option.
 */
void ECstep_sync( branch, process )
     int   branch;
     char *process;
{
  PStepNodeTyp  pnn;
  BehTyp        b,g;
  DescriptorTyp proc;

  if ((proc=GetProcess(process))==-1 )
    return;

  pnn = (PStepNodeTyp)Look_Stack(step_nodes);
  b   = pnn->exp_beh;

  /* Refused-Synchronization Information */

  if ( branch < 0 ) {
    if ( (pnn->nst!=NULL) && StepOK( pnn->nst, -branch ) ) {
      (void)printTarget("\n Events involved in the Synchronization ");
      PrintInt(printTarget,branch);
      (void)printTarget(": \n\n");
      VPrintST( LookArgIB(pnn->nst,-branch), printTarget, proc, 1 );
      (void)printTarget("\n");
    }
    else
      (void)printTarget("\n   Invalid option.\n\n");
    return;
  }

  /* Synchronization Information */

  if ( (branch>0) && ((b==NULL) || (LookTypeB(b)==StopC)) ) {
    printMsgs("\n   DEADLOCK\n\n");
    return;
  }
  else {
    if ( StepOK( b, branch ) ) {
      g  = LookActionArgIB(b,branch);
      if ( IsEventLeafST(g) ){
	printTarget("\n Event ");
	PrintInt(printTarget,branch);
	(void)printTarget(": \n\n");
	VPrintST( g, printTarget, proc, 1 );
      }
      else {
	printTarget("\n Events involved in the Synchronization ");
	PrintInt(printTarget,branch);
	(void)printTarget(": \n\n");
	VPrintST( (BehTyp)LookAInfo(LookA(g,STA)), printTarget, proc, 1 );
      }
      (void)printTarget("\n");
      return;
    }
  }
  printMsgs("\n   Invalid option.\n\n");
}


/******************************************************************
 *                                                                *
 * ECstep_select                                                  *
 *                                                                *
 *******************************************************************/

/* ECstep_select
 * Select the subset of transitions from the menu option, given by the
 * list of alternatives numbers opts.
 */
void ECstep_select( opts )
     ListTyp opts;
{
  PStepNodeTyp pnn;
  int          numArg,n;
  BehTyp       b,res;


  pnn    = (PStepNodeTyp)Look_Stack(step_nodes);
  b      = pnn->exp_beh;
  numArg = NumArgIB(b);
  res    = NULL;
  for ( ; opts!=NULL; opts=Next_list(opts) ){
    n = (int)LookInfo_list(opts);
    if ( n<0 || n>numArg ){
      Warning("Selection out of range.\n");
    }
    else
      res = AppendUB( res, CopyUntilActB(LookArgIB(b,n)) );
  }
  FreeB(UnshareB(b));
  if ( res == NULL )
    res = MakeB(0,StopC);
  pnn->exp_beh = ShareB(res);
}


/******************************************************************
 *                                                                *
 * ECstep_help                                                    *
 *                                                                *
 *******************************************************************/

/* ECstep_help
 * Display Step mode help.
 */
void ECstep_help()
{
  printTarget("\n");
  printTarget(" Step-by-Step Simulation Commands:\n");
  printTarget("     Print    : print the behaviour at the current state.\n");
  printTarget("                Syntax: Print [-p] [-t] [-a] [<depth>] [<output_file>]\n");
  printTarget("\n");
  printTarget("     Menu     : menu of transitions offered at the current state.\n");
  printTarget("     Refused  : menu of unsuccessful synchronizations (due to data value\n");
  printTarget("                offering mismatch) at the current state.\n");
  printTarget("                The numbers in parenthesis are the line numbers of the\n");
  printTarget("                events involved in the unsuccessful synchronization.\n");
  printTarget("                Note that the menu labels are negative numbers.\n");
  printTarget("     Sync <n> [<proc_name>] :\n");
  printTarget("                For a transition <n> it shows the events that produced it.\n");
  printTarget("                For an unsuccessful synchronization <n> it shows the events\n");
  printTarget("                that could not synchronize.\n");
  printTarget("                Each event is diplayed below the stack of processes instantiated\n");
  printTarget("                to produce it. If <proc_name> is specified then only the \n");
  printTarget("                instantiations of that process are displayed.\n");
  printTarget("     <n>      : execute transition labelled <n> from the menu of transitions.\n");
  printTarget("     Undo     : undo the last simulation step (back to previous state).\n");
  printTarget("     Trace    : sequence of transitions that lead to the current state.\n");
  printTarget("\n");
  printTarget("     Exit     : quit simulation mode.\n");
  printTarget("\n");

}


/******************************************************************
 *                                                                *
 *  ECstep_print                                                  *
 *                                                                *
 *******************************************************************/

static boolean opcionA, opcionP, opcionT;


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

  opcionP = FALSE;
  opcionT = FALSE;
  opcionA = 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]=='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 ");
  PrintInt(printMsgs,num);
  printMsgs(" ");
  if (ident[0]!='\0')
    printMsgs(ident);
  printMsgs("\n\n");
}

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

/* output file */
static  FILE *fd;


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

/* ECstep_print
 * Executes the command print (step mode).
 * 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 ECstep_print( contopcio, lst_opcio, depth, outfile, pstr )
     int   depth, contopcio;
     char *outfile, *lst_opcio;
     void (*pstr)();
{
  PStepNodeTyp pnn;
  BehTyp       p;
  int          proc;

  pnn = (PStepNodeTyp)Look_Stack(step_nodes);
  p = pnn->init_beh;
  check_opcion_print(contopcio,lst_opcio);
  echo_print(depth,outfile);

  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]!='\0')
    if ((fd = 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);

  if (outfile[0]!='\0') {
    (void)fflush(fd);
    (void)close((int)fd);
  }
  printMsgs("\n");
}

/******************************************************************
 *
 *  ECstep_exit
 *
 *******************************************************************/

/* ECstep_exit
 * Finishes simulation mode and return the lola mode.
 */
void ECstep_exit()
{
  Free_Stack( step_nodes , Free_StepNode );
  step_nodes = Create_Stack();
  printMsgs("\n   Step-by-step simulation finished.\n\n");
}


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



















