← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/Pipe.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/Pipe.java
1
1
package pipe.gui;
 
2
 
2
3
import java.awt.Color;
3
4
 
4
5
public class Pipe {
10
11
           return "" + Pipe.TOOL + " " + Pipe.VERSION;
11
12
   }
12
13
   
13
 
   // Define the drawingmode 
14
14
        public enum drawmodes {
15
 
            PETRINET, TIMEDPETRINET, TIMEDARCPETRINET
 
15
                PETRINET, TIMEDPETRINET, TIMEDARCPETRINET
16
16
        }
17
 
        
 
17
 
18
18
        // For TAPAAL we hardcode the drawingmode
19
19
        public static drawmodes drawingmode = Pipe.drawmodes.TIMEDARCPETRINET;
20
 
        
21
 
   
22
 
   
23
 
//  Filesystem Definitions
24
 
   public static final String PROPERTY_FILE_EXTENSION = ".properties";
25
 
   public static final String PROPERTY_FILE_DESC = "PIPE Properties file";
26
 
   public static final String CLASS_FILE_EXTENSION = ".class";
27
 
   public static final String CLASS_FILE_DESC = "Java Class File";   
28
 
//      File DEFAULT_DIRECTORY = new File("Petri-Nets");
29
 
//      String DEFAULT_FILENAME = "PetriNet.xml";
30
 
   
31
 
//PetriNet Object Type Definitions
32
 
   public static final int ANIMATE      = 98;
33
 
   public static final int RANDOM       = 99;
34
 
   public static final int START        = 100;
35
 
   public static final int FIRE         = 101;
36
 
   public static final int STEPFORWARD  = 102;
37
 
   public static final int STEPBACKWARD = 103;
38
 
   public static final int STOP         = 104;
39
 
   
40
 
   public static final int PLACE        = 105;
41
 
   
42
 
   public static final int IMMTRANS     = 106;
43
 
   public static final int TIMEDTRANS   = 114;
44
 
   public static final int ADDTOKEN     = 107;
45
 
   public static final int DELTOKEN     = 108;
46
 
   public static final int ANNOTATION   = 109;
47
 
   public static final int SELECT       = 110;
48
 
   public static final int DELETE       = 111;
49
 
   public static final int ARC          = 112;
50
 
   public static final int GRID         = 113;
51
 
   public static final int INHIBARC     = 116;
52
 
   
53
 
   
54
 
   
55
 
   
56
 
   // Values for Timed-Arc Petri Nets
57
 
   public static final int TAPNPLACE   = 700; 
58
 
   public static final int TAPNTRANS = 701;
59
 
   
60
 
   public static final int TAPNARC      = 702;
61
 
   public static final int TRANSPORTARC = 703; 
62
 
   
63
 
   public static final int FAST_TAPNPLACE      = 705;
64
 
   public static final int FAST_TAPNTRANSITION = 706;
65
 
   public static final int TAPNINHIBITOR_ARC = 707; 
66
 
   
67
 
   
68
 
   // Other
69
 
   public static final int DRAW         = 115;
70
 
   
71
 
   public static final int DRAG         = 120;
72
 
   
73
 
   
74
 
   public static final int FAST_PLACE      = 150;
75
 
   public static final int FAST_TRANSITION = 151;
76
 
            
77
 
   // Special:  Parsing in a PNML file - creating components
78
 
   public static final int CREATING     = 200;   
79
 
   
80
 
   public static final int DEFAULT_ELEMENT_TYPE = SELECT;
81
 
   
82
 
   public static final int PLACE_TRANSITION_HEIGHT=30;
83
 
   
84
 
   public static final Color ENABLED_TRANSITION_COLOUR = new Color(192,0,0);
85
 
   public static final Color ELEMENT_LINE_COLOUR = Color.BLACK;
86
 
   public static final Color ELEMENT_FILL_COLOUR = Color.WHITE;
87
 
   public static final Color SELECTION_LINE_COLOUR = new Color(0,0,192);
88
 
   public static final Color SELECTION_FILL_COLOUR = new Color(192,192,255);
89
 
   
90
 
   // For ArcPath:
91
 
   public static final int ARC_CONTROL_POINT_CONSTANT = 3;
92
 
   public static final int ARC_PATH_SELECTION_WIDTH = 6;
93
 
   public static final int ARC_PATH_PROXIMITY_WIDTH = 10;
94
 
   
95
 
   // For Place/Transition Arc Snap-To behaviour:
96
 
   public static final int PLACE_TRANSITION_PROXIMITY_RADIUS = 25;
97
 
   
98
 
   // Object layer positions for GuiView:
99
 
   public static final int WHITE_LAYER_OFFSET = 80;
100
 
   public static final int ARC_POINT_LAYER_OFFSET = 50;
101
 
   public static final int ARC_LAYER_OFFSET = 20;
