← Back to branch summary

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

« back to all changes in this revision

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

  • Committer: srba.jiri at gmail
  • Date: 2021-04-16 20:59:15 UTC
  • mfrom: (231.1.16 random-fix)
  • Revision ID: srba.jiri@gmail.com-20210416205915-8d22jkkj14aff05i
merged in lp:~tapaal-ltl/verifypn/random-fix adding LTL heuristic, fixing random search and adding partitioning to CPN unfodling

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/Algorithm/RandomNDFS.h
18
18
#ifndef VERIFYPN_RANDOMNDFS_H
19
19
#define VERIFYPN_RANDOMNDFS_H
20
20
 
21
 
#include "ModelChecker.h"
 
21
#include "LTL/Algorithm/ModelChecker.h"
22
22
#include "PetriEngine/Structures/StateSet.h"
23
23
#include "PetriEngine/Structures/State.h"
24
24
#include "PetriEngine/Structures/Queue.h"
26
26
 
27
27
#include <ptrie/ptrie_stable.h>
28
28
 
29
 
using namespace PetriEngine;
30
 
 
31
29
namespace LTL {
32
 
    class RandomNDFS : public ModelChecker {
 
30
    class RandomNDFS : public ModelChecker<LTL::SpoolingSuccessorGenerator> {
33
31
    public:
34
 
        RandomNDFS(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr)
35
 
                : ModelChecker(net, ptr, false), factory{net, successorGenerator->initial_buchi_state()},
36
 
                  mark1(net, 0, (int) net.numberOfPlaces() + 1), mark2(net, 0, (int) net.numberOfPlaces() + 1) {}
 
32
        RandomNDFS(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,
 
33
                   const Structures::BuchiAutomaton &buchi,
 
34
                   LTL::SpoolingSuccessorGenerator &&successorGen, TraceLevel level,
 
35
                   bool shortcircuitweak, size_t random_seed)
 
36
                : ModelChecker(net, cond, buchi, std::move(successorGen), level, shortcircuitweak),
 
37
                  factory{net, successorGenerator->initial_buchi_state()},
 
38
                  mark1(*net, 0, (int) net->numberOfPlaces() + 1), mark2(*net, 0, (int) net->numberOfPlaces() + 1),
 
39
                  random_seed(random_seed) {}
37
40
 
38
41
        bool isSatisfied() override;
39
42
 
49
52
 
50
53
        State *seed;
51
54
        bool violation = false;
 
55
        size_t random_seed;
52
56
 
53
57
        void dfs();
54
58