← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/BlueTransitionControl.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/BlueTransitionControl.java
1
 
package pipe.gui;
2
 
 
3
 
import java.awt.BorderLayout;
4
 
import java.awt.Dimension;
5
 
import java.awt.Frame;
6
 
import java.awt.GridBagConstraints;
7
 
import java.awt.GridBagLayout;
8
 
import java.awt.Insets;
9
 
import java.awt.event.ActionEvent;
10
 
import java.awt.event.ActionListener;
11
 
import java.math.BigDecimal;
12
 
import java.math.MathContext;
13
 
import java.util.Hashtable;
14
 
 
15
 
import javax.swing.BorderFactory;
16
 
import javax.swing.JButton;
17
 
import javax.swing.JCheckBox;
18
 
import javax.swing.JComboBox;
19
 
import javax.swing.JDialog;
20
 
import javax.swing.JLabel;
21
 
import javax.swing.JPanel;
22
 
import javax.swing.JSlider;
23
 
 
24
 
import pipe.gui.widgets.EscapableDialog;
25
 
 
26
 
import dk.aau.cs.model.tapn.simulation.DelayMode;
27
 
import dk.aau.cs.model.tapn.simulation.ManualDelayMode;
28
 
import dk.aau.cs.model.tapn.simulation.RandomDelayMode;
29
 
import dk.aau.cs.model.tapn.simulation.ShortestDelayMode;
30
 
 
31
 
public class BlueTransitionControl extends JPanel{
32
 
 
33
 
        private static final long serialVersionUID = -5735674907635981304L;
34
 
        private static DelayMode defaultDelayMode = ShortestDelayMode.getInstance();
35
 
        private static BigDecimal defaultGranularity = new BigDecimal("0.1");
36
 
        private static boolean defaultIsRandomTrasition;
37
 
        
38
 
        JLabel precitionLabel;
39
 
        JSlider bluePrecision;
40
 
        JLabel delayModeLabel;
41
 
        JComboBox delayMode;
42
 
        JCheckBox randomMode;
43
 
        
44
 
