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

/***********************************
  
  Santiago Pavon Gomez
  
  22 January 1991
  
  Expansion functions
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  SDEBUG : activate debugging mode
  
  TYPE DEFINITIONS:
  
  FUNCTION DEFINITIONS:
  NameDupProc : new name for a new duplicated process
  FreeExpand : free expansion
  StepExpand : show next offered transitions (and let the user choose one)
  Expand : expansion with duplicate behaviour detection
  VarExpand :  parameterized expansion with duplicate behaviour detection
  TestExpand : test expansion
  OneExpand : random symbolic execution
  
  
  ************************************/


#ifndef EXexpansion_H
#define EXexpansion_H

#include "babeh.h"


#define REJECT     1
#define MAY        2
#define MUST       3



/* NameDupProc
 * returns a new name for a new duplicated process.
 */
extern char * NameDupProc();


/* FreeExpand
 * Free expansion of b until depth.
 */
extern void FreeExpand( /* b, d, verbose, i_remove */ );
/*  BehTyp b;
    int    d; 
    boolean verbose, i_remove; */


/* StepExpand
 * Free expansion of b of depth 1.
 * debug_info is TRUE if debugging information is computed.
 */
extern BehTyp StepExpand( /* b, debug_info */ );
/*  BehTyp b; 
    boolean debug_info; */


/* Expand
 * Expansion of b until depth.
 */
extern void Expand( /* b, d, verbose, i_remove */ );
/*  BehTyp b;
    int    d; 
    boolean verbose, i_remove; */


/* VarExpand
 * Parameterized Expansion of b until depth.
 */
extern void VarExpand( /* b, d, verbose, i_remove */ );
/*  BehTyp b;
    int    d; 
    boolean verbose, i_remove; */


/* TestExpand
 * Test Expansion of b.
 * d is the depth of the exploration.
 * se is the name of the sucess event.
 * opta, optd, opte and opts are output control options.
 * proc is the name of the test process.
 * mayc forces MAY tests to be thoroughly tested.
 * i_removal removes some redundant internal actions.
 * wbcontext says whether b is in a context suitable for i-removal.
 * x_resp is the expected test response ( MUST,MAY,REJECT or UNDEFINED ).
 * optq flag forces LOLA to quit on unexpected response.
 */
extern void TestExpand(/* b,d,se,opta,optd,opte,opts,proc,verbose,mayc,
			  i_removal,wbcontext,
                          x_resp, optq,
			  percentage, seed, bhsize */);
/*     BehTyp        b;
       int           d; 
       DescriptorTyp se;
       boolean opta, optd, opte, opts, verbose,mayc,i_removal,wbcontext,optq;
       DescriptorTyp proc;
       int           x_resp, percentage, seed, bhsize;
       */



/* OneExpand
 * One Expansion of b.
 * d is the depth of the exploration.
 * se is the name of an optional termination event.
 * proc is the name of the test process.
 *
 * return the next random value
 */
extern int OneExpand( /* b, d, se, proc, seed, verbose, i_remove */ );
/*  BehTyp b;
    int    d,seed; 
    DescriptorTyp se, proc;
    boolean verbose, i_remove; */



/* InterExpand
 * Interleaved Expansion of b.
 * d is the depth of the exploration.
 * se is the name of the sucess event.
 * proc is the name of the test process.
 */
extern void InterExpand( /* b, d, se, proc, dup, param, verbose */ );
/*     BehTyp        b;
       int           d; 
       DescriptorTyp se,proc;
       boolean       dup, param, verbose;
       */


#endif



