/***********************************
  (C) Copyright 1990, 1991; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************
  $Log:  itintexp.h,v $
  * 
  ***********************************/

/***********************************
  
  Santiago Pavon Gomez
  David Larrabeiti Lopez
  
  Dec 18, 1992
  
  Optimized Interleaved Expansion.
  
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  (none)
  
  TYPE DEFINITIONS:
  
  FUNCTION DEFINITIONS:
  
  ************************************/


#ifndef ITintexp_H
#define ITintexp_H


#include "babeh.h"


/* InitIT
 * Initialization of the interface InTerleaved
 */
extern void InitIT();

/* 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; */




/* InterleavedExpansion
 * Returns the interleaved expansion of the behaviour b.
 * The exploration stops after a depth d of synchronizations or when
 * the success event se is offered by the continuation.
 * If dup (or param), the explorations also stops when a duplicate state
 * (or a parameterized duplicated state) is found.
 */
extern BehTyp InterleavedExpansion(/* b, d, se, proc, dup, param */);
/*     BehTyp        b;
       int           d;
       DescriptorTyp se,proc;
       boolean       dup, param; */


#endif

