1
#include "PetriEngine/ReducingSuccessorGenerator.h"
4
#include "PetriEngine/PQL/Contexts.h"
6
namespace PetriEngine {
8
ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net) : SuccessorGenerator(net), _inhibpost(net._nplaces){
10
_enabled = std::make_unique<bool[]>(net._ntransitions);
11
_stubborn = std::make_unique<bool[]>(net._ntransitions);
12
_dependency = std::make_unique<uint32_t[]>(net._ntransitions);
13
_places_seen = std::make_unique<uint8_t[]>(_net.numberOfPlaces());
16
constructDependency();
20
ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries) : ReducingSuccessorGenerator(net) {
21
_queries.reserve(queries.size());
22
for(auto& q : queries)
23
_queries.push_back(q.get());
26
ReducingSuccessorGenerator::~ReducingSuccessorGenerator() {
29
void ReducingSuccessorGenerator::checkForInhibitor(){
30
_netContainsInhibitorArcs=false;
31
for (uint32_t t = 0; t < _net._ntransitions; t++) {
32
const TransPtr& ptr = _net._transitions[t];
33
uint32_t finv = ptr.inputs;
34
uint32_t linv = ptr.outputs;
35
for (; finv < linv; finv++) { // Post set of places
36
if (_net._invariants[finv].inhibitor) {
37
_netContainsInhibitorArcs=true;
44
void ReducingSuccessorGenerator::constructPrePost() {
45
std::vector<std::pair<std::vector<trans_t>, std::vector < trans_t>>> tmp_places(_net._nplaces);
47
for (uint32_t t = 0; t < _net._ntransitions; t++) {
48
const TransPtr& ptr = _net._transitions[t];
49
uint32_t finv = ptr.inputs;
50
uint32_t linv = ptr.outputs;
51
for (; finv < linv; finv++) { // Post set of places
52
if (_net._invariants[finv].inhibitor) {
53
_inhibpost[_net._invariants[finv].place].push_back(t);
54
_netContainsInhibitorArcs=true;
56
tmp_places[_net._invariants[finv].place].second.emplace_back(t, _net._invariants[finv].direction);
61
linv = _net._transitions[t + 1].inputs;
62
for (; finv < linv; finv++) { // Pre set of places
63
if(_net._invariants[finv].direction > 0)
64
tmp_places[_net._invariants[finv].place].first.emplace_back(t, _net._invariants[finv].direction);
70
for (auto p : tmp_places) {
71
ntrans += p.first.size() + p.second.size();
73
_transitions.reset(new trans_t[ntrans]);
75
_places.reset(new place_t[_net._nplaces + 1]);
78
for (; p < _net._nplaces; ++p) {
79
auto& pre = tmp_places[p].first;
80
auto& post = tmp_places[p].second;
82
// keep things nice for caches
83
std::sort(pre.begin(), pre.end());
84
std::sort(post.begin(), post.end());
86
_places.get()[p].pre = offset;
88
_places.get()[p].post = offset;
89
offset += post.size();
90
for (size_t tn = 0; tn < pre.size(); ++tn) {
91
_transitions.get()[tn + _places.get()[p].pre] = pre[tn];
94
for (size_t tn = 0; tn < post.size(); ++tn) {
95
_transitions.get()[tn + _places.get()[p].post] = post[tn];
99
assert(offset == ntrans);
100
_places.get()[p].pre = offset;
101
_places.get()[p].post = offset;
104
void ReducingSuccessorGenerator::constructDependency() {
105
memset(_dependency.get(), 0, sizeof(uint32_t) * _net._ntransitions);
107
for (uint32_t t = 0; t < _net._ntransitions; t++) {
108
uint32_t finv = _net._transitions[t].inputs;
109
uint32_t linv = _net._transitions[t].outputs;
111
for (; finv < linv; finv++) {
112
const Invariant& inv = _net._invariants[finv];
113
uint32_t p = inv.place;
114
uint32_t ntrans = (_places.get()[p + 1].pre - _places.get()[p].post);
116
for (uint32_t tIndex = 0; tIndex < ntrans; tIndex++) {
123
void ReducingSuccessorGenerator::constructEnabled() {
125
for (uint32_t p = 0; p < _net._nplaces; ++p) {
126
// orphans are currently under "place 0" as a special case
127
if (p == 0 || (*_parent).marking()[p] > 0) {
128
uint32_t t = _net._placeToPtrs[p];
129
uint32_t last = _net._placeToPtrs[p + 1];
131
for (; t != last; ++t) {
132
if (!checkPreset(t)) continue;
134
_ordering.push_back(t);
140
bool ReducingSuccessorGenerator::seenPre(uint32_t place) const
142
return (_places_seen.get()[place] & 1) != 0;
145
bool ReducingSuccessorGenerator::seenPost(uint32_t place) const
147
return (_places_seen.get()[place] & 2) != 0;
150
void ReducingSuccessorGenerator::presetOf(uint32_t place, bool make_closure) {
151
if((_places_seen.get()[place] & 1) != 0) return;
152
_places_seen.get()[place] = _places_seen.get()[place] | 1;
153
for (uint32_t t = _places.get()[place].pre; t < _places.get()[place].post; t++)
155
auto& tr = _transitions.get()[t];
158
if(make_closure) closure();
161
void ReducingSuccessorGenerator::postsetOf(uint32_t place, bool make_closure) {
162
if((_places_seen.get()[place] & 2) != 0) return;
163
_places_seen.get()[place] = _places_seen.get()[place] | 2;
164
for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++) {
165
auto tr = _transitions.get()[t];
169
if(make_closure) closure();
172
void ReducingSuccessorGenerator::addToStub(uint32_t t)
177
_unprocessed.push_back(t);
181
void ReducingSuccessorGenerator::inhibitorPostsetOf(uint32_t place){
182
if((_places_seen.get()[place] & 4) != 0) return;
183
_places_seen.get()[place] = _places_seen.get()[place] | 4;
184
for(uint32_t& newstub : _inhibpost[place])
188
void ReducingSuccessorGenerator::postPresetOf(uint32_t t, bool make_closure) {
189
const TransPtr& ptr = _net._transitions[t];
190
uint32_t finv = ptr.inputs;
191
uint32_t linv = ptr.outputs;
192
for (; finv < linv; finv++) { // pre-set of t
193
if(_net._invariants[finv].inhibitor){
194
presetOf(_net._invariants[finv].place, make_closure);
196
postsetOf(_net._invariants[finv].place, make_closure);
202
void ReducingSuccessorGenerator::prepare(const Structures::State* state) {
204
memset(_places_seen.get(), 0, _net.numberOfPlaces());
206
if(_ordering.size() == 0) return;
207
if(_ordering.size() == 1)
209
_stubborn[_ordering.front()] = true;
212
for (auto &q : _queries) {
213
q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
214
q->findInteresting(*this, false);
220
void ReducingSuccessorGenerator::closure()
222
while (!_unprocessed.empty()) {
223
uint32_t tr = _unprocessed.front();
224
_unprocessed.pop_front();
225
const TransPtr& ptr = _net._transitions[tr];
226
uint32_t finv = ptr.inputs;
227
uint32_t linv = ptr.outputs;
229
for (; finv < linv; finv++) {
230
if(_net._invariants[finv].direction < 0)
232
auto place = _net._invariants[finv].place;
233
for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++)
234
addToStub(_transitions.get()[t].index);
237
if(_netContainsInhibitorArcs){
238
uint32_t next_finv = _net._transitions[tr+1].inputs;
239
for (; linv < next_finv; linv++)
241
if(_net._invariants[linv].direction > 0)
242
inhibitorPostsetOf(_net._invariants[linv].place);
248
uint32_t cand = std::numeric_limits<uint32_t>::max();
250
// Lets try to see if we havent already added sufficient pre/post
251
// for this transition.
252
for (; finv < linv; ++finv) {
253
const Invariant& inv = _net._invariants[finv];
254
if ((*_parent).marking()[inv.place] < inv.tokens && !inv.inhibitor) {
256
ok = (_places_seen.get()[inv.place] & 1) != 0;
258
} else if ((*_parent).marking()[inv.place] >= inv.tokens && inv.inhibitor) {
260
ok = (_places_seen.get()[inv.place] & 2) != 0;
267
// OK, we didnt have sufficient, we just pick whatever is left
269
assert(cand != std::numeric_limits<uint32_t>::max());
270
if(!ok && cand != std::numeric_limits<uint32_t>::max())
272
if(!inhib) presetOf(cand);
273
else postsetOf(cand);
279
bool ReducingSuccessorGenerator::next(Structures::State& write) {
280
while (!_ordering.empty()) {
281
_current = _ordering.front();
282
_ordering.pop_front();
283
if (_stubborn[_current]) {
284
assert(_enabled[_current]);
285
memcpy(write.marking(), (*_parent).marking(), _net._nplaces*sizeof(MarkVal));
286
consumePreset(write, _current);
287
producePostset(write, _current);
295
uint32_t ReducingSuccessorGenerator::leastDependentEnabled() {
296
uint32_t tLeast = -1;
297
bool foundLeast = false;
298
for (uint32_t t = 0; t < _net._ntransitions; t++) {
304
if (_dependency[t] < _dependency[tLeast]) {
313
void ReducingSuccessorGenerator::reset() {
314
SuccessorGenerator::reset();
315
memset(_enabled.get(), false, sizeof(bool) * _net._ntransitions);
316
memset(_stubborn.get(), false, sizeof(bool) * _net._ntransitions);