← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to CTL/PetriNets/OnTheFlyDG.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
CTL/PetriNets/OnTheFlyDG.h
1
 
#ifndef ONTHEFLYDG_H
2
 
#define ONTHEFLYDG_H
3
 
 
4
 
#include <functional>
5
 
 
6
 
#include "CTL/DependencyGraph/BasicDependencyGraph.h"
7
 
#include "CTL/DependencyGraph/Configuration.h"
8
 
#include "CTL/DependencyGraph/Edge.h"
9
 
#include "PetriConfig.h"
10
 
#include "PetriParse/PNMLParser.h"
11
 
#include "PetriEngine/PQL/PQL.h"
12
 
#include "PetriEngine/Structures/ptrie_map.h"
13
 
#include "PetriEngine/Structures/AlignedEncoder.h"
14
 
#include "PetriEngine/Structures/linked_bucket.h"
15
 
#include "PetriEngine/ReducingSuccessorGenerator.h"
16
 
 
17
 
namespace PetriNets {
18
 
class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
19
 
{
20
 
public:
21
 
    using Condition = PetriEngine::PQL::Condition;
22
 
    using Condition_ptr = PetriEngine::PQL::Condition_ptr;
23
 
    using Marking = PetriEngine::Structures::State;
24
 
    OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
25
 
 
26
 
    virtual ~OnTheFlyDG();
27
 
 
28
 
    //Dependency graph interface
29
 
    virtual std::vector<DependencyGraph::Edge*> successors(DependencyGraph::Configuration *c) override;
30
 
    virtual DependencyGraph::Configuration *initialConfiguration() override;
31
 
    virtual void cleanUp() override;
32
 
    void setQuery(const Condition_ptr& query);
33
 
 
34
 
    virtual void release(DependencyGraph::Edge* e) override;
35
 
 
36
 
    size_t owner(Marking& marking, Condition* cond);
37
 
    size_t owner(Marking& marking, const Condition_ptr& cond)
38
 
    {
39
 
        return owner(marking, cond.get());
40
 
    }
41
 
 
42
 
 
43
 
    //stats
44
 
    size_t configurationCount() const;
45
 
    size_t markingCount() const;
46
 
    
47
 
    Condition::Result initialEval();
48
 
 
49
 
protected:
50
 
 
51
 
    //initialized from constructor
52
 
    AlignedEncoder encoder;
53
 
    PetriEngine::PetriNet *net = nullptr;
54
 
    PetriConfig* initial_config;
55
 
    Marking working_marking;
56
 
    Marking query_marking;
57
 
    uint32_t n_transitions = 0;
58
 
    uint32_t n_places = 0;
59
 
    size_t _markingCount = 0;
60
 
    size_t _configurationCount = 0;
61
 
    //used after query is set
62
 
    Condition_ptr query = nullptr;
63
 
 
64
 
    Condition::Result fastEval(Condition* query, Marking* unfolded);
65
 
    Condition::Result fastEval(const Condition_ptr& query, Marking* unfolded)
66
 
    {
67
 
        return fastEval(query.get(), unfolded);
68
 
    }
69
 
    void nextStates(Marking& t_marking, Condition*,
70
 
    std::function<void ()> pre, 
71
 
    std::function<bool (Marking&)> foreach, 
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
 
    }
90
 
    PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
91
 
    PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
92
 
    {
93
 
        return createConfiguration(marking, own, query.get());
94
 
    }
95
 
    size_t createMarking(Marking &marking);
96
 
    void markingStats(const uint32_t* marking, size_t& sum, bool& allsame, uint32_t& val, uint32_t& active, uint32_t& last);
97
 
    
98
 
    DependencyGraph::Edge* newEdge(DependencyGraph::Configuration &t_source, uint32_t weight);
99
 
 
100
 
    std::stack<DependencyGraph::Edge*> recycle;
101
 
    ptrie::map<std::vector<PetriConfig*> > trie;
102
 
    linked_bucket_t<DependencyGraph::Edge,1024*10>* edge_alloc = nullptr;
103
 
 
104
 
    // Problem  with linked bucket and complex constructor
105
 
    linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>* conf_alloc = nullptr;
106
 
    
107
 
    PetriEngine::ReducingSuccessorGenerator _redgen;
108
 
    bool _partial_order = false;
109
 
 
110
 
};
111
 
 
112
 
 
113
 
}
114
 
#endif // ONTHEFLYDG_H