TAPAAL

Merge lp:~yrke/tapaal/fix-1887524-prepostSetSize into lp:tapaal

  1. fix-1887524-prepostSetSize
  2. Merge into trunk
Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1069
Merged at revision: 1071
Proposed branch: lp:~yrke/tapaal/fix-1887524-prepostSetSize
Merge into: lp:tapaal
Diff against target: 309 lines (+36/-33)
10 files modified
src/dk/aau/cs/model/tapn/TimedArcPetriNet.java (+1/-1)
src/dk/aau/cs/model/tapn/TimedPlace.java (+1/-2)
src/dk/aau/cs/model/tapn/TimedTransition.java (+7/-3)
src/dk/aau/cs/translations/Degree2Converter.java (+7/-7)
src/dk/aau/cs/translations/Degree2Pairing.java (+1/-1)
src/dk/aau/cs/translations/tapn/BroadcastTranslation.java (+5/-5)
src/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.java (+7/-7)
src/dk/aau/cs/translations/tapn/OptimizedStandardTranslation.java (+4/-4)
src/dk/aau/cs/translations/tapn/StandardTranslation.java (+2/-2)
src/dk/aau/cs/translations/tapn/TAPNToConservativeTAPNConverter.java (+1/-1)
To merge this branch: bzr merge lp:~yrke/tapaal/fix-1887524-prepostSetSize
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+387513@code.launchpad.net
To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNet.java'
2--- src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-06-22 08:20:47 +0000
3+++ src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-07-16 11:42:18 +0000
4@@ -366,7 +366,7 @@
5
6 public boolean isDegree2(){
7 for(TimedTransition t : this.transitions()) {
8- if(t.presetSize() > 2 || t.postsetSize() > 2)
9+ if(t.presetSizeWithoutInhibitorArcs() > 2 || t.postsetSize() > 2)
10 return false;
11 }
12 return true;
13
14=== modified file 'src/dk/aau/cs/model/tapn/TimedPlace.java'
15--- src/dk/aau/cs/model/tapn/TimedPlace.java 2020-06-22 08:20:47 +0000
16+++ src/dk/aau/cs/model/tapn/TimedPlace.java 2020-07-16 11:42:18 +0000
17@@ -200,11 +200,10 @@
18 }
19
20 public int presetSize() {
21- return preset.size() + transportArcs.size() + inhibitorArcs.size();
22+ return preset.size() + transportArcs.size();
23 }
24
25 public int postsetSize() {
26 return postset.size() + transportArcs.size() + inhibitorArcs.size();
27 }
28-
29 }
30\ No newline at end of file
31
32=== modified file 'src/dk/aau/cs/model/tapn/TimedTransition.java'
33--- src/dk/aau/cs/model/tapn/TimedTransition.java 2020-06-22 08:20:47 +0000
34+++ src/dk/aau/cs/model/tapn/TimedTransition.java 2020-07-16 11:42:18 +0000
35@@ -185,12 +185,16 @@
36 model().remove(this);
37 }
38
39- public int presetSize() {
40- return preset.size() + transportArcsGoingThrough.size() + inhibitorArcs.size();
41+ //XXX: See bug #1887524, old degree-2 converter does not expect inhibitorArcs to count in the size of preset
42+ public int presetSizeWithoutInhibitorArcs() {
43+ return preset.size() + transportArcsGoingThrough.size();
44 }
45+ public int presetSize() {
46+ return preset.size() + transportArcsGoingThrough.size() + inhibitorArcs.size();
47+ }
48
49 public int postsetSize() {
50- return postset.size() + transportArcsGoingThrough.size() + inhibitorArcs.size();
51+ return postset.size() + transportArcsGoingThrough.size();
52 }
53
54 public boolean isDEnabled(){
55
56=== modified file 'src/dk/aau/cs/translations/Degree2Converter.java'
57--- src/dk/aau/cs/translations/Degree2Converter.java 2011-06-28 16:30:37 +0000
58+++ src/dk/aau/cs/translations/Degree2Converter.java 2020-07-16 11:42:18 +0000
59@@ -80,11 +80,11 @@
60
61
62 private boolean isTransitionDegree1(TimedTransition t) {
63- return t.presetSize() == 1 && t.postsetSize() == 1;
64+ return t.presetSizeWithoutInhibitorArcs() == 1 && t.postsetSize() == 1;
65 }
66
67 private boolean isTransitionDegree2(TimedTransition t) {
68- return t.presetSize() == 2 && t.postsetSize() == 2;
69+ return t.presetSizeWithoutInhibitorArcs() == 2 && t.postsetSize() == 2;
70 }
71
72 private void createCopyOfOriginalTransition(TimedTransition transition, Pairing pairing) {
73@@ -111,7 +111,7 @@
74
75 private void createRingStructure(TimedTransition transition, Pairing p) {
76 String transitionName = transition.name();
77- int transitionsToCreate = 2 * transition.presetSize() - 1;
78+ int transitionsToCreate = 2 * transition.presetSizeWithoutInhibitorArcs() - 1;
79 TimedPlace previousPlace = null;
80
81 // create t^i_in (with corresponding places)
82@@ -173,7 +173,7 @@
83 int numPresetArcs = 1;
84 String transitionName = transition.name();
85 for(TimedInputArc inputArc : transition.getInputArcs()) {
86- if (numPresetArcs == transition.presetSize()) {
87+ if (numPresetArcs == transition.presetSizeWithoutInhibitorArcs()) {
88 TimedTransition tmax = degree2Model.getTransitionByName(String.format(T_MAX_FORMAT, transitionName, numPresetArcs));
89 degree2Model.add(new TimedInputArc(degree2Model.getPlaceByName(inputArc.source().name()), tmax, inputArc.interval().copy()));
90 degree2Model.add(new TimedOutputArc(tmax, degree2Model.getPlaceByName(pairing.getOutputArcFor(inputArc).destination().name())));
91@@ -196,7 +196,7 @@
92 }
93
94 for(TransportArc transArc : transition.getTransportArcsGoingThrough()) {
95- if (numPresetArcs == transition.presetSize()) {
96+ if (numPresetArcs == transition.presetSizeWithoutInhibitorArcs()) {
97 degree2Model.add(new TransportArc(degree2Model.getPlaceByName(transArc.source().name()),
98 degree2Model.getTransitionByName(String.format(T_MAX_FORMAT, transitionName, numPresetArcs)),
99 degree2Model.getPlaceByName(transArc.destination().name()),
100@@ -217,11 +217,11 @@
101 }
102
103 private void createInhibitorArcs(TimedTransition t) {
104- if(t.presetSize() == 0)
105+ if(t.presetSizeWithoutInhibitorArcs() == 0)
106 return;
107
108 for(TimedInhibitorArc inhibArc : t.getInhibitorArcs()) {
109- if(t.presetSize() == 1) {
110+ if(t.presetSizeWithoutInhibitorArcs() == 1) {
111 degree2Model.add(new TimedInhibitorArc(degree2Model.getPlaceByName(inhibArc.source().name()),
112 degree2Model.getTransitionByName(String.format(T_MAX_FORMAT, t.name(), 1)),
113 inhibArc.interval().copy()));
114
115=== modified file 'src/dk/aau/cs/translations/Degree2Pairing.java'
116--- src/dk/aau/cs/translations/Degree2Pairing.java 2013-10-22 08:41:03 +0000
117+++ src/dk/aau/cs/translations/Degree2Pairing.java 2020-07-16 11:42:18 +0000
118@@ -28,7 +28,7 @@
119 Require.that(presetSize == postsetSize, "The provided model is not conservative");
120 Require.that(presetSize <= 2, "The provided model is more than degree 2");
121
122- if(getTransition().presetSize() == 0)
123+ if(getTransition().presetSizeWithoutInhibitorArcs() == 0)
124 return;
125 else if(getTransition().getInputArcs().size() == 1)
126 add(getTransition().getInputArcs().get(0), getTransition().getOutputArcs().get(0));
127
128=== modified file 'src/dk/aau/cs/translations/tapn/BroadcastTranslation.java'
129--- src/dk/aau/cs/translations/tapn/BroadcastTranslation.java 2020-04-18 16:08:44 +0000
130+++ src/dk/aau/cs/translations/tapn/BroadcastTranslation.java 2020-07-16 11:42:18 +0000
131@@ -188,7 +188,7 @@
132 }
133
134 for (TimedTransition t : model.transitions()) {
135- if(t.presetSize() == 0 && !t.hasInhibitorArcs()) {
136+ if(t.presetSizeWithoutInhibitorArcs() == 0 && !t.hasInhibitorArcs()) {
137 continue;
138 } else if (isTransitionDegree1(t) && !t.hasInhibitorArcs()) {
139 builder.append("broadcast chan ");
140@@ -221,11 +221,11 @@
141 }
142
143 private boolean isTransitionDegree1(TimedTransition t) {
144- return t.presetSize() == 1 && t.postsetSize() == 1;
145+ return t.presetSizeWithoutInhibitorArcs() == 1 && t.postsetSize() == 1;
146 }
147
148 private boolean isTransitionDegree2(TimedTransition t) {
149- return t.presetSize() == 2 && t.postsetSize() == 2;
150+ return t.presetSizeWithoutInhibitorArcs() == 2 && t.postsetSize() == 2;
151 }
152
153 private TimedAutomaton createControlTemplate(TimedArcPetriNet model) {
154@@ -256,7 +256,7 @@
155 protected void createTransitionSimulations(TimedAutomaton control, Location lock, TimedArcPetriNet model) {
156
157 for (TimedTransition transition : model.transitions()) {
158- if(transition.presetSize() == 0 && !transition.hasInhibitorArcs())
159+ if(transition.presetSizeWithoutInhibitorArcs() == 0 && !transition.hasInhibitorArcs())
160 continue;
161
162 if (!(isTransitionDegree1(transition) || isTransitionDegree2(transition)) || transition.hasInhibitorArcs()) {
163@@ -430,7 +430,7 @@
164 ta.setLocations(CreateLocationsFromModel(model));
165
166 for (TimedTransition t : model.transitions()) {
167- int presetSize = t.presetSize() + t.getInhibitorArcs().size();
168+ int presetSize = t.presetSizeWithoutInhibitorArcs() + t.getInhibitorArcs().size();
169
170 if(presetSize == 0)
171 continue;
172
173=== modified file 'src/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.java'
174--- src/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.java 2020-04-18 16:08:44 +0000
175+++ src/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.java 2020-07-16 11:42:18 +0000
176@@ -196,7 +196,7 @@
177 }
178
179 for (TimedTransition t : degree2Net.transitions()) {
180- if(t.presetSize() == 0 && !t.hasInhibitorArcs()) {
181+ if(t.presetSizeWithoutInhibitorArcs() == 0 && !t.hasInhibitorArcs()) {
182 continue;
183 }
184 else if (isTransitionDegree1(t)) {
185@@ -216,7 +216,7 @@
186 }
187
188 for (TimedTransition t : originalModel.transitions()) {
189- if((t.presetSize() == 0 || isTransitionDegree1(t)) && !t.hasInhibitorArcs()) {
190+ if((t.presetSizeWithoutInhibitorArcs() == 0 || isTransitionDegree1(t)) && !t.hasInhibitorArcs()) {
191 continue;
192 }
193 else if (!isTransitionDegree2(t) || t.hasInhibitorArcs()) {
194@@ -240,11 +240,11 @@
195 }
196
197 private boolean isTransitionDegree1(TimedTransition t) {
198- return t.presetSize() == 1 && t.postsetSize() == 1;
199+ return t.presetSizeWithoutInhibitorArcs() == 1 && t.postsetSize() == 1;
200 }
201
202 private boolean isTransitionDegree2(TimedTransition t) {
203- return t.presetSize() == 2 && t.postsetSize() == 2;
204+ return t.presetSizeWithoutInhibitorArcs() == 2 && t.postsetSize() == 2;
205 }
206
207 protected String convertInvariant(TimedPlace place) {
208@@ -339,7 +339,7 @@
209 Edge first = new Edge(getLocationByName(PLOCK), ptest, "", String.format(TEST_CHANNEL, transition.name(), "!"), "");
210 control.addTransition(first);
211
212- if (transition.presetSize() != 1) {
213+ if (transition.presetSizeWithoutInhibitorArcs() != 1) {
214 Edge second = new Edge(ptest, getLocationByName(String.format(P_T_IN_FORMAT, transition.name(), 1)),
215 "", String.format(T_I_IN_FORMAT + "%3$s", transition.name(), 1, "!"),
216 createResetExpressionForControl(transition));
217@@ -399,7 +399,7 @@
218
219 private void createEdgesForTokenAutomata(TimedArcPetriNet degree2Net, TimedAutomaton token) {
220 for (TimedTransition transition : degree2Net.transitions()) {
221- if(transition.presetSize() == 0 && !transition.hasInhibitorArcs())
222+ if(transition.presetSizeWithoutInhibitorArcs() == 0 && !transition.hasInhibitorArcs())
223 continue;
224
225 Degree2Pairing pairing = new Degree2Pairing(transition);
226@@ -496,7 +496,7 @@
227 private void createTestingEdgesForTokenAutomata(TimedArcPetriNet originalModel, TimedAutomaton ta) throws Exception {
228
229 for (TimedTransition transition : originalModel.transitions()) {
230- int size = transition.presetSize() + transition.getInhibitorArcs().size();
231+ int size = transition.presetSizeWithoutInhibitorArcs() + transition.getInhibitorArcs().size();
232 if (size > largestPresetSize)
233 largestPresetSize = size;
234
235
236=== modified file 'src/dk/aau/cs/translations/tapn/OptimizedStandardTranslation.java'
237--- src/dk/aau/cs/translations/tapn/OptimizedStandardTranslation.java 2020-04-18 16:08:44 +0000
238+++ src/dk/aau/cs/translations/tapn/OptimizedStandardTranslation.java 2020-07-16 11:42:18 +0000
239@@ -184,7 +184,7 @@
240 }
241
242 for (TimedTransition t : degree2Model.transitions()) {
243- if(t.presetSize() == 0) {
244+ if(t.presetSizeWithoutInhibitorArcs() == 0) {
245 continue;
246 }
247 else if (isTransitionDegree1(t)) {
248@@ -299,7 +299,7 @@
249 if(transition.hasInhibitorArcs())
250 throw new RuntimeException("Standard translation does not support inhibitor arcs!");
251
252- if(transition.presetSize() == 0)
253+ if(transition.presetSizeWithoutInhibitorArcs() == 0)
254 continue;
255
256 Degree2Pairing pairing = new Degree2Pairing(transition);
257@@ -351,7 +351,7 @@
258 }
259
260 private boolean isTransitionDegree1(TimedTransition transition) {
261- return transition.presetSize() == 1 && transition.postsetSize() == 1;
262+ return transition.presetSizeWithoutInhibitorArcs() == 1 && transition.postsetSize() == 1;
263 }
264
265 private String createTransitionGuardWithLock(TimeInterval interval) {
266@@ -504,7 +504,7 @@
267 return false;
268
269 for(TimedTransition t : model.transitions()) {
270- if(t.presetSize() > 2 || t.postsetSize() > 2)
271+ if(t.presetSizeWithoutInhibitorArcs() > 2 || t.postsetSize() > 2)
272 return false;
273 }
274
275
276=== modified file 'src/dk/aau/cs/translations/tapn/StandardTranslation.java'
277--- src/dk/aau/cs/translations/tapn/StandardTranslation.java 2020-04-18 16:08:44 +0000
278+++ src/dk/aau/cs/translations/tapn/StandardTranslation.java 2020-07-16 11:42:18 +0000
279@@ -181,7 +181,7 @@
280 }
281
282 for (TimedTransition t : degree2Model.transitions()) {
283- if(t.presetSize() == 0) {
284+ if(t.presetSizeWithoutInhibitorArcs() == 0) {
285 continue;
286 }
287
288@@ -279,7 +279,7 @@
289
290 private void createEdgesForTokenAutomata(TimedArcPetriNet degree2Model, TimedAutomaton tokenTA) {
291 for(TimedTransition transition : degree2Model.transitions()) {
292- if(transition.presetSize() == 0)
293+ if(transition.presetSizeWithoutInhibitorArcs() == 0)
294 continue;
295
296 Degree2Pairing pairing = new Degree2Pairing(transition);
297
298=== modified file 'src/dk/aau/cs/translations/tapn/TAPNToConservativeTAPNConverter.java'
299--- src/dk/aau/cs/translations/tapn/TAPNToConservativeTAPNConverter.java 2011-06-28 16:30:37 +0000
300+++ src/dk/aau/cs/translations/tapn/TAPNToConservativeTAPNConverter.java 2020-07-16 11:42:18 +0000
301@@ -23,7 +23,7 @@
302
303
304 for (TimedTransition t : conservativeModel.transitions()) {
305- int difference = t.postsetSize() - t.presetSize();
306+ int difference = t.postsetSize() - t.presetSizeWithoutInhibitorArcs();
307
308 if (difference < 0) {
309 for(int i = 0; i < Math.abs(difference); i++) {

Subscribers

People subscribed via source and target branches