← Back to branch summary

~tapaal-contributor/tapaal/query-export-bug-1767615

« back to all changes in this revision

Viewing changes to src/pipe/gui/GuiFrame.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/GuiFrame.java
67
67
import pipe.gui.graphicElements.tapn.*;
68
68
import pipe.gui.handler.SpecialMacHandler;
69
69
import pipe.gui.undo.ChangeSpacingEdit;
70
 
import pipe.gui.undo.DeleteTransportArcCommand;
71
 
import pipe.gui.undo.UndoManager;
72
70
import pipe.gui.widgets.EngineDialogPanel;
73
71
import pipe.gui.widgets.EscapableDialog;
74
72
import pipe.gui.widgets.FileBrowser;
129
127
        private TypeAction annotationAction, arcAction, inhibarcAction,
130
128
        placeAction, transAction, timedtransAction, tokenAction,
131
129
        selectAction, deleteTokenAction, timedPlaceAction;
132
 
        private ViewAction showTokenAgeAction, showComponentsAction, showQueriesAction, showConstantsAction,showZeroToInfinityIntervalsAction,showEnabledTransitionsAction,showBlueTransitionsAction,showToolTipsAction,showAdvancedWorkspaceAction,showSimpleWorkspaceAction,saveWorkSpaceAction;
 
130
        private ViewAction showTokenAgeAction, showComponentsAction, showQueriesAction, showConstantsAction,showZeroToInfinityIntervalsAction,showEnabledTransitionsAction, showDelayEnabledTransitionsAction,showToolTipsAction,showAdvancedWorkspaceAction,showSimpleWorkspaceAction,saveWorkSpaceAction;
133
131
        private HelpAction showAboutAction, showHomepage, showAskQuestionAction, showReportBugAction, showFAQAction, checkUpdate;
134
132
 
135
133
        private JMenuItem statistics;
154
152
        private JCheckBoxMenuItem showComponentsCheckBox;
155
153
        private JCheckBoxMenuItem showQueriesCheckBox;
156
154
        private JCheckBoxMenuItem showEnabledTransitionsCheckBox;
157
 
        private JCheckBoxMenuItem showBlueTransitionsCheckBox;
 
155
        private JCheckBoxMenuItem showDelayEnabledTransitionsCheckBox;
158
156
        private JCheckBoxMenuItem showConstantsCheckBox;
159
157
        private JCheckBoxMenuItem showToolTipsCheckBox;
160
158
        private JCheckBoxMenuItem showTokenAgeCheckBox;
163
161
        private boolean showConstants = true;
164
162
        private boolean showQueries = true;
165
163
        private boolean showEnabledTransitions = true;
166
 
        private boolean showBlueTransitions = true;
 
164
        private boolean showDelayEnabledTransitions = true;
167
165
        private boolean showToolTips = true;
168
166
 
169
167
        private GUIMode guiMode = GUIMode.noNet;
255
253
                showConstants = prefs.getShowConstants();
256
254
 
257
255
                showEnabledTransitions = prefs.getShowEnabledTransitions();
258
 
                showBlueTransitions = prefs.getShowBlueTransitions();
259
 
                BlueTransitionControl.setDefaultDelayMode(prefs.getBlueTransitionDelayMode());
260
 
                BlueTransitionControl.setDefaultGranularity(prefs.getBlueTransitionGranularity());
261
 
                BlueTransitionControl.setDefaultIsRandomTransition(prefs.getBlueTransitionIsRandomTransition());
 
256
                showDelayEnabledTransitions = prefs.getShowDelayEnabledTransitions();
 
257
                DelayEnabledTransitionControl.setDefaultDelayMode(prefs.getDelayEnabledTransitionDelayMode());
 
258
                DelayEnabledTransitionControl.setDefaultGranularity(prefs.getDelayEnabledTransitionGranularity());
 
259
                DelayEnabledTransitionControl.setDefaultIsRandomTransition(prefs.getDelayEnabledTransitionIsRandomTransition());
262
260
 
263
261
                showToolTips = prefs.getShowToolTips();
264
262
 
601
599
                                showEnabledTransitionsCheckBox = new JCheckBoxMenuItem());
602
600
                showEnabledTransitionsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('4', shortcutkey));
603
601
 
604
 
                addCheckboxMenuItem(viewMenu, showBlueTransitions, showBlueTransitionsAction = new ViewAction("Display future-enabled transitions",
 
602
                addCheckboxMenuItem(viewMenu, showDelayEnabledTransitions, showDelayEnabledTransitionsAction = new ViewAction("Display future-enabled transitions",
605
603
                                453247, "Highlight transitions which can be enabled after a delay","ctrl 5",true),
606
 
                                showBlueTransitionsCheckBox = new JCheckBoxMenuItem());
607
 
                showBlueTransitionsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('5', shortcutkey));
 
604
                                showDelayEnabledTransitionsCheckBox = new JCheckBoxMenuItem());
 
605
                showDelayEnabledTransitionsAction.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke('5', shortcutkey));
608
606
 
