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

/***********************************

  David Larrabeiti Lopez

  4 January 1991

  Module to compute synchronization between gates.

  The sequence of operation is:
  if ( Synchr( gatebeh1, gatebeh2 ) )
  {
  pred           = Doffer();             (* in any order *)
  varassignlist1 = Assign1();
  varassignlist2 = Assign2();
  }

  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:

  (none)

  ************************************/


#include "limisc.h"
#include "badefca.h"
#include "exsynchr.h"
#include "basust_v.h"
#include "babool.h"

/* KJT 22/01/23: added function prototypes */

boolean Comp_SortOL (OfferListTyp ol1, OfferListTyp ol2);

#ifdef TIME
static PTimeTyp      time;         /* Future Time constraints  */
static ExprTyp       guard;        /* Future guard for time intervals */
#endif
static ExprListTyp  el;            /* Future components of guard */
static OfferListTyp ol;            /* Future new offer after synchronization */
static PredicateTyp  pred;         /* Future global predicate */
static VarAssignListTyp val1,val2; /* Future val's */

static void release_lists()
{
  FreeVAL( val1 );
  FreeVAL( val2 );
  FreeEL( el );
  FreeOL( ol );
}

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

/* Synchr
 * Checks whether the sinchronization is possible between gates.
 * Builds up 3 internal lists necessary for Merge, Assign1, Assign2 & Doffer
 * so that Synchr is to be called before any of them.
 */
