← Back to branch summary

~tapaal-ltl/verifypn/answer-for-gui

« back to all changes in this revision

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

  • Committer: srba.jiri at gmail
  • Date: 2021-04-02 18:13:50 UTC
  • mfrom: (230.1.28 mcc2021)
  • Revision ID: srba.jiri@gmail.com-20210402181350-k71xtjut3r48l1o5
merged in lp:~tapaal-ltl/verifypn/mcc2021 adding LTL, colored fixed-point unfolding for CPN and other performance improvements

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/PetriEngine/Reachability/ReachabilitySearch.h
28
28
#include "../Structures/Queue.h"
29
29
#include "../SuccessorGenerator.h"
30
30
#include "../ReducingSuccessorGenerator.h"
 
31
#include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
31
32
 
32
33
#include <memory>
33
34
#include <vector>
93
94
            Structures::State _initial;
94
95
            AbstractHandler& _callback;
95
96
        };
96
 
        
 
97
 
 
98
        template <typename G>
 
99
        inline G _makeSucGen(PetriNet &net, std::vector<PQL::Condition_ptr> &queries) {
 
100
            return G{net, queries};
 
101
        }
 
102
        template <>
 
103
        inline ReducingSuccessorGenerator _makeSucGen(PetriNet &net, std::vector<PQL::Condition_ptr> &queries) {
 
104
            return ReducingSuccessorGenerator{net, queries, std::make_shared<ReachabilityStubbornSet>(net, queries)};
 
105
        }
 
106
 
97
107
        template<typename Q, typename W, typename G>
98
108
        bool ReachabilitySearch::tryReach(   std::vector<std::shared_ptr<PQL::Condition> >& queries,
99
109
                                        std::vector<ResultPrinter::Result>& results, bool usequeries,
117
127
            
118
128
            W states(_net, _kbound);    // stateset
119
129
            Q queue(&states);           // working queue
120
 
            G generator(_net, queries); // successor generator
 
130
            G generator = _makeSucGen<G>(_net, queries); // successor generator
121
131
            auto r = states.add(state);
122
132
            // this can fail due to reductions; we push tokens around and violate K
123
133
            if(r.first){