/**************************************************************
 *       tree.c - LBM Interpreter Kernel Tree Functions
 **************************************************************/
/***********************************************
 (C) Copyright 1993-1994; dit/upm
   Distributed under the conditions stated in the
   TOPO General Public License (see file LICENSE)
 ***********************************************
 $Log: tree.c,v $
 * Revision 1.3  1994/10/17  16:41:31  lotos
 * cosmetics
 *
 * Revision 1.2  1993/11/08  17:14:46  lotos
 * corregido error en funcion clean_offer_propagation
 * liberando las ofertas del kt. Ahora se llama a la
 * funcion apropiada (free_sset_off en vez de free_set_off)
 *
 * Revision 1.1  1993/10/16  10:52:00  lotos
 * Initial revision
 *
 **********************************************
 $Id: tree.c,v 1.3 1994/10/17 16:41:31 lotos Exp $
 **********************************************/

# include "swbus.h"

/* A bit of explanation is need for the following variables.    */
/* Why "static" variables in a library? In a library without no */
/* other static variables, I mean. The fact is that I have the  */
/* values of the parameters for the processes (including global */
/* variables, i.e. the variables of the specification) BEFORE   */
/* the definition of these parameters. It's a pity, 'cause the  */
/* funtion for building the kernel tree is very compact. How to */
/* solve it without "distorting" the homogeneus building ? You  */
/* guessed, by means of global, static variables which will     */
/* contain the values for the parameters. Then, when a BUT      */
/* definition is found (AFTER its instantiation), these global  */
/* variables will be used for initialize the parameters.        */
/* ARGC and ARGV are used for the parameters of the             */
/* specification and processes. The same mechanism is use for   */
/* the exit (...) >> ACCEPT var_decls  construction.            */

PRIVATE int    ARGC     = 0;
PRIVATE kdatum *ARGV    = NULL;

PRIVATE int
NumPars (s)
  char *s;
{
  char *blank = " ", *tok = NULL, *r, *p;
  int i = 0;

  if ((s == NULL) || (strlen (s) == 0))
    return 0;

  r = strdup (s);
  p = r;

  for (tok = strtok (r, blank);
       tok != NULL;
       tok = strtok (NULL, blank))
    i++;

  free (p);
  return i;
}

PRIVATE char**
ConvertPars (argc, s)
  int  argc;
  char *s;
{
  char *blank = " ", *tok = NULL, *r, *p, **argv = NULL;
  int i = 0;

  if ((s == NULL) || (strlen (s) == 0) || (argc == 0))
    return NULL;

  argv = (char**) emalloc (argc * sizeof (char*));
  for (i = 0; i < argc; i++)
    argv[i] = NULL;

  r = strdup (s);
  p = r;

  for (i = 0, tok = strtok (r, blank);
       tok != NULL;
       i++, tok = strtok (NULL, blank))
    argv[i] = strdup (tok);

  free (p);
  return argv;
}

/* checks if the arguments match with
 * the specification parameters
 * and initializes them in the kernel tree
 */
PRIVATE void
set_arguments (S, pars)
  spe  S;
  char *pars;
{
  TNODE   *first;
  char    **troceado;
  INTlist vl, varl;
  int     i;

  ARGC = NumPars (pars);

  first = S->BUTlist->sons;              /* The first behaviour unit */
  if (ARGC == 0) {
    if (find_attr (c_var_list, first) != NULL) {
      (void)fprintf (stderr, "Wrong parameter number\n");
      exit (1);
    }
  }
  else {
    if (find_attr (c_var_list, first) == NULL) {
      (void)fprintf (stderr, "Wrong parameter number, none expected\n");
      exit (1);
    }
    else {
      varl = (INTlist)takeclr (c_var_list, first);
      if (ARGC != INTlength (varl)) {
	(void)fprintf (stderr,
		       "Wrong parameter number, %d expected, %d passed \n",
		       INTlength ((INTlist)takeclr (c_var_list, first)),
		       ARGC);
	exit (1);
      }
    }
  }

  /* prepare the global variables with the data */
  if (ARGC != 0) {
    ARGV = (kdatum*)emalloc (ARGC * sizeof (kdatum));
    troceado = ConvertPars (ARGC, pars);
    for (i = 0; i < ARGC; i++)
      ARGV[i] = NULL;
    for (vl = varl, i = 0; (i < ARGC); i++, vl = INTtail (vl))
      if (troceado[i] == NULL) {
	(void)fprintf (stderr, "Null parameter for %d\n", i);
	exit (1);
      }
      else
	if (!kd_parse (id2uisort (S, (CLR_TYPE)INThead (vl)),
		       &(troceado[i]), &(ARGV[i])))
	  fatal_error ("Cannot parse value for parameter",
		       __FILE__, __LINE__);
  }
}

