← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/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:
include/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
    std::unique_ptr<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
    std::unique_ptr<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_ */