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

/***********************************
  
  Miguel Angel Palomares Ortega
  
  22-4-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 the behaviour must not
  be recursive (and it must be deterministic if we are going to de -
  compose by Visible Communication).      
  
  
  
  ************************************/

#ifdef INVEXP

#include "iefunc.h"
#include "ie_nrec.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 "balotosf.h"



/******************************************************************
 *
 *  function declarations
 *
 *******************************************************************/



static BehTyp Sync();

static void Rrest_();

static void DE();


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


/* QuickSortBranches
 * QuickSorts to sort the branches of the Alternative b.
 */
static void QuickSortBranches(b,left,right)
     BehTyp b;
     int left,right;
{
  int i,j,x;
  BehTyp auxi, auxj;
  
  i = left;
  j = right;
  x = LookNameB(LookArgB(b,(left+right)/2));
  do {
    while (LookNameB(LookArgB(b,i)) < x) i++;
    while (LookNameB(LookArgB(b,j)) > x) j--;
    if (i<j) {
      auxj = GetArgB(b,j);
      auxi = GetArgB(b,i);
      PutArgB(b,auxi,j);
      PutArgB(b,auxj,i);
    }
    if (i<=j) {
      i++;
      j--;
    }
  } while (i<=j);
  if (left<j) 
    QuickSortBranches(b,left,j);
  if (right>i) 
    QuickSortBranches(b,i,right);
}


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


/* Rsort
 * Recursive function used for sorting the behaviour "b".
 * (Sort call it)
 */
static void Rsort(b)
     BehTyp b;
{
  CellTypeTyp type;
  int i,n;
  
  LASSERT(b != NULL);
  type = LookType(b);
  switch(type) 
    { case StopC :
	return;
	
      case AlternativeC :
	n = NumArgB(b);
	QuickSortBranches(b,1,n);
	for (i=1 ; i<=n ; i++)
	  Rsort(LookArgB(b,i));
	return;
	
      case GateC :
	Rsort(LookArgB(b,1));
	return;
	
      default : 
	Error("Invalid Lotos Operator for Inverse Expansion");
	break;
      } 
  return;
}   


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


/* Sort
 * Sorts all the branches of the behaviour b deleting "stops" in alternatives.
 * It returns a sorted copy of "b".
 */
static BehTyp Sort(b)
     BehTyp b;
{ 
  BehTyp bcopy;
  
  bcopy=CopyB(b);
  bcopy=RmAltStopInBeh(bcopy);
  Rsort(bcopy);
  return bcopy;
}


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


/* Cmp
 * Returns if behaviour b1 is equal than b2.
 */
static boolean Cmp(b1,b2)
     BehTyp b1,b2;
{
  CellTypeTyp type1;
  DescriptorTyp k,i,j,equal1,equal2;
  GateSetTyp gs;
  int num;
  boolean found;
  
  
  LASSERT(b1 != NULL);
  LASSERT(b2 != NULL);
  
  
  if ((type1=LookTypeB(b1)) != LookTypeB(b2))
    return FALSE;
  else
    switch(type1)
      { case StopC:
          return TRUE;
          
        case GateC:
          if (LookNameB(b1) != LookNameB(b2))
            return FALSE;
          else 
            return Cmp(LookArgB(b1,1),LookArgB(b2,1));
          
        case AlternativeC:
          num = NumArgB(b1);
          if (num != NumArgB(b2))
            return FALSE;
          i = 1;
          while(i <= num)
            {
              if (LookNameB(LookArgB(b1,i)) != LookNameB(LookArgB(b2,i)))
                return FALSE;
              j = i + 1;
              while( ( j <= num ) && ( LookNameB(LookArgB(b1,i)) == LookNameB(LookArgB(b1,j)) ) )
                j++;
              equal1 = j - i;
              
              j = i + 1;
              while( ( j <= num ) && ( LookNameB(LookArgB(b2,i)) == LookNameB(LookArgB(b2,j)) ) )
                j++;
              equal2 = j - i;
              
              if (equal1 != equal2)
                return FALSE;
              gs = NewGS();
              for (j = i ; j < i + equal1 ; j++)
                gs = AddGS(gs,j);
	      
              for (j = i ; j < i + equal1 ; j++)
                {
                  found = FALSE;
                  for (k = i ; k < i + equal1 ; k++)
                    if (found == FALSE)
                      if (GateInGS(k,gs) == TRUE)
                        if (Cmp(LookArgB(b1,j),LookArgB(b2,k)) == TRUE)
                          {
                            gs = RemoveGS(gs,k);
                            found = TRUE;
                          }
                  
                  if (found == FALSE)
                    {
                      FreeGS(gs);
                      return FALSE;
                    }
                }
	      
              LASSERT(IsEmptyGS(gs) == TRUE);
              FreeGS(gs);
              i = i + equal1;
            }       /* while (i <= num) */
          
          return TRUE;
	  
          
        default:
          Error("Invalid Lotos Operator for Inverse Expansion");
          break;
        }
  return FALSE;
}



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



