Merge lp:~tapaal-ltl/verifypn/ruleI.5 into lp:~tapaal-ltl/verifypn/ltl-model-checker
- ruleI.5
- Merge into ltl-model-checker
Proposed by
Simon Virenfeldt
Status: | Merged |
---|---|
Merged at revision: | 252 |
Proposed branch: | lp:~tapaal-ltl/verifypn/ruleI.5 |
Merge into: | lp:~tapaal-ltl/verifypn/ltl-model-checker |
Diff against target: |
375 lines (+171/-122) 3 files modified
include/PetriEngine/Reducer.h (+8/-3) src/PetriEngine/Reducer.cpp (+162/-118) src/VerifyPN.cpp (+1/-1) |
To merge this branch: | bzr merge lp:~tapaal-ltl/verifypn/ruleI.5 |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Nikolaj Jensen Ulrik | Approve | ||
Review via email: mp+398248@code.launchpad.net |
Commit message
Description of the change
Implements the new structural reduction rule K which is a weaker version of rule I tailored to LTL reduction.
To post a comment you must log in.
Revision history for this message
Nikolaj Jensen Ulrik (waefwerf) : | # |
review:
Approve
lp:~tapaal-ltl/verifypn/ruleI.5
updated
- 252. By Simon Virenfeldt
-
Merge lp:~tapaal-ltl/verifypn/ruleI.5@253
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'include/PetriEngine/Reducer.h' | |||
2 | --- include/PetriEngine/Reducer.h 2020-11-26 10:36:20 +0000 | |||
3 | +++ include/PetriEngine/Reducer.h 2021-02-18 12:06:25 +0000 | |||
4 | @@ -110,7 +110,8 @@ | |||
5 | 110 | << "Applications of rule G: " << _ruleG << "\n" | 110 | << "Applications of rule G: " << _ruleG << "\n" |
6 | 111 | << "Applications of rule H: " << _ruleH << "\n" | 111 | << "Applications of rule H: " << _ruleH << "\n" |
7 | 112 | << "Applications of rule I: " << _ruleI << "\n" | 112 | << "Applications of rule I: " << _ruleI << "\n" |
9 | 113 | << "Applications of rule J: " << _ruleJ << std::endl; | 113 | << "Applications of rule J: " << _ruleJ << "\n" |
10 | 114 | << "Applications of rule K: " << _ruleK << std::endl; | ||
11 | 114 | } | 115 | } |
12 | 115 | 116 | ||
13 | 116 | void postFire(std::ostream&, const std::string& transition); | 117 | void postFire(std::ostream&, const std::string& transition); |
14 | @@ -120,7 +121,7 @@ | |||
15 | 120 | private: | 121 | private: |
16 | 121 | size_t _removedTransitions = 0; | 122 | size_t _removedTransitions = 0; |
17 | 122 | size_t _removedPlaces= 0; | 123 | size_t _removedPlaces= 0; |
19 | 123 | size_t _ruleA = 0, _ruleB = 0, _ruleC = 0, _ruleD = 0, _ruleE = 0, _ruleF = 0, _ruleG = 0, _ruleH = 0, _ruleI = 0, _ruleJ = 0; | 124 | size_t _ruleA = 0, _ruleB = 0, _ruleC = 0, _ruleD = 0, _ruleE = 0, _ruleF = 0, _ruleG = 0, _ruleH = 0, _ruleI = 0, _ruleJ = 0, _ruleK = 0; |
20 | 124 | PetriNetBuilder* parent = nullptr; | 125 | PetriNetBuilder* parent = nullptr; |
21 | 125 | bool reconstructTrace = false; | 126 | bool reconstructTrace = false; |
22 | 126 | std::chrono::high_resolution_clock::time_point _timer; | 127 | std::chrono::high_resolution_clock::time_point _timer; |
23 | @@ -137,7 +138,11 @@ | |||
24 | 137 | bool ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers); | 138 | bool ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers); |
25 | 138 | bool ReducebyRuleH(uint32_t* placeInQuery); | 139 | bool ReducebyRuleH(uint32_t* placeInQuery); |
26 | 139 | bool ReducebyRuleJ(uint32_t* placeInQuery); | 140 | bool ReducebyRuleJ(uint32_t* placeInQuery); |
28 | 140 | 141 | bool ReducebyRuleK(uint32_t* placeInQuery, bool remove_consumers); | |
29 | 142 | |||
30 | 143 | std::optional<std::pair<std::vector<bool>, std::vector<bool>>>relevant(const uint32_t* placeInQuery, bool remove_consumers); | ||
31 | 144 | bool remove_irrelevant(const uint32_t* placeInQuery, const std::vector<bool> &tseen, const std::vector<bool> &pseen); | ||
32 | 145 | |||
33 | 141 | std::string getTransitionName(uint32_t transition); | 146 | std::string getTransitionName(uint32_t transition); |
34 | 142 | std::string getPlaceName(uint32_t place); | 147 | std::string getPlaceName(uint32_t place); |
35 | 143 | 148 | ||
36 | 144 | 149 | ||
37 | === modified file 'src/PetriEngine/Reducer.cpp' | |||
38 | --- src/PetriEngine/Reducer.cpp 2020-12-04 11:14:38 +0000 | |||
39 | +++ src/PetriEngine/Reducer.cpp 2021-02-18 12:06:25 +0000 | |||
40 | @@ -903,131 +903,24 @@ | |||
41 | 903 | 903 | ||
42 | 904 | if(skipplace) | 904 | if(skipplace) |
43 | 905 | skipPlace(p); | 905 | skipPlace(p); |
45 | 906 | 906 | ||
46 | 907 | } | 907 | } |
47 | 908 | assert(consistent()); | 908 | assert(consistent()); |
48 | 909 | return continueReductions; | 909 | return continueReductions; |
49 | 910 | } | 910 | } |
51 | 911 | 911 | ||
52 | 912 | bool Reducer::ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) { | 912 | bool Reducer::ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) { |
53 | 913 | bool reduced = false; | 913 | bool reduced = false; |
54 | 914 | if(remove_loops) | 914 | if(remove_loops) |
55 | 915 | { | 915 | { |
171 | 916 | std::vector<uint32_t> wtrans; | 916 | |
172 | 917 | std::vector<bool> tseen(parent->numberOfTransitions(), false); | 917 | auto result = relevant(placeInQuery, remove_consumers); |
173 | 918 | 918 | if (!result) { | |
174 | 919 | for(uint32_t p = 0; p < parent->numberOfPlaces(); ++p) | 919 | return false; |
175 | 920 | { | 920 | } |
176 | 921 | if(hasTimedout()) return false; | 921 | auto[tseen, pseen] = result.value(); |
177 | 922 | if(placeInQuery[p] > 0) | 922 | |
178 | 923 | { | 923 | reduced |= remove_irrelevant(placeInQuery, tseen, pseen); |
64 | 924 | const Place& place = parent->_places[p]; | ||
65 | 925 | for(auto t : place.consumers) | ||
66 | 926 | { | ||
67 | 927 | if(!tseen[t]) | ||
68 | 928 | { | ||
69 | 929 | wtrans.push_back(t); | ||
70 | 930 | tseen[t] = true; | ||
71 | 931 | } | ||
72 | 932 | } | ||
73 | 933 | for(auto t : place.producers) | ||
74 | 934 | { | ||
75 | 935 | if(!tseen[t]) | ||
76 | 936 | { | ||
77 | 937 | wtrans.push_back(t); | ||
78 | 938 | tseen[t] = true; | ||
79 | 939 | } | ||
80 | 940 | } | ||
81 | 941 | } | ||
82 | 942 | } | ||
83 | 943 | |||
84 | 944 | std::vector<bool> pseen(parent->numberOfPlaces(), false); | ||
85 | 945 | while(!wtrans.empty()) | ||
86 | 946 | { | ||
87 | 947 | if(hasTimedout()) return false; | ||
88 | 948 | auto t = wtrans.back(); | ||
89 | 949 | wtrans.pop_back(); | ||
90 | 950 | const Transition& trans = parent->_transitions[t]; | ||
91 | 951 | for(const Arc& arc : trans.pre) | ||
92 | 952 | { | ||
93 | 953 | const Place& place = parent->_places[arc.place]; | ||
94 | 954 | if(arc.inhib) | ||
95 | 955 | { | ||
96 | 956 | for(auto pt : place.consumers) | ||
97 | 957 | { | ||
98 | 958 | if(!tseen[pt]) | ||
99 | 959 | { | ||
100 | 960 | Transition& trans = parent->_transitions[pt]; | ||
101 | 961 | auto it = trans.post.begin(); | ||
102 | 962 | for(; it != trans.post.end(); ++it) | ||
103 | 963 | if(it->place >= arc.place) break; | ||
104 | 964 | if(it != trans.post.end() && it->place == arc.place) | ||
105 | 965 | { | ||
106 | 966 | auto it2 = trans.pre.begin(); | ||
107 | 967 | for(; it2 != trans.pre.end(); ++it2) | ||
108 | 968 | if(it2->place >= arc.place || it2->inhib) break; | ||
109 | 969 | if(it->weight <= it2->weight) continue; | ||
110 | 970 | } | ||
111 | 971 | tseen[pt] = true; | ||
112 | 972 | wtrans.push_back(pt); | ||
113 | 973 | } | ||
114 | 974 | } | ||
115 | 975 | } | ||
116 | 976 | else | ||
117 | 977 | { | ||
118 | 978 | for(auto pt : place.producers) | ||
119 | 979 | { | ||
120 | 980 | if(!tseen[pt]) | ||
121 | 981 | { | ||
122 | 982 | Transition& trans = parent->_transitions[pt]; | ||
123 | 983 | auto it = trans.pre.begin(); | ||
124 | 984 | for(; it != trans.pre.end(); ++it) | ||
125 | 985 | if(it->place >= arc.place) break; | ||
126 | 986 | |||
127 | 987 | if(it != trans.pre.end() && it->place == arc.place && !it->inhib) | ||
128 | 988 | { | ||
129 | 989 | auto it2 = trans.post.begin(); | ||
130 | 990 | for(; it2 != trans.post.end(); ++it2) | ||
131 | 991 | if(it2->place >= arc.place) break; | ||
132 | 992 | if(it->weight >= it2->weight) continue; | ||
133 | 993 | } | ||
134 | 994 | |||
135 | 995 | tseen[pt] = true; | ||
136 | 996 | wtrans.push_back(pt); | ||
137 | 997 | } | ||
138 | 998 | } | ||
139 | 999 | |||
140 | 1000 | for(auto pt : place.consumers) | ||
141 | 1001 | { | ||
142 | 1002 | if(!tseen[pt] && (!remove_consumers || placeInQuery[arc.place] > 0)) | ||
143 | 1003 | { | ||
144 | 1004 | tseen[pt] = true; | ||
145 | 1005 | wtrans.push_back(pt); | ||
146 | 1006 | } | ||
147 | 1007 | } | ||
148 | 1008 | } | ||
149 | 1009 | pseen[arc.place] = true; | ||
150 | 1010 | } | ||
151 | 1011 | } | ||
152 | 1012 | |||
153 | 1013 | for(size_t t = 0; t < parent->numberOfTransitions(); ++t) | ||
154 | 1014 | { | ||
155 | 1015 | if(!tseen[t] && !parent->_transitions[t].skip) | ||
156 | 1016 | { | ||
157 | 1017 | skipTransition(t); | ||
158 | 1018 | reduced = true; | ||
159 | 1019 | } | ||
160 | 1020 | } | ||
161 | 1021 | |||
162 | 1022 | for(size_t p = 0; p < parent->numberOfPlaces(); ++p) | ||
163 | 1023 | { | ||
164 | 1024 | if(!pseen[p] && !parent->_places[p].skip && placeInQuery[p] == 0) | ||
165 | 1025 | { | ||
166 | 1026 | assert(placeInQuery[p] == 0); | ||
167 | 1027 | skipPlace(p); | ||
168 | 1028 | reduced = true; | ||
169 | 1029 | } | ||
170 | 1030 | } | ||
179 | 1031 | 924 | ||
180 | 1032 | if(reduced) | 925 | if(reduced) |
181 | 1033 | ++_ruleI; | 926 | ++_ruleI; |
182 | @@ -1565,6 +1458,153 @@ | |||
183 | 1565 | } | 1458 | } |
184 | 1566 | return continueReductions; | 1459 | return continueReductions; |
185 | 1567 | } | 1460 | } |
186 | 1461 | |||
187 | 1462 | bool Reducer::ReducebyRuleK(uint32_t *placeInQuery, bool remove_consumers) { | ||
188 | 1463 | bool reduced = false; | ||
189 | 1464 | auto opt = relevant(placeInQuery, remove_consumers); | ||
190 | 1465 | if (!opt) | ||
191 | 1466 | return false; | ||
192 | 1467 | auto[tseen, pseen] = opt.value(); | ||
193 | 1468 | for (std::size_t p = 0; p < parent->numberOfPlaces(); ++p) { | ||
194 | 1469 | if (placeInQuery[p] != 0) | ||
195 | 1470 | pseen[p] = true; | ||
196 | 1471 | } | ||
197 | 1472 | |||
198 | 1473 | for (std::size_t t = 0; t < parent->numberOfTransitions(); ++t) { | ||
199 | 1474 | auto transition = parent->_transitions[t]; | ||
200 | 1475 | if (!tseen[t] && !transition.skip && !transition.inhib && transition.pre.size() == 1 && | ||
201 | 1476 | transition.post.size() == 1 | ||
202 | 1477 | && transition.pre[0].place == transition.post[0].place) { | ||
203 | 1478 | auto p = transition.pre[0].place; | ||
204 | 1479 | if (!pseen[p] && !parent->_places[p].inhib) { | ||
205 | 1480 | if (parent->initialMarking[p] >= transition.pre[0].weight){ | ||
206 | 1481 | //Mark the initially marked self loop as relevant. | ||
207 | 1482 | tseen[t] = true; | ||
208 | 1483 | pseen[p] = true; | ||
209 | 1484 | reduced |= remove_irrelevant(placeInQuery, tseen, pseen); | ||
210 | 1485 | _ruleK++; | ||
211 | 1486 | return reduced; | ||
212 | 1487 | } | ||
213 | 1488 | if (transition.pre[0].weight == 1){ | ||
214 | 1489 | for (auto t2 : parent->_places[p].consumers) { | ||
215 | 1490 | auto transition2 = parent->_transitions[t2]; | ||
216 | 1491 | if (t != t2 && !tseen[t2] && !transition2.skip) { | ||
217 | 1492 | skipTransition(t2); | ||
218 | 1493 | reduced = true; | ||
219 | 1494 | _ruleK++; | ||
220 | 1495 | } | ||
221 | 1496 | } | ||
222 | 1497 | } | ||
223 | 1498 | } | ||
224 | 1499 | } | ||
225 | 1500 | } | ||
226 | 1501 | return reduced; | ||
227 | 1502 | } | ||
228 | 1503 | |||
229 | 1504 | std::optional<std::pair<std::vector<bool>, std::vector<bool>>> | ||
230 | 1505 | Reducer::relevant(const uint32_t *placeInQuery, bool remove_consumers) { | ||
231 | 1506 | std::vector<uint32_t> wtrans; | ||
232 | 1507 | std::vector<bool> tseen(parent->numberOfTransitions(), false); | ||
233 | 1508 | for (uint32_t p = 0; p < parent->numberOfPlaces(); ++p) { | ||
234 | 1509 | if (hasTimedout()) return std::nullopt; | ||
235 | 1510 | if (placeInQuery[p] > 0) { | ||
236 | 1511 | const Place &place = parent->_places[p]; | ||
237 | 1512 | for (auto t : place.consumers) { | ||
238 | 1513 | if (!tseen[t]) { | ||
239 | 1514 | wtrans.push_back(t); | ||
240 | 1515 | tseen[t] = true; | ||
241 | 1516 | } | ||
242 | 1517 | } | ||
243 | 1518 | for (auto t : place.producers) { | ||
244 | 1519 | if (!tseen[t]) { | ||
245 | 1520 | wtrans.push_back(t); | ||
246 | 1521 | tseen[t] = true; | ||
247 | 1522 | } | ||
248 | 1523 | } | ||
249 | 1524 | } | ||
250 | 1525 | } | ||
251 | 1526 | std::vector<bool> pseen(parent->numberOfPlaces(), false); | ||
252 | 1527 | |||
253 | 1528 | while (!wtrans.empty()) { | ||
254 | 1529 | if (hasTimedout()) return std::nullopt; | ||
255 | 1530 | auto t = wtrans.back(); | ||
256 | 1531 | wtrans.pop_back(); | ||
257 | 1532 | const Transition &trans = parent->_transitions[t]; | ||
258 | 1533 | for (const Arc &arc : trans.pre) { | ||
259 | 1534 | const Place &place = parent->_places[arc.place]; | ||
260 | 1535 | if (arc.inhib) { | ||
261 | 1536 | for (auto pt : place.consumers) { | ||
262 | 1537 | if (!tseen[pt]) { | ||
263 | 1538 | Transition &trans = parent->_transitions[pt]; | ||
264 | 1539 | auto it = trans.post.begin(); | ||
265 | 1540 | for (; it != trans.post.end(); ++it) | ||
266 | 1541 | if (it->place >= arc.place) break; | ||
267 | 1542 | if (it != trans.post.end() && it->place == arc.place) { | ||
268 | 1543 | auto it2 = trans.pre.begin(); | ||
269 | 1544 | for (; it2 != trans.pre.end(); ++it2) | ||
270 | 1545 | if (it2->place >= arc.place || it2->inhib) break; | ||
271 | 1546 | if (it->weight <= it2->weight) continue; | ||
272 | 1547 | } | ||
273 | 1548 | tseen[pt] = true; | ||
274 | 1549 | wtrans.push_back(pt); | ||
275 | 1550 | } | ||
276 | 1551 | } | ||
277 | 1552 | } else { | ||
278 | 1553 | for (auto pt : place.producers) { | ||
279 | 1554 | if (!tseen[pt]) { | ||
280 | 1555 | Transition &trans = parent->_transitions[pt]; | ||
281 | 1556 | auto it = trans.pre.begin(); | ||
282 | 1557 | for (; it != trans.pre.end(); ++it) | ||
283 | 1558 | if (it->place >= arc.place) break; | ||
284 | 1559 | |||
285 | 1560 | if (it != trans.pre.end() && it->place == arc.place && !it->inhib) { | ||
286 | 1561 | auto it2 = trans.post.begin(); | ||
287 | 1562 | for (; it2 != trans.post.end(); ++it2) | ||
288 | 1563 | if (it2->place >= arc.place) break; | ||
289 | 1564 | if (it->weight >= it2->weight) continue; | ||
290 | 1565 | } | ||
291 | 1566 | |||
292 | 1567 | tseen[pt] = true; | ||
293 | 1568 | wtrans.push_back(pt); | ||
294 | 1569 | } | ||
295 | 1570 | } | ||
296 | 1571 | |||
297 | 1572 | for (auto pt : place.consumers) { | ||
298 | 1573 | if (!tseen[pt] && (!remove_consumers || placeInQuery[arc.place] > 0)) { | ||
299 | 1574 | tseen[pt] = true; | ||
300 | 1575 | wtrans.push_back(pt); | ||
301 | 1576 | } | ||
302 | 1577 | } | ||
303 | 1578 | } | ||
304 | 1579 | pseen[arc.place] = true; | ||
305 | 1580 | } | ||
306 | 1581 | } | ||
307 | 1582 | return std::make_optional(std::pair(tseen, pseen)); | ||
308 | 1583 | } | ||
309 | 1584 | |||
310 | 1585 | bool Reducer::remove_irrelevant(const uint32_t* placeInQuery, const std::vector<bool> &tseen, const std::vector<bool> &pseen) { | ||
311 | 1586 | bool reduced = false; | ||
312 | 1587 | for(size_t t = 0; t < parent->numberOfTransitions(); ++t) | ||
313 | 1588 | { | ||
314 | 1589 | if(!tseen[t] && !parent->_transitions[t].skip) | ||
315 | 1590 | { | ||
316 | 1591 | skipTransition(t); | ||
317 | 1592 | reduced = true; | ||
318 | 1593 | } | ||
319 | 1594 | } | ||
320 | 1595 | |||
321 | 1596 | for(size_t p = 0; p < parent->numberOfPlaces(); ++p) | ||
322 | 1597 | { | ||
323 | 1598 | if(!pseen[p] && !parent->_places[p].skip && placeInQuery[p] == 0) | ||
324 | 1599 | { | ||
325 | 1600 | assert(placeInQuery[p] == 0); | ||
326 | 1601 | skipPlace(p); | ||
327 | 1602 | reduced = true; | ||
328 | 1603 | } | ||
329 | 1604 | } | ||
330 | 1605 | return reduced; | ||
331 | 1606 | } | ||
332 | 1607 | |||
333 | 1568 | void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reduction) { | 1608 | void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reduction) { |
334 | 1569 | 1609 | ||
335 | 1570 | this->_timeout = timeout; | 1610 | this->_timeout = timeout; |
336 | @@ -1603,6 +1643,7 @@ | |||
337 | 1603 | if(!remove_loops) | 1643 | if(!remove_loops) |
338 | 1604 | while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true; | 1644 | while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true; |
339 | 1605 | while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true; | 1645 | while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true; |
340 | 1646 | changed |= ReducebyRuleK(context.getQueryPlaceCount(), remove_consumers); | ||
341 | 1606 | } | 1647 | } |
342 | 1607 | } while(changed && !hasTimedout()); | 1648 | } while(changed && !hasTimedout()); |
343 | 1608 | if(!next_safe) | 1649 | if(!next_safe) |
344 | @@ -1622,7 +1663,7 @@ | |||
345 | 1622 | } | 1663 | } |
346 | 1623 | else | 1664 | else |
347 | 1624 | { | 1665 | { |
349 | 1625 | const char* rnames = "ABCDEFGHIJ"; | 1666 | const char* rnames = "ABCDEFGHIJK"; |
350 | 1626 | for(int i = reduction.size() - 1; i >= 0; --i) | 1667 | for(int i = reduction.size() - 1; i >= 0; --i) |
351 | 1627 | { | 1668 | { |
352 | 1628 | if(next_safe) | 1669 | if(next_safe) |
353 | @@ -1683,6 +1724,9 @@ | |||
354 | 1683 | case 9: | 1724 | case 9: |
355 | 1684 | while(ReducebyRuleJ(context.getQueryPlaceCount())) changed = true; | 1725 | while(ReducebyRuleJ(context.getQueryPlaceCount())) changed = true; |
356 | 1685 | break; | 1726 | break; |
357 | 1727 | case 10: | ||
358 | 1728 | if (ReducebyRuleK(context.getQueryPlaceCount(), remove_consumers)) changed = true; | ||
359 | 1729 | break; | ||
360 | 1686 | } | 1730 | } |
361 | 1687 | #ifndef NDEBUG | 1731 | #ifndef NDEBUG |
362 | 1688 | auto end = std::chrono::high_resolution_clock::now(); | 1732 | auto end = std::chrono::high_resolution_clock::now(); |
363 | 1689 | 1733 | ||
364 | === modified file 'src/VerifyPN.cpp' | |||
365 | --- src/VerifyPN.cpp 2021-02-04 11:16:09 +0000 | |||
366 | +++ src/VerifyPN.cpp 2021-02-18 12:06:25 +0000 | |||
367 | @@ -204,7 +204,7 @@ | |||
368 | 204 | for(auto& qn : q) | 204 | for(auto& qn : q) |
369 | 205 | { | 205 | { |
370 | 206 | int32_t n; | 206 | int32_t n; |
372 | 207 | if(sscanf(qn.c_str(), "%d", &n) != 1 || n < 0 || n > 9) | 207 | if(sscanf(qn.c_str(), "%d", &n) != 1 || n < 0 || n > 10) |
373 | 208 | { | 208 | { |
374 | 209 | std::cerr << "Error in reduction rule choice : " << qn << std::endl; | 209 | std::cerr << "Error in reduction rule choice : " << qn << std::endl; |
375 | 210 | return ErrorCode; | 210 | return ErrorCode; |