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

  FileName    [amcInt.h]

  PackageName [amc]

  Synopsis    [Internal data type definitions and macros to handle the
  structures of the amc package.]

  Author      [Woohyuk Lee <woohyuk@duke.colorado.edu>]

  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: amcInt.h,v 1.23 2002/09/08 02:10:46 fabio Exp $]

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

#ifndef _AMCINT
#define _AMCINT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
/* #include <unistd.h> */
#include "amc.h"
#include <string.h>


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

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef int (*AmcCallBackProc)  ARGS((Amc_Info_t *, Ctlp_Formula_t *, int));
typedef void (*AmcFreeProc) ARGS((Amc_Info_t *));


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

  Synopsis    [Information regarding a subsystem.]

  Description [Each field represents information associated with a subsystem.]

  SeeAlso     [AmcInfoStruct]

******************************************************************************/
struct AmcSubsystemInfo{
  Fsm_Fsm_t	*fsm;		       /* Sub-Fsm of this subsystem */
  array_t	*relationArray;        /* Array of MDD representation of the 
					  transition relation */
  mdd_t		*nextStateVarSmoothen; /* Transition relation of subsystems
					  with next state variables existentially
 					  quantified */
  mdd_t		*satisfyStates;        /* Sub(Super)-set of states satisfying 
					  given formula */
  st_table 	*vertexTable;          /* Vertices in the subsystem */
  st_table	*fanInTable;           /* */
  st_table	*fanOutTable;          /* */
  int		takenIntoOptimal;      /* If 1, the subsystem is part of the system */
  char		*methodSpecificData;   /* May be used to store method specific data */
};


/**Struct**********************************************************************

  Synopsis    [Information regarding the amc package.]

  Description [This is a higher level of information related to the amc package.]

  SeeAlso     [AmcSubsystemInfo]

******************************************************************************/
struct AmcInfoStruct{
  Ntk_Network_t		*network;	 /* Corresponding network */
  Amc_MethodType	methodType;	 /* Approximation method type */
  void                  *methodData;     /* Method-dependent data structure */

  array_t		*subSystemArray; /* Array of AmcSubsystemInfo *  */
  Amc_SubsystemInfo_t 	*optimalSystem;  /* */
  mdd_t			*initialStates;  /* */
  AmcCallBackProc	amcBoundProc;    /* Function using upper bound approximation */ 
  AmcFreeProc		amcFreeProc;	 /* Function to free method-specific data structure */
  int			isVerified;	 /* isVerified=1  whenever formula is verified */
  Amc_Verified_Answer   amcAnswer;       /* {Unknown, True, False} */
  int			isMBM;		 /* isMBM=1 when Machine by Machine method is applied */
  int			groupingMethod;  /* */
  boolean		lowerBound;      /* lowerBound=1 when lower bound approximation is used */
  int                   currentLevel;    /* Current lattice approximation level */  
};


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


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

#define AmcSubsystemReadFsm(system) \
  (system)->fsm

#define AmcSubsystemSetFsm(system, data) \
  (system)->fsm = (data)


#define AmcSubsystemReadRelationArray(system) \
  (system)->relationArray

#define AmcSubsystemSetRelationArray(system, data) \
  (system)->relationArray = (data)


#define AmcSubsystemReadNextStateVarSmoothen(system) \
  (system)->nextStateVarSmoothen

#define AmcSubsystemSetNextStateVarSmoothen(system, data) \
  (system)->nextStateVarSmoothen = (data)


#define AmcSubsystemReadSatisfy(system) \
  (system)->satisfyStates

#define AmcSubsystemSetSatisfy(system, data) \
  (system)->satisfyStates = (data)


#define AmcSubsystemReadVertexTable(system) \
  (system)->vertexTable

#define AmcSubsystemSetVertexTable(system, data) \
  (system)->vertexTable = (data)


#define AmcSubsystemReadFanInTable(system) \
  (system)->fanInTable

#define AmcSubsystemSetFanInTable(system, data) \
  (system)->fanInTable = (data)


#define AmcSubsystemReadFanOutTable(system) \
  (system)->fanOutTable

#define AmcSubsystemSetFanOutTable(system, data) \
  (system)->fanOutTable = (data)


#define AmcSubsystemReadMethodSpecificData(system) \
  (system)->methodSpecificData

#define AmcSubsystemSetMethodSpecificData(system, data) \
  (system)->methodSpecificData = (char *) (data)


#define AmcReadInitialStates(system) \
  (system)->initialStates

#define AmcSetInitialStates(system, data) \
  (system)->initialStates = (data)


#define AmcReadOptimalSystem(system) \
  (system)->optimalSystem

#define AmcSetOptimalSystem(system, data) \
  (system)->optimalSystem = (data)


#define AmcReadMethodData(system) \
  (system)->methodData

#define AmcSetMethodData(system, data) \
  (system)->methodData = (data)




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

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

EXTERN array_t	* AmcCreateSubsystemArray(Ntk_Network_t *network, Ctlp_Formula_t *formulA);
EXTERN void AmcPrintOptimalSystem(FILE *fp, Amc_Info_t *amcInfo);
EXTERN void AmcCheckSupportAndOutputFunctions(array_t *subSystemArray);
EXTERN st_table * AmcCreateFunctionSupportTable(Mvf_Function_t *mvf);
EXTERN mdd_t * AmcModelCheckAtomicFormula(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula);
EXTERN int AmcBlockTearingProc(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, int verbosity);
EXTERN void AmcFreeBlock(Amc_Info_t *amcInfo);
EXTERN boolean FormulaTestIsForallQuantifier(Ctlp_Formula_t *formula);

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

#endif /* _AMCINT */