← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/ReducingSuccessorGenerator.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:
PetriEngine/ReducingSuccessorGenerator.h
1
 
#ifndef PETRIENGINE_REDUCINGSUCCESSORGENERATOR_H_
2
 
#define PETRIENGINE_REDUCINGSUCCESSORGENERATOR_H_
3
 
 
4
 
#include "SuccessorGenerator.h"
5
 
#include "Structures/State.h"
6
 
#include "Structures/light_deque.h"
7
 
#include "PQL/PQL.h"
8
 
#include <memory>
9
 
 
10
 
namespace PetriEngine {
11
 
 
12
 
class ReducingSuccessorGenerator : public SuccessorGenerator {
13
 
 
14
 
public:
15
 
    struct place_t {
16
 
        uint32_t pre, post;
17
 
    };
18
 
    struct trans_t {
19
 
        uint32_t index;
20
 
        int8_t direction;
21
 
        trans_t() = default;
22
 
        trans_t(uint32_t id, int8_t dir) : index(id), direction(dir) {};
23
 
        bool operator<(const trans_t& t) const
24
 
        {
25
 
            return index < t.index;
26
 
        }
27
 
    };
28
 
    ReducingSuccessorGenerator(const PetriNet& net);
29
 
    ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries);
30
 
    virtual ~ReducingSuccessorGenerator();
31
 
    void prepare(const Structures::State* state);
32
 
    bool next(Structures::State& write);
33
 
    void presetOf(uint32_t place, bool make_closure = false);
34
 
    void postsetOf(uint32_t place, bool make_closure = false);
35
 
    void postPresetOf(uint32_t t, bool make_closure = false);
36
 
    void inhibitorPostsetOf(uint32_t place);
37
 
    bool seenPre(uint32_t place) const;
38
 
    bool seenPost(uint32_t place) const;
39
 
    uint32_t leastDependentEnabled();
40
 
    uint32_t fired()
41
 
    {
42
 
       return _current;
43
 
    }
44
 
    void setQuery(PQL::Condition* ptr) { _queries.clear(); _queries = {ptr};}
45
 
    void reset();
46
 
 
47
 
private:
48
 
    inline void addToStub(uint32_t t);
49
 
    void closure();
50
 
    bool *_enabled, *_stubborn;
51
 
    std::unique_ptr<uint8_t> _places_seen;
52
 
    std::unique_ptr<place_t[]> _places;
53
 
    std::unique_ptr<trans_t[]> _transitions;
54
 
    light_deque<uint32_t> _unprocessed, _ordering;
55
 
    uint32_t *_dependency;
56
 
    uint32_t _current;
57
 
    bool _netContainsInhibitorArcs;
58
 
    std::vector<std::vector<uint32_t>> _inhibpost;
59
 
    
60
 
    std::vector<PQL::Condition* > _queries;
61
 
    void constructEnabled();
62
 
    void constructPrePost();
63
 
    void constructDependency();
64
 
    void checkForInhibitor();
65
 
};
66
 
}
67
 
 
68
 
#endif /* PETRIENGINE_REDUCINGSUCCESSORGENERATOR_H_ */