/**************************************************************
 *       spec.c - LBM Interpreter Specification Functions
 **************************************************************/
/***********************************************
 (C) Copyright 1993-1994; dit/upm
   Distributed under the conditions stated in the
   TOPO General Public License (see file LICENSE)
 ***********************************************
 $Log: spec.c,v $
 * Revision 1.4  1994/11/14  11:24:37  lotos
 * avoid name collision
 *
 * Revision 1.3  1994/10/17  16:41:26  lotos
 * cosmetics
 *
 * Revision 1.2  1993/12/22  17:19:45  lotos
 * Changed a number of names in the interface
 * Added function  to work with instances of processes and their gates
 * CLOSING BASIC LOTOS VERSION OF LIBRARY!
 *
 * Revision 1.1  1993/10/16  10:51:26  lotos
 * Initial revision
 *
 **********************************************
 $Id: spec.c,v 1.4 1994/11/14 11:24:37 lotos Exp $
 **********************************************/

#include "swbus.h"

/*  ------- CODE FOR SPECIFICATION INTERNAL IDENTIFIER --------  */
/* This function returns a different
 * number each time is called.
 * this number is used as the internal identifier
 * of the specification. Such identifier is used
 * to avoid the very same name of variables belonging
 * to different copies of the same specification.
 * it may be avoid when the ldi library handles
 * severals sets of data.
 */
PUBLIC long int
new_spec_inter_id ()
{
  static long int spec_code = 0; /* Internal identifier */

  return spec_code++;
}
/*  ------- CODE FOR SPECIFICATION INTERNAL IDENTIFIER --------  */

PRIVATE void
init_lbm (S)
  spe S;
{
  char *alname, *lname;
  FILE *specfile, *alfile;

  alname  = emalloc ((strlen (S->name) + 5)*sizeof(char));
  lname   = emalloc ((strlen (S->name) + 5)*sizeof(char));

  (void)sprintf (alname, "%s.agf", S->name);
  (void)sprintf (lname, "%s.lbm", S->name);

  specfile = efopen (lname, "r");
  alfile = efopen (alname, "r");

  S->lbmroot = restore (specfile);
  S->alroot = restore (alfile);

  S->lastBUTnumber = (int)find_attr (c_pr, S->lbmroot)->value;
  S->grnl = (IAT*) find_attr (c_grnl, S->lbmroot)->value;
  S->grnl->incr = 16;
  S->grnl->class = 1;
  S->ATable = (AT*) find_attr (c_at, S->alroot)->value;
  S->SymbolTable= (ST*) find_attr (c_ll, S->alroot)->value;
  S->SymbolTable->incr = 16;
  S->SymbolTable->class = 1;

  (void)fclose (specfile);
  (void)fclose (alfile);

  S->lastBUTnumber = do_transform (S->lbmroot, S->ATable, S->SymbolTable,
				   S->lastBUTnumber, S->grnl);

  if ((int)S->lbmroot->value1 & 1) /* there exist the first _annotation_list */
    S->BUTlist = S->lbmroot->sons->brothers;
  else
    S->BUTlist = S->lbmroot->sons;
  set_attr (c_refcount, S->lbmroot, (CLR_TYPE)1);

  free (alname);
  free (lname);
}

PRIVATE soffert*
get_soffers (S, kt)
  spe   S;
  krnlt kt;
{
  soffert *soffs, *aux;

  assert (S != NULL);
  assert (kt != NULL);

  offer_propagation (S, kt);

  soffs = available_events (kt);
  for (aux = soffs; aux != NULL; aux = aux->next)
    if (aux->OffId == -1) /* Identifier not assigned yet */
      aux->OffId = S->lastOffId++;
  return soffs;
}

PUBLIC spe
spe_init (name, pars, doph, keepgrd)
  char    *name;
  char    *pars;
  boolean doph;
  boolean keepgrd;
{
  spe S;

  assert (name != NULL);

  S = new_spe ();
  S->code = new_spec_inter_id ();
  S->name = strdup (name);
  S->keepguards = keepgrd;

  init_lbm (S);

  if ((S->ldi = ldi_init (S->name)) != 0)
    fatal_error ("cannot open Data Interpreter", __FILE__, __LINE__);

  S->doph = doph;

  init_kt (S, pars);

  if (doph)
    S->ph = S->kt->ph;

  return S;
}

