← Back to branch summary

~verifypn-stub/verifypn/encoder-fix

« back to all changes in this revision

Viewing changes to CTL/PetriNets/OnTheFlyDG.h

  • Committer: Jiri Srba
  • Date: 2018-01-04 10:34:16 UTC
  • mfrom: (190.4.12 ctlse)
  • Revision ID: srba.jiri@gmail.com-20180104103416-fjdk15rww3vrbv4k
merged in branch lp:~verifypn-stub/verifypn/ctl-structural adding structurcal reduction
for CTL model checking and Stubborn sets for EF/AG leafs in the CTL algorithm

Show diffs side-by-side

added added

removed removed

Lines of Context:
CTL/PetriNets/OnTheFlyDG.h
12
12
#include "PetriEngine/Structures/ptrie_map.h"
13
13
#include "PetriEngine/Structures/AlignedEncoder.h"
14
14
#include "PetriEngine/Structures/linked_bucket.h"
 
15
#include "PetriEngine/ReducingSuccessorGenerator.h"
15
16
 
16
17
namespace PetriNets {
17
18
class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
20
21
    using Condition = PetriEngine::PQL::Condition;
21
22
    using Condition_ptr = PetriEngine::PQL::Condition_ptr;
22
23
    using Marking = PetriEngine::Structures::State;
23
 
    OnTheFlyDG(PetriEngine::PetriNet *t_net);
 
24
    OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
24
25
 
25
26
    virtual ~OnTheFlyDG();
26
27
 
57
58
    uint32_t n_places = 0;
58
59
    size_t _markingCount = 0;
59
60
    size_t _configurationCount = 0;
60
 
 
61
61
    //used after query is set
62
62
    Condition_ptr query = nullptr;
63
63
 
66
66
    {
67
67
        return fastEval(query.get(), unfolded);
68
68
    }
69
 
    void nextStates(Marking& t_marking, 
 
69
    void nextStates(Marking& t_marking, Condition*,
70
70
    std::function<void ()> pre, 
71
71
    std::function<bool (Marking&)> foreach, 
72
72
    std::function<void ()> post);
 
73
    template<typename T>
 
74
    void dowork(T& gen, bool& first, 
 
75
    std::function<void ()>& pre, 
 
76
    std::function<bool (Marking&)>& foreach)
 
77
    {
 
78
        gen.prepare(&query_marking);
 
79
 
 
80
        while(gen.next(working_marking)){
 
81
            if(first) pre();
 
82
            first = false;
 
83
            if(!foreach(working_marking))
 
84
            {
 
85
                gen.reset();
 
86
                break;
 
87
            }
 
88
        }
 
89
    }
73
90
    PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
74
91
    PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
75
92
    {
86
103
 
87
104
    // Problem  with linked bucket and complex constructor
88
105
    linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>* conf_alloc = nullptr;
89
 
        
 
106
    
 
107
    PetriEngine::ReducingSuccessorGenerator _redgen;
 
108
    bool _partial_order = false;
 
109
 
90
110
};
 
111
 
 
112
 
91
113
}
92
114
#endif // ONTHEFLYDG_H