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

/***********************************
  
  Miguel Angel Palomares Ortega
  
  10-9-1992
  
  
  This module contains  functions that implement a Inverse Expansion 
  algorithm. This decomposition will be posible with all type of
  behaviours (even recursive or deterministic). The behaviours will
  be decomposed into two behaviours that will communicate each other
  with visible and invisible (hidden) actions.
  
  
  ************************************/

#ifdef INVEXP

#include "iefunc.h"
#include "ie_k.h"
#include "licell.h"
#include "badefca.h"
#include "babeh.h"
#include "listdh.h"
#include "limisc.h"
#include "lilists.h"
#include "listdout.h"
#include "baattr.h"
#include "expostex.h"
#include "eximmed.h"
#include "expre_br.h"
#include "batables.h"
#include "exexpans.h"
#include "baattr.h"
#include "libst.h"


#define TABLE_SIZE 100   
#define LENGTH 10



/******************************************************************
 *
 *  type definitions
 *
 *******************************************************************/



/* KTypeTyp 
 * Contains type of K gate. 
 */
typedef enum { ka1,
		 ka2,
		 kb1,
		 kb2} KTypeTyp;    


/* GateTyp
 * Contains type of decomposition gateset.
 */
typedef enum { GS1,
		 GS2} GateTyp;     


/* EntryTyp
 * Defines an entry of TabTyp table. "desc" is the descriptor of the 
 * decomposed process , "d1" is  the descriptor of its gateset 1 process 
 * and "d2" is the descriptor of its gateset 2 process.
 */
typedef struct { DescriptorTyp desc;
                 DescriptorTyp d1;
                 DescriptorTyp d2;
               } EntryTyp;


/* TabTyp
 * Table used for decomposition of processes.
 */
typedef struct { EntryTyp* entry;
                 int last;
                 int size;
               } TabTyp;



/******************************************************************
 *
 *  globals variables
 *
 *******************************************************************/


static int num_ki;     /* counter for Ki's */

static int num_kc;     /* counter for Kc`s */

static int num_kp;     /* counter for Kp`s */

static DescriptorTyp tablelength; /* contains the length of the Gate Table 
                                     before Adding more gates */

static ListTyp list;   /* list used for recursive proposals */

static BstTyp bst;     /* binary tree used for recursive proposals */

static TabTyp tab;     /* table for decomposition of processes */




/******************************************************************
 *
 *                     Table Functions
 *
 *******************************************************************/



/* InitTab
 * Initialices tab and allocates memory.
 */
static void InitTab()
     
{
  tab.entry = (EntryTyp *)emalloc(TABLE_SIZE*sizeof(EntryTyp));
  tab.last = 0;
  tab.size = TABLE_SIZE;
}



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



/* ReallocTab 
 * Reallocates memory for tab.
 */
static void ReallocTab()
     
{
  tab.entry = (EntryTyp *)erealloc((void*)tab.entry,(int)(tab.size + TABLE_SIZE)*sizeof(EntryTyp));
  tab.size += TABLE_SIZE;
}



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



/* Add_Tab  
 * Adds the descriptor "newd" of the process with the decomposition
 * gateset indicated by "gtype" being "d" the descriptor of the de -
 * composed process.
 */
static void Add_Tab(d,newd,gtype)
     DescriptorTyp d,newd;
     GateTyp gtype;
     
{
  int i;
  
  
  if (tab.last == tab.size)
    ReallocTab();
  
  i = 0;
  while ( (tab.entry[i].desc != d) && (i < tab.last) )
    i++;
  
  tab.entry[i].desc = d;
  
  switch(gtype)
    {
    case GS1:
      tab.entry[i].d1 = newd;
      tab.entry[i].d2 = 0;
      break;
      
    case GS2:
      tab.entry[i].d2 = newd;
      break;
    }
  
  if (i == tab.last)
    tab.last ++;
}




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



/* LookTab
 * returns (if exists) the descriptor of the decomposition process of
 * the process "d" with the gateset type "gtype". If not exists it
 * returns 0.
 */
static DescriptorTyp LookTab(d,gtype)
     DescriptorTyp d;
     GateTyp gtype;
     
{
  int i;
  
  for (i = 0 ; i < tab.last ; i++)
    if (tab.entry[i].desc == d)
      {
        if (gtype == GS1)
          return tab.entry[i].d1;
        else if (gtype == GS2)
          return tab.entry[i].d2;
      }
  return 0;
}



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



/* FreeTab
 * Frees memory allocated to tab.
 */
static void FreeTab()
     
{
  free((char *)tab.entry);
}



/*****************************************************************
 *
 *              Binary Search Tree functions 
 *
 ******************************************************************/




/* BstKey
 * Returns the bst key.
 */
static int BstKey(desc)
     int desc;
     
{
  return desc;
}



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


/* BstCmp
 * Comparation function for the bst.
 */
static boolean BstCmp(desc1,desc2)
     int desc1,desc2;
     
{
  return (desc1 == desc2);
}




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


/* BstFree
 * Free memory function for the bst (it is a bst of integers and so
 * we don't need to free memory).
 */
static void BstFree(desc)
     int desc;
     
{
#ifdef lint
  (void)printf("%d",desc);
#endif
  return;
}



/******************************************************************
 *
 *  Auxiliar Functions
 *
 *******************************************************************/




/* KGetGatesOfProc
 * Gets all the gates of "b" in "gs".
 */
static void KGetGatesOfProc(b,gs)
     BehTyp b;
     GateSetTyp gs;
     
