-
Notifications
You must be signed in to change notification settings - Fork 1
/
or.eol
47 lines (36 loc) · 1.35 KB
/
or.eol
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
import "equivalence.eol";
import "petri_net_navigation.eol";
operation Transition applyOrRule() : Map {
var result = Map{'a_transition_was_reduced?' = false, 'impacted_transitions' = Set {}, 'deleted_transition' = null};
-- This step is only allowed "when the preset and postset of transition are both singletons"
if (self.prep.size() == 1 and self.postp.size() == 1) {
var q = self.prep.first;
var r = self.postp.first;
if ((q == r) or not q.shares_a_transition_with?(r)) {
("Performing OR reduction for e=" + self.name + ", q=" + q.name + ",r=" + r.name).println();
var merger = q.equivalent();
var mergee = r.equivalent();
merger.contains.add(self.equivalent());
if (q <> r) {
// Update statechart
merger.name = merger.name + mergee.name;
merger.contains.addAll(mergee.contains);
delete mergee;
// Update Petri net
q.name = q.name + r.name;
q.pret.addAll(r.pret);
q.postt.addAll(r.postt);
delete r;
}
result.put('impacted_transitions', self.neighbours_and_siblings());
result.put('deleted_transition', self);
result.put('a_transition_was_reduced?', true);
delete self;
}
}
return result;
}
operation Place shares_a_transition_with?(other : Place) : Boolean {
return self.pret.exists(e|e.postp.includes(other)) or
self.postt.exists(e|e.prep.includes(other));
}