/***********************************
  (C) Copyright 1992-1993; dit/upm
   Distributed under the conditions stated in the
   TOPO General Public License (see file LICENSE)
 ***********************************
 * $Log: elib.c,v $
 * Revision 1.4  1994/11/14  14:45:43  lotos
 * port to msdos
 *
 * Revision 1.3  1993/12/22  18:11:38  lotos
 * fix a bug
 *
 * Revision 1.2  1993/10/18  17:56:43  lotos
 * cleanup interface to interlib
 *
 * Revision 1.1  1993/09/30  14:30:46  lotos
 * Initial revision
 *
 ***********************************/

#ifndef lint
static char rcsid[]= "$Id: elib.c,v 1.4 1994/11/14 14:45:43 lotos Exp $";
#endif

# include "ltgswbus.h"
#include "omgrc.h"

/* KJT 20/01/23: added headers */
#include <string.h>

# define BUCKSIZE 256
# define ACTS 4

/*****  private types  *****/

typedef struct Glist {
	char** gates;
	int    max;
	int    size;
      } glist;
/*****  private variables  *****/

static glist* gl=NULL;
static int prnumber =0;
/* KJT 20/01/23: added "int" type */
static int Indent = 0;

/*****  private functions headers  *****/

/*****  private function bodies  *****/
PRIVATE int
show (fp, str)
  FILE* fp;
  char* str;
{
  int	ln;
  ln = strlen (str);
  (void) fprintf (fp, str);

  return ln;
}

PRIVATE void
Indentar (fp, I)
  FILE* fp;
  int   I;
{
  (void) fprintf (fp, "\t");
  for (; I > 0; I--)
    (void) fprintf (fp, " ");
}

PRIVATE prevs*
newprevs ()
{
  prevs* new;

  new = (prevs*) emalloc (sizeof (prevs));
  return new;
}
PRIVATE TNaction*
newact ()
{
  TNaction* act;

  act = (TNaction*) emalloc ((int)sizeof (TNaction));
  act-> actl     = NULL;
  act-> prev     = NULL;
  act-> brothers = NULL;
  act-> sons     = NULL;
  /* KJT 20/01/23: set to 0 instead of NULL */
  act-> off      = 0;
  act-> actname  = NULL;
  act-> lsp      = NULL; /* from lsp to nsp */
  act-> nsp      = NULL; /* from lsp to nsp */
  act-> obj      = NULL;
  act-> bt       = NONE;
  act-> type     = NONE;

  return act;
}


PRIVATE void
putact(fp, act)
     FILE*	fp;
     TNaction*	act;
{
  TNaction*	aux;
  int		i;

  writeact (fp, (CLR_TYPE*) act->actname   );
  assert (act->depth != -1);
  (void) fprintf (fp, "{%d}", act->depth);
  if (act->type == TREFUSE)
    (void) fprintf (fp, "[R]");
  (void) fprintf (fp, "(");
  for (i=0,aux = act->sons; aux != NULL; aux = aux->brothers, i++){
    if (i > 0)
      (void) fprintf (fp, ",");
    putact(fp,aux);

  }
  (void) fprintf (fp, ")");
}

/*
  It evaluates the minimum lenght of a trace
*/
/*
  It evaluates the maximum lenght of a trace
*/
PRIVATE int
getmax (gmax)
	int gmax;
{
  int res;

  if (gmax == -1)
    res = 7;
  else
    res = gmax;

  return res;
}

PRIVATE int
Isinglist (name)
	char* name;
{
  int i;

  for (i=1; i<=gl->size; i++){
    if (0 == strcmp (name, gl->gates[i-1]))
      return TRUE;
  }
  return FALSE;
}


/*
  Functions for gate name collection
*/
PRIVATE void
evalg (root)
	TNaction* root;
{
  TNaction* aux;

  if ((root->actname != NULL) && (!Isinglist (root->actname))){
    assert (gl->size < 1024);
    gl->gates[gl->size++]= root->actname;
  }
  for (aux = root->sons; aux != NULL; aux = aux->brothers)
    evalg(aux);
}

