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

/***********************************
  
  Miguel Angel Palomares Ortega
  
  12-11-1992
  
  This module contains complementary functions which are
  used in the Inverse Expansion algorithms.
  
  
  ************************************/

#ifdef INVEXP


#include "licell.h"
#include "badefca.h"
#include "babeh.h"
#include "listdh.h"
#include "limisc.h"
#include "lilists.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 "ietables.h"
#include "lihash.h"


#define MAXGATES MAX_GATES


/****************************************************************
 *
 *              global variables
 *
 *****************************************************************/



/* hash table used for storing states in the functions "Call_Cmp_Rec_Beh"
   and "Cmp_Rec_Beh" */

static HashDTyp htab;


/* list used for searching repeated states in recursive functions */

static ListTyp list;




/****************************************************************
 *
 *              FUNCTIONS
 *
 *****************************************************************/




/* Equal_Sortlist
 * Returns the boolean: "list l1 == list l2".
 * The order of the elements must be the same.
 * eq is a function that returns the equality of two elements of the list
 * boolean eq( e1, e2 )
 */
boolean Equal_Sortlist( l1, l2, eq )
     register ListTyp l1,l2;
     boolean (*eq)();
{
  boolean equal;
  
  equal=TRUE;
  while ((l1!=NULL)&&(l2!=NULL)&&equal) {
    if (eq == NULL)
      {
        if ((l1->info) == (l2->info))
          equal = TRUE;
        else
          equal = FALSE;
      }
    else
      equal = eq( l1->info, l2->info );
    
    l1=l1->next;
    l2=l2->next;
  }
  return (l1 == l2) && equal;
  
}




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



/* Sort_Add_IfNotIn_list
 * Unlike Add_list the element is not Added if it is already in the list.
 * The new element is added sortly (with integer comparison).
 * f == NULL => integer comparison.
 */
ListTyp Sort_Add_IfNotIn_list( e, l, f )
     DataListTyp  e;
     ListTyp l;
     boolean (*f)();
     
{   
  register ListTyp aux, prev , newnode;
  
  
  if (l==NULL)
    return Insert_list(e,Create_list());
  if ( f==NULL ) {
    for ( aux=l; aux!=NULL; prev=aux, aux=aux->next )
      if (e==aux->info)
        return l;
  }
  else
    for ( aux=l; aux!=NULL; prev=aux, aux=aux->next )
      if ((*f)(e,aux->info))
        return l;
  
  if (aux==NULL)
    {
      for (aux = l ; aux !=NULL ; prev = aux , aux = aux->next)
        {
          LASSERT(aux->info != e);
          if (aux->info > e)
            {
              if (aux == l)
                return Insert_list(e,l);
              else
                {
                  newnode = Insert_list(e,aux);
                  prev->next = newnode;
                  return l;
                }
            }
        }
      LASSERT(aux == NULL);
      return Add_list(e,l);
    }   /* if (aux == NULL) */
  return (ListTyp)NULL;
}




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




/* PutStopCell
 * Puts a Stop Cell the first argument of "b".
 */
void PutStopCell(b)
     BehTyp b;
     
{
  BehTyp newcell;
  
  newcell=MakeB(0,StopC);
  PutArgB(b,newcell,1);
}



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



/* PutNewCell
 * Put "newcell" the first argument of "b" (if b is not NULL) and 
 * returns newcell.
 */
BehTyp PutNewCell(b,newcell)
     BehTyp b,newcell;
     
{
  if (b != NULL)
    {
      PutArgB(b,newcell,1);
      b=LookArgB(b,1);
    }
  else
    b=newcell;
  
  return b;
}




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




/* Get_Branches
 * Returns the actions that offers "b" in a sorted list.
 */
ListTyp Get_Branches(b,l)
     BehTyp b;
     ListTyp l;
     
{
  int num,i;
  CellTypeTyp type,typebeh;
  
  
  LASSERT(b != NULL);
  
  
  typebeh = LookTypeB(b);
  
  if (typebeh == ProcessDefC)
    l = Get_Branches(LookArgB(b,1),l);
  
  else if (typebeh == ProcessInstC)
    l = Get_Branches(LookArgB(GetP_def(LookNameB(b)),1),l);
  
  else if (typebeh == AlternativeC)
    {
      num = NumArgB(b);
      for (i=1 ; i<=num ; i++)
        {
          type = LookTypeB(LookArgB(b,i));
          if (type == GateC)
            l = Sort_Add_IfNotIn_list((DataListTyp)LookArgB(b,i),l,(boolean (*) ())NULL);
          else if (type == ProcessInstC)
            l = Get_Branches(LookArgB(GetP_def(LookNameB(LookArgB(b,i))),1),l);
        }
    }
  else if (typebeh == GateC)
    l = Sort_Add_IfNotIn_list((DataListTyp)b,l,(boolean (*) ())NULL);
  
  return l;
}




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



