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

/***********************************
  
  Santiago Pavon Gomez
  
  8 February 1991
  
  Pre_branch
  This module contains the implementation
  of the Theorem of Expansion.
  Each function provides the expansion
  of a LOTOS operator.
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  (none)
  
  TYPE DEFINITIONS:
  (none)
  
  FUNCTION DEFINITIONS:
  InitEX : Initialization of the interface EXpansion
  Pre_Branch : return an equivalent one-immediate behaviour
  Pre_Branch_Stop : remove stop alternatives
  Pre_Branch_Choice : distribute a value choice over a behaviour choice
  Pre_Branch_Alt : flatten a two-level nested alternatives
  Pre_Branch_Guard : distribute a guard over a behaviour choice
  Pre_Processing : expand a non-immediate LOTOS operator
  Pre_Branch_2 : convert into an equivalent one-immediate behaviour
  (with shared expansion )
  Pre_Branch_Stop_2 : remove stop alternatives  (with shared expansion )
  Pre_Branch_Choice_2 : distribute a value choice over a behaviour choice
  (with shared expansion )
  Pre_Branch_Alt_2 : flatten a two-level nested alternatives
  (with shared expansion)
  Pre_Branch_Guard_2 : distribute a guard over a behaviour choice
  (with shared expansion)
  Pre_Processing_2 : expand a non-immediate LOTOS operator
  (with shared expansion)
  Disabling_Expand : expand B1 [> B2 where B1 is one-immediate
  Enabling_Expand :  expand B1 >> B2 where B1 is one-immediate
  Hide_Expand : expand hide g1,...,gn in B
  Inst_Processing : expand process_instantiation[g1,...,gn](v1,...,vm)
  Let_Processing : expand let v1:s1,...,vn:sn in B
  Plet_Processing : expand plet v1:s1,...,vn:sn in B
  Par_Expand : expand B1 |[g1,...,gn]| B2 where B1 & B2 are one-immediate
  Relabel_Expand : expand relabeling [ a1/f1, ..., an/fn ] in B
  Par_Expr_Processing : expand par g1,..,gn in [ h1,...,hm ] |[A]| B
  Sum_Expr_Processing : expand choice g1,..,gn in [ h1,...,hm ] [] B
  IT_Processing : expand IT( B1, B2, Vij(Bij) )
  
  GLOBAL VARIABLES:
  expansion_flags: type of expansion. This variable is the
  reference to know what kind of state exploration 
  is being performed, determines the way in which 
  process instantiations have to be expanded
  (symbolically or not), if the expansion is done 
  over the bahviour (in the same place) and the 
  internal action will be removes according to weak 
  observational equivalence.
  
  ************************************/


#ifndef EXpre_branch_H
#define EXpre_branch_H


#include "babeh.h"


/* expansion_flags
 *
 * These flags indicate the type of expansion to make.
 *
 *    DUPLICATE_EXP     : Duplicate state detection.
 *    PARAMETERIZED_EXP : Parameterized expansion.
 *    SHARED_EXP        : Shared Expansion.
 *    WEAK_EQUIV_EXP    : i removal during expansion.
 *    STEP_EXP          : Step_by_Step Expansion.
 *    NOT_PRE_PROC_EXP  : do not leave pre_processed operands under actions
 *    TEST_EQUIV_EXP    : Expansion maintains Testing Equivalence relation.
 *
 *
 * The flag SHARED_EXP is incompatible with TEST_EQUIV_EXP, 
 * DUPLICATE_EXP and PARAMETERIZED_EXP. 
 *
 * The flag TEST_EQUIV_EXP must be always specified with WEAK_EQUIV_EXP.
 *
 */

extern int expansion_flags;

#define DUPLICATE_EXP     1
#define PARAMETERIZED_EXP 2
#define SHARED_EXP        4
#define WEAK_EQUIV_EXP    8
#define STEP_EXP         16
#define NOT_PRE_PROC_EXP 32
#define TEST_EQUIV_EXP   64
#define INTERLEAVED_EXP 128
#define ENABLE_FES_EXP  256