PRIVATE void
headproc ()
{
  int i;

    /* close the LOTOS commen opened when starting obj: ... */
  if (flagd > 0)
    (void) fprintf (ofp," *)");


    /* proces head properly */
  (void) fprintf (ofp,"\n");
  Indentar (ofp, 0);
  (void) fprintf (ofp,"process t%d", ++prnumber);

    /* proces'gates if exist */
  if (gl->size != 0){
    (void) fprintf (ofp," [");
    for (i=1; i<=gl->size; i++){
      if (i >1)
	(void) fprintf (ofp, ", %s ", gl->gates[i-1]);
      else
	(void) fprintf (ofp, " %s ", gl->gates[i-1]);
    }
    (void) fprintf (ofp," ]");
  }

    /* proces'values when exist
  (void) fprintf (ofp," ( ) ");
    */

  (void) fprintf (ofp," : noexit := ");
}

PRIVATE void
evalgates (root)
	TNaction* root;
{

  if (gl == NULL){
    gl = (glist*) emalloc (sizeof (glist));
    gl->gates = (char**) emalloc (1024 *sizeof (char*));
    gl->max=1024;
  }
  gl->size =0;
  evalg (root);
}

PRIVATE int
isinternal (of)
	TNaction*	of;
{
  /* Utilizo la "i" como interna */
  if (0 == strcmp (of->actname, "i"))
    return TRUE;
  else
    return FALSE;
}
PRIVATE int
machof (sp, of, tof)
	spe     sp;
	offert	of;
	testof*	tof;
{
  if (0 == strcmp (offertname(sp,of),tof->name))
    return TRUE;
  else
    return FALSE;
}

PRIVATE TNaction*
isinsons (act, ord)
	TNaction*       act;
	int		ord;
{
  TNaction* son;
  for (son = act->sons; son != NULL; son = son->brothers)
    if (son->order == ord)
      return son;

  return NULL;
}

PRIVATE void
mkpath (actl,act,tof,lmin,lmax,gmin,gmax,ldepth,obj,node,pactl,pactlpos)
	TNactcol*	actl;
	TNaction*	act;
	testof*		tof;
	int		lmin;
	int		lmax;
	int		gmin;
	int		gmax;
	int		ldepth;
	int		obj;
	TNODE*		node;    /* current node in the  Test pattern Tree */
	TNactcol*       pactl;
	int		pactlpos;   /* order of the previous sobj */
{
  set_off  auxl;
  offert   aux;
  TNaction* new;
  prevs*    nprev;
  TNaction* old=NULL;
  int	    i;

  if (((lmax == -1)||(ldepth <= lmax)) && ((gmax == -1)||(act->depth < gmax))){
    auxl = get_spec_offers (act->nsp);
    for (i=1; auxl != NULL; i++){
      aux = first_off (auxl);
      if (NULL != (old = isinsons (act, i))){
	new = old;
      } else {
	new = newact();
	new->actl     = NULL;
	new->sob      = FALSE;
	new->prev     = act;
	new->off      = aux;
	new->order    = i;
	new->lsp      = cp_spe (act->nsp);
	new->nsp      = cp_spe (act->nsp);
	step (new->nsp, aux);
	new->type     = NONE;
	new->actname  = offertname (act->nsp,aux);
	new->brothers = act -> sons;

	if (isinternal (new))
	  new-> depth    = act->depth;
	else
	  new-> depth    = act->depth+1;

	act->sons      = new;
      }
      if (TRUE == machof (act->nsp, aux, tof)){
	if (((obj==TRUE)&&(new->depth>=gmin))||((obj==FALSE)&&(ldepth>=lmin))){
	  if (actl->nsons == actl->maxsons){
	    actl->actions = (TNaction**)
		realloc((char*)actl->actions,
			(unsigned)((ACTS+actl->maxsons)*sizeof(TNaction*)));
	    actl->prevsobj = (prevs**)
		realloc((char*)actl->prevsobj,
			(unsigned)((ACTS+actl->maxsons)*sizeof(prevs*)));
	    actl->maxsons = ACTS+actl->maxsons;
	  }
	  actl->actions[actl->nsons] = new;
	  nprev =newprevs();
	  actl->prevsobj[actl->nsons]= nprev;
	  actl->prevsobj[actl->nsons]->pactl    = pactl;
	  actl->prevsobj[actl->nsons]->ldepth   = ldepth;
	  actl->prevsobj[actl->nsons]->pactlpos = pactlpos;
	  actl->nsons++;
	  new->sob = TRUE;
	  new->obj = node;
	  new->actl= actl;

	}
      }
      mkpath(actl,new,tof,lmin,lmax,gmin,gmax,ldepth+1,obj,node,pactl,pactlpos);
      auxl=del_off(aux,auxl);
    }
  }
}