/* Call_Cmp_Sort
 * Returns if "b1" (sorted) is equal than "b2" (sorted).
 */
static boolean Call_Cmp_Sort(b1,b2)
     BehTyp b1,b2;
     
{
  BehTyp bsort1,bsort2;
  
  
  bsort1=Sort(b1);
  bsort2=Sort(b2);
  
  
  if (Cmp(bsort1,bsort2)) {
    FreeB(bsort1);
    FreeB(bsort2);
    return TRUE;
  }
  else {
    FreeB(bsort1);
    FreeB(bsort2);
    return FALSE;
  }
}


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


/* Glue_Beh_Decomp
 * Compose in parallel behaviours "b1" and "b2" by the ParallelCell
 * "comp" creating the new processes depending on the mode "mode" of
 * decomposition and glue this parallel behaviour into "b".
 */
static void Glue_Beh_Decomp(b,b1,b2,comp,gs1,gs2,mode)
     BehTyp b,b1,b2;
     BehTyp comp;
     GateSetTyp gs1,gs2;
     IEmode mode;
     
{ 
  DescriptorTyp desc1,desc2;
  char* name;
  BehTyp def;
  GateListTyp gl1,gl2;
  PAttrTyp at1,at2;
  
  def=MakeB(0,ProcessDefC);
  PutArgB(def,b1,1);
  gl1=GateSet_to_GateList(gs1);
  at1=MakeA((AttrValueTyp)gl1,GLA);
  PutA(def,at1);
  name=(char*)emalloc(NAMESIZE);
  if (mode == VCM)
    (void)sprintf(name,"%s","vc_proc");
  else if (mode == PIM)
    (void)sprintf(name,"%s","pi_proc");
  desc1 = Declare_proc(name,def,NOEXITF);
  PutNameB(def,desc1);      
  
  def = MakeB(0,ProcessDefC);
  PutArgB(def,b2,1);
  gl2=GateSet_to_GateList(gs2);
  at2=MakeA((AttrValueTyp)gl2,GLA);  
  PutA(def,at2);
  desc2=Declare_proc(name,def,NOEXITF);
  PutNameB(def,desc2); 
  
  def=MakeB(0,ProcessInstC);
  PutNameB(def,desc1); 
  PutA(def,at1);
  AddArgB(comp,def);
  def=MakeB(0,ProcessInstC);
  PutNameB(def,desc2);
  PutA(def,at2);
  AddArgB(comp,def);
  GlueB(b,comp);
}


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


/* Allowed_Cells
 * Returns if behaviour "b" contains allowed cells for this Inverse
 * Expansion algorithms.
 */ 
static boolean Allowed_Cells(b)
     BehTyp b;
     
{
  int i,num;
  CellTypeTyp type;
  PAttrTyp at;  
  
  
  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 Allowed_Cells(LookArgB(b,1));
      
    case AlternativeC:
      num=NumArgB(b);
      for (i=1 ;i <= num ;++i)
        if (Allowed_Cells(LookArgB(b,i)) == FALSE)
          return FALSE;
      return TRUE;
      
    default:
      return FALSE;
    }
}





/**********************************************************************
 *
 *    Pure Interleaving Decomposition functions
 *
 ***********************************************************************/


/* Rrest
 * Recursive function that evaluates the pure interleaving restriction
 * function of the behaviour "b" with the gateset "gs".
 * The "rest tree" is built over the auxiliar cell "baux".
 * (Rest call it)
 */
static void Rrest(b,baux,gs)
     BehTyp b,baux;
     GateSetTyp gs;
     
