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

/***********************************
  
  Maria Hultstrom
  
  10-9-1991
  
  Checks if a specification diverges or is unguarded.
  
  COMPILATION OPTIONS: The behaviour of this module can be modified
  by the following compilation flags:
  
  TYPE DEFINITIONS:
  
  FUNCTION DEFINITIONS:
  InitDiver : initializes this module
  Expandable : checks whether a specification and processes are expandable
  
  ************************************/

#ifndef exdiver_H
#define exdiver_H


/* InitDiver
 * Initializes this module.
 * This function must be called when a new specification is loaded.
 */
extern void InitDiver();


/* Expandable
 * Checks if the processes of the specification are possible to expand,
 * i.e. they do not diverge nor are unguarded. 
 * If the specification is not expandable then this function will inform
 * the user why not.
 * divergence  : divergence analysis check 
 * unguardance : unuarded process detection
 */
extern void Expandable(/* divergence, unguardance */);
/*       boolean divergence, unguardance; */


/* IsUnguardedProc
 * Says if a process p is unguarded
 */
extern boolean IsUnguardedProc( /* p */ );
/* DescriptorTyp p; */


/* UngProcBefAct
 * Returns TRUE if in the behaviour "b" there are any instantiation to
 * an unguarded process.
 * This exploration ends in the actions.
 */
extern boolean UngProcBefAct( /* b */ );
/* BehTyp b; */

#endif