#define IS_DUPLICATE_EXP      ((expansion_flags & DUPLICATE_EXP)     !=0)
#define IS_PARAMETERIZED_EXP  ((expansion_flags & PARAMETERIZED_EXP) !=0)
#define IS_SHARED_EXP         ((expansion_flags & SHARED_EXP)        !=0)
#define IS_WEAK_EQUIV_EXP     ((expansion_flags & WEAK_EQUIV_EXP)    !=0)
#define IS_STEP_EXP           ((expansion_flags & STEP_EXP)          !=0)
#define IS_NOT_PRE_PROC_EXP   ((expansion_flags & NOT_PRE_PROC_EXP)  !=0)
#define IS_TEST_EQUIV_EXP     ((expansion_flags & TEST_EQUIV_EXP)    !=0)
#define IS_INTERLEAVED_EXP    ((expansion_flags & INTERLEAVED_EXP)   !=0)
#define IS_ENABLE_FES_EXP     ((expansion_flags & ENABLE_FES_EXP)    !=0)

/*
   Maximum depth for recursive Pre_Branch's on i-removal
   */
#define MAXDEPTH_I_RMV 5

/*
   number of states to be stored at each call to Filter_i in order to
   detect a loop of internal actions.
   
   notice that :
   the effective i-removal depth for a Pre_Branch is :
   
   MAX_ICANCEL x MAXDEPTH_I_RMV
   */
#define MAX_ICANCEL 2



/******************************************************************
 *                                                                *
 *     Pre_Branch                                                 *
 *                                                                *
 *     Original function for one level expansion                  *
 *     The behaviour is unshared until actions and                *
 *     then transformed                                           *
 *                                                                *
 *******************************************************************/


/* InitEX
 * Initialization of the interface EXpansion
 */
extern void InitEX();


/* Pre_Branch
 * Transforms behaviour b into a 1_immediate behaviour.
 * If *i_rm_depth > 0 then apply Weak Bisimulation Congruence.
 */
extern BehTyp Pre_Branch( /* b, i_rm_depth */ );
/* BehTyp b;
   int    *i_rm_depth */

/* Pre_Branch_Stop
 * Transforms ...[]B1[]stop[]B2[]... into ...[]B1[]B2...
 */
extern BehTyp Pre_Branch_Stop( /* b */ );
/* BehTyp b; */

/* Pre_Branch_Choice
 * Distribute a value choice into a behaviour choice.
 * choice v:s [] ( B1[]B2 ) = (choice v:s [] B1) [] (choice v:s [] B2)
 */
extern BehTyp Pre_Branch_Choice(/* b */);
/* BehTyp b; */

/* Pre_Branch_Alt
 * Flatten a 2-level alternative tree.
 * b1 [] ( b2 [] b3) [] b4 = b1 [] b2 [] b3 [] b4
 */
extern BehTyp Pre_Branch_Alt(/* b */);
/*     BehTyp b; */

/* Pre_Branch_Guard
 * Distribute a guard into a behaviour choice
 * [ BE ]-> ( B1[]B2 ) = ([ BE ]-> B1) [] ([ BE ]-> B2)
 */
extern BehTyp Pre_Branch_Guard(/* b */);
/*       BehTyp b; */

/* Pre_Processing
 * Pre_Processing of a non-immediate behaviour.
 * Returns a behaviour such that its first operator is either
 * alternative, choice, guard, gate, i, stop or exit.
 */
extern BehTyp Pre_Processing( /* b */ );
/*  BehTyp b; */


/******************************************************************
 *                                                                *
 *     Pre_Branch_2                                               *
 *                                                                *
 *     Function for one level expansion IN SITU                   *
 *     The behaviour is pre_processed before unsharing, then      *
 *     is unshared until actions and finally gets transformed     *
 *                                                                *
 ******************************************************************/

/* Pre_Branch_2
 * Transforms behaviour b into a 1_immediate behaviour.
 * If *i_rm_depth>0 then apply Weak Bisimulation Congruence.
 */