{
  BehTyp newcell;
  CellTypeTyp type;
  ListTyp l,laux;
  int numbranches;
  int i;
  
  LASSERT (b != NULL);
  type = LookTypeB(b);
  switch(type)
    {
    case StopC:
      PutStopCell(baux);
      return;
      
    case GateC:
      if (GateInGS(LookNameB(b),gs) == TRUE)
        {
          newcell=MakeB(LookNameB(b),GateC);
          baux=PutNewCell(baux,newcell);
          Rrest(LookArgB(b,1),baux,gs);
          return;
        }
      else
        {
          PutStopCell(baux);
          return;
        }  
      
    case AlternativeC:
      numbranches=0;
      l=Create_list();
      for (i=1; i<=NumArgB(b); i++)
        if (GateInGS(LookNameB(LookArgB(b,i)),gs) == TRUE) 
          {
            ++numbranches;
            l=Add_list((DataListTyp)i,l);
          }
      if (numbranches == 0)
        {
          Disp_list(l);
          PutStopCell(baux);
          return;
        }
      else if (numbranches == 1)
        {
          newcell=MakeB(LookNameB(LookArgB(b,(int) LookInfo_list(l))),
			GateC);
          baux=PutNewCell(baux,newcell);
          Rrest(LookArgB(LookArgB(b,(int) LookInfo_list(l)),1),baux,gs);
          Disp_list(l);
          return;
        }
      else if (numbranches >= 2)
        {
          newcell=MakeB(0,AlternativeC);
          baux=PutNewCell(baux,newcell);
          laux = l;
          for (i=1 ;i <= numbranches ; ++i,l=Next_list(l))
            {
              newcell=MakeB(LookNameB(LookArgB(b,(int) LookInfo_list(l))),GateC);
              AddArgB(baux,newcell);
              Rrest(LookArgB(LookArgB(b,(int) LookInfo_list(l)),1),LookArgB(baux,i),gs);
            }
          Disp_list(laux);
          return;
        }                             
      
    default:
      Error("Invalid Lotos operator for Inverse Expansion");
      break;
    }     /* switch */
}



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


/* Rest
 * Returns the b`s "rest behaviour" with the gateset "gs"(calling Rrest).
 */
static BehTyp Rest(b,gs)
     BehTyp b;
     GateSetTyp gs;
     
{
  BehTyp baux1,baux2;
  
  b=RmAltStopInBeh(b);
  baux1=MakeB(0,StopC);
  Rrest(b,baux1,gs);    /* builds b's rest tree  being baux1 is root */
  baux2=GetArgB(baux1,1);
  FreeB(baux1);
  return baux2;
}


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


/* Call_Cmp_Rest
 * Returns if the "rest tree" of "b1" with the gateset "gs1" is equal
 * than the "rest tree" of "b2" with the gateset "gs2".
 */
static boolean Call_Cmp_Rest(b1,gs1,b2,gs2)
     BehTyp b1,b2;
     GateSetTyp gs1,gs2;
     
{
  BehTyp brest1,brest2;
  BehTyp bsort1,bsort2;
  
  
  brest1=Rest(b1,gs1);
  brest2=Rest(b2,gs2);  
  bsort1=Sort(brest1);
  bsort2=Sort(brest2);
  
  
  if (Cmp(bsort1,bsort2) == TRUE)
    {
      FreeB(brest1);
      FreeB(brest2);       
      FreeB(bsort1);
      FreeB(bsort2);
      return TRUE;
    }
  else
    {
      FreeB(brest1);
      FreeB(brest2);       
      FreeB(bsort1);
      FreeB(bsort2);
      return FALSE;
    }
}


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


/* IsPar
 * Returns if the behaviour "b" can be decomposed by Pure Interleaving
 * with the gateset "gs1" ("gs2" is the complementary gateset of "gs1").
 */
static boolean IsPar(gs1,gs2,b)
     GateSetTyp gs1,gs2;
     BehTyp b;
     
{
  int i;
  CellTypeTyp type;
  
  type=LookTypeB(b);
  switch(type)
    {
    case StopC:
      return TRUE;
      
    case GateC:
      if (GateInGS(LookNameB(b),gs1) == TRUE)
        {
          if (Call_Cmp_Rest(b,gs2,LookArgB(b,1),gs2) == FALSE)
            return FALSE;
        }
      else
        if (Call_Cmp_Rest(b,gs1,LookArgB(b,1),gs1) == FALSE)
          return FALSE;
      return IsPar(gs1,gs2,LookArgB(b,1));
      
    case AlternativeC:
      for (i=1 ;i <= NumArgB(b) ;++i)
        {
          if (GateInGS(LookNameB(LookArgB(b,i)),gs1) == TRUE)      
            {
              if (Call_Cmp_Rest(b,gs2,LookArgB(LookArgB(b,i),1),gs2) == FALSE)
                return FALSE;
            }
          else
            if (Call_Cmp_Rest(b,gs1,LookArgB(LookArgB(b,i),1),gs1) == FALSE)
              return FALSE;
        }
      for (i=1 ;i <= NumArgB(b) ;++i)
        if (IsPar(gs1,gs2,LookArgB(LookArgB(b,i),1)) == FALSE)
          return FALSE;
      
      return TRUE;
      
    default:
      Error("Invalid Lotos operator for Inverse Expansion");
      break;
    }
  return (boolean)NULL;
}  


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