{
  DescriptorTyp i,num,name;
  CellTypeTyp type;
  
  
  LASSERT(b != NULL);
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return ;
      
    case GateC:
      name = LookNameB(b);
      if (GateInGS(name,gs) == FALSE)
        gs = AddGS(gs,name);
      
      KGetGatesOfProc(LookArgB(b,1),gs);
      return;
      
    case IC:
      KGetGatesOfProc(LookArgB(b,1),gs);
      return;
      
    case AlternativeC:
      num = NumArgB(b);
      for (i = 1; i <= num ; i++)
        KGetGatesOfProc(LookArgB(b,i),gs);
      
      return;
      
    case ProcessInstC:
      KGetGatesOfProc(GetP_def(LookNameB(b)),gs);
      return;
      
    case ProcessDefC:
      if (LookForBST((DataBstTyp)LookNameB(b),bst,BstKey,BstCmp) != NULL)
        return;
      else
        bst = InsertBST((DataBstTyp)LookNameB(b),bst,BstKey);
      
      KGetGatesOfProc(LookArgB(b,1),gs);
      return; 
      
    default:
      Error("invalid cell type.");
      break;
    }
  
}





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




/* Call_KGetGates
 * Returns the gates of the process "b".
 */
static GateSetTyp Call_KGetGates(b)
     BehTyp b;
     
{
  GateSetTyp gs;
  
  
  LASSERT(LookTypeB(b) == ProcessDefC);
  gs = NewGS();
  bst = CreateBST();
  KGetGatesOfProc(b,gs);
  FreeBST(bst,BstFree);
  
  return gs;
}




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




/* KPutGatestoInsts
 * Puts the gatelist attribute to all process instantiations of "b".
 */
static void KPutGatestoInsts(b)
     BehTyp b;
     
{
  DescriptorTyp i,num;
  BehTyp bdef;
  CellTypeTyp type;
  PAttrTyp at;
  
  
  LASSERT(b != NULL);
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      KPutGatestoInsts(LookArgB(b,1));
      return;
      
    case IC:
      KPutGatestoInsts(LookArgB(b,1));
      return;
      
    case AlternativeC:
      num = NumArgB(b);
      for (i = 1 ; i <= num ; i++)
        KPutGatestoInsts(LookArgB(b,i));
      
      return;
      
    case ProcessInstC:
      bdef = GetP_def(LookNameB(b));
      at = LookA(bdef,GLA);
      PutA(b,at);
      
      return;
      
    case ProcessDefC:
      KPutGatestoInsts(LookArgB(b,1));
      return;
      
    default:
      Error("Invalid cell type.");
      break;
    }
}




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




/* KPutGatestoProcs
 * Puts gatelist attribute to all "ProcessDefC" cells between the position
 * "first" and "last" of the process table and to all "ProcessInstC" cells
 * that are called in these processes.
 */
static void KPutGatestoProcs(first,last)
     DescriptorTyp first,last;
     
{
  DescriptorTyp i;
  BehTyp bdef;
  GateSetTyp gs;
  GateListTyp gl;
  PAttrTyp at;
  
  
  
  for (i = first ; i <= last ; i++)
    {
      bdef = GetP_def(i);
      gs = Call_KGetGates(bdef);
      gl = GateSet_to_GateList(gs);
      FreeGS(gs);
      at = MakeA((AttrValueTyp)gl,GLA);
      PutA(bdef,at);
    }
  
  for (i = first ; i <= last ; i++)
    KPutGatestoInsts(GetP_def(i));
}




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



/* Kill_IC
 * "Kills" useless IC actions.
 */
static void Kill_IC(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,num;
  BehTyp nextb,branch;
  
  
  LASSERT(b != NULL);
  
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      nextb = LookArgB(b,1);
      if (LookTypeB(nextb) == IC)
        {
          GlueB(nextb,LookArgB(nextb,1));
          Kill_IC(nextb);
        }
      else
        Kill_IC(LookArgB(b,1));
      
      return;
      
    case IC:
      GlueB(b,LookArgB(b,1));
      Kill_IC(LookArgB(b,1));
      return;
      
    case AlternativeC:
      num = NumArgB(b);
      for (i = 1 ; i <= num ; i++)
        {
          branch = LookArgB(b,i);
          if (LookTypeB(branch) == IC)
            Kill_IC(LookArgB(branch,1));
          else
            Kill_IC(branch);
        }
      
      return;
      
    case ProcessDefC:
      if (In_list((DataListTyp)b, list,(boolean (*) ())NULL) == TRUE)
        return;
      else
        list = Add_list((DataListTyp)b,list);
      
      Kill_IC(LookArgB(b,1));
      return;
      
    case ProcessInstC:
      Kill_IC(GetP_def(LookNameB(b)));
      return;
      
    default:
      Error("Invalid cell type");
      break;
    }
}



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


/* Call_Kill_IC
 * Calls "Kill_IC" function.
 */
static void Call_Kill_IC(b)
     BehTyp b;
     
{
  list = Create_list();
  Kill_IC(b);
  Disp_list(list);
}



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



/* K_Allowed_Cells
 * Returns if behaviour "b" contains allowed cells for this Inverse
 * Expansion algorithms.
 */ 
static boolean K_Allowed_Cells(b)
     BehTyp b;
     
{
  int i,num;
  CellTypeTyp type;
  PAttrTyp at;
  
  
  LASSERT(b!=NULL);
  type=LookTypeB(b);
  if (type == ProcessDefC)
    {
      if (In_list((DataListTyp)LookNameB(b),list,(boolean (*) ())NULL) == TRUE)
        return TRUE;
      else
        {
          list = Add_list((DataListTyp)LookNameB(b),list);           
          at = LookA(b,ELA);
          if (at != NULL)
            return FALSE;
          b = LookArgB(b,1);
          type=LookTypeB(b);
        }
    }
  
  switch(type)
    {
    case StopC:
      return TRUE;
      
    case GateC:
      at = LookA(b,OLA);      
      if (at != NULL)
        return FALSE;
      at = LookA(b,PA);      
      if (at != NULL)
        return FALSE;
      
      return K_Allowed_Cells(LookArgB(b,1));
      
    case AlternativeC:
      num=NumArgB(b);
      for (i=1 ;i <= num ;++i)
        if (K_Allowed_Cells(LookArgB(b,i)) == FALSE)
          return FALSE;
      return TRUE;
      
    case IC:
      at = LookA(b,OLA);      
      if (at != NULL)
        return FALSE;
      at = LookA(b,PA);      
      if (at != NULL)
        return FALSE;
      
      return K_Allowed_Cells(LookArgB(b,1));
      
    case ProcessInstC:
      at = LookA(b,ELA);
      if (at != NULL)
        return FALSE;
      
      
      return K_Allowed_Cells(GetP_def(LookNameB(b)));
      
    default:
      return FALSE;
    }
}



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