PRIVATE void
BUT_convert_pars (S, vexpl, pi)
  spe   S;
  TNODE *vexpl;
  int   pi;
{
  TNODE *aux;
  int   i;

  assert (vexpl->type == tvalue_exp_list);
  assert (ARGC == 0);
  assert (ARGV == NULL);

  for (aux = gt_fs (vexpl); aux != NULL; aux = gt_rb (aux))
    ARGC++;

  if (ARGC != 0) {
    ARGV = (kdatum*)emalloc (ARGC * sizeof (kdatum));
    for (aux = gt_fs (vexpl), i = 0;
	 i < ARGC;
	 i++, aux = gt_rb (aux))
      ARGV[i] = val_exp2kdatum (S, pi, aux);
  }
}

PRIVATE krnlt
search_enabling_kt (kt)
  krnlt kt;
{
  if (kt == NULL)
    return NULL;
  if (kt->class == LENABLING)
    return kt;
  else
    return search_enabling_kt (kt->fth);
}

PUBLIC void
set_values_for_exit (S, sof, kt)
  spe     S;
  soffert *sof;
  krnlt   kt;
{
  INTlist varl = NULL;
  int i, ldiui;

  if (sof->nexp > 0) {
    kt = search_kt (INThead (sof->ktl), kt);
    if ((kt = search_enabling_kt (kt)) != NULL) { /* An enabling was found */
      assert (kt->class == LENABLING);
      /* well, updating variables of enabling */
      for (i = 0, varl = (INTlist)takeclr (c_var_list, kt->lb);
	   varl != NULL;
	   i++, varl = INTtail (varl)) {
	assert (i < sof->nexp);
	if (sof->expl[i]->val != NULL) {
	  ldiui = get_var_id (unique_var_id (S, INThead (varl), kt->pi),
			      id2uisort (S, (CLR_TYPE)INThead (varl)));
	  if (ldiui >= 0)
	    fatal_error ("Cannot find variable", __FILE__, __LINE__);
	}
	if (!let_var (ldiui, kd_rw_node (kd_copy (sof->expl[i]->val))))
	  fatal_error ("Cannot initilize variable", __FILE__, __LINE__);
      }
    }
  }
}

PRIVATE TNODE*
search_BUT_inst (butl, crt)
  TNODE *butl; /* BUT list */
  int   crt;   /* BUT to be searched */
{
  for (butl = gt_fs (butl); butl != NULL; butl = gt_rb (butl)) {
    if (crt == (int)takeclr (c_BUT_number, butl))
      return butl;
  }
  fatal_error ("Such BUT does not exist", __FILE__, __LINE__);
  return NULL; /* to shut lint off */
}