PRIVATE int
cmpact (of1, of2)
	TNaction*	of1;
	TNaction*	of2;
{
  if (0 == strcmp (of1->actname, of2->actname))
    return TRUE;
  else
    return FALSE;
}

/* It searchs for an observable action to end the lateral branch */
PRIVATE void
labeltestact (tact)
	TNaction*	tact;
{
  TNaction* auxact;

  if (tact != NULL){
    if ((tact->bt != MAIN) && (!isinternal (tact))){
      tact->bt = LATERAL;
      tact->type = INCONCLUSIVE;
    } else {
      for (auxact = tact->sons; auxact != NULL; auxact = auxact ->brothers){
	/* Inclussion of a observable event has test */
	labeltestact (auxact);
      }
    }
  }
}

/* It labels a lateral brach comparing with the main brach */
PRIVATE int
labelact (lact, mainact, depth)
	TNaction*	lact;
	TNaction*	mainact;
	int		depth;
{
  TNaction* auxact;
  int       status;

  if (lact == mainact)
    return FALSE;
  assert (lact->bt == NONE);
  if ((lact -> sons == NULL ) && (mainact -> sons == NULL)){
    lact->bt = LATERAL;
    lact->type = INCONCLUSIVE;
    return TRUE;
  }
  status = FALSE; /* not maching of lact with mainact */
  if (isinternal(lact)){
    for (auxact = lact->sons; auxact != NULL; auxact = auxact ->brothers){
      if (TRUE == labelact (auxact, mainact, depth))
	status = TRUE;
    }
    lact->bt = LATERAL;
    if (status == FALSE){
      /*if thereis not maching among  lact'sons and mainact continuation*/
      for (auxact = lact->sons; auxact != NULL; auxact = auxact ->brothers){
	/* Inclussion of a observable event has test */
	labeltestact (auxact);
      }
    }
  } else if (isinternal (mainact)){
    auxact = mainact->sons;
    if (auxact != NULL){
      for (; (auxact != NULL) && (auxact->bt != MAIN); auxact = auxact ->brothers){
	assert (auxact != NULL);
      }
      assert (auxact != NULL);
      status = labelact (lact, auxact, depth);
    }
  } else if (mainact == NULL){
    lact->bt = LATERAL;
    lact->type = INCONCLUSIVE;
  } else if (cmpact (lact, mainact)){
    lact->bt = LATERAL;
    for (auxact = mainact->sons;
	 (auxact != NULL) && (auxact->bt != MAIN);
	 auxact = auxact ->brothers)
      ;
    if (auxact != NULL){
      mainact = auxact;
      for (auxact = lact->sons; auxact != NULL; auxact = auxact ->brothers){
	if ( TRUE == labelact (auxact, mainact, depth+1))
	  status = TRUE ;
      }
    }
    if (status == FALSE){
      /*if thereis not maching among  lact'sons and mainact continuation*/
      for (auxact = lact->sons; auxact != NULL; auxact = auxact ->brothers){
	/* Inclussion of a observable event has test */
	labeltestact (auxact);
      }
    }
    status = TRUE;
  }

  return status;
}

/********** public functions *****/
PUBLIC TNactcol*
newactl ()
{
  TNactcol* actl;

  actl = (TNactcol*) emalloc ((int)sizeof (TNactcol));
  actl->actions = (TNaction**)emalloc (ACTS*(int)sizeof (TNaction*));
  actl->prevsobj= (prevs**)emalloc (ACTS*(int)sizeof (prevs*));
  actl->nsons   = 0;
  actl->maxsons = ACTS;

  return actl;
}
PUBLIC testof*
newtestof ()
{
  testof* new;

  new = (testof*) emalloc ((int)sizeof (testof));
  new-> name    = NULL;
  new-> explist = NULL;
  new-> nexp    = 0;

  return new;
}

PUBLIC expr*
newexp ()
{
  expr* new;

  new = (expr*) emalloc ((int)sizeof (expr));
  new-> type    = -1;
  new-> val     = -1;
  new-> sort    = -1;
  return new;
}