/* Call_K_Allowed_Cells
 * Calls K_Allowed_Cells function (initialization purposes).
 */
static boolean Call_K_Allowed_Cells(b)
     BehTyp b;
     
{
  boolean bool;
  PAttrTyp at;
  
  
  list = Create_list();
  if (LookTypeB(b) == SpecificationC)
    {
      at = LookA(b,ELA);
      if (at != NULL)
        return FALSE;
      bool = K_Allowed_Cells(LookArgB(b,1));
    }
  else
    bool = K_Allowed_Cells(b);
  Disp_list(list);
  return bool;
}



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




/* CreatePDef
 * Returns the ProcessDefC of the decomposition process of process "desc"
 * with the gateset type "gtype".
 */ 
static BehTyp CreatePDef(desc,gtype)
     DescriptorTyp desc;
     GateTyp gtype;
     
{
  char *name,*nameaux;
  int length;
  BehTyp def;
  DescriptorTyp d;
  
  
  nameaux = GetP_name(desc);
  length = strlen(nameaux);
  name = (char *)emalloc(length + 3);
  
  switch(gtype)
    {
    case GS1:
      (void)sprintf(name,"%s_1",nameaux);
      break;
      
    case GS2:
      (void)sprintf(name,"%s_2",nameaux);
      break;
    }
  
  def = MakeB(0,ProcessDefC);
  d = Declare_proc(name,def,NOEXITF);
  PutNameB(def,d);
  Add_Tab(desc,d,gtype);
  return def;
}





/******************************************************************
 *
 *  Visible and Invisible Decomposition Functions
 *
 *******************************************************************/




/* PutTypeIC
 * Decides if IC actions belongs to B1 or B2.
 */
static void PutTypeIC(b,gs,gsa,gsb)
     BehTyp b;
     GateSetTyp gs,gsa,gsb;
     
{
  int i,num;
  BehTyp branch;
  
  
  LASSERT(b != NULL);
  LASSERT(LookTypeB(b) == AlternativeC);
  
  num = NumArgB(b);
  for (i = 1 ; i <= num ; i++)
    {
      branch = LookArgB(b,i);
      if (LookTypeB(branch) == IC)
        {
          if (EqualGS(gs,gsa) == TRUE)
            PutNameB(branch,-1);        /* this i action belongs to B1 */
          if (EqualGS(gs,gsb) == TRUE)
            PutNameB(branch,1);        /* this i action belongs to B2 */
        }
    }
}




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



/* KsInAlt
 * Returns TRUE if you need to synchronize in the alternative "b".
 * "gsa","gsb" and "gcs" are gatesets of A actions , B actions and
 * synchronization actions respectively.
 */      
static  boolean KsInAlt(b,gsa,gsb,gsc)
     BehTyp b;
     GateSetTyp gsa,gsb,gsc;
     
{
  int numa,numb,numc,numi;
  int num,i,j;
  DescriptorTyp name;
  BehTyp branch;
  
  
  LASSERT(b != NULL);
  LASSERT(LookTypeB(b) == AlternativeC);
  
  numa = 0;
  numb = 0;
  numc = 0;
  numi = 0;
  num = NumArgB(b);
  for(i =1 ; i <= num ; i++)
    {
      branch = LookArgB(b,i);
      if (LookTypeB(branch) == IC)
        numi++;
      else
        {
          name = LookNameB(branch);
          LASSERT(LookTypeB(branch) == GateC);
          if (GateInGS(name,gsa) == TRUE)
            numa++;
          if (GateInGS(name,gsb) == TRUE)
            numb++;
          if (GateInGS(name,gsc) == TRUE)
            numc++;
        }
    }
  
  if ( ( (numa == 0) && (numc == 0) && (numb >0) ) || ( (numb == 0) && (numc == 0) && (numa > 0) ) )
    return FALSE;
  
  if ( (numa == 0) && (numb == 0) )
    if (numi > 0)
      return TRUE;
    else
      {
        for (i = 1 ; i <= num ; i++)
          for (j = 1 ; j <= num ; j++)
            if ( (i != j) && (LookNameB(LookArgB(b,i)) == LookNameB(LookArgB(b,j))) )
              return TRUE;
        return FALSE;
      }
  
  return TRUE;
}




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



/* Initkc
 * Initializes counter of Kc`s.
 */ 
static void Initkc()
     
{
  num_kc = 1;
}




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





/* Initki
 * Initializes counter of Ki`s.
 */ 
static void Initki()
     
{
  num_ki = 1;
}




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


/* Createk
 * Returns a synchronization gate (K gate) of the type "ktype" to synchronize
 * in a alternative.
 */
static BehTyp Createk(ktype)
     KTypeTyp ktype;
     
{
  char *name,*nameaux;
  DescriptorTyp desc;
  BehTyp kgate;
  
  
  name = (char*)emalloc(LENGTH);
  switch(ktype)
    {
    case ka1:
      name = "ka1";
      break;
      
    case ka2:
      name = "ka2";
      break;
      
    case kb1:
      name = "kb1";
      break;
      
    case kb2:
      name = "kb2";
      break;
    }
  
  /* HORROR - Arreglar esta funcion */
  desc = FindG(name);
  while ( (desc != 0) && (desc <= tablelength) )
    {
      nameaux = (char*)emalloc(strlen(name) + 2);
      (void)sprintf(nameaux,"k%s",name);
      name = (char*)emalloc(strlen(nameaux));
      name = nameaux;
      desc = FindG(name);
    }
  
  if (desc == 0)
    desc = Declare_gate(name);
  
  kgate = MakeB(desc,GateC);
  return kgate;
}




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



