← Back to branch summary

~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

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

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-04-12 09:50:16 UTC
  • mfrom: (329.1.188 tapaal-1.5)
  • Revision ID: mail@yrke.dk-20110412095016-e4hqdgab5596ja09
Merged with branch addning support for new 1.5 features

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/AnimationController.java
1
1
package pipe.gui;
2
2
 
 
3
import java.awt.Dimension;
3
4
import java.awt.FlowLayout;
4
5
import java.awt.GridBagConstraints;
5
6
import java.awt.GridBagLayout;
14
15
import java.text.ParseException;
15
16
 
16
17
import javax.swing.Action;
 
18
import javax.swing.BorderFactory;
17
19
import javax.swing.JComboBox;
18
20
import javax.swing.JLabel;
19
21
import javax.swing.JPanel;
21
23
import javax.swing.JToggleButton;
22
24
import javax.swing.JToolBar;
23
25
import javax.swing.KeyStroke;
 
26
import javax.swing.border.EmptyBorder;
24
27
 
25
28
import pipe.dataLayer.NetType;
26
 
import pipe.exception.InvariantViolatedAnimationException;
27
29
import pipe.gui.action.GuiAction;
 
30
import dk.aau.cs.model.tapn.simulation.FiringMode;
28
31
 
29
32
/**
30
33
 * Implementes af class handling drawing of animation functions
31
34
 * 
32
 
 * Copyright 2009
33
 
 * Author Kenneth Yrke Joergensen <kenneth@yrke.dk>
34
 
 * Based on code from GuiFrame
 
35
 * Copyright 2009 Author Kenneth Yrke Joergensen <kenneth@yrke.dk> Based on code
 
36
 * from GuiFrame
35
37
 * 
36
38
 * Licensed under the Open Software License version 3.0
37
39
 */
51
53
                 */
52
54
                private static final long serialVersionUID = -6594894202788511816L;
53
55
 
