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

/***********************************
  
  Miguel Angel Palomares Ortega
  
  11-11-1992
  
  This module contains  functions that implement Inverse Expansion 
  algorithms. The restrictions on the behaviour to be decomposed are
  that no internal actions may be present and it must be determinis-
  tic. Recursive behaviours can be decomposed.
  
  ************************************/


#ifdef INVEXP

#include "ievcdeex.h"
#include "iefunc.h"
#include "ie_vc.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 "balotosf.h"
#include "baprint.h"
#include "lihash.h"
#include "limisc.h"
#include "libst.h"




/******************************************************************
 *
 *  function declarations and global variables declarations
 *
 *******************************************************************/


/* binary search tree used for storing states in the function
   "GetGatesOfProc" */

static BstTyp bst;

/* list used for storing states in recursives functions */

static ListTyp list;

/* table used in the decomposition process of the original behaviour */

static DTableTyp table;



static void Rec_Rest();

static BehTyp Rec_Sync();

static void ParalComp();




/*****************************************************************
 *
 *
 *       TABLE MANAGEMENT FUNCTIONS
 *
 *
 *****************************************************************/




/* Init_Desc_Table
 * Initializes descriptors table.
 */
static void Init_Desc_Table()
     
{
  DescriptorTyp length,i;
  
  length = LastTableP();
  table = (DTableEntryTyp*)emalloc((length + 1)*sizeof(DTableEntryTyp));
  
  for (i = 0 ; i<= length ; i++)
    {
      table[i].rest1 = 0;
      table[i].rest2 = 0;
      table[i].sync1 = 0;
      table[i].sync2 = 0;
    }
}




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




/* Free_Desc_Table
 * Frees memory used for "table".
 */
static void Free_Desc_Table()
     
{
  free((char *)table);
}




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




/* Add_Desc_Table
 * Adds "newdesc" descriptor in "entry" entry with the decomposition
 * mode indicated by "decmode" and "gsmode".
 */
static void Add_Desc_Table(decmode,gsmode,entry,newdesc)
     DescriptorTyp entry,newdesc;
     Decomp_Mode decmode;
     GateSet_Mode gsmode;
     
{
  LASSERT ( entry <= LastTableP() );
  switch(decmode + gsmode)
    {
    case 1:
      table[entry-1].rest1 = newdesc;
      break;
      
    case 2:
      table[entry-1].rest2 = newdesc;
      break;
      
    case 3:
      table[entry-1].sync1 = newdesc;
      break;
      
    case 4:
      table[entry-1].sync2 = newdesc;
      break;
      
    default:
      Error("Invalid Mode");
      break;
      
    }
}




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




/* LookDescTable
 * Returns the descriptor of the "entry" entry with the decomposition
 * mode indicated by "decmode" and "gsmode".
 */
static DescriptorTyp LookDescTable(entry,decmode,gsmode)
     DescriptorTyp entry;
     GateSet_Mode gsmode;
     Decomp_Mode decmode;
     
{
  switch (decmode + gsmode)
    {
    case 1:
      return (table[entry-1].rest1);
      
    case 2:
      return (table[entry-1].rest2);
      
    case 3:
      return (table[entry-1].sync1);
      
    case 4:
      return (table[entry-1].sync2);
      
    default:
      Error("Invalid Mode");
      break;
    }
  return (DescriptorTyp)NULL;
}





/*****************************************************************
 *
 *              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;
}





/*****************************************************************
 *
 *   Complementary Functions 
 *
 ******************************************************************/





/* GetGatesOfProc
 * Gets all the gates of "b" in "gs".
 */
static void GetGatesOfProc(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);
      
      GetGatesOfProc(LookArgB(b,1),gs);
      return;
      
    case AlternativeC:
      num = NumArgB(b);
      for (i = 1; i <= num ; i++)
        GetGatesOfProc(LookArgB(b,i),gs);
      
      return;
      
    case ProcessInstC:
      GetGatesOfProc(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);
      
      GetGatesOfProc(LookArgB(b,1),gs);
      return; 
      
    default:
      Error("invalid cell type.");
      break;
    }
  
}





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




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




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




/* PutGatestoInsts
 * Puts the gatelist attribute to all process instantiations of "b".
 */
static void PutGatestoInsts(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:
      PutGatestoInsts(LookArgB(b,1));
      return;
      
    case AlternativeC:
      num = NumArgB(b);
      for (i = 1 ; i <= num ; i++)
        PutGatestoInsts(LookArgB(b,i));
      
      return;
      
    case ProcessInstC:
      bdef = GetP_def(LookNameB(b));
      at = LookA(bdef,GLA);
      PutA(b,at);
      
      return;
      
    case ProcessDefC:
      PutGatestoInsts(LookArgB(b,1));
      return;
      
    default:
      Error("Invalid cell type.");
      break;
    }
}




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




/* PutGatestoProcs
 * 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 PutGatestoProcs(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_GetGates(bdef);
      gl = GateSet_to_GateList(gs);
      FreeGS(gs);
      at = MakeA((AttrValueTyp)gl,GLA);
      PutA(bdef,at);
    }
  
  for (i = first ; i <= last ; i++)
    PutGatestoInsts(GetP_def(i));
}




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



/* Rec_Allowed_Cells
 * Returns if behaviour "b" contains allowed cells for this Inverse
 * Expansion algorithms.
 */ 
static boolean Rec_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 Rec_Allowed_Cells(LookArgB(b,1));
      
    case AlternativeC:
      num=NumArgB(b);
      for (i=1 ;i <= num ;++i)
	
        if (Rec_Allowed_Cells(LookArgB(b,i)) == FALSE)
          return FALSE;
      
      return TRUE;
      
    case ProcessInstC:
      at = LookA(b,ELA);
      if (at != NULL)
        return FALSE;
      
      return Rec_Allowed_Cells(GetP_def(LookNameB(b)));
      
    default:
      return FALSE;
    }
}



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




/* Call_Allowed_Cells
 * Calls Allowed_Cells function (initialization purposes).
 */
boolean Call_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 = Rec_Allowed_Cells(LookArgB(b,1));
    }
  else
    bool = Rec_Allowed_Cells(b);
  
  Disp_list(list);
  return bool;
}






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




/* IsDecomp
 * Returns the ParallelCell that communicate "b1" and "b2" if behaviour
 * "b" can be decomposed  in "b1" and  "b2". Returns NULL if
 * it is not posible.
 */
static BehTyp IsDecomp(b,b1,b2)
     BehTyp b,b1,b2;
     
{
  BehTyp comp,comp_store;
  GateSetTyp inters_gs,gsa,gsb;
  int last;
  
  
  gsa = GateList_to_GateSet((GateListTyp)LookAInfo(LookA(b1,GLA)));
  gsb = GateList_to_GateSet((GateListTyp)LookAInfo(LookA(b2,GLA)));
  inters_gs = IntersGS(gsa,gsb);  
  comp = MakeB(0,ParallelC);
  if (IsEmptyGS(inters_gs)) {
    PutNameB(comp,INTER_SYNC);
    FreeGS(inters_gs);
    FreeGS(gsa);
    FreeGS(gsb);
  }
  else if (EqualGS(gsa,gsb)) {
    PutNameB(comp,FULL_SYNC);
    FreeGS(inters_gs);
    FreeGS(gsa);
    FreeGS(gsb);
  }
  else {
    PutNameB(comp,PART_SYNC);
    PutA(comp,MakeA((AttrValueTyp)inters_gs,GSA));
    FreeGS(gsa);
    FreeGS(gsb);
  }
  
  
  comp_store=CopyB(comp);
  (void)ShareB(comp); 
  
  ParalComp(comp,b1,b2);
  
  last = LastTableP();
  Expand(comp,-1,FALSE,FALSE,FALSE);
  
  
  if (Call_Cmp_Rec_Beh(b,comp) == TRUE) {
    comp = UnshareB(comp);
    FreeB(comp);
    FreeProcTable(last + 1,LastTableP());
    return comp_store;
  }
  else {
    comp = UnshareB(comp);
    FreeB(comp);
    FreeB(comp_store);
    return NULL;
  }
}




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




/* ParalComp
 * Adds instantiations of the processes "def1" and "def2" to the
 * parallel cell "comp".
 */