/* Rec_Is_Determ
 * Returns TRUE is behaviour "b" is deterministic (FALSE if not).
 */
static boolean Rec_Is_Determ(b)
     BehTyp b;
     
{
  int numarg,num,i,j;
  CellTypeTyp type;
  ListTyp lgates,l1,l2;
  
  
  
  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);           
          b = LookArgB(b,1);
          type=LookTypeB(b);
        }
    }
  
  switch(type)
    {
    case StopC:
      return TRUE;
      
    case GateC:
      return Rec_Is_Determ(LookArgB(b,1));
      
    case AlternativeC:
      lgates = Create_list();
      lgates = Get_Branches(b,lgates);
      num = Length_list(lgates);
      l1 = lgates;
      for (i=1 ;i <= num ;++i,l1 = Next_list(l1))
        {
          l2 = lgates;
          for (j=1 ;j <= num ;++j,l2 = Next_list(l2)) 
            if ((j != i) && (LookNameB((BehTyp)LookInfo_list(l1)) == LookNameB((BehTyp)LookInfo_list(l2))))
              {
                Disp_list(lgates);
                return FALSE;
              }
        }
      
      Disp_list(lgates);
      
      numarg = NumArgB(b);
      for (i=1 ;i<=numarg ;++i)
        if (Rec_Is_Determ(LookArgB(b,i)) == FALSE)
          return FALSE;
      
      return TRUE;
      
    case ProcessInstC:
      return Rec_Is_Determ(GetP_def(LookNameB(b)));
      
    default:
      Error("Invalid Lotos Operator for Inverse Expansion");
      break;
    }
  return FALSE;
}




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




/* Call_Is_Determ
 * Calls Rec_Is_Determ function (initialization purposes).
 */
boolean Call_Is_Determ(b)
     BehTyp b;
     
{
  boolean bool;
  
  list = Create_list();
  bool = Rec_Is_Determ(b);
  Disp_list(list);
  return bool;
}



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



/* FreeProcTable
 * Frees the processes behaviours from "first" position to "last" 
 * position of the Process Table and puts a stop cell.
 */
void FreeProcTable(first,last)
     DescriptorTyp first,last;
     
{
  DescriptorTyp i;
  BehTyp bdef;
  
  
  for (i = first ; i <= last ; i++)
    {
      bdef = GetP_def(i);
      TrfStop(LookArgB(bdef,1));
    }
}




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



/* NewProc
 * Creates a new process called "proc" and returns its descriptor.
 */
DescriptorTyp NewProc()
     
{
  char* name;
  BehTyp def;
  DescriptorTyp desc;
  
  name = "proc";
  def = MakeB(0,ProcessDefC);
  desc = Declare_proc(name,def,NOEXITF);
  PutNameB(def,desc);
  PutStopCell(def);
  return desc;
}




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




/* MakeProcInst
 * Makes a process Instantiation cell with name "desc" and returns it.
 */
BehTyp MakeProcInst(desc)
     DescriptorTyp desc;
     
{
  BehTyp pinst; 
  
  pinst = MakeB(desc,ProcessInstC);
  
  return pinst;
}



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



/* GetNames
 * Returns a sorted list with the "names" of the gates of "l1" if they
 * are the same for "l2" . If not it returns NULL.
 */
static ListTyp GetNames(l1,l2)
     ListTyp l1,l2;
     
{
  ListTyp l1aux,l2aux,list1,list2;
  
  
  LASSERT(l1 != NULL);
  LASSERT(l2 != NULL);
  
  list1 = Create_list();
  list2 = Create_list();
  
  for (l1aux = l1 ; l1aux != NULL ; l1aux = Next_list(l1aux))
    list1 = Sort_Add_IfNotIn_list((DataListTyp)LookNameB((BehTyp)LookInfo_list(l1aux)),list1,(boolean (*) ())NULL);
  
  for (l2aux = l2 ; l2aux != NULL ; l2aux = Next_list(l2aux))
    list2 = Sort_Add_IfNotIn_list((DataListTyp)LookNameB((BehTyp)LookInfo_list(l2aux)),list2,(boolean (*) ())NULL);
  
  if (Equal_Sortlist(list1,list2,(boolean (*) ())NULL) == TRUE)
    {
      Disp_list(list2);
      return list1;
    }
  else 
    {
      Disp_list(list1);
      Disp_list(list2);
      return (ListTyp)NULL;
    }
}




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




/* Cmp_Rec_Beh
 * Returns TRUE if the lists of behaviours "list1" and "list2" offers
 * the same actions. (FALSE if not)
 */
static boolean Cmp_Rec_Beh(list1,list2)
     ListTyp list1,list2;
     