PRIVATE void
build_kt (S, r, kt)
  spe   S;
  TNODE *r;
  krnlt kt;
{
  TNODE *h[MAX_TNODES];

  h[0] = r;
  switch (lbm_node_type (S, r)) {
  case _lbm_1 :
    myheval (h[0], h);

    build_kt (S, h[2], kt);

    break;
  case _BUT_definition_list_1 :
    h[1]= gt_fs (h[0]);
    h[5]= gt_ls (h[0]);

    build_kt (S, h[1], kt);

    break;
  case _BUT_definition_1 :
    myheval (h[0], h);

    kt->lb  = h[1];
    kt->BUT = (int)takeclr (c_BUT_number, h[0]);
    kt->pi = S->lastPI++;

    if (ARGC != 0) {
      /* Declares & initializes variables */
      BUT_definition_parameters (S, kt, ARGC, ARGV, h[0]);
      while (ARGC > 0)
	ARGV[--ARGC] = NULL;
      assert (ARGC == 0);
      free ((char*)ARGV);
      ARGV = NULL;
    }

    if (S->doph) {
      kt->ph = new_node (0);
      set_attr (c_BUT_number, kt->ph, (CLR_TYPE)kt->BUT);
      set_attr (c_proc, kt->ph, (CLR_TYPE)kt->pi);
      set_attr (c_procname, kt->ph, (CLR_TYPE)l2s (S, kt->BUT));
      if (kt->fth != NULL)
	if (!lnsons (kt->fth->ph, kt->ph))
	  fatal_error ("cannot link sons", __FILE__, __LINE__);
    }
    build_kt (S, h[1], kt);

    break;
  case _let_exp_1 :
    myheval (h[0], h);

    let_exp_dec_vars (S, kt, kt->pi, h[1]);
    kt->lb = h[2];
    build_kt (S, h[2], kt);

    break;
  case _var_choice_exp_1 :
    myheval (h[0], h);

    fatal_error ("Choice on variables not supported", __FILE__, __LINE__);

    break;
  case _gate_choice_exp_1 :
  case _par_exp_full_synch_1 :
  case _par_exp_inter_1 :
  case _par_exp_expli_1 :

    fatal_error ("Tree bad transformed", __FILE__, __LINE__);

    break;
  case _hiding_exp_1 :
    myheval (h[0], h);

    kt->class = LHIDE;
    kt->gtes  = INTdup ((INTlist)takeclr (c_gate_decl, h[0]));

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    break;
  case _enable_exp_1 :
    myheval (h[0], h);

    enable_exp_dec_vars (S, kt, kt->pi, r);

    kt->class = LENABLING;

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    kt->son2      = new_kt ();
    kt->son2->uid = S->lastUID++;
    kt->son2->fth = kt;
    kt->son2->lb  = h[2];
    kt->son2->BUT = kt->BUT;
    kt->son2->ph  = kt->ph;
    kt->son2->pi  = kt->pi;
    /* Second son of a enabling is not expanded, */
    /* until an "exit" be offered.               */

    break;
  case _disable_exp_1 :
    myheval (h[0], h);

    kt->class = LDISABLING;

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    kt->son2      = new_kt ();
    kt->son2->uid = S->lastUID++;
    kt->son2->fth = kt;
    kt->son2->lb  = h[2];
    kt->son2->BUT = kt->BUT;
    kt->son2->ph  = kt->ph;
    kt->son2->pi  = kt->pi;
    build_kt (S, h[2], kt->son2);

    break;
  case _parallel_full_synch_1 :
    myheval (h[0], h);

    kt->class = LFULL_SYNC;

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    kt->son2      = new_kt ();
    kt->son2->uid = S->lastUID++;
    kt->son2->fth = kt;
    kt->son2->lb  = h[2];
    kt->son2->BUT = kt->BUT;
    kt->son2->ph  = kt->ph;
    kt->son2->pi  = kt->pi;
    build_kt (S, h[2], kt->son2);

    break;
  case _parallel_interleaving_1 :
    myheval (h[0], h);

    kt->class = LINTERLEAVING;

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    kt->son2      = new_kt ();
    kt->son2->uid = S->lastUID++;
    kt->son2->fth = kt;
    kt->son2->lb  = h[2];
    kt->son2->BUT = kt->BUT;
    kt->son2->ph  = kt->ph;
    kt->son2->pi  = kt->pi;
    build_kt (S, h[2], kt->son2);

    break;
  case _parallel_explicit_1 :
    myheval (h[0], h);

    kt->class = LSYNC;
    kt->gtes  = INTdup ((INTlist)takeclr (c_gate_list, h[0]));

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    kt->son2      = new_kt ();
    kt->son2->uid = S->lastUID++;
    kt->son2->fth = kt;
    kt->son2->lb  = h[2];
    kt->son2->BUT = kt->BUT;
    kt->son2->ph  = kt->ph;
    kt->son2->pi  = kt->pi;
    build_kt (S, h[2], kt->son2);

    break;
  case _choice_exp_1 :
    myheval (h[0], h);

    kt->class = LCHOICE;

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->BUT = kt->BUT;
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, h[1], kt->son1);

    kt->son2      = new_kt ();
    kt->son2->uid = S->lastUID++;
    kt->son2->fth = kt;
    kt->son2->lb  = h[2];
    kt->son2->BUT = kt->BUT;
    kt->son2->ph  = kt->ph;
    kt->son2->pi  = kt->pi;
    build_kt (S, h[2], kt->son2);

    break;
  case _guard_exp_1 :
    {
      int res;
      kdatum val1;
      kdatum val2;
      cond g;

      myheval (h[0], h);

      /* The rest of the tree would be */
      /* built if the guard successes  */

      val1 = val_exp2kdatum (S, kt->pi, h[1]);
      val2 = val_exp2kdatum (S, kt->pi, h[2]);
      res = ldiequal (kd_copy (val1), kd_copy (val2));
      if (res == NEQ) {
	kt->class = LSTOP;
      }
      else {
	kt->lb = h[3];
	build_kt (S, h[3], kt);
	if ((res == UNDEF) && S->keepguards) {
	  g = new_cond ();
	  g->val1 = kd_copy (val1);
	  g->val2 = kd_copy (val2);
	  kt->grdl = CNDcons (g, kt->grdl);
	}
      }
      kd_free (val1);
      kd_free (val2);
    }
    break;
  case _external_offer_1 :
    myheval (h[0], h);

    kt->class = LACTION;
    kt->g     = (int)takeclr (c_gate_id, h[0]);
    if (h[1] != NULL)
      ext_off_dec_vars (S, kt, kt->pi, h[1]);

    break;
  case _internal_action_1 :
    myheval (h[0], h);

    kt->class = LINTERNAL;

    break;
  case _stop_exp_1 :
    myheval (h[0], h);

    kt->class = LSTOP;

    break;
  case _exit_exp_1 :
    myheval (h[0], h);

    kt->class = LEXIT;
    kt->g     = LEXITG;

    break;
  case _BUT_instantiation_1 :
    myheval (h[0], h);

    kt->class     = LINSTANTIATION;

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = search_BUT_inst (S->BUTlist,
				     (int)takeclr (c_BUT_number, r));
    if (find_attr (c_gate_list, r) != NULL) {
      /* actual */
      kt->gtes = INTdup ((INTlist)takeclr (c_gate_list, h[0]));
      /* formal */
      kt->rlb =	create_rlbset (kt->gtes,
			       (INTlist)takeclr (c_gate_decl, kt->son1->lb));
    }

    /* The parameters for the BUT should be prepared. They   */
    /* are declared and initialized in the _BUT_definition.  */
    /* They are passed in ARGC and ARGV (global variables).  */
    if (h[1] != NULL)
      BUT_convert_pars (S, h[1], kt->pi);

    build_kt (S, kt->son1->lb, kt->son1);

    break;
  case _relabel_1 :
    myheval (h[0], h);

    kt->class = LRELABEL;
    kt->gtes  = INTdup ((INTlist)takeclr (c_gate_list, h[0])); /* actual */
    kt->rlb   =
      create_rlbset (kt->gtes,
		     (INTlist)takeclr (c_gate_decl, h[0])); /* formal */

    kt->son1      = new_kt ();
    kt->son1->uid = S->lastUID++;
    kt->son1->fth = kt;
    kt->son1->lb  = h[1];
    kt->son1->ph  = kt->ph;
    kt->son1->pi  = kt->pi;
    build_kt (S, kt->son1->lb, kt->son1);

    break;
  case _call_1 :
    myheval (h[0], h);

    kt->lb = search_BUT_inst (S->BUTlist, (int)takeclr (c_BUT_number, r));

    build_kt (S, kt->lb, kt);

    break;
  default :
    fatal_error ("Wrong node", __FILE__, __LINE__);
  }
}