PRIVATE int
get_pair (Tenv, ldiui)
  xnviron Tenv;
  int     ldiui;
{
  int i;

  for (i = 0; i < Tenv->size; i++)
    if (Tenv->data[2*i] == ldiui)
      return Tenv->data[2*i+1];

  fatal_error ("Erroneus table", __FILE__, __LINE__);
  return 0; /* to shut lint off */
}

PRIVATE void
soffs_change_suffix (Tenv, S, soffs)
  xnviron Tenv;
  spe     S;
  soffert *soffs;
{
  int     i;
  soffert *aux;
  INTlist vl;

  if (soffs == NULL)
    return;

                   /* change suffix in offerts */
  for (aux = soffs; aux != NULL; aux = aux->next) {
    for (i = 0; i < aux->nexp; i++) {
      if (aux->expl[i]->ldiui < 0) /* there is a variable */
	aux->expl[i]->ldiui = get_pair (Tenv, aux->expl[i]->ldiui);
      for (vl = aux->expl[i]->vrlst; vl != NULL; vl = INTtail (vl)) {
	INThead (vl) = get_pair (Tenv, INThead (vl));
      }
    }
  }
}

PRIVATE void
offers_change_suffix (Tenv, S, kt)
  xnviron Tenv;
  spe     S;
  krnlt   kt;
{
  int     i;
  soffert *aux;
  INTlist vl;

  if (kt == NULL)
    return;

  if (kt->soffs != NULL) {                 /* change suffix in offerts */
    for (aux = kt->soffs; aux != NULL; aux = aux->next) {
      for (i = 0; i < aux->nexp; i++) {
	if (aux->expl[i]->ldiui < 0) /* there is a variable */
	  aux->expl[i]->ldiui = get_pair (Tenv, aux->expl[i]->ldiui);
	for (vl = aux->expl[i]->vrlst; vl != NULL; vl = INTtail (vl)) {
	  INThead (vl) = get_pair (Tenv, INThead (vl));
	}
      }
    }
  }
  offers_change_suffix (Tenv, S, kt->son1);
  offers_change_suffix (Tenv, S, kt->son2);
}

PRIVATE xnviron
kt_change_suffix (Tenv, S, kt)
  xnviron Tenv;
  spe     S;
  krnlt   kt;
{
  int    i, vid, oldvid;
  kdatum val;

  if (kt == NULL)
    return NULL;

  if (kt->env != NULL) {              /* change suffix in environments */
    for (i = 0; i < kt->env->size; i++) {
      oldvid = kt->env->data[i*2+1];
      vid = Var_Declaration (S, kt->env->data[i*2], kt->pi);
      kt->env->data[i*2+1] = vid;
      (void)I2Tadd (oldvid, vid, Tenv);
      val = get_value (oldvid);
      if (val != NULL)
	if (!let_var (vid, kd_copy (val)))
	  fatal_error ("Cannot initialize variable", __FILE__, __LINE__);
    }
  }
  Tenv = kt_change_suffix (Tenv, S, kt->son1);
  Tenv = kt_change_suffix (Tenv, S, kt->son2);

  return Tenv;
}