/* PI_nrec
 * Decompose the behaviour "b" into two sub-behaviours composed in pure
 * interleaving if it is posible: one sub-behaviour with the gates contained
 * in "gs1" and the other with the others gates.
 * If the decomposition is not posible it will be indicated with a message.
 */
void PI_nrec(b,gs1)
     BehTyp b;
     GateSetTyp gs1;
     
{
  GateSetTyp gs_full,gs1_compl;
  BehTyp b1,b2,comp,bcopy;
  
  
  LASSERT(b != NULL);
  LASSERT(gs1 != NULL);
  while (LookTypeB(b) == ProcessInstC)
    b = LookArgB(GetP_def(LookNameB(b)),1);
  
  if (Allowed_Cells(b) == FALSE)
    {
      Warning("This behaviour contains not supported LOTOS operators.\n");
      return;
    }
  
  bcopy = GetB(b); 
  
  gs_full   = (GateSetTyp)GetGates(bcopy);
  gs1_compl = DiffGS(gs_full,gs1);
  FreeGS(gs_full);
  if (IsPar(gs1,gs1_compl,bcopy) == TRUE) {
    b1=Rest(bcopy,gs1);
    b2=Rest(bcopy,gs1_compl);
    FreeB(bcopy);
    comp=MakeB(0,ParallelC);
    PutNameB(comp,INTER_SYNC);
    Glue_Beh_Decomp(b,b1,b2,comp,gs1,gs1_compl,PIM);
  }
  else {
    FreeB(bcopy);
    FreeGS(gs1_compl);
    printTarget("  The current behaviour can not be decomposed in this way.\n\n");
  }
}



/****************************************************************
 *
 *   Visible Communication Decomposition functions
 *
 *****************************************************************/



/* CallRrest_
 * This function is used for calling "Rrest_" differentiating "syncs calls"
 * and "rest calls". The gateset "gsync" will be the gateset "gs1" of the 
 * Rest_ function if it is a "sync call" and empty if not. The others para-
 * meters are the same that in Rrest_.
 */
static void CallRrest_(b,gs1,gs2,baux,gsync)
     BehTyp b,baux;
     GateSetTyp gs1,gs2,gsync;
     
{
  GateSetTyp gs;
  
  if (IsEmptyGS(gsync) == TRUE)
    Rrest_(b,gs1,gs2,baux,gsync);
  else {
    gs=NewGS();
    Rrest_(b,gsync,gs2,baux,gs);
    FreeGS(gs);
  }
}


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


/* Rrest_
 * 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 auxiliar cell "baux".
 * (Rest_ and Sync functions call this function).
 */  
static void Rrest_(b,gs1,gs2,baux,gsync)
     BehTyp b,baux;
     GateSetTyp gs1,gs2,gsync;
     
