← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to 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:
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 <memory>
24
 
#include <vector>
25
 
 
26
 
#include "../Structures/State.h"
27
 
#include "ReachabilityResult.h"
28
 
#include "../PQL/PQL.h"
29
 
#include "../PetriNet.h"
30
 
#include "../Structures/StateSet.h"
31
 
#include "../Structures/Queue.h"
32
 
#include "../SuccessorGenerator.h"
33
 
#include "../ReducingSuccessorGenerator.h"
34
 
 
35
 
namespace PetriEngine {
36
 
    namespace Reachability {
37
 
 
38
 
        enum Strategy {
39
 
            BFS,
40
 
            DFS,
41
 
            HEUR,
42
 
            RDFS,
43
 
            OverApprox,
44
 
            DEFAULT
45
 
        };
46
 
        
47
 
        /** Implements reachability check in a BFS manner using a hash table */
48
 
        class ReachabilitySearch {
49
 
        private:
50
 
            ResultPrinter& printer;
51
 
            
52
 
 
53
 
        public:
54
 
 
55
 
            ReachabilitySearch(ResultPrinter& printer, PetriNet& net, int kbound = 0)
56
 
            : printer(printer), _net(net) {
57
 
                _kbound = kbound;
58
 
            }
59
 
            
60
 
            ~ReachabilitySearch()
61
 
            {
62
 
            }
63
 
 
64
 
            /** Perform reachability check using BFS with hasing */
65
 
            void reachable(                    
66
 
                    std::vector<std::shared_ptr<PQL::Condition > >& queries,
67
 
                    std::vector<ResultPrinter::Result>& results,
68
 
                    Strategy strategy,
69
 
                    bool usestubborn,
70
 
                    bool statespacesearch,
71
 
                    bool printstats,
72
 
                    bool keep_trace);
73
 
        private:
74
 
            struct searchstate_t {
75
 
                size_t expandedStates = 0;
76
 
                size_t exploredStates = 1;
77
 
                std::vector<size_t> enabledTransitionsCount;
78
 
                size_t heurquery = 0;               
79
 
                bool usequeries;
80
 
            };
81
 
            
82
 
            template<typename Q, typename W = Structures::StateSet, typename G>
83
 
            void tryReach(
84
 
                std::vector<std::shared_ptr<PQL::Condition > >& queries,
85
 
                std::vector<ResultPrinter::Result>& results,
86
 
                bool usequeries,
87
 
                bool printstats);
88
 
            void printStats(searchstate_t& s, Structures::StateSetInterface*);
89
 
            bool checkQueries(  std::vector<std::shared_ptr<PQL::Condition > >&,
90
 
                                std::vector<ResultPrinter::Result>&,
91
 
                                Structures::State&, searchstate_t&, Structures::StateSetInterface*);
92
 
            ResultPrinter::Result printQuery(std::shared_ptr<PQL::Condition>& query, size_t i, ResultPrinter::Result, searchstate_t&, Structures::StateSetInterface*);
93
 
            
94
 
            int _kbound;
95
 
            PetriNet& _net;
96
 
            size_t _satisfyingMarking = 0;
97
 
        };
98
 
        
99
 
        template<typename Q, typename W, typename G>
100
 
        void ReachabilitySearch::tryReach(   std::vector<std::shared_ptr<PQL::Condition> >& queries, 
101
 
                                        std::vector<ResultPrinter::Result>& results, bool usequeries,
102
 
                                        bool printstats)
103
 
        {
104
 
 
105
 
            // set up state
106
 
            searchstate_t ss;
107
 
            ss.enabledTransitionsCount.resize(_net.numberOfTransitions(), 0);
108
 
            ss.expandedStates = 0;
109
 
            ss.exploredStates = 1;
110
 
            ss.heurquery = 0;
111
 
            ss.usequeries = usequeries;
112
 
 
113
 
            // set up working area
114
 
            Structures::State state;
115
 
            Structures::State working;
116
 
            state.setMarking(_net.makeInitialMarking());
117
 
            working.setMarking(_net.makeInitialMarking());
118
 
            
119
 
            W states(_net, _kbound);    // stateset
120
 
            Q queue(&states);           // working queue
121
 
            G generator(_net, queries); // successor generator
122
 
            auto r = states.add(state);
123
 
            // this can fail due to reductions; we push tokens around and violate K
124
 
            if(r.first){ 
125
 
                // add initial to states, check queries on initial state
126
 
                _satisfyingMarking = r.second;
127
 
                // check initial marking
128
 
                if(ss.usequeries) 
129
 
                {
130
 
                    if(checkQueries(queries, results, working, ss, &states))
131
 
                    {
132
 
                        if(printstats) printStats(ss, &states);
133
 
                            return;
134
 
                    }
135
 
                }
136
 
                // add initial to queue
137
 
                {
138
 
                    PQL::DistanceContext dc(&_net, working.marking());
139
 
                    queue.push(r.second, dc, queries[ss.heurquery]);
140
 
                }
141
 
 
142
 
                // Search!
143
 
                while (queue.pop(state)) {
144
 
                    generator.prepare(&state);
145
 
 
146
 
                    while(generator.next(working)){
147
 
                        ss.enabledTransitionsCount[generator.fired()]++;
148
 
                        auto res = states.add(working);
149
 
                        if (res.first) {
150
 
                            {
151
 
                                PQL::DistanceContext dc(&_net, working.marking());
152
 
                                queue.push(res.second, dc, queries[ss.heurquery]);
153
 
                            }
154
 
                            states.setHistory(res.second, generator.fired());
155
 
                            _satisfyingMarking = res.second;
156
 
                            ss.exploredStates++;
157
 
                            if (checkQueries(queries, results, working, ss, &states)) {
158
 
                                if(printstats) printStats(ss, &states);
159
 
                                return;
160
 
                            }
161
 
                        }
162
 
                    }
163
 
                    ss.expandedStates++;
164
 
                }
165
 
            }
166
 
 
167
 
            // no more successors, print last results
168
 
            for(size_t i= 0; i < queries.size(); ++i)
169
 
            {
170
 
                if(results[i] == ResultPrinter::Unknown)
171
 
                {
172
 
                    results[i] = printQuery(queries[i], i, ResultPrinter::NotSatisfied, ss, &states);                    
173
 
                }
174
 
            }            
175
 
 
176
 
            if(printstats) printStats(ss, &states);
177
 
        }
178
 
 
179
 
    }
180
 
} // Namespaces
181
 
 
182
 
#endif // BREADTHFIRSTREACHABILITYSEARCH_H