PRIVATE TNODE*
next_lbm_state (S, r)
  spe   S;
  TNODE *r;
{
  TNODE *h[MAX_TNODES];

  h[0] = r;
  switch (lbm_node_type (S, r)) {
  case _external_offer_1 :
    myheval (h[0], h);
    return h[3];
  case _internal_action_1 :
    myheval (h[0], h);
    return h[1];
  case _exit_exp_1 :
    return NULL;      /* No more states to be reached */
  default :
    fatal_error ("Wrong state searching next state", __FILE__, __LINE__);
    return NULL; /* To shut lint off */
  }
}

/* Concatenates two I2T tables
 * arguments are "freeded" (virtually).
 * If you want to keep arguments,
 * pass a copy to this function
 */
PRIVATE I2T*
addtable (first, second)
  I2T *first, *second;
{
  I2T *new = NULL;

  if ((first == NULL) && (second == NULL))
    return NULL;
  if (first == NULL)
    return second;
  if (second == NULL)
    return first;

  new = first;
  while (second->size > 0) {
    (void)I2Tadd (second->data[0], second->data[1], new);
    I2Trm (0, second);
  }
  fI2T ((CLR_TYPE)second);
  return new;
}

/* This function colapses two consecutive relabeling nodes:       */
/*          |		The kt is a relabeling node which only    */
/* relabel ( ) (kt)	son is also a relabeling. Both of them    */
/*          |  		may be colapse in one node.               */
/*          |		So, the node son will be unchained from   */
/*          |		his father, and the father will be freed. */
/*          |		The variable declaration of the father    */
/* relabel ( )		will be kept in the son. There is no      */
/*          |		brother to be care of.                    */
PRIVATE krnlt
simp_kt_rlb (kt)
krnlt kt;
{
  krnlt son;

  assert (kt != NULL);
  assert ((kt->son1 != NULL) && (kt->son2 == NULL));
  assert (((kt->class == LRELABEL) && (kt->son1->class == LRELABEL)) ||
	  ((kt->class == LRELABEL) && (kt->son1->class == LRELABEL)));

  son = kt->son1;
  kt->son1 = NULL;

  /* dealing with declared variables */
  if (kt->class == LRELABEL) { /* joining declarations */
    son->env = addtable (kt->env, son->env);
    kt->env = NULL;
  }
  else { /* freeing variables out of scope */
    free_environ (kt->env);
    kt->env = NULL;
  }

  /* Joining relabelings */
  son->rlb = simp_relabel (kt->rlb, son->rlb);
  kt->rlb = NULL;

  free_kt (kt);

  return son;
}

