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

  FileName    [ltl.h]

  PackageName [ltl]

  Synopsis    [Internal declarations.]

  Author      [Chao Wang<chao.wang@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: ltl.h,v 1.19 2005/04/30 04:00:25 fabio Exp $]

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

#ifndef _LTL
#define _LTL

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "vm.h"
#include "ctlsp.h"
#include "hrc.h"
#include "ntk.h"
#include "fsm.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
/*define DEBUG_LTLMC */

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


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct LtlAutomatonStruct Ltl_Automaton_t;
typedef struct LtlAutomatonNodeStruct Ltl_AutomatonNode_t;


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


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


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

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

EXTERN void Ltl_Init(void);
EXTERN void Ltl_End(void);
EXTERN Ltl_Automaton_t * Ltl_McFormulaToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *Formula, int options_algorithm, int options_rewriting, int options_prunefair, int options_iocompatible, int options_directsim, int options_reversesim, int options_directsimMaximize, int options_verbosity, int checkSemantics);
EXTERN Hrc_Manager_t * Ltl_McAutomatonToNetwork(Ntk_Network_t *designNetwork, Ltl_Automaton_t *automaton, int verbosity);
EXTERN boolean Ltl_FormulaStaticSemanticCheckOnNetwork(Ctlsp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
EXTERN Ltl_Automaton_t * Ltl_AutomatonCreate(void);
EXTERN void Ltl_AutomatonFree(gGeneric g);
EXTERN Ltl_AutomatonNode_t * Ltl_AutomatonNodeCreate(Ltl_Automaton_t *aut);
EXTERN void Ltl_AutomatonNodeFree(gGeneric g);
EXTERN void Ltl_AutomatonNodePrint(Ltl_Automaton_t *aut, Ltl_AutomatonNode_t *node);
EXTERN void Ltl_AutomatonPrint(Ltl_Automaton_t *aut, int verbosity);
EXTERN void Ltl_AutomatonToDot(FILE *fp, Ltl_Automaton_t *aut, int level);
EXTERN int Ltl_AutomatonToBlifMv(FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A);
EXTERN int Ltl_AutomatonToVerilog(FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A);
EXTERN int Ltl_AutomatonToSmv(FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A);
EXTERN int Ltl_AutomatonMinimizeByIOCompatible(Ltl_Automaton_t *A, int verbosity);
EXTERN int Ltl_AutomatonMinimizeByDirectSimulation(Ltl_Automaton_t *A, int verbosity);
EXTERN void Ltl_AutomatonAddFairStates(Ltl_Automaton_t *A);
EXTERN int Ltl_AutomatonMaximizeByDirectSimulation(Ltl_Automaton_t *A, int verbosity);
EXTERN int Ltl_AutomatonMinimizeByReverseSimulation(Ltl_Automaton_t *A, int verbosity);
EXTERN int Ltl_AutomatonMinimizeByPrune(Ltl_Automaton_t *A, int verbosity);
EXTERN void Ltl_AutomatonComputeSCC(Ltl_Automaton_t *A, int force);
EXTERN int Ltl_AutomatonIsWeak(Ltl_Automaton_t *A);
EXTERN Mc_AutStrength_t Ltl_AutomatonGetStrength(Ltl_Automaton_t *A);
EXTERN Ltl_Automaton_t * Ltl_AutomatonCreateQuotient(Ltl_Automaton_t *A, st_table *partition);
EXTERN int Ltl_AutomatonVtxGetNodeIdx(vertex_t *v);

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

#endif /* _LTL */