verifypn

Merge lp:~verifypn-stub/verifypn/dl-structural-bug into lp:verifypn

  1. dl-structural-bug
  2. Merge into new-trunk
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 205
Merged at revision: 204
Proposed branch: lp:~verifypn-stub/verifypn/dl-structural-bug
Merge into: lp:verifypn
Diff against target: 160 lines (+35/-2)
4 files modified
PetriEngine/PQL/Expressions.cpp (+16/-0)
PetriEngine/PQL/Expressions.h (+14/-1)
PetriEngine/PQL/PQL.h (+1/-0)
PetriEngine/PetriNetBuilder.cpp (+4/-1)
To merge this branch: bzr merge lp:~verifypn-stub/verifypn/dl-structural-bug
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+344852@code.launchpad.net

Commit message

Makes sure that structural reductions are not used when deadlock proposition is in conjunction or disjunction with other predicates. Fixes bug #1750629.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

Fixes the bug but needs a special fix for 2.2 version.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'PetriEngine/PQL/Expressions.cpp'
--- PetriEngine/PQL/Expressions.cpp 2018-04-17 12:13:30 +0000
+++ PetriEngine/PQL/Expressions.cpp 2018-04-30 15:54:05 +0000
@@ -4046,6 +4046,22 @@
4046 init(std::move(exprs));4046 init(std::move(exprs));
4047 }4047 }
40484048
4049 bool LogicalCondition::nestedDeadlock() const {
4050 for(auto& c : _conds)
4051 {
4052 if(c->getQuantifier() == PQL::DEADLOCK ||
4053 c->nestedDeadlock() ||
4054 (c->getQuantifier() == PQL::NEG &&
4055 (*static_cast<NotCondition*>(c.get()))[0]->getQuantifier() == PQL::DEADLOCK
4056 ))
4057 {
4058 return true;
4059 }
4060 }
4061 return false;
4062 }
4063
4064
4049 } // PQL4065 } // PQL
4050} // PetriEngine4066} // PetriEngine
40514067
40524068
=== modified file 'PetriEngine/PQL/Expressions.h'
--- PetriEngine/PQL/Expressions.h 2018-03-29 19:20:35 +0000
+++ PetriEngine/PQL/Expressions.h 2018-04-30 15:54:05 +0000
@@ -337,6 +337,7 @@
337 const Condition_ptr& operator[](size_t i) const { return _cond; };337 const Condition_ptr& operator[](size_t i) const { return _cond; };
338 virtual bool isTemporal() const override { return _temporal;}338 virtual bool isTemporal() const override { return _temporal;}
339 bool containsNext() const override { return _cond->containsNext(); }339 bool containsNext() const override { return _cond->containsNext(); }
340 bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
340#ifdef ENABLE_TAR341#ifdef ENABLE_TAR
341 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;342 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
342#endif343#endif
@@ -375,6 +376,7 @@
375 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;376 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
376 virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}377 virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
377 virtual bool containsNext() const override { return _cond->containsNext(); }378 virtual bool containsNext() const override { return _cond->containsNext(); }
379 bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
378#ifdef ENABLE_TAR380#ifdef ENABLE_TAR
379 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const381 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
380 {382 {
@@ -525,6 +527,7 @@
525 Path getPath() const override 527 Path getPath() const override
526 { return Path::U; }528 { return Path::U; }
527 bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }529 bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
530 bool nestedDeadlock() const override { return _cond1->nestedDeadlock() || _cond2->nestedDeadlock(); }
528 private:531 private:
529 virtual std::string op() const = 0; 532 virtual std::string op() const = 0;
530 533
@@ -605,6 +608,8 @@
605 { return _compiled->formulaSize(); }608 { return _compiled->formulaSize(); }
606 bool containsNext() const override609 bool containsNext() const override
607 { return false; }610 { return false; }
611 bool nestedDeadlock() const override
612 { return false; }
608#ifdef ENABLE_TAR613#ifdef ENABLE_TAR
609 z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const override614 z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const override
610 {615 {
@@ -704,6 +709,8 @@
704 bool singular() const { return _conds.size() == 1; }709 bool singular() const { return _conds.size() == 1; }
705 bool containsNext() const override 710 bool containsNext() const override
706 { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }711 { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
712 bool nestedDeadlock() const override;
713
707 protected:714 protected:
708 LogicalCondition() {};715 LogicalCondition() {};
709 Retval simplifyOr(SimplificationContext& context) const;716 Retval simplifyOr(SimplificationContext& context) const;
@@ -838,6 +845,7 @@
838 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());845 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
839 };846 };
840 bool containsNext() const override { return false;}847 bool containsNext() const override { return false;}
848 bool nestedDeadlock() const override { return false; }
841#ifdef ENABLE_TAR849#ifdef ENABLE_TAR
842 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;850 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
843#endif851#endif
@@ -875,6 +883,7 @@
875 else return _expr2;883 else return _expr2;
876 }884 }
877 bool containsNext() const override { return false; }885 bool containsNext() const override { return false; }
886 bool nestedDeadlock() const override { return false; }
878 protected:887 protected:
879 uint32_t _distance(DistanceContext& c, 888 uint32_t _distance(DistanceContext& c,
880 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const889 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
@@ -1053,6 +1062,7 @@
1053 Path getPath() const override { return Path::pError; }1062 Path getPath() const override { return Path::pError; }
1054 CTLType getQueryType() const override { return CTLType::EVAL; }1063 CTLType getQueryType() const override { return CTLType::EVAL; }
1055 bool containsNext() const override { return false; }1064 bool containsNext() const override { return false; }
1065 bool nestedDeadlock() const override { return false; }
1056#ifdef ENABLE_TAR1066#ifdef ENABLE_TAR
1057 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const1067 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
1058 {1068 {
@@ -1087,10 +1097,11 @@
1087 void toBinary(std::ostream&) const override;1097 void toBinary(std::ostream&) const override;
1088 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;1098 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
1089 static Condition_ptr DEADLOCK;1099 static Condition_ptr DEADLOCK;
1090 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }1100 Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
1091 Path getPath() const override { return Path::pError; }1101 Path getPath() const override { return Path::pError; }
1092 CTLType getQueryType() const override { return CTLType::EVAL; }1102 CTLType getQueryType() const override { return CTLType::EVAL; }
1093 bool containsNext() const override { return false; }1103 bool containsNext() const override { return false; }
1104 bool nestedDeadlock() const override { return false; }
1094#ifdef ENABLE_TAR1105#ifdef ENABLE_TAR
1095 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;1106 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
1096#endif1107#endif
@@ -1140,6 +1151,7 @@
1140 Path getPath() const override { return Path::pError; }1151 Path getPath() const override { return Path::pError; }
1141 CTLType getQueryType() const override { return CTLType::EVAL; }1152 CTLType getQueryType() const override { return CTLType::EVAL; }
1142 bool containsNext() const override { return false; }1153 bool containsNext() const override { return false; }
1154 bool nestedDeadlock() const override { return false; }
1143#ifdef ENABLE_TAR1155#ifdef ENABLE_TAR
1144 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const 1156 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
1145 { return _compiled->encodeSat(net, context, uses, incremented); }1157 { return _compiled->encodeSat(net, context, uses, incremented); }
@@ -1192,6 +1204,7 @@
1192 Path getPath() const override { return Path::pError; }1204 Path getPath() const override { return Path::pError; }
1193 CTLType getQueryType() const override { return CTLType::EVAL; }1205 CTLType getQueryType() const override { return CTLType::EVAL; }
1194 bool containsNext() const override { return false; }1206 bool containsNext() const override { return false; }
1207 bool nestedDeadlock() const override { return false; }
1195 size_t bounds() const { return _bound; }1208 size_t bounds() const { return _bound; }
1196#ifdef ENABLE_TAR1209#ifdef ENABLE_TAR
1197 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;1210 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
11981211
=== modified file 'PetriEngine/PQL/PQL.h'
--- PetriEngine/PQL/PQL.h 2018-04-17 12:13:30 +0000
+++ PetriEngine/PQL/PQL.h 2018-04-30 15:54:05 +0000
@@ -283,6 +283,7 @@
283 static std::shared_ptr<Condition> 283 static std::shared_ptr<Condition>
284 initialMarkingRW(std::function<std::shared_ptr<Condition> ()> func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw);284 initialMarkingRW(std::function<std::shared_ptr<Condition> ()> func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw);
285 virtual bool containsNext() const = 0; 285 virtual bool containsNext() const = 0;
286 virtual bool nestedDeadlock() const = 0;
286 protected:287 protected:
287 //Value for checking if condition is trivially true or false.288 //Value for checking if condition is trivially true or false.
288 //0 is undecided (default), 1 is true, 2 is false.289 //0 is undecided (default), 1 is true, 2 is false.
289290
=== modified file 'PetriEngine/PetriNetBuilder.cpp'
--- PetriEngine/PetriNetBuilder.cpp 2018-02-22 16:42:37 +0000
+++ PetriEngine/PetriNetBuilder.cpp 2018-04-30 15:54:05 +0000
@@ -27,6 +27,7 @@
27#include "PQL/PQL.h"27#include "PQL/PQL.h"
28#include "PQL/Contexts.h"28#include "PQL/Contexts.h"
29#include "Reducer.h"29#include "Reducer.h"
30#include "PQL/Expressions.h"
3031
31using namespace std;32using namespace std;
3233
@@ -463,7 +464,9 @@
463 queries[i]->analyze(placecontext);464 queries[i]->analyze(placecontext);
464 all_reach &= (results[i] != Reachability::ResultPrinter::CTL);465 all_reach &= (results[i] != Reachability::ResultPrinter::CTL);
465 remove_loops &= !queries[i]->isLoopSensitive();466 remove_loops &= !queries[i]->isLoopSensitive();
466 contains_next |= queries[i]->containsNext();467 // There is a deadlock somewhere, if it is not alone, we cannot reduce.
468 // this has similar problems as nested next.
469 contains_next |= queries[i]->containsNext() || queries[i]->nestedDeadlock();
467 }470 }
468 }471 }
469 reducer.Reduce(placecontext, reductiontype, reconstructTrace, timeout, remove_loops, all_reach, contains_next);472 reducer.Reduce(placecontext, reductiontype, reconstructTrace, timeout, remove_loops, all_reach, contains_next);

Subscribers

People subscribed via source and target branches