static void ParalComp(comp,def1,def2)
     BehTyp comp,def1,def2;
     
{
  PAttrTyp at1,at2;
  BehTyp def;
  
  
  def = MakeB(0,ProcessInstC);
  PutNameB(def,LookNameB(def1));
  at1 = LookA(def1,GLA);
  PutA(def,at1);
  AddArgB(comp,def);
  
  def = MakeB(0,ProcessInstC);
  PutNameB(def,LookNameB(def2));
  at2 = LookA(def2,GLA);
  PutA(def,at2);
  AddArgB(comp,def);
  
}




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




/* KillNextLoopProc
 * Removes the "ProcessInstC" cell with descriptor the following element
 * of the list "l" from arguments of the process "bdef".
 */
static void KillNextLoopProc(bdef,l)
     BehTyp bdef;
     ListTyp l;
     
{
  BehTyp bnext,branch;
  ListTyp laux;
  CellTypeTyp type;
  DescriptorTyp nextproc;
  boolean found;
  int i;
  
  
  LASSERT(bdef != NULL);
  LASSERT(l != NULL);
  
  laux = l;
  laux = Next_list(laux);
  nextproc = (DescriptorTyp)LookInfo_list(laux);
  bnext = LookArgB(bdef,1);
  type = LookTypeB(bnext);
  if (type == ProcessInstC)
    {
      LASSERT(LookNameB(bnext) == nextproc);
      FreeArgB(bdef,1);
    }
  else if (type == AlternativeC)
    {
      found = FALSE;
      i = 1;
      while ((found == FALSE) && (i <= NumArgB(bnext)))
        {
          branch = LookArgB(bnext,i);
          if ((LookTypeB(branch) == ProcessInstC) && (LookNameB(branch) == nextproc))
            {
              FreeArgB(bnext,i);
              found = TRUE;
            }
          i++;
        }
      LASSERT(found == TRUE);
    }
  else
    Error("Invalid cell type");
}




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




/* BreakLoop
 * Breaks the loop of processes at process with descriptor "proc" ,
 * adds arguments of the others processes of the loop to this process
 * and puts the behaviours of the other processes of the loop the
 * behaviour of this process.
 */ 
static void BreakLoop(proc,l)
     DescriptorTyp proc;
     ListTyp l;
     
{
  int length,i;
  ListTyp laux,l2aux;
  BehTyp bdef,bdef1,bnext,branch,newbeh,pinst;
  CellTypeTyp type;
  DescriptorTyp nextproc;
  PAttrTyp at;
  
  
  LASSERT(proc > 0);
  LASSERT(l != NULL);
  
  
  laux = LookFor_list((DataListTyp)proc,l,(boolean (*) ())NULL);
  LASSERT(laux != NULL);
  length = Length_list(laux);
  LASSERT(length > 0);
  if (length == 1)
    {
      bdef = GetP_def(proc);
      bnext = LookArgB(bdef,1);
      type = LookTypeB(bnext);
      if (type == ProcessInstC)
        {
          LASSERT(LookNameB(bnext) == proc);
          TrfStop(bnext);
          return;
        }
      else if (type == AlternativeC)
        {
          for (i = 1 ; i <= NumArgB(bnext) ; i++)
            {
              branch = LookArgB(bnext,i);
              if ((LookTypeB(branch) == ProcessInstC) && (LookNameB(branch) == proc))
                {
                  FreeArgB(bnext,i);
                  return;
                }
            }
          Error("Found no branch to kill");
        }
      else
        Error("Incorrect cell type");
    }  /* if (length == 1) */
  
  LASSERT(length > 1);
  bdef = GetP_def(proc);
  KillNextLoopProc(bdef,laux);
  
  if (LookArgB(bdef,1) != NULL)
    newbeh = GetArgB(bdef,1);
  else
    newbeh = NULL;
  
  laux = Add_list((DataListTyp)proc,laux);
  laux = Next_list(laux);
  l2aux = laux;
  l2aux = Next_list(l2aux);
  while ((laux != NULL) && (l2aux != NULL))
    {
      nextproc = (DescriptorTyp)LookInfo_list(laux);
      bdef1 = GetP_def(nextproc);
      KillNextLoopProc(bdef1,laux);
      if (LookArgB(bdef1,1) != NULL)
        {
          bnext = GetArgB(bdef1,1);
          newbeh = AppendUB(newbeh,bnext);
        }
      pinst = MakeB(proc,ProcessInstC);
      at = LookA(bdef,GLA);
      if (at != NULL)
        PutA(pinst,at);
      PutArgB(bdef1,pinst,1);
      
      laux = Next_list(laux);
      l2aux = Next_list(l2aux);
    }
  
  if (newbeh != NULL)
    PutArgB(bdef,newbeh,1);
  else
    PutStopCell(bdef);
  
}




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