        private BlueTransitionControl() {
45
 
                super(new GridBagLayout());
46
 
                
47
 
                //0 corresponds to 0.00001, 5 corresponds to 1 (   thus x corresponds to 1/(10^(5−x))  )
48
 
                bluePrecision = new JSlider(JSlider.HORIZONTAL, 0, 5, 4);
49
 
                Hashtable<Integer, JLabel> labelTable = new Hashtable<Integer, JLabel>();
50
 
                labelTable.put(new Integer(0), new JLabel("0.00001"));
51
 
                labelTable.put(new Integer(1), new JLabel("0.0001"));
52
 
                labelTable.put(new Integer(2), new JLabel("0.001"));
53
 
                labelTable.put(new Integer(3), new JLabel("0.01"));
54
 
                labelTable.put(new Integer(4), new JLabel("0.1"));
55
 
                labelTable.put(new Integer(5), new JLabel("1"));
56
 
                
57
 
                bluePrecision.setLabelTable(labelTable);
58
 
                bluePrecision.setSnapToTicks(true);
59
 
                bluePrecision.setMajorTickSpacing(1);
60
 
                bluePrecision.setPaintLabels(true);
61
 
                bluePrecision.setPaintTicks(true);
62
 
                bluePrecision.setPaintTrack(false);
63
 
                bluePrecision.setPreferredSize(new Dimension(340, bluePrecision.getPreferredSize().height));
64
 
                setValue(defaultGranularity);
65
 
                //UIManager.put("Slider.paintValue", false);
66
 
                //UIManager.getLookAndFeelDefaults().put("Slider.paintValue", false);
67
 
                
68
 
                //TODO is this good? it's the only soloution I've found
69
 
                //It makes sure the value of the slider is NOT written 
70
 
                //above the knob.
71
 
                /*Class<?> sliderUIClass;
72
 
                try {
73
 
                        sliderUIClass = Class.forName("javax.swing.plaf.synth.SynthSliderUI");
74
 
                        Field paintValue = sliderUIClass.getDeclaredField("paintValue");
75
 
                paintValue.setAccessible(true);
76
 
                paintValue.set(bluePrecision.getUI(), false);
77
 
                } catch (Exception e) {
78
 
                        e.printStackTrace();
79
 
                }*/
80
 
                
81
 
                DelayMode[] items = {ShortestDelayMode.getInstance(), RandomDelayMode.getInstance(), ManualDelayMode.getInstance()};
82
 
                delayMode = new JComboBox(items);
83
 
                setDelayMode(defaultDelayMode);
84
 
                
85
 
                randomMode = new JCheckBox("Choose next transition randomly");
86
 
                setRandomTransitionMode(defaultIsRandomTrasition);
87
 
        
88
 
                GridBagConstraints gbc = new GridBagConstraints();
89
 
                gbc.gridwidth = 2;
90
 
                gbc.anchor = GridBagConstraints.WEST;
91
 
                gbc.fill = GridBagConstraints.HORIZONTAL;
92
 
                gbc.weightx = 1.0;
93
 
                gbc.gridx = 0;
94
 
                gbc.gridy = 0;
95
 
                add(precitionLabel = new JLabel("Set the delay granularity"), gbc);
96
 
                
97
 
                gbc = new GridBagConstraints();
98
 
                gbc.gridwidth = 2;
99
 
                gbc.anchor = GridBagConstraints.WEST;
100
 
                gbc.fill = GridBagConstraints.HORIZONTAL;
101
 
                gbc.weightx = 1.0;
102
 
                gbc.gridx = 0;
103
 
                gbc.gridy = 1;
104
 
                add(bluePrecision, gbc);
105
 
                
106
 
                gbc = new GridBagConstraints();
107
 
                gbc.anchor = GridBagConstraints.WEST;
108
 
                gbc.fill = GridBagConstraints.HORIZONTAL;
109
 
                gbc.gridx = 0;
110
 
                gbc.gridy = 2;
111
 
                add(delayModeLabel = new JLabel("Delay Mode:"), gbc);
112
 
                
113
 
                gbc = new GridBagConstraints();
114
 
                gbc.anchor = GridBagConstraints.WEST;
115
 
                gbc.fill = GridBagConstraints.HORIZONTAL;
116
 
                gbc.weightx = 1.0;
117
 
                gbc.gridx = 1;
118
 
                gbc.gridy = 2;
119
 
                add(delayMode, gbc);
120
 
                
121
 
                gbc = new GridBagConstraints();
122
 
                gbc.anchor = GridBagConstraints.WEST;
123
 
                gbc.weightx = 1.0;
124
 
                gbc.gridx = 0;
125
 
                gbc.gridy = 3;
126
 
                add(randomMode, gbc);
127
 
                
128
 
                setBorder(BorderFactory.createCompoundBorder(
129
 
                                BorderFactory.createTitledBorder("Delay controller"), 
130
 
                                BorderFactory.createEmptyBorder(3, 3, 3, 3)));
131
 
        }
132
 
        
133
 
        private int getValueFromDecimal(BigDecimal decimal) {
134
 
                if(new BigDecimal("0.00001").compareTo(decimal) == 0) return 0;
135
 
                if(new BigDecimal("0.0001").compareTo(decimal) == 0) return 1;
136
 
                if(new BigDecimal("0.001").compareTo(decimal) == 0) return 2;
137
 
                if(new BigDecimal("0.01").compareTo(decimal) == 0) return 3;
138
 
                if(new BigDecimal("0.1").compareTo(decimal) == 0) return 4;
139
 
                if(new BigDecimal("1").compareTo(decimal) == 0) return 5;
140
 
                return 4;
141
 
        }
142
 
 
143
 
        //0 corresponds to 0.00001, 5 corresponds to 1 (   thus x corresponds to 1/(10^(5−x))  )
144
 
        public BigDecimal getValue(){ 
145
 
                return new BigDecimal(1.0/(Math.pow(10.0, (5.0-bluePrecision.getValue()))), new MathContext(Pipe.AGE_PRECISION));
146
 
        }
147
 
        
148
 
        public void setValue(BigDecimal value){
149
 
                bluePrecision.setValue(getValueFromDecimal(value));
150
 
        }
151
 
        
152
 
        public DelayMode getDelayMode(){
153
 
                return (DelayMode)delayMode.getSelectedItem();
154
 
        }
155
 
        
156
 
