/**CHeaderFile*****************************************************************

  FileName    [amc.h]

  PackageName [amc]

  Synopsis    [Model Check using over(under)-approximation of the transition
  relation.]

  Description [The package implements the approximate_model_check command.
  The command is designed as a wrapper around the model_check command. 
  The command contains dual algorithms.  Predefined abstraction of the 
  transition relation is performed in a controlled way to ensure that the result 
  is reliable. By default, the command makes its effort to prove whether 
  the given ACTL formula is positive. User must set an environment variable 
  "amc_prove_false" when he/she wishes to prove whether the given ACTL formula 
  is negative.  When the formula is proven FALSE, then the error trace is 
  returned as in the model_check command. 
  Currently, one predefined approximation method, namely a "block-tearing"
  method, is implemented. The package manipulate the internal data structure
  of FSM to obtain over(under)-approximation of a given system. The algorithm
  begin with coarse approximation in which the degree of initial approximation
  is set by the user. Initial degree of approximation can be set by using 
  "amc_sizeof_group" environment. When the initial attempt using the coarse
  approximation fails, the algorithm automatically combine subsystems(take 
  synchronous product) to obtain refined approximations. The procedure is
  repeated until the approximation is good enough so that the result is 
  reliable. 
  ]


  Author      [Woohyuk Lee]

  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

  Revision    [$Id: amc.h,v 1.17 2002/09/08 23:15:15 fabio Exp $]

******************************************************************************/

#ifndef _AMC
#define _AMC

#include "part.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/**Enum************************************************************************

  Synopsis    [Methods for Approximation.]

  Description [Currently, only Amc_Block_c is used. Amc_Block_c method
  implements the abstraction method called "block tearing". The blocks of 
  subsystem is created by grouping the subset of vertices of the partition.
  Based on the initial grouping into blocks of subsystems, over(under)-
  approximation of the transition relation is created. The approximations of
  the transition relation is used to conservatively verify either true
  positive or true negative of a given ACTL formula.]

******************************************************************************/
typedef enum {
  Amc_Variable_c,
  Amc_Block_c,
  Amc_Default_c
} Amc_MethodType;

/**Enum************************************************************************

  Synopsis    [Verbosity Levels.]

******************************************************************************/
typedef enum {
  Amc_VerbosityNone_c,
  Amc_VerbositySpit_c,
  Amc_VerbosityVomit_c
} Amc_VerbosityLevel;

/**Enum************************************************************************

  Synopsis    [Quantification Mode.]

******************************************************************************/
typedef enum {
  Amc_PresentVars_c,
  Amc_NextVars_c,
  Amc_InputVars_c,
  Amc_User_c
} Amc_QuantificationMode;

/**Enum************************************************************************

  Synopsis    [Verification Results.]

******************************************************************************/
typedef enum {
  Amc_Verified_Unknown_c,
  Amc_Verified_True_c,
  Amc_Verified_False_c
} Amc_Verified_Answer;

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct AmcSubsystemInfo Amc_SubsystemInfo_t;
typedef struct AmcInfoStruct Amc_Info_t;