/* This function cuts off the tree, in the following way:          */
/*            |			The father is an operation which   */
/*        op ( ) (father)	is about to be simplified. The son */
/*           / \		is the node which will remain.     */
/*          /   \		So, the node son will be unchained */
/*         /     \		from his father, and the father    */
/*        /       \		will be freed. The variable decla- */
/*   B1 ( )    B2 ( )  (son)	ration of the father will be kept  */
/*              ^		in the son. The brother, of course */
/*		|		will die with the father.          */
/*	    to be kept						   */
PRIVATE krnlt
simp_kt (father, son)
  krnlt father, son;
{
  assert (father != NULL);
  assert (son != NULL);
  assert ((son == father->son1) || (son == father->son2));

  /* keep declared variables */
  son->env = addtable (father->env, son->env);
  father->env = NULL;

  if (father->son1 == son) /* Unlinking the proper son */
    father->son1 = NULL;
  else
    father->son2 = NULL;

  free_kt (father);

  return son;
}

PUBLIC krnlt
simplify_kt (kt)
  krnlt kt;
{
  krnlt   father = NULL;

  assert (kt != NULL);
  assert (kt->xto != NOCHOOSEN);

  father = FATHER (kt);

  switch (kt->class) {
  case LSTOP :
  case LINTERNAL :
  case LACTION :
  case LEXIT :
    /* Nothing to simplify */
    break;
  case LCHOICE :
    if ((kt->son1->xto == NOCHOOSEN) && (kt->son2->xto == NOCHOOSEN))
      /* this may happend because the kernel tree evolutes BEFORE  */
      /* simplify it. So, for example a; (exit [] stop) if a is    */
      /* offered, the choice substitutes it, and is marked as such */
      /* However, its sons are not marked: they are just born :-)  */
      break;
    if (kt->son1->xto != NOCHOOSEN) {
      kt = simp_kt (kt, kt->son1);
      kt->fth = father;
      kt = simplify_kt (kt);
    }
    else if (kt->son2->xto != NOCHOOSEN) {
      kt = simp_kt (kt, kt->son2);
      kt->fth = father;
      kt = simplify_kt (kt);
    }
    break;
  case LFULL_SYNC :
  case LINTERLEAVING :
  case LSYNC :
    if (kt->son1->xto != NOCHOOSEN) {
      kt->son1 = simplify_kt (kt->son1);
    }
    if (kt->son2->xto != NOCHOOSEN) {
      kt->son2 = simplify_kt (kt->son2);
    }
    break;
  case LDISABLING :
    if (kt->son2->xto != NOCHOOSEN) {
      kt = simp_kt (kt, kt->son2);
      kt->fth = father;
      kt = simplify_kt (kt);
    }
    else if (kt->son1->xto != NOCHOOSEN) {
      if (kt->son1->xto == EXITED) {
	/* taking care exit* [> B2 => stop    */
	/* The exit would have been converted */
	/* in a stop by the evol_kt function  */
	kt = simp_kt (kt, kt->son1);
	kt->fth = father;
      }
      else
	kt->son1 = simplify_kt (kt->son1);
    }
    break;
  case LENABLING :
    if (kt->son1->xto != NOCHOOSEN)
      /* taking care exit* >> B1 >> B2  =>  B1 >> B2      */
      if (kt->son1->xto == EXITED) {
	kt = simp_kt (kt, kt->son2);
	kt->fth = father;
      }
      else {
	kt->son1 = simplify_kt (kt->son1);
      }
    break;
  case LRELABEL :
    if (kt->son1->xto != NOCHOOSEN) {
      kt->son1 = simplify_kt (kt->son1);
    }
    if (kt->son1->class == LRELABEL) {
      kt = simp_kt_rlb (kt);
      kt->fth = father;
    }
    break;
  case LHIDE :
    if (kt->son1->xto != NOCHOOSEN) {
      kt->son1 = simplify_kt (kt->son1);
    }
    break;
  case LINSTANTIATION :
    if (kt->son1->xto != NOCHOOSEN) {
      kt->son1 = simplify_kt (kt->son1);
    }
/*    if (kt->son1->class == LINSTANTIATION) {
      kt = simp_kt_rlb (kt);
      kt->fth = father;
    }
*/
    break;
    default :
      fatal_error ("No such node simplifying a tree", __FILE__, __LINE__);
  }
  kt->xto = NOCHOOSEN;
  return kt;
}

