~danilovesky/workcraft/trunk-menu-tools
» Revision
607
: SONPlugin/src/org/workcraft/plugins/son/algorithm/SimulationAlg.java
« back to all changes in this revision
Viewing changes to SONPlugin/src/org/workcraft/plugins/son/algorithm/SimulationAlg.java
- browse files at revision 607
- compare with another revision
- download diff
- download tarball
- view history from revision 607
- Committer: Danil Sokolov
- Date: 2015-05-15 15:46:50 UTC
- mfrom: (599.1.8 trunk-son-mbson)
- Revision ID: danilovesky@gmail.com-20150515154650-es3cqmx1x1d4p757
Merge proposal for blueprint son-bson-extension approved.
- files modified:
- SONPlugin/src/org/workcraft/plugins/son/ONGroup.java
added
removed
SONPlugin/src/org/workcraft/plugins/son/algorithm/SimulationAlg.java
2
2
3
3
import java.util.ArrayList;
4
4
import java.util.Collection;
5
import java.util.HashMap;
5
6
import java.util.HashSet;
7
import java.util.LinkedList;
6
8
import java.util.List;
7
9
import java.util.Map;
10
import java.util.Stack;
8
11
9
12
import org.workcraft.dom.Node;
10
13
import org.workcraft.plugins.son.ONGroup;
11
14
import org.workcraft.plugins.son.Phase;
12
15
import org.workcraft.plugins.son.SON;
13
import org.workcraft.plugins.son.connections.SONConnection;
14
16
import org.workcraft.plugins.son.connections.SONConnection.Semantics;
15
17
import org.workcraft.plugins.son.elements.ChannelPlace;
16
18
import org.workcraft.plugins.son.elements.Condition;
19
import org.workcraft.plugins.son.elements.PlaceNode;
17
20
import org.workcraft.plugins.son.elements.TransitionNode;
18
21
import org.workcraft.plugins.son.exception.InvalidStructureException;
19
22
22
25
private SON net;
23
26
private BSONAlg bsonAlg;
24
27
25
private Collection<ONGroup> abstractGroups;
26
private Collection<ONGroup> bhvGroups;
27
28
private Collection<Node> checkedNodes = new HashSet<Node>();
28
private Collection<ONGroup> upperGroups;
29
private Collection<ONGroup> lowerGroups;
30
29
31
30
32
public SimulationAlg(SON net){
31
33
super(net);
32
34
this.net = net;
33
35
bsonAlg = new BSONAlg(net);
34
36
35
abstractGroups = bsonAlg.getAbstractGroups(net.getGroups());
36
bhvGroups = bsonAlg.getBhvGroups(net.getGroups());
37
}
38
39
private Collection<Node> getSyncMinimum (TransitionNode e, Collection<Path> sync, Collection<TransitionNode> enabledEvents){
40
Collection<Node> result = new HashSet<Node>();
41
HashSet<Node> syncEvents = new HashSet<Node>();
42
//get related synchronous events
43
for(Path cycle : sync){
44
if(cycle.contains(e))
45
syncEvents.addAll(cycle);
46
}
47
//e is in synchronous cycle
48
if(!syncEvents.isEmpty()){
49
for(Node n : syncEvents){
50
//add all related synchronous cycle to result
51
if(enabledEvents.contains(n) && !result.contains(n)){
52
result.add(n);
53
//continue to check the event which is the pre-aysn-event of related synchronous cycle
54
for(TransitionNode pre : getPreAsynEvents((TransitionNode)n)){
55
if(!syncEvents.contains(pre) && enabledEvents.contains(pre)){
56
result.addAll(getSyncMinimum((TransitionNode)pre, sync, enabledEvents));
57
}
58
}
59
}
60
if(!enabledEvents.contains(n))
61
throw new RuntimeException("algorithm error: has unenabled event in sync cycle "+net.getNodeReference(n));
62
}
63
}
64
//e is not in synchronous cycle but has pre asyn event
65
else if(!getPreAsynEvents(e).isEmpty() && enabledEvents.contains(e)){
66
if(!result.contains(e))
67
result.add(e);
68
69
for(TransitionNode n : getPreAsynEvents(e))
70
if(!result.contains(n) && enabledEvents.contains(n)){
71
result.add(n);
72
result.addAll(getSyncMinimum((TransitionNode)n, sync, enabledEvents));
73
}
74
}
75
else{
76
result.add(e);
77
}
78
return result;
79
}
80
81
/**
82
* return minimal execution set of a given node.
83
* contain other nodes which have synchronous with the clicked node.
84
*/
85
public List<TransitionNode> getMinFires (TransitionNode e, Collection<Path> sync, Collection<TransitionNode> enabledEvents){
86
List<TransitionNode> result = new ArrayList<TransitionNode>();
87
88
for(Node n : getSyncMinimum(e, sync, enabledEvents))
89
if(n instanceof TransitionNode)
90
result.add((TransitionNode)n);;
91
92
return result;
93
}
94
95
96
private Collection<Node> getMaxFireSet(TransitionNode e, Collection<Path> sync, Collection<TransitionNode> enabledEvents){
97
Collection<Node> result = new HashSet<Node>();
98
Collection<Node> syncEvents = new HashSet<Node>();
99
100
for(Path cycle : sync){
101
if(cycle.contains(e))
102
syncEvents.addAll(cycle);
103
}
104
105
if(!syncEvents.isEmpty()){
106
for(Node n : syncEvents){
107
if(enabledEvents.contains(n) && !result.contains(n)){
108
result.add(n);
109
110
for(TransitionNode post : this.getPostAsynEvents((TransitionNode)n)){
111
if(!syncEvents.contains(post) && enabledEvents.contains(post)){
112
result.add(post);
113
result.addAll(getMaxFireSet((TransitionNode)post, sync, enabledEvents));
114
}
115
}
116
117
}
118
if(!enabledEvents.contains(n))
119
throw new RuntimeException("algorithm error: has unenable event in sync cycle");
120
}
121
}
122
else if(!getPostAsynEvents(e).isEmpty() && enabledEvents.contains(e)){
123
if(!result.contains(e))
124
result.add(e);
125
126
for(TransitionNode n : getPostAsynEvents(e))
127
if(!result.contains(n) && enabledEvents.contains(n)){
128
result.add(n);
129
result.addAll(getMaxFireSet((TransitionNode)n, sync, enabledEvents));
130
}
131
}
132
else{
133
result.add(e);
134
}
135
return result;
136
}
137
138
public List<TransitionNode> getMaxFires (TransitionNode e, Collection<Path> sync, Collection<TransitionNode> enabledEvents){
139
List<TransitionNode> result = new ArrayList<TransitionNode>();
140
141
for(Node n : getMaxFireSet(e, sync, enabledEvents))
142
if(n instanceof TransitionNode)
143
result.add((TransitionNode)n);
144
145
return result;
146
}
147
148
private boolean isPNEnabled (TransitionNode e) {
149
// gather number of connections for each pre-place
150
for (Node n : net.getPreset(e)){
151
if(n instanceof Condition)
152
if (!((Condition)n).isMarked())
153
return false;
154
}
37
upperGroups = bsonAlg.getUpperGroups(net.getGroups());
38
lowerGroups = bsonAlg.getLowerGroups(net.getGroups());
39
}
40
41
public List<TransitionNode> getMinFire(TransitionNode e, Collection<Path> sync, Collection<TransitionNode> fireList, boolean isRev){
42
List<TransitionNode> result = null;
43
if(!isRev){
44
result = getForwordMinFire(e, sync, fireList);
45
}else{
46
result = getRevMinFire(e, sync, fireList);
47
}
48
49
return result;
50
}
51
52
//set initial marking
53
public Map<PlaceNode, Boolean> getInitialMarking(){
54
HashMap<PlaceNode, Boolean> result = new HashMap<PlaceNode, Boolean>();
55
Collection<ONGroup> upperGroups = bsonAlg.getUpperGroups(net.getGroups());
56
Collection<ONGroup> lowerGroups = bsonAlg.getLowerGroups(net.getGroups());
57
58
for(PlaceNode c : net.getPlaceNodes())
59
result.put(c, false);
60
61
for(ONGroup group : net.getGroups()){
62
if(upperGroups.contains(group))
63
for(Condition c : getInitial(group.getConditions())){
64
result.put(c, true);
65
}
66
//an initial state of a lower group is the initial state of SON
67
//if all of its upper conditions are the initial states.
68
else if(lowerGroups.contains(group)){
69
for(Condition c : getInitial(group.getConditions())){
70
boolean isInitial = true;
71
Collection<Condition> set = bsonAlg.getUpperConditions(c);
72
for(Condition c2 : set){
73
if(!isInitial(c2)){
74
ONGroup group2 = net.getGroup(c2);
75
if(!set.containsAll(getInitial(group2.getConditions())))
76
isInitial = false;
77
}
78
}
79
if(isInitial)
80
result.put(c, true);
81
}
82
}
83
else{
84
for(Condition c : getInitial(group.getConditions())){
85
result.put(c, true);
86
}
87
}
88
}
89
return result;
90
}
91
92
/**
93
* return minimal execution set for a given node.
94
* contain other nodes which have synchronous and PRE- relation with the selected one.
95
*/
96
private List<TransitionNode> getForwordMinFire(TransitionNode e, Collection<Path> sync, Collection<TransitionNode> fireList){
97
List<TransitionNode> result = new ArrayList<TransitionNode>();
98
Collection<TransitionNode> u = new ArrayList<TransitionNode>();
99
Stack<TransitionNode> stack = new Stack<TransitionNode>();
100
u.addAll(fireList);
101
102
if(e!= null){
103
stack.push(e);
104
while(!stack.empty()){
105
e = stack.pop();
106
if(!result.contains(e)){
107
result.add(e);
108
u.remove(e);
109
}
110
//event in sync cycle belongs to the result
111
for(Path cycle : sync){
112
if(cycle.contains(e))
113
for(Node e2 : cycle){
114
if(e2 instanceof TransitionNode && u.contains(e2)){
115
u.remove(e2);
116
stack.push((TransitionNode)e2);
117
}
118
else if(!fireList.contains(e2)){
119
throw new RuntimeException
120
("algorithm error: unenabled event in sync cycle"+net.getNodeReference(e2));
121
}
122
}
123
}
124
//event which is the preset w.r.t weak causality, of selected event belongs to the result.
125
if(!getPreAsynEvents(e).isEmpty()){
126
for(TransitionNode e3 : getPreAsynEvents(e)){
127
if(u.contains(e3)){
128
u.remove(e3);
129
stack.push((TransitionNode)e3);
130
}
131
}
132
}
133
}
134
}
135
return result;
136
}
137
138
/**
139
* return maximal execution set for a given node.
140
* contain other nodes which have synchronous and POST- relation with the selected one.
141
*/
142
private List<TransitionNode> getRevMinFire(TransitionNode e, Collection<Path> sync, Collection<TransitionNode> fireList){
143
List<TransitionNode> result = new ArrayList<TransitionNode>();
144
Collection<TransitionNode> u = new ArrayList<TransitionNode>();
145
Stack<TransitionNode> stack = new Stack<TransitionNode>();
146
u.addAll(fireList);
147
148
if(e!= null){
149
stack.push(e);
150
while(!stack.empty()){
151
e = stack.pop();
152
if(!result.contains(e)){
153
result.add(e);
154
u.remove(e);
155
}
156
157
for(Path cycle : sync){
158
if(cycle.contains(e))
159
for(Node e2 : cycle){
160
if(e2 instanceof TransitionNode && u.contains(e2)){
161
u.remove(e2);
162
stack.push((TransitionNode)e2);
163
}
164
else if(!fireList.contains(e2)){
165
throw new RuntimeException
166
("algorithm error: unenabled event in sync cycle"+net.getNodeReference(e2));
167
}
168
}
169
}
170
if(!getPostAsynEvents(e).isEmpty()){
171
for(TransitionNode e3 : getPostAsynEvents(e)){
172
if(u.contains(e3)){
173
u.remove(e3);
174
stack.push((TransitionNode)e3);
175
}
176
}
177
}
178
}
179
}
180
return result;
181
}
182
183
final public List<TransitionNode> getEnabledNodes(Collection<Path> sync, Map<Condition, Collection<Phase>> phases, boolean isRev){
184
List<TransitionNode> result = null;
185
if(!isRev)
186
result = getEnabled(sync, phases);
187
else
188
result = getRevEnabled(sync, phases);
189
190
return result;
191
}
192
193
194
private boolean isONEnabled (TransitionNode e) {
155
195
if(net.getPreset(e).isEmpty())
156
196
return false;
157
197
158
return true;
159
}
160
161
private boolean isSyncEnabled(TransitionNode e, Collection<Path> sync, Map<Condition, Phase> phases){
162
Collection<Node> relatedSync = new HashSet<Node>();
163
//get nodes which have synchronous relation with e
164
for(Path cycle : sync){
165
if(cycle.contains(e))
166
relatedSync.addAll(cycle);
167
}
168
169
if(relatedSync.contains(e)){
170
checkedNodes.addAll(relatedSync);
171
for(Node n : relatedSync)
172
if(n instanceof TransitionNode){
173
if(!isPNEnabled((TransitionNode)n) || !isBhvEnabled((TransitionNode)n, phases))
174
return false;
175
for(TransitionNode pre : getPreAsynEvents((TransitionNode)n)){
176
if(!relatedSync.contains(pre)){
177
if(!isAsynEnabled((TransitionNode)n, sync, phases)
178
|| !isBhvEnabled((TransitionNode)n, phases))
179
return false;
180
}
181
}
182
}
183
}
184
185
return true;
186
}
187
188
private boolean isAsynEnabled(TransitionNode e, Collection<Path> sync, Map<Condition, Phase> phases){
189
//get pre-channel place q of e
190
198
for (Node n : net.getPreset(e)){
191
if(n instanceof ChannelPlace)
192
//if q is un-marked (synchronous semantic)
193
if (((ChannelPlace)n).isMarked() == false)
194
//get the input transition node of q, if it is unenabled then e is unenabled
195
for(Node node : net.getPreset(n)){
196
if(node instanceof TransitionNode && !checkedNodes.contains(node)){
197
if(!isPNEnabled((TransitionNode)node)
198
||!isSyncEnabled((TransitionNode)node, sync, phases)
199
||!isAsynEnabled((TransitionNode)node, sync, phases)
200
||!isBhvEnabled((TransitionNode)node, phases))
201
return false;
202
}
203
}
204
}
199
if(n instanceof Condition)
200
if (!((Condition)n).isMarked())
201
return false;
202
}
203
205
204
return true;
206
205
}
207
206
208
private boolean isBhvEnabled(TransitionNode e, Map<Condition, Phase> phases){
209
//if e is abstract event, e is enabled if the maximal phase of e's pre-condition is marked
210
for(ONGroup group : abstractGroups){
207
private boolean isBSONEnabled(TransitionNode e, Map<Condition, Collection<Phase>> phases){
208
//if e is upper event, e is BSON enabled if every condition in the maximal phases of e is marked
209
for(ONGroup group : upperGroups){
211
210
if(group.getComponents().contains(e)){
212
for(Node pre : getPrePNSet(e))
213
if(pre instanceof Condition){
214
Phase phase = phases.get((Condition)pre);
215
for(Condition max : bsonAlg.getMaximalPhase(phase))
216
if(!max.isMarked())
217
return false;
211
for(Node pre : getPrePNSet(e)){
212
Condition c = (Condition)pre;
213
Collection<Phase> phase = phases.get(c);
214
Collection<Condition> max = bsonAlg.getMaximalPhase(phase);
215
for(Condition c2 : max)
216
if(!c2.isMarked())
217
return false;
218
218
}
219
219
return true;
220
220
}
221
221
}
222
222
223
for(ONGroup group : bhvGroups){
223
//if e is lower event, e is BSON enabled if every e's upper condition is marked
224
for(ONGroup group : lowerGroups){
224
225
if(group.getComponents().contains(e)){
225
for(Condition c : phases.keySet()){
226
//if c is marked
227
if(c.isMarked())
228
//e is unenbled if
229
//1. e belong to c
230
//2. either the pre- or post condition of e not belong to c's phase
231
if((!phases.get(c).containsAll(getPrePNSet(e))
232
&& phases.get(c).containsAll(getPostPNSet(e)))
233
|| (!phases.get(c).containsAll(getPostPNSet(e))
234
&& phases.get(c).containsAll(getPrePNSet(e)))){
226
for(Condition c : bsonAlg.getUpperConditions(e))
227
if(!c.isMarked())
235
228
return false;
236
}
237
//if c is not marked
238
if(!c.isMarked())
239
//e is un-enabled if the pre- and post-conditions of e all belong to the phase of c.
240
if(phases.get(c).containsAll(getPostPNSet(e))
241
&& phases.get(c).containsAll(getPrePNSet(e)))
242
return false;
243
}
244
}
245
}
229
}
230
}
246
231
return true;
247
232
}
248
233
249
final public boolean isEnabled (TransitionNode e, Collection<Path> sync, Map<Condition, Phase> phases){
250
checkedNodes.clear();
251
if(isPNEnabled(e)
252
&& isSyncEnabled(e, sync, phases)
253
&& isAsynEnabled(e, sync, phases)
254
&& isBhvEnabled(e, phases)){
255
return true;
256
}
257
return false;
234
235
private List<TransitionNode> getEnabled(Collection<Path> sync, Map<Condition, Collection<Phase>> phases){
236
List<TransitionNode> result = new ArrayList<TransitionNode>();
237
Collection<Node> del = new HashSet<Node>();
238
Stack<TransitionNode> stack = new Stack<TransitionNode>();
239
240
//ON and BSON enabled
241
for(TransitionNode e : net.getTransitionNodes()){
242
if(isONEnabled(e) && isBSONEnabled(e, phases)){
243
result.add(e);
244
}
245
}
246
247
//Sync enabled
248
for(Path cycle : sync){
249
for(Node n : cycle){
250
if(n instanceof TransitionNode && !result.contains(n)){
251
del.addAll(cycle);
252
break;
253
}
254
}
255
}
256
257
//Aync enabled
258
for(TransitionNode e : result){
259
LinkedList<Node> visit = new LinkedList<Node>();
260
stack.push(e);
261
262
while(!stack.isEmpty()){
263
e = stack.peek();
264
visit.add(e);
265
266
TransitionNode e2 = null;
267
for(Node pre : net.getPreset(e)){
268
if(pre instanceof ChannelPlace){
269
if(!((ChannelPlace)pre).isMarked()){
270
for(Node pre2 : net.getPreset(pre)){
271
if(visit.contains(pre2)){
272
continue;
273
}
274
else if(!result.contains(pre2) || del.contains(pre2)){
275
// e2 = (TransitionNode)pre2;
276
// stack.push(e2);
277
visit.add(e2);
278
del.addAll(visit);
279
visit.removeLast();
280
break;
281
}
282
else if(!visit.contains(pre2)){
283
e2 = (TransitionNode)pre2;
284
stack.push(e2);
285
}
286
}
287
}
288
}
289
}
290
if(e2 == null){
291
while(!stack.isEmpty()){
292
e = stack.peek();
293
if(!visit.isEmpty() && e==visit.peekLast()){
294
stack.pop();
295
visit.removeLast();
296
}else{
297
break;
298
}
299
}
300
}
301
}
302
}
303
304
result.removeAll(del);
305
return result;
258
306
}
259
307
260
public void fire(Collection<TransitionNode> fireList) throws InvalidStructureException{
261
262
for(TransitionNode e : fireList){
263
for (SONConnection c : net.getSONConnections(e)) {
264
if (c.getSemantics() == Semantics.PNLINE && e==c.getFirst()) {
265
Condition to = (Condition)c.getSecond();
266
if(to.isMarked())
267
throw new InvalidStructureException("Token amount > 1: "+net.getNodeReference(to));
268
to.setMarked(true);
269
}
270
if (c.getSemantics() == Semantics.PNLINE && e==c.getSecond()) {
271
Condition from = (Condition)c.getFirst();
272
if(!from.isMarked())
273
throw new InvalidStructureException("Token amount = 0: "+net.getNodeReference(from));
274
from.setMarked(false);
275
}
276
if (c.getSemantics() == Semantics.ASYNLINE && e==c.getFirst()){
277
ChannelPlace to = (ChannelPlace)c.getSecond();
278
if(fireList.containsAll(net.getPostset(to)) && fireList.containsAll(net.getPreset(to)))
279
to.setMarked(((ChannelPlace)to).isMarked());
280
else{
281
if(to.isMarked())
282
throw new InvalidStructureException("Token amount > 1: "+net.getNodeReference(to));
283
to.setMarked(true);
284
}
285
}
286
if (c.getSemantics() == Semantics.ASYNLINE && e==c.getSecond()){
287
ChannelPlace from = (ChannelPlace)c.getFirst();
288
if(fireList.containsAll(net.getPostset(from)) && fireList.containsAll(net.getPreset(from)))
289
from.setMarked(((ChannelPlace)from).isMarked());
290
else
291
if(!from.isMarked())
292
throw new InvalidStructureException("Token amount = 0: "+net.getNodeReference(from));
293
from.setMarked(false);
294
}
295
}
296
297
//if e is an abstract events, get preMax - maximal phase of e's input, and postMin - minimal phase of e' output
298
Collection<Condition> preMax = new HashSet<Condition>();
299
Collection<Condition> postMin = new HashSet<Condition>();
300
for(Node pre : getPrePNSet(e)){
301
if(bsonAlg.isAbstractCondition(pre))
302
preMax.addAll(bsonAlg.getMaximalPhase(bsonAlg.getPhase((Condition)pre)));
303
}
304
for(Node post : getPostPNSet(e)){
305
if(bsonAlg.isAbstractCondition(post))
306
postMin.addAll(bsonAlg.getMinimalPhase(bsonAlg.getPhase((Condition)post)));
307
}
308
//if preMax and postMin are in separate ONs.
309
if(!preMax.containsAll(postMin)){
310
boolean isFinal=true;
311
//if preMax are the final states of an ON
312
for(Condition fin : preMax){
313
if(!isFinal(fin)){
314
isFinal=false;
315
break;
316
}
317
}
318
//token in preMax sets to false if none of corresponding abstract conditions is marked
319
if(isFinal){
320
for(Condition fin : preMax){
321
int tokens = 0;
322
for(Node c : bsonAlg.getAbstractConditions(fin)){
323
if(((Condition)c).isMarked())
324
tokens++;
325
}
326
if(fin.isMarked() && tokens == 0)
327
fin.setMarked(false);
328
}
329
}
330
//if postMin are the initial states of another ON
331
boolean isInitial = true;
332
for(Condition init : postMin){
333
if(!isInitial(init)){
334
isInitial=false;
335
break;
336
}
337
}
338
//token in postMin sets to true if ALL corresponding abstract conditions is marked
339
if(isInitial)
340
for(Condition ini : postMin){
341
int tokens = 0;
342
int count = 0;
343
for(Node c : bsonAlg.getAbstractConditions(ini)){
344
count++;
345
if(((Condition)c).isMarked())
346
tokens++;
347
}
348
if(!ini.isMarked() && tokens == count)
349
ini.setMarked(true);
350
}
351
}
352
}
353
}
354
355
356
308
//reverse simulation
357
309
358
final public boolean isUnfireEnabled (TransitionNode e, Collection<Path> sync, Map<Condition, Phase> phases) {
359
checkedNodes.clear();
360
if(isPNUnEnabled(e) && isSyncUnEnabled(e, sync, phases) && this.isAsynUnEnabled(e, sync, phases) && isBhvUnEnabled(e, phases))
361
return true;
362
return false;
363
}
364
365
366
private boolean isPNUnEnabled (TransitionNode e) {
310
private boolean isRevONEnabled (TransitionNode e) {
311
if(net.getPostset (e).isEmpty())
312
return false;
313
367
314
for (Node n : net.getPostset(e)){
368
315
if(n instanceof Condition)
369
316
if (!((Condition)n).isMarked())
370
317
return false;
371
318
}
372
if(net.getPostset(e).isEmpty())
373
return false;
319
374
320
return true;
375
321
}
376
322
377
private boolean isSyncUnEnabled(TransitionNode e, Collection<Path> sync, Map<Condition, Phase> phases){
378
HashSet<Node> relatedSync = new HashSet<Node>();
379
380
for(Path cycle : sync){
381
if(cycle.contains(e))
382
relatedSync.addAll(cycle);
383
}
384
385
if(relatedSync.contains(e)){
386
checkedNodes.addAll(relatedSync);
387
for(Node n : relatedSync)
388
if(n instanceof TransitionNode){
389
if(!this.isPNUnEnabled((TransitionNode)n) || !this.isBhvUnEnabled((TransitionNode)n, phases))
323
private boolean isRevBSONEnabled(TransitionNode e, Map<Condition, Collection<Phase>> phases){
324
//if e is upper event, e is BSON unfire enabled if every condition in the minimal phases of e is marked
325
for(ONGroup group : upperGroups){
326
if(group.getComponents().contains(e)){
327
for(Node post : getPostPNSet(e)){
328
Condition c = (Condition)post;
329
Collection<Phase> phase = phases.get(c);
330
Collection<Condition> min = bsonAlg.getMinimalPhase(phase);
331
for(Condition c2 : min)
332
if(!c2.isMarked())
390
333
return false;
391
for(Node post : this.getPostAsynEvents((TransitionNode)n)){
392
if(post instanceof TransitionNode && !relatedSync.contains(post)){
393
if(!this.isAsynUnEnabled((TransitionNode)n, sync, phases)||!this.isBhvUnEnabled((TransitionNode)n, phases))
394
return false;
395
}
396
}
397
}
398
}
399
return true;
400
}
401
402
private boolean isAsynUnEnabled(TransitionNode e, Collection<Path> sync, Map<Condition, Phase> phases){
403
404
for (Node n : net.getPostset(e)){
405
if(n instanceof ChannelPlace)
406
if (((ChannelPlace)n).isMarked() == false)
407
for(Node node : net.getPostset(n)){
408
if(node instanceof TransitionNode && !checkedNodes.contains(node)){
409
if(!this.isPNUnEnabled((TransitionNode)node)
410
||!this.isSyncUnEnabled((TransitionNode)node, sync, phases)
411
||!this.isAsynUnEnabled((TransitionNode)node, sync, phases)
412
||!this.isBhvUnEnabled((TransitionNode)node, phases))
413
return false;
414
}
415
}
416
}
417
return true;
418
}
419
420
private boolean isBhvUnEnabled(TransitionNode e, Map<Condition, Phase> phases){
421
for(ONGroup group : abstractGroups){
422
if(group.getComponents().contains(e)){
423
for(Node pre : getPostPNSet(e))
424
if(pre instanceof Condition){
425
Phase phase = phases.get((Condition)pre);
426
for(Condition min : bsonAlg.getMinimalPhase(phase))
427
if(!min.isMarked())
428
return false;
429
334
}
430
335
return true;
431
336
}
432
337
}
433
338
434
for(ONGroup group : bhvGroups){
339
//if e is lower event, e is BSON enabled if every e's upper condition is marked
340
for(ONGroup group : lowerGroups){
435
341
if(group.getComponents().contains(e)){
436
for(Condition c : phases.keySet()){
437
if(c.isMarked())
438
if((!phases.get(c).containsAll(getPrePNSet(e))
439
&& phases.get(c).containsAll(getPostPNSet(e)))
440
|| (!phases.get(c).containsAll(getPostPNSet(e))
441
&& phases.get(c).containsAll(getPrePNSet(e))))
442
return false;
342
for(Condition c : bsonAlg.getUpperConditions(e))
443
343
if(!c.isMarked())
444
if(phases.get(c).containsAll(getPostPNSet(e)) && phases.get(c).containsAll(getPrePNSet(e)))
445
return false;
446
}
447
}
448
}
449
return true;
450
}
451
452
public void unFire(Collection<TransitionNode> fireList) throws InvalidStructureException{
453
for(TransitionNode e : fireList){
454
for (SONConnection c : net.getSONConnections(e)) {
455
if (c.getSemantics() == Semantics.PNLINE && e==c.getSecond()) {
456
Condition to = (Condition)c.getFirst();
457
if(to.isMarked())
458
throw new InvalidStructureException("Reverse Token amount > 1: "+net.getNodeReference(to));
459
to.setMarked(true);
460
}
461
if (c.getSemantics() == Semantics.PNLINE && e==c.getFirst()) {
462
Condition from = (Condition)c.getSecond();
463
if(!from.isMarked())
464
throw new InvalidStructureException("Reverse Token amount = 0: "+net.getNodeReference(from));
465
from.setMarked(false);
466
}
467
if (c.getSemantics() == Semantics.ASYNLINE && e==c.getSecond()){
468
ChannelPlace to = (ChannelPlace)c.getFirst();
469
if(fireList.containsAll(net.getPreset(to)) && fireList.containsAll(net.getPostset(to)))
470
to.setMarked(((ChannelPlace)to).isMarked());
471
else
472
if(to.isMarked())
473
throw new InvalidStructureException("Reverse Token amount > 1: "+net.getNodeReference(to));
474
to.setMarked(!to.isMarked());
475
}
476
if (c.getSemantics() == Semantics.ASYNLINE && e==c.getFirst()){
477
ChannelPlace from = (ChannelPlace)c.getSecond();
478
if(fireList.containsAll(net.getPreset(from)) && fireList.containsAll(net.getPostset(from)))
479
from.setMarked(((ChannelPlace)from).isMarked());
480
else
481
if(!from.isMarked())
482
throw new InvalidStructureException("Reverse Token amount = 0: "+net.getNodeReference(from));
483
from.setMarked(!from.isMarked());
484
}
485
}
486
487
488
//if e is an abstract events, get preMax - maximal phase of e's input, and postMin - minimal phase of e' output
489
Collection<Condition> preMax = new HashSet<Condition>();
490
Collection<Condition> postMin = new HashSet<Condition>();
491
for(Node pre : getPrePNSet(e)){
492
if(bsonAlg.isAbstractCondition(pre))
493
preMax.addAll(bsonAlg.getMaximalPhase(bsonAlg.getPhase((Condition)pre)));
494
}
495
for(Node post : getPostPNSet(e)){
496
if(bsonAlg.isAbstractCondition(post))
497
postMin.addAll(bsonAlg.getMinimalPhase(bsonAlg.getPhase((Condition)post)));
498
}
499
//if preMax and postMin are in separate ONs.
500
if(!preMax.containsAll(postMin)){
501
boolean isFinal=true;
502
//if preMax are the final states of an ON
503
for(Condition fin : preMax){
504
if(!isFinal(fin)){
505
isFinal=false;
506
break;
507
}
508
}
509
//token in preMax sets to true if all of corresponding abstract conditions is marked
510
if(isFinal){
511
for(Condition fin : preMax){
512
int tokens = 0;
513
int count = 0;
514
for(Node c : bsonAlg.getAbstractConditions(fin)){
515
count++;
516
if(((Condition)c).isMarked())
517
tokens++;
518
}
519
if(!fin.isMarked() && tokens == count)
520
fin.setMarked(true);
521
}
522
}
523
//if postMin are the initial states of another ON
524
boolean isInitial = true;
525
for(Condition init : postMin){
526
if(!isInitial(init)){
527
isInitial=false;
528
break;
529
}
530
}
531
//token in postMin sets to false if none of corresponding abstract conditions is marked
532
if(isInitial)
533
for(Condition ini : postMin){
534
int tokens = 0;
535
for(Node c : bsonAlg.getAbstractConditions(ini)){
536
if(((Condition)c).isMarked())
537
tokens++;
538
}
539
if(ini.isMarked() && tokens == 0)
540
ini.setMarked(false);
541
}
542
}
344
return false;
345
}
543
346
}
347
return true;
348
}
349
350
private List<TransitionNode> getRevEnabled(Collection<Path> sync, Map<Condition, Collection<Phase>> phases){
351
List<TransitionNode> result = new ArrayList<TransitionNode>();
352
Collection<Node> del = new HashSet<Node>();
353
Stack<TransitionNode> stack = new Stack<TransitionNode>();
354
355
//ON and BSON enabled
356
for(TransitionNode e : net.getTransitionNodes()){
357
if(isRevONEnabled(e) && isRevBSONEnabled(e, phases)){
358
result.add(e);
359
}
360
}
361
362
//Sync enabled
363
for(Path cycle : sync){
364
for(Node n : cycle){
365
if(n instanceof TransitionNode && !result.contains(n)){
366
del.addAll(cycle);
367
break;
368
}
369
}
370
}
371
372
//Aync enabled
373
for(TransitionNode e : result){
374
LinkedList<Node> visit = new LinkedList<Node>();
375
stack.push(e);
376
377
while(!stack.isEmpty()){
378
e = stack.peek();
379
visit.add(e);
380
381
TransitionNode e2 = null;
382
for(Node post : net.getPostset(e)){
383
if(post instanceof ChannelPlace){
384
if(!((ChannelPlace)post).isMarked()){
385
for(Node post2 : net.getPostset(post)){
386
if(visit.contains(post2)){
387
continue;
388
}
389
else if(!result.contains(post2) || del.contains(post2)){
390
// e2 = (TransitionNode)pre2;
391
// stack.push(e2);
392
visit.add(e2);
393
del.addAll(visit);
394
visit.removeLast();
395
break;
396
}
397
else if(!visit.contains(post2)){
398
e2 = (TransitionNode)post2;
399
stack.push(e2);
400
}
401
}
402
}
403
}
404
}
405
if(e2 == null){
406
while(!stack.isEmpty()){
407
e = stack.peek();
408
if(!visit.isEmpty() && e==visit.peekLast()){
409
stack.pop();
410
visit.removeLast();
411
}else{
412
break;
413
}
414
}
415
}
416
}
417
}
418
419
result.removeAll(del);
420
return result;
421
}
422
423
public void setMarking(Collection<TransitionNode> step, Map<Condition, Collection<Phase>> phases, boolean isRev) throws InvalidStructureException{
424
if(!isRev)
425
fire(step, phases);
426
else
427
revFire(step, phases);
428
}
429
430
/**
431
* token setting after forward fire.
432
*/
433
private void fire(Collection<TransitionNode> step, Map<Condition, Collection<Phase>> phases) throws InvalidStructureException{
434
//rough checking
435
for(TransitionNode e : step){
436
for(Node post : net.getPostset(e)){
437
if(post instanceof PlaceNode)
438
if(((PlaceNode)post).isMarked())
439
throw new InvalidStructureException("Token amount > 1: "+net.getNodeReference(post));
440
}
441
}
442
443
for(TransitionNode e : step){
444
for(Node pre : net.getPreset(e)){
445
//if e is upper event, remove marking for every maximal phase of pre{e}.
446
if(bsonAlg.isUpperCondition(pre)){
447
Condition c = (Condition)pre;
448
Collection<Condition> maxSet = bsonAlg.getMaximalPhase(phases.get(c));
449
for(Condition c2 : maxSet)
450
c2.setMarked(false);
451
}
452
}
453
for(Node post : net.getPostset(e)){
454
//set marking for each post node of step U
455
if((post instanceof PlaceNode) && net.getSONConnectionType(e, post) != Semantics.SYNCLINE)
456
((PlaceNode)post).setMarked(true);
457
//if e is upper event, set marking for every minimal phase of post{e}.
458
if(bsonAlg.isUpperCondition(post)){
459
Condition c = (Condition)post;
460
Collection<Condition> minSet = bsonAlg.getMinimalPhase(phases.get(c));
461
for(Condition c2 : minSet)
462
c2.setMarked(true);
463
}
464
}
465
}
466
467
for(TransitionNode e : step){
468
//remove marking for each pre node of step U
469
for(Node pre : net.getPreset(e)){
470
if((pre instanceof PlaceNode) && net.getSONConnectionType(e, pre) != Semantics.SYNCLINE)
471
((PlaceNode)pre).setMarked(false);
472
}
473
}
474
}
475
476
477
/**
478
* token setting after reverse fire.
479
*/
480
private void revFire(Collection<TransitionNode> step, Map<Condition, Collection<Phase>> phases) throws InvalidStructureException{
481
//rough checking
482
for(TransitionNode e : step){
483
for(Node pre : net.getPreset(e)){
484
if(pre instanceof PlaceNode)
485
if(((PlaceNode)pre).isMarked())
486
throw new InvalidStructureException("Token amount > 1: "+net.getNodeReference(pre));
487
}
488
}
489
490
for(TransitionNode e : step){
491
for(Node post : net.getPostset(e)){
492
//if e is upper event, remove marking for every minimal phase of pre{e}.
493
if(bsonAlg.isUpperCondition(post)){
494
Condition c = (Condition)post;
495
Collection<Condition> minSet = bsonAlg.getMinimalPhase(phases.get(c));
496
for(Condition c2 : minSet)
497
c2.setMarked(false);
498
}
499
}
500
for(Node pre : net.getPreset(e)){
501
//set marking for each post node of step U
502
if((pre instanceof PlaceNode) && net.getSONConnectionType(e, pre) != Semantics.SYNCLINE)
503
((PlaceNode)pre).setMarked(true);
504
//if e is upper event, set marking for every minimal phase of post{e}.
505
if(bsonAlg.isUpperCondition(pre)){
506
Condition c = (Condition)pre;
507
Collection<Condition> maxSet = bsonAlg.getMaximalPhase(phases.get(c));
508
for(Condition c2 : maxSet)
509
c2.setMarked(true);
510
}
511
}
512
}
513
514
for(TransitionNode e : step){
515
//remove marking for each post node of step U
516
for(Node post : net.getPostset(e)){
517
if((post instanceof PlaceNode) && net.getSONConnectionType(e, post) != Semantics.SYNCLINE)
518
((PlaceNode)post).setMarked(false);
519
}
520
}
544
521
}
545
522
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1