/*****  public functions bodies  *****/
/* IO Colours functions */

/* read one action node list   */
PUBLIC CLR_TYPE
readacts (fp)
	FILE*  fp;
{
  (void)fprintf(ofp,"ltg: not implemented\n");
  exit(1);
}

PUBLIC void
writeacts (fp, val)
	FILE*		fp;
	CLR_TYPE*	val;
{
  TNactcol*	aux;
  int i;

  (void) fprintf (fp, "ACT: ");

  aux=(TNactcol*)val;
  if (aux->nsons >0){
    for (i=0; i<aux->nsons; i++)
      putact(fp,aux->actions[i]);
  }
}


PUBLIC void
writeact  (fp, val)
	FILE*           fp;
	CLR_TYPE*       val;
{
  char* name;

  name = (char*) val;
  if (name != NULL){
    Indent = Indent + show(fp," ");
    Indent = Indent + show(fp,name);
    Indent = Indent + show(fp," ");
  }
}

PUBLIC void
wrtof  (fp, val)
	FILE*           fp;
	CLR_TYPE*       val;
{
  wrexl  (fp, val);
}

PUBLIC void
wrexl  (fp, val)
	FILE*           fp;
	CLR_TYPE*       val;
{
  testof* exprl;
  int 	  i;

  exprl = (testof*) val;
  (void)fprintf(fp, " %s:",exprl->name);
  for (i=0; i < exprl->nexp; i++){
    (void)fprintf(fp,"|");
    if (exprl->explist[i]->type == VARIABLE){
      (void)fprintf(fp,"VARIABLE");
    } else {
      (void)fprintf(fp,"VALUE:");
      assert (exprl->explist[i]->val != -1);
      (void)fprintf(fp,"%s", SymbolTable->data[exprl->explist[i]->val]);
    }
    if (exprl->explist[i]->sort != -1){
      (void)fprintf(fp,"[%s]", SymbolTable->data[exprl->explist[i]->sort]);
    }
  }
}

PUBLIC void
wrexp  (fp, val)
	FILE*           fp;
	CLR_TYPE*       val;
{
  expr* xp;

  xp = (expr*) val;
  if (xp->type == VARIABLE)
    (void)fprintf(fp,"VARIABLE");
  else
    (void)fprintf(fp,"VALUE");
}

PUBLIC void*
my_realloc (ptr, size)
  char *ptr;
  int size;

{
 void * v;
 assert (size >0);

 v = (void *) realloc(ptr, (unsigned)size);
 if (v == NULL) {
   (void)fprintf(ofp,"Out of Memory\n");
   exit (1);
 }
 return v;
}



/*
PUBLIC char*
emalloc (i)
  int i;
{
  char *p;

  p = malloc ((unsigned)i);
  if (p == NULL) {
    (void)fprintf (ofp, "%s: Out of memory\n", progname);
    exit (1);
  }
  return p;
}
*/

PUBLIC TNactcol*
newactcol (sp)
  spe     sp;
{
  TNactcol* actl;
  TNaction* act;

  actl = newactl ();
  /*
  actl = (TNactcol*) emalloc (sizeof (TNactcol));
  actl->actions = (TNaction**)emalloc (ACTS*sizeof (TNaction*));
  actl->nsons   = 0;
  actl->maxsons = ACTS;
  */

  act = (TNaction*) emalloc (sizeof (TNaction));
  act-> prev     = NULL;
  act-> brothers = NULL;
  act-> sons     = NULL;
  /* KJT 20/01/23: set to 0 instead of NULL */
  act-> off      = 0;
  act-> lsp      = NULL;
  act-> nsp      = sp;
  act-> obj      = NULL;
  act-> actname  = NULL;

  actl->actions[0] = act;
  actl->prevsobj[0] = newprevs();
  actl->nsons++;

  return actl;
}