{
  ListTyp laux,lgatesaux,lgates,l1,l2;
  ListTyp  oftab1[MAXGATES];
  ListTyp  oftab2[MAXGATES];
  boolean alllistsintab;
  int i,j,count,length1,length2,numgates;
  BehTyp beh;
  DescriptorTyp gate;
  EntryTyp pair;
  
  
  LASSERT(list1 != NULL);
  LASSERT(list2 != NULL);
  
  lgates = Create_list();
  lgates = GetNames(list1,list2);
  if (lgates == NULL)
    return FALSE;
  numgates = Length_list(lgates);
  
  lgatesaux = lgates;
  count = 0;
  length1 = Length_list(list1);
  length2 = Length_list(list2);
  for (i = 1 ; i <= numgates ; i++ , lgatesaux = Next_list(lgatesaux))
    {
      gate = (DescriptorTyp)LookInfo_list(lgatesaux);
      l1 = Create_list();
      laux = list1;
      for (j = 1 ; j <= length1 ; j++ , laux = Next_list(laux))
        {
          beh = (BehTyp)LookInfo_list(laux);
          if (LookNameB(beh) == gate)
            l1 = Get_Branches(LookArgB(beh,1),l1);
        }
      
      l2 = Create_list();
      laux = list2;
      for (j = 1 ; j <= length2 ; j++ , laux = Next_list(laux))
        {
          beh = (BehTyp)LookInfo_list(laux);
          if (LookNameB(beh) == gate)
            l2 = Get_Branches(LookArgB(beh,1),l2);
        }
      
      if ( (l1 == NULL) || (l2 == NULL) )
        {
          if ( (l1 != NULL) || (l2 != NULL) )
            {
              for (j = 0 ; j < count ; j++)
                {
                  Disp_list(oftab1[j]);
                  Disp_list(oftab2[j]);
                }
              Disp_list(l1);
              Disp_list(l2);
              Disp_list(lgates);
              return FALSE;
            }
        }
      else
        {
          oftab1[count] = l1;
          oftab2[count] = l2;
          count++;
        }
    }     /* for (i = 1 ... */
  
  Disp_list(lgates);
  if (count == 0)
    return TRUE;
  
  alllistsintab = TRUE;
  for (i = 0 ; i < count ; i++)
    {
      pair = (EntryTyp)Emalloc2Words();
      pair->l1 = oftab1[i];
      pair->l2 = oftab2[i];
      if (In_HT(htab,(DataHashTyp)pair) == FALSE)
        {
          alllistsintab = FALSE;
          Insert_HT(htab,(DataHashTyp)pair);
        }
      else
        {
          Disp_list(oftab1[i]);
          Disp_list(oftab2[i]);
          Free2Words((void*)pair);
          oftab1[i] = Create_list();
          oftab2[i] = Create_list();
        }
    }
  
  if (alllistsintab == TRUE)
    return TRUE;
  
  for (i = 0 ; i < count ; i++)
    if ( (oftab1[i] != NULL) && (oftab2[i] != NULL) )
      if (Cmp_Rec_Beh(oftab1[i],oftab2[i]) == FALSE)
        {
          for (j = 0 ; j < count ; j++)
	    if ( (oftab1[j] != NULL) && (oftab2[j] != NULL) )
	      {
		pair = (EntryTyp)Emalloc2Words();
		pair->l1 = oftab1[j];
		pair->l2 = oftab2[j];
		Remove_HT(htab,(DataHashTyp)pair);
		Free2Words((void*)pair);
	      }
          return FALSE;
        }
  
  return TRUE;
}




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




/* Call_Cmp_Rec_Beh
 * Calls "Cmp_Rec_Beh" function (initialization and termination purposes).
 * Returns if "b1" and "b2" offers the same actions (if they are equivalents).
 */
boolean Call_Cmp_Rec_Beh(b1,b2)
     BehTyp b1;
     BehTyp b2;
     
{
  ListTyp list1,list2;
  boolean bool;
  EntryTyp pair;
  
  
  LASSERT(b1 != NULL);
  LASSERT(b2 != NULL);
  
  list1 = Create_list();
  list2 = Create_list();
  list1 = Get_Branches(b1,list1);
  list2 = Get_Branches(b2,list2);
  
  if ( (list1 == NULL) || (list2 == NULL) )
    {
      if ( (list1 == NULL) && (list2 == NULL) )
        return TRUE;
      else
        {
          Disp_list(list1);
          Disp_list(list2);
          return FALSE;
        }
    }
  htab = CreateHTab();
  pair = (EntryTyp)Emalloc2Words();
  pair->l1 = list1;
  pair->l2 = list2;
  Insert_HT(htab,(DataHashTyp)pair);
  bool = Cmp_Rec_Beh(list1,list2);
  Free_HT(htab);
  return bool;
  
}


#endif /* INVEXP */
