~tapaal-ltl/verifypn/rule-D-fix

« back to all changes in this revision

Viewing changes to PetriEngine/ValidationBuilder.h

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 * 
 
6
 * This program is free software: you can redistribute it and/or modify
 
7
 * it under the terms of the GNU General Public License as published by
 
8
 * the Free Software Foundation, either version 3 of the License, or
 
9
 * (at your option) any later version.
 
10
 * 
 
11
 * This program is distributed in the hope that it will be useful,
 
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
 * GNU General Public License for more details.
 
15
 * 
 
16
 * You should have received a copy of the GNU General Public License
 
17
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
18
 */
 
19
#ifndef VALIDATIONBUILDER_H
 
20
#define VALIDATIONBUILDER_H
 
21
 
 
22
#include "AbstractPetriNetBuilder.h"
 
23
#include "PQL/PQL.h"
 
24
 
 
25
#include <string>
 
26
#include <vector>
 
27
 
 
28
namespace PetriEngine{
 
29
 
 
30
class ValidationBuilder;
 
31
 
 
32
/** Error experienced during Validation */
 
33
class ValidationError{
 
34
        /** Create error for an arc */
 
35
        ValidationError(const std::string& startId,
 
36
                                        const std::string& endId,
 
37
                                        const std::string& text)
 
38
         : _startId(startId), _endId(endId), _text(text) {
 
39
                _hasExprError = false;
 
40
                _isConditionError = false;
 
41
        }
 
42
 
 
43
        /** Create error for a PQL expression */
 
44
        ValidationError(const std::string& id,
 
45
                                        const PQL::ExprError& error,
 
46
                                        bool isConditionError)
 
47
         : _startId(id), _exprError(error) {
 
48
                _hasExprError = true;
 
49
                _isConditionError = isConditionError;
 
50
        }
 
51
 
 
52
        /** Create error for an entity */
 
53
        ValidationError(const std::string& id,
 
54
                                        const std::string& text)
 
55
         : _startId(id), _text(text) {
 
56
                _hasExprError = false;
 
57
                _isConditionError = false;
 
58
        }
 
59
public:
 
60
        /** Identifier related to the error, start identifier if related to an arc */
 
61
        const std::string& startIdentifier() const { return _startId; }
 
62
 
 
63
        /** End identifier to the error if related to an arc, otherwise empty */
 
64
        const std::string& endIdentifier() const { return _endId; }
 
65
 
 
66
        /** True, if this error carries and non-empty PQL::ExprError */
 
67
        bool hasExprError() const { return _hasExprError; }
 
68
 
 
69
        /** True, if this error carries an non-empty PQL::ExprError
 
70
         * related to a condition, false if it's related to AssignmentExpression
 
71
         * or carries an empty PQL::ExprError. See also hasExprError().
 
72
         */
 
73
        bool isConditionError() const {return _isConditionError; }
 
74
 
 
75
        /** Expression error, found in an expression */
 
76
        const PQL::ExprError& exprError() const { return _exprError; }
 
77
 
 
78
        /** Explanation of the error, empty of it's carries an PQL::ExprError */
 
79
        const std::string& text() const { return _text; }
 
80
private:
 
81
        std::string _startId, _endId;
 
82
        bool _hasExprError;
 
83
        bool _isConditionError;
 
84
        PQL::ExprError _exprError;
 
85
        std::string _text;
 
86
        friend class ValidationBuilder;
 
87
};
 
88
 
 
89
/** Builder for validating the consistency of Petri Nets
 
90
 * @remarks This builder ensures the following properties:
 
91
 *              - Identifiers are unique
 
92
 *              - Conditions can be parsed and analysed without problems
 
93
 *              - Assignments can be parsed and analysed without problems
 
94
 *              - Initial value of variables is within range
 
95
 *              - The inital marking isn't negative
 
96
 *              - No weights are negative
 
97
 *              - Arcs goes between existing start and end points of correct type
 
98
 */
 
99
class ValidationBuilder : public AbstractPetriNetBuilder
 
100
{
 
101
        /** Arc, just internal stuff */
 
102
        struct Arc{
 
103
                Arc(const std::string& start,
 
104
                        const std::string& end){
 
105
                        this->start = start;
 
106
                        this->end = end;
 
107
                }
 
108
                std::string start;
 
109
                std::string end;
 
110
        };
 
111
public:
 
112
    ValidationBuilder();
 
113
        void addVariable(const std::string& name,
 
114
                                         int initialValue,
 
115
                                         int range);
 
116
        void addPlace(const std::string& name,
 
117
                                  int tokens,
 
118
                                  double x,
 
119
                                  double y);
 
120
        void addTransition(const std::string& name,
 
121
                                           const std::string& conditions,
 
122
                                           const std::string& assignments,
 
123
                                           double x,
 
124
                                           double y);
 
125
        void addInputArc(const std::string& place,
 
126
                                         const std::string& transition,
 
127
                                         int weight);
 
128
        void addOutputArc(const std::string& transition,
 
129
                                          const std::string& place,
 
130
                                          int weight);
 
131
        /** Stop accepting stuff, and start validating
 
132
         * @return true, if no errors were found
 
133
         */
 
134
        bool validate();
 
135
 
 
136
        /** Get errors found during evaluation */
 
137
        const std::vector<ValidationError>& errors() const { return _errors; }
 
138
private:
 
139
        /** Get the number of matching identifiers */
 
140
        int countMatchingIds(const std::string& id);
 
141
        std::vector<ValidationError> _errors;
 
142
        std::vector<std::string> _varNames;
 
143
        std::vector<std::string> _placeNames;
 
144
        std::vector<std::string> _transitionNames;
 
145
        std::vector<std::string> _conditions;
 
146
        std::vector<std::string> _assignments;
 
147
        std::vector<Arc> _inputArcs;
 
148
        std::vector<Arc> _outputArcs;
 
149
};
 
150
 
 
151
} // PetriEngine
 
152
 
 
153
#endif // VALIDATIONBUILDER_H
 
154