/* Kill_Loop
 * If some loop of processes is found in "b" then removes the first loop
 * of processes found and returns TRUE. If it is not found any loop then
 * returns FALSE. "l" is a list used for keeping the processes of the loop.
 */
static boolean Kill_Loop(b,l)
     BehTyp b;
     ListTyp l;
     
{
  CellTypeTyp type;
  BehTyp bnext,branch;
  int i,num;
  ListTyp laux;
  DescriptorTyp proc;
  
  
  LASSERT(b != NULL);
  LASSERT(LookTypeB(b) == ProcessDefC);
  
  proc = LookNameB(b);
  if (In_list((DataListTyp)proc,l,(boolean (*) ())NULL) == TRUE)
    {
      BreakLoop(proc,l);
      Disp_list(l);
      return TRUE;
    }
  else
    {
      l = Add_list((DataListTyp)proc,l);
      bnext = LookArgB(b,1);
      type = LookTypeB(bnext);
      switch(type)
        {
        case StopC:
          Disp_list(l);
          return FALSE;
          
        case GateC:
          Disp_list(l);
          return FALSE;
          
        case ProcessInstC:
          return Kill_Loop(GetP_def(LookNameB(bnext)),l);
          
        case AlternativeC:
          num = NumArgB(bnext);
          for (i = 1 ; i <= num ; i++)
            {
              branch = LookArgB(bnext,i);
              if (LookTypeB(branch) == ProcessInstC)
                {
                  laux = Copy_list(l,(DataListTyp (*) ())NULL);
                  if (Kill_Loop(GetP_def(LookNameB(branch)),laux) == TRUE)
                    {
                      Disp_list(l);
                      return TRUE;
                    }
                }
            }
          Disp_list(l);
          return FALSE;
          
        default:
          Error("Incorrect cell type");
          break;
        }
    }  /* else */
  return FALSE;
}





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




/* RmvLoops
 * Removes loops of processes from process number "proc1" to "procn".
 */
void RmvLoops(proc1,procn)
     DescriptorTyp proc1,procn;
     
     
{
  DescriptorTyp i;
  ListTyp l;
  
  
  LASSERT(proc1 <= procn);
  
  
  for (i = proc1 ; i <= procn ; i++)
    {
      l = Create_list();
      while (Kill_Loop(GetP_def(i),l) == TRUE)
        l = Create_list();
    }
}




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





/* RmvStopProcs
 * Removes process instantiations of a alternative if these processes
 * are stop processes in the behaviour "b".
 */
static void RmvStopProcs(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,num;
  BehTyp bdef,beh;
  
  
  LASSERT( b != NULL);
  
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      RmvStopProcs(LookArgB(b,1));
      return;
      
    case AlternativeC:
      i = 1;
      while ((i <= NumArgB(b)) && (LookTypeB(b) == AlternativeC))
        {
          beh = LookArgB(b,i);
          if (LookTypeB(beh) == ProcessInstC)
            {
              bdef = LookArgB(GetP_def(LookNameB(beh)),1);
              while (LookTypeB(bdef) == ProcessInstC)
                bdef = LookArgB(GetP_def(LookNameB(bdef)),1);           
              if (LookTypeB(bdef) == StopC)
                {
                  FreeArgB(b,i);
                  i--;
                }
            }
          i++;
        }
      
      if (LookTypeB(b) == AlternativeC)
        {
          num = NumArgB(b);
          for (i=1 ; i<=num ; i++)
            RmvStopProcs(LookArgB(b,i));
        }
      else
        RmvStopProcs(b);
      
      return;
      
    case ProcessInstC:
      RmvStopProcs(GetP_def(LookNameB(b)));
      return;
      
    case ProcessDefC:
      if (In_list((DataListTyp)LookNameB(b),list,(boolean (*) ())NULL) ==TRUE)
        return;
      else
        list = Add_list((DataListTyp)LookNameB(b),list);
      
      RmvStopProcs(LookArgB(b,1));
      return;
      
    default:
      Error("invalid cell");
      break;
    }
  
}




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