PUBLIC TNactcol*
mkactl (actlist, tof, node, lmin, lmax, gmin, gmax, obj)
  TNactcol*	actlist; /* list of actions at this level */
  testof* 	tof;  /* target action */
  TNODE*	node;    /* current node in the  Test pattern Tree */
  int		lmin;    /* local min current lenght */
  int		lmax;    /* local max current lenght */
  int		gmin;    /* global min current lenght */
  int		gmax;    /* global max current lenght */
  int		obj;     /* it is an objective */
{
  int i;

  TNactcol* actl;

  gmax = getmax (gmax);

  actl = newactl ();

  if (actlist->nsons >0){
    for (i=0; i<actlist->nsons; i++){
       mkpath (actl,actlist->actions[i],tof,lmin,lmax,gmin,gmax,1,obj,
	       node,actlist,i);
    }
  }

  return actl;
}

PUBLIC TNactcol*
mkractl (actlist, tof, node)
  TNactcol*	actlist;
  testof*	tof;
  TNODE*	node;
{
  TNactcol* actl;
  TNaction* act;
  int       i;

  act = newact ();
  act-> actname = tof->name;
  act-> type   = TREFUSE;

  actl = newactl ();
  actl->nsons   = 1;
  actl->actions[0] = act;

  if (actlist->nsons >0){
    for (i=0; i<actlist->nsons; i++){
      assert (i < ACTS);
      actlist->actions[i]->sons = act;
      act -> prev = actlist->actions[i];
      act ->actname = tof->name;
      act ->depth = (actlist->actions[i]->depth)+1;
    }
  }

  return actl;
}

PUBLIC expr*
mkexp (type, vallexv, sortlexv)
	int	type;
	int	vallexv;
	int	sortlexv;
{
  expr* new;

  new = newexp ();
  new-> type = type;
  new-> val  = vallexv;
  new-> sort = sortlexv;

  return new;
}

PUBLIC testof*
mktof (gname, exl)
	int	gname;
	testof*	exl;
{
  if (exl == NULL)
    exl = newtestof ();

  exl->name = SymbolTable->data[gname];
  return exl;
}

PUBLIC int
l2i (lexv)
  int 	lexv;
{
  char* name;
  int res,i;

  name = SymbolTable->data[lexv];
  res = sscanf (name, "%d", &i);
  assert (res==1);
  return i;
}

PRIVATE int
cont (act)
  TNaction* act;
{
  if ((act->sons == NULL) ||
      (act->type == INCONCLUSIVE) ||
      (act->type == TACCEPT) ||
      (act->type == TREFUSE))
    return FALSE;
  else
    return TRUE;

}

PRIVATE int
actsons(act)
  TNaction* act;
{
  TNaction* aux;
  int	    count = 0;

  for (aux = act->sons; aux != NULL; aux = aux->brothers)
    if ((act ->bt== LATERAL) || (act ->bt== MAIN)){
      if (count == 1)
	return 2;
      else
	count++;
    }
  return count;
}

PRIVATE void
showact (act, branch)
  TNaction* act;
  int	    branch;
{
  TNaction* auxact;
  int nsons, sons;
  int chindent, previndent;

  previndent = Indent;
  writeact (ofp,(CLR_TYPE*) act->actname   );
  if ((branch == MAIN) && (act->sobj == TRUE)){
    Indent = Indent + show (ofp , "(*S*)");
    act->sobj = FALSE;
  }

  sons = 0;
  if (cont (act)){

    if (act -> prev != NULL)
      Indent = Indent + show (ofp,";");

    nsons =0;
    for (auxact=act->sons; auxact!=0; auxact= auxact->brothers){
      if ((auxact->bt == MAIN) || (auxact->bt ==  LATERAL))
	nsons++;
    }
    if ((nsons > 1) && (act -> prev != NULL))
      Indent = Indent + show (ofp,"(");

    chindent = Indent;

    for (auxact=act->sons; auxact!=0; auxact= auxact->brothers){
      Indent = chindent;
      if ((auxact->bt == MAIN) || (auxact->bt ==  LATERAL)){
	if (sons > 0){
	  (void) fprintf (ofp,  "\n");
	  Indentar (ofp, Indent);
	  (void) show (ofp,"[]");
	  (void) fprintf (ofp,  "\n");
	  Indentar (ofp, Indent);
	}
	if (nsons > 1){
	  Indent = Indent + show (ofp, " (");
	}
	if ((branch == MAIN) && (auxact->bt == LATERAL)){
	  /*when I am starting the lateral branch */
	  Indent = Indent + show (ofp,"(* L *)");
	  showact (auxact, LATERAL) ;
	} else {
	  showact (auxact, branch);
	}
	if (nsons > 1){
	  Indent = Indent + show (ofp, " )");
	}
	sons++;
      }
    }
    if ((nsons > 1) && (act -> prev != NULL)){
      (void) fprintf (ofp,  "\n");
      Indentar (ofp, chindent-1);
      (void) show (ofp,")");

    }
  } else {
    if (branch == MAIN){
      if (act->type == TREFUSE){
	assert (act->sons == 0);
	(void) show (ofp, " ; stop (* R *)");
      } else
	(void) show (ofp," ; stop (* A *)");
    } else if (act->type == INCONCLUSIVE){
      (void) show (ofp," ; stop (* I *)");
      act->type = NONE;
    } else
      assert ((branch == MAIN)||(act->type == INCONCLUSIVE));
  }
  if (branch == LATERAL){
    assert (act->bt == LATERAL);
    act->bt = NONE;
  }
  Indent = previndent;
}