/* Createkc
 * Returns a "Kc gate" to synchronize in a alternative when there is
 * no determinism in synchronization actions (C actions).
 */
static BehTyp Createkc()
     
{
  char *name,*nameaux;
  DescriptorTyp desc;
  BehTyp kgate;
  
  
  name = (char*)emalloc(LENGTH);
  (void)sprintf(name,"kc%d",num_kc);
  num_kc++;
  
  desc = FindG(name);
  while ( (desc != 0) && (desc <= tablelength) )
    {
      nameaux = (char*)emalloc(strlen(name) + 2);
      (void)sprintf(nameaux,"k%s",name);
      name = (char*)emalloc(strlen(nameaux));
      name = nameaux;
      desc = FindG(name);
    }
  
  if (desc == 0)
    desc = Declare_gate(name);
  
  kgate = MakeB(desc,GateC);
  
  
  return kgate;
}



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




/* Createki
 * Returns a "Ki gate" to synchronize in a alternative.
 */
static BehTyp Createki()
     
{
  char *name,*nameaux;
  DescriptorTyp desc;
  BehTyp kgate;
  
  
  name = (char*)emalloc(LENGTH);
  (void)sprintf(name,"ki%d",num_ki);
  num_ki++;
  
  desc = FindG(name);
  while ( (desc != 0) && (desc <= tablelength) )
    {
      nameaux = (char*)emalloc(strlen(name) + 2);
      (void)sprintf(nameaux,"k%s",name);
      name = (char*)emalloc(strlen(nameaux));
      name = nameaux;
      desc = FindG(name);
    }
  
  if (desc == 0)
    desc = Declare_gate(name);
  
  kgate = MakeB(desc,GateC);
  
  
  return kgate;
}



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



/* Createkexit
 * Returns a "K gate" to synchronize in the i exit of a zone.
 */
static BehTyp Createkexit(i)
     int i;
     
{
  char *name,*nameaux;
  DescriptorTyp desc;
  BehTyp kgate;
  
  
  name = (char*)emalloc(LENGTH);
  (void)sprintf(name,"k%d",i);
  
  desc = FindG(name);
  while ( (desc != 0) && (desc <= tablelength) )
    {
      nameaux = (char*)emalloc(strlen(name) + 2);
      (void)sprintf(nameaux,"k%s",name);
      name = (char*)emalloc(strlen(nameaux));
      name = nameaux;
      desc = FindG(name);
    }
  
  if (desc == 0)
    desc = Declare_gate(name);
  
  kgate = MakeB(desc,GateC);
  
  return kgate;
}




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




/* CreatekProc
 * Returns a "Kp gate" to synchronize in the entry of a process.
 */ 
static BehTyp CreatekProc()
     
{
  char *name,*nameaux;
  DescriptorTyp desc;
  BehTyp kgate;
  
  
  
  name = (char*)emalloc(LENGTH);
  (void)sprintf(name,"kp%d",num_kp);
  num_kp++;
  desc = FindG(name);
  while ( (desc != 0) && (desc <= tablelength) )
    {
      nameaux = (char*)emalloc(strlen(name) + 2);
      (void)sprintf(nameaux,"k%s",name);
      name = (char*)emalloc(strlen(nameaux));
      name = nameaux;
      desc = FindG(name);
    }
  
  if (desc == 0)
    desc = Declare_gate(name);
  kgate = MakeB(desc,GateC);
  return kgate;
}  




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



/* CreateAltP
 * Returns the ProcessDefC of a new process named alt_i used when K
 * synchronization in a alternative is necessary.
 */ 
static BehTyp CreateAltP()
     
{
  char        * name;
  BehTyp        def;
  DescriptorTyp desc;
  
  
  name = "alt";
  def  = MakeB(0,ProcessDefC);
  desc = Declare_proc(name,def,NOEXITF);
  PutNameB(def,desc);
  
  return def;
}




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



/* PutKsInAlt
 * Introduces the K actions in "b" alternative and returns its ProcessDefC.
 */
static BehTyp PutKsInAlt(b,gsa,gsb,gsc)
     BehTyp b;
     GateSetTyp gsa,gsb,gsc;
     