/* RmvAltStops
 * Removes stops in alternatives in the recursive behaviour "b".
 */
BehTyp RmvAltStops(b)
     BehTyp b;
     
{
  b = RmAltStopInBeh(b);
  list = Create_list();
  RmvStopProcs(b); 
  Disp_list(list);
  return b;
}




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



/* RmvAltSameP
 * Removes from alternatives instantiations of the same process in the
 * behaviour "b".
 */
static void RmvAltSameP(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,j,num;
  BehTyp beh1,beh2;
  
  
  LASSERT( b != NULL);
  
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      RmvAltSameP(LookArgB(b,1));
      return;
      
    case AlternativeC:
      i = 1;
      while ((i <= NumArgB(b)) && (LookTypeB(b) == AlternativeC))
        {
          beh1 = LookArgB(b,i);
          if (LookTypeB(beh1) == ProcessInstC)
            for (j = i + 1 ; j <= NumArgB(b) ; ++j)
              {
                beh2 = LookArgB(b,j);
                if (LookTypeB(beh2) == ProcessInstC)
                  if (LookNameB(beh1) == LookNameB(beh2))
                    {
                      FreeArgB(b,j);
                      j--;
                    }
              }
          i++;
        }
      
      if (LookTypeB(b) == AlternativeC)
        {
          num = NumArgB(b);
          for (i=1 ; i<=num ; i++)
            RmvAltSameP(LookArgB(b,i));
        }
      else
        RmvAltSameP(b);
      
      return;
      
    case ProcessInstC:
      RmvAltSameP(GetP_def(LookNameB(b)));
      return;
      
    case ProcessDefC:
      if (In_list((DataListTyp)LookNameB(b),list,(boolean (*) ())NULL) ==TRUE)
        return;   
      else
        list = Add_list((DataListTyp)LookNameB(b),list);
      
      RmvAltSameP(LookArgB(b,1));
      return;
      
    default:
      Error("invalid cell");
      break;
    }
  
}




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



/* Call_RmvAltSameP
 * Calls RmvAltSameP function (initialization purposes).
 */
static void Call_RmvAltSameP(b)
     BehTyp b;
     
{
  list = Create_list();
  RmvAltSameP(b); 
  Disp_list(list);
}






/*******************************************************************
 *
 *
 *         DECOMPOSITION FUNCTIONS
 *
 *
 ********************************************************************/




/* Make_DefC
 * Creates the process definition cell of the decomposition process 
 * of the process with descriptor "desc" and returns it.
 * Its decomposition mode is indicated by "decmode" and "gsmode".
 */
static BehTyp Make_DefC(desc,decmode,gsmode)
     DescriptorTyp desc;
     Decomp_Mode decmode;
     GateSet_Mode gsmode;
     
{
  char* name;
  char* nameaux;
  int   length;
  BehTyp def;
  DescriptorTyp d;
  
  
  nameaux = GetP_name(desc);
  length = strlen(nameaux);
  name = (char*)emalloc(length + 4);
  
  switch(decmode + gsmode)
    {
    case 1:
      (void)sprintf(name,"%s_r1",nameaux);
      break;
      
    case 2:
      (void)sprintf(name,"%s_r2",nameaux);
      break;
      
    case 3:
      (void)sprintf(name,"%s_s1",nameaux);
      break;
      
    case 4:
      (void)sprintf(name,"%s_s2",nameaux);
      break;
      
    default:
      Error("Invalid Mode");
      break;
    }
  
  def = MakeB(0,ProcessDefC);
  d = Declare_proc(name,def,NOEXITF);
  PutNameB(def,d);
  Add_Desc_Table(decmode,gsmode,desc,d);
  return def;
}




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