PUBLIC void
label_kt (kt, lab)
  krnlt kt;
  int   lab;
{
  krnlt father = FATHER (kt);

  assert ((lab == EXITED) || (lab == NORMAL));
  kt->xto = lab;
  if (father != NULL) {
    if ((father->class == LENABLING) && (lab == EXITED))
      label_kt (father, NORMAL);
    else
      label_kt (father, lab);
  }
}

PUBLIC void
init_kt (S, pars)
  spe  S;
  char *pars;
{
  set_arguments (S, pars);
  S->kt = new_kt ();
  S->kt->uid = S->lastUID++;
  build_kt (S, S->lbmroot, S->kt);
}

PRIVATE krnlt
look_enable_ancestor (kt)
  krnlt kt;
{
  if (kt == NULL)
    return NULL;
  if (FATHER (kt) == NULL)
    return NULL;
  if (FATHER (kt)->class == LENABLING)
    return FATHER (kt);
  return look_enable_ancestor (FATHER (kt));
}

PUBLIC void
evol_kt (S, r, kt)
  spe   S;
  TNODE *r;
  krnlt kt;
{
  krnlt aux = NULL;

  kt->lb = next_lbm_state (S, kt->lb);
  if (kt->lb != NULL)
    /* If NULL, there are no more states to be reached */
    build_kt (S, kt->lb, kt);
  else {
    assert (kt->class == LEXIT);
    if ((aux = look_enable_ancestor (kt)) != NULL)
      build_kt (S, SSON (aux)->lb, SSON (aux));
    kt->class = LSTOP; /* An EXIT which was offered becomes a STOP */
  }
}

PUBLIC void
clean_offer_propagation (kt)
  krnlt kt;
{
  if (kt->soffs != NULL) { /* Cleanning this node */
    free_sset_off (kt->soffs);
    kt->soffs = NULL;
  }

  switch (kt->class) { /* Cleaning the sons */
                         /**** TERMINALS NODES ****/
  case LSTOP :
  case LINTERNAL :
  case LACTION :
  case LEXIT :
    break;

                      /**** NON TERMINALS NODES ****/
  case LCHOICE :
  case LFULL_SYNC :
  case LINTERLEAVING :
  case LSYNC :
  case LDISABLING :
    clean_offer_propagation (kt->son1);
    clean_offer_propagation (kt->son2);
    break;
  case LENABLING :
  case LHIDE :
  case LRELABEL :
  case LINSTANTIATION :
    clean_offer_propagation (kt->son1);
    break;
  default :
    fatal_error ("No such node in stable tree", __FILE__, __LINE__);
  }
}