{
  BehTyp beh_a,beh_b,behalt,baux,beh_inst,alt,bc,gate;
  BehTyp beh_k1,beh_k2,beh_k3,beh_k4,beh_kc1,beh_kc2,beh_ki;
  int i,j,num;
  boolean equal,end;
  
  
#ifdef lint
  gsc = NewGS();
  PrintGS(gsc,printTarget); 
#endif
  Initkc();
  Initki();
  beh_a = NULL;
  beh_b = NULL;
  behalt = CreateAltP();
  
  bc = CopyB(b);
  end = FALSE;
  for(i = 1 ; i <= NumArgB(bc) ; i++)
    {
      if (LookTypeB(bc) == AlternativeC)
        gate = LookArgB(bc,i);
      else
        gate = bc;
      
      if (LookTypeB(gate) != IC)
        {
          LASSERT(LookTypeB(gate) == GateC);
          if (GateInGS(LookNameB(gate),gsa) == TRUE)
            {
              if (LookTypeB(bc) == AlternativeC)
                {
                  baux = GetArgB(bc,i);
                  FreeArgB(bc,i);
                  i--;
                }
              else
                {
                  baux = bc;
                  end = TRUE;
                }
              
              beh_a = AppendUB(beh_a,baux);
            }
          
          if (GateInGS(LookNameB(gate),gsb) == TRUE)
            {
              if (LookTypeB(bc) == AlternativeC)
                {
                  baux = GetArgB(bc,i);
                  FreeArgB(bc,i);
                  i--;
                }
              else
                {
                  baux = bc;
                  end = TRUE;
                }
              beh_b = AppendUB(beh_b,baux);
            }
        }
    }  /* for(...) */
  
  alt = MakeB(0,AlternativeC);
  AddArgB(behalt,alt);
  
  if (beh_a != NULL)
    {
      beh_k1 = Createk(ka1);
      beh_k2 = Createk(ka2);
      beh_inst = MakeProcInst(LookNameB(behalt));
      AddArgB(beh_k2,beh_inst);
      beh_k2 = AppendUB(beh_k2,beh_a);
      AddArgB(beh_k1,beh_k2);
      AddArgB(alt,beh_k1);
    }
  
  if (beh_b != NULL)
    {
      beh_k3 = Createk(kb1);
      beh_k4 = Createk(kb2);
      beh_inst = MakeProcInst(LookNameB(behalt));
      AddArgB(beh_k4,beh_inst);
      beh_k4 = AppendUB(beh_k4,beh_b);
      AddArgB(beh_k3,beh_k4);
      AddArgB(alt,beh_k3);
    }
  
  
  if (end == FALSE)
    {
      if (LookTypeB(bc) == GateC)
        {
          LASSERT(GateInGS(LookNameB(bc),gsc) == TRUE);
          AddArgB(alt,bc);
        }
      else if (LookTypeB(bc) == IC)
        {
          baux = GetArgB(bc,1);
          FreeB(bc);
          beh_ki = Createki();
          PutArgB(beh_ki,baux,1);
          AddArgB(alt,beh_ki);
        }
      else if (LookTypeB(bc) == AlternativeC)
        {
          num = NumArgB(bc);
          for(i = 1 ; i <= num ; i++)
            {
              gate = LookArgB(bc,i);
              if (LookTypeB(gate) == IC)
                {
                  baux = GetArgB(gate,1);
                  beh_ki = Createki();
                  PutArgB(beh_ki,baux,1);
                  AddArgB(alt,beh_ki);
                }
              else
                {
                  LASSERT(GateInGS(LookNameB(gate),gsc) == TRUE);
                  equal = FALSE;
                  for(j = 1 ; j <= num ; j++)
                    if (LookTypeB(LookArgB(bc,j)) != IC)
                      if ((i != j) && (LookNameB(gate) == LookNameB(LookArgB(bc,j))))
                        equal = TRUE;
                  
                  if (equal == FALSE)
                    AddArgB(alt,gate);
                  else
                    {
                      beh_kc1 = Createkc();
                      beh_kc2 = Createkc();
                      beh_inst = MakeProcInst(LookNameB(behalt));
                      AddArgB(beh_kc2,beh_inst);
                      beh_kc2 = AppendUB(beh_kc2,gate);
                      AddArgB(beh_kc1,beh_kc2);
                      AddArgB(alt,beh_kc1);
                    }
                }
            }  /* for (...) */
          FreeB(bc);
        }  /* else if ... */
    }   /* if (end == FALSE) */
  
  beh_inst = MakeProcInst(LookNameB(behalt));
  
  GlueB(b,beh_inst);
  
  return behalt;
}




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



/* FindExits
 * Finds the exits of the zone "b" with gateset "gs" adding these to "l".
 * "bprev" is the previous cell of "b" and "gsync" is the synchronization
 * gateset. It returns the exits list "l".
 */
static ListTyp FindExits(b,bprev,gs,gsync,gsa,gsb,l)
     BehTyp b,bprev;
     GateSetTyp gs,gsync,gsa,gsb;
     ListTyp l;
     
{
  CellTypeTyp type;
  int num,i,j;
  DescriptorTyp name;
  BehTyp branch;
  boolean iaction;
  
  
  LASSERT(b != NULL);
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return l;
      
    case GateC:
      if (GateInGS(LookNameB(b),gs) == TRUE)
        {
          l = FindExits(LookArgB(b,1),b,gs,gsync,gsa,gsb,l);
          return l;
        }
      else
        {
          l = Add_list((DataListTyp)bprev,l);
          return l;
        }
      
    case ProcessInstC:
      l = Add_list((DataListTyp)bprev,l);
      return l;
      
    case AlternativeC:
      iaction = FALSE;
      num = NumArgB(b);
      if (EqualGS(gs,gsync) == TRUE)
        for(i = 1 ; i <= num ; i++)
          {
            branch = LookArgB(b,i);
            if (LookTypeB(branch) == IC)
              {
                l = Add_list((DataListTyp)bprev,l);
                return l;
              }
            else
              {
                if (GateInGS(LookNameB(branch),gs) == FALSE)
                  {
                    l = Add_list((DataListTyp)bprev,l);
                    return l;
                  }
                else
                  {
                    name = LookNameB(branch);
                    for(j = 1 ; j <= num ; j++)
                      if (LookTypeB(LookArgB(b,j)) != IC)
                        if ((i != j) && (LookNameB(LookArgB(b,j)) == name))
                          {
                            l = Add_list((DataListTyp)bprev,l);
                            return l;
                          }
                  }
              }
          }  /* for (...) */
      else
        for(i = 1 ; i <= num ; i++)
          {
            branch = LookArgB(b,i);
            if (LookTypeB(branch) != IC)
              {
                if (GateInGS(LookNameB(branch),gs) == FALSE)
                  {
                    l = Add_list((DataListTyp)bprev,l);
                    return l;
                  }
              }
            else
              iaction = TRUE;
          }
      
      if (iaction == TRUE)
        PutTypeIC(b,gs,gsa,gsb);
      
      
      for(i = 1 ; i <= num ; i++)
        l = FindExits(LookArgB(LookArgB(b,i),1),LookArgB(b,i),gs,gsync,gsa,gsb,l);
      
      return l;
      
    default:
      Error("Invalid cell type");
      break;
    }
  return (ListTyp)NULL;
}




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



/* PutkInExit
 * Puts the  i "K exit" in the exit "b" and returns it.
 */
static BehTyp PutkInExit(b,i)
     BehTyp b;
     int i;
     