102
 
   public static final int PLACE_TRANSITION_LAYER_OFFSET = 30;
103
 
   public static final int NOTE_LAYER_OFFSET = 10;
104
 
   public static final int SELECTION_LAYER_OFFSET = 90;
105
 
   public static final int LOWEST_LAYER_OFFSET = 0;
106
 
   
107
 
   // For AnnotationNote appearance:
108
 
   public static final int RESERVED_BORDER = 12;
109
 
   public static final int ANNOTATION_SIZE_OFFSET = 4;
110
 
   public static final int ANNOTATION_MIN_WIDTH = 40;
111
 
   public static final Color NOTE_DISABLED_COLOUR = Color.BLACK;
112
 
   public static final Color NOTE_EDITING_COLOUR = Color.BLACK;
113
 
   public static final Color RESIZE_POINT_DOWN_COLOUR = new Color(220,220,255);
114
 
   public static final String ANNOTATION_DEFAULT_FONT = "Helvetica";
115
 
   public static final int ANNOTATION_DEFAULT_FONT_SIZE = 12;
116
 
   
117
 
   
118
 
   public static final String LABEL_FONT = "Dialog";
119
 
   public static final int    LABEL_DEFAULT_FONT_SIZE = 10;
120
 
   
121
 
   
122
 
   public static final int DEFAULT_OFFSET_X = -5;
123
 
   public static final int DEFAULT_OFFSET_Y = 35;
124
 
   
125
 
   public static final int NAMELABEL_OFFSET = 12;
126
 
 
127
 
   public static int DEFAULT_BUFFER_CAPACITY = 50;
128
 
   
129
 
   public static boolean JOIN_ARCS = false;
130
 
 
131
 
   public static final int ZOOM_DELTA   = 10;
132
 
   public static final int ZOOM_MAX     = 300;
133
 
   public static final int ZOOM_MIN     = 40;
134
 
   public static final int ZOOM_DEFAULT = 100;
135
 
 
136
 
   public static Color BACKGROUND_COLOR = new Color(255, 255, 255, 200);
137
 
   public static Color ANIMATION_BACKGROUND_COLOR = new Color(246,250,255);
138
 
 
139
 
   public static final int MAX_NODES = 20000; //it was 10000 previously
140
 
   // TODO: find a better value for MAX_NODES
141
 
   
142
 
   public static final int TIMEPASS = 700;
143
 
 
144
 
 
145
 
   public static final int verifytaMinRev=4543;//4409;
146
 
   public static final int AGE_DECIMAL_PRECISION = 5;
147
 
   public static final int AGE_PRECISION = AGE_DECIMAL_PRECISION+4;
148
 
   
149
 
   //public static final int NUMBER_OF_BUTTONS = MouseInfo.getNumberOfButtons();
150
 
   
151
 
   
 
20
 
 
21
        // Filesystem Definitions
 
22
        public static final String PROPERTY_FILE_EXTENSION = ".properties";
 
23
        public static final String PROPERTY_FILE_DESC = "PIPE Properties file";
 
24
        public static final String CLASS_FILE_EXTENSION = ".class";
 
25
        public static final String CLASS_FILE_DESC = "Java Class File";
 
26
        // File DEFAULT_DIRECTORY = new File("Petri-Nets");
 
27
        // String DEFAULT_FILENAME = "PetriNet.xml";
 
28
 
 
29
        // PetriNet Object Type Definitions
 
30
        public static final int ANIMATE = 98;
 
31
        public static final int RANDOM = 99;
 
32
        public static final int START = 100;
 
33
        public static final int FIRE = 101;
 
34
        public static final int STEPFORWARD = 102;
 
35
        public static final int STEPBACKWARD = 103;
 
36
        public static final int STOP = 104;
 
37
 
 
38
        public static final int PLACE = 105;
 
39
 
 
40
        public static final int IMMTRANS = 106;
 
41
        public static final int TIMEDTRANS = 114;
 
42
        public static final int ADDTOKEN = 107;
 
43
        public static final int DELTOKEN = 108;
 
44
        public static final int ANNOTATION = 109;
 
45
        public static final int SELECT = 110;
 
46
        public static final int DELETE = 111;
 
47
        public static final int ARC = 112;
 
48
        public static final int GRID = 113;
 
49
        public static final int INHIBARC = 116;
 
50
 
 
51
        // Values for Timed-Arc Petri Nets
 
52
        public static final int TAPNPLACE = 700;
 
53
        public static final int TAPNTRANS = 701;
 
54
 
 
55
        public static final int TAPNARC = 702;
 
56
        public static final int TRANSPORTARC = 703;
 
57
 
 
58
        public static final int FAST_TAPNPLACE = 705;
 
59
        public static final int FAST_TAPNTRANSITION = 706;
 
60
        public static final int TAPNINHIBITOR_ARC = 707;
 
61
 
 
62
        // Other
 
