← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/Reachability/ReachabilitySearch.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/PetriEngine/Reachability/ReachabilitySearch.h
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 *                     Peter Gjøl Jensen <root@petergjoel.dk>
 
6
 * 
 
7
 * This program is free software: you can redistribute it and/or modify
 
8
 * it under the terms of the GNU General Public License as published by
 
9
 * the Free Software Foundation, either version 3 of the License, or
 
10
 * (at your option) any later version.
 
11
 * 
 
12
 * This program is distributed in the hope that it will be useful,
 
13
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
15
 * GNU General Public License for more details.
 
16
 * 
 
17
 * You should have received a copy of the GNU General Public License
 
18
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
19
 */
 
20
#ifndef BREADTHFIRSTREACHABILITYSEARCH_H
 
21
#define BREADTHFIRSTREACHABILITYSEARCH_H
 
22
 
 
23
#include "../Structures/State.h"
 
24
#include "ReachabilityResult.h"
 
25
#include "../PQL/PQL.h"
 
26
#include "../PetriNet.h"
 
27
#include "../Structures/StateSet.h"
 
28
#include "../Structures/Queue.h"
 
29
#include "../SuccessorGenerator.h"
 
30
#include "../ReducingSuccessorGenerator.h"
 
31
 
 
32
#include <memory>
 
33
#include <vector>
 
34
 
 
35
 
 
36
namespace PetriEngine {
 
37
    namespace Reachability {
 
38
 
 
39
        enum Strategy {
 
40
            BFS,
 
41
            DFS,
 
42
            HEUR,
 
43
            RDFS,
 
44
            OverApprox,
 
45
            DEFAULT
 
46
        };
 
47
        
 
48
        /** Implements reachability check in a BFS manner using a hash table */
 
49
        class ReachabilitySearch {
 
50
        public:
 
51
 
 
52
            ReachabilitySearch(PetriNet& net, AbstractHandler& callback, int kbound = 0, bool early = false)
 
53
            : _net(net), _kbound(kbound), _callback(callback) {
 
54
            }
 
55
            
 
56
            ~ReachabilitySearch()
 
57
            {
 
58
            }
 
59
 
 
60
            /** Perform reachability check using BFS with hasing */
 
61
            bool reachable(
 
62
                    std::vector<std::shared_ptr<PQL::Condition > >& queries,
 
63
                    std::vector<ResultPrinter::Result>& results,
 
64
                    Strategy strategy,
 
65
                    bool usestubborn,
 
66
                    bool statespacesearch,
 
67
                    bool printstats,
 
68
                    bool keep_trace);
 
69
        private:
 
70
            struct searchstate_t {
 
71
                size_t expandedStates = 0;
 
72
                size_t exploredStates = 1;
 
73
                std::vector<size_t> enabledTransitionsCount;
 
74
                size_t heurquery = 0;
 
75
                bool usequeries;
 
76
            };
 
77
            
 
78
            template<typename Q, typename W = Structures::StateSet, typename G>
 
79
            bool tryReach(
 
80
                std::vector<std::shared_ptr<PQL::Condition > >& queries,
 
81
                std::vector<ResultPrinter::Result>& results,
 
82
                bool usequeries,
 
83
                bool printstats);
 
84
            void printStats(searchstate_t& s, Structures::StateSetInterface*);
 
85
            bool checkQueries(  std::vector<std::shared_ptr<PQL::Condition > >&,
 
86
                                    std::vector<ResultPrinter::Result>&,
 
87
                                    Structures::State&, searchstate_t&, Structures::StateSetInterface*);
 
88
            std::pair<ResultPrinter::Result,bool> doCallback(std::shared_ptr<PQL::Condition>& query, size_t i, ResultPrinter::Result r, searchstate_t &ss, Structures::StateSetInterface *states);
 
89
            
 
90
            PetriNet& _net;
 
91
            int _kbound;
 
92
            size_t _satisfyingMarking = 0;
 
93
            Structures::State _initial;
 
94
            AbstractHandler& _callback;
 
95
        };
 
96
        
 
97
        template<typename Q, typename W, typename G>
 
98
        bool ReachabilitySearch::tryReach(   std::vector<std::shared_ptr<PQL::Condition> >& queries,
 
99
                                        std::vector<ResultPrinter::Result>& results, bool usequeries,
 
100
                                        bool printstats)
 
101
        {
 
102
 
 
103
            // set up state
 
104
            searchstate_t ss;
 
105
            ss.enabledTransitionsCount.resize(_net.numberOfTransitions(), 0);
 
106
            ss.expandedStates = 0;
 
107
            ss.exploredStates = 1;
 
108
            ss.heurquery = queries.size() >= 2 ? std::rand() % queries.size() : 0;
 
109
            ss.usequeries = usequeries;
 
110
 
 
111
            // set up working area
 
112
            Structures::State state;
 
113
            Structures::State working;
 
114
            _initial.setMarking(_net.makeInitialMarking());
 
115
            state.setMarking(_net.makeInitialMarking());
 
116
            working.setMarking(_net.makeInitialMarking());
 
117
            
 
118
            W states(_net, _kbound);    // stateset
 
119
            Q queue(&states);           // working queue
 
120
            G generator(_net, queries); // successor generator
 
121
            auto r = states.add(state);
 
122
            // this can fail due to reductions; we push tokens around and violate K
 
123
            if(r.first){ 
 
124
                // add initial to states, check queries on initial state
 
125
                _satisfyingMarking = r.second;
 
126
                // check initial marking
 
127
                if(ss.usequeries) 
 
128
                {
 
129
                    if(checkQueries(queries, results, working, ss, &states))
 
130
                    {
 
131
                        if(printstats) printStats(ss, &states);
 
132
                            return true;
 
133
                    }
 
134
                }
 
135
                // add initial to queue
 
136
                {
 
137
                    PQL::DistanceContext dc(&_net, working.marking());
 
138
                    queue.push(r.second, dc, queries[ss.heurquery]);
 
139
                }
 
140
 
 
141
                // Search!
 
142
                while (queue.pop(state)) {
 
143
                    generator.prepare(&state);
 
144
 
 
145
                    while(generator.next(working)){
 
146
                        ss.enabledTransitionsCount[generator.fired()]++;
 
147
                        auto res = states.add(working);
 
148
                        if (res.first) {
 
149
                            {
 
150
                                PQL::DistanceContext dc(&_net, working.marking());
 
151
                                queue.push(res.second, dc, queries[ss.heurquery]);
 
152
                            }
 
153
                            states.setHistory(res.second, generator.fired());
 
154
                            _satisfyingMarking = res.second;
 
155
                            ss.exploredStates++;
 
156
                            if (checkQueries(queries, results, working, ss, &states)) {
 
157
                                if(printstats) printStats(ss, &states);
 
158
                                return true;
 
159
                            }
 
160
                        }
 
161
                    }
 
162
                    ss.expandedStates++;
 
163
                }
 
164
            }
 
165
 
 
166
            // no more successors, print last results
 
167
            for(size_t i= 0; i < queries.size(); ++i)
 
168
            {
 
169
                if(results[i] == ResultPrinter::Unknown)
 
170
                {
 
171
                    results[i] = doCallback(queries[i], i, ResultPrinter::NotSatisfied, ss, &states).first;
 
172
                }
 
173
            }            
 
174
 
 
175
            if(printstats) printStats(ss, &states);
 
176
            return false;
 
177
        }
 
178
 
 
179
    }
 
180
} // Namespaces
 
181
 
 
182
#endif // BREADTHFIRSTREACHABILITYSEARCH_H