1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
// Property automaton -*- c++ -*-
#ifndef PROPERTY_H_
# define PROPERTY_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include "PropertyState.h"
# include "BitVector.h"
/** @file Property.h
* Automaton representing the negation of a property being verified
*/
/* Copyright 1999-2002 Marko Mkel (msmakela@tcs.hut.fi).
This file is part of MARIA, a reachability analyzer and model checker
for high-level Petri nets.
MARIA is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2, or (at your option)
any later version.
MARIA is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
The GNU General Public License is often shipped with GNU software, and
is generally kept in a file called COPYING or LICENSE. If you do not
have a copy of the license, write to the Free Software Foundation,
59 Temple Place, Suite 330, Boston, MA 02111 USA. */
/** Property automaton */
class Property
{
public:
/** Unary operators */
enum Unop { opNot, opFinally, opGlobally, opNext };
/** Binary operators */
enum Binop { opAnd, opOr, opUntil, opRelease };
/** Constructor */
Property ();
private:
/** Copy constructor */
explicit Property (const class Property& old);
/** Assignment operator */
class Property operator= (const class Property& old);
public:
/** Destructor */
~Property ();
# ifdef BUILTIN_LTL
/** Create the property automaton from an expression
* @param expr expression to be translated to an automaton
*/
bool create (class Expression& expr);
# else // BUILTIN_LTL
/** Create the property automaton from an expression
* @param translator command line for invoking an external translator
* @param expr expression to be translated to an automaton
* @return true if the automaton was successfully generated
*/
bool create (const char* translator,
class Expression& expr);
# endif // BUILTIN_LTL
/** Append a constant to the formula string
* @param b the constant (true or false)
* @return the translated object
*/
class Ltl* addConstant (bool b);
/** Append a unary operator to the formula string
* @param op operator to be appended
* @param expr the operand
* @return the translated object
*/
class Ltl* addUnop (enum Unop op,
class Expression& expr);
/** Append a unary operator to the formula string
* @param op operator to be appended
* @param left the first operand
* @param right the second operand
* @return the translated object
*/
class Ltl* addBinop (enum Binop op,
class Expression& left,
class Expression& right);
/** Append a proposition to the formula string
* @param expr proposition to be appended
* @return the translated object
*/
class Ltl* addExpression (class Expression& expr);
/** Determine the index number of the initial state */
unsigned getInitialState () const { return myInitialState; }
/** Determine the index number of the accepting state */
unsigned getFinalState () const { return myFinalState; }
/** Determine the number of states in the property automaton */
unsigned getNumStates () const { return myNumStates; }
/** Determine the number of acceptance sets in the property automaton */
unsigned getNumSets () const { return myNumSets; }
/** Access a state of the automaton
* @param i number of the state
* @return the state
*/
const class PropertyState& operator[] (unsigned i) const {
assert (i < myNumStates);
return myStates[i];
}
/** Determine whether a state belongs to an acceptance set
* @param i number of the state
* @param acc number of the acceptance set
*/
bool accepts (unsigned i, unsigned acc) const {
assert (!isFinite ());
assert (myStatesAccept && i < myNumStates);
assert (acc < myNumSets);
return (*myStatesAccept)[myNumSets ? i * myNumSets + acc : i];
}
/** Determine whether the automaton is a finite-word automaton */
bool isFinite () const { return !myNumSets; }
private:
# ifdef BUILTIN_LTL
/** Flag: is the formula negated? */
bool myNegated;
# else // BUILTIN_LTL
/** File handle for translating the formula */
int myFD;
# endif // BUILTIN_LTL
/** Number of atomic propositions */
unsigned myNumExprs;
/** The atomic propositions (boolean expressions, the alphabet) */
class Expression** myExprs;
/** Number of states */
unsigned myNumStates;
/** The states */
class PropertyState* myStates;
/** Acceptance sets the states belong to */
class BitVector* myStatesAccept;
/** Index number of the initial state */
unsigned myInitialState;
/** Index number of the accepting state (for finite-word automata) */
unsigned myFinalState;
/** Number of acceptance sets */
unsigned myNumSets;
};
#endif // PROPERTY_H_
|