{
  BehTyp bsync;
  BehTyp beh;
  BehTyp newcell;
  ListTyp l1,l2_1,l1aux,l2_1aux;
  int i,j;
  int length1,length2_1;
  int NumArg;
  CellTypeTyp type;
  GateSetTyp intersgs;
  
  
  LASSERT(b != NULL);
  type=LookTypeB(b);
  switch(type)
    { case StopC:
	PutStopCell(baux);
	return;
	
      case GateC:
	intersgs=NewGS();
	intersgs=IntersGS(gs1,gs2); 
	
	if (GateInGS(LookNameB(b),gs1) == TRUE) {
	  newcell=MakeB(LookNameB(b),GateC);
	  baux=PutNewCell(baux,newcell);
	  CallRrest_(LookArgB(b,1),gs1,gs2,baux,gsync);
	  FreeGS(intersgs);
	  return;
	}
	else if ((GateInGS(LookNameB(b),DiffGS(gs2,gs1)) == TRUE)
		 && (IsEmptyGS(intersgs) == FALSE))
	  {
	    bsync=Sync(LookArgB(b,1),gs1,gs2,gsync);
	    if (LookTypeB(bsync) == StopC) {
	      PutStopCell(baux);
	      FreeGS(intersgs);
	      return;
	    }
	    else {
	      baux=PutNewCell(baux,bsync);
	      FreeGS(intersgs);
	      return;
	    }
	  }
	else {
	  FreeGS(intersgs);
	  PutStopCell(baux);
	  return;
	}
	
      case AlternativeC:       
	l1=Create_list();    /* branches that belong to gs1 */
	l2_1=Create_list();  /* branches that belong to gs2-gs1 */
	intersgs=NewGS();
	intersgs=IntersGS(gs1,gs2); 
	
	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(gs2,gs1)) == TRUE) && (IsEmptyGS(intersgs) == FALSE))
	    l2_1=Add_list((DataListTyp)i,l2_1);
	}
	
	FreeGS(intersgs);
	length1=Length_list(l1);
	length2_1=Length_list(l2_1);
	
	beh=NULL;
	
	l1aux = Create_list();
	l2_1aux = Create_list();
	
	if (length1 > 0)
	  {
	    l1aux = l1;
	    for (i=1; i<=length1; i++,l1=Next_list(l1)) {
	      newcell=MakeB(LookNameB(LookArgB(b,(int) LookInfo_list(l1))),GateC);       
	      beh=AppendUB(beh,newcell);
	      if (LookTypeB(beh) == AlternativeC)
		CallRrest_(LookArgB(LookArgB(b,(int) LookInfo_list(l1)),1),gs1,gs2,LookArgB(beh,i),gsync);
	      else
		CallRrest_(LookArgB(LookArgB(b,(int) LookInfo_list(l1)),1),gs1,gs2,beh,gsync);
	    }
	  }
	if (length2_1 > 0)
	  {
	    l2_1aux = l2_1;
	    for (i=1; i<=length2_1; i++,l2_1=Next_list(l2_1)) {
	      bsync=Sync(LookArgB(LookArgB(b,(int) LookInfo_list(l2_1)),1),gs1,gs2,gsync);
	      switch(LookTypeB(bsync))
		{ case StopC:
		    break;
		    
		  case GateC:
		    beh=AppendUB(beh,bsync);
		    break;
		    
		  case AlternativeC:
		    NumArg=NumArgB(bsync);
		    for(j=1; j<= NumArg; j++)
		      beh=AppendUB(beh,LookArgB(bsync,j));
		    break;
		    
		  default:
		    Error("Invalid Lotos operator for Inverse Expansion");
		    break;
		  }   /* switch */
	    }  /* for */
	  }
	
	if ((length1 == 0) && ((length2_1 == 0) || (beh == NULL))) {
	  Disp_list(l1aux);
	  Disp_list(l2_1aux);
	  PutStopCell(baux);
	  return;
	}
	else {
	  baux=PutNewCell(baux,beh);
	  Disp_list(l1aux);
	  Disp_list(l2_1aux);
	  return;
	}
	
      default:   
	Error("Invalid Lotos operator for Inverse Expansion");
	break;
      }  /* switch */
}  


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


/* Rest_
 * Return the b's "rest behaviour" with the gatesets "gs1" and "gs2" (in this
 * order).
 * Makes the first "rest call" using Rrest_ function.
 */
static BehTyp Rest_(b,gs1,gs2)
     BehTyp b;
     GateSetTyp gs1,gs2;
     
{
  BehTyp baux1,baux2;
  GateSetTyp gs;
  
  b=RmAltStopInBeh(b); 
  gs=NewGS();
  baux1=MakeB(0,StopC);
  Rrest_(b,gs1,gs2,baux1,gs);
  baux2=GetArgB(baux1,1);
  FreeB(baux1);
  FreeGS(gs);
  return baux2;
}


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


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


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


/* DE
 * Remove non-determinism in the behaviour "b".
 */
static void DE(b)
     BehTyp b;
     
