source: vis_dev/vis-2.3/src/ltl/ltl.h @ 14

Last change on this file since 14 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 4.8 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [ltl.h]
4
5  PackageName [ltl]
6
7  Synopsis    [Internal declarations.]
8
9  Author      [Chao Wang<chao.wang@colorado.EDU>]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15  Revision    [$Id: ltl.h,v 1.19 2005/04/30 04:00:25 fabio Exp $]
16
17******************************************************************************/
18
19#ifndef _LTL
20#define _LTL
21
22/*---------------------------------------------------------------------------*/
23/* Nested includes                                                           */
24/*---------------------------------------------------------------------------*/
25#include "vm.h"
26#include "ctlsp.h"
27#include "hrc.h"
28#include "ntk.h"
29#include "fsm.h"
30/*---------------------------------------------------------------------------*/
31/* Constant declarations                                                     */
32/*---------------------------------------------------------------------------*/
33/*define DEBUG_LTLMC */
34
35/*---------------------------------------------------------------------------*/
36/* Structure declarations                                                    */
37/*---------------------------------------------------------------------------*/
38
39
40/*---------------------------------------------------------------------------*/
41/* Type declarations                                                         */
42/*---------------------------------------------------------------------------*/
43typedef struct LtlAutomatonStruct Ltl_Automaton_t;
44typedef struct LtlAutomatonNodeStruct Ltl_AutomatonNode_t;
45
46
47/*---------------------------------------------------------------------------*/
48/* Variable declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Macro declarations                                                        */
54/*---------------------------------------------------------------------------*/
55
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Function prototypes                                                       */
61/*---------------------------------------------------------------------------*/
62
63EXTERN void Ltl_Init(void);
64EXTERN void Ltl_End(void);
65EXTERN 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);
66EXTERN Hrc_Manager_t * Ltl_McAutomatonToNetwork(Ntk_Network_t *designNetwork, Ltl_Automaton_t *automaton, int verbosity);
67EXTERN boolean Ltl_FormulaStaticSemanticCheckOnNetwork(Ctlsp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
68EXTERN Ltl_Automaton_t * Ltl_AutomatonCreate(void);
69EXTERN void Ltl_AutomatonFree(gGeneric g);
70EXTERN Ltl_AutomatonNode_t * Ltl_AutomatonNodeCreate(Ltl_Automaton_t *aut);
71EXTERN void Ltl_AutomatonNodeFree(gGeneric g);
72EXTERN void Ltl_AutomatonNodePrint(Ltl_Automaton_t *aut, Ltl_AutomatonNode_t *node);
73EXTERN void Ltl_AutomatonPrint(Ltl_Automaton_t *aut, int verbosity);
74EXTERN void Ltl_AutomatonToDot(FILE *fp, Ltl_Automaton_t *aut, int level);
75EXTERN int Ltl_AutomatonToBlifMv(FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A);
76EXTERN int Ltl_AutomatonToVerilog(FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A);
77EXTERN int Ltl_AutomatonToSmv(FILE *fp, Ntk_Network_t *network, Ltl_Automaton_t *A);
78EXTERN int Ltl_AutomatonMinimizeByIOCompatible(Ltl_Automaton_t *A, int verbosity);
79EXTERN int Ltl_AutomatonMinimizeByDirectSimulation(Ltl_Automaton_t *A, int verbosity);
80EXTERN void Ltl_AutomatonAddFairStates(Ltl_Automaton_t *A);
81EXTERN int Ltl_AutomatonMaximizeByDirectSimulation(Ltl_Automaton_t *A, int verbosity);
82EXTERN int Ltl_AutomatonMinimizeByReverseSimulation(Ltl_Automaton_t *A, int verbosity);
83EXTERN int Ltl_AutomatonMinimizeByPrune(Ltl_Automaton_t *A, int verbosity);
84EXTERN void Ltl_AutomatonComputeSCC(Ltl_Automaton_t *A, int force);
85EXTERN int Ltl_AutomatonIsWeak(Ltl_Automaton_t *A);
86EXTERN Mc_AutStrength_t Ltl_AutomatonGetStrength(Ltl_Automaton_t *A);
87EXTERN Ltl_Automaton_t * Ltl_AutomatonCreateQuotient(Ltl_Automaton_t *A, st_table *partition);
88EXTERN int Ltl_AutomatonVtxGetNodeIdx(vertex_t *v);
89
90/**AutomaticEnd***************************************************************/
91
92#endif /* _LTL */
Note: See TracBrowser for help on using the repository browser.