extern void Pre_Branch_2( /* b, i_rm_depth */ );
/* BehTyp b;
   int *i_rm_depth */


/* Pre_Branch_Stop_2
 * Transforms ...[]B1[]stop[]B2[]... into ...[]B1[]B2...
 */
extern void Pre_Branch_Stop_2( /* b */ );
/* BehTyp b; */


/* Pre_Branch_Choice_2
 * Distribute a value choice into a behaviour choice.
 * choice v:s [] ( B1[]B2 ) = (choice v:s [] B1) [] (choice v:s [] B2)
 */
extern void Pre_Branch_Choice_2(/* b */);
/* BehTyp b; */


/* Pre_Branch_Alt_2
 * Flatten a 2-level alternative tree.
 * b1 [] ( b2 [] b3) [] b4 = b1 [] b2 [] b3 [] b4
 */
extern void Pre_Branch_Alt_2(/* b */);
/*     BehTyp b; */


/* Pre_Branch_Guard_2
 * Distribute a guard into a behaviour choice
 * [ BE ]-> ( B1[]B2 ) = ([ BE ]-> B1) [] ([ BE ]-> B2)
 */
extern void Pre_Branch_Guard_2(/* b */);
/*       BehTyp b; */


/* Pre_Processing_2
 * Pre_Processing of a non-immediate behaviour.
 * Returns a behaviour such that its first operator is either
 * alternative, choice, guard, gate, i, stop or exit.
 */
extern void Pre_Processing_2( /* b */ );
/*  BehTyp b; */



/******************************************************************
 *                                                                *
 *             LOTOS Operators Expansion Functions                *
 *                                                                *
 *******************************************************************/


/* Disabling_Expand
 * Expansion of a Disabling operator b.
 *
 *      b = b1 [> b2
 *
 * where b1 is a one-immediate behaviour.
 */
extern BehTyp Disabling_Expand( /* b */ );
/* BehTyp b;*/


/* Enabling_Expand
 * Expansion of an Enabling operator b.
 *
 *      b = b1 >> b2
 *
 * where b1 is a one-immediate behaviour.
 */
extern BehTyp Enabling_Expand( /* b */ );
/* BehTyp b;*/


/* Hide_Expand
 * Processing of the Hiding operator hide.
 *
 *     hide = hide GSet in b
 *
 * where b is any behaviour.
 */
extern BehTyp Hide_Expand( /* hide */ );
/* BehTyp hide;*/


/* Inst_Processing
 * Returns the process instantiation defined by the ProcessInstC procInst.
 * It consists of :
 *                  RelabellingC * Only if the actual gatelist of the instCell
 *                       |         is different from the formal defCell's gl.
 *                       |
 *                     PLetC     * Always, although the VAL is empty .
 *                       |         Its content depend on expansion_flags .
 *                       |
 *                       B
 *            (shared with ProcessDefC)
 */
extern BehTyp Inst_Processing( /* procInst */ );
/* BehTyp procInst; */


/* Let_Processing
 * Processing of the Let operator let.
 *
 *      let = Let v1:s1=E1,...,vn:sn=En in b
 *
 * where b is any behaviour.
 */
extern BehTyp Let_Processing(/* let */);
/* BehTyp let;*/


/* Plet_Processing
 * Processing of the PLet operator plet.
 *
 *      plet = Plet v1:s1=E1,...,vn:sn=En in b
 *
 * where b is any behaviour.
 */
extern BehTyp Plet_Processing( /* plet */ );
/* BehTyp plet; */