{
  CellTypeTyp type;
  int i,j;
  BehTyp baux,baux2;
  DescriptorTyp name;
  boolean rde;  
  
  
  LASSERT(b!=NULL);
  b=Pre_Branch_Stop(b);
  type=LookTypeB(b);
  switch(type)
    {
    case StopC:
      return;
      
    case GateC:
      DE(LookArgB(b,1));
      return;
      
    case AlternativeC:
      i=1;
      while(i<NumArgB(b)) {
        rde=FALSE;
        for(j=i+1 ;j<=NumArgB(b) ;++j)
          {
            name=LookNameB(LookArgB(b,i));
            if  ( name == LookNameB(LookArgB(b,j)) )
              {
                rde=TRUE;
                baux=GetArgB(LookArgB(b,j),1);
                baux2=GetArgB(LookArgB(b,i),1);
                FreeArgB(b,j);
                baux2=AppendUB(baux2,baux);
                if (type=LookTypeB(b) == AlternativeC) {
                  baux=LookArgB(b,i);
                  PutArgB(baux,baux2,1);
                  DE(LookArgB(LookArgB(b,i),1));
                }
                else {
                  PutArgB(b,baux2,1);
                  DE(LookArgB(b,1));
                }
                --j;
              }
          }  /* for (j=i+1 ... */
        
        if (rde == FALSE)
          DE(LookArgB(LookArgB(b,i),1));
        ++i;
      }
      if (NumArgB(b) == i)
        DE(LookArgB(LookArgB(b,i),1));      
      return;
      
    default:
      Error("Invalid Lotos Operator for Inverse Expansion");
      break;
    }
  return;
}


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


/* Decomp
 * Returns b's "rest behaviour" with the gatesets "gs1" and "gs2" (in this
 * order) removing non-determinism.
 */
static BehTyp Decomp(b,gs1,gs2)
     BehTyp b;
     GateSetTyp gs1,gs2;
     
{
  BehTyp baux;
  
  baux=Rest_(b,gs1,gs2);
  DE(baux);
  return baux;
}


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


/* VC_IsPar
 * Returns the ParallelCell that communicate "b1" and "b2" if behaviour
 * "b" can be decomposed by Visible Communication in "b1" (containing
 * the gates of "gs1") and "b2" (containing the gates of "gs2"). Returns
 * NULL if it is not posible.
 */
static BehTyp VC_IsPar(b,b1,b2,gs1,gs2)
     BehTyp b,b1,b2;
     GateSetTyp gs1,gs2;
     
{
  BehTyp comp,comp_store;
  GateSetTyp inters_gs;
  
  
  inters_gs=IntersGS(gs1,gs2);  
  comp=MakeB(0,ParallelC);
  if (IsEmptyGS(inters_gs)) {
    PutNameB(comp,INTER_SYNC);
    FreeGS(inters_gs);
  }
  else if (EqualGS(gs1,gs2)) {
    PutNameB(comp,FULL_SYNC);
    FreeGS(inters_gs);
  }
  else {
    PutNameB(comp,PART_SYNC);
    PutA(comp,MakeA((AttrValueTyp)inters_gs,GSA));
  }
  
  comp_store=CopyB(comp);
  (void)ShareB(comp); 
  AddArgB(comp,b1);
  AddArgB(comp,b2);
  FreeExpand(comp,-1,FALSE,FALSE,FALSE);
  
  if (Call_Cmp_Sort(b,comp) == TRUE) {
    FreeB(comp); 
    return comp_store;
  }
  else {
    FreeB(comp);
    FreeB(comp_store);
    return NULL;
  }
}


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


/* VC_nrec
 * Decompose the behaviour "b" into two sub-behaviours communicating with
 * the common gates of "gs1" and "gs2" 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 VC_nrec(b,gs1,gs2)
     BehTyp b;
     GateSetTyp gs1,gs2;
     
{
  BehTyp b1,b2,comp;
  BehTyp bcopy,b1_copy,b2_copy;
  
  
  LASSERT(b != NULL);
  LASSERT(gs1 != NULL);
  LASSERT(gs2 != NULL);
  
  while (LookTypeB(b) == ProcessInstC)
    b = LookArgB(GetP_def(LookNameB(b)),1);
  
  if (Allowed_Cells(b) == FALSE) {
    Warning("This behaviour contains not supported LOTOS operators.\n");
    return;
  }
  if (Call_Is_Determ(b) == FALSE) {
    Warning("Only supported deterministic behaviours.\n");
    return;
  }  
  
  LASSERT(b->copy > 0);
  bcopy=GetB(b);  
  b1=Decomp(bcopy,gs1,gs2);
  b2=Decomp(bcopy,gs2,gs1);  
  b1_copy=CopyB(b1);
  b2_copy=CopyB(b2);
  comp=VC_IsPar(bcopy,b1_copy,b2_copy,gs1,gs2);
  FreeB(bcopy);
  if (comp != NULL)
    Glue_Beh_Decomp(b,b1,b2,comp,gs1,gs2,VCM);
  else {
    FreeB(b1);
    FreeB(b2);
    printTarget("  The current behaviour can not be decomposed in this way.\n\n");
  }
}


#endif /* INVEXP */