/* Call_Rec_Rest
 * This function is used for calling "Rec_Rest" (Rest call) differently
 * depending if the previous call was a "Sync call" or it was
 * a "Rest call". The gateset "gsync" will be the gateset "gs1" of the 
 * Rest_ function if it was a "Sync call" and empty if not. The others para-
 * meters are the same that in "Rec_Rest".
 */
static void Call_Rec_Rest(b,brest,gs1,gs2,gsync,gsmode)
     BehTyp b,brest;
     GateSetTyp gs1,gs2,gsync;
     GateSet_Mode gsmode;
     
{
  GateSetTyp gs;
  
  if (IsEmptyGS(gsync) == TRUE)
    Rec_Rest(b,brest,gs1,gs2,gsync,gsmode);   /* the previous call  */
  else                                        /* was a Rest call.   */
    {
      gs=CreateGS();
      Rec_Rest(b,brest,gsync,gs2,gs,gsmode);   /* the previous call */
      FreeGS(gs);                              /* was a Sync call.  */
    }
}






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




/* Rec_Rest
 * Recursive function that evaluates the visible communication restriction
 * function of the behaviour "b" with the gatesets "gs1" and "gs2" (in 
 * this order).
 * The "rest tree" is built over the cell "brest", "gsmode" signals the
 * decomposition gateset mode and "gsync" is a gateset used for "Sync calls".
 */  
static void Rec_Rest(b,brest,gs1,gs2,gsync,gsmode)
     BehTyp b,brest;
     GateSetTyp gs1,gs2,gsync;
     GateSet_Mode gsmode;
     
