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 | 344 | if (firstLetter == 'a') { | 344 | if (firstLetter == 'a') { |
6 | 345 | //Construct all-paths | 345 | //Construct all-paths |
7 | 346 | query = new CTLQuery(A, getPathOperator(root), false, ""); | 346 | query = new CTLQuery(A, getPathOperator(root), false, ""); |
9 | 347 | assert(query->GetQuantifier() == A && "Failed setting quantifier"); | 347 | if(query->GetQuantifier() != A){ |
10 | 348 | std::cerr << "Error: Failed setting all operator." << std::endl; | ||
11 | 349 | exit(EXIT_FAILURE); | ||
12 | 350 | } | ||
13 | 348 | } | 351 | } |
14 | 349 | else if (firstLetter == 'e' ) { | 352 | else if (firstLetter == 'e' ) { |
15 | 350 | //Construct exists-path | 353 | //Construct exists-path |
16 | 351 | query = new CTLQuery(E, getPathOperator(root), false, ""); | 354 | query = new CTLQuery(E, getPathOperator(root), false, ""); |
18 | 352 | assert(query->GetQuantifier() == E && "Failed setting path operator"); | 355 | if(query->GetQuantifier() != E){ |
19 | 356 | std::cerr << "Error: Failed setting exists operator." << std::endl; | ||
20 | 357 | exit(EXIT_FAILURE); | ||
21 | 358 | } | ||
22 | 353 | } | 359 | } |
23 | 354 | else if (firstLetter == 'n' ) { | 360 | else if (firstLetter == 'n' ) { |
24 | 355 | //Construct negation | 361 | //Construct negation |
25 | 356 | query = new CTLQuery(NEG, pError, false, ""); | 362 | query = new CTLQuery(NEG, pError, false, ""); |
27 | 357 | assert(query->GetQuantifier() == NEG && "Failed setting negation operator"); | 363 | if(query->GetQuantifier() != NEG){ |
28 | 364 | std::cerr << "Error: Failed setting negation operator." << std::endl; | ||
29 | 365 | exit(EXIT_FAILURE); | ||
30 | 366 | } | ||
31 | 358 | } | 367 | } |
32 | 359 | else if (firstLetter == 'c' ) { | 368 | else if (firstLetter == 'c' ) { |
33 | 360 | //Construct conjunction | 369 | //Construct conjunction |
34 | 361 | query = new CTLQuery(AND, pError, false, ""); | 370 | query = new CTLQuery(AND, pError, false, ""); |
36 | 362 | assert(query->GetQuantifier() == AND && "Failed setting and operator"); | 371 | if(query->GetQuantifier() != AND){ |
37 | 372 | std::cerr << "Error: Failed setting and operator." << std::endl; | ||
38 | 373 | exit(EXIT_FAILURE); | ||
39 | 374 | } | ||
40 | 363 | } | 375 | } |
41 | 364 | else if (firstLetter == 'd' ) { | 376 | else if (firstLetter == 'd' ) { |
42 | 365 | if( root_name[1] == 'i' ){ | 377 | if( root_name[1] == 'i' ){ |
43 | 366 | //Construct disjunction | 378 | //Construct disjunction |
44 | 367 | query = new CTLQuery(OR, pError, false, ""); | 379 | query = new CTLQuery(OR, pError, false, ""); |
46 | 368 | assert(query->GetQuantifier() == OR && "Failed setting or operator"); | 380 | if(query->GetQuantifier() != OR){ |
47 | 381 | std::cerr << "Error: Failed setting or operator." << std::endl; | ||
48 | 382 | exit(EXIT_FAILURE); | ||
49 | 383 | } | ||
50 | 369 | } | 384 | } |
51 | 370 | else if (root_name[1] == 'e'){ | 385 | else if (root_name[1] == 'e'){ |
52 | 371 | //Deadlock query | 386 | //Deadlock query |
53 | @@ -403,7 +418,7 @@ | |||
54 | 403 | 418 | ||
55 | 404 | loperator = loperator_sym(loperator); | 419 | loperator = loperator_sym(loperator); |
56 | 405 | 420 | ||
58 | 406 | atom_str = first + loperator + second; | 421 | atom_str = first + "}" + loperator + "{" + second; |
59 | 407 | 422 | ||
60 | 408 | } | 423 | } |
61 | 409 | else { | 424 | else { |
62 | @@ -512,9 +527,18 @@ | |||
63 | 512 | parameter_str = parameter_str + ")"; | 527 | parameter_str = parameter_str + ")"; |
64 | 513 | } | 528 | } |
65 | 514 | 529 | ||
67 | 515 | else if(parameter->name()[0] == 'i'){ | 530 | else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'c'){ |
68 | 516 | parameter_str = parameter_str + choppy(parameter->value()) + ")"; | 531 | parameter_str = parameter_str + choppy(parameter->value()) + ")"; |
69 | 517 | } | 532 | } |
70 | 533 | else if(parameter->name()[0] == 'i' && parameter->name()[8] == 's'){ | ||
71 | 534 | parameter_str = parameter_str + parsePar(parameter->first_node()) + " + " + parsePar(parameter->first_node()->next_sibling()) + ")"; | ||
72 | 535 | } | ||
73 | 536 | else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'p'){ | ||
74 | 537 | parameter_str = parameter_str + parsePar(parameter->first_node()) + " * " + parsePar(parameter->first_node()->next_sibling()) + ")"; | ||
75 | 538 | } | ||
76 | 539 | else if(parameter->name()[0] == 'i' && parameter->name()[8] == 'd'){ | ||
77 | 540 | parameter_str = parameter_str + parsePar(parameter->first_node()) + " - " + parsePar(parameter->first_node()->next_sibling()) + ")"; | ||
78 | 541 | } | ||
79 | 518 | else { | 542 | else { |
80 | 519 | std::cerr << "Error: Failed parsing query file provided. Incorrect format around the parameter: " << parameter->name() << ". Please check spelling." << std::endl; | 543 | std::cerr << "Error: Failed parsing query file provided. Incorrect format around the parameter: " << parameter->name() << ". Please check spelling." << std::endl; |
81 | 520 | exit(EXIT_FAILURE); | 544 | exit(EXIT_FAILURE); |
82 | 521 | 545 | ||
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 | 134 | 134 | ||
88 | 135 | std::string CTLQuery::ToString(){ | 135 | std::string CTLQuery::ToString(){ |
89 | 136 | if(_hasAtom){ | 136 | if(_hasAtom){ |
91 | 137 | return _a; | 137 | return _proposition->ToString(); |
92 | 138 | } | 138 | } |
93 | 139 | else if(_q == AND){ | 139 | else if(_q == AND){ |
94 | 140 | return "(" + _firstchild->ToString() + " & " + _secondchild->ToString() + ")"; | 140 | return "(" + _firstchild->ToString() + " & " + _secondchild->ToString() + ")"; |
95 | @@ -152,13 +152,13 @@ | |||
96 | 152 | } | 152 | } |
97 | 153 | else quanti = "E"; | 153 | else quanti = "E"; |
98 | 154 | if(_path == F){ | 154 | if(_path == F){ |
100 | 155 | return quanti + "F" + _firstchild->ToString(); | 155 | return quanti + "F " + _firstchild->ToString(); |
101 | 156 | } | 156 | } |
102 | 157 | else if(_path == G){ | 157 | else if(_path == G){ |
104 | 158 | return quanti + "G" + _firstchild->ToString(); | 158 | return quanti + "G " + _firstchild->ToString(); |
105 | 159 | } | 159 | } |
106 | 160 | else if(_path == X){ | 160 | else if(_path == X){ |
108 | 161 | return quanti + "X" + _firstchild->ToString(); | 161 | return quanti + "X " + _firstchild->ToString(); |
109 | 162 | } | 162 | } |
110 | 163 | else if(_path == U){ | 163 | else if(_path == U){ |
111 | 164 | return quanti + "(" + _firstchild->ToString() + ") U (" + _secondchild->ToString() + ")"; | 164 | return quanti + "(" + _firstchild->ToString() + ") U (" + _secondchild->ToString() + ")"; |
112 | 165 | 165 | ||
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 | 37 | _loperator = SetLoperator(a); | 37 | _loperator = SetLoperator(a); |
118 | 38 | assert(_loperator != NOT_CARDINALITY); | 38 | assert(_loperator != NOT_CARDINALITY); |
119 | 39 | 39 | ||
124 | 40 | size_t begin = a.find('(') + 1; | 40 | //size_t begin = a.find('(') + 1; |
125 | 41 | size_t end = a.find(')') - begin; | 41 | size_t end = a.find('}'); |
126 | 42 | std::string first_parameter_str = a.substr(begin, end); | 42 | std::string first_parameter_str = a.substr(0, end); |
127 | 43 | a = a.substr(a.find(')') + 1); | 43 | a = a.substr(a.find('}') + 1); |
128 | 44 | 44 | ||
132 | 45 | begin = a.find('(') + 1; | 45 | size_t begin = a.find('{') + 1; |
133 | 46 | end = a.find(')') - begin; | 46 | //end = a.find(')') - begin; |
134 | 47 | std::string second_parameter_str = a.substr(begin, end); | 47 | std::string second_parameter_str = a.substr(begin); |
135 | 48 | _firstParameter = CreateParameter(first_parameter_str, net->placeNames(), net->numberOfPlaces()); | 48 | _firstParameter = CreateParameter(first_parameter_str, net->placeNames(), net->numberOfPlaces()); |
136 | 49 | _secondParameter = CreateParameter(second_parameter_str, net->placeNames(), net->numberOfPlaces()); | 49 | _secondParameter = CreateParameter(second_parameter_str, net->placeNames(), net->numberOfPlaces()); |
137 | 50 | } | 50 | } |
138 | @@ -90,7 +90,8 @@ | |||
139 | 90 | SetFireset("all", net->transitionNames(), net->numberOfTransitions()); | 90 | SetFireset("all", net->transitionNames(), net->numberOfTransitions()); |
140 | 91 | } | 91 | } |
141 | 92 | else{ | 92 | else{ |
143 | 93 | assert(false && "Atomic string proposed for proposition could not be parsed"); | 93 | std::cerr << "Error: Could not identify Evaluateable Proposition type from atom string: "<<a<<"." << std::endl; |
144 | 94 | exit(EXIT_FAILURE); | ||
145 | 94 | } | 95 | } |
146 | 95 | } | 96 | } |
147 | 96 | 97 | ||
148 | @@ -139,7 +140,51 @@ | |||
149 | 139 | } | 140 | } |
150 | 140 | 141 | ||
151 | 141 | CardinalityParameter* EvaluateableProposition::CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p){ | 142 | CardinalityParameter* EvaluateableProposition::CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p){ |
153 | 142 | CardinalityParameter *param = new CardinalityParameter(); | 143 | CardinalityParameter *param = new CardinalityParameter(); |
154 | 144 | while(parameter_str.substr(0,1).compare(" ")==0){ | ||
155 | 145 | parameter_str = parameter_str.substr(1); | ||
156 | 146 | } | ||
157 | 147 | //std::cout<<"ParamString: "<<parameter_str<<"\n"<<std::flush; | ||
158 | 148 | |||
159 | 149 | ParameterHolder* typeHolder = new ParameterHolder(); | ||
160 | 150 | if(parameter_str.substr(0,11).compare("integer-sum")==0){ | ||
161 | 151 | typeHolder->type = SUM; | ||
162 | 152 | typeHolder->body = parameter_str.substr(11); | ||
163 | 153 | } | ||
164 | 154 | else if(parameter_str.substr(0,15).compare("integer-product")==0){ | ||
165 | 155 | typeHolder->type = PRODUCT; | ||
166 | 156 | typeHolder->body = parameter_str.substr(15); | ||
167 | 157 | } | ||
168 | 158 | else if(parameter_str.substr(0,18).compare("integer-difference")==0){ | ||
169 | 159 | typeHolder->type = DIFF; | ||
170 | 160 | typeHolder->body = parameter_str.substr(18); | ||
171 | 161 | } | ||
172 | 162 | else if(parameter_str.substr(0,16).compare("integer-constant")==0){ | ||
173 | 163 | typeHolder->type = CONST; | ||
174 | 164 | typeHolder->body = parameter_str.substr(16); | ||
175 | 165 | } | ||
176 | 166 | else if(parameter_str.substr(0,12).compare("tokens-count")==0){ | ||
177 | 167 | typeHolder->type = PLACE; | ||
178 | 168 | typeHolder->body = parameter_str.substr(12); | ||
179 | 169 | } | ||
180 | 170 | else{ | ||
181 | 171 | std::cerr << "Error: Internal parse error - \"" << parameter_str <<"\" has unrecognized beginning." << std::endl; | ||
182 | 172 | exit(EXIT_FAILURE); | ||
183 | 173 | } | ||
184 | 174 | |||
185 | 175 | std::size_t found = typeHolder->body.find_last_of(")"); | ||
186 | 176 | parameter_str = typeHolder->body.substr(1,found-1); | ||
187 | 177 | |||
188 | 178 | if(typeHolder->type != CONST && typeHolder->type != PLACE){ | ||
189 | 179 | std::size_t end_of_first = GetEndingParamIndex(parameter_str) + 1; | ||
190 | 180 | param->isArithmetic = true; | ||
191 | 181 | param->arithmetictype = typeHolder->type; | ||
192 | 182 | param->arithmA = CreateParameter(parameter_str.substr(0,end_of_first), p_names, numberof_p); | ||
193 | 183 | param->arithmB = CreateParameter(parameter_str.substr(end_of_first + 2), p_names, numberof_p); | ||
194 | 184 | return param; | ||
195 | 185 | } | ||
196 | 186 | |||
197 | 187 | |||
198 | 143 | char c; | 188 | char c; |
199 | 144 | if(sscanf(parameter_str.c_str(), "%d%c", ¶m->value, &c) == 1) { | 189 | if(sscanf(parameter_str.c_str(), "%d%c", ¶m->value, &c) == 1) { |
200 | 145 | //If string is identifier starting with a number, you will read two items. | 190 | //If string is identifier starting with a number, you will read two items. |
201 | @@ -178,8 +223,30 @@ | |||
202 | 178 | return param; | 223 | return param; |
203 | 179 | } | 224 | } |
204 | 180 | 225 | ||
205 | 226 | std::size_t EvaluateableProposition::GetEndingParamIndex(std::string param_str){ | ||
206 | 227 | size_t pos = param_str.find('('); | ||
207 | 228 | size_t start_count =1; | ||
208 | 229 | size_t end_count =0; | ||
209 | 230 | std::string temp = param_str.substr(pos+1); | ||
210 | 231 | while(start_count != end_count){ | ||
211 | 232 | size_t new_pos = 0; | ||
212 | 233 | if(temp.find('(') < temp.find(')')){ | ||
213 | 234 | start_count++; | ||
214 | 235 | new_pos = temp.find('(') + 1; | ||
215 | 236 | } | ||
216 | 237 | else{ | ||
217 | 238 | end_count++; | ||
218 | 239 | new_pos = temp.find(')') + 1; | ||
219 | 240 | } | ||
220 | 241 | pos = pos + new_pos; | ||
221 | 242 | temp = temp.substr(new_pos); | ||
222 | 243 | } | ||
223 | 244 | |||
224 | 245 | return pos; | ||
225 | 246 | } | ||
226 | 247 | |||
227 | 181 | LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){ | 248 | LoperatorType EvaluateableProposition::SetLoperator(std::string atom_str){ |
229 | 182 | std::string loperator_str = atom_str.substr(atom_str.find(')') + 1); | 249 | std::string loperator_str = atom_str.substr(atom_str.find('}') + 1); |
230 | 183 | loperator_str = loperator_str.substr(0, 4); | 250 | loperator_str = loperator_str.substr(0, 4); |
231 | 184 | if(loperator_str.compare(" le ")== 0) | 251 | if(loperator_str.compare(" le ")== 0) |
232 | 185 | return LEQ; | 252 | return LEQ; |
233 | @@ -206,22 +273,60 @@ | |||
234 | 206 | return fire_str + ")"; | 273 | return fire_str + ")"; |
235 | 207 | } | 274 | } |
236 | 208 | else if (_type == CARDINALITY){ | 275 | else if (_type == CARDINALITY){ |
250 | 209 | std::string cardi_str = "("; | 276 | return Parameter_tostring(_firstParameter) + Loperator_tostring() + Parameter_tostring(_secondParameter); |
251 | 210 | if(_firstParameter->isPlace) | 277 | } |
252 | 211 | cardi_str = cardi_str + "place(" + patch::to_string(_firstParameter->value) + ")"; | 278 | std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl; |
253 | 212 | else | 279 | exit(EXIT_FAILURE); |
254 | 213 | cardi_str = cardi_str = patch::to_string(_firstParameter->value); | 280 | } |
255 | 214 | 281 | ||
256 | 215 | cardi_str = cardi_str + " loperator "; | 282 | |
257 | 216 | 283 | std::string EvaluateableProposition::Parameter_tostring(CardinalityParameter* param){ | |
258 | 217 | if(_secondParameter->isPlace) | 284 | std::string cardi_str = ""; |
259 | 218 | cardi_str = cardi_str + "place(" + patch::to_string(_secondParameter->value) + ")"; | 285 | if(param->isPlace){ |
260 | 219 | else | 286 | cardi_str = cardi_str + "place("; |
261 | 220 | cardi_str = cardi_str = patch::to_string(_secondParameter->value); | 287 | int i = 0; |
262 | 221 | return cardi_str + ")"; | 288 | while(i != param->places_i.size()){ |
263 | 289 | cardi_str = cardi_str + patch::to_string(param->places_i[i]); | ||
264 | 290 | |||
265 | 291 | if(++i < param->places_i.size()){ | ||
266 | 292 | cardi_str = cardi_str + ", "; | ||
267 | 293 | } | ||
268 | 294 | } | ||
269 | 295 | cardi_str = cardi_str + ")"; | ||
270 | 296 | } | ||
271 | 297 | else if(param->isArithmetic){ | ||
272 | 298 | std::string arthm_ope = ""; | ||
273 | 299 | if(param->arithmetictype == SUM) | ||
274 | 300 | arthm_ope = " + "; | ||
275 | 301 | else if (param->arithmetictype == PRODUCT) | ||
276 | 302 | arthm_ope = " * "; | ||
277 | 303 | else if (param->arithmetictype == DIFF) | ||
278 | 304 | arthm_ope = " - "; | ||
279 | 305 | else { | ||
280 | 306 | std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl; | ||
281 | 307 | exit(EXIT_FAILURE); | ||
282 | 308 | } | ||
283 | 309 | cardi_str = cardi_str + Parameter_tostring(param->arithmA) + arthm_ope + Parameter_tostring(param->arithmB); | ||
284 | 222 | } | 310 | } |
285 | 223 | else | 311 | else |
287 | 224 | std::cerr << "Error: An unknown error occured while converting a proposition to string. " << std::endl; | 312 | cardi_str = cardi_str = patch::to_string(param->value); |
288 | 313 | return cardi_str; | ||
289 | 314 | } | ||
290 | 315 | |||
291 | 316 | std::string EvaluateableProposition::Loperator_tostring(){ | ||
292 | 317 | if(_loperator == LEQ) | ||
293 | 318 | return " <= "; | ||
294 | 319 | else if (_loperator == GRQ) | ||
295 | 320 | return " >= "; | ||
296 | 321 | else if (_loperator == EQ) | ||
297 | 322 | return " == "; | ||
298 | 323 | else if (_loperator == GR) | ||
299 | 324 | return " > "; | ||
300 | 325 | else if (_loperator == LE) | ||
301 | 326 | return " < "; | ||
302 | 327 | else if (_loperator == NE) | ||
303 | 328 | return " != "; | ||
304 | 329 | else std::cerr << "Error: Could not convert loperator to string" << std::endl; | ||
305 | 225 | exit(EXIT_FAILURE); | 330 | exit(EXIT_FAILURE); |
306 | 226 | } | 331 | } |
307 | 227 | 332 | ||
308 | 228 | 333 | ||
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 | 18 | 18 | ||
314 | 19 | 19 | ||
315 | 20 | enum PropositionType {PropError = -1, CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2}; | 20 | enum PropositionType {PropError = -1, CARDINALITY = 0, FIREABILITY = 1, DEADLOCK = 2}; |
316 | 21 | enum ArithmeticType {NON = -1, SUM = 0, PRODUCT = 1, DIFF = 2, CONST = 3, PLACE = 4}; | ||
317 | 21 | enum LoperatorType {LopError = -1, NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4, NE = 5}; | 22 | enum LoperatorType {LopError = -1, NOT_CARDINALITY = -1, EQ = 0, LE = 1, LEQ = 2, GR = 3, GRQ = 4, NE = 5}; |
318 | 22 | 23 | ||
319 | 24 | struct ParameterHolder{ | ||
320 | 25 | ArithmeticType type = NON; | ||
321 | 26 | std::string body = ""; | ||
322 | 27 | }; | ||
323 | 28 | |||
324 | 23 | struct CardinalityParameter{ | 29 | struct CardinalityParameter{ |
325 | 24 | bool isPlace = false; | 30 | bool isPlace = false; |
326 | 31 | bool isArithmetic = false; | ||
327 | 25 | int value = -1; | 32 | int value = -1; |
328 | 26 | std::vector<int> places_i; | 33 | std::vector<int> places_i; |
329 | 34 | ArithmeticType arithmetictype = NON; | ||
330 | 35 | CardinalityParameter* arithmA; | ||
331 | 36 | CardinalityParameter* arithmB; | ||
332 | 27 | }; | 37 | }; |
333 | 28 | 38 | ||
334 | 29 | class EvaluateableProposition { | 39 | class EvaluateableProposition { |
335 | @@ -39,6 +49,7 @@ | |||
336 | 39 | private: | 49 | private: |
337 | 40 | void SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t); | 50 | void SetFireset(std::string fireset_str, std::vector<std::string> t_names, unsigned int numberof_t); |
338 | 41 | CardinalityParameter* CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p); | 51 | CardinalityParameter* CreateParameter(std::string parameter_str, std::vector<std::string> p_names, unsigned int numberof_p); |
339 | 52 | std::size_t GetEndingParamIndex(std::string parameter_str); | ||
340 | 42 | LoperatorType SetLoperator(std::string atom_str); | 53 | LoperatorType SetLoperator(std::string atom_str); |
341 | 43 | 54 | ||
342 | 44 | PropositionType _type = PropError; | 55 | PropositionType _type = PropError; |
343 | @@ -46,6 +57,8 @@ | |||
344 | 46 | std::vector<int> _fireset; | 57 | std::vector<int> _fireset; |
345 | 47 | CardinalityParameter* _firstParameter = nullptr; | 58 | CardinalityParameter* _firstParameter = nullptr; |
346 | 48 | CardinalityParameter* _secondParameter = nullptr; | 59 | CardinalityParameter* _secondParameter = nullptr; |
347 | 60 | std::string Parameter_tostring(CardinalityParameter *param); | ||
348 | 61 | std::string Loperator_tostring(); | ||
349 | 49 | 62 | ||
350 | 50 | }; | 63 | }; |
351 | 51 | 64 | ||
352 | 52 | 65 | ||
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 | 395 | } | 395 | } |
358 | 396 | return res; | 396 | return res; |
359 | 397 | } | 397 | } |
362 | 398 | else{ | 398 | else if(param->isArithmetic){ |
363 | 399 | return param->value; | 399 | if(param->arithmetictype == NON){ |
364 | 400 | std::cerr << "Error: Arithmetic param is not assigned a type"<< std::endl; | ||
365 | 401 | exit(EXIT_FAILURE); | ||
366 | 402 | } | ||
367 | 403 | else if(param->arithmetictype == SUM){ | ||
368 | 404 | return GetParamValue(param->arithmA, marking) + GetParamValue(param->arithmB, marking); | ||
369 | 405 | } | ||
370 | 406 | else if(param->arithmetictype == PRODUCT){ | ||
371 | 407 | return GetParamValue(param->arithmA, marking) * GetParamValue(param->arithmB, marking); | ||
372 | 408 | } | ||
373 | 409 | else if(param->arithmetictype == DIFF){ | ||
374 | 410 | return GetParamValue(param->arithmA, marking) - GetParamValue(param->arithmB, marking); | ||
375 | 411 | } | ||
376 | 400 | } | 412 | } |
377 | 413 | return param->value; | ||
378 | 401 | } | 414 | } |
379 | 402 | 415 | ||
380 | 403 | bool OnTheFlyDG::EvalCardianlity(int a, LoperatorType lop, int b) { | 416 | bool OnTheFlyDG::EvalCardianlity(int a, LoperatorType lop, int b) { |
381 | 404 | 417 | ||
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 | 39 | uint32_t finv = ptr.inputs; | 39 | uint32_t finv = ptr.inputs; |
387 | 40 | uint32_t linv = ptr.outputs; | 40 | uint32_t linv = ptr.outputs; |
388 | 41 | for (; finv < linv; ++finv) { | 41 | for (; finv < linv; ++finv) { |
390 | 42 | write.marking()[_net._invariants[finv].place] -= _net._invariants[finv].tokens; | 42 | if(!_net._invariants[finv].inhibitor) { |
391 | 43 | write.marking()[_net._invariants[finv].place] -= _net._invariants[finv].tokens; | ||
392 | 44 | } | ||
393 | 43 | } | 45 | } |
394 | 44 | } | 46 | } |
395 | 45 | 47 | ||
396 | 46 | 48 | ||
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 | 386 | Expr_ptr child = parseIntegerExpression(it); | 386 | Expr_ptr child = parseIntegerExpression(it); |
402 | 387 | if(child == NULL) return NULL; | 387 | if(child == NULL) return NULL; |
403 | 388 | expr = isMult ? | 388 | expr = isMult ? |
406 | 389 | (Expr_ptr)std::make_shared<PlusExpr>(expr, child) : | 389 | (Expr_ptr)std::make_shared<MultiplyExpr>(expr, child): |
407 | 390 | (Expr_ptr)std::make_shared<MultiplyExpr>(expr, child); | 390 | (Expr_ptr)std::make_shared<PlusExpr>(expr, child); |
408 | 391 | } | 391 | } |
409 | 392 | return expr; | 392 | return expr; |
410 | 393 | } else if (elementName == "integer-difference") { | 393 | } 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>
<