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
|
// Variable definition class -*- c++ -*-
#ifndef VARIABLEDEFINITION_H_
# define VARIABLEDEFINITION_H_
# ifdef __GNUC__
# pragma interface
# endif // __GNUC__
# include <map>
# include "typedefs.h"
/** @file VariableDefinition.h
* A variable that can be assigned a value in a Valuation
*/
/* Copyright 1999-2001 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. */
/** Variable definition */
class VariableDefinition
{
public:
/** Map of quantifier variables associated with an aggregate variable */
typedef std::map<char*,class VariableDefinition*> ChildMap;
/** Default constructor */
VariableDefinition ();
/** Constructor
* @param name Name of the variable
* @param type Type of the variable
* @param aggregate Flag: is this an aggregate variable (quantifier)
* @param hidden Flag: is the variable hidden
*/
VariableDefinition (char* name, const class Type& type,
bool aggregate, bool hidden = false);
/** Copy constructor */
VariableDefinition (const class VariableDefinition& old);
private:
/** Assignment operator */
class VariableDefinition& operator= (const class VariableDefinition& old);
public:
/** Destructor */
~VariableDefinition ();
/** Determine the name of the variable */
const char* getName () const { return myName; }
/** Determine the type of the variable */
const class Type& getType () const { return *myType; }
/** Determine the father of the variable */
const class VariableDefinition* getFather () const { return myFather; }
/** Determine whether this is an aggregate variable */
bool isAggregate () const { return myIsAggregate; }
/** Determine whether this variable may be undefined */
bool isUndefined () const { return myIsUndefined; }
/** Determine whether this variable has been referenced */
bool isReferenced () const { return myIsReferenced; }
/** Determine whether this variable is hidden */
bool isHidden () const { return myIsHidden; }
/** Flag that the variable may be undefined */
void flagUndefined () { myIsUndefined = true; }
/** Set the "referenced" flag of the variable */
void flagReferenced (bool referenced) const { myIsReferenced = referenced; }
/** Set the "hidden" flag of the variable */
void flagHidden (bool hidden) { myIsHidden = hidden; }
/** Find a child variable to a quantified variable
* @param name name of the child variable
* @return the variable, or NULL if not found
*/
const class VariableDefinition* findChild (const char* name) const;
/** Add a child variable to a quantified variable
* @param name name of the child variable
* @param type type of the child variable
* @return the variable, or NULL if contradictory definition
*/
const class VariableDefinition* addChild (char* name,
const class Type& type) const;
# ifdef EXPR_COMPILE
/** Determine the number of the compiled variable */
unsigned getNumber () const { return myNumber; }
/** Set the number of the compiled variable */
void setNumber (unsigned number) { myNumber = number; }
# endif // EXPR_COMPILE
private:
/** Name of the variable */
char* myName;
/** Type of the variable */
const class Type* myType;
/** Flag: is this an aggregate variable? */
const bool myIsAggregate;
/** Flag: may the variable be undefined? */
bool myIsUndefined;
/** Flag: has the variable been referenced? */
mutable bool myIsReferenced;
/** Flag: has the variable been hidden? */
bool myIsHidden;
# ifdef EXPR_COMPILE
/** Number of the compiled variable */
unsigned myNumber;
# endif // EXPR_COMPILE
/** The child variables of an aggregate variable */
mutable ChildMap myChildMap;
/** The father of a child variable */
const class VariableDefinition* myFather;
};
#endif // VARIABLEDEFINITION_H_
|