PRIVATE soffert*
collect_ready_actions_from_sons (kt)
  krnlt kt;
{
  soffert *new;

  new = Ready_fun (cp_sset_off (kt->son1->soffs));
  if (kt->son2 != NULL)
    new = union_sset_off (Ready_fun (cp_sset_off (kt->son2->soffs)), new);
  return new;
}

PUBLIC void
offer_propagation (S, kt)
  spe   S;
  krnlt kt;
{
  soffert *soff, *aux;

  if (kt->soffs != NULL) /* evaluated in some other phase */
    return;

  switch (kt->class) {
                         /**** TERMINALS NODES ****/
  case LSTOP :
    kt->soffs = NULL;
    break;
  case LINTERNAL :
    soff = new_soffert ();
    soff->ready = TRUE;
    soff->g = LINTERG;     /* Internal gate */
    soff->ktl = INTcons (kt->uid, (INTlist)NULL);
    kt->soffs = soff;
    break;
  case LACTION :
    soff = new_soffert ();
    soff->g = (int)takeclr (c_gate_id, kt->lb); /* Identifier of the gate */
    add_exper (S, soff, kt->pi, kt->lb);
    add_predi (S, soff, kt->pi, kt->lb);
    soff->ktl = INTcons (kt->uid, (INTlist)NULL);
    kt->soffs = soff;
    break;
  case LEXIT :
    soff = new_soffert ();
    soff->g = LEXITG;     /* the delta gate */
    add_exper (S, soff, kt->pi, kt->lb);
    soff->ktl = INTcons (kt->uid, (INTlist)NULL);
    kt->soffs = soff;
    break;

                      /**** NON TERMINALS NODES ****/
  case LCHOICE :
    offer_propagation (S, kt->son1);
    offer_propagation (S, kt->son2);
    kt->soffs = union_sset_off (cp_sset_off (kt->son1->soffs),
				cp_sset_off (kt->son2->soffs));
    break;
  case LFULL_SYNC :
    offer_propagation (S, kt->son1);
    offer_propagation (S, kt->son2);
    kt->soffs = inter_sset_off (cp_sset_off (kt->son1->soffs),
				cp_sset_off (kt->son2->soffs));
    kt->soffs = union_sset_off (collect_ready_actions_from_sons (kt),
				kt->soffs);
    break;
  case LINTERLEAVING :
    offer_propagation (S, kt->son1);
    offer_propagation (S, kt->son2);
    kt->soffs = inter_sset_off (Sd_fun (cp_sset_off (kt->son1->soffs)),
				Sd_fun (cp_sset_off (kt->son2->soffs)));
    kt->soffs = union_sset_off (Dd_fun (cp_sset_off (kt->son1->soffs)),
				kt->soffs);
    kt->soffs = union_sset_off (Dd_fun (cp_sset_off (kt->son2->soffs)),
				kt->soffs);
    kt->soffs = union_sset_off (collect_ready_actions_from_sons (kt),
				kt->soffs);
    break;
  case LSYNC :
    offer_propagation (S, kt->son1);
    offer_propagation (S, kt->son2);
    kt->soffs =
	  inter_sset_off (Sgd_fun (cp_sset_off (kt->son1->soffs), kt->gtes),
			  Sgd_fun (cp_sset_off (kt->son2->soffs), kt->gtes));
    kt->soffs =
	  union_sset_off (Dgd_fun (cp_sset_off (kt->son1->soffs), kt->gtes),
			  kt->soffs);
    kt->soffs =
	  union_sset_off (Dgd_fun (cp_sset_off (kt->son2->soffs), kt->gtes),
			  kt->soffs);
    kt->soffs = union_sset_off (collect_ready_actions_from_sons (kt),
				kt->soffs);
    break;
  case LDISABLING :
    offer_propagation (S, kt->son1);
    offer_propagation (S, kt->son2);
    kt->soffs = union_sset_off (cp_sset_off (kt->son1->soffs),
				cp_sset_off (kt->son2->soffs));
    break;
  case LENABLING :
    offer_propagation (S, kt->son1);
    kt->soffs = Dd_fun (cp_sset_off (kt->son1->soffs));
    aux = Become_Ready (Sd_fun (cp_sset_off (kt->son1->soffs)));
    kt->soffs = union_sset_off (aux, kt->soffs);
    kt->soffs = union_sset_off (collect_ready_actions_from_sons (kt),
				kt->soffs);
    break;
  case LHIDE :
    offer_propagation (S, kt->son1);
    kt->soffs = Dg_fun (cp_sset_off (kt->son1->soffs), kt->gtes);
    aux = Become_Ready (Sg_fun (cp_sset_off (kt->son1->soffs), kt->gtes));
    kt->soffs = union_sset_off (aux, kt->soffs);
    kt->soffs = union_sset_off (collect_ready_actions_from_sons (kt),
				kt->soffs);
    break;
  case LRELABEL :
  case LINSTANTIATION :
    offer_propagation (S, kt->son1);
    if (kt->rlb != NULL) {
      kt->soffs = Rp_fun (kt->rlb->formal, kt->rlb->actual,
			  cp_sset_off (kt->son1->soffs));
      kt->soffs = union_sset_off (collect_ready_actions_from_sons (kt),
				  kt->soffs);
    }
    else
      kt->soffs = cp_sset_off (kt->son1->soffs);
    break;
    default :
      fatal_error ("No such node in stable tree", __FILE__, __LINE__);
  }
}