boolean Synchr( g1, g2 )
     BehTyp g1,g2;
{
  OfferListTyp     ol1, ol2;
  ExprTyp          exp;
  SVdescriptorTyp  sv1;
  PredicateTyp     p1, p2;
  boolean mustFreeP1, mustFreeP2;
#ifdef TIME
  ExprTyp       inter,lb1,ub1;
  PTimeTyp       t1,t2;
  DescriptorTyp  tre;
#endif

  if ( LookNameB(g1)!=LookNameB(g2) )
    return FALSE;

  ol1 = (OfferListTyp)LookAInfo( LookA(g1,OLA) );
  ol2 = (OfferListTyp)LookAInfo( LookA(g2,OLA) );
  if ( !Comp_SortOL( ol1, ol2 ) ) {
    return FALSE;
  }

#ifdef TIME
  inter = NULL;
  t1 = (PTimeTyp)LookAInfo( LookA(g1,TA) );
  t2 = (PTimeTyp)LookAInfo( LookA(g2,TA) );
  if (LookType(g1)== GateC) {
    inter = InterT(t1,t2);
    if (strcmp(ExprToStringE(inter),"false")==0) {
      FreeE(inter);
      return FALSE;
    }
  }

  guard = NULL;
#endif

  val1 = Create_list();
  val2 = Create_list();
  el   = CreateEL();
  ol   = CreateOL();
  pred = NULL;


  while ( ol1!=NULL ) {
    if ( LookKindOffer(ol2)==QUESTION ) {          /* !? ?? */
      val2 = AddVAL( val2, LookNameE(LookExprOffer(ol2)),
		    LookExprOffer(ol1) );
      ol = AddOL( MakeOffer(LookKindOffer(ol1),LookExprOffer(ol1)),
		 ol );                       /* mse */
    }
    else
      if ( LookKindOffer(ol1)==EXCLAMATION ) {      /* !! */

	if (!EqualE(LookExprOffer(ol1),LookExprOffer(ol2)))
	  if ((!IsConstE(LookExprOffer(ol1))) ||
	      (!IsConstE(LookExprOffer(ol2)))) {
	    exp = MakeE(GetEqual(),OperationC);
	    AddArgE(exp,LookExprOffer(ol1));   /*mse*/
	    AddArgE(exp,LookExprOffer(ol2));
	    el = AddEL( exp , el );
	  }
	  else {
#ifdef TIME
	    if (inter!=NULL)
	      FreeE(inter);
#endif
	    release_lists();
	    return FALSE;
	  }
	/* mse */
	ol = AddOL( MakeOffer(EXCLAMATION,LookExprOffer(ol1)), ol );
      }
      else {                                         /* ?! */
	val1 = AddVAL( val1, LookNameE(LookExprOffer(ol1)),
		      LookExprOffer(ol2) );
	ol = AddOL(MakeOffer(EXCLAMATION,LookExprOffer(ol2)),ol);
      }                                     /* mse */
    ol1 = MvNextOffer( ol1 );
    ol2 = MvNextOffer( ol2 );
  }

#ifdef TIME
  if (LookType(g1)== GateC ||
      LookType(g1)== IC ||
      LookType(g1)== ExitC   ) {
    lb1 = LowerT(t1,t2);
    ub1 = UpperT(t1,t2);
    if (!EqualE(lb1,ub1)){
      if ((t2->tvar !=NULL) &&
	  !IsConstE(t2->tvar) ){
	if ((t1->tvar!=NULL) &&
	    !IsConstE(t1->tvar)){
	  time= MakeT(t1->tvar,lb1,ub1);
	  val2 = AddVAL( val2, LookNameE(t2->tvar),t1->tvar );
	}
	else
	  time= MakeT(t2->tvar,lb1,ub1);
      }
      else
	if ((t1->tvar!=NULL) &&
	    !IsConstE(t1->tvar))
	  time= MakeT(t1->tvar,lb1,ub1);
	else
	  time= MakeT((ExprTyp) NULL ,lb1,ub1);
    }
    else {
      time= MakeT((ExprTyp)NULL,lb1,ub1);
      if ((t2->tvar !=NULL) &&
	    !IsConstE(t2->tvar) )
	val2 = AddVAL( val2, LookNameE(t2->tvar),lb1);

      if ((t1->tvar!=NULL) &&
	  !IsConstE(t1->tvar))
	val2 = AddVAL( val2, LookNameE(t1->tvar),lb1 );
    }
    if (inter !=NULL)
      if ( !IsConstE(inter)) {
	guard = MakeE(GetEqual(),OperationC);
	tre = FindO("true", FindS("bool"));
	AddArgE(guard,inter);
	AddArgE(guard, MakeE(tre,OperationC));
      }
      else
	FreeE(inter);
  }
#endif

  p1 = (PredicateTyp)LookAInfo(LookA(g1,PA));
  p2 = (PredicateTyp)LookAInfo(LookA(g2,PA));

  mustFreeP1 = FALSE;
  mustFreeP2 = FALSE;

  if ( p1!=NULL && p2!=NULL)  {          /* p1!=NULL && p2!=NULL */
    if (val2!=NULL) {
      sv1 = CreateSV();
      Insert_VAL_SV( val2, &sv1 );
      if ( Var_in_Pred_SV(p2,&sv1) ) {
	mustFreeP2 = TRUE;
	p2  = CopyPred( p2 );
	(void)SubstPredSV( &p2, &sv1 ); /**/
      }
      FreeSV( &sv1 );
    }
    if ( !IsFalse( LookRwPred(p2) ) ) {
      if (val1!=NULL) {
	sv1 = CreateSV();
	Insert_VAL_SV( val1, &sv1 );
	if ( Var_in_Pred_SV(p1,&sv1) ) {
	  mustFreeP1 = TRUE;
	  p1  = CopyPred(p1);
	  (void)SubstPredSV( &p1, &sv1 ); /**/
	}
	FreeSV( &sv1 );
      }
      if ( !IsFalse( LookRwPred(p1) ) ) {
	pred = MakeAndPred(p1,p2);
	if (mustFreeP1) FreePred( p1 );
	if (mustFreeP2) FreePred( p2 );
	if ( !IsFalse( LookRwPred(pred) ) ) {
	  if ( IsTrue( LookRwPred(pred) ) ) {
	    FreePred( pred );
	    pred = NULL;
	  }
	  return TRUE;
	}
      }
      else {
	if (mustFreeP1) FreePred( p1 );
	if (mustFreeP2) FreePred( p2 );
      }
    }
    else
      if (mustFreeP2) FreePred( p2 );
  }
  else {
    if ( p1!=NULL || p2!=NULL ) {
      sv1 = CreateSV();
      if ( p1==NULL ) {           /* p1==NULL */
	if (val2!=NULL) {
	  Insert_VAL_SV( val2, &sv1 );
	  if ( Var_in_Pred_SV(p2,&sv1) ) {
	    pred = CopyPred( p2 );
	    (void)SubstPredSV( &pred, &sv1 ); /**/
	  }
	  else
	    pred = SharePred(p2);
	}
	else
	  pred = SharePred(p2);
      }
      else {                      /* p2==NULL */
	if (val1!=NULL) {
	  Insert_VAL_SV( val1, &sv1 );
	  if ( Var_in_Pred_SV(p1,&sv1) ) {
	    pred = CopyPred( p1 );
	    (void)SubstPredSV( &pred, &sv1 ); /**/
	  }
	  else
	    pred = SharePred(p1);
	}
	else
	  pred = SharePred(p1);
      }
      FreeSV( &sv1 );

      if ( !IsFalse( LookRwPred(pred) ) ) {
	if ( IsTrue( LookRwPred(pred) ) ) {
	  FreePred( pred );
	  pred = NULL;
	}
	return TRUE;
      }
    }
    else
      return TRUE;
  }

#ifdef TIME
  if (guard!=NULL)
    FreeE (guard);
  FreeT (time);
#endif
  if ( pred!=NULL )
    FreePred( pred );
  release_lists();
  return FALSE;
}

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

/* Doffer
 * Returns a list of predicates that have to be satisfied by the expressions
 * in the offerlists to synchronize.
 * ( ex.in : a !E1 ?x:s !E2 |[a]| a !E3 !E4 !E5
 *           ( (E1=E3) , (E2=E5) ) is returned .)
 */
ExprListTyp Doffer()
{
  return el;
}

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

/* Assign1
 * Returns the VarAssignList induced in the first branch of the parallel
 * behaviour by the synchronization.
 */
VarAssignListTyp Assign1()
{
  return val1;
}

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

/* Assign2
 * Returns the VarAssignList induced in the second branch of the parallel
 * behaviour by the synchronization.
 */
VarAssignListTyp Assign2()
{
  return val2;
}

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

/* Merge
 * Returns the OfferList resulting from the synchronization.
 */
OfferListTyp Merge()
{
  return ol;
}

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

/* Global_Pred
 * Returns the resulting predicate.
 */
PredicateTyp Global_Pred()
{
  return pred;
}

#ifdef TIME

/* Global_Time
 * Returns the resulting time constraint.
 */
PTimeTyp  Global_Time()
{
  return time;
}

/* GuardT
 * Returns the symbolic intersection  time intervals of g1, g2
 */
ExprTyp  GuardT()
{
return guard;
}

#endif
/*----------------------------------------------------------------*/
