← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/Structures/Queue.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/Structures/Queue.h
 
1
/*
 
2
 * To change this license header, choose License Headers in Project Properties.
 
3
 * To change this template file, choose Tools | Templates
 
4
 * and open the template in the editor.
 
5
 */
 
6
 
 
7
/* 
 
8
 * File:   Queue.h
 
9
 * Author: Peter G. Jensen
 
10
 *
 
11
 * Created on 30 March 2016, 21:12
 
12
 */
 
13
 
 
14
#ifndef QUEUE_H
 
15
#define QUEUE_H
 
16
 
 
17
#include <memory>
 
18
#include <queue>
 
19
#include <stack>
 
20
 
 
21
#include "../PQL/PQL.h"
 
22
#include "StateSet.h"
 
23
 
 
24
namespace PetriEngine {
 
25
    namespace Structures {
 
26
        class Queue {
 
27
        public:
 
28
            Queue(StateSetInterface* states);
 
29
            virtual ~Queue();
 
30
            virtual bool pop(Structures::State& state) = 0;
 
31
            virtual void push(size_t id, PQL::DistanceContext&,
 
32
                std::shared_ptr<PQL::Condition>& query) = 0;
 
33
            size_t lastPopped()
 
34
            {
 
35
                return last;
 
36
            }
 
37
        protected:
 
38
            StateSetInterface* _states;
 
39
            size_t last = 0;
 
40
        };
 
41
        
 
42
        class BFSQueue : public Queue {
 
43
        public:
 
44
            BFSQueue(StateSetInterface* states);
 
45
            virtual ~BFSQueue();
 
46
            
 
47
            virtual bool pop(Structures::State& state);
 
48
            virtual void push(size_t id, PQL::DistanceContext&,
 
49
                std::shared_ptr<PQL::Condition>& query);
 
50
        private:
 
51
            size_t _cnt;
 
52
            size_t _nstates;
 
53
        };
 
54
        
 
55
        class DFSQueue : public Queue {
 
56
        public:
 
57
            DFSQueue(StateSetInterface* states);
 
58
            virtual ~DFSQueue();
 
59
            
 
60
            virtual bool pop(Structures::State& state);
 
61
            virtual void push(size_t id, PQL::DistanceContext&,
 
62
                std::shared_ptr<PQL::Condition>& query);
 
63
        private:
 
64
            std::stack<uint32_t> _stack;
 
65
        };
 
66
        
 
67
        class RDFSQueue : public Queue {
 
68
        public:
 
69
            RDFSQueue(StateSetInterface* states);
 
70
            virtual ~RDFSQueue();
 
71
            
 
72
            virtual bool pop(Structures::State& state);
 
73
            virtual void push(size_t id, PQL::DistanceContext&,
 
74
                std::shared_ptr<PQL::Condition>& query);
 
75
        private:
 
76
            std::stack<uint32_t> _stack;
 
77
            std::vector<uint32_t> _cache;
 
78
        };
 
79
        
 
80
        class HeuristicQueue : public Queue {
 
81
        public:
 
82
            struct weighted_t {
 
83
                uint32_t weight;
 
84
                uint32_t item;
 
85
                weighted_t(uint32_t w, uint32_t i) : weight(w), item(i) {};
 
86
                bool operator <(const weighted_t& y) const {
 
87
                    if(weight == y.weight) return item < y.item;// do dfs if they match
 
88
//                    if(weight == y.weight) return item > y.item;// do bfs if they match
 
89
                    return weight > y.weight;
 
90
                }
 
91
            };
 
92
 
 
93
            HeuristicQueue(StateSetInterface* states);
 
94
            virtual ~HeuristicQueue();
 
95
            
 
96
            virtual bool pop(Structures::State& state);
 
97
            virtual void push(size_t id, PQL::DistanceContext&,
 
98
                std::shared_ptr<PQL::Condition>& query);
 
99
        private:
 
100
            std::priority_queue<weighted_t> _queue;
 
101
        };
 
102
    }
 
103
}
 
104
 
 
105
#endif /* QUEUE_H */
 
106