← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

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