← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to src/PetriEngine/Structures/Queue.cpp

  • 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:
src/PetriEngine/Structures/Queue.cpp
 
1
/* VerifyPN - TAPAAL Petri Net Engine
 
2
 * Copyright (C) 2016  Peter Gjøl Jensen <root@petergjoel.dk>
 
3
 * 
 
4
 * This program is free software: you can redistribute it and/or modify
 
5
 * it under the terms of the GNU General Public License as published by
 
6
 * the Free Software Foundation, either version 3 of the License, or
 
7
 * (at your option) any later version.
 
8
 * 
 
9
 * This program is distributed in the hope that it will be useful,
 
10
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
12
 * GNU General Public License for more details.
 
13
 * 
 
14
 * You should have received a copy of the GNU General Public License
 
15
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
16
 */
 
17
 
 
18
#include "PetriEngine/Structures/Queue.h"
 
19
#include "PetriEngine/PQL/Contexts.h"
 
20
 
 
21
#include <algorithm>
 
22
#include <random>
 
23
 
 
24
namespace PetriEngine {
 
25
    namespace Structures {
 
26
        Queue::Queue(StateSetInterface* states) : _states(states) {} 
 
27
 
 
28
        Queue::~Queue() {
 
29
        }
 
30
        
 
31
        
 
32
        BFSQueue::BFSQueue(StateSetInterface* states) : Queue(states), _cnt(0), _nstates(0) {}
 
33
        BFSQueue::~BFSQueue(){}
 
34
                
 
35
        bool BFSQueue::pop(Structures::State& state)
 
36
        {
 
37
            if(_cnt < _nstates)
 
38
            {
 
39
                _states->decode(state, _cnt);
 
40
                ++_cnt;
 
41
                return true;
 
42
            }
 
43
            else
 
44
            {
 
45
                return false;
 
46
            }
 
47
        }
 
48
        
 
49
        void BFSQueue::push(size_t id, PQL::DistanceContext&,
 
50
            std::shared_ptr<PQL::Condition>& query)
 
51
        {
 
52
            ++_nstates;
 
53
            // nothing
 
54
        }
 
55
        
 
56
        DFSQueue::DFSQueue(StateSetInterface* states) : Queue(states) {}
 
57
        DFSQueue::~DFSQueue(){}
 
58
                
 
59
        bool DFSQueue::pop(Structures::State& state)
 
60
        {
 
61
            if(_stack.empty()) return false;
 
62
            uint32_t n = _stack.top();
 
63
            _stack.pop();
 
64
            _states->decode(state, n);
 
65
            return true;
 
66
        }
 
67
        
 
68
        void DFSQueue::push(size_t id, PQL::DistanceContext&,
 
69
            std::shared_ptr<PQL::Condition>& query)
 
70
        {
 
71
            _stack.push(id);
 
72
        }
 
73
        
 
74
        RDFSQueue::RDFSQueue(StateSetInterface* states) : Queue(states) {}
 
75
        RDFSQueue::~RDFSQueue(){}
 
76
       
 
77
        auto rng = std::default_random_engine {};
 
78
        bool RDFSQueue::pop(Structures::State& state)
 
79
        {
 
80
            if(_cache.empty())
 
81
            {
 
82
                if(_stack.empty()) return false;
 
83
                uint32_t n = _stack.top();
 
84
                _stack.pop();
 
85
                _states->decode(state, n);
 
86
                return true;                
 
87
            }
 
88
            else
 
89
            {
 
90
                std::shuffle ( _cache.begin(), _cache.end(), rng );
 
91
                uint32_t n = _cache.back();
 
92
                _states->decode(state, n);
 
93
                for(size_t i = 0; i < (_cache.size() - 1); ++i)
 
94
                {
 
95
                    _stack.push(_cache[i]);
 
96
                }
 
97
                _cache.clear();
 
98
                return true;
 
99
            }
 
100
        }
 
101
        
 
102
        void RDFSQueue::push(size_t id, PQL::DistanceContext&,
 
103
            std::shared_ptr<PQL::Condition>& query)
 
104
        {
 
105
            _cache.push_back(id);
 
106
        }
 
107
        
 
108
        HeuristicQueue::HeuristicQueue(StateSetInterface* states) : Queue(states) {}
 
109
        HeuristicQueue::~HeuristicQueue(){}
 
110
                
 
111
        bool HeuristicQueue::pop(Structures::State& state)
 
112
        {
 
113
            if(_queue.empty()) return false;
 
114
            uint32_t n = _queue.top().item;
 
115
            _queue.pop();
 
116
            _states->decode(state, n);
 
117
            return true;
 
118
        }
 
119
        
 
120
        void HeuristicQueue::push(size_t id, PQL::DistanceContext& context,
 
121
            std::shared_ptr<PQL::Condition>& query)
 
122
        {
 
123
            // invert result, highest numbers are on top!
 
124
            uint32_t dist = query->distance(context);
 
125
            _queue.emplace(dist, (uint32_t)id);
 
126
        }
 
127
 
 
128
    }
 
129
}