63
        public static final int DRAW = 115;
 
64
 
 
65
        public static final int DRAG = 120;
 
66
 
 
67
        public static final int FAST_PLACE = 150;
 
68
        public static final int FAST_TRANSITION = 151;
 
69
 
 
70
        // Special: Parsing in a PNML file - creating components
 
71
        public static final int CREATING = 200;
 
72
 
 
73
        public static final int DEFAULT_ELEMENT_TYPE = SELECT;
 
74
 
 
75
        public static final int PLACE_TRANSITION_HEIGHT = 30;
 
76
        public static final int DASHED_PADDING = 8;
 
77
 
 
78
        public static final Color ENABLED_TRANSITION_COLOUR = new Color(192, 0, 0);
 
79
        public static final Color ELEMENT_LINE_COLOUR = Color.BLACK;
 
80
        public static final Color ELEMENT_FILL_COLOUR = Color.WHITE;
 
81
        public static final Color SELECTION_LINE_COLOUR = new Color(0, 0, 192);
 
82
        public static final Color SELECTION_FILL_COLOUR = new Color(192, 192, 255);
 
83
        public static final Color SELECTION_TEXT_COLOUR = SELECTION_LINE_COLOUR;
 
84
        public static final Color ELEMENT_TEXT_COLOUR = ELEMENT_LINE_COLOUR;
 
85
 
 
86
        // For ArcPath:
 
87
        public static final int ARC_CONTROL_POINT_CONSTANT = 3;
 
88
        public static final int ARC_PATH_SELECTION_WIDTH = 6;
 
89
        public static final int ARC_PATH_PROXIMITY_WIDTH = 10;
 
90
 
 
91
        // For Place/Transition Arc Snap-To behaviour:
 
92
        public static final int PLACE_TRANSITION_PROXIMITY_RADIUS = 25;
 
93
 
 
94
        // Object layer positions for GuiView:
 
95
        public static final int WHITE_LAYER_OFFSET = 80;
 
96
        public static final int ARC_POINT_LAYER_OFFSET = 50;
 
97
        public static final int ARC_LAYER_OFFSET = 20;
 
98
        public static final int PLACE_TRANSITION_LAYER_OFFSET = 30;
 
99
        public static final int NOTE_LAYER_OFFSET = 10;
 
100
        public static final int SELECTION_LAYER_OFFSET = 90;
 
101
        public static final int LOWEST_LAYER_OFFSET = 0;
 
102
 
 
103
        // For AnnotationNote appearance:
 
104
        public static final int RESERVED_BORDER = 12;
 
105
        public static final int ANNOTATION_SIZE_OFFSET = 4;
 
106
        public static final int ANNOTATION_MIN_WIDTH = 40;
 
107
        public static final Color NOTE_DISABLED_COLOUR = Color.BLACK;
 
108
        public static final Color NOTE_EDITING_COLOUR = Color.BLACK;
 
109
        public static final Color RESIZE_POINT_DOWN_COLOUR = new Color(220, 220,
 
110
                        255);
 
111
        public static final String ANNOTATION_DEFAULT_FONT = "Helvetica";
 
112
        public static final int ANNOTATION_DEFAULT_FONT_SIZE = 12;
 
113
 
 
114
        public static final String LABEL_FONT = "Dialog";
 
115
        public static final int LABEL_DEFAULT_FONT_SIZE = 10;
 
116
 
 
117
        public static final int DEFAULT_OFFSET_X = -5;
 
118
        public static final int DEFAULT_OFFSET_Y = 35;
 
119
 
 
120
        public static final int NAMELABEL_OFFSET = 12;
 
121
 
 
122
        public static int DEFAULT_BUFFER_CAPACITY = 50;
 
123
 
 
124
        public static boolean JOIN_ARCS = false;
 
125
 
 
126
        public static final int ZOOM_DELTA = 10;
 
127
        public static final int ZOOM_MAX = 300;
 
128
        public static final int ZOOM_MIN = 40;
 
129
        public static final int ZOOM_DEFAULT = 100;
 
130
 
 
131
        public static Color BACKGROUND_COLOR = new Color(255, 255, 255, 200);
 
132
        public static Color ANIMATION_BACKGROUND_COLOR = new Color(246, 250, 255);
 
133
 
 
134
        public static final int MAX_NODES = 20000; // it was 10000 previously
 
135
        // TODO: find a better value for MAX_NODES
 
136
 
 
137
        public static final int TIMEPASS = 700;
 
138
 
 
139
        public static final int verifytaMinRev = 4543;// 4409;
 
140
        public static final int AGE_DECIMAL_PRECISION = 5;
 
141
        public static final int AGE_PRECISION = AGE_DECIMAL_PRECISION + 4;
 
142
 
 
143
        // public static final int NUMBER_OF_BUTTONS =
 
144
        // MouseInfo.getNumberOfButtons();
 
145
 
152
146
}