54
 
 
55
56
                public ToggleButton(Action a) {
56
57
                        super(a);
57
58
                        if (a.getValue(Action.SMALL_ICON) != null) {
61
62
                        a.addPropertyChangeListener(this);
62
63
                }
63
64
 
64
 
 
65
65
                public void propertyChange(PropertyChangeEvent evt) {
66
66
                        if (evt.getPropertyName() == "selected") {
67
 
                                Boolean b = (Boolean)evt.getNewValue();
 
67
                                Boolean b = (Boolean) evt.getNewValue();
68
68
                                if (b != null) {
69
69
                                        setSelected(b.booleanValue());
70
70
                                }
72
72
                }
73
73
 
74
74
        }
 
75
 
75
76
        private void addButton(JToolBar toolBar, GuiAction action) {
76
77
 
77
78
                if (action.getValue("selected") != null) {
82
83
        }
83
84
 
84
85
        AnimateAction startAction, stepforwardAction, stepbackwardAction,
85
 
        randomAction, randomAnimateAction, timeAction;
86
 
 
87
 
        public AnimationController(String text) throws 
88
 
        javax.swing.text.BadLocationException {
89
 
 
90
 
 
91
 
                startAction = new AnimateAction("Simulation mode", 
92
 
                                Pipe.START, "Toggle Simulation Mode", "Ctrl A", true);
93
 
 
94
 
 
95
 
                stepbackwardAction =
96
 
                        new AnimateAction("Back", Pipe.STEPBACKWARD,
97
 
                                        "Step backward a firing", "typed 4" );
98
 
                stepforwardAction  =
99
 
                        new AnimateAction("Forward", Pipe.STEPFORWARD,
100
 
                                        "Step forward a firing", "typed 6" );
 
86
                        randomAction, randomAnimateAction, timeAction;
 
87
 
 
88
        public AnimationController() {
 
89
                startAction = new AnimateAction("Simulation mode", Pipe.START,
 
90
                                "Toggle Simulation Mode", "Ctrl A", true);
 
91
 
 
92
                stepbackwardAction = new AnimateAction("Back", Pipe.STEPBACKWARD,
 
93
                                "Step backward a firing", "typed 4");
 
94
                stepforwardAction = new AnimateAction("Forward", Pipe.STEPFORWARD,
 
95
                                "Step forward a firing", "typed 6");
101
96
 
102
97
                stepbackwardAction.setEnabled(false);
103
98
                stepforwardAction.setEnabled(false);
104
99
 
105
 
                //timeAction = new AnimateAction("Time", Pipe.TIMEPASS, "Let Time pass", "_");
106
 
 
107
 
                randomAction =
108
 
                        new AnimateAction("Random", Pipe.RANDOM,
109
 
                                        "Randomly fire a transition", "typed 5");
110
 
                randomAnimateAction =
111
 
                        new AnimateAction("Simulate", Pipe.ANIMATE,
112
 
                                        "Randomly fire a number of transitions", "typed 7",true);      
113
 
 
 
100
                // timeAction = new AnimateAction("Time", Pipe.TIMEPASS,
 
101
                // "Let Time pass", "_");
 
102
 
 
103
                randomAction = new AnimateAction("Random", Pipe.RANDOM,
 
104
                                "Randomly fire a transition", "typed 5");
 
105
                randomAnimateAction = new AnimateAction("Simulate", Pipe.ANIMATE,
 
106
                                "Randomly fire a number of transitions", "typed 7", true);
114
107
 
115
108
                setLayout(new GridBagLayout());
116
109
                GridBagConstraints c = new GridBagConstraints();
117
110
 
118
 
 
119
 
 
120
 
                //Use the default FlowLayout.
121
 
                //Create everything.
122
 
 
123
 
                JLabel label = new JLabel("Simulator");
124
 
 
125
 
                c.fill = GridBagConstraints.HORIZONTAL;
126
 
                c.weightx = 0.5;
127
 
                c.gridx = 0;
128
 
                c.gridy = 0;
129
 
                add(label, c);
 
111
                // Use the default FlowLayout.
 
112
                // Create everything.
130
113
 
131
114
                firermodebox = new JComboBox(FIRINGMODES);
132
115
                updateFiringModeComboBox();
133
116
 
134
 
 
135
117
                firermodebox.addActionListener(new java.awt.event.ActionListener() {
136
118
                        public void actionPerformed(java.awt.event.ActionEvent evt) {
137
 
 
138
 
                                CreateGui.getAnimator().setFiringmode(firermodebox.getSelectedItem().toString());
 
119
                                CreateGui.getAnimator().setFiringmode(
 
120
                                                (String) firermodebox.getSelectedItem());
139
121
                        }
140
122
                });
141
 
                
 
123
 
142
124
                JToolBar animationToolBar = new JToolBar();
143
125
                animationToolBar.setFloatable(false);
 
126
                animationToolBar.setBorder(new EmptyBorder(0, 0, 0, 0));
144
127
                addButton(animationToolBar, stepbackwardAction);
145
128
                addButton(animationToolBar, stepforwardAction);
146
129
 
149
132
                c.fill = GridBagConstraints.HORIZONTAL;
150
133
                c.weightx = 0.5;
151
134
                c.gridx = 0;
152
 
                c.gridy = 2;
153
 
                add(animationToolBar, c);    
154
 
                
155
 
                if(!CreateGui.getModel().netType().equals(NetType.UNTIMED)){
 
135
                c.gridy = 1;
 
136
                add(animationToolBar, c);
 
137
 
 
138
                if (!CreateGui.getModel().netType().equals(NetType.UNTIMED)) {
156
139
                        JPanel firemode = new JPanel(new FlowLayout(FlowLayout.LEFT));
157
140
 
158
 
                        label = new JLabel("Token selection mode: ");
 
141
                        JLabel label = new JLabel("Token selection mode: ");
159
142
 
160
143
                        firemode.add(label);
161
144
                        firemode.add(firermodebox);
162
145
 
163
 
 
164
 
 
165
146
                        c.weightx = 0.5;
166
147
                        c.gridx = 0;
167
 
                        c.gridy = 1;
 
148
                        c.gridy = 0;
168
149
                        add(firemode, c);
169
 
                        
170
150
 
171
151
                        JPanel timedelayPanel = new JPanel(new FlowLayout(FlowLayout.LEFT));
172
152
 
173
 
 
174
153
                        okButton = new javax.swing.JButton();
175
154
 
176
155
                        okButton.setText("Time delay");
177
 
                        //okButton.setMaximumSize(new java.awt.Dimension(75, 25));
 
156
                        // okButton.setMaximumSize(new java.awt.Dimension(75, 25));
178
157
                        okButton.setMinimumSize(new java.awt.Dimension(75, 25));
179
 
                        //okButton.setPreferredSize(new java.awt.Dimension(75, 25));
 
158
                        // okButton.setPreferredSize(new java.awt.Dimension(75, 25));
180
159
                        okButton.addActionListener(new java.awt.event.ActionListener() {
181
160
                                public void actionPerformed(java.awt.event.ActionEvent evt) {
182
 
                                        //okButtonHandler(evt);
 
161
                                        // okButtonHandler(evt);
183
162
                                        addTimeDelayToHistory();
184
163
                                }
185
164
                        });
186
165
 
187
 
                        TimeDelayField.addKeyListener(new KeyListener(){
 
166
                        TimeDelayField.addKeyListener(new KeyListener() {
188
167
                                public void keyPressed(KeyEvent e) {
189
 
                                        if (e.getKeyCode() == KeyEvent.VK_ENTER){
 
168
                                        if (e.getKeyCode() == KeyEvent.VK_ENTER) {
190
169
                                                addTimeDelayToHistory();
191
170
                                        }
192
171
                                }
193
172
 
194
173
                                public void keyReleased(KeyEvent e) {
195
174
 
196
 
 
197
175
                                }
198
176
 
199
177
                                public void keyTyped(KeyEvent e) {
212
190
                        timedelayPanel.add(TimeDelayField);
213
191
                        timedelayPanel.add(okButton);
214
192
 
215
 
                        //                    c.fill = GridBagConstraints.HORIZONTAL;
216
 
                        //                              c.weightx = 0.5;
217
 
                        //                              c.gridx = 0;
218
 
                        //                              c.gridy = 3;
219
 
                        //                    add(timedelayPanel, c);
220
 
                        animationToolBar.add(timedelayPanel);           
221
 
                }  
 
193
                        // c.fill = GridBagConstraints.HORIZONTAL;
 
194
                        // c.weightx = 0.5;
 
195
                        // c.gridx = 0;
 
196
                        // c.gridy = 3;
 
197
                        // add(timedelayPanel, c);
 
198
                        animationToolBar.add(timedelayPanel);
 
199
                }
 
200
 
 
201
                setBorder(BorderFactory.createCompoundBorder(BorderFactory
 
202
                                .createTitledBorder("Simulation Control"), BorderFactory
 
203
                                .createEmptyBorder(3, 3, 3, 3)));
 
204
                this.setPreferredSize(new Dimension(275, 100));
 
205
                this.setMinimumSize(new Dimension(275, 100));
222
206
        }
223
207
 
224
208
        public void updateFiringModeComboBox() {
225
 
                String currentFiringMode = CreateGui.getAnimator().getFiringmode().getName();
226
 
                firermodebox.setSelectedItem(currentFiringMode);
227
 
        }
228
 
 
229
 
        public void addTimeDelayToHistory(BigDecimal delay){
230
 
                AnimationHistory animBox = CreateGui.getAnimationHistory();
231
 
                animBox.clearStepsForward();
232
 
                try {
233
 
 
234
 
                        BigDecimal timeDelayToSet  =  delay;
235
 
 
236
 
 
237
 
                        //      BigDecimal timeDelayToSet = new BigDecimal(TimeDelayField.getText(), new MathContext(Pipe.AGE_PRECISION));
238
 
                        if (timeDelayToSet.compareTo(new BigDecimal(0l))<=0){
239
 
                                //Nothing to do, illegal value 
240
 
                                System.err.println("Illegal value");
241
 
                        }else{
242
 
                                CreateGui.getAnimator().letTimePass(timeDelayToSet);                                                     
243
 
                        }
244
 
                } catch (NumberFormatException e) {
245
 
                        //Do nothing, invalud number 
246
 
                } catch (InvariantViolatedAnimationException e) {
247
 
                        // TODO Auto-generated catch block
248
 
                        System.err.println("Invariant Violated, TimeDelay Not allowed");
249
 
                } 
250
 
 
251
 
                setAnimationButtonsEnabled();
252
 
        }
253
 
 
254
 
        private void addTimeDelayToHistory(){
255
 
                AnimationHistory animBox = CreateGui.getAnimationHistory();
256
 
                animBox.clearStepsForward();
257
 
                try {
258
 
 
259
 
                        //Hack to allow usage of localised numbes
 
209
                FiringMode currentFiringMode = CreateGui.getAnimator().getFiringmode();
 
210
                if (currentFiringMode == null) {
 
211
                        firermodebox.setSelectedItem("Manual");
 
212
                } else {
 
213
                        firermodebox.setSelectedItem(currentFiringMode.toString());
 
214
                }
 
215
 
 
216
        }
 
217
 
 
218
        private void addTimeDelayToHistory() {
 
219
                AnimationHistoryComponent animBox = CreateGui.getAnimationHistory();
 
220
                animBox.clearStepsForward();
 
221
                try {
 
222
 
 
223
                        // Hack to allow usage of localised numbes
260
224
                        DecimalFormat df = new DecimalFormat();
261
225
                        df.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
262
226
                        df.setMinimumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
266
230
                        parser.setMaximumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
267
231
                        parser.setMinimumFractionDigits(Pipe.AGE_DECIMAL_PRECISION);
268
232
 
269
 
                        Number parseTime = parser.parse(TimeDelayField.getText()); // Parse the number localised
 
233
                        Number parseTime = parser.parse(TimeDelayField.getText()); // Parse
 
234
                                                                                                                                                // the
 
235
                                                                                                                                                // number
 
236
                                                                                                                                                // localised
270
237
                        // Try parse
271
238
 
272
 
                        BigDecimal timeDelayToSet  =  new BigDecimal(parseTime.toString(), new MathContext(Pipe.AGE_PRECISION));
273
 
 
274
 
 
275
 
                        //      BigDecimal timeDelayToSet = new BigDecimal(TimeDelayField.getText(), new MathContext(Pipe.AGE_PRECISION));
276
 
                        if (timeDelayToSet.compareTo(new BigDecimal(0l))<=0){
277
 
                                //Nothing to do, illegal value 
 
239
                        BigDecimal timeDelayToSet = new BigDecimal(parseTime.toString(),
 
240
                                        new MathContext(Pipe.AGE_PRECISION));
 
241
 
 
242
                        // BigDecimal timeDelayToSet = new
 
243
                        // BigDecimal(TimeDelayField.getText(), new
 
244
                        // MathContext(Pipe.AGE_PRECISION));
 
245
                        if (timeDelayToSet.compareTo(new BigDecimal(0l)) <= 0) {
 
246
                                // Nothing to do, illegal value
278
247
                                System.err.println("Illegal value");
279
 
                        }else{
280
 
                                CreateGui.getAnimator().letTimePass(timeDelayToSet);                                                     
 
248
                        } else {
 
249
                                CreateGui.getAnimator().letTimePass(timeDelayToSet);
281
250
                        }
282
251
                } catch (NumberFormatException e) {
283
 
                        //Do nothing, invalud number 
284
 
                } catch (InvariantViolatedAnimationException e) {
285
 
                        // TODO Auto-generated catch block
286
 
                        System.err.println("Invariant Violated, TimeDelay Not allowed");
 
252
                        // Do nothing, invalud number
287
253
                } catch (ParseException e) {
288
254
                        // TODO Auto-generated catch block
289
255
                        e.printStackTrace();
290
256
                }
291
257
 
292
 
 
293
258
                setAnimationButtonsEnabled();
294
259
        }
295
260
 
300
265
                 */
301
266
                private static final long serialVersionUID = -4066032248332540289L;
302
267
                private int typeID;
303
 
                private AnimationHistory animBox;
304
 
 
305
 
 
306
 
                AnimateAction(String name, int typeID, String tooltip, String keystroke){
 
268
                private AnimationHistoryComponent animBox;
 
269
 
 
270
                AnimateAction(String name, int typeID, String tooltip, String keystroke) {
307
271
                        super(name, tooltip, keystroke);
308
272
                        this.typeID = typeID;
309
273
                }
310
274
 
311
 
                AnimateAction(String name, int typeID, String tooltip, String keystroke,
312
 
                                boolean toggleable){
 
275
                AnimateAction(String name, int typeID, String tooltip,
 
276
                                String keystroke, boolean toggleable) {
313
277
                        super(name, tooltip, keystroke, toggleable);
314
278
                        this.typeID = typeID;
315
279
                }
316
280
 
317
 
 
318
281
                public AnimateAction(String name, int typeID, String tooltip,
319
282
                                KeyStroke keyStroke) {
320
283
                        super(name, tooltip, keyStroke);
321
284
                        this.typeID = typeID;
322
285
                }
323
286
 
324
 
                public void actionPerformed(ActionEvent ae){
 
287
                public void actionPerformed(ActionEvent ae) {
325
288
 
326
289
                        animBox = CreateGui.getAnimationHistory();
327
290
 
328
 
                        switch(typeID){
 
291
                        switch (typeID) {
329
292
                        case Pipe.TIMEPASS:
330
293
                                animBox.clearStepsForward();
331
 
                                try {
332
 
                                        CreateGui.getAnimator().letTimePass(new BigDecimal(1, new MathContext(Pipe.AGE_PRECISION)));
333
 
                                } catch (InvariantViolatedAnimationException e) {
334
 
                                        // TODO Auto-generated catch block
335
 
                                        e.printStackTrace();
336
 
                                }
337
 
 
338
 
                                setAnimationButtonsEnabled();
339
 
 
340
 
                                break;
341
 
 
342
 
                        case Pipe.RANDOM:
343
 
                                animBox.clearStepsForward();
344
 
                                CreateGui.getAnimator().doRandomFiring();
345
 
 
346
 
                                setAnimationButtonsEnabled();
347
 
                                break;
 
294
                                CreateGui.getAnimator().letTimePass(
 
295
                                                new BigDecimal(1, new MathContext(Pipe.AGE_PRECISION)));
 
296
 
 
297
                                setAnimationButtonsEnabled();
 
298
 
 
299
                                break;
 
300
 
 
301
                        // case Pipe.RANDOM:
 
302
                        // animBox.clearStepsForward();
 
303
                        // CreateGui.getAnimator().doRandomFiring();
 
304
                        //
 
305
                        // setAnimationButtonsEnabled();
 
306
                        // break;
348
307
 
349
308
                        case Pipe.STEPFORWARD:
350
309
                                animBox.stepForward();
358
317
                                setAnimationButtonsEnabled();
359
318
                                break;
360
319
 
361
 
                        case Pipe.ANIMATE:
362
 
                                Animator a = CreateGui.getAnimator();
363
 
                                if (a.getNumberSequences() > 0) {
364
 
                                        a.setNumberSequences(0); // stop animation
365
 
                                        setSelected(false);
366
 
                                } else {
367
 
                                        setAnimationButtonsEnabled();
368
 
                                        randomAction.setEnabled(false);
369
 
                                        setSelected(true);
370
 
                                        animBox.clearStepsForward();
371
 
                                        CreateGui.getAnimator().startRandomFiring();
372
 
                                }
373
 
                                break;
374
 
 
375
320
                        default:
376
321
                                break;
377
322
                        }
383
328
                stepbackwardAction.setEnabled(b);
384
329
 
385
330
        }
 
331
 
386
332
        private void setEnabledStepforwardAction(boolean b) {
387
333
                stepforwardAction.setEnabled(b);
388
334
 
389
335
        }
390
336
 
391
 
        public void setAnimationButtonsEnabled(){
392
 
                AnimationHistory animationHistory = CreateGui.getAnimationHistory();
 
337
        public void setAnimationButtonsEnabled() {
 
338
                AnimationHistoryComponent animationHistory = CreateGui.getAnimationHistory();
393
339
 
394
340
                setEnabledStepforwardAction(animationHistory.isStepForwardAllowed());
395
341
                setEnabledStepbackwardAction(animationHistory.isStepBackAllowed());
396
342
 
397
343
                CreateGui.appGui.setEnabledStepForwardAction(animationHistory.isStepForwardAllowed());
398
344
                CreateGui.appGui.setEnabledStepBackwardAction(animationHistory.isStepBackAllowed());
399
 
 
400
 
                //                 setEnabledStepforwardAction(false);
401
 
                //                 setEnabledStepbackwardAction(false);
402
345
        }
403
346
 
404
347
        JTextField TimeDelayField = new JTextField();