← Back to branch summary

~tapaal-contributor/tapaal/display-shared-places-transitions-1879126

« back to all changes in this revision

Viewing changes to src/pipe/gui/Animator.java

  • Committer: Jiri Srba
  • Date: 2020-04-28 19:15:28 UTC
  • mfrom: (998.2.376 testbranch)
  • Revision ID: srba@cs.aau.dk-20200428191528-3xxjqa1r4jcob5ur
merged in lp:~yrke/tapaal/testbranch doing majour refactoring of the GUI

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/Animator.java
55
55
                return isUrgentTransitionEnabled;
56
56
        }
57
57
 
58
 
        public Animator() {
 
58
        public Animator(TabContent tab) {
59
59
                actionHistory = new ArrayList<TAPNNetworkTraceStep>();
60
60
                currentAction = -1;
61
61
                markings = new ArrayList<NetworkMarking>();
 
62
                setTabContent(tab);
62
63
        }
63
64
 
64
 
        public void setTabContent(TabContent tab) {
 
65
        private void setTabContent(TabContent tab)  {
65
66
                this.tab = tab;
66
67
        }
67
68
 
69
70
                return markings.get(currentMarkingIndex);
70
71
        }
71
72
 
72
 
        public void SetTrace(TAPNNetworkTrace trace) {
 
73
        public void setTrace(TAPNNetworkTrace trace) {
 
74
        CreateGui.getCurrentTab().setAnimationMode(true);
 
75
 
73
76
                if (trace.isConcreteTrace()) {
74
77
                        this.trace = trace;
75
78
                        setTimedTrace(trace);
80
83
                currentAction = -1;
81
84
                currentMarkingIndex = 0;
82
85
                tab.network().setMarking(markings.get(currentMarkingIndex));
83
 
                CreateGui.getCurrentTab().getAnimationHistory().setSelectedIndex(0);
84
 
                CreateGui.getCurrentTab().getAnimationController().setAnimationButtonsEnabled();
 
86
                tab.getAnimationHistory().setSelectedIndex(0);
 
87
                tab.getAnimationController().setAnimationButtonsEnabled();
85
88
                updateFireableTransitions();
86
89
        }
87
90
 
88
91
        private void setUntimedTrace(TAPNNetworkTrace trace) {
89
92
                tab.addAbstractAnimationPane();
90
 
                AnimationHistoryComponent untimedAnimationHistory = CreateGui.getCurrentTab().getUntimedAnimationHistory();
 
93
                AnimationHistoryComponent<String> untimedAnimationHistory = tab.getUntimedAnimationHistory();
91
94
 
92
95
                for(TAPNNetworkTraceStep step : trace){
93
96
                        untimedAnimationHistory.addHistoryItem(step.toString());
94
97
                }
95
98
 
96
 
                CreateGui.getCurrentTab().getUntimedAnimationHistory().setSelectedIndex(0);
 
99
                tab.getUntimedAnimationHistory().setSelectedIndex(0);
97
100
                setFiringmode("Random");
98
101
 
99
102
                JOptionPane.showMessageDialog(CreateGui.getApp(),
113
116
                        addMarking(step, step.performStepFrom(currentMarking()));
114
117
                }
115
118
                if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock.
116
 
                        CreateGui.getCurrentTab().getAnimationHistory().setLastShown(getTrace().getTraceType());
 
119
                        tab.getAnimationHistory().setLastShown(getTrace().getTraceType());
117
120
                }
118
121
        }
119
122
 
154
157
        /**
155
158
         * Called during animation to unhighlight previously highlighted transitions
156
159
         */
157
 
        public void unhighlightDisabledTransitions() {
 
160
        private void unhighlightDisabledTransitions() {
158
161
                DataLayer current = activeGuiModel();
159
162
 
160
163
                Iterator<Transition> transitionIterator = current.returnTransitions();
167
170
        }
168
171
 
169
172
        public void updateFireableTransitions(){
170
 
                TransitionFireingComponent transFireComponent = CreateGui.getCurrentTab().getTransitionFireingComponent();
 
173
                TransitionFireingComponent transFireComponent = tab.getTransitionFireingComponent();
171
174
                transFireComponent.startReInit();
172
175
                isUrgentTransitionEnabled = false;
173
176
                
174
 
                outer: for( Template temp : CreateGui.getCurrentTab().activeTemplates()){
 
177
                outer: for( Template temp : tab.activeTemplates()){
175
178
                        Iterator<Transition> transitionIterator = temp.guiModel().returnTransitions();
176
179
                        while (transitionIterator.hasNext()) {
177
180
                                Transition tempTransition = transitionIterator.next();
182
185
                        }
183
186
                }
184
187
                
185
 
                for( Template temp : CreateGui.getCurrentTab().activeTemplates()){
 
188
                for( Template temp : tab.activeTemplates()){
186
189
                        Iterator<Transition> transitionIterator = temp.guiModel().returnTransitions();
187
190
                        while (transitionIterator.hasNext()) {
188
191
                                Transition tempTransition = transitionIterator.next();
226
229
         * unhighlighted
227
230
         */
228
231
        public void restoreModel() {
229
 
                disableTransitions();
230
 
                tab.network().setMarking(initialMarking);
231
 
                currentAction = -1;
 
232
                if (tab != null) {
 
233
                        disableTransitions();
 
234
                        tab.network().setMarking(initialMarking);
 
235
                        currentAction = -1;
 
236
                }
232
237
        }
233
238
 
234
239
        /**
241
246
                if (!actionHistory.isEmpty()){
242
247
                        TAPNNetworkTraceStep lastStep = actionHistory.get(currentAction);
243
248
                        if(isDisplayingUntimedTrace && lastStep instanceof TAPNNetworkTimedTransitionStep){
244
 
                                AnimationHistoryComponent untimedAnimationHistory = tab.getUntimedAnimationHistory();
 
249
                                AnimationHistoryComponent<String> untimedAnimationHistory = tab.getUntimedAnimationHistory();
245
250
                                String previousInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex());
246
251
                                if(previousInUntimedTrace.equals(lastStep.toString())){
247
252
                                        untimedAnimationHistory.stepBackwards();
264
269
 
265
270
        public void stepForward() {
266
271
                if(currentAction == actionHistory.size()-1 && trace != null){
267
 
                        int selectedIndex = CreateGui.getCurrentTab().getAnimationHistory().getSelectedIndex();
 
272
                        int selectedIndex = tab.getAnimationHistory().getSelectedIndex();
268
273
                        int action = currentAction;
269
274
                        int markingIndex = currentMarkingIndex;
270
275
 
275
280
                                addToTimedTrace(getTrace().getLoopSteps());
276
281
                        }
277
282
 
278
 
                        CreateGui.getCurrentTab().getAnimationHistory().setSelectedIndex(selectedIndex);
 
283
                        tab.getAnimationHistory().setSelectedIndex(selectedIndex);
279
284
                        currentAction = action;
280
285
                        currentMarkingIndex = markingIndex;
281
286
                }
283
288
                if (currentAction < actionHistory.size() - 1) {
284
289
                        TAPNNetworkTraceStep nextStep = actionHistory.get(currentAction+1);
285
290
                        if(isDisplayingUntimedTrace && nextStep instanceof TAPNNetworkTimedTransitionStep){
286
 
                                AnimationHistoryComponent untimedAnimationHistory = tab.getUntimedAnimationHistory();
 
291
                                AnimationHistoryComponent<String> untimedAnimationHistory = tab.getUntimedAnimationHistory();
287
292
                                String nextInUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);
288
293
                                if(nextInUntimedTrace.equals(nextStep.toString())){
289
294
                                        untimedAnimationHistory.stepForward();
326
331
                
327
332
                TimeInterval dInterval = transition.getdInterval();
328
333
                
329
 
                BigDecimal delayGranularity = CreateGui.getCurrentTab().getDelayEnabledTransitionControl().getValue();
 
334
                BigDecimal delayGranularity = tab.getDelayEnabledTransitionControl().getValue();
330
335
                //Make sure the granularity is small enough
331
336
                BigDecimal lowerBound = IntervalOperations.getRatBound(dInterval.lowerBound()).getBound();
332
337
                if(!dInterval.IsLowerBoundNonStrict() && !dInterval.isIncluded(lowerBound.add(delayGranularity))){
338
343
                if(delayGranularity.compareTo(new BigDecimal("0.00001")) < 0){
339
344
                        JOptionPane.showMessageDialog(CreateGui.getApp(), "<html>Due to the limit of only five decimal points in the simulator</br> its not possible to fire the transition</html>");
340
345
                } else {
341
 
                        BigDecimal delay = CreateGui.getCurrentTab().getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity);
 
346
                        BigDecimal delay = tab.getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity);
342
347
                        if(delay != null){
343
348
                                if(delay.compareTo(BigDecimal.ZERO) != 0){ //Don't delay if the chosen delay is 0
344
349
                                        if(!letTimePass(delay)){
377
382
                // cancelling the token selection dialogue above should not result in changes 
378
383
                // to the untimed animation history
379
384
                if (isDisplayingUntimedTrace){
380
 
                        AnimationHistoryComponent untimedAnimationHistory = tab.getUntimedAnimationHistory();
 
385
                        AnimationHistoryComponent<String> untimedAnimationHistory = tab.getUntimedAnimationHistory();
381
386
                        if(untimedAnimationHistory.isStepForwardAllowed()){
382
387
                                String nextFromUntimedTrace = untimedAnimationHistory.getElement(untimedAnimationHistory.getSelectedIndex()+1);
383
388
 
433
438
        public void reportBlockingPlaces(){
434
439
 
435
440
                try{
436
 
                        BigDecimal delay = CreateGui.getCurrentTab().getAnimationController().getCurrentDelay();
 
441
                        BigDecimal delay = tab.getAnimationController().getCurrentDelay();
437
442
                if(isUrgentTransitionEnabled && delay.compareTo(new BigDecimal(0))>0){
438
 
                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
 
443
                        tab.getAnimationController().getOkButton().setEnabled(false);
439
444
                        StringBuilder sb = new StringBuilder();
440
445
                        sb.append("<html>Time delay is disabled due to the<br /> following enabled urgent transitions:<br /><br />");
441
 
                        for( Template temp : CreateGui.getCurrentTab().activeTemplates()){
 
446
                        for( Template temp : tab.activeTemplates()){
442
447
                                Iterator<Transition> transitionIterator = temp.guiModel().returnTransitions();
443
448
                                while (transitionIterator.hasNext()) {
444
449
                                        Transition tempTransition = transitionIterator.next();
448
453
                                }
449
454
                        }
450
455
                        sb.append("</html>");
451
 
                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText(sb.toString());
 
456
                        tab.getAnimationController().getOkButton().setToolTipText(sb.toString());
452
457
                        return;
453
458
                }
454
459
                        if(delay.compareTo(new BigDecimal(0))<0){
455
 
                                CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
456
 
                                CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers");
 
460
                                tab.getAnimationController().getOkButton().setEnabled(false);
 
461
                                tab.getAnimationController().getOkButton().setToolTipText("Time delay is possible only for nonnegative rational numbers");
457
462
                        } else {
458
463
                                List<TimedPlace> blockingPlaces = currentMarking().getBlockingPlaces(delay);
459
464
                                if(blockingPlaces.size() == 0){
460
 
                                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(true);
461
 
                                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText("Press to add the delay");
 
465
                                        tab.getAnimationController().getOkButton().setEnabled(true);
 
466
                                        tab.getAnimationController().getOkButton().setToolTipText("Press to add the delay");
462
467
                                } else {
463
468
                                        StringBuilder sb = new StringBuilder();
464
469
                                        sb.append("<html>Time delay of " + delay + " time unit(s) is disabled due to <br /> age invariants in the following places:<br /><br />");
467
472
                                        }
468
473
                                        //JOptionPane.showMessageDialog(null, sb.toString());
469
474
                                        sb.append("</html>");
470
 
                                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
471
 
                                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText(sb.toString());
 
475
                                        tab.getAnimationController().getOkButton().setEnabled(false);
 
476
                                        tab.getAnimationController().getOkButton().setToolTipText(sb.toString());
472
477
                                }
473
478
                        }
474
479
                } catch (NumberFormatException e) {
475
480
                        // Do nothing, invalud number
476
481
                } catch (ParseException e) {
477
 
                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setEnabled(false);
478
 
                        CreateGui.getCurrentTab().getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number");
 
482
                        tab.getAnimationController().getOkButton().setEnabled(false);
 
483
                        tab.getAnimationController().getOkButton().setToolTipText("The text in the input field is not a number");
479
484
                }
480
485
        }
481
486
 
483
488
                return tab.currentTemplate().guiModel();
484
489
        }
485
490
 
486
 
        public void resethistory() {
 
491
        private void resethistory() {
487
492
                actionHistory.clear();
488
493
                markings.clear();
489
494
                currentAction = -1;
511
516
                        removeStoredActions(currentAction + 1);
512
517
 
513
518
                tab.network().setMarking(marking);
514
 
                CreateGui.getCurrentTab().getAnimationHistory().addHistoryItem(action.toString());
 
519
                tab.getAnimationHistory().addHistoryItem(action.toString());
515
520
                actionHistory.add(action);
516
521
                markings.add(marking);
517
522
                currentAction++;
524
529
        }
525
530
 
526
531
        public void setFiringmode(String t) {
527
 
                if (t.equals("Random")) {
528
 
                        firingmode = new RandomFiringMode();
529
 
                } else if (t.equals("Youngest")) {
530
 
                        firingmode = new YoungestFiringMode();
531
 
                } else if (t.equals("Oldest")) {
532
 
                        firingmode = new OldestFiringMode();
533
 
                } else if (t.equals("Manual")) {
534
 
                        firingmode = null;
535
 
                } else {
536
 
                        System.err
537
 
                        .println("Illegal firing mode mode: " + t + " not found.");
 
532
                switch (t) {
 
533
                        case "Random":
 
534
                                firingmode = new RandomFiringMode();
 
535
                                break;
 
536
                        case "Youngest":
 
537
                                firingmode = new YoungestFiringMode();
 
538
                                break;
 
539
                        case "Oldest":
 
540
                                firingmode = new OldestFiringMode();
 
541
                                break;
 
542
                        case "Manual":
 
543
                                firingmode = null;
 
544
                                break;
 
545
                        default:
 
546
                                System.err
 
547
                                                .println("Illegal firing mode mode: " + t + " not found.");
 
548
                                break;
538
549
                }
539
550
 
540
 
                CreateGui.getCurrentTab().getAnimationController().updateFiringModeComboBox();
541
 
                CreateGui.getCurrentTab().getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing");
 
551
                tab.getAnimationController().updateFiringModeComboBox();
 
552
                tab.getAnimationController().setToolTipText("Select a method for choosing tokens during transition firing");
542
553
        }       
543
554
 
544
555
        enum FillListStatus{
603
614
                }
604
615
        }
605
616
 
606
 
        public List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) {
 
617
        private List<TimedToken> showSelectSimulatorDialogue(TimedTransition transition) {
607
618
                EscapableDialog guiDialog = new EscapableDialog(CreateGui.getApp(), "Select Tokens", true);
608
619
 
609
620
                Container contentPane = guiDialog.getContentPane();
633
644
                }
634
645
        }
635
646
 
636
 
        public boolean removeSetTrace(boolean askUser){
 
647
        private boolean removeSetTrace(boolean askUser){
637
648
                if(askUser && isShowingTrace()){ //Warn about deleting trace
638
649
                        int answer = JOptionPane.showConfirmDialog(CreateGui.getApp(), 
639
650
                                        "You are about to remove the current trace.", 
641
652
                        if(answer != JOptionPane.OK_OPTION) return false;
642
653
                }
643
654
                if(isDisplayingUntimedTrace){
644
 
                        CreateGui.getCurrentTab().removeAbstractAnimationPane();
 
655
                        tab.removeAbstractAnimationPane();
645
656
                }
646
657
                isDisplayingUntimedTrace = false;
647
658
                trace = null;
658
669
                        answer = removeSetTrace(true);
659
670
                }
660
671
                if(answer){
661
 
                        CreateGui.getCurrentTab().getAnimationHistory().clearStepsForward();
 
672
                        tab.getAnimationHistory().clearStepsForward();
662
673
                }
663
674
                return answer;
664
675
        }
665
676
 
666
 
        public boolean isShowingTrace(){
 
677
        private boolean isShowingTrace(){
667
678
                return isDisplayingUntimedTrace || trace != null;
668
679
        }
669
680
        
670
 
        public ArrayList<TAPNNetworkTraceStep> getActionHistory() {
671
 
            return actionHistory;
672
 
        }   
 
681
        public ArrayList<TAPNNetworkTraceStep> getActionHistory() {
 
682
                return actionHistory;
 
683
        }
673
684
        
674
685
}