/* Par_Expand
 * Expansion of a parallel behaviour b.
 * Both arguments of b must be 1-immediate .That's to say:
 * 
 *       Mxi                           Mxj
 *  b= ( SUMi( CHi Gi gi;Bi ) |[GSet]| SUMj( CHj Gj gj;Bj ) )
 *        1                             1
 *
 * where:
 *
 *   gk:= visible-action | i-action | exit        (Mxk>1)
 *   gk:= visible-action | i-action | exit | stop (Mxk=1)
 *
 *
 * This function is called with the following parameters:
 *
 *    Par_Expand( Exp(B1)|[A]|Exp(B2), B1, B2, rmI1 , rmI2 )
 *
 * where:
 * 
 *  B1 and B2 are the arguments of the parallel operator before
 *  being pre_processed. They are used when a behaviour with IT
 *  operator is expanded. Example:
 * 
 *      If ( IS_NOT_PRE_PROC_EXP ) then
 *         if Exp(B1)=g;B1', g not in A then
 *             Par_Expand( Exp(B1)|[A]|Exp(B2), B1, B2 ) = g;(B1'|A|B2)
 *
 *  rmI1 and rmI2 indicates that the first or the second argument of
 *  "b" only offer internal actions, such that the visible actions of 
 *  the other branch can be delayed. (ONLY FOR TESTING).
 */          
extern BehTyp Par_Expand( /* b , b1, b2, rmI1 , rmI2 */ );
/* BehTyp b,b1,b2;
   boolean rmI1, rmI2; */


/* Relabel_Expand
 * Processing of the Relabel operator relab.
 *
 *     relab = relab rfl in b
 *
 * where b is any behaviour.
 */
extern BehTyp Relabel_Expand( /* relab */ );
/* BehTyp relab;*/


/* Par_Expr_Processing
 * Expands any extended parallel.
 */
extern BehTyp Par_Expr_Processing( /* b */ );
/* BehTyp b */


/* Sum_Expr_Processing
 * Expands any gate-choice.
 */
extern BehTyp Sum_Expr_Processing( /* b */ );
/* BehTyp b; */


/* IT_Processing
 * Extract the first actions that an IT can offer
 */
extern BehTyp IT_Processing( /* b */ );
/*     BehTyp b; */


/******************************************************************
 *
 *  Unsuccessful synchronizations (STEP-BY-STEP mode) of the last
 *  state expanded. 
 *
 *******************************************************************/

/* GetRefusedSync
 * Return the unsuccessful synchronizations stored in "refusedSynchr"
 * and set this variable to NULL.
 */
extern BehTyp GetRefusedSync();

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

/******************************************************************
 *
 * Testing after Iexpansion ( to be moved up )
 *
 *******************************************************************/

/* IT_Testing
 */
extern void IT_Testing(/* b, success_event, proc, verb */);
/*     BehTyp        b;
       DescriptorTyp success_event, proc;
       boolean       verb;
       */

/******************************************************************
 *                                                                *
 *    Interleaved Expansion Preprocessing                         *
 *                                                                *
 *    The Interleaved expansion needs a especial preprocessing    *
 *    that leaves the sub-state in an unexpanded canonical form.  *
 *    The following functions are involved in this task.          *
 *                                                                *
 ******************************************************************/

/* Distribute_Choice
 * Distribute a value choice into a behaviour choice ( alternative )
 * just after the guards.
 * choice v:s [] ( B1[]B2 ) = (choice v:s [] B1) [] (choice v:s [] B2)
 */
extern BehTyp Distribute_Choice(/* b */);
/*     BehTyp b; */


/* Distribute_Guard
 * Distribute a guard into a behaviour choice ( alternative )
 * [ BE ]-> ( B1[]B2 ) = ([ BE ]-> B1) [] ([ BE ]-> B2)
 */
extern BehTyp Distribute_Guard(/* b */);
/*     BehTyp b; */


/* Iexp_Hide_Proc
 */
extern BehTyp Iexp_Hide_Proc(/* hide */);
/*     BehTyp hide; */


/* Iexp_Relabel_Proc
 * Processing of the Relabel operator relab.
 *
 *     relab = relab rfl in b
 *
 * where b is Iexp_Pre_Processed
 */
extern BehTyp Iexp_Relabel_Proc(/* relab */);
/*     BehTyp relab; */


/* Iexp_Pre_Proc
 * Pre-processing previous to the application of the iexpansion at every
 * sub-state of the exploration.
 * b must be got-until-actions.
 * return the canonical representation of the state.
 */
extern BehTyp Iexp_Pre_Proc(/* b */);
/*     BehTyp b; */


#endif