609
607
                addCheckboxMenuItem(viewMenu, CreateGui.showZeroToInfinityIntervals(), showZeroToInfinityIntervalsAction = new ViewAction("Display intervals [0,inf)",
610
608
                                453246, "Show/hide intervals [0,inf) that do not restrict transition firing in any way.","ctrl 6",true),
808
806
                if(!CreateGui.showTokenAge()){
809
807
                        showTokenAgeCheckBox.doClick();
810
808
                }
811
 
                //BlueTransitions
812
 
                showBlueTransitions(advanced);
813
 
                BlueTransitionControl.getInstance().setValue(new BigDecimal("0.1"));
814
 
                BlueTransitionControl.getInstance().setDelayMode(ShortestDelayMode.getInstance());
815
 
                BlueTransitionControl.getInstance().setRandomTransitionMode(false);
 
809
                //Delay-enabled Transitions
 
810
                showDelayEnabledTransitions(advanced);
 
811
                DelayEnabledTransitionControl.getInstance().setValue(new BigDecimal("0.1"));
 
812
                DelayEnabledTransitionControl.getInstance().setDelayMode(ShortestDelayMode.getInstance());
 
813
                DelayEnabledTransitionControl.getInstance().setRandomTransitionMode(false);
816
814
        }
817
815
 
818
816
        public void saveWorkspace(){
828
826
                prefs.setShowConstants(showConstants);
829
827
 
830
828
                prefs.setShowEnabledTrasitions(showEnabledTransitions);
831
 
                prefs.setShowBlueTransitions(showBlueTransitions);
 
829
                prefs.setShowDelayEnabledTransitions(showDelayEnabledTransitions);
832
830
                prefs.setShowTokenAge(CreateGui.showTokenAge());
833
 
                prefs.setBlueTransitionDelayMode(BlueTransitionControl.getDefaultDelayMode());
834
 
                prefs.setBlueTransitionGranularity(BlueTransitionControl.getDefaultGranularity());
835
 
                prefs.setBlueTransitionIsRandomTransition(BlueTransitionControl.isRandomTransition());
 
831
                prefs.setDelayEnabledTransitionDelayMode(DelayEnabledTransitionControl.getDefaultDelayMode());
 
832
                prefs.setDelayEnabledTransitionGranularity(DelayEnabledTransitionControl.getDefaultGranularity());
 
833
                prefs.setDelayEnabledTransitionIsRandomTransition(DelayEnabledTransitionControl.isRandomTransition());
836
834
 
837
835
                JOptionPane.showMessageDialog(this, 
838
836
                                "The workspace has now been saved into your preferences.\n" 
1031
1029
 
1032
1030
                        deleteAction.setEnabled(true);
1033
1031
                        showEnabledTransitionsAction.setEnabled(false);
1034
 
                        showBlueTransitionsAction.setEnabled(false);
 
1032
                        showDelayEnabledTransitionsAction.setEnabled(false);
1035
1033
 
1036
1034
                        verifyAction.setEnabled(CreateGui.getCurrentTab().isQueryPossible());
1037
1035
 
1173
1171
                showQueriesAction.setEnabled(enable);
1174
1172
                showZeroToInfinityIntervalsAction.setEnabled(enable);
1175
1173
                showEnabledTransitionsAction.setEnabled(enable);
1176
 
                showBlueTransitionsAction.setEnabled(enable);
 
1174
                showDelayEnabledTransitionsAction.setEnabled(enable);
1177
1175
                showToolTipsAction.setEnabled(enable);
1178
1176
                showTokenAgeAction.setEnabled(enable);
1179
1177
                showAdvancedWorkspaceAction.setEnabled(enable);
1304
1302
                showEnabledTransitionsList(!showEnabledTransitions);
1305
1303
        }
1306
1304
 
1307
 
        public void showBlueTransitions(boolean enable){
1308
 
                showBlueTransitions = enable;
1309
 
                CreateGui.getCurrentTab().showBlueTransitions(enable);
1310
 
                showBlueTransitionsCheckBox.setSelected(enable);
 
1305
        public void showDelayEnabledTransitions(boolean enable){
 
1306
                showDelayEnabledTransitions = enable;
 
1307
                CreateGui.getCurrentTab().showDelayEnabledTransitions(enable);
 
1308
                showDelayEnabledTransitionsCheckBox.setSelected(enable);
1311
1309
        }
1312
 
        public void toggleBlueTransitions(){
1313
 
                showBlueTransitions(!showBlueTransitions);
 
1310
        public void toggleDelayEnabledTransitions(){
 
1311
                showDelayEnabledTransitions(!showDelayEnabledTransitions);
1314
1312
        }
1315
1313
 
1316
1314
        public void saveOperation(boolean forceSave){
2388
2386
                                toggleZeroToInfinityIntervals();
2389
2387
                        } else if (this == showEnabledTransitionsAction) {
2390
2388
                                toggleEnabledTransitionsList();
2391
 
                        } else if (this == showBlueTransitionsAction) {
2392
 
                                toggleBlueTransitions();
 
2389
                        } else if (this == showDelayEnabledTransitionsAction) {
 
2390
                                toggleDelayEnabledTransitions();
2393
2391
                        } else if (this == showToolTipsAction) {
2394
2392
                                toggleToolTips();
2395
2393
                        } else if (this == showTokenAgeAction) {
2735
2733
                return appTab.getTitleAt(appTab.getSelectedIndex());
2736
2734
        }
2737
2735
 
2738
 
        public boolean isShowingBlueTransitions() {
2739
 
                return showBlueTransitions;
 
2736
        public boolean isShowingDelayEnabledTransitions() {
 
2737
                return showDelayEnabledTransitions;
2740
2738
        }
2741
2739
 
2742
2740
}