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

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

vis2.3
File size: 12.6 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [ltlInt.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: ltlInt.h,v 1.26 2008/04/22 21:21:45 fabio Exp $]
16
17******************************************************************************/
18
19#ifndef _LTLINT
20#define _LTLINT
21
22/*---------------------------------------------------------------------------*/
23/* Nested includes                                                           */
24/*---------------------------------------------------------------------------*/
25#include "io.h"
26#include "ltl.h"
27#include "cmd.h"
28#include "ctlsp.h"
29#include "fsm.h"
30#include "ntk.h"
31#include "ord.h"
32#include "part.h"
33#include "mc.h"
34#include <string.h>
35
36
37/*---------------------------------------------------------------------------*/
38/* Constant declarations                                                     */
39/*---------------------------------------------------------------------------*/
40typedef struct LtlMcOption LtlMcOption_t;
41typedef struct LtlTableauEntry  LtlTableauEntry_t;
42typedef struct LtlTableauStruct LtlTableau_t;
43typedef struct LtlSetStruct  LtlSet_t;
44typedef struct LtlPairStruct LtlPair_t;
45
46
47/**Enum************************************************************************
48
49  Synopsis    [Level to which debugging of CTL formulae is performed.]
50
51******************************************************************************/
52
53typedef enum {
54  LtlMcDbgLevelNone_c,
55  LtlMcDbgLevelMin_c,
56  LtlMcDbgLevelMinVerbose_c,
57  LtlMcDbgLevelMax_c,
58  LtlMcDbgLevelInteractive_c
59} LtlMcDbgLevel;
60
61/**Enum************************************************************************
62
63  Synopsis    [Automaton->File Formats.]
64
65  Description []
66
67******************************************************************************/
68
69typedef enum {
70    Aut2File_DOT_c,
71    Aut2File_BLIFMV_c,
72    Aut2File_VERILOG_c,
73    Aut2File_ALL_c
74}Aut2FileType;
75
76/**Enum************************************************************************
77
78  Synopsis    [LTL->Automaton Translation Algorithm.]
79
80  Description []
81
82******************************************************************************/
83
84typedef enum {
85    Ltl2Aut_GPVW_c,
86    Ltl2Aut_GPVWplus_c,
87    Ltl2Aut_LTL2AUT_c,
88    Ltl2Aut_WRING_c
89} Ltl2AutAlgorithm;
90
91
92/*---------------------------------------------------------------------------*/
93/* Structure declarations                                                    */
94/*---------------------------------------------------------------------------*/
95
96
97/**Struct**********************************************************************
98
99  Synopsis    [A struct for keeping the command line options.]
100
101******************************************************************************/
102struct LtlMcOption {
103  boolean printInputs;
104  FILE *ltlFile;              /* contains the ltl formulae */
105  FILE *debugFile;
106  boolean useMore;            /* use more as pipe for debug output */
107  boolean simValue;
108  Mc_LeMethod_t leMethod;
109  Mc_DcLevel dcLevel;
110  LtlMcDbgLevel dbgLevel;
111  Mc_GSHScheduleType schedule;
112  Mc_FwdBwdAnalysis direction;
113  int lockstep;
114  Mc_VerbosityLevel verbosity;
115  int timeOutPeriod;
116
117  Ltl2AutAlgorithm algorithm; /* GPVW/GPVW+/LTL2AUT/WRING */
118  boolean booleanmin;         /* use boolean minimization to simplify cover */
119  boolean rewriting;          /* rewriting the fomula */
120  boolean prunefair;          /* prune the fairness */
121  boolean iocompatible;       /* minimization by io-compatible */
122  boolean directsim;          /* minimization by direct simulation rln */
123  boolean reversesim;         /* minimization by reverse simulation rln */
124  boolean directsimMaximize;  /* adding arcs by direct simulation rln */
125
126  int noIncrementalPartition; /* ? build the parition of MxA incrementally */
127  int noStrengthReduction;    /* ? use different decision procedures */
128                              /*   for different automaton strength */
129  int noShuffleToTop;         /* ? shuffle automaton vars to the top */
130
131  Aut2FileType outputformat;  /* write blifmv/verilog/smv/dot file as output */
132  char *outputfilename;
133};
134
135
136/**Struct**********************************************************************
137
138  Synopsis    [A struct for holding the Tableau Rule Expansition of 1 Formula.]
139
140******************************************************************************/
141struct LtlTableauEntry {
142  Ctlsp_Formula_t  *F;        /* the formula */
143  struct alpha {              /* alpha[0].beta[0]*alpha[0].beta[1] + */
144    int B[2];                 /* alpha[1].beta[0]*alpha[1].beta[1]   */
145    int n;
146  } A[2];
147  int notF_idx;               /* negation of 'f' */
148  Ctlsp_Formula_t  *notF;
149};
150
151/**Struct**********************************************************************
152
153  Synopsis    [A struct for holding the Tableau Rule Expansition of All the
154  sub-Formulae of the given LTL Formula F and its negation.]
155
156******************************************************************************/
157struct LtlTableauStruct {
158  Ctlsp_Formula_t *F;         /* Formula in NNF */
159  Ctlsp_Formula_t *notF;      /* & its negation */
160  st_table *formulaUniqueTable;
161  st_table *untilUniqueTable;
162
163  int abIndex;                /* Alpha_Beta_Table */
164  LtlTableauEntry_t *abTable;
165  array_t *abTableNegate;     /* provide Negate method, for set operation */
166 
167  int labelIndex;             /* label table: (ID/TRUE/FALSE) */
168  Ctlsp_Formula_t **labelTable;
169  array_t *labelTableNegate;  /*provide Negate method, for set operation */
170
171  int algorithm;              /* algorithm GPVW/GPVW+/LTL2AUT/WRING */
172  int booleanmin;             /* switch: for boolean minimization */
173  int verbosity;
174};
175
176/**Struct**********************************************************************
177
178  Synopsis    [A struct for holding a set, in which each index corresponds to
179  an elementary formula.]
180
181******************************************************************************/
182struct LtlSetStruct {
183  var_set_t *e;       
184};
185
186
187/**Struct**********************************************************************
188
189  Synopsis    [The Buechi Automaton / Quotient Graph  struct.]
190
191******************************************************************************/
192struct LtlAutomatonStruct {
193  LtlTableau_t *tableau;      /* <optional>, the tableau */
194  Ltl_Automaton_t *Q;         /* <optional>, Quotion graph */
195  st_table *SCC;              /* <optional>, SCC partitions */
196  int isQuotientGraph;
197  /* in automaton graph, Q->SCC is (component, 0) */
198  /* in quotient graph, Q->SCC is a mapping (component, Q_vtx) */
199
200  /*--below are required fields-------------------------------------------*/
201  char *name;
202  graph_t *G;
203  st_table  *Init;            /* initial states (vertices) */
204  st_table *dontcare;         /* these state can be in/out FairSets*/
205  lsList  Fair;               /* list of sets (hash tables) */
206  array_t *labelTable;        /* unique table for propositionals (labels),
207                                 'node->Labes' is a var_set_t refer to it.
208                                 Initially it's a Clone of
209                                 'tableau->labelTable',
210                                 from which it shares nothing in common */
211  array_t *labelTableNegate;  /* provide Negate method for each label item */
212  int node_idx;               /* auxilary counter in creating nodes */
213  bdd_t     *transitionRelation; /* Holds the bdd of the translation relation */
214  bdd_t     *initialStates;      /* Holds the bdd of the initial states */
215  bdd_t     *fairSets;           /* Holds the bdd of the fair states */
216  array_t   *fairSetArray;       /* Holda bdd of all fair sets.*/
217  st_table  *psNsTable;          /* Maps present state to next state*/
218  st_table  *nsPsTable;          /* Maps next state to present state*/
219};
220
221
222/**Struct**********************************************************************
223
224  Synopsis    [The struct for a node in the Buechi Automaton / Quotient
225  graph. It's attached to each vertex (vertex->user_data).]
226
227******************************************************************************/
228struct LtlAutomatonNodeStruct { 
229  int index;
230  LtlSet_t *Labels;           /* a list of constant formulae, state labels */
231   
232  LtlSet_t *CoverSet;         /* <optional> */
233  st_table *Class;
234  mdd_t    *Encode;           /* Encode the state of automaton */
235  int      *cnfIndex;
236};
237
238
239/**Struct**********************************************************************
240
241  Synopsis    [The struct for holding a Generic Pair (ordered).]
242
243******************************************************************************/
244struct LtlPairStruct {
245  char *First;
246  char *Second;
247};
248
249/*---------------------------------------------------------------------------*/
250/* Type declarations                                                         */
251/*---------------------------------------------------------------------------*/
252
253
254/*---------------------------------------------------------------------------*/
255/* Variable declarations                                                     */
256/*---------------------------------------------------------------------------*/
257
258
259/*---------------------------------------------------------------------------*/
260/* Macro declarations                                                        */
261/*---------------------------------------------------------------------------*/
262
263
264/**AutomaticStart*************************************************************/
265
266/*---------------------------------------------------------------------------*/
267/* Function prototypes                                                       */
268/*---------------------------------------------------------------------------*/
269
270EXTERN Ltl_Automaton_t * LtlMcFormulaToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *Formula, LtlMcOption_t *options, int checkSemantics);
271EXTERN void LtlFsmLoadFairness(Fsm_Fsm_t *compFsm, Fsm_Fairness_t *designFairness, int NumberOfFairSets, int *AutomatonStrength);
272EXTERN LtlMcOption_t * LtlMcOptionAlloc(void);
273EXTERN void LtlMcOptionFree(LtlMcOption_t *result);
274EXTERN Ltl_Automaton_t * LtlAutomatonGeneration(LtlTableau_t *tableau);
275EXTERN int LtlAutomatonSetIsFair(LtlTableau_t *tableau, LtlSet_t *r);
276EXTERN LtlSet_t * LtlAutomatonVertexGetLabels(vertex_t *vtx);
277EXTERN LtlSet_t * LtlSetNew(int size);
278EXTERN void LtlSetFree(LtlSet_t *set);
279EXTERN LtlSet_t * LtlSetCopy(LtlSet_t *from);
280EXTERN void LtlSetAssign(LtlSet_t *to, LtlSet_t *from);
281EXTERN int LtlSetEqual(LtlSet_t *s1, LtlSet_t *s2);
282EXTERN int LtlSetCardinality(LtlSet_t *set);
283EXTERN int LtlSetCompareCardinality(const void *p1, const void *p2);
284EXTERN int LtlSetIsContradictory(LtlSet_t *set, array_t *Negate);
285EXTERN int LtlSetInclude(LtlSet_t *large, LtlSet_t *small);
286EXTERN void LtlSetOR(LtlSet_t *to, LtlSet_t *from1, LtlSet_t *from2);
287EXTERN void LtlSetClear(LtlSet_t *set);
288EXTERN void LtlSetSetElt(LtlSet_t *set, int index);
289EXTERN void LtlSetClearElt(LtlSet_t *set, int index);
290EXTERN int LtlSetGetElt(LtlSet_t *set, int index);
291EXTERN int LtlSetIsEmpty(LtlSet_t *set);
292EXTERN LtlSet_t * LtlSetIsInList(LtlSet_t *set, lsList list);
293EXTERN LtlSet_t * LtlSetToLabelSet(LtlTableau_t *tableau, LtlSet_t *set);
294EXTERN void LtlSetPrint(LtlTableau_t *tableau, LtlSet_t *set);
295EXTERN void LtlSetPrintIndex(int length, LtlSet_t *set);
296EXTERN LtlPair_t * LtlPairNew(char *First, char *Second);
297EXTERN void LtlPairFree(LtlPair_t *pair);
298EXTERN int LtlPairHash(char *key, int modulus);
299EXTERN int LtlPairCompare(const char *key1, const char *key2);
300EXTERN void LtlPairPrint(LtlPair_t *pair);
301EXTERN void LtlCoverPrintIndex(int length, lsList cover);
302EXTERN lsList LtlCoverCompleteSum(lsList Cover, array_t *Negate);
303EXTERN LtlSet_t * LtlSetConsensus(LtlSet_t *first, LtlSet_t *second, array_t *Negate);
304EXTERN lsList LtlCoverCofactor(lsList Cover, LtlSet_t *c, array_t *Negate);
305EXTERN int LtlCoverIsTautology(lsList Cover, array_t *Negate);
306EXTERN int LtlCoverIsImpliedBy(lsList Cover, LtlSet_t *term, array_t *Negate);
307EXTERN lsList LtlCoverPrimeAndIrredundant(LtlTableau_t *tableau, lsList Cover, array_t *Negate);
308EXTERN LtlSet_t * LtlCoverGetSuperCube(lsList Cover, array_t *Negate);
309EXTERN mdd_t * LtlSetModelCheckFormulae(LtlSet_t *set, array_t *labelTable, Fsm_Fsm_t *fsm);
310EXTERN LtlTableau_t * LtlTableauGenerateTableau(Ctlsp_Formula_t *formula);
311EXTERN LtlTableau_t * LtlTableauCreate(void);
312EXTERN void LtlTableauFree(LtlTableau_t *tableau);
313EXTERN void LtlTableauPrint(FILE *fp, LtlTableau_t *tableau);
314EXTERN Ctlsp_Formula_t * LtlTableauGetUniqueXFormula(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
315
316/**AutomaticEnd***************************************************************/
317
318#endif /* _LTLINT */
Note: See TracBrowser for help on using the repository browser.