← Back to branch summary

~tapaal-contributor/tapaal/save-as-fix-1648076

« back to all changes in this revision

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

merged in branch fixing enabled-transition-in-editor-fix-1641313
that also changes the future enabled transitions from blue to yellow

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/Animator.java
36
36
import dk.aau.cs.util.RequireException;
37
37
import dk.aau.cs.util.Tuple;
38
38
import dk.aau.cs.verification.VerifyTAPN.TraceType;
39
 
import pipe.gui.AnimationHistoryComponent;
40
39
 
41
40
public class Animator {
42
41
        private ArrayList<TAPNNetworkTraceStep> actionHistory;
146
145
                Iterator<Transition> transitionIterator = current.returnTransitions();
147
146
                while (transitionIterator.hasNext()) {
148
147
                        Transition tempTransition = transitionIterator.next();
149
 
                        if (tempTransition.isEnabled(true) || (tempTransition.isBlueTransition(true) && !isUrgentTransitionEnabled)) {
 
148
                        if (tempTransition.isEnabled(true) || (tempTransition.isDelayEnabledTransition(true) && !isUrgentTransitionEnabled)) {
150
149
                                current.notifyObservers();
151
150
                                tempTransition.repaint();
152
151
                        }
162
161
                Iterator<Transition> transitionIterator = current.returnTransitions();
163
162
                while (transitionIterator.hasNext()) {
164
163
                        Transition tempTransition = transitionIterator.next();
165
 
                        if (!(tempTransition.isEnabled(true)) || !tempTransition.isBlueTransition(true) || (tempTransition.isBlueTransition(true) && isUrgentTransitionEnabled)) {
 
164
                        if (!(tempTransition.isEnabled(true)) || !tempTransition.isDelayEnabledTransition(true) || (tempTransition.isDelayEnabledTransition(true) && isUrgentTransitionEnabled)) {
166
165
                                current.notifyObservers();
167
166
                                tempTransition.repaint();
168
167
                        }
189
188
                        Iterator<Transition> transitionIterator = temp.guiModel().returnTransitions();
190
189
                        while (transitionIterator.hasNext()) {
191
190
                                Transition tempTransition = transitionIterator.next();
192
 
                                if (tempTransition.isEnabled(true) || (tempTransition.isBlueTransition(true) && CreateGui.getApp().isShowingBlueTransitions() && !isUrgentTransitionEnabled)) {
 
191
                                if (tempTransition.isEnabled(true) || (tempTransition.isDelayEnabledTransition(true) && CreateGui.getApp().isShowingDelayEnabledTransitions() && !isUrgentTransitionEnabled)) {
193
192
                                        transFireComponent.addTransition(temp, tempTransition);
194
193
                                }
195
194
                        }
209
208
                        while (transitionIterator.hasNext()) {
210
209
                                Transition tempTransition = transitionIterator.next();
211
210
                                tempTransition.setEnabledFalse();
212
 
                                tempTransition.setBlueTransitionFalse();
 
211
                                tempTransition.setDelayEnabledTransitionFalse();
213
212
                                activeGuiModel().notifyObservers();
214
213
                                tempTransition.repaint();
215
214
                        }
323
322
        }
324
323
        
325
324
        public void dFireTransition(TimedTransition transition){
326
 
                if(!CreateGui.getApp().isShowingBlueTransitions() || isUrgentTransitionEnabled()){
 
325
                if(!CreateGui.getApp().isShowingDelayEnabledTransitions() || isUrgentTransitionEnabled()){
327
326
                        fireTransition(transition);
328
327
                        return;
329
328
                }
330
329
                
331
330
                TimeInterval dInterval = transition.getdInterval();
332
331
                
333
 
                BigDecimal delayGranularity = CreateGui.getCurrentTab().getBlueTransitionControl().getValue();
 
332
                BigDecimal delayGranularity = CreateGui.getCurrentTab().getDelayEnabledTransitionControl().getValue();
334
333
                //Make sure the granularity is small enough
335
334
                BigDecimal lowerBound = IntervalOperations.getRatBound(dInterval.lowerBound()).getBound();
336
335
                if(!dInterval.IsLowerBoundNonStrict() && !dInterval.isIncluded(lowerBound.add(delayGranularity))){
342
341
                if(delayGranularity.compareTo(new BigDecimal("0.00001")) < 0){
343
342
                        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>");
344
343
                } else {
345
 
                        BigDecimal delay = CreateGui.getCurrentTab().getBlueTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity);
 
344
                        BigDecimal delay = CreateGui.getCurrentTab().getDelayEnabledTransitionControl().getDelayMode().GetDelay(transition, dInterval, delayGranularity);
346
345
                        if(delay != null){
347
346
                                if(delay.compareTo(BigDecimal.ZERO) != 0){ //Don't delay if the chosen delay is 0
348
347
                                        if(!letTimePass(delay)){