PUBLIC spe
cp_spe (S)
  spe S;
{
  spe     aux;
  xnviron Tenv = I2Tcreate (100, 10, 1); /* size 100, incr 10, class 1 */

  aux = new_spe ();

  aux->code          = new_spec_inter_id ();
  aux->name          = strdup (S->name);
  aux->lbmroot       = S->lbmroot; /* Increments the reference counter */
  find_attr (c_refcount, S->lbmroot)->value =
    (CLR_TYPE)((int)takeclr (c_refcount, S->lbmroot) + 1);
  aux->BUTlist       = S->BUTlist;
  aux->alroot        = S->alroot;
  aux->ATable        = S->ATable;
  aux->SymbolTable   = S->SymbolTable;
  aux->ldi           = S->ldi; /* should it be duplicated ? */
  aux->lastBUTnumber = S->lastBUTnumber;
  aux->lastPI        = S->lastPI;
  aux->lastOffId     = S->lastOffId;
  aux->lastUID       = S->lastUID;
  aux->grnl          = S->grnl;
  aux->kt            = cp_kt (S->kt);
  aux->keepguards    = S->keepguards;
  aux->doph          = S->doph;
  if (S->doph)
    aux->ph = cp_tree (S->ph, TRUE);
  if (S->soffs != NULL)
    aux->soffs = cp_sset_off (S->soffs);
  aux->cfg.rndm      = S->cfg.rndm;

  /* Ok the copy is ready. However, we need   */
  /* to change the suffixes of all variables. */

  Tenv = kt_change_suffix (Tenv, aux, aux->kt);
  offers_change_suffix (Tenv, aux, aux->kt);
  soffs_change_suffix (Tenv, aux, aux->soffs);
  fI2T ((CLR_TYPE)Tenv);

  return aux;
}

PUBLIC void
step (S, off)
  spe    S;
  offert off;
{
  INTlist  ktl;
  krnlt    *ktarray;
  int      idx, ktmax;
  int      label;
  soffert  *soffer;

  soffer = search_soffert (S, off);

  /* Searching states, to avoid repetitions */
  /* Building an array which contains all the leaves */
  ktmax = INTlength (soffer->ktl);
  assert (ktmax > 0);
  ktarray = (krnlt*)emalloc (ktmax * sizeof (krnlt));
  for (idx = 0, ktl = soffer->ktl;
       ktl != NULL;
       idx++, ktl = INTtail (ktl))
    ktarray[idx] = search_kt (INThead (ktl), S->kt);

  /* labeling evolving states */
  label = (soffer->g == LEXITG) ? EXITED : NORMAL;
  for (idx = 0; idx < ktmax; idx++)
    label_kt (ktarray[idx], label);

  /* updating values for negotiated variables */
  if (soffer->g == LEXITG)
    set_values_for_exit (S, soffer, S->kt);
  else
    update_values (soffer);

  /* evolving to next state */
  for (idx = 0; idx < ktmax; idx++)
    evol_kt (S, ktarray[idx]->lb, ktarray[idx]);

  /* cleaning a bit */
  free ((char*)ktarray);
  clean_offer_propagation (S->kt);
  free_sset_off (S->soffs); 
  S->soffs = NULL;

  /* simplifying redundant or undesired behaviour */
  S->kt = simplify_kt (S->kt);
}

PUBLIC set_off
get_spec_offers (S)
  spe S;
{
  set_off il = NULL;
  soffert *aux, *a1;

  aux = get_soffers (S, S->kt);

  for (a1 = aux; a1 != NULL; a1 = a1->next)
    il = INTcons (a1->OffId, il);

  S->soffs = union_sset_off (aux, S->soffs);

  return il;
}

PUBLIC set_off
get_proc_offers (S, p)
  spe  S;
  proc p;
{
  set_off il = NULL;
  soffert *aux, *a1;
  krnlt   kt;

  assert (S != NULL);

  kt = search_pi_kt (p, S->kt);
  if (kt == NULL)
    return NULL;

  aux = get_soffers (S, kt);

  for (a1 = aux; a1 != NULL; a1 = a1->next)
    il = INTcons (a1->OffId, il);

  S->soffs = union_sset_off (S->soffs, aux);

  return il;
}

PUBLIC TNODE*
get_ph (S)
  spe S;
{
  return S->ph;
}

PUBLIC proclist
get_act_proc (S)
  spe S;
{
  return getactpikt ((proclist)NULL, S->kt);
}

PUBLIC void
set_spe_random (S, rndm)
  spe S;
  long (*rndm)();
{
  assert (S != NULL);

  S->cfg.rndm = rndm;
}
