3
3
import java.awt.Container;
4
import java.awt.event.ActionEvent;
5
import java.awt.event.ActionListener;
6
4
import java.math.BigDecimal;
7
import java.math.MathContext;
8
import java.text.DecimalFormat;
9
5
import java.util.ArrayList;
10
import java.util.HashMap;
11
6
import java.util.Iterator;
12
7
import java.util.List;
13
import java.util.Random;
15
9
import javax.swing.BoxLayout;
16
import javax.swing.JComboBox;
17
10
import javax.swing.JOptionPane;
18
import javax.swing.Timer;
20
import pipe.dataLayer.Arc;
21
import pipe.dataLayer.ColoredDiscreteFiringAction;
22
12
import pipe.dataLayer.DataLayer;
23
import pipe.dataLayer.DiscreetFiringAction;
24
import pipe.dataLayer.FiringAction;
25
import pipe.dataLayer.Place;
26
import pipe.dataLayer.TAPNTrace;
27
import pipe.dataLayer.TAPNTransition;
28
import pipe.dataLayer.TimeDelayFiringAction;
29
import pipe.dataLayer.TimedPlace;
30
13
import pipe.dataLayer.Transition;
31
import pipe.dataLayer.colors.ColoredToken;
32
import pipe.exception.InvariantViolatedAnimationException;
33
14
import pipe.gui.widgets.AnimationSelectmodeDialog;
34
15
import pipe.gui.widgets.EscapableDialog;
35
import dk.aau.cs.debug.Logger;
39
* This class is used to process clicks by the user to manually step
40
* through enabled transitions in the net.
42
* @author unspecified wrote this code
43
* @author David Patterson fixed a bug with double-firing transitions
44
* in the doRandomFiring method. I also renamed the fireTransition
45
* method to recordFiredTransition to better describe what it does.
47
* @author Pere Bonet modified the recordFiredTransition method to
48
* fix the unexcepted behaviour observed during animation playback.
49
* The method is renamed back to fireTransition.
51
* @author Edwin Chung fixed the bug where users can still step forward to
52
* previous firing sequence even though it has been reset. The issue where an
53
* unexpected behaviour will occur when the firing sequence has been altered
54
* has been resolved. The problem where animation will freeze halfway while
55
* stepping back a firing sequence has also been fixed (Feb 2007)
57
* @author Dave Patterson The code now outputs an error message in the status
58
* bar if there is no transition to be found when picking a random transition
59
* to fire. This is related to the problem described in bug 1699546.
61
* @author Joakim Byg Edited the code so that it can animate time passing in
62
* TAPN. This include refactoring lastFiredTransition so that it also
63
* contains timePasses. The rest of the code is altered so that it takes
64
* this into account (count is renamed to currentAction). (Feb 2009)
16
import dk.aau.cs.gui.TabContent;
17
import dk.aau.cs.model.tapn.NetworkMarking;
18
import dk.aau.cs.model.tapn.TimedToken;
19
import dk.aau.cs.model.tapn.TimedTransition;
20
import dk.aau.cs.model.tapn.simulation.FiringMode;
21
import dk.aau.cs.model.tapn.simulation.OldestFiringMode;
22
import dk.aau.cs.model.tapn.simulation.RandomFiringMode;
23
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
24
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTraceStep;
25
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTimeDelayStep;
26
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTimedTransitionStep;
27
import dk.aau.cs.model.tapn.simulation.YoungestFiringMode;
28
import dk.aau.cs.util.RequireException;
67
30
public class Animator {
71
private ArrayList<FiringAction> actionHistory;
31
private ArrayList<TAPNNetworkTraceStep> actionHistory;
72
32
private int currentAction;
73
private ArrayList<HashMap<TimedPlace, ArrayList<BigDecimal>>> markingHistory;
75
public Firingmode firingmode = new RandomFiringmode();
78
actionHistory = new ArrayList<FiringAction>();
80
timer = new Timer(0, new ActionListener() {
81
public void actionPerformed(ActionEvent evt) {
82
if ((getNumberSequences() < 1) ||
83
!CreateGui.getView().isInAnimationMode()) {
85
CreateGui.getApp().setRandomAnimationMode(false);
89
setNumberSequences(getNumberSequences() - 1);
33
private ArrayList<NetworkMarking> markings;
34
private int currentMarkingIndex = 0;
36
public FiringMode firingmode = new RandomFiringMode();
37
private TabContent tab;
38
private NetworkMarking initialMarking;
40
private boolean isDisplayingUntimedTrace = false;
43
actionHistory = new ArrayList<TAPNNetworkTraceStep>();
92
44
currentAction = -1;
93
markingHistory = new ArrayList<HashMap<TimedPlace,ArrayList<BigDecimal>>>();
97
public void SetTrace(TAPNTrace trace){
98
if(trace.isConcreteTrace()){
45
markings = new ArrayList<NetworkMarking>();
48
public void setTabContent(TabContent tab) {
52
private NetworkMarking currentMarking() {
53
return markings.get(currentMarkingIndex);
56
public void SetTrace(TAPNNetworkTrace trace) {
57
if (trace.isConcreteTrace()) {
99
58
setTimedTrace(trace);
101
60
setUntimedTrace(trace);
61
isDisplayingUntimedTrace = true;
64
currentMarkingIndex = 0;
65
CreateGui.getAnimationHistory().setSelectedIndex(0);
66
CreateGui.getAnimationController().setAnimationButtonsEnabled();
105
private void setUntimedTrace(TAPNTrace trace) {
106
CreateGui.addAbstractAnimationPane();
107
AnimationHistory untimedAnimationHistory = CreateGui.getAbstractAnimationPane();
108
for(FiringAction action : trace){
109
String transitionName = action instanceof ColoredDiscreteFiringAction ? ((ColoredDiscreteFiringAction)action).getTransition().getName() : ((DiscreetFiringAction)action).getTransition().getName();
110
untimedAnimationHistory.addHistoryItemDontChange(transitionName);
69
private void setUntimedTrace(TAPNNetworkTrace trace) {
70
tab.addAbstractAnimationPane();
71
AnimationHistoryComponent untimedAnimationHistory = CreateGui.getAbstractAnimationPane();
73
for(TAPNNetworkTraceStep step : trace){
74
untimedAnimationHistory.addHistoryItem(step.toString());
77
CreateGui.getAbstractAnimationPane().setSelectedIndex(0);
112
78
setFiringmode("Manual");
114
80
JOptionPane.showMessageDialog(CreateGui.getApp(),
115
"The verification process returned an untimed trace.\n\n"+
116
"This means that with appropriate time delays the displayed\n"+
117
"sequence of discrete transitions can become a concrete trace.\n"+
118
"In case of liveness properties (EG, AF) the untimed trace\n"+
119
"either ends in a deadlock, or time divergent computation without\n" +
120
"any discrete transitions, or it loops back to some earlier configuration.\n"+
121
"The user may experiment in the simulator with different time delays\n"+
122
"in order to realize the suggested untimed trace in the model.",
123
"Verification Information",
124
JOptionPane.INFORMATION_MESSAGE);
81
"The verification process returned an untimed trace.\n\n"
82
+ "This means that with appropriate time delays the displayed\n"
83
+ "sequence of discrete transitions can become a concrete trace.\n"
84
+ "In case of liveness properties (EG, AF) the untimed trace\n"
85
+ "either ends in a deadlock, a time divergent computation without\n"
86
+ "any discrete transitions, or it loops back to some earlier configuration.\n"
87
+ "The user may experiment in the simulator with different time delays\n"
88
+ "in order to realize the suggested untimed trace in the model.",
89
"Verification Information", JOptionPane.INFORMATION_MESSAGE);
127
private void setTimedTrace(TAPNTrace trace) {
128
for(FiringAction action : trace){
129
if(action instanceof TimeDelayFiringAction)
130
manipulatehistory(((TimeDelayFiringAction)action).getDealy());
131
else if(action instanceof DiscreetFiringAction){
132
manipulatehistory((DiscreetFiringAction)action);
133
}else if(action instanceof ColoredDiscreteFiringAction){
134
manipulatehistory((ColoredDiscreteFiringAction)action);
92
private void setTimedTrace(TAPNNetworkTrace trace) {
93
for (TAPNNetworkTraceStep step : trace) {
94
addMarking(step, step.performStepFrom(currentMarking()));
98
public NetworkMarking getInitialMarking(){
99
return initialMarking;
141
103
* Highlights enabled transitions
143
public void highlightEnabledTransitions(){
144
/* rewritten by wjk 03/10/2007 */
145
DataLayer current = CreateGui.currentPNMLData();
147
//current.setEnabledTransitions();
105
public void highlightEnabledTransitions() {
106
DataLayer current = activeGuiModel();
149
108
Iterator<Transition> transitionIterator = current.returnTransitions();
150
109
while (transitionIterator.hasNext()) {
180
* Called at end of animation and resets all Transitions to false and
135
* Called at end of animation and resets all Transitions to false and
183
private void disableTransitions(){
184
Iterator<Transition> transitionIterator =
185
CreateGui.currentPNMLData().returnTransitions();
138
private void disableTransitions() {
139
Iterator<Transition> transitionIterator = activeGuiModel()
140
.returnTransitions();
186
141
while (transitionIterator.hasNext()) {
187
142
Transition tempTransition = transitionIterator.next();
188
143
tempTransition.setEnabledFalse();
189
CreateGui.currentPNMLData().notifyObservers();
144
activeGuiModel().notifyObservers();
190
145
tempTransition.repaint();
196
150
* Stores model at start of animation
198
public void storeModel(){
199
CreateGui.setupModelForSimulation();
200
CreateGui.currentPNMLData().storeState();
152
public void storeModel() {
153
initialMarking = tab.network().marking();
155
markings.add(initialMarking);
205
* Restores model at end of animation and sets all transitions to false and
159
* Restores model at end of animation and sets all transitions to false and
208
public void restoreModel(){
209
CreateGui.restoreModelForEditing();
210
CreateGui.currentPNMLData().restoreState();
162
public void restoreModel() {
211
163
disableTransitions();
164
tab.network().setMarking(initialMarking);
212
165
currentAction = -1;
216
public void startRandomFiring(){
217
if (getNumberSequences() > 0) {
219
setNumberSequences(0);
222
String s = JOptionPane.showInputDialog(
223
"Enter number of firings to perform", "1");
224
this.numberSequences=Integer.parseInt(s);
225
s = JOptionPane.showInputDialog(
226
"Enter time delay between firing /ms", "50");
227
timer.setDelay(Integer.parseInt(s));
229
} catch (NumberFormatException e) {
230
CreateGui.getApp().setRandomAnimationMode(false);
236
public void stopRandomFiring() {
242
* This method randomly fires one of the enabled transitions. It then records
243
* the information about this by calling the recordFiredTransition method.
245
* @author Dave Patterson Apr 29, 2007
246
* I changed the code to keep the random transition found by the DataLayer.
247
* If it is not null, I call the fireTransition method, otherwise I put
248
* out an error message in the status bar.
250
public void doRandomFiring() {
251
DataLayer data = CreateGui.currentPNMLData();
252
Transition t = data.fireRandomTransition(); //revisar
253
//CreateGui.getAnimationHistory().clearStepsForward(); //ok - igual
254
//removeStoredTransitions(); //ok - igual
256
fireTransition(t); //revisar
257
//unhighlightDisabledTransitions();
258
//highlightEnabledTransitions();
260
CreateGui.getApp().getStatusBar().changeText(
261
"ERROR: No transition to fire." );
267
169
* Steps back through previously fired transitions
268
171
* @author jokke refactored and added backwards firing for TAPNTransitions
270
public void stepBack(){
272
if ( ! actionHistory.isEmpty() ){
274
if (actionHistory.get(currentAction) instanceof DiscreetFiringAction){
275
TAPNTransition transition = (TAPNTransition)((DiscreetFiringAction)actionHistory.get(currentAction)).getTransition(); // XXX - unsafe cast
276
HashMap<TimedPlace, ArrayList<BigDecimal>> markingToGoBackTo = markingHistory.get(currentAction);
278
if (markingToGoBackTo == null){
279
System.err.println("No marking to go back to, ERROR!");
282
HashMap<TimedPlace, ArrayList<BigDecimal>> presetMarking = new HashMap<TimedPlace, ArrayList<BigDecimal>>();
283
for (Arc a : transition.getPreset() ){
284
TimedPlace place = (TimedPlace)a.getSource();
285
presetMarking.put(place, (ArrayList<BigDecimal>)markingToGoBackTo.get(place).clone());
288
HashMap<TimedPlace, ArrayList<BigDecimal>> postsetMarking = new HashMap<TimedPlace, ArrayList<BigDecimal>>();
289
for (Arc a : transition.getPostset() ){
290
TimedPlace place = (TimedPlace)a.getTarget();
291
postsetMarking.put(place, (ArrayList<BigDecimal>)markingToGoBackTo.get(place).clone());
294
CreateGui.currentPNMLData().fireTimedTransitionBackwards(presetMarking, postsetMarking, transition);
296
//If untimed simulation
297
if (CreateGui.getAbstractAnimationPane() != null){
299
AnimationHistory untimedAnimationHistory = CreateGui.getAbstractAnimationPane();
300
int current = untimedAnimationHistory.getCurrentItem();
301
if ((untimedAnimationHistory.getElement(current)).trim().equals(transition.getName())){ //Possible null pointer exception
303
untimedAnimationHistory.stepBackwards();
308
}else if(actionHistory.get(currentAction) instanceof ColoredDiscreteFiringAction){
309
CreateGui.currentPNMLData().fireColoredTransitionBackwards((ColoredDiscreteFiringAction)actionHistory.get(currentAction));
310
}else if (actionHistory.get(currentAction) instanceof Transition ){
312
}else if ( actionHistory.get(currentAction) instanceof TimeDelayFiringAction){
313
BigDecimal timeDelay = ((TimeDelayFiringAction)actionHistory.get(currentAction)).getDealy();
315
CreateGui.getModel().letTimePass(timeDelay.negate());
316
} catch (InvariantViolatedAnimationException e) {
317
// XXX - kyrke, An error can not come here as this is valid states stored in animator
322
System.err.println("problem in Animator");
174
public void stepBack() {
175
if (!actionHistory.isEmpty()){
176
TAPNNetworkTraceStep lastStep = actionHistory.get(currentAction);
177
if(isDisplayingUntimedTrace && lastStep instanceof TAPNNetworkTimedTransitionStep){
178
AnimationHistoryComponent untimedAnimationHistory = tab.getUntimedAnimationHistory();
179
String previousInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex());
180
if(previousInUntimedTrace.equals(lastStep.toString())){
181
untimedAnimationHistory.stepBackwards();
328
CreateGui.currentPNMLData().setEnabledTransitions();
185
tab.network().setMarking(markings.get(currentMarkingIndex - 1));
187
activeGuiModel().repaintPlaces();
329
188
unhighlightDisabledTransitions();
330
189
highlightEnabledTransitions();
191
currentMarkingIndex--;
337
196
* Steps forward through previously fired transitions
339
public void stepForward(){
340
if ( currentAction < actionHistory.size()-1 ) {
343
//Marking history did not contain anything, so we must calculate the next marking
344
//We do this using hacked firingmode.
346
if ( actionHistory.get(currentAction+1) instanceof DiscreetFiringAction){
347
TAPNTransition nextTransition = (TAPNTransition)((DiscreetFiringAction)actionHistory.get(currentAction+1)).getTransition(); // XXX - unsafe cast
349
// Before we firer the transition we need to setup Select firing mode, and
350
// firer the transition with the same tokens as in the DiscreetFiringAction
351
// IT IS A HACK TO USE FIRING MODEL SELECT TO THIS !!! -- kyrke
355
//If this marking is not saved in marking history (e.g. its a uppaal trace)
357
if (markingHistory.get(currentAction+1)==null){
358
Logger.log("Marking is null, we will fix it");
360
HashMap<TimedPlace, ArrayList<BigDecimal>> currentmakring = CreateGui.currentPNMLData().getCurrentMarking();
361
markingHistory.set(currentAction+1, currentmakring);
364
HashMap<Place, ArrayList<BigDecimal>> consumedTokens = ((DiscreetFiringAction)actionHistory.get(currentAction+1)).getConsumedTokensList();
366
CreateGui.currentPNMLData().fireTransition(nextTransition, consumedTokens);
368
CreateGui.currentPNMLData().setEnabledTransitions();
369
unhighlightDisabledTransitions();
370
highlightEnabledTransitions();
373
//If untimed simulation
374
if (CreateGui.getAbstractAnimationPane() != null){
376
AnimationHistory untimedAnimationHistory = CreateGui.getAbstractAnimationPane();
377
int current = untimedAnimationHistory.getCurrentItem();
378
if ((untimedAnimationHistory.getElement(current+1)).trim().equals(nextTransition.getName())){ //Possible null pointer exception
380
untimedAnimationHistory.stepForward();
386
}else if(actionHistory.get(currentAction+1) instanceof ColoredDiscreteFiringAction){
387
ColoredDiscreteFiringAction action = (ColoredDiscreteFiringAction)actionHistory.get(currentAction+1);
388
CreateGui.currentPNMLData().fireTransition(action);
389
CreateGui.currentPNMLData().setEnabledTransitions();
390
unhighlightDisabledTransitions();
391
highlightEnabledTransitions();
393
}else if (actionHistory.get(currentAction+1) instanceof TimeDelayFiringAction){
394
BigDecimal timeDelay = ((TimeDelayFiringAction)actionHistory.get(currentAction+1)).getDealy();
396
//If this marking is not saved in marking history (e.g. its a uppaal trace)
398
if (markingHistory.get(currentAction+1)==null){
399
Logger.log("Marking is null, we will fix it");
401
HashMap<TimedPlace, ArrayList<BigDecimal>> currentmakring = CreateGui.currentPNMLData().getCurrentMarking();
402
markingHistory.set(currentAction+1, currentmakring);
406
CreateGui.getModel().letTimePass(timeDelay);
407
} catch (InvariantViolatedAnimationException e) {
408
// XXX - kyrke, An error can con come here as this is valid states stored in animator
411
CreateGui.currentPNMLData().setEnabledTransitions();
412
unhighlightDisabledTransitions();
413
highlightEnabledTransitions();
199
public void stepForward() {
200
if (currentAction < actionHistory.size() - 1) {
201
TAPNNetworkTraceStep nextStep = actionHistory.get(currentAction+1);
202
if(isDisplayingUntimedTrace && nextStep instanceof TAPNNetworkTimedTransitionStep){
203
AnimationHistoryComponent untimedAnimationHistory = tab.getUntimedAnimationHistory();
204
String nextInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);
205
if(nextInUntimedTrace.equals(nextStep.toString())){
206
untimedAnimationHistory.stepForward();
416
CreateGui.currentPNMLData().redrawVisibleTokenLists();
210
tab.network().setMarking(markings.get(currentMarkingIndex + 1));
212
activeGuiModel().repaintPlaces();
213
unhighlightDisabledTransitions();
214
highlightEnabledTransitions();
216
currentMarkingIndex++;
217
activeGuiModel().redrawVisibleTokenLists();
420
/** This method keeps track of a fired transition in the AnimationHistory
421
* object, enables transitions after the recent firing, and properly displays
424
* @author David Patterson renamed this method and changed the
425
* AnimationHandler to make it fire the transition before calling this method.
426
* This prevents double-firing a transition.
428
* @author Pere Bonet modified this method so that it now stores transitions
429
* that has just been fired in an array so that it can be accessed during
430
* backwards and stepping to fix the unexcepted behaviour observed during
431
* animation playback.
432
* The method is renamed back to fireTransition.
436
public void fireTransition(Transition transition){
438
Animator animator = CreateGui.getAnimator();
440
HashMap<TimedPlace, ArrayList<BigDecimal>> currentmakring = CreateGui.currentPNMLData().getCurrentMarking();
442
//If untimed simulation
443
if (CreateGui.getAbstractAnimationPane() != null){
445
AnimationHistory untimedAnimationHistory = CreateGui.getAbstractAnimationPane();
446
int current = untimedAnimationHistory.getCurrentItem();
448
//Only make this check if we have more steps in the untimed trace, if we dont the user can do whatever he like
449
if (untimedAnimationHistory.isStepForwardAllowed()){
450
if ((untimedAnimationHistory.getElement(current+1)).trim().equals(transition.getName())){ //Possible null pointer exception
452
untimedAnimationHistory.stepForward();
223
// TODO: Clean up this method
224
public void fireTransition(TimedTransition transition) {
225
NetworkMarking next = null;
227
if (getFiringmode() != null) {
228
next = currentMarking().fireTransition(transition, getFiringmode());
230
List<TimedToken> tokensToConsume = showSelectSimulatorDialogue(transition);
231
if(tokensToConsume == null) return; // Cancelled
232
next = currentMarking().fireTransition(transition, tokensToConsume);
234
}catch(RequireException e){
235
JOptionPane.showMessageDialog(CreateGui.getApp(), "There was an error firing the transition. Reason: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);
239
// It is important that this comes after the above, since
240
// cancelling the token selection dialogue above should not result in changes
241
// to the untimed animation history
242
if (isDisplayingUntimedTrace){
243
AnimationHistoryComponent untimedAnimationHistory = tab.getUntimedAnimationHistory();
244
if(untimedAnimationHistory.isStepForwardAllowed()){
245
String nextFromUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);
247
if(nextFromUntimedTrace.equals(transition.model().name() + "." + transition.name())){
248
untimedAnimationHistory.stepForward();
454
int fireTransition = JOptionPane.showConfirmDialog( CreateGui.getApp().getRootPane(),
455
"Are you sure you want to fire a transition which does not follow the untimed trace?\n" +
456
"Firing this transition will discard the untimed trace and revert to standard simulation.",
457
"Discrading Untimed Trace",
458
JOptionPane.YES_NO_OPTION );
459
if (fireTransition > 0){
250
int fireTransition = JOptionPane.showConfirmDialog(CreateGui.getApp(),
251
"Are you sure you want to fire a transition which does not follow the untimed trace?\n"
252
+ "Firing this transition will discard the untimed trace and revert to standard simulation.",
253
"Discrading Untimed Trace", JOptionPane.YES_NO_OPTION );
255
if (fireTransition == JOptionPane.NO_OPTION){
462
258
CreateGui.removeAbstractAnimationPane();
463
CreateGui.updateLeftPanel();
259
isDisplayingUntimedTrace = false;
469
CreateGui.getAnimationHistory().addHistoryItem(transition.getName());
471
fired = CreateGui.currentPNMLData().fireTransition(transition);
474
if ( currentAction < actionHistory.size()-1 ){
475
removeStoredActions(currentAction+1);
476
addToHistory( fired, currentmakring);
478
addToHistory( fired, currentmakring );
481
CreateGui.currentPNMLData().setEnabledTransitions();
482
animator.highlightEnabledTransitions();
483
animator.unhighlightDisabledTransitions();
487
public void letTimePass(BigDecimal timeToPass) throws InvariantViolatedAnimationException{
488
Animator animator = CreateGui.getAnimator();
490
if (CreateGui.currentPNMLData().canTimePass(timeToPass)){
492
if ( currentAction < actionHistory.size()-1 ){
493
removeStoredActions(currentAction+1);
494
addToHistory( new TimeDelayFiringAction(timeToPass), CreateGui.currentPNMLData().getCurrentMarking() );
496
addToHistory( new TimeDelayFiringAction(timeToPass), CreateGui.currentPNMLData().getCurrentMarking() );
501
//Catch exception and dont add history, throw exception again
502
// to alow handling further on.
503
//Stripping too long decimals
505
//This is a trick to get locals (, vs .) right in the text box.
506
DecimalFormat df = new DecimalFormat();
507
df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
508
df.setMinimumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
510
BigDecimal strippedTimeDelay = new BigDecimal(timeToPass.toString(), new MathContext(Pipe.AGE_PRECISION));
512
CreateGui.currentPNMLData().letTimePass(strippedTimeDelay);
514
CreateGui.getAnimationHistory().addHistoryItem("Time delay: "+ df.format(strippedTimeDelay));
517
} catch (InvariantViolatedAnimationException e) {
523
for (Place p : CreateGui.getModel().getPlaces()){
528
CreateGui.currentPNMLData().setEnabledTransitions();
529
animator.highlightEnabledTransitions();
530
animator.unhighlightDisabledTransitions();
537
public void resethistory(){
538
markingHistory.clear();
265
addMarking(new TAPNNetworkTimedTransitionStep(transition, null), next);
266
tab.network().setMarking(currentMarking());
268
activeGuiModel().repaintPlaces();
269
highlightEnabledTransitions();
270
unhighlightDisabledTransitions();
274
public void letTimePass(BigDecimal delay) {
275
if (currentMarking().isDelayPossible(delay)) {
276
addMarking(new TAPNNetworkTimeDelayStep(delay), currentMarking().delay(delay));
277
tab.network().setMarking(currentMarking());
280
activeGuiModel().repaintPlaces();
281
highlightEnabledTransitions();
282
unhighlightDisabledTransitions();
285
private DataLayer activeGuiModel() {
286
return tab.activeTemplate().guiModel();
289
public void resethistory() {
539
290
actionHistory.clear();
540
292
currentAction = -1;
543
public void manipulatehistory(ColoredDiscreteFiringAction dfa){
546
markingHistory.add(null);
548
actionHistory.add(dfa); // newAction = the transition to fire
549
CreateGui.getAnimationHistory().addHistoryItemDontChange(dfa.getTransition().getName());
551
CreateGui.animControlerBox.setAnimationButtonsEnabled();
554
public void manipulatehistory(DiscreetFiringAction dfa){
557
markingHistory.add(null);
559
actionHistory.add(dfa); // newAction = the transition to fire
560
CreateGui.getAnimationHistory().addHistoryItemDontChange(dfa.getTransition().getName());
562
CreateGui.animControlerBox.setAnimationButtonsEnabled();
564
public void manipulatehistory(BigDecimal delay){
565
markingHistory.add(null);
566
actionHistory.add(new TimeDelayFiringAction(delay));
568
CreateGui.getAnimationHistory().addHistoryItemDontChange("Time delay: "+ delay);
570
CreateGui.animControlerBox.setAnimationButtonsEnabled();
573
public Firingmode getFiringmode() {
293
currentMarkingIndex = 0;
294
tab.getAnimationHistory().reset();
295
if(tab.getUntimedAnimationHistory() != null){
296
tab.getUntimedAnimationHistory().reset();
300
public FiringMode getFiringmode() {
574
301
return firingmode;
578
//removes stored markings and actions from index "startWith" (included)
304
// removes stored markings and actions from index "startWith" (included)
579
305
private void removeStoredActions(int startWith) {
580
int lastIndex = actionHistory.size()-1;
581
for (int i=startWith; i<=lastIndex; i++){
306
int lastIndex = actionHistory.size() - 1;
307
for (int i = startWith; i <= lastIndex; i++) {
582
308
removeLastHistoryStep();
586
public synchronized int getNumberSequences() {
587
return numberSequences;
590
public synchronized void setNumberSequences(int numberSequences) {
591
this.numberSequences = numberSequences;
594
private void addToHistory(FiringAction newAction, HashMap<TimedPlace, ArrayList<BigDecimal>> currentMarking){
595
actionHistory.add(newAction);
596
markingHistory.add(currentMarking);
312
private void addMarking(TAPNNetworkTraceStep action, NetworkMarking marking) {
313
if (currentAction < actionHistory.size() - 1)
314
removeStoredActions(currentAction + 1);
316
CreateGui.getAnimationHistory().addHistoryItem(action.toString());
317
actionHistory.add(action);
318
markings.add(marking);
600
private void removeLastHistoryStep(){
601
actionHistory.remove(actionHistory.size()-1);
602
markingHistory.remove(markingHistory.size()-1);
607
public void setFiringmode(String t){
609
if (t.equals("Random")){
610
firingmode = new RandomFiringmode();
611
} else if (t.equals("Youngest")){
612
firingmode = new YoungestFiringmode();
613
} else if (t.equals("Oldest")){
614
firingmode = new OldestFiringmode();
615
} else if (t.equals("Manual")){
616
firingmode = new SelectFiringmode();
320
currentMarkingIndex++;
323
private void removeLastHistoryStep() {
324
actionHistory.remove(actionHistory.size() - 1);
325
markings.remove(markings.size() - 1);
328
public void setFiringmode(String t) {
329
if (t.equals("Random")) {
330
firingmode = new RandomFiringMode();
331
} else if (t.equals("Youngest")) {
332
firingmode = new YoungestFiringMode();
333
} else if (t.equals("Oldest")) {
334
firingmode = new OldestFiringMode();
335
} else if (t.equals("Manual")) {
618
System.err.println("Iligal firing mode mode: " + t + " not found.");
621
CreateGui.animControlerBox.updateFiringModeComboBox();
624
public interface Firingmode {
626
public ColoredToken fire(List<ColoredToken> tokens);
627
public BigDecimal fire(List<BigDecimal> tokens);
628
public String getName();
632
public class OldestFiringmode implements Firingmode {
634
public BigDecimal fire(List<BigDecimal> tokens) {
635
BigDecimal max=tokens.get(0);
636
for (BigDecimal a : tokens){
637
if (a.compareTo(max) > 0){
644
public String getName() {
648
public ColoredToken fire(List<ColoredToken> tokens) {
649
ColoredToken oldest = tokens.get(0);
650
for(ColoredToken token : tokens){
651
if(token.getAge().compareTo(oldest.getAge()) > 0){
661
public class YoungestFiringmode implements Firingmode {
663
public BigDecimal fire(List<BigDecimal> tokens) {
664
BigDecimal min=tokens.get(0);
665
for (BigDecimal a : tokens){
666
if (a.compareTo(min) < 0){
673
public String getName() {
677
public ColoredToken fire(List<ColoredToken> tokens) {
678
ColoredToken youngest = tokens.get(0);
679
for(ColoredToken token : tokens){
680
if(token.getAge().compareTo(youngest.getAge()) < 0){
691
public class RandomFiringmode implements Firingmode {
693
public BigDecimal fire(List<BigDecimal> tokens) {
694
Random generator = new Random();
696
int random = generator.nextInt(tokens.size());
698
return tokens.get(random);
701
public String getName() {
705
public ColoredToken fire(List<ColoredToken> tokens) {
706
Random generator = new Random();
707
int random = generator.nextInt(tokens.size());
708
return tokens.get(random);
712
public class SelectFiringmode implements Firingmode {
714
ArrayList<Integer> tokensToFire = new ArrayList<Integer>();
719
public void setTokensToFire( ArrayList<Integer> a){
724
public BigDecimal fire(List<BigDecimal> tokens) {
726
BigDecimal toReturn = tokens.get(tokensToFire.get(0));
727
tokensToFire.remove(0);
732
public String getName() {
736
public ColoredToken fire(List<ColoredToken> tokens) {
737
ColoredToken token = tokens.get(tokensToFire.get(0));
738
tokensToFire.remove(0);
745
public boolean showSelectSimulatorDialogue(Transition t){
746
EscapableDialog guiDialog =
747
new EscapableDialog(CreateGui.getApp(), Pipe.getProgramName(), true);
339
.println("Illegal firing mode mode: " + t + " not found.");
342
CreateGui.getAnimationController().updateFiringModeComboBox();
345
public List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) {
346
EscapableDialog guiDialog = new EscapableDialog(CreateGui.getApp(), Pipe.getProgramName(), true);
749
348
Container contentPane = guiDialog.getContentPane();
752
contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS));
755
AnimationSelectmodeDialog animationSelectmodeDialog = new AnimationSelectmodeDialog(t);
349
contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS));
350
AnimationSelectmodeDialog animationSelectmodeDialog = new AnimationSelectmodeDialog(transition);
756
351
contentPane.add(animationSelectmodeDialog);
758
guiDialog.setResizable(true);
352
guiDialog.setResizable(true);
760
354
// Make window fit contents' preferred size
761
355
guiDialog.pack();
added
removed
src/pipe/gui/Animator.java
