~tapaal-ltl/verifypn/reach-aut-stub

« back to all changes in this revision

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

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2021-04-14 10:48:15 UTC
  • Revision ID: nikolaj@njulrik.dk-20210414104815-7k8k4hai5c3yrbav
Add switch between reach aut stub and visible stub

Show diffs side-by-side

added added

removed removed

Lines of Context:
26
26
 
27
27
#include <ptrie/ptrie_stable.h>
28
28
 
29
 
// TODO >:(
30
 
using namespace PetriEngine;
31
 
 
32
29
namespace LTL {
33
 
    class RandomNDFS : public ModelChecker<LTL::SpoolingSuccessorGenerator> {
 
30
    class RandomNDFS : public ModelChecker<ProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator> {
34
31
    public:
35
 
        RandomNDFS(const PetriNet &net, const PetriEngine::PQL::Condition_ptr &cond,
 
32
        RandomNDFS(const PetriEngine::PetriNet &net, const PetriEngine::PQL::Condition_ptr &cond,
36
33
                   const Structures::BuchiAutomaton &buchi,
37
34
                   LTL::SpoolingSuccessorGenerator &&successorGen, TraceLevel level,
38
35
                   bool shortcircuitweak)