← Back to branch summary

~tapaal-ltl/verifypn/composed-heuristics

« back to all changes in this revision

Viewing changes to include/LTL/Algorithm/NestedDepthFirstSearch.h

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2021-04-06 13:58:02 UTC
  • Revision ID: nikolaj@njulrik.dk-20210406135802-xy5zng0w38n9gb5s
Merge ltl-trunk@255..258

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/Algorithm/NestedDepthFirstSearch.h
48
48
    template<typename W>
49
49
class NestedDepthFirstSearch : public ModelChecker<LTL::ResumingSuccessorGenerator> {
50
50
    public:
51
 
        NestedDepthFirstSearch(const PetriEngine::PetriNet &net, const PetriEngine::PQL::Condition_ptr &query,
 
51
        NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,
52
52
                               const Structures::BuchiAutomaton &buchi,
53
53
                               TraceLevel level = TraceLevel::Full, const bool shortcircuitweak = true)
54
 
                : ModelChecker(net, query, buchi, LTL::ResumingSuccessorGenerator{net, query}, level, shortcircuitweak),
 
54
                : ModelChecker(net, query, buchi, LTL::ResumingSuccessorGenerator{*net, query}, level, shortcircuitweak),
55
55
                  factory{net, successorGenerator->initial_buchi_state()},
56
 
                  states(net, 0, (int) net.numberOfPlaces() + 1) {}
 
56
                  states(*net, 0, (int) net->numberOfPlaces() + 1) {}
57
57
 
58
58
        bool isSatisfied() override;
59
59