{
  BehTyp bsync;
  BehTyp beh;
  BehTyp newcell;
  BehTyp pinst,def;
  ListTyp l1,l2_1,laux1,laux2;
  int i;
  int length1,length2_1;
  CellTypeTyp type;
  DescriptorTyp d;
  GateSetTyp intersgs,diffgs;
  
  
  LASSERT(b != NULL);
  
  if (LookTypeB(b) == ProcessDefC)
    b = LookArgB(b,1);
  
  type=LookTypeB(b);
  switch(type)
    {
    case StopC:
      PutStopCell(brest);
      return;
      
    case GateC:
      intersgs=IntersGS(gs1,gs2); 
      
      if (GateInGS(LookNameB(b),gs1) == TRUE)
        {
          newcell=MakeB(LookNameB(b),GateC);
          brest=PutNewCell(brest,newcell);
          Call_Rec_Rest(LookArgB(b,1),brest,gs1,gs2,gsync,gsmode);
          FreeGS(intersgs);
          return;
        }
      
      diffgs=DiffGS(gs2,gs1);
      if ((GateInGS(LookNameB(b),diffgs) == TRUE) &&
          (IsEmptyGS(intersgs) == FALSE))
        {
          FreeGS(diffgs);
          FreeGS(intersgs);
          bsync=Rec_Sync(LookArgB(b,1),gs1,gs2,gsync,gsmode);
          brest=PutNewCell(brest,bsync);
          return;
        }
      else
        {
          FreeGS(diffgs);
          FreeGS(intersgs);
          PutStopCell(brest);
          return;
        }
      
    case AlternativeC:       
      l1=Create_list();    /* branches that belong to gs1 */
      l2_1=Create_list();  /* branches that belong to gs2-gs1 */
      intersgs=IntersGS(gs1,gs2); 
      
      diffgs = DiffGS(gs2,gs1);
      for (i=1; i<=NumArgB(b); i++)
        {
          if (GateInGS(LookNameB(LookArgB(b,i)),gs1) == TRUE)
            l1=Add_list((DataListTyp)i,l1);
          else
            if ((GateInGS(LookNameB(LookArgB(b,i)),diffgs) == TRUE) && (IsEmptyGS(intersgs) == FALSE))
	      l2_1=Add_list((DataListTyp)i,l2_1);
        }
      
      FreeGS(diffgs);
      FreeGS(intersgs);
      length1=Length_list(l1);
      length2_1=Length_list(l2_1);
      
      beh=NULL;
      
      laux1=l1;
      if (length1 > 0)
        for (i=1; i<=length1; i++,laux1=Next_list(laux1))
          {
            newcell=MakeB(LookNameB(LookArgB(b,(int) LookInfo_list(laux1))),GateC);       
            beh=AppendUB(beh,newcell);
            if (LookTypeB(beh) == AlternativeC)
              Call_Rec_Rest(LookArgB(LookArgB(b,(int) LookInfo_list(laux1)),1),LookArgB(beh,i),gs1,gs2,gsync,gsmode);
            else
              Call_Rec_Rest(LookArgB(LookArgB(b,(int) LookInfo_list(laux1)),1),beh,gs1,gs2,gsync,gsmode);
          }
      
      laux2=l2_1;
      if (length2_1 > 0)
        for (i=1; i<=length2_1; i++,laux2=Next_list(laux2))
          {
            bsync=Rec_Sync(LookArgB(LookArgB(b,(int) LookInfo_list(laux2)),1),gs1,gs2,gsync,gsmode);
            switch(LookTypeB(bsync))
              {
              case StopC:
                FreeB(bsync); 
                break;
                
              case GateC:
                beh=AppendUB(beh,bsync);
                break;
                
              case AlternativeC:
                beh=AppendUB(beh,bsync);
                break;
		
              case ProcessInstC:
                beh=AppendUB(beh,bsync);
                break;
		
              default:
                Error("Invalid Lotos operator for Inverse Expansion");
                break;
              }   /* switch */
          }  /* for */
      if ((length1 == 0) && ((length2_1 == 0) || (beh == NULL)))
        {
          Disp_list(l1);
          Disp_list(l2_1);
          PutStopCell(brest);
          return;
        }
      else
        {
          brest=PutNewCell(brest,beh);
          Disp_list(l1);
          Disp_list(l2_1);
          return;
        }
      
    case ProcessInstC:
      if (IsEmptyGS(gsync) == TRUE)        /* rest call */
	{
	  if ((d = LookDescTable(LookNameB(b),REST,gsmode)) != 0)
	    {
	      pinst = MakeProcInst(d);
	      brest = PutNewCell(brest,pinst);
	      return;
	    }
	  else
	    {
	      def = Make_DefC(LookNameB(b),REST,gsmode);
	      Rec_Rest(GetP_def(LookNameB(b)),def,gs1,gs2,gsync,gsmode);
	      pinst = MakeProcInst(LookNameB(def));
	      brest = PutNewCell(brest,pinst);
	      return;
	    }
	}
      else              /* sync call */
	{
	  if ((d = LookDescTable(LookNameB(b),SYNCR,gsmode)) != 0)
	    {
	      pinst = MakeProcInst(d);
	      brest = PutNewCell(brest,pinst);
	      return;
	    }
	  else
	    {
	      def = Make_DefC(LookNameB(b),SYNCR,gsmode);
	      Rec_Rest(GetP_def(LookNameB(b)),def,gs1,gs2,gsync,gsmode);
	      pinst = MakeProcInst(LookNameB(def));
	      brest = PutNewCell(brest,pinst);
	      return;
	    }
	}
      
    default:   
      Error("Invalid Lotos operator for Inverse Expansion");
      break;
    }  /* switch */
}  





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




/* Rec_Sync
 * Returns the b's "sync behaviour" with the gatesets "gs1" and "gs2" (in this
 * order) being "gsmode" the decomposition gateset mode.
 * Makes a "Sync call" using Rec_Rest function.
 */
static BehTyp Rec_Sync(b,gs1,gs2,gsync,gsmode)
     BehTyp b;
     GateSetTyp gs1,gs2,gsync;
     GateSet_Mode gsmode;
     
{
  BehTyp baux1,baux2;
  GateSetTyp gs;
  
  if (IsEmptyGS(gsync) == TRUE)            /* call from rest */
    {
      gs = IntersGS(gs1,gs2);
      baux1 = MakeB(0,StopC);
      Rec_Rest(b,baux1,gs,gs2,gs1,gsmode);
      baux2 = GetArgB(baux1,1);
      FreeB(baux1); 
      FreeGS(gs);
      return baux2;
    }
  else                                     /* call from sync */
    {
      baux1=MakeB(0,StopC);
      Rec_Rest(b,baux1,gs1,gs2,gsync,gsmode);
      baux2=GetArgB(baux1,1);
      FreeB(baux1); 
      return baux2;
    }
}




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




