source: vis_dev/vis-2.3/src/ctlp/ctlp.h @ 20

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

vis2.3
File size: 11.1 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [ctlp.h]
4
5  PackageName [ctlp]
6
7  Synopsis    [Routines for parsing, writing and accessing CTL formulas.]
8
9  Description [This package implements a parser for CTL (Computation Tree
10  Logic) formulas.  CTL is a language used to describe properties of systems.
11  For the syntax of CTL formulas, refer to <A HREF="../ctl_ltl/ctl_ltl/ctl_ltl.html">
12  the VIS CTL and LTL syntax manual</A>.]
13
14  SeeAlso     [mc]
15
16  Author      [Gary York, Ramin Hojati, Tom Shiple, Adnan Aziz, Yuji Kukimoto,
17               Jae-Young Jang, In-Ho Moon]
18
19  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
20  All rights reserved.
21
22  Permission is hereby granted, without written agreement and without license
23  or royalty fees, to use, copy, modify, and distribute this software and its
24  documentation for any purpose, provided that the above copyright notice and
25  the following two paragraphs appear in all copies of this software.
26
27  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
28  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
29  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
30  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
31
32  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
33  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
34  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
35  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
36  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
37
38  Revision    [$Id: ctlp.h,v 1.29 2005/05/08 14:51:46 fabio Exp $]
39
40******************************************************************************/
41
42#ifndef _CTLP
43#define _CTLP
44
45#include "vm.h"
46
47/*---------------------------------------------------------------------------*/
48/* Structure declarations                                                    */
49/*---------------------------------------------------------------------------*/
50
51/**Enum************************************************************************
52
53  Synopsis    [Types of operators allowed in CTL formulas.]
54
55  Description [The types of nodes in a CTL formula parse tree. ID, TRUE, and
56  FALSE are leaves, and all others are internal nodes.]
57
58  SeeAlso     [Ctlp_FormulaReadType]
59
60******************************************************************************/
61typedef enum {
62  Ctlp_EX_c,     /* there exists a next state */
63  Ctlp_EG_c,     /* there exists a path globally */
64  Ctlp_EF_c,     /* there exists a path finally */
65  Ctlp_EU_c,     /* there exists a path, until (not symmetric in args) */ 
66  Ctlp_AX_c,     /* for all next states */
67  Ctlp_AG_c,     /* for all paths globally */
68  Ctlp_AF_c,     /* for all paths finally */
69  Ctlp_AU_c,     /* for all paths, until (not symmetric in args) */
70  Ctlp_OR_c,     /* Boolean disjunction */
71  Ctlp_AND_c,    /* Boolean conjunction */
72  Ctlp_NOT_c,    /* Boolean negation*/
73  Ctlp_THEN_c,   /* Boolean implies (not symmetric) */
74  Ctlp_XOR_c,    /* Boolean not equal */
75  Ctlp_EQ_c,     /* Boolean equal */
76  Ctlp_ID_c,     /* an atomic proposition */
77  Ctlp_TRUE_c,   /* tautology (used only for translation to exist. form) */
78  Ctlp_FALSE_c,  /* empty (used only for translation to exist. form) */
79  Ctlp_FwdU_c,   /* forward until */
80  Ctlp_FwdG_c,   /* forward global */
81  Ctlp_EY_c,     /* there exists a previous state */
82  Ctlp_EH_c,     /* there exists a path globally in the past */
83  Ctlp_Init_c,   /* initial states */
84  Ctlp_Cmp_c     /* compare two leaves in forward CTL */
85} Ctlp_FormulaType;
86
87 
88/**Enum************************************************************************
89
90  Synopsis    [Classification of CTL formulae according to quantification.]
91
92  Description [A CTL formula is quantifier-free if it contains no
93  quantifiers.  A CTL formula is classifed in ECTL if it contains quantifiers
94  and every existential quantifier is under an even number of negations, while
95  every universal quantifier is under an odd number of negations.  For an ACTL
96  formula, the negation parity is exchanged.  All remaining formulae are
97  mixed.]
98
99  SeeAlso     []
100
101******************************************************************************/
102typedef enum {
103  Ctlp_ECTL_c,
104  Ctlp_ACTL_c,
105  Ctlp_Mixed_c,
106  Ctlp_QuantifierFree_c
107} Ctlp_FormulaClass;
108
109
110/**Enum************************************************************************
111
112  Synopsis    [Classification of ACTL formulae according to Beer et al..]
113
114  Description [w-ACTL is the subset of ACTL to which the vacuity detection
115  algorithm of Beer et al. (CAV 97) is applicable.  An ACTL formula is in
116  w-ACTL if at least one child of every binary operator is propositional.
117  A simple formula is a propositional, while a state formula is a
118  non-propositional w-ACTL.]
119
120  SeeAlso     []
121
122******************************************************************************/
123typedef enum {
124    Ctlp_WACTLsimple_c,
125    Ctlp_WACTLstate_c,
126    Ctlp_NONWACTL_c
127} Ctlp_FormulaACTLSubClass;
128
129
130/**Enum************************************************************************
131
132  Synopsis    [Types of approximations that are possible]
133
134  Description [We can have overapproximations, underapproximations, exact
135  approximations, or incomparable sets.  Question: is ctlp the right place for
136  this?  It is used in ctlp, mc, rch. (RB)]
137
138  SeeAlso     []
139
140******************************************************************************/
141typedef enum {
142  Ctlp_Incomparable_c,
143  Ctlp_Underapprox_c,
144  Ctlp_Overapprox_c,
145  Ctlp_Exact_c
146} Ctlp_Approx_t;
147
148
149/**Enum************************************************************************
150
151  Synopsis    [Negation parity of a node.]
152
153  Description [It can be even, odd, or both.  The fourth value is for
154  uninitialized.  For a formula with no sharing, XOR and EQ nodes cause
155  their descendants to have both parities.]
156
157  SeeAlso     []
158
159******************************************************************************/
160typedef enum {
161  Ctlp_NoParity_c,
162  Ctlp_Even_c,
163  Ctlp_Odd_c,
164  Ctlp_EvenOdd_c
165} Ctlp_Parity_t;
166
167
168/*---------------------------------------------------------------------------*/
169/* Type declarations                                                         */
170/*---------------------------------------------------------------------------*/
171typedef struct CtlpFormulaStruct Ctlp_Formula_t;
172typedef void   (*Ctlp_DbgInfoFreeFn) (Ctlp_Formula_t *);
173typedef array_t Ctlp_FormulaArray_t; /* array of Ctlp_Formula_t * */
174
175/**AutomaticStart*************************************************************/
176
177/*---------------------------------------------------------------------------*/
178/* Function prototypes                                                       */
179/*---------------------------------------------------------------------------*/
180
181EXTERN void Ctlp_Init(void);
182EXTERN void Ctlp_End(void);
183EXTERN array_t * Ctlp_FileParseFormulaArray(FILE * fp);
184EXTERN char * Ctlp_FormulaConvertToString(Ctlp_Formula_t * formula);
185EXTERN void Ctlp_FormulaPrint(FILE * fp, Ctlp_Formula_t * formula);
186EXTERN Ctlp_FormulaType Ctlp_FormulaReadType(Ctlp_Formula_t * formula);
187EXTERN int Ctlp_FormulaReadCompareValue(Ctlp_Formula_t * formula);
188EXTERN char * Ctlp_FormulaReadVariableName(Ctlp_Formula_t * formula);
189EXTERN char * Ctlp_FormulaReadValueName(Ctlp_Formula_t * formula);
190EXTERN Ctlp_Formula_t * Ctlp_FormulaReadLeftChild(Ctlp_Formula_t * formula);
191EXTERN Ctlp_Formula_t * Ctlp_FormulaReadRightChild(Ctlp_Formula_t * formula);
192EXTERN mdd_t * Ctlp_FormulaObtainStates(Ctlp_Formula_t * formula);
193EXTERN mdd_t * Ctlp_FormulaObtainLatestApprox(Ctlp_Formula_t *formula);
194EXTERN mdd_t * Ctlp_FormulaObtainApproxStates(Ctlp_Formula_t *formula, Ctlp_Approx_t approx);
195EXTERN void Ctlp_FormulaSetStates(Ctlp_Formula_t * formula, mdd_t * states);
196EXTERN void Ctlp_FormulaSetApproxStates(Ctlp_Formula_t * formula, mdd_t * states, Ctlp_Approx_t approx);
197EXTERN void Ctlp_FormulaSetDbgInfo(Ctlp_Formula_t * formula, void *data, Ctlp_DbgInfoFreeFn freeFn);
198EXTERN void * Ctlp_FormulaReadDebugData(Ctlp_Formula_t * formula);
199EXTERN boolean Ctlp_FormulaTestIsConverted(Ctlp_Formula_t * formula);
200EXTERN boolean Ctlp_FormulaTestIsQuantifierFree(Ctlp_Formula_t *formula);
201EXTERN Ctlp_Formula_t * Ctlp_FormulaReadOriginalFormula(Ctlp_Formula_t * formula);
202EXTERN void Ctlp_FormulaFree(Ctlp_Formula_t *formula);
203EXTERN void Ctlp_FlushStates(Ctlp_Formula_t * formula);
204EXTERN Ctlp_Formula_t * Ctlp_FormulaDup(Ctlp_Formula_t * formula);
205EXTERN Ctlp_Formula_t * Ctlp_FormulaConverttoComplement(Ctlp_Formula_t * formula);
206EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertAFtoAU(Ctlp_Formula_t * formula);
207EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertEFtoOR(Ctlp_Formula_t * formula);
208EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertEUtoOR(Ctlp_Formula_t * formula);
209EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertXORtoOR(Ctlp_Formula_t * formula);
210EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertEQtoOR(Ctlp_Formula_t * formula);
211EXTERN Ctlp_Formula_t * Ctlp_FormulaPushNegation(Ctlp_Formula_t * formula);
212EXTERN void Ctlp_FormulaArrayFree(array_t * formulaArray);
213EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertToExistentialForm(Ctlp_Formula_t * formula);
214EXTERN Ctlp_Formula_t * Ctlp_FormulaConvertToSimpleExistentialForm(Ctlp_Formula_t * formula);
215EXTERN array_t * Ctlp_FormulaArrayConvertToExistentialFormTree(array_t * formulaArray);
216EXTERN array_t * Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(array_t * formulaArray);
217EXTERN array_t * Ctlp_FormulaArrayConvertToDAG(array_t *formulaArray);
218EXTERN array_t * Ctlp_FormulaDAGConvertToExistentialFormDAG(array_t *formulaDAG);
219EXTERN Ctlp_Formula_t * Ctlp_FormulaCreate(Ctlp_FormulaType type, void * left, void * right);
220EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateOr(char *name, char *valueStr);
221EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateVectorAnd(char *nameVector, char *value);
222EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateVectorOr(char *nameVector, char *valueStr);
223EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateEquiv(char *left, char *right);
224EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateVectorEquiv(char *left, char *right);
225EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateAXMult(char *string, Ctlp_Formula_t *formula);
226EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateEXMult(char *string, Ctlp_Formula_t *formula);
227EXTERN array_t * Ctlp_FormulaArrayConvertToForward(array_t *formulaArray, int singleInitial, boolean doNotShareFlag);
228EXTERN char * Ctlp_FormulaGetTypeString(Ctlp_Formula_t *formula);
229EXTERN Ctlp_FormulaClass Ctlp_CheckClassOfExistentialFormula(Ctlp_Formula_t *formula);
230EXTERN Ctlp_FormulaClass Ctlp_CheckClassOfExistentialFormulaArray(array_t *formulaArray);
231EXTERN boolean Ctlp_FormulaIdentical(Ctlp_Formula_t *formula1, Ctlp_Formula_t *formula2);
232EXTERN void Ctlp_FormulaMakeMonotonic(Ctlp_Formula_t *formula);
233EXTERN void Ctlp_FormulaArrayMakeMonotonic(array_t *formulaArray);
234EXTERN void Ctlp_FormulaNegations(Ctlp_Formula_t *formula, Ctlp_Parity_t parity);
235EXTERN Ctlp_FormulaACTLSubClass Ctlp_CheckIfWACTL(Ctlp_Formula_t *formula);
236EXTERN Ctlp_Formula_t * Ctlp_FormulaCreateWitnessFormula(Ctlp_Formula_t *formula);
237
238/**AutomaticEnd***************************************************************/
239
240#endif /* _CTLP */
Note: See TracBrowser for help on using the repository browser.