Merge lp:~tapaal-dist-ctl/verifypn/arithmeticExpressions into lp:verifypn
- arithmeticExpressions
- Merge into new-trunk
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 188 |
Merged at revision: | 183 |
Proposed branch: | lp:~tapaal-dist-ctl/verifypn/arithmeticExpressions |
Merge into: | lp:verifypn |
Diff against target: |
410 lines (+197/-40) 7 files modified
CTL/CTLParser/CTLParser.cpp (+31/-7) CTL/CTLParser/CTLQuery.cpp (+4/-4) CTL/CTLParser/EvaluateableProposition.cpp (+129/-24) CTL/CTLParser/EvaluateableProposition.h (+13/-0) CTL/PetriNets/OnTheFlyDG.cpp (+15/-2) PetriEngine/SuccessorGenerator.cpp (+3/-1) PetriParse/QueryXMLParser.cpp (+2/-2) |
To merge this branch: | bzr merge lp:~tapaal-dist-ctl/verifypn/arithmeticExpressions |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+326178@code.launchpad.net |
This proposal supersedes a proposal from 2017-06-19.
Commit message
Description of the change
Added the requested syntax for arithmetic expressions:
integer-sum
integer-product
integer-difference
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
Lasse S. Jensen (lasjen12) wrote : Posted in a previous version of this proposal | # |
> I can see some problems when parsing the expressions.
>
> A query in the GUI is:
>
> EF N.P0 * N.P1 + N.P2 * N.P2 - N.P4 = 0
>
> and your engine prints it as:
>
> Query before reduction: AG (((P0 + P1) * ((P2 + P2) - P4)) == 0)
>
> but the XML query output seems correct:
>
> <exists-path>
> <finally>
> <integer-eq>
> <integer-sum>
> <integer-product>
> <tokens-count>
> <place>P0</place>
> </tokens-count>
> <tokens-count>
> <place>P1</place>
> </tokens-count>
> </integer-product>
> <integer-
> <integer-product>
> <tokens-count>
> <place>P2</place>
> </tokens-count>
> <tokens-count>
> <place>P2</place>
> </tokens-count>
> </integer-product>
> <tokens-count>
> <place>P4</place>
> </tokens-count>
> </integer-
> </integer-sum>
> <integer-
> </integer-eq>
> </finally>
> </exists-path>
The xml query is not correct. sum and product have been swapped with each other. This was an issue in the parser in verifypn.
Jiri Srba (srba) : | # |
Preview Diff
1 | === modified file 'CTL/CTLParser/CTLParser.cpp' |
2 | --- CTL/CTLParser/CTLParser.cpp 2017-03-15 20:19:30 +0000 |
3 | +++ CTL/CTLParser/CTLParser.cpp 2017-06-22 19:33:43 +0000 |
4 | @@ -344,28 +344,43 @@ |
5 | if (firstLetter == 'a') { |
6 | //Construct all-paths |
7 | query = new CTLQuery(A, getPathOperator(root), false, ""); |
8 | - assert(query->GetQuantifier() == A && "Failed setting quantifier"); |
9 | + if(query->GetQuantifier() != A){ |
10 | + std::cerr << "Error: Failed setting all operator." << std::endl; |
11 | + exit(EXIT_FAILURE); |
12 | + } |
13 | } |
14 | else if (firstLetter == 'e' ) { |
15 | //Construct exists-path |
16 | query = new CTLQuery(E, getPathOperator(root), false, ""); |
17 | - assert(query->GetQuantifier() == E && "Failed setting path operator"); |
18 | + if(query->GetQuantifier() != E){ |
19 | + std::cerr << "Error: Failed setting exists operator." << std::endl; |
20 | + exit(EXIT_FAILURE); |
21 | + } |
22 | } |
23 | else if (firstLetter == 'n' ) { |
24 | //Construct negation |
25 | query = new CTLQuery(NEG, pError, false, ""); |
26 | - assert(query->GetQuantifier() == NEG && "Failed setting negation operator"); |
27 | + if(query->GetQuantifier() != NEG){ |
28 | + std::cerr << "Error: Failed setting negation operator." << std::endl; |
29 | + exit(EXIT_FAILURE); |
30 | + } |
31 | } |
32 | else if (firstLetter == 'c' ) { |
33 | //Construct conjunction |
34 | query = new CTLQuery(AND, pError, false, ""); |
35 | - assert(query->GetQuantifier() == AND && "Failed setting and operator"); |
36 | + if(query->GetQuantifier() != AND){ |
37 | + std::cerr << "Error: Failed setting and operator." << std::endl; |
38 | + exit(EXIT_FAILURE); |
39 | + } |
40 | } |
41 | else if (firstLetter == 'd' ) { |
42 | if( root_name[1] == 'i' ){ |
43 | //Construct disjunction |
44 | query = new CTLQuery(OR, pError, false, ""); |
45 | - assert(query->GetQuantifier() == OR && "Failed setting or operator"); |
46 | + if(query->GetQuantifier() != OR){ |
47 | + std::cerr << "Error: Failed setting or operator." << std::endl; |
48 | + exit(EXIT_FAILURE); |
49 | + } |
50 | } |
51 | else if (root_name[1] == 'e'){ |
52 | //Deadlock query |
53 | @@ -403,7 +418,7 @@ |
54 | |
55 | loperator = loperator_sym(loperator); |
56 | |
57 | - atom_str = first + loperator + second; |
58 | + atom_str = first + "}" + loperator + "{" + second; |
59 | |
60 | } |
61 | else { |
62 | @@ -512,9 +527,18 @@ |
63 | parameter_str = parameter_str + ")"; |
64 | } |
65 | |
66 | - else if(parameter->name()[0] == 'i'){ |
67 | + else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'c'){ |
68 | parameter_str = parameter_str + choppy(parameter->value()) + ")"; |
69 | } |
70 | + else if(parameter->name()[0] == 'i' && parameter->name()[8] == 's'){ |
71 | + parameter_str = parameter_str + parsePar(parameter->first_node()) + " + " + parsePar(parameter->first_node()->next_sibling()) + ")"; |
72 | + } |
73 | + else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'p'){ |
74 | + parameter_str = parameter_str + parsePar(parameter->first_node()) + " * " + parsePar(parameter->first_node()->next_sibling()) + ")"; |
75 | + } |
76 | + else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'd'){ |
77 | + parameter_str = parameter_str + parsePar(parameter->first_node()) + " - " + parsePar(parameter->first_node()->next_sibling()) + ")"; |
78 | + } |
79 | else { |
80 | std::cerr << "Error: Failed parsing query file provided. Incorrect format around the parameter: " << parameter->name() << ". Please check spelling." << std::endl; |
81 | exit(EXIT_FAILURE); |
82 | |
83 | === modified file 'CTL/CTLParser/CTLQuery.cpp' |
84 | --- CTL/CTLParser/CTLQuery.cpp 2017-03-12 18:46:15 +0000 |
85 | +++ CTL/CTLParser/CTLQuery.cpp 2017-06-22 19:33:43 +0000 |
86 | @@ -134,7 +134,7 @@ |
87 | |
88 | std::string CTLQuery::ToString(){ |
89 | if(_hasAtom){ |
90 | - return _a; |
91 | + return _proposition->ToString(); |
92 | } |
93 | else if(_q == AND){ |
94 | return "(" + _firstchild->ToString() + " & " + _secondchild->ToString() + ")"; |
95 | @@ -152,13 +152,13 @@ |
96 | } |
97 | else quanti = "E"; |
98 | if(_path == F){ |
99 | - return quanti + "F" + _firstchild->ToString(); |
100 | + return quanti + "F " + _firstchild->ToString(); |
101 | } |
102 | else if(_path == G){ |
103 | - return quanti + "G" + _firstchild->ToString(); |
104 | + return quanti + "G " + _firstchild->ToString(); |
105 | } |
106 | else if(_path == X){ |
107 | - return quanti + "X" + _firstchild->ToString(); |
108 | + return quanti + "X " + _firstchild->ToString(); |
109 | } |
110 | else if(_path == U){ |
111 | return quanti + "(" + _firstchild->ToString() + ") U (" + _secondchild->ToString() + ")"; |
112 | |
113 | === modified file 'CTL/CTLParser/EvaluateableProposition.cpp' |
114 | --- CTL/CTLParser/EvaluateableProposition.cpp 2017-04-11 10:21:33 +0000 |
115 | +++ CTL/CTLParser/EvaluateableProposition.cpp 2017-06-22 19:33:43 +0000 |
116 | @@ -37,14 +37,14 @@ |
117 | _loperator = SetLoperator(a); |
118 | assert(_loperator != NOT_CARDINALITY); |
119 | |
120 | - size_t begin = a.find('(') + 1; |
121 | - size_t end = a.find(')') - begin; |
122 | - std::string first_parameter_str = a.substr(begin, end); |
123 | - a = a.substr(a.find(')') + 1); |
124 | + //size_t begin = a.find('(') + 1; |
125 | + size_t end = a.find('}'); |
126 | + std::string first_parameter_str = a.substr(0, end); |
127 | + a = a.substr(a.find('}') + 1); |
128 | |
129 | - begin = a.find('(') + 1; |
130 | - end = a.find(')') - begin; |
131 | - std::string second_parameter_str = a.substr(begin, end); |
132 | + size_t begin = a.find('{') + 1; |
133 | + //end = a.find(')') - begin; |
134 | + std::string second_parameter_str = a.substr(begin); |
135 | _firstParameter = CreateParameter(first_parameter_str, net->placeNames(), net->numberOfPlaces()); |
136 | _secondParameter = CreateParameter(second_parameter_str, net->placeNames(), net->numberOfPlaces()); |
137 | } |
138 | @@ -90,7 +90,8 @@ |
139 | SetFireset("all", net->transitionNames(), net->numberOfTransitions()); |
140 | } |
141 | else{ |
142 | - assert(false && "Atomic string proposed for proposition could not be parsed"); |
143 | + std::cerr << "Error: Could not identify Evaluateable Proposition type from atom string: "<<a<<"." << std::endl; |
144 | + exit(EXIT_FAILURE); |
145 | } |
146 | } |
147 | |
148 | @@ -139,7 +140,51 @@ |
149 | } |
150 | |
151 | CardinalityParameter* EvaluateableProposition::CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p){ |
152 | - CardinalityParameter *param = new CardinalityParameter(); |
153 | + CardinalityParameter *param = new CardinalityParameter(); |
154 | + while(parameter_str.substr(0,1).compare(" ")==0){ |
155 | + parameter_str = parameter_str.substr(1); |
156 | + } |
157 | + //std::cout<<"ParamString: "<<parameter_str<<"\n"<<std::flush; |
158 | + |
159 | + ParameterHolder* typeHolder = new ParameterHolder(); |
160 | + if(parameter_str.substr(0,11).compare("integer-sum")==0){ |
161 | + typeHolder->type = SUM; |
162 | + typeHolder->body = parameter_str.substr(11); |
163 | + } |
164 | + else if(parameter_str.substr(0,15).compare("integer-product")==0){ |
165 | + typeHolder->type = PRODUCT; |
166 | + typeHolder->body = parameter_str.substr(15); |
167 | + } |
168 | + else if(parameter_str.substr(0,18).compare("integer-difference")==0){ |
169 | + typeHolder->type = DIFF; |
170 | + typeHolder->body = parameter_str.substr(18); |
171 | + } |
172 | + else if(parameter_str.substr(0,16).compare("integer-constant")==0){ |
173 | + typeHolder->type = CONST; |
174 | + typeHolder->body = parameter_str.substr(16); |
175 | + } |
176 | + else if(parameter_str.substr(0,12).compare("tokens-count")==0){ |
177 | + typeHolder->type = PLACE; |
178 | + typeHolder->body = parameter_str.substr(12); |
179 | + } |
180 | + else{ |
181 | + std::cerr << "Error: Internal parse error - \"" << parameter_str <<"\" has unrecognized beginning." << std::endl; |
182 | + exit(EXIT_FAILURE); |
183 | + } |
184 | + |
185 | + std::size_t found = typeHolder->body.find_last_of(")"); |
186 | + parameter_str = typeHolder->body.substr(1,found-1); |
187 | + |
188 | + if(typeHolder->type != CONST && typeHolder->type != PLACE){ |
189 | + std::size_t end_of_first = GetEndingParamIndex(parameter_str) + 1; |
190 | + param->isArithmetic = true; |
191 | + param->arithmetictype = typeHolder->type; |
192 | + param->arithmA = CreateParameter(parameter_str.substr(0,end_of_first), p_names, numberof_p); |
193 | + param->arithmB = CreateParameter(parameter_str.substr(end_of_first + 2), p_names, numberof_p); |
194 | + return param; |
195 | + } |
196 | + |
197 | + |
198 | char c; |
199 | if(sscanf(parameter_str.c_str(), "%d%c", ¶m->value, &c) == 1) { |
200 | //If string is identifier starting with a number, you will read two items. |
201 | @@ -178,8 +223,30 @@ |
202 | return param; |
203 | } |
204 | |
205 | +std::size_t EvaluateableProposition::GetEndingParamIndex(std::string param_str){ |
206 | + size_t pos = param_str.find('('); |
207 | + size_t start_count =1; |
208 | + size_t end_count =0; |
209 | + std::string temp = param_str.substr(pos+1); |
210 | + while(start_count != end_count){ |
211 | + size_t new_pos = 0; |
212 | + if(temp.find('(') < temp.find(')')){ |
213 | + start_count++; |
214 | + new_pos = temp.find('(') + 1; |
215 | + } |
216 | + else{ |
217 | + end_count++; |
218 | + new_pos = temp.find(')') + 1; |
219 | + } |
220 | + pos = pos + new_pos; |
221 | + temp = temp.substr(new_pos); |
222 | + } |
223 | + |
224 | + return pos; |
225 | +} |
226 | + |
227 | LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){ |
228 | - std::string loperator_str = atom_str.substr(atom_str.find(')') + 1); |
229 | + std::string loperator_str = atom_str.substr(atom_str.find('}') + 1); |
230 | loperator_str = loperator_str.substr(0, 4); |
231 | if(loperator_str.compare(" le ")== 0) |
232 | return LEQ; |
233 | @@ -206,22 +273,60 @@ |
234 | return fire_str + ")"; |
235 | } |
236 | else if (_type == CARDINALITY){ |
237 | - std::string cardi_str = "("; |
238 | - if(_firstParameter->isPlace) |
239 | - cardi_str = cardi_str + "place(" + patch::to_string(_firstParameter->value) + ")"; |
240 | - else |
241 | - cardi_str = cardi_str = patch::to_string(_firstParameter->value); |
242 | - |
243 | - cardi_str = cardi_str + " loperator "; |
244 | - |
245 | - if(_secondParameter->isPlace) |
246 | - cardi_str = cardi_str + "place(" + patch::to_string(_secondParameter->value) + ")"; |
247 | - else |
248 | - cardi_str = cardi_str = patch::to_string(_secondParameter->value); |
249 | - return cardi_str + ")"; |
250 | + return Parameter_tostring(_firstParameter) + Loperator_tostring() + Parameter_tostring(_secondParameter); |
251 | + } |
252 | + std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl; |
253 | + exit(EXIT_FAILURE); |
254 | +} |
255 | + |
256 | + |
257 | +std::string EvaluateableProposition::Parameter_tostring(CardinalityParameter* param){ |
258 | + std::string cardi_str = ""; |
259 | + if(param->isPlace){ |
260 | + cardi_str = cardi_str + "place("; |
261 | + int i = 0; |
262 | + while(i != param->places_i.size()){ |
263 | + cardi_str = cardi_str + patch::to_string(param->places_i[i]); |
264 | + |
265 | + if(++i < param->places_i.size()){ |
266 | + cardi_str = cardi_str + ", "; |
267 | + } |
268 | + } |
269 | + cardi_str = cardi_str + ")"; |
270 | + } |
271 | + else if(param->isArithmetic){ |
272 | + std::string arthm_ope = ""; |
273 | + if(param->arithmetictype == SUM) |
274 | + arthm_ope = " + "; |
275 | + else if (param->arithmetictype == PRODUCT) |
276 | + arthm_ope = " * "; |
277 | + else if (param->arithmetictype == DIFF) |
278 | + arthm_ope = " - "; |
279 | + else { |
280 | + std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl; |
281 | + exit(EXIT_FAILURE); |
282 | + } |
283 | + cardi_str = cardi_str + Parameter_tostring(param->arithmA) + arthm_ope + Parameter_tostring(param->arithmB); |
284 | } |
285 | else |
286 | - std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl; |
287 | + cardi_str = cardi_str = patch::to_string(param->value); |
288 | + return cardi_str; |
289 | +} |
290 | + |
291 | +std::string EvaluateableProposition::Loperator_tostring(){ |
292 | + if(_loperator == LEQ) |
293 | + return " <= "; |
294 | + else if (_loperator == GRQ) |
295 | + return " >= "; |
296 | + else if (_loperator == EQ) |
297 | + return " == "; |
298 | + else if (_loperator == GR) |
299 | + return " > "; |
300 | + else if (_loperator == LE) |
301 | + return " < "; |
302 | + else if (_loperator == NE) |
303 | + return " != "; |
304 | + else std::cerr << "Error: Could not convert loperator to string" << std::endl; |
305 | exit(EXIT_FAILURE); |
306 | } |
307 | |
308 | |
309 | === modified file 'CTL/CTLParser/EvaluateableProposition.h' |
310 | --- CTL/CTLParser/EvaluateableProposition.h 2017-02-08 19:14:47 +0000 |
311 | +++ CTL/CTLParser/EvaluateableProposition.h 2017-06-22 19:33:43 +0000 |
312 | @@ -18,12 +18,22 @@ |
313 | |
314 | |
315 | enum PropositionType {PropError = -1, CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2}; |
316 | +enum ArithmeticType {NON = -1, SUM = 0, PRODUCT = 1, DIFF = 2, CONST = 3, PLACE = 4}; |
317 | enum LoperatorType {LopError = -1, NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4, NE = 5}; |
318 | |
319 | +struct ParameterHolder{ |
320 | + ArithmeticType type = NON; |
321 | + std::string body = ""; |
322 | +}; |
323 | + |
324 | struct CardinalityParameter{ |
325 | bool isPlace = false; |
326 | + bool isArithmetic = false; |
327 | int value = -1; |
328 | std::vector<int> places_i; |
329 | + ArithmeticType arithmetictype = NON; |
330 | + CardinalityParameter* arithmA; |
331 | + CardinalityParameter* arithmB; |
332 | }; |
333 | |
334 | class EvaluateableProposition { |
335 | @@ -39,6 +49,7 @@ |
336 | private: |
337 | void SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t); |
338 | CardinalityParameter* CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p); |
339 | + std::size_t GetEndingParamIndex(std::string parameter_str); |
340 | LoperatorType SetLoperator(std::string atom_str); |
341 | |
342 | PropositionType _type = PropError; |
343 | @@ -46,6 +57,8 @@ |
344 | std::vector<int> _fireset; |
345 | CardinalityParameter* _firstParameter = nullptr; |
346 | CardinalityParameter* _secondParameter = nullptr; |
347 | + std::string Parameter_tostring(CardinalityParameter *param); |
348 | + std::string Loperator_tostring(); |
349 | |
350 | }; |
351 | |
352 | |
353 | === modified file 'CTL/PetriNets/OnTheFlyDG.cpp' |
354 | --- CTL/PetriNets/OnTheFlyDG.cpp 2017-04-11 19:03:34 +0000 |
355 | +++ CTL/PetriNets/OnTheFlyDG.cpp 2017-06-22 19:33:43 +0000 |
356 | @@ -395,9 +395,22 @@ |
357 | } |
358 | return res; |
359 | } |
360 | - else{ |
361 | - return param->value; |
362 | + else if(param->isArithmetic){ |
363 | + if(param->arithmetictype == NON){ |
364 | + std::cerr << "Error: Arithmetic param is not assigned a type"<< std::endl; |
365 | + exit(EXIT_FAILURE); |
366 | + } |
367 | + else if(param->arithmetictype == SUM){ |
368 | + return GetParamValue(param->arithmA, marking) + GetParamValue(param->arithmB, marking); |
369 | + } |
370 | + else if(param->arithmetictype == PRODUCT){ |
371 | + return GetParamValue(param->arithmA, marking) * GetParamValue(param->arithmB, marking); |
372 | + } |
373 | + else if(param->arithmetictype == DIFF){ |
374 | + return GetParamValue(param->arithmA, marking) - GetParamValue(param->arithmB, marking); |
375 | + } |
376 | } |
377 | + return param->value; |
378 | } |
379 | |
380 | bool OnTheFlyDG::EvalCardianlity(int a, LoperatorType lop, int b) { |
381 | |
382 | === modified file 'PetriEngine/SuccessorGenerator.cpp' |
383 | --- PetriEngine/SuccessorGenerator.cpp 2017-03-05 16:08:26 +0000 |
384 | +++ PetriEngine/SuccessorGenerator.cpp 2017-06-22 19:33:43 +0000 |
385 | @@ -39,7 +39,9 @@ |
386 | uint32_t finv = ptr.inputs; |
387 | uint32_t linv = ptr.outputs; |
388 | for (; finv < linv; ++finv) { |
389 | - write.marking()[_net._invariants[finv].place] -= _net._invariants[finv].tokens; |
390 | + if(!_net._invariants[finv].inhibitor) { |
391 | + write.marking()[_net._invariants[finv].place] -= _net._invariants[finv].tokens; |
392 | + } |
393 | } |
394 | } |
395 | |
396 | |
397 | === modified file 'PetriParse/QueryXMLParser.cpp' |
398 | --- PetriParse/QueryXMLParser.cpp 2017-04-09 15:12:50 +0000 |
399 | +++ PetriParse/QueryXMLParser.cpp 2017-06-22 19:33:43 +0000 |
400 | @@ -386,8 +386,8 @@ |
401 | Expr_ptr child = parseIntegerExpression(it); |
402 | if(child == NULL) return NULL; |
403 | expr = isMult ? |
404 | - (Expr_ptr)std::make_shared<PlusExpr>(expr, child) : |
405 | - (Expr_ptr)std::make_shared<MultiplyExpr>(expr, child); |
406 | + (Expr_ptr)std::make_shared<MultiplyExpr>(expr, child): |
407 | + (Expr_ptr)std::make_shared<PlusExpr>(expr, child); |
408 | } |
409 | return expr; |
410 | } else if (elementName == "integer-difference") { |
I can see some problems when parsing the expressions.
A query in the GUI is:
EF N.P0 * N.P1 + N.P2 * N.P2 - N.P4 = 0
and your engine prints it as:
Query before reduction: AG (((P0 + P1) * ((P2 + P2) - P4)) == 0)
but the XML query output seems correct:
<exists-path>
<integer- eq>
<integer- sum>
<integer- product>
<tokens- count>
<place> P0</place>
</tokens- count>
<tokens- count>
<place> P1</place>
</tokens- count>
</integer- product>
<integer- difference>
<integer- product>
<tokens- count>
< place>P2< /place>
</tokens- count>
<tokens- count>
< place>P2< /place>
</tokens- count>
</integer- product>
<tokens- count>
<place> P4</place>
</tokens- count>
</integer- difference>
</ integer- sum>
<integer- constant> 0</integer- constant>
</integer- eq> /exists- path>
<finally>
</finally>
<