PUBLIC soffert*
available_events (kt)
  krnlt kt;
{
  return check_predicates (cp_sset_off (kt->soffs));
}

PUBLIC krnlt
cp_kt (kt)
  krnlt kt;
{
  krnlt aux;

  aux = new_kt ();

  aux->uid   = kt->uid;
  aux->class = kt->class;
  if (kt->env != NULL)
    aux->env = I2Tdup (kt->env);
  aux->lb    = kt->lb;
  if (kt->son1 != NULL) {
    aux->son1 = cp_kt (kt->son1);
    aux->son1->fth = aux;
  }
  if (kt->son2 != NULL) {
    aux->son2 = cp_kt (kt->son2);
    aux->son2->fth = aux;
  }
  aux->xto   = kt->xto;
  aux->BUT   = kt->BUT;
  aux->ph    = cp_tree (kt->ph, TRUE);
  aux->pi    = kt->pi;
  if (kt->soffs != NULL)
    aux->soffs = cp_sset_off (kt->soffs);
  aux->g     = kt->g;
  aux->gtes  = INTdup (kt->gtes);
  if (kt->rlb != NULL)
    aux->rlb  = rlbsetdup (kt->rlb);

  return aux;
}

PUBLIC proclist
getactpikt (tbl, kt)
  proclist tbl;
  krnlt kt;
{
  if (kt != NULL) {
    if (kt->class != LINSTANTIATION)
      if (!INTIsIn (kt->pi, tbl))
	tbl = INTcons (kt->pi, tbl);
    tbl = getactpikt (tbl, kt->son1);
    tbl = getactpikt (tbl, kt->son2);
  }
  return tbl;
}


/* Search a kt node by
 * Kernel Tree Node Unique Identifier.
 * Each node is univoquely identify
 */
PUBLIC krnlt
search_kt (ui, kt)
  int   ui;
  krnlt kt;
{
  krnlt aux = NULL;

  if (kt == NULL)
    return NULL;  /* not found */
  if (kt->uid == ui)
    return kt;    /* found! */
  aux = search_kt (ui, kt->son1);
  if (aux != NULL)
    return aux;
  return search_kt (ui, kt->son2);
}

/* Search a kt node by "pi"
 * i.e., the Process Instance
 * several nodes may have the same "pi"
 * the first encountered is returned
 */
PUBLIC krnlt
search_pi_kt (pi, kt)
  int   pi;
  krnlt kt;
{
  krnlt aux = NULL;

  if (kt == NULL)
    return NULL;  /* not found */
  if (kt->pi == pi)
    return kt;    /* found! */
  aux = search_pi_kt (pi, kt->son1);
  if (aux != NULL)
    return aux;
  return search_pi_kt (pi, kt->son2);
}

