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

/***********************************
  
  Santiago Pavon Gomez
  
  13/09/1993
  
  Module to keep track of which is the success event in any point of a
  behaviour.
  
  During the test-expansion process, LOLA applies some rules to remove
  internal action (expansion of the parallel operator) in order to reduce the
  number of state to explore.
  
  For example     i;B1 [] i;B2 |[A]| a;B3  
  is expanded to  i;(B1 |[A]| a;B3) [] i;(B2 |[A]| a;B3) 
  
  The third branch (a;(i;B1 [] i;B2 |[A]| B3)) has been removed because
  the testing equivalence relation is maintained.
  
  The problem is that if "a" is the success event, then we are delaying the
  ocurrence of this event and we will explore more states than necessary.
  
  This module maintains an internal stack with the success event actions in
  order to not apply the optimization rules when the success event is offered.
  Note that the success event is a gate set because different gates can be
  relabelled to the success event.
  
  Then the expansion is modified to apply this rule:
  
  (B1 [] choice x:t [] ok;B) |[A]| B2
  
  is transformed into
  
  choice x:t [] ok;stop
  
  where the choice is optional.
  
  Three functions must be called to update the success event set
  when we find a relabel, a parallel or a hide operator:
  
  - HIDE:     The gates of the success event set belonging to the hide set
              must be not considered below the hide operator.
  - RELABEL:  The gates of the success event set must be relabeled to know
              what is the new success event set below the relab operator.
  - PARALLEL: The synchronization gates are removed from the success
              event set. Perhaps, the parallel operator must do any
              synchronization to be able to produce the success event.
  - GENERALIZED PAR: Don't worry. It is transformed into a normal 
              parallel operator.
  
  ************************************/


#ifndef EXsucces_H
#define EXsucces_H

#include "babeh.h"

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

/* InitSuccessStack
 * Init the internal stack with the gate set { g }.
 * If "g" is zero, then it is initialized with NULL.
 */ 
extern void InitSuccessStack( /* g */ );
/* DescriptorTyp g; */

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

/* PopSuccessStack
 * Pop the last element on the stack
 */
extern void PopSuccessStack();

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

/* RelabUpdateSuccessStack
 * Calculate what is the new success event set after the relabel function
 * "rfl", and store it in the internal stack.
 */
extern void RelabUpdateSuccessStack( /* rfl */ );
/* RelabFuncListTyp rfl; */

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

/* HideUpdateSuccessStack
 * Calculate what is the new success event set after the hide operator
 * whose gate set is hgs, and store it in the internal stack.
 */
extern void HideUpdateSuccessStack( /* hgs */ );
/* GateSetTyp hgs; */

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

/* ParUpdateSuccessStack 
 * Calculate what is the new success event set after the parallel operator
 * pointed by b, and store it in the internal stack.
 */
extern void ParUpdateSuccessStack( /* b */ );
/* BehTyp b; */

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

/* Par_to_Success
 * If the parallel operator b offers the success event, then
 * b is glued by that success event anf TRUE is returned.
 */ 
extern boolean Par_to_Success( /* b */ );
/* BehTyp b; */

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

#endif