        public void setDelayMode(DelayMode delayMode){
157
 
                this.delayMode.setSelectedItem(delayMode);
158
 
        }
159
 
        
160
 
        public boolean isRandomTransitionMode(){
161
 
                if(SimulationControl.getInstance().randomSimulation()){
162
 
                        return true;
163
 
                } else {
164
 
                        return randomMode.isSelected();
165
 
                }
166
 
        }
167
 
        
168
 
        public void setRandomTransitionMode(boolean randomTransition){
169
 
                randomMode.setSelected(randomTransition);
170
 
        }
171
 
        
172
 
        private static BlueTransitionControl instance;
173
 
        private static JButton closeDialogButton;
174
 
        private static JDialog dialog;
175
 
        
176
 
        public static void showBlueTransitionDialog(){
177
 
                JPanel contentPane = new JPanel(new GridBagLayout());
178
 
                
179
 
                closeDialogButton = new JButton("Close");
180
 
                closeDialogButton.addActionListener(new ActionListener() {
181
 
                        
182
 
                        public void actionPerformed(ActionEvent arg0) {
183
 
                                dialog.setVisible(false);
184
 
                        }
185
 
                });
186
 
                
187
 
                GridBagConstraints gbc = new GridBagConstraints();
188
 
                gbc.anchor = GridBagConstraints.NORTHWEST;
189
 
                gbc.insets = new Insets(0, 3, 0, 3);
190
 
                gbc.fill = GridBagConstraints.BOTH;
191
 
                contentPane.add(getInstance(), gbc);
192
 
                
193
 
                gbc = new GridBagConstraints();
194
 
                gbc.anchor = GridBagConstraints.NORTHWEST;
195
 
                gbc.insets = new Insets(3, 3, 0, 3);
196
 
                gbc.gridy = 1;
197
 
                gbc.fill = GridBagConstraints.HORIZONTAL;
198
 
                contentPane.add(closeDialogButton, gbc);
199
 
                
200
 
                dialog = new EscapableDialog(CreateGui.getApp(), "Delay controller", true);
201
 
                dialog.setContentPane(contentPane);
202
 
                dialog.pack();
203
 
                dialog.setResizable(false);
204
 
                dialog.setLocationRelativeTo(CreateGui.getApp());
205
 
                dialog.setVisible(true);
206
 
        }
207
 
        
208
 
        public static BlueTransitionControl getInstance(){
209
 
                if(instance == null){
210
 
                        instance = new BlueTransitionControl();
211
 
                }
212
 
                return instance;
213
 
        }
214
 
        
215
 
        public static void setDefaultDelayMode(DelayMode delayMode){
216
 
                defaultDelayMode = delayMode;
217
 
        }
218
 
        
219
 
        public static DelayMode getDefaultDelayMode(){
220
 
                if(instance != null){
221
 
                        return getInstance().getDelayMode();
222
 
                } else {
223
 
                        return defaultDelayMode;
224
 
                }
225
 
        }
226
 
        
227
 
        public static void setDefaultGranularity(BigDecimal granularity){
228
 
                defaultGranularity = granularity;
229
 
        }
230
 
        
231
 
        public static BigDecimal getDefaultGranularity(){
232
 
                if(instance != null){
233
 
                        return getInstance().getValue();
234
 
                } else {
235
 
                        return defaultGranularity;
236
 
                }
237
 
        }
238
 
 
239
 
        public static void setDefaultIsRandomTransition(boolean blueTransitionIsRandomTransition) {
240
 
                defaultIsRandomTrasition = blueTransitionIsRandomTransition;
241
 
        }
242
 
        
243
 
        public static boolean isRandomTransition(){
244
 
                if(instance != null){
245
 
                        return getInstance().isRandomTransitionMode();
246
 
                } else {
247
 
                        return defaultIsRandomTrasition;
248
 
                }
249
 
        }
250
 
        
251
 
        @Override
252
 
        public void setEnabled(boolean enabled) {
253
 
                super.setEnabled(enabled);
254
 
                precitionLabel.setEnabled(enabled);
255
 
                bluePrecision.setEnabled(enabled);
256
 
                delayModeLabel.setEnabled(enabled);
257
 
                delayMode.setEnabled(enabled);
258
 
                randomMode.setEnabled(enabled);
259
 
        }
260
 
}