/* Make_Rest_Procs
 * Returns the "rest behaviour" of "b" with the gatesets "gs1" and
 * "gs2" (in this order) and the decomposition gateset mode "gsmode".
 * "desc" is the descriptor that will be passed to "Make_DefC" to
 * make the process definition cell.
 */
BehTyp Make_Rest_Procs(desc,b,gs1,gs2,gsmode)
     BehTyp b;
     GateSetTyp gs1,gs2;
     GateSet_Mode gsmode;
     DescriptorTyp desc;
     
{
  GateSetTyp gsync;
  BehTyp def;
  
  
  LASSERT(b != NULL);
  LASSERT(gs1 != NULL);
  LASSERT(gs2 != NULL);
  
  def = Make_DefC(desc,REST,gsmode);
  
  gsync = CreateGS();
  Rec_Rest(b,def,gs1,gs2,gsync,gsmode);
  FreeGS(gsync);
  
  return def;
}





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




/* Rec_InvExp
 * Decompose the behaviour "b" into two sub-behaviours communicating with
 * the common gates of "gs1" and "gs2" (if they have , if not , by pure
 * interleaving) if it is posible: one sub-behaviour with the gates contained
 * in "gs1" and the other with the gates of "gs2".
 * If the decomposition is not posible it will be indicated with a message.
 */
void Rec_InvExp(b,gs1,gs2)
     BehTyp b;
     GateSetTyp gs1,gs2;
     
{
  DescriptorTyp proc_1,proc_n,proc_1_1;
  BehTyp def1,def2,comp;
  DescriptorTyp newproc;
  
  
  LASSERT(b != NULL);
  LASSERT(gs1 != NULL);
  LASSERT(gs2 != NULL);
  
  
  if (LookTypeB(b) == ProcessInstC)
    b = GetP_def(LookNameB(b));
  
  if (Call_Allowed_Cells(b) == FALSE)
    {
      printError("      ");
      printError("The current behaviour contains not supported operators.\n");
      return;
    }
  
  if (Call_Is_Determ(b) == FALSE)
    {
      printError("      ");
      printError("Only deterministic behaviours are supported.\n");
      return;
    }
  
  
  Init_Desc_Table();
  if (LookTypeB(b) != ProcessDefC)
    {
      newproc = NewProc();
      proc_1 = LastTableP();
      def1 = Make_Rest_Procs(newproc,b,gs1,gs2,GS1);
      proc_1_1 = LastTableP();
      def2 = Make_Rest_Procs(newproc,b,gs2,gs1,GS2);
    }
  else
    {
      proc_1 = LastTableP();
      def1 = Make_Rest_Procs(LookNameB(b),b,gs1,gs2,GS1);
      proc_1_1 = LastTableP();
      def2 = Make_Rest_Procs(LookNameB(b),b,gs2,gs1,GS2);
    }
  
  
  Free_Desc_Table();
  proc_n = LastTableP();
  
  PutGatestoProcs(proc_1 + 1,proc_n);
  
  
  RmvLoops(proc_1 + 1,proc_n);  
  
  
  def1 = RmvAltStops(def1);
  def2 = RmvAltStops(def2);
  
  Call_RmvAltSameP(def1);
  Call_RmvAltSameP(def2);
  
  
  VC_DE_Expand(def1,FALSE); 
  VC_DE_Expand(def2,FALSE);
  
  
  comp = IsDecomp(b,def1,def2);
  
  
  if (comp != NULL)
    {
      FreeProcTable(proc_1 + 2,proc_1_1);
      FreeProcTable(proc_1_1 + 2,proc_n);
      ParalComp(comp,def1,def2);
      if (LookTypeB(b) == ProcessDefC)
        b = LookArgB(b,1);
      GlueB(b,comp);
    }
  else
    {
      FreeProcTable(proc_1 + 1,LastTableP());
      printTarget("The current behaviour can not be decomposed in this way.\n\n");
    }      
}


#endif /* INVEXP */