{
  BehTyp behk,baux;
  
  
  behk = Createkexit(i);
  baux = GetArgB(b,1);
  PutArgB(b,behk,1);
  PutArgB(behk,baux,1);
  
  return behk;
}




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



/* KInExit
 * Returns TRUE if you need to put a "K exit" in the exit "b" being
 * "gs" the zone gateset and "gsync" the synchronization gateset (returns
 * FALSE if not).
 */ 
static boolean KInExit(b,gs,gsync)
     BehTyp b;
     GateSetTyp gs,gsync;
     
{
  int i,num;
  CellTypeTyp type;
  BehTyp nextb;
  DescriptorTyp name;
  boolean onlyki;
  
  
  LASSERT(b != NULL);
  
  if ( (LookTypeB(b) == GateC) && (GateInGS(LookNameB(b),gsync) == TRUE) )
    return FALSE;
  
  nextb = LookArgB(b,1);
  type = LookTypeB(nextb);
  switch(type)
    {
    case ProcessInstC:
      return FALSE;
      
    case GateC:      
      if (GateInGS(LookNameB(nextb),gsync) == TRUE)
        return FALSE;
      else 
        return TRUE;
      
    case AlternativeC:
      num = NumArgB(nextb);
      for(i = 1 ; i <= num ; i ++)
        if (LookTypeB(LookArgB(nextb,i)) != IC)
          {
            name = LookNameB(LookArgB(nextb,i));
            if ((GateInGS(name,gs) == TRUE) || (GateInGS(name,gsync) == TRUE))
              return FALSE;
          }
      
      onlyki = TRUE;
      for(i = 1 ; i <= num ; i ++)
        if (LookTypeB(LookArgB(nextb,i)) != IC)
          onlyki = FALSE;
      
      if (onlyki == TRUE)
        return FALSE;
      
      return TRUE;
      
    default:
      Error("Invalid cell type");
      break;
    }
  return (boolean)NULL;
}




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



/* PutkProc
 * Puts a "Kp gate" in the entry of the process "b" and returns it.
 */
static BehTyp PutkProc(b)
     BehTyp b;
     
{
  BehTyp beh_kp,baux;
  
  
  LASSERT(LookTypeB(b) == ProcessDefC);
  beh_kp = CreatekProc();
  baux = GetArgB(b,1);
  PutArgB(b,beh_kp,1);
  PutArgB(beh_kp,baux,1);
  
  return beh_kp;
}




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




/* KInProc
 * Returns TRUE if you have to put a "Kp gate" in the process "b"
 * (returns FALSE if not). "gsa " , "gsb" and "gsc" are A gateset , B
 * gateset and synchronization gateset respectively.
 */  
static boolean KInProc(b,gsa,gsb,gsc)
     BehTyp b;
     GateSetTyp gsa,gsb,gsc;
     
{
  CellTypeTyp type;
  DescriptorTyp name;
  int numa,numb,numc;
  int i,num;
  
  
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return FALSE;
      
    case GateC:
      name = LookNameB(b);
      if ((GateInGS(name,gsa) == TRUE) || (GateInGS(name,gsb) == TRUE))
        return TRUE;
      else
        return FALSE;
      
    case AlternativeC:
      numa = 0;
      numb = 0;
      numc = 0;
      num = NumArgB(b);
      for(i = 1 ; i <= num ; i++)
        if (LookTypeB(LookArgB(b,i)) != IC)
          {
            name = LookNameB(LookArgB(b,i));
            if (GateInGS(name,gsa) == TRUE)
              numa++;
            if (GateInGS(name,gsb) == TRUE)
              numb++;
            if (GateInGS(name,gsc) == TRUE)
              numc++;
          }
      
      
      if ( ( (numc == 0) && (numa == 0) && (numb > 0) ) || ( (numc == 0) && (numb == 0) && (numa > 0) ) )
        return TRUE;
      else 
        return FALSE;
      
    case ProcessInstC:
      return FALSE;
      
    default:
      Error("Invalid cell type");
      break;
    }
  return FALSE;
}




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



/* Zone
 * Introduces synchronizations actions (K actions) in the behaviour "b"
 * if you need. "gsa" , "gsb" and "gsc" are A gateset , B gateset
 * and synchronization gateset respectively.
 */
static void Zone(b,gsa,gsb,gsc)
     BehTyp b;
     GateSetTyp gsa,gsb,gsc;
     
