verifypn

Merge lp:~tapaal-ltl/verifypn/ltl-weak-ndfs into lp:~tapaal-ltl/verifypn/ltl_model_checker

  1. ltl-weak-ndfs
  2. Merge into ltl_model_checker
Proposed by Simon Virenfeldt
Status: Merged
Approved by: Simon Virenfeldt
Approved revision: 266
Merged at revision: 233
Proposed branch: lp:~tapaal-ltl/verifypn/ltl-weak-ndfs
Merge into: lp:~tapaal-ltl/verifypn/ltl_model_checker
Diff against target: 112 lines (+21/-4)
6 files modified
include/LTL/BuchiSuccessorGenerator.h (+4/-0)
include/LTL/LTL_algorithm/ModelChecker.h (+1/-0)
include/LTL/LTL_algorithm/NestedDepthFirstSearch.h (+4/-2)
include/LTL/ProductSuccessorGenerator.h (+4/-0)
src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp (+6/-0)
src/LTLMain.cpp (+2/-2)
To merge this branch: bzr merge lp:~tapaal-ltl/verifypn/ltl-weak-ndfs
Reviewer Review Type Date Requested Status
Nikolaj Jensen Ulrik Approve
Review via email: mp+394108@code.launchpad.net
To post a comment you must log in.
Revision history for this message
Nikolaj Jensen Ulrik (waefwerf) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'include/LTL/BuchiSuccessorGenerator.h'
2--- include/LTL/BuchiSuccessorGenerator.h 2020-11-04 10:50:29 +0000
3+++ include/LTL/BuchiSuccessorGenerator.h 2020-11-18 12:57:55 +0000
4@@ -53,6 +53,10 @@
5 return aut.ap_info.at(i).expression;
6 }
7
8+ [[nodiscard]] bool is_weak() const {
9+ return (bool) aut.buchi->prop_weak();
10+ }
11+
12 private:
13 Structures::BuchiAutomaton aut;
14 std::unique_ptr<spot::twa_succ_iterator> succ;
15
16=== modified file 'include/LTL/LTL_algorithm/ModelChecker.h'
17--- include/LTL/LTL_algorithm/ModelChecker.h 2020-11-04 09:40:16 +0000
18+++ include/LTL/LTL_algorithm/ModelChecker.h 2020-11-18 12:57:55 +0000
19@@ -16,6 +16,7 @@
20 virtual bool isSatisfied() = 0;
21
22 virtual ~ModelChecker() = default;
23+ bool weakskip = false;
24 protected:
25 std::unique_ptr<ProductSuccessorGenerator> successorGenerator;
26 const PetriEngine::PetriNet &net;
27
28=== modified file 'include/LTL/LTL_algorithm/NestedDepthFirstSearch.h'
29--- include/LTL/LTL_algorithm/NestedDepthFirstSearch.h 2020-11-09 13:58:30 +0000
30+++ include/LTL/LTL_algorithm/NestedDepthFirstSearch.h 2020-11-18 12:57:55 +0000
31@@ -19,9 +19,9 @@
32 namespace LTL {
33 class NestedDepthFirstSearch : public ModelChecker {
34 public:
35- NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr)
36+ NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak)
37 : ModelChecker(net, ptr), factory{net, successorGenerator->initial_buchi_state()},
38- states(net, 0, (int)net.numberOfPlaces() + 1) {}
39+ states(net, 0, (int)net.numberOfPlaces() + 1), shortcircuitweak(shortcircuitweak) {}
40
41 bool isSatisfied() override;
42
43@@ -40,6 +40,8 @@
44
45 State *seed;
46 bool violation = false;
47+ bool is_weak = false;
48+ const bool shortcircuitweak;
49
50 void dfs();
51
52
53=== modified file 'include/LTL/ProductSuccessorGenerator.h'
54--- include/LTL/ProductSuccessorGenerator.h 2020-10-28 13:05:44 +0000
55+++ include/LTL/ProductSuccessorGenerator.h 2020-11-18 12:57:55 +0000
56@@ -109,6 +109,10 @@
57 */
58 bool next(Structures::ProductState &state, successor_info &sucinfo);
59
60+ [[nodiscard]] bool is_weak() const {
61+ return buchi.is_weak();
62+ }
63+
64 private:
65 BuchiSuccessorGenerator buchi;
66 bdd cond;
67
68=== modified file 'src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp'
69--- src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp 2020-11-04 11:31:45 +0000
70+++ src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp 2020-11-18 12:57:55 +0000
71@@ -19,6 +19,8 @@
72 #endif
73
74 bool NestedDepthFirstSearch::isSatisfied() {
75+ is_weak = successorGenerator->is_weak();
76+ std::cerr << "Is weak: " << is_weak << std::endl;
77 dfs();
78 #ifdef _PRINTF_DEBUG
79 std::cout << "discovered " << _discovered << " states." << std::endl;
80@@ -100,6 +102,10 @@
81 #ifdef PRINTF_DEBUG
82 dump_state(working);
83 #endif
84+ if (shortcircuitweak && is_weak && !successorGenerator->isAccepting(working)) {
85+ weakskip = true;
86+ continue;
87+ }
88 if (working == *seed) {
89 #ifdef _PRINTF_DEBUG
90 std::cerr << "seed:\n "; dump_state(*seed);
91
92=== modified file 'src/LTLMain.cpp'
93--- src/LTLMain.cpp 2020-11-04 14:22:15 +0000
94+++ src/LTLMain.cpp 2020-11-18 12:57:55 +0000
95@@ -496,7 +496,7 @@
96 std::unique_ptr<LTL::ModelChecker> modelChecker;
97 switch (options.ltlalgorithm) {
98 case LTL::Algorithm::NDFS:
99- modelChecker = std::make_unique<LTL::NestedDepthFirstSearch>(*net, negated_formula);
100+ modelChecker = std::make_unique<LTL::NestedDepthFirstSearch>(*net, negated_formula, true);
101 break;
102 case LTL::Algorithm::Tarjan:
103 if (options.trace)
104@@ -507,7 +507,7 @@
105 }
106
107 bool satisfied = negate_answer ^ modelChecker->isSatisfied();
108- std::cout << "FORMULA " << query.id << (satisfied ? " TRUE" : " FALSE") << " TECHNIQUES EXPLICIT" << (options.ltlalgorithm == LTL::Algorithm::NDFS ? " NDFS" : " TARJAN") << std::endl;
109+ std::cout << "FORMULA " << query.id << (satisfied ? " TRUE" : " FALSE") << " TECHNIQUES EXPLICIT" << (options.ltlalgorithm == LTL::Algorithm::NDFS ? " NDFS" : " TARJAN") << (modelChecker->weakskip ? " WEAK_SKIP" : "") << std::endl;
110 }
111 }
112 return SuccessCode;

Subscribers

People subscribed via source and target branches

to all changes: