/***********************************
  (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)
  
  TYPE DEFINITIONS:
  
  (none)
  
  
  FUNCTION DEFINITIONS:
  Synchr : says whether two actions can synchronize or not
  Doffer : resultant offer matching condition for the synchronization
  Assign1 : resultant assignation after the synchronization in the first
  branch of the parallel
  Assign2 : resultant assignation after the synchronization in the second
  branch of the parallel
  Merge : resultant offer list
  Global_Pred :resultant predicate
  
  
  ************************************/


#ifndef EXsynchr_H
#define EXsynchr_H


#include "baattr.h"


/* Synchr
 * Checks whether the sinchronization is possible between two gates.
 * Builds up 3 internal lists necessary for Merge, Assign1, Assign2 & Doffer
 * so that Synchr is to be called before any of them.
 */
extern boolean Synchr(/*g1,g2*/);
/*     BehTyp g1,g2;*/


/* 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 .)
 */
extern ExprListTyp Doffer();


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


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


/* Merge
 * Returns the OfferList resulting from the synchronization.
 */
extern OfferListTyp Merge();


/* Global_Pred
 * Returns the resulting predicate.
 */
extern PredicateTyp Global_Pred();


#ifdef TIME 

/* Global_Time 
 * Returns the resulting time constraint.  
 */ 
extern PTimeTyp  Global_Time(); 


/* GuardT 
 * Returns the symbolic intersection  time intervals of g1, g2 
 */
extern ExprTyp  GuardT();   

#endif 


#endif