{
  BehTyp behexit,behk,behalt,branch,bdef;
  CellTypeTyp type;
  int number,i,num,length;
  DescriptorTyp name;
  GateSetTyp gs;
  ListTyp l,lexit;
  
  
  
  LASSERT(b != NULL);
  type = LookTypeB(b);
  switch(type)
    {
    case GateC:
      name = LookNameB(b);
      
      if (GateInGS(name,gsa) == TRUE)
        gs = gsa;
      if (GateInGS(name,gsb) == TRUE)
        gs = gsb;
      if (GateInGS(name,gsc) == TRUE)
        gs = gsc;
      
      if ( (gs == gsa) || (gs == gsb) )
        {
          lexit = Create_list();
          lexit = FindExits(LookArgB(b,1),b,gs,gsc,gsa,gsb,lexit);
          length = Length_list(lexit);
          if (length > 0)
            {
              number = 1;
              l = Create_list();
              l = lexit;
              for(i = 1 ; i <= length ; i++,l = Next_list(l))
                {
                  behexit = (BehTyp)LookInfo_list(l);
                  if (KInExit(behexit,gs,gsc) == TRUE)
                    {
                      behk = PutkInExit(behexit,number);
                      number++;
                      Zone(LookArgB(behk,1),gsa,gsb,gsc);
                    }
                  else
                    Zone(LookArgB(behexit,1),gsa,gsb,gsc);
                }
            }  /* if (length > 0) */
          Disp_list(lexit);
        }  /* if ((gs == gsa) || ... */
      else if (gs == gsc)
        {
          lexit = Create_list();
          lexit = FindExits(LookArgB(b,1),b,gs,gsc,gsa,gsb,lexit);
          length = Length_list(lexit);
          if (length > 0)
            {
              number = 1;
              l = Create_list();
              l = lexit;
              for(i = 1 ; i <= length ; i ++ , l = Next_list(l))
                {
                  behexit = (BehTyp)LookInfo_list(l);
                  Zone(LookArgB(behexit,1),gsa,gsb,gsc);
                }
            }
          Disp_list(lexit);
        }  /* else if ... */
      
      return;
      
    case AlternativeC:
      if (KsInAlt(b,gsa,gsb,gsc) == TRUE)
        {
          behalt = PutKsInAlt(b,gsa,gsb,gsc);
          behalt = LookArgB(behalt,1);
          LASSERT(LookTypeB(behalt) == AlternativeC);
          num = NumArgB(behalt);
          for(i = 1 ; i <= num ; i++)
            {
              branch = LookArgB(behalt,i);
              name = LookNameB(branch);
              if (name <= tablelength)
                Zone(branch,gsa,gsb,gsc);
              else
                Zone(LookArgB(branch,1),gsa,gsb,gsc);
            }             
        }
      else
        {
          if (LookTypeB(LookArgB(b,1)) != IC)
            name = LookNameB(LookArgB(b,1));
          i = 2;
          while (name > tablelength)
            {
              if (LookTypeB(LookArgB(b,i)) != IC)
                name = LookNameB(LookArgB(b,i));
              i++;
            }
	  
          if (GateInGS(name,gsa) == TRUE)
            gs = gsa;
          if (GateInGS(name,gsb) == TRUE)
            gs = gsb;
          if (GateInGS(name,gsc) == TRUE)
            gs = gsc;
	  
          lexit = Create_list();
          num = NumArgB(b);
          for(i = 1 ; i <= num ; i++)
            {
              branch = LookArgB(b,i);
              if((LookNameB(branch)<=tablelength) || (LookTypeB(branch) == IC))
                lexit = FindExits(LookArgB(branch,1),branch,gs,gsc,gsa,gsb,lexit);
            }
          PutTypeIC(b,gs,gsa,gsb);
	  
          length = Length_list(lexit);
          if (length > 0)
            {
              number = 1;
              l = Create_list();
              l = lexit;
              for(i = 1 ; i <= length ; i++,l = Next_list(l))
                {
                  behexit = (BehTyp)LookInfo_list(l);
                  if (KInExit(behexit,gs,gsc) == TRUE)
                    {
                      behk = PutkInExit(behexit,number);
                      number++;
                      Zone(LookArgB(behk,1),gsa,gsb,gsc);
                    }
                  else
                    Zone(LookArgB(behexit,1),gsa,gsb,gsc);
                }
            }  /* if (length > 0) */
          Disp_list(lexit);
        }  /* else */
      
      return;
      
    case ProcessInstC:
      bdef = GetP_def(LookNameB(b));
      if (In_list((DataListTyp)bdef,list ,(boolean (*) ())NULL) == TRUE)
        return;
      else
        list = Add_list((DataListTyp)bdef,list);
      
      if (KInProc(LookArgB(bdef,1),gsa,gsb,gsc) == TRUE)
        {
          behk = PutkProc(bdef);
          Zone(LookArgB(behk,1),gsa,gsb,gsc);
        }
      else
        Zone(LookArgB(bdef,1),gsa,gsb,gsc);
      
      return;
      
    case ProcessDefC:
      if (In_list((DataListTyp)b,list ,(boolean (*) ())NULL) == TRUE)
        return;
      else
        list = Add_list((DataListTyp)b,list);
      
      if (KInProc(LookArgB(b,1),gsa,gsb,gsc) == TRUE)
        {
          behk = PutkProc(b);
          Zone(LookArgB(behk,1),gsa,gsb,gsc);
        }
      else
        Zone(LookArgB(b,1),gsa,gsb,gsc);
      
      return;
      
    case StopC:
      return;
      
    default:
      Error("Invalid cell type");
      break;
    }
}




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



/* GluekBeh
 * Makes the parallel composition of "b1" (with gates "gs1") and "b2" (with
 * gates "gs2") and glues it to "b", hiding K`s gates (gates to synchronize
 * that are introduced).
 */
static void GluekBeh(b,b1,b2,gs1,gs2)
     BehTyp b,b1,b2;
     GateSetTyp gs1,gs2;
     
{
  GateSetTyp gsync,gshide;
  DescriptorTyp last,i;
  BehTyp bpar,pinst1,pinst2,bhide;
  PAttrTyp at1,at2,athide;
  
  
  gshide = NewGS();
  gsync = IntersGS(gs1,gs2);
  last = LastTableG();
  for (i = tablelength + 1 ; i <= last ; i++)
    {
      gsync = AddGS(gsync,i);
      gshide = AddGS(gshide,i);
    }
  
  bpar = MakeB(0,ParallelC);
  if (IsEmptyGS(gsync))
    {
      PutNameB(bpar,INTER_SYNC);
      FreeGS(gsync);
    }
  else if (EqualGS(gs1,gs2))
    {
      PutNameB(bpar,FULL_SYNC);
      FreeGS(gsync);
    }
  else
    {
      PutNameB(bpar,PART_SYNC);
      PutA(bpar,MakeA((AttrValueTyp)gsync,GSA));
    }
  
  
  pinst1 = MakeB(0,ProcessInstC);
  PutNameB(pinst1,LookNameB(b1));
  at1 = LookA(b1,GLA);
  PutA(pinst1,at1);
  AddArgB(bpar,pinst1);
  
  pinst2 = MakeB(0,ProcessInstC);
  PutNameB(pinst2,LookNameB(b2));
  at2 = LookA(b2,GLA);
  PutA(pinst2,at2);
  AddArgB(bpar,pinst2);
  
  if (LookTypeB(b) == ProcessDefC)
    b = LookArgB(b,1); 
  
  bhide = MakeB(0,HidingC);
  athide = MakeA((AttrValueTyp)gshide,GSA);
  PutA(bhide,athide);
  PutArgB(bhide,bpar,1);
  
  GlueB(b,bhide);
}




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