PRIVATE int
wrtact (act, depth, prvs)
  TNaction* act;
  int       depth;
  prevs*    prvs;
{
  TNaction* auxact;

  if (flagd > 0)
    writeact (ofp, (CLR_TYPE*) act->actname   );

  if (depth == prvs->ldepth){
    if (act->prev != NULL) /* It is the root node=>it is not an event */
      act->sobj = TRUE;
    assert (act == prvs->pactl->actions[prvs->pactlpos]);
    if (flagd > 0)
      (void) fprintf (ofp, "SUB");
    prvs = prvs->pactl->prevsobj[prvs->pactlpos];
    depth=0;
  }

  assert (act->bt==NONE); /* check it is not printing */
  act->bt=MAIN;

  assert (act->depth != -1);
  if (flagd > 0)
    (void) fprintf (ofp, "{%d}", act->depth);
  if (act->type == TREFUSE){
    if (flagd > 0)
      (void) fprintf (ofp, "[R]");
  } else if (act->type == TACCEPT){
    if (flagd > 0)
      (void) fprintf (ofp, "[A]");
  }
  if (act->prev != 0){
    if (flagd > 0)
      (void) fprintf (ofp," <- ");
    for (auxact = act->prev->sons; auxact != NULL; auxact = auxact ->brothers){
      (void) labelact (auxact, act, 1);
    }
    wrtact(act->prev, depth+1, prvs);
  } else {
    evalgates(act);
    headproc ();
    Indent = 2;
    (void) fprintf (ofp,  "\n");
    Indentar (ofp,Indent);
    showact (act, act->bt);
    (void) fprintf (ofp,  "\n");
    Indentar (ofp, 0);
    (void) fprintf (ofp,"endproc (* %d *)\n", prnumber);
  }

  assert (act->bt==MAIN);
  act->bt=NONE;
  /* reset printing label */

}

PUBLIC int
wrttest (actl)
TNactcol* actl;
{
  TNactcol*     aux;
  prevs*        prv;
  int old;
  int i;

  aux=actl;
  prv =  newprevs ();
  if (aux->nsons > 0){
    for (i=0; i<aux->nsons; i++){
      /* open comment for obj: .. line */
      if (flagd > 0)
	(void) fprintf (ofp, "\n (* obj: ");
      old = aux->actions[i]->type;
      aux->actions[i]->type = TACCEPT;
      prv->pactl=actl;
      prv->ldepth=0;
      prv->pactlpos=i;
      wrtact (aux->actions[i], 0, prv);
      aux->actions[i]->type = old;
      if (flagd > 0)
	(void) fprintf (ofp, "\n");
    }
  }
  (void) fprintf (ofp, "\n");

  return 1;
}

PUBLIC spe
spinit (s, n)
	int	s;
	int	n;
{

  char* spec_name;
  spe spec;

  if (s < 0){
    (void)fprintf (stdout,"Specification name not valid\n");
    exit(1);
  } else {
    /*
    spec = spe_init ();
    */
    spec_name=SymbolTable->data[s];
    if ((spec_name == NULL) || (strlen (spec_name) == 0)) {
      (void)fprintf (stdout,"Specification name not valid\n");
      exit(1);
    } else
      spec = spe_init (spec_name, (char*)NULL, FALSE, FALSE);
  }
  return spec;
}