#include "mc.h"

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN void Amc_AmcEvaluateFormula(Ntk_Network_t *network, Ctlp_Formula_t *formula, int verbosity);
EXTERN Amc_Info_t * Amc_AmcInfoInitialize(Ntk_Network_t *network, Ctlp_Formula_t *formula, Amc_MethodType methodType, int verbosity);
EXTERN mdd_t * Amc_AmcExistentialQuantifySubsystem(Amc_SubsystemInfo_t *subSystem, array_t *quantifyVars, Amc_QuantificationMode quantificationMode);
EXTERN array_t * Amc_AmcExistentialQuantifySubsystemArray(array_t *subSystemArray, Amc_SubsystemInfo_t *currentSystem, array_t *quantifyVars, Amc_QuantificationMode quantificationMode);
EXTERN Fsm_Fsm_t * Amc_AmcSubsystemReadFsm(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetFsm(Amc_SubsystemInfo_t *system, Fsm_Fsm_t *info);
EXTERN array_t * Amc_AmcSubsystemReadRelationArray(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetRelationArray(Amc_SubsystemInfo_t *system, array_t *info);
EXTERN mdd_t * Amc_AmcSubsystemReadNextStateVarSmoothen(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetNextStateVarSmoothen(Amc_SubsystemInfo_t *system, mdd_t *info);
EXTERN mdd_t * Amc_AmcSubsystemReadSatisfy(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetSatisfy(Amc_SubsystemInfo_t *system, mdd_t *data);
EXTERN st_table * Amc_AmcSubsystemReadVertexTable(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetVertexTable(Amc_SubsystemInfo_t *system, st_table *data);
EXTERN st_table * Amc_AmcSubsystemReadFanInTable(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetFanInTable(Amc_SubsystemInfo_t *system, st_table *data);
EXTERN st_table * Amc_AmcSubsystemReadFanOutTable(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetFanOutTable(Amc_SubsystemInfo_t *system, st_table *data);
EXTERN char * Amc_AmcSubsystemReadMethodSpecificData(Amc_SubsystemInfo_t *system);
EXTERN void Amc_AmcSubsystemSetMethodSpecificData(Amc_SubsystemInfo_t *system, char *data);
EXTERN mdd_t * Amc_AmcReadInitialStates(Amc_Info_t *system);
EXTERN void Amc_AmcSetInitialStates(Amc_Info_t *system, mdd_t *data);
EXTERN Amc_SubsystemInfo_t * Amc_AmcReadOptimalSystem(Amc_Info_t *system);
EXTERN void Amc_AmcSetOptimalSystem(Amc_Info_t *system, Amc_SubsystemInfo_t *data);
EXTERN void * Amc_AmcReadMethodData(Amc_Info_t *system);
EXTERN void Amc_AmcSetMethodData(Amc_Info_t *system, void *data);
EXTERN Amc_SubsystemInfo_t * Amc_AmcSubsystemAllocate(void);
EXTERN Amc_SubsystemInfo_t * Amc_AmcSubsystemCreate(Fsm_Fsm_t *fsm, mdd_t *satisfyStates, st_table *vertexTable, st_table *fanInTable, st_table *fanOutTable);
EXTERN Amc_SubsystemInfo_t * Amc_AmcSubsystemDuplicate(Ntk_Network_t *network, Amc_SubsystemInfo_t *subSystem);
EXTERN void Amc_AmcSubsystemFree(Amc_SubsystemInfo_t *subSystem);
EXTERN void Amc_AmcSubsystemFreeAlsoPartition(Amc_SubsystemInfo_t *subSystem);
EXTERN Amc_SubsystemInfo_t * Amc_CombineSubsystems(Ntk_Network_t *network, Amc_SubsystemInfo_t *subSystem1, Amc_SubsystemInfo_t *subSystem2);
EXTERN Img_ImageInfo_t * Amc_AmcReadOrCreateImageInfo(Fsm_Fsm_t *fsm);
EXTERN mdd_t * Amc_AmcEvaluateCTLFormula(Amc_SubsystemInfo_t *subSystem, array_t *subSystemArray, Ctlp_Formula_t *ctlFormula, mdd_t *fairStates, Fsm_Fairness_t *fairCondition, mdd_t *modelCareStates, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN mdd_t * Amc_AmcEvaluateEXFormula(Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *targetMdd, mdd_t *fairStates, mdd_t *careStates, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN mdd_t * Amc_AmcEvaluateEUFormula(Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *invariantMdd, mdd_t *targetMdd, mdd_t *fairStates, mdd_t *careStates, array_t *onionRings, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN mdd_t * Amc_AmcEvaluateEGFormula(Fsm_Fsm_t *modelFsm, array_t *subSystemArray, Amc_SubsystemInfo_t *subSystem, mdd_t *invariantMdd, mdd_t *fairStates, Fsm_Fairness_t *modelFairness, mdd_t *careStates, array_t *onionRingsArrayForDbg, boolean lowerBound, array_t *quantifyVars, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
EXTERN void Amc_Init(void);
EXTERN void Amc_End(void);

/**AutomaticEnd***************************************************************/

#endif /* _AMC */