/* Decomp
 * Decomposes the behaviour "b" in another behaviour that contains "K gates"
 * and "gs" gates only. The new behaviour is built using "baux".
 */
static void Decomp(b,baux,gs,gtype)
     BehTyp b,baux;
     GateSetTyp gs;
     GateTyp gtype;
     
{
  CellTypeTyp type;
  int i,num;
  DescriptorTyp name,d;
  BehTyp beh,altbeh,beh1,pinst,pdef;
  
  
  
  LASSERT(b != NULL);
  
  if (LookTypeB(b) == ProcessDefC)
    b = LookArgB(b,1);
  
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      PutStopCell(baux);
      return;
      
    case GateC:
      name = LookNameB(b);
      if ( (GateInGS(name,gs) == TRUE) || (name > tablelength) )
        {
          beh = MakeB(name,GateC);
          PutArgB(baux,beh,1);
          Decomp(LookArgB(b,1),beh,gs,gtype);
          return;
        }
      else
        {
          Decomp(LookArgB(b,1),baux,gs,gtype);
          return;
        }
      
    case AlternativeC:
      num = NumArgB(b);
      altbeh = NULL;
      for (i = 1 ; i <= num ; i++)
        {
          beh = MakeB(0,StopC);
          Decomp(LookArgB(b,i),beh,gs,gtype);
          if (LookTypeB(LookArgB(beh,1)) != StopC)
            {
              beh1 = GetArgB(beh,1);
              FreeB(beh);
              altbeh = AppendUB(altbeh,beh1);
            }
          else
            FreeB(beh);
        }
      
      if (altbeh == NULL)
        PutStopCell(baux);
      else
        PutArgB(baux,altbeh,1);
      
      return;
      
    case ProcessInstC:
      d = LookTab(LookNameB(b),gtype);
      if (d != 0)
        {
          pinst = MakeProcInst(d);
          PutArgB(baux,pinst,1);
          return;
        }
      else
        {
          pdef = CreatePDef(LookNameB(b),gtype);
          Decomp(GetP_def(LookNameB(b)),pdef,gs,gtype);
          pinst = MakeProcInst(LookNameB(pdef));
          PutArgB(baux,pinst,1);
          return;
        }
      
    case IC:
      name = LookNameB(b);
      if (((gtype == GS1) && (name == -1)) || ((gtype == GS2) && (name == 1)))
        {
          beh = MakeB(0,IC);
          PutArgB(baux,beh,1);
          Decomp(LookArgB(b,1),beh,gs,gtype);
        }
      else
        Decomp(LookArgB(b,1),baux,gs,gtype);
      
      return;
      
      
    default:
      Error("Invalid cell type.");
      break;
    }
}



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



/* MakeDecomp
 * Makes the decomposition of "b" with "gs" gateset and "gtype" gateset
 * type over a ProcessDefC created with the parameters "desc" ,"gs" and
 * "gtype" (see CreatePDef function).
 */
static BehTyp MakeDecomp(desc,b,gs,gtype)
     DescriptorTyp desc;
     BehTyp b;
     GateSetTyp gs;
     GateTyp gtype;
     
{
  BehTyp beh;
  
  
  beh = CreatePDef(desc,gtype);
  Decomp(b,beh,gs,gtype);
  
  return beh;
}




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



/* Kdecomp
 * Decomposes behaviour "b" into two behaviours ,one with gates of "gs1"
 * and the other with gates of "gs2" and composes these in parallel
 * with visible and invisible communication.
 */ 
void Kdecomp(b,gs1,gs2)
     BehTyp b;
     GateSetTyp gs1,gs2;
     
{
  GateSetTyp gsa,gsb,gsc;
  DescriptorTyp desc,firstp,lastp,proc_1,proc_n;
  BehTyp b1,b2;
  
  
  LASSERT(b != NULL);
  LASSERT(gs1 != NULL);
  LASSERT(gs2 != NULL);
  
  
  if (Call_K_Allowed_Cells(b) == FALSE)
    {
      printError("      The current behaviour contains not supported operators.\n");
      return;
    }
  
  
  gsc = IntersGS(gs1,gs2);
  gsa = DiffGS(gs1,gsc);
  gsb = DiffGS(gs2,gsc);
  
  tablelength = LastTableG();
  num_kp = 1;
  
  firstp = LastTableP();
  
  Expand(b,-1,FALSE,FALSE,FALSE);
  
  
  if (LookTypeB(b) == SpecificationC)
    b = LookArgB(b,1);
  
  if (LookTypeB(b) == ProcessInstC)
    b = GetP_def(LookNameB(b));
  
  b = RmAltStopInBeh(b);
  Call_Kill_IC(b);
  
  
  list = Create_list();
  Zone(b,gsa,gsb,gsc); 
  Disp_list(list);
  
  FreeGS(gsa);
  FreeGS(gsb);
  FreeGS(gsc);
  
  
  
  lastp = LastTableP();
  
  InitTab();
  
  if (LookTypeB(b) != ProcessDefC)
    {
      desc = NewProc();
      proc_1 = LastTableP();
      b1 = MakeDecomp(desc,b,gs1,GS1);
      b2 = MakeDecomp(desc,b,gs2,GS2);
    }
  else
    {
      proc_1 = LastTableP();      
      b1 = MakeDecomp(LookNameB(b),b,gs1,GS1);
      b2 = MakeDecomp(LookNameB(b),b,gs2,GS2);      
    }
  proc_n = LastTableP();
  
  FreeTab();
  FreeProcTable(firstp + 1,lastp);
  
  KPutGatestoProcs(proc_1 + 1,proc_n);
  
  GluekBeh(b,b1,b2,gs1,gs2);
  
}

#endif /* INVEXP */
