/******************************************************************
 *  (C) Copyright 1994; dit/upm
 *  Distributed under the conditions stated in the
 *  TOPO General Public License (see file LICENSE)
 ******************************************************************
 *  $Log$
 ******************************************************************/

/******************************************************************
 *  
 *  Santiago Pavon Gomez
 *
 *  29 Aug 1991
 *
 *  Some general functions to manage LOTOS expressions.
 *  
 *  COMPILATION FLAGS:
 *  
 *  TYPE DEFINITIONS:
 *  
 *  FUNCTION DEFINITIONS:
 *     TrfStop             : transform a behaviour into stop,
 *                           using the same memory place
 *     SolvePredicate      : rewrite the predicate of a visible action or guard
 *     SolvePredicateBeh   : simplify a behaviour according to its predicate
 *     LookPredicate       : return the current predicate evaluation
 *     GateInPar           : say whether a gate is in a parallel operator
 *     GateInHide          : say whether a gate is in a hide operator
 *     JoinHides           : collapse two hide operators 
 *     SimplifyPredAndOL   : simplify the predicate and offer list of a gate
 *     GetGates            : set of visible gates of a behaviour
 *     GetTerminations     : list of visible terminations of a behaviour
 *     GetSuccessEvent     : return the descriptor of the success event gate
 *     GetTestProcess      : return the descriptor of the test process
 *     Compose_b_with_Test : composition of behaviour and test
 *
 *  LOG:
 *     20/07/92. dlarra. 
 *     Appended SimplifyPredAndOL.
 *
 ******************************************************************/


#ifndef balotosf_H
#define balotosf_H


#include "baattr.h"
#include "babeh.h"
#include "batables.h"


/* TrfStop
 * Transform the behaviour b into stop, using the same memory place.
 */
extern void TrfStop( /* b */ );
/* BehTyp b; */


/* SolvePredicate
 * Rewrite the predicate of a visible action or guard, if it exists.
 * SolvePredicate returns 't', 'f' or 'i' depending on the result.
 * If there is no predicate, return 'T'.
 * Guards have always predicates.
 */
extern char SolvePredicate( /* g */ );
/* BehTyp  g;  */


/* SolvePredicateBeh
 * Take as input an action prefix like g[e];B or a guarded behaviour [e]->B.
 * SolvePredicateBeh transforms those behaviours
 *  into stop                    if predicate e is false ,
 * or
 *  into g;B and B, respectively if e is true.
 * Leave the behaviour unchanged if the predicate is not true nor false.
 * The predicate is not rewritten, it must have already been rewritten.
 */
extern void SolvePredicateBeh( /* g */ );
/* BehTyp  g;  */


/* LookPredicate
 * Look at the predicate of the gate or guard b and returns 'i','f' or 't'
 * depending on the contents of the rewritten predicate :
 * undetermined, false or true respectively.
 */
extern char LookPredicate( /* b */ );
/* BehTyp b; */


/* GateInPar
 * Say whether gate g is in the gate set of the parallel operator b.
 */
extern boolean GateInPar( /* g, b */ );
/*  BehTyp       g, b;  */


/* GateInHide
 * Say whether gate g is in the gate set of the hide operator b.
 */
extern boolean GateInHide( /* g,b */ );
/*  BehTyp       g,b;  */


/* JoinHides
 * Transform :  hide GS1 in hide GS2 in B
 * into      :  hide GS1 U GS2 in B.
 */
extern BehTyp JoinHides( /* h1,h2 */ );
/*  BehTyp  h1,h2;  */


/* SimplifyPredAndOL
 * Simplify the predicate and offer list of a gate.
 *  Example :
 *
 *        g ?x1 ?x2 ?x3 ?x4 [ x1=v, x2=opn, x3=g(x4) , f(x1,x2,x3,x4) ] 
 *
 *    <=> g !v !opn ?x3 ?x4 [ x3=g(x4) , f(v,opn,x3,x4) ] 
 *
 *  These subtitutions are also done in the behaviour after the action.
 */
extern void SimplifyPredAndOL( /* g */ );
/*   BehTyp g; */


/* GetGates
 * Return a set with the visible gates of a behaviour.
 */
extern GateSetTyp GetGates( /* b */ );
/* BehTyp b;  */


/* GetTerminations
 * Return a list with the visible terminations of a behaviour.
 */
extern ListTyp GetTerminations( /* b */ );
/*     BehTyp b;  */


/* GetSuccessEvent
 * Return the descriptor of the success event gate.
 * If event success does not exist then return -1.
 * If event success is empty ("")  then return 0.
 */
extern DescriptorTyp GetSuccessEvent( /* success */ );
/*   char *success; */ 


/* GetTestProcess
 * Return the descriptor of a process.
 * If process does not exist or it has parameters then return -1.
 * If process is empty ("")                       then return  0.
 */
extern DescriptorTyp GetTestProcess( /* process */ );
/*   char *process; */ 


/* Compose_b_with_Test
 * Replace b by the parallel composition of the behaviour b and the
 * test process proc, synchronizing in all their gates but success_event.
 *  
 *         b[A1] |[A]| proc[A2,success_event],  where A = A1 + A2
 */
extern BehTyp Compose_b_with_Test( /* b, proc, success_event */ );
/* BehTyp        b;
   DescriptorTyp proc, success_event; */ 


#endif

