← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.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/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.java
1
1
package dk.aau.cs.translations.tapn;
2
2
 
3
3
import java.util.ArrayList;
4
 
import java.util.HashSet;
5
4
import java.util.Hashtable;
6
5
import java.util.List;
7
6
import java.util.regex.Matcher;
8
7
import java.util.regex.Pattern;
9
8
 
10
 
import dk.aau.cs.TA.Edge;
11
 
import dk.aau.cs.TA.Location;
12
 
import dk.aau.cs.TA.NTA;
13
 
import dk.aau.cs.TA.StandardUPPAALQuery;
14
 
import dk.aau.cs.TA.TimedAutomaton;
15
 
import dk.aau.cs.TA.UPPAALQuery;
16
9
import dk.aau.cs.TCTL.visitors.BroadcastTranslationQueryVisitor;
17
 
import dk.aau.cs.petrinet.Arc;
18
 
import dk.aau.cs.petrinet.Degree2Converter;
19
 
import dk.aau.cs.petrinet.PetriNetUtil;
20
 
import dk.aau.cs.petrinet.TAPN;
21
 
import dk.aau.cs.petrinet.TAPNArc;
22
 
import dk.aau.cs.petrinet.TAPNInhibitorArc;
23
 
import dk.aau.cs.petrinet.TAPNPlace;
24
 
import dk.aau.cs.petrinet.TAPNQuery;
25
 
import dk.aau.cs.petrinet.TAPNTransition;
26
 
import dk.aau.cs.petrinet.TAPNTransportArc;
27
 
import dk.aau.cs.petrinet.TimedArcPetriNet;
28
 
import dk.aau.cs.petrinet.Token;
29
 
import dk.aau.cs.petrinet.degree2converters.InhibDegree2Converter;
 
10
import dk.aau.cs.model.NTA.Edge;
 
11
import dk.aau.cs.model.NTA.Location;
 
12
import dk.aau.cs.model.NTA.NTA;
 
13
import dk.aau.cs.model.NTA.StandardUPPAALQuery;
 
14
import dk.aau.cs.model.NTA.TimedAutomaton;
 
15
import dk.aau.cs.model.NTA.UPPAALQuery;
 
16
import dk.aau.cs.model.tapn.Bound;
 
17
import dk.aau.cs.model.tapn.TAPNQuery;
 
18
import dk.aau.cs.model.tapn.TimeInterval;
 
19
import dk.aau.cs.model.tapn.TimeInvariant;
 
20
import dk.aau.cs.model.tapn.TimedArcPetriNet;
 
21
import dk.aau.cs.model.tapn.TimedInhibitorArc;
 
22
import dk.aau.cs.model.tapn.TimedInputArc;
 
23
import dk.aau.cs.model.tapn.TimedOutputArc;
 
24
import dk.aau.cs.model.tapn.TimedPlace;
 
25
import dk.aau.cs.model.tapn.TimedToken;
 
26
import dk.aau.cs.model.tapn.TimedTransition;
 
27
import dk.aau.cs.model.tapn.TransportArc;
 
28
import dk.aau.cs.translations.Degree2Converter;
 
29
import dk.aau.cs.translations.Degree2Pairing;
30
30
import dk.aau.cs.translations.ModelTranslator;
31
 
import dk.aau.cs.translations.Pairing;
32
 
import dk.aau.cs.translations.QueryTranslator;
33
31
import dk.aau.cs.translations.TranslationNamingScheme;
34
 
import dk.aau.cs.translations.Pairing.ArcType;
35
32
import dk.aau.cs.translations.TranslationNamingScheme.TransitionTranslation.SequenceInfo;
 
33
import dk.aau.cs.util.Tuple;
36
34
 
 
35
//TODO: Simplify the code by making it output the same NTA for both symmetry and no symmetry, 
 
36
//with the only difference being in the global declarations:
 
37
//symmetry: typedef scalar[N] id_t;
 
38
//no symmetry: typedef int[1,N] id_t;
 
39
//See e.g. OptimizedStandardTranslation for how its done
37
40
public class Degree2BroadcastTranslation implements
38
 
ModelTranslator<TimedArcPetriNet, NTA>,
39
 
QueryTranslator<TAPNQuery, UPPAALQuery>{
 
41
                ModelTranslator<TimedArcPetriNet, TAPNQuery, NTA, UPPAALQuery> {
40
42
 
41
43
        private static final String DEG2_SUFFIX = "_deg2";
42
44
        private static final String DEG1_SUFFIX = "_single";
43
 
        protected static final String QUERY_PATTERN = "([a-zA-Z][a-zA-Z0-9_]*) (==|<|<=|>=|>) ([0-9])*";
44
45
        private static final String PLOCK = "P_lock";
45
 
        private static final String P_CAPACITY = "P_capacity";
 
46
        protected static final String P_CAPACITY = "_BOTTOM_";
46
47
        private static final String TOKEN_TEMPLATE_NAME = "Token";
47
48
        private static final String CONTROL_TEMPLATE_NAME = "Control";
48
49
        private static final String ID_TYPE = "id_t";
58
59
        protected static final String LOCK_BOOL = "lock";
59
60
 
60
61
        private Hashtable<String, Location> namesToLocations = new Hashtable<String, Location>();
61
 
        private Hashtable<Arc, String> arcsToCounters = new Hashtable<Arc, String>();
62
 
        private Hashtable<String, Hashtable<String, String>> arcGuards = new Hashtable<String, Hashtable<String,String>>();
 
62
        private Hashtable<TimedInputArc, String> inputArcsToCounters = new Hashtable<TimedInputArc, String>();
 
63
        private Hashtable<TimedInhibitorArc, String> inhibitorArcsToCounters = new Hashtable<TimedInhibitorArc, String>();
 
64
        private Hashtable<TransportArc, String> transportArcsToCounters = new Hashtable<TransportArc, String>();
 
65
        private Hashtable<String, Hashtable<String, String>> arcGuards = new Hashtable<String, Hashtable<String, String>>();
 
66
        
 
67
        private List<TimedTransition> retainedTransitions;
 
68
        
63
69
        private int numberOfInitChannels = 0;
64
70
        protected int extraTokens = 0;
65
71
        private int largestPresetSize = 0;
66
72
        protected boolean useSymmetry;
67
73
 
68
 
        public Degree2BroadcastTranslation(int extraTokens, boolean useSymmetry) {
69
 
                this.extraTokens = extraTokens;
 
74
        public Degree2BroadcastTranslation(boolean useSymmetry) {
70
75
                this.useSymmetry = useSymmetry;
71
76
        }
 
77
        
 
78
        public Tuple<NTA, UPPAALQuery> translate(TimedArcPetriNet model, TAPNQuery query) throws Exception {
 
79
                extraTokens = query.getExtraTokens();
 
80
                NTA nta = transformModel(model);
 
81
                UPPAALQuery uppaalQuery = transformQuery(query, model);
 
82
                
 
83
                return new Tuple<NTA, UPPAALQuery>(nta, uppaalQuery);
 
84
        }
72
85
 
73
 
        public NTA transformModel(TimedArcPetriNet model) throws Exception {
74
 
                arcsToCounters.clear();
 
86
        protected NTA transformModel(TimedArcPetriNet model) throws Exception {
 
87
                clearArcMappings();
75
88
                arcGuards.clear();
76
89
                clearLocationMappings();
77
90
                numberOfInitChannels = 0;
78
91
                largestPresetSize = 0;
79
92
 
80
 
                TimedArcPetriNet degree2Net = getDegree2Converter().transform((TAPN)model);
 
93
                TimedArcPetriNet conservativeModel = null;
 
94
                TimedArcPetriNet degree2Model = null;
 
95
                try {
 
96
                        TAPNToConservativeTAPNConverter conservativeConverter = new TAPNToConservativeTAPNConverter();
 
97
                        conservativeModel = conservativeConverter.makeConservative(model);
 
98
                        
 
99
                        Degree2Converter converter = new Degree2Converter();
 
100
                        degree2Model = converter.transformModel(conservativeModel);
 
101
                        retainedTransitions = converter.getRetainedTransitions();
 
102
                } catch (Exception e) {
 
103
                        return null;
 
104
                }
81
105
 
82
106
                NTA nta = new NTA();
83
 
                if(useSymmetry || model.getNumberOfTokens()+extraTokens == 0){
84
 
                        TimedAutomaton ta = createTokenAutomaton(degree2Net, model, null);
85
 
                        createInitializationTransitionsForTokenAutomata(degree2Net, ta);
 
107
                if (useSymmetry || degree2Model.marking().size() + extraTokens == 0) {
 
108
                        TimedAutomaton ta = createTokenAutomaton(degree2Model, conservativeModel, null);
 
109
                        createInitializationTransitionsForTokenAutomata(degree2Model, ta);
86
110
                        ta.setName(TOKEN_TEMPLATE_NAME);
87
111
                        ta.setInitLocation(getLocationByName(P_CAPACITY));
88
 
                        if(useSymmetry) ta.setParameters("const " + ID_TYPE + " " + ID_PARAMETER_NAME);
 
112
                        if (useSymmetry)
 
113
                                ta.setParameters("const " + ID_TYPE + " " + ID_PARAMETER_NAME);
89
114
                        nta.addTimedAutomaton(ta);
90
 
                }else{
 
115
                } else {
91
116
                        int j = 0;
92
 
                        for(Token token : degree2Net.getTokens()){
93
 
                                if(!token.place().getName().equals(PLOCK)){
94
 
                                        clearLocationMappings();
95
 
                                        arcsToCounters.clear();
96
 
                                        TimedAutomaton ta = createTokenAutomaton(degree2Net, model, token);
97
 
                                        ta.setName(TOKEN_TEMPLATE_NAME + j);
98
 
                                        ta.setInitLocation(getLocationByName(token.place().getName()));
99
 
                                        nta.addTimedAutomaton(ta);
100
 
                                        j++;
 
117
                        for(TimedPlace p : degree2Model.places()) {
 
118
                                for (TimedToken token : degree2Model.marking().getTokensFor(p)) {
 
119
                                        if (!token.place().name().equals(PLOCK)) {
 
120
                                                clearLocationMappings();
 
121
                                                clearArcMappings();
 
122
                                                TimedAutomaton ta = createTokenAutomaton(degree2Model, conservativeModel, token);
 
123
                                                ta.setName(TOKEN_TEMPLATE_NAME + j);
 
124
                                                ta.setInitLocation(getLocationByName(token.place().name()));
 
125
                                                nta.addTimedAutomaton(ta);
 
126
                                                j++;
 
127
                                        }
101
128
                                }
102
129
                        }
103
130
 
104
 
                        for(int i = 0; i < extraTokens; i++){
 
131
                        TimedPlace bottom = degree2Model.getPlaceByName(P_CAPACITY);
 
132
                        for (int i = 0; i < extraTokens; i++) {
105
133
                                clearLocationMappings();
106
 
                                arcsToCounters.clear();
107
 
                                TimedAutomaton tokenTemplate = createTokenAutomaton(degree2Net, model, new Token(degree2Net.getPlaceByName(P_CAPACITY)));
 
134
                                clearArcMappings();
 
135
                                TimedAutomaton tokenTemplate = createTokenAutomaton(degree2Model, conservativeModel, new TimedToken(bottom));
108
136
                                tokenTemplate.setInitLocation(getLocationByName(P_CAPACITY));
109
137
                                nta.addTimedAutomaton(tokenTemplate);
110
 
                                tokenTemplate.setName(TOKEN_TEMPLATE_NAME + String.valueOf(degree2Net.getNumberOfTokens()-1+i));
 
138
                                tokenTemplate.setName(TOKEN_TEMPLATE_NAME + String.valueOf(degree2Model.marking().size() - 1 + i));
111
139
                        }
112
140
                }
113
141
 
114
 
                nta.addTimedAutomaton(createControlAutomaton(degree2Net, model));
115
 
                nta.setSystemDeclarations(createSystemDeclaration(degree2Net.getNumberOfTokens()));
116
 
                nta.setGlobalDeclarations(createGlobalDeclarations(degree2Net, model));
 
142
                nta.addTimedAutomaton(createControlAutomaton(degree2Model, conservativeModel));
 
143
                nta.setSystemDeclarations(createSystemDeclaration(degree2Model.marking().size()));
 
144
                nta.setGlobalDeclarations(createGlobalDeclarations(degree2Model, conservativeModel));
117
145
 
118
146
                return nta;
119
147
        }
120
148
 
121
 
        protected Degree2Converter getDegree2Converter() {
122
 
                return new InhibDegree2Converter();
123
 
        }
124
 
 
125
149
        private String createSystemDeclaration(int tokensInModel) {
126
 
                if(useSymmetry  || tokensInModel + extraTokens == 1){
127
 
                        return "system " + CONTROL_TEMPLATE_NAME + "," + TOKEN_TEMPLATE_NAME + ";";
128
 
                }else{
 
150
                if (useSymmetry || tokensInModel + extraTokens == 1) {
 
151
                        return "system " + CONTROL_TEMPLATE_NAME + ","
 
152
                                        + TOKEN_TEMPLATE_NAME + ";";
 
153
                } else {
129
154
                        StringBuilder builder = new StringBuilder("system ");
130
155
                        builder.append(CONTROL_TEMPLATE_NAME);
131
156
 
132
 
                        for(int i = 0; i < extraTokens + tokensInModel - 1; i++)
133
 
                        {
 
157
                        for (int i = 0; i < extraTokens + tokensInModel - 1; i++) {
134
158
                                builder.append(", ");
135
159
                                builder.append(TOKEN_TEMPLATE_NAME);
136
160
                                builder.append(i);
144
168
        protected String createGlobalDeclarations(TimedArcPetriNet degree2Net, TimedArcPetriNet originalModel) {
145
169
                StringBuilder builder = new StringBuilder();
146
170
 
147
 
                if(useSymmetry){
 
171
                if (useSymmetry) {
148
172
                        builder.append("const int N = ");
149
 
                        builder.append(degree2Net.getTokens().size() + extraTokens - 1);
 
173
                        builder.append(degree2Net.marking().size() + extraTokens - 1);
150
174
                        builder.append(";\n");
151
175
                        builder.append("typedef ");
152
176
                        builder.append("scalar[N] ");
153
177
                        builder.append(ID_TYPE);
154
178
                        builder.append(";\n");
155
179
 
156
 
                        for(int i = 0; i < numberOfInitChannels; i++){
 
180
                        for (int i = 0; i < numberOfInitChannels; i++) {
157
181
                                builder.append("chan ");
158
 
                                builder.append(String.format(INIT_CHANNEL, i,""));
 
182
                                builder.append(String.format(INIT_CHANNEL, i, ""));
159
183
                                builder.append(";\n");
160
184
                        }
161
185
                }
162
186
 
163
 
 
164
 
                for(TAPNTransition t : degree2Net.getTransitions()){
165
 
                        if(t.isFromOriginalNet()){
166
 
                                if(t.getPreset().size() == 1){
 
187
                for (TimedTransition t : degree2Net.transitions()) {
 
188
                        if(t.presetSize() == 0 && !t.hasInhibitorArcs()) {
 
189
                                continue;
 
190
                        }
 
191
                        else if (isTransitionDegree1(t)) {
167
192
                                        builder.append("broadcast chan ");
168
 
                                        builder.append(t.getName() + DEG1_SUFFIX);
169
 
                                        builder.append(";\n");
170
 
                                }else if(t.getPreset().size() == 2){
171
 
                                        builder.append("chan ");
172
 
                                        builder.append(t.getName() + DEG2_SUFFIX);
173
 
                                        builder.append(";\n");
174
 
                                }
175
 
                        }else{
176
 
                                builder.append("chan ");
177
 
                                builder.append(t.getName());
 
193
                                        builder.append(t.name() + DEG1_SUFFIX);
 
194
                                        builder.append(";\n");
 
195
                        }
 
196
                        else if (retainedTransitions.contains(t)) {
 
197
                                builder.append("chan ");
 
198
                                builder.append(t.name() + DEG2_SUFFIX);
 
199
                                builder.append(";\n");
 
200
                        } else {
 
201
                                builder.append("chan ");
 
202
                                builder.append(t.name());
178
203
                                builder.append(";\n");
179
204
                        }
180
205
                }
181
206
 
182
 
                for(TAPNTransition t : originalModel.getTransitions()){
183
 
                        if(!t.isDegree2() || t.hasInhibitorArcs()){
 
207
                for (TimedTransition t : originalModel.transitions()) {
 
208
                        if((t.presetSize() == 0 || isTransitionDegree1(t)) && !t.hasInhibitorArcs()) {
 
209
                                continue;
 
210
                        }
 
211
                        else if (!isTransitionDegree2(t) || t.hasInhibitorArcs()) {
184
212
                                builder.append("broadcast chan ");
185
 
                                builder.append(String.format(TEST_CHANNEL, t.getName(),""));
 
213
                                builder.append(String.format(TEST_CHANNEL, t.name(), ""));
186
214
                                builder.append(";\n");
187
215
                        }
188
 
                }               
 
216
                }
189
217
 
190
 
                for(int i = 0; i < largestPresetSize; i++){
 
218
                for (int i = 0; i < largestPresetSize; i++) {
191
219
                        builder.append("bool ");
192
220
                        builder.append(String.format(COUNTER_NAME, i));
193
221
                        builder.append(";\n");
200
228
                return builder.toString();
201
229
        }
202
230
 
203
 
        protected String convertInvariant(TAPNPlace place) {
 
231
        private boolean isTransitionDegree1(TimedTransition t) {
 
232
                return t.presetSize() == 1 && t.postsetSize() == 1;
 
233
        }
 
234
        
 
235
        private boolean isTransitionDegree2(TimedTransition t) {
 
236
                return t.presetSize() == 2 && t.postsetSize() == 2;
 
237
        }
 
238
 
 
239
        protected String convertInvariant(TimedPlace place) {
204
240
                String inv = "";
205
 
                String invariant = place.getInvariant();
206
 
                if(!invariant.equals("<inf")){
207
 
                        inv = CLOCK_NAME + " " + invariant;
 
241
                TimeInvariant invariant = place.invariant();
 
242
                if (!invariant.equals(TimeInvariant.LESS_THAN_INFINITY)) {
 
243
                        inv = CLOCK_NAME + " " + invariant.toString(false);
208
244
                }
209
245
 
210
246
                return inv;
211
247
        }
212
248
 
213
 
        protected Location getLocationByName(String name){
 
249
        protected Location getLocationByName(String name) {
214
250
                return namesToLocations.get(name);
215
251
        }
216
252
 
217
 
        protected void addLocationMapping(String name, Location location){
 
253
        protected void addLocationMapping(String name, Location location) {
218
254
                namesToLocations.put(name, location);
219
255
        }
220
256
 
221
 
        protected void clearLocationMappings(){
 
257
        protected void clearLocationMappings() {
222
258
                namesToLocations.clear();
223
259
        }
 
260
        
 
261
        private void clearArcMappings() {
 
262
                inputArcsToCounters.clear();
 
263
                inhibitorArcsToCounters.clear();
 
264
                transportArcsToCounters.clear();        
 
265
        }
224
266
 
225
 
        private TimedAutomaton createControlAutomaton(TimedArcPetriNet degree2Net,
226
 
                        TimedArcPetriNet model) {
 
267
        private TimedAutomaton createControlAutomaton(TimedArcPetriNet degree2Net, TimedArcPetriNet model) {
227
268
                TimedAutomaton control = new TimedAutomaton();
228
269
                createInitialLocationsForControlAutomaton(degree2Net, control);
229
270
                createEdgesForControlAutomaton(degree2Net, model, control);
230
271
                control.setName(CONTROL_TEMPLATE_NAME);
231
 
                if(useSymmetry){
232
 
                        Location initial = createInitializationTransitionsForControlAutomaton(degree2Net,control);
 
272
                if (useSymmetry) {
 
273
                        Location initial = createInitializationTransitionsForControlAutomaton(degree2Net, control);
233
274
                        control.setInitLocation(initial);
234
 
                }else{
 
275
                } else {
235
276
                        control.setInitLocation(getLocationByName(PLOCK));
236
277
                }
237
278
 
238
279
                return control;
239
280
        }
240
281
 
241
 
        private Location createInitializationTransitionsForControlAutomaton(
242
 
                        TimedArcPetriNet degree2Net, TimedAutomaton control) {
243
 
                if(degree2Net.getNumberOfTokens() == 1) return getLocationByName(PLOCK);
244
 
                        
245
 
                Location first = new Location("","");
 
282
        private Location createInitializationTransitionsForControlAutomaton(TimedArcPetriNet degree2Net, TimedAutomaton control) {
 
283
                if (degree2Net.marking().size() == 1)
 
284
                        return getLocationByName(PLOCK);
 
285
 
 
286
                Location first = new Location("", "");
246
287
                first.setCommitted(true);
247
288
                control.addLocation(first);
248
289
                Location prev = first;
249
290
 
250
 
                for(int i = 0; i < degree2Net.getNumberOfTokens()-2; i++){
251
 
                        Location l = new Location("","");
 
291
                for (int i = 0; i < degree2Net.marking().size() - 2; i++) {
 
292
                        Location l = new Location("", "");
252
293
                        l.setCommitted(true);
253
294
                        control.addLocation(l);
254
295
 
255
 
                        Edge e = new Edge(prev,
256
 
                                        l,
257
 
                                        "",
258
 
                                        String.format(INIT_CHANNEL, i, "!"),
259
 
                        "");
 
296
                        Edge e = new Edge(prev, l, "", String.format(INIT_CHANNEL, i, "!"),     "");
260
297
                        control.addTransition(e);
261
298
                        prev = l;
262
299
                }
263
300
 
264
 
                Edge e = new Edge(prev,
265
 
                                getLocationByName(PLOCK),
266
 
                                "",
267
 
                                String.format(INIT_CHANNEL, degree2Net.getNumberOfTokens()-2,"!"),
268
 
                "");
 
301
                Edge e = new Edge(prev, getLocationByName(PLOCK), "", String.format(INIT_CHANNEL, degree2Net.marking().size() - 2, "!"), "");
269
302
                control.addTransition(e);
270
303
                return first;
271
304
        }
272
305
 
273
 
        private void createEdgesForControlAutomaton(TimedArcPetriNet degree2Net,
274
 
                        TimedArcPetriNet originalModel,
275
 
                        TimedAutomaton control) {
276
 
                for(TAPNTransition transition : degree2Net.getTransitions()){
277
 
                        if(!transition.isFromOriginalNet()){
278
 
                                Pairing pairing = createPairing(transition, false);
279
 
 
280
 
                                if(!pairing.getInput().getName().equals(PLOCK)){
281
 
                                        Edge e = new Edge(getLocationByName(pairing.getInput().getName()),
282
 
                                                        getLocationByName(pairing.getOutput().getName()),
283
 
                                                        "",
284
 
                                                        transition.getName() + "!",
285
 
                                        "");
286
 
                                        control.addTransition(e);
 
306
        private void createEdgesForControlAutomaton(TimedArcPetriNet degree2Net, TimedArcPetriNet originalModel, TimedAutomaton control) {
 
307
                for (TimedTransition transition : degree2Net.transitions()) {
 
308
                        if (!retainedTransitions.contains(transition)) {
 
309
                                Degree2Pairing pairing = new Degree2Pairing(transition);
 
310
                                
 
311
                                for(TimedInputArc inputArc : transition.getInputArcs()) {
 
312
                                        if (!inputArc.source().name().equals(PLOCK) && isPartOfLockTemplate(inputArc.source().name())) {
 
313
                                                Edge e = new Edge(getLocationByName(inputArc.source().name()), 
 
314
                                                                getLocationByName(pairing.getOutputArcFor(inputArc).destination().name()), 
 
315
                                                                "", transition.name() + "!", "");
 
316
                                                control.addTransition(e);
 
317
                                        }
287
318
                                }
288
319
                        }
289
 
                }       
 
320
                }
290
321
 
291
 
                for(TAPNTransition transition : originalModel.getTransitions()){
292
 
                        if(!transition.isDegree2() || transition.hasInhibitorArcs()){
293
 
                                Location ptest = new Location("",createInvariantForControl(transition));
 
322
                for (TimedTransition transition : originalModel.transitions()) {
 
323
                        if (!(isTransitionDegree1(transition) || isTransitionDegree2(transition)) || transition.hasInhibitorArcs()) {
 
324
                                Location ptest = new Location("", createInvariantForControl(transition));
294
325
                                ptest.setCommitted(true);
295
326
                                control.addLocation(ptest);
296
327
 
297
 
                                Edge first = new Edge(getLocationByName(PLOCK),
298
 
                                                ptest,
299
 
                                                "",
300
 
                                                String.format(TEST_CHANNEL, transition.getName(), "!"),
301
 
                                "");
 
328
                                Edge first = new Edge(getLocationByName(PLOCK), ptest, "", String.format(TEST_CHANNEL, transition.name(), "!"), "");
302
329
                                control.addTransition(first);
303
330
 
304
 
                                if(transition.getPreset().size() != 1){
305
 
                                        Edge second = new Edge(ptest,
306
 
                                                        getLocationByName(String.format(P_T_IN_FORMAT, transition.getName(), 1)),
307
 
                                                        "",
308
 
                                                        String.format(T_I_IN_FORMAT+"%3$s", transition.getName(), 1, "!"),
 
331
                                if (transition.presetSize() != 1) {
 
332
                                        Edge second = new Edge(ptest, getLocationByName(String.format(P_T_IN_FORMAT, transition.name(), 1)),
 
333
                                                        "", String.format(T_I_IN_FORMAT + "%3$s", transition.name(), 1, "!"),
309
334
                                                        createResetExpressionForControl(transition));
310
335
                                        control.addTransition(second);
311
 
                                }else{
312
 
                                        Edge second = new Edge(ptest,
313
 
                                                        getLocationByName(PLOCK),
314
 
                                                        "",
315
 
                                                        String.format(T_MAX_FORMAT+"%3$s", transition.getName(), 1, "!"),
 
336
                                } else {
 
337
                                        Edge second = new Edge(ptest, getLocationByName(PLOCK), "",
 
338
                                                        String.format(T_MAX_FORMAT + "%3$s", transition.name(), 1, "!"),
316
339
                                                        createResetExpressionForControl(transition));
317
340
                                        control.addTransition(second);
318
341
                                }
320
343
                }
321
344
        }
322
345
 
323
 
        private void createInitialLocationsForControlAutomaton(
324
 
                        TimedArcPetriNet degree2Net, TimedAutomaton ta) {
325
 
                for(TAPNPlace place: degree2Net.getPlaces()){                   
326
 
                        if(isPartOfLockTemplate(place.getName())){
327
 
                                Location l = new Location(place.getName(),"");
 
346
        private void createInitialLocationsForControlAutomaton(TimedArcPetriNet degree2Net, TimedAutomaton ta) {
 
347
                for (TimedPlace place : degree2Net.places()) {
 
348
                        if (isPartOfLockTemplate(place.name())) {
 
349
                                Location l = new Location(place.name(), "");
328
350
 
329
 
                                if(!place.getName().equals(PLOCK)){
 
351
                                if (!place.name().equals(PLOCK)) {
330
352
                                        l.setCommitted(true);
331
353
                                }
332
354
 
333
355
                                ta.addLocation(l);
334
 
                                addLocationMapping(place.getName(), l);
 
356
                                addLocationMapping(place.name(), l);
335
357
                        }
336
358
                }
337
359
        }
338
360
 
339
 
        private TimedAutomaton createTokenAutomaton(TimedArcPetriNet degree2Net,
340
 
                        TimedArcPetriNet originalModel, Token token) throws Exception {
 
361
        private TimedAutomaton createTokenAutomaton(TimedArcPetriNet degree2Net, TimedArcPetriNet originalModel, TimedToken token) throws Exception {
341
362
                TimedAutomaton tokenTA = new TimedAutomaton();
342
363
                createInitialLocationsForTokenAutomata(degree2Net, tokenTA);
343
364
                createEdgesForTokenAutomata(degree2Net, tokenTA);
344
365
                createTestingEdgesForTokenAutomata(originalModel, tokenTA);
345
 
                tokenTA.setDeclarations(createLocalDeclarations(originalModel, token));
 
366
                tokenTA.setDeclarations(createLocalDeclarations());
346
367
 
347
368
                return tokenTA;
348
369
        }
349
370
 
350
 
        protected String createLocalDeclarations(TimedArcPetriNet model, Token token) {
 
371
        protected String createLocalDeclarations() {
351
372
                return "clock " + CLOCK_NAME + ";";
352
373
        }
353
374
 
354
 
        private void createInitializationTransitionsForTokenAutomata(TimedArcPetriNet degree2Net,
355
 
                        TimedAutomaton ta) {
356
 
                int i = 0;
357
 
                for(Token token : degree2Net.getTokens()){
358
 
                        if(!token.place().getName().equals(PLOCK) && !token.place().getName().equals(P_CAPACITY)){
359
 
                                Edge e = new Edge(getLocationByName(P_CAPACITY),
360
 
                                                getLocationByName(token.place().getName()),
361
 
                                                "",
362
 
                                                String.format(INIT_CHANNEL, i, "?"),
363
 
                                                createUpdateExpressionForTokenInitialization(token));
364
 
                                ta.addTransition(e);
365
 
                                i++;
366
 
                                numberOfInitChannels++;
 
375
        private void createInitializationTransitionsForTokenAutomata(TimedArcPetriNet degree2Net, TimedAutomaton ta) {
 
376
                int j = 0;
 
377
                for(TimedPlace p : degree2Net.places()) {
 
378
                        for (int i = 0; i < p.numberOfTokens(); i++) {
 
379
                                if (!p.name().equals(PLOCK) && !p.name().equals(P_CAPACITY)) {
 
380
                                        Edge e = new Edge(getLocationByName(P_CAPACITY), getLocationByName(p.name()), "", String.format(INIT_CHANNEL, j, "?"), "");
 
381
                                        ta.addTransition(e);
 
382
                                        numberOfInitChannels++;
 
383
                                        j++;
 
384
                                }
367
385
                        }
368
386
                }
369
387
        }
370
388
 
371
389
        private void createEdgesForTokenAutomata(TimedArcPetriNet degree2Net, TimedAutomaton token) {
372
 
                for(TAPNTransition transition : degree2Net.getTransitions()){
373
 
                        if(transition.isFromOriginalNet()){
374
 
                                if(transition.getPreset().size() == 1){
375
 
                                        Pairing pairing = createPairing(transition, true);
376
 
                                        String guard = createTransitionGuardWithLock(pairing.getInputArc(), pairing.getOutput(), pairing.getArcType().equals(ArcType.TARC));
377
 
                                        Edge e = new Edge(getLocationByName(pairing.getInput().getName()),
378
 
                                                        getLocationByName(pairing.getOutput().getName()),
379
 
                                                        guard,
380
 
                                                        transition.getName() + DEG1_SUFFIX + "!",
381
 
                                                        CreateResetExpressionIfNormalArc(pairing.getOutputArc()));
382
 
                                        token.addTransition(e);
383
 
                                        saveGuard(transition.getName(),pairing.getInput().getName(), guard);
384
 
                                }else{
385
 
                                        List<Pairing> pairing = CreatePairing(transition);
386
 
 
387
 
                                        Pairing pair1 = pairing.get(0);
388
 
                                        String guard1 = createTransitionGuardWithLock(pair1.getInputArc(), pair1.getOutput(), pair1.getArcType().equals(ArcType.TARC));
389
 
                                        Edge e1 = new Edge(getLocationByName(pair1.getInput().getName()),
390
 
                                                        getLocationByName(pair1.getOutput().getName()),
391
 
                                                        guard1,
392
 
                                                        transition.getName() + DEG2_SUFFIX + "?",
393
 
                                                        CreateResetExpressionIfNormalArc(pair1.getOutputArc()));
394
 
                                        token.addTransition(e1);
395
 
                                        saveGuard(transition.getName(), pair1.getInput().getName(), guard1);
396
 
 
397
 
                                        Pairing pair2 = pairing.get(1);
398
 
                                        String guard2 = createTransitionGuardWithLock(pair2.getInputArc(), pair2.getOutput(), pair2.getArcType().equals(ArcType.TARC));
399
 
                                        Edge e2 = new Edge(getLocationByName(pair2.getInput().getName()),
400
 
                                                        getLocationByName(pair2.getOutput().getName()),
401
 
                                                        guard2,
402
 
                                                        transition.getName() + DEG2_SUFFIX + "!",
403
 
                                                        CreateResetExpressionIfNormalArc(pair2.getOutputArc()));
404
 
                                        token.addTransition(e2);
405
 
                                        saveGuard(transition.getName(), pair2.getInput().getName(), guard2);
406
 
                                }
407
 
                        }else{
408
 
                                Pairing pairing = createPairing(transition, true);
409
 
                                String guard = createTransitionGuard(pairing.getInputArc(), pairing.getOutput(), pairing.getArcType().equals(ArcType.TARC));
410
 
                                Edge e = new Edge(getLocationByName(pairing.getInput().getName()),
411
 
                                                getLocationByName(pairing.getOutput().getName()),
412
 
                                                guard,
413
 
                                                transition.getName() + "?",
414
 
                                                CreateResetExpressionIfNormalArc(pairing.getOutputArc()));
415
 
                                token.addTransition(e);
416
 
                                saveGuard(transition.getName(), pairing.getInput().getName(), guard);
 
390
                for (TimedTransition transition : degree2Net.transitions()) {
 
391
                        if(transition.presetSize() == 0 && !transition.hasInhibitorArcs())
 
392
                                continue;
 
393
                        
 
394
                        Degree2Pairing pairing = new Degree2Pairing(transition);
 
395
                        
 
396
                        if (retainedTransitions.contains(transition)) {
 
397
                                        boolean first = true;
 
398
                                        String suffix = isTransitionDegree1(transition) ? DEG1_SUFFIX : DEG2_SUFFIX;
 
399
                                        
 
400
                                        for(TimedInputArc inputArc : transition.getInputArcs()) {
 
401
                                                if(isPartOfLockTemplate(inputArc.source().name()))
 
402
                                                        continue;
 
403
                                                
 
404
                                                TimedOutputArc outputArc = pairing.getOutputArcFor(inputArc);
 
405
                                                String guard = createTransitionGuardWithLock(inputArc, outputArc.destination(), false);
 
406
                                                Edge e = new Edge(getLocationByName(inputArc.source().name()), 
 
407
                                                                getLocationByName(outputArc.destination().name()), guard, 
 
408
                                                                transition.name() + suffix + (first ? "!" : "?"),
 
409
                                                                createResetExpressionForNormalArc());
 
410
                                                token.addTransition(e);
 
411
                                                saveGuard(transition.name(), inputArc.source().name(), guard);
 
412
                                                first = false;
 
413
                                        }
 
414
 
 
415
                                        for(TransportArc transArc : transition.getTransportArcsGoingThrough()) {
 
416
                                                String guard = createTransitionGuardWithLock(transArc, transArc.destination(), true);
 
417
                                                Edge e = new Edge(getLocationByName(transArc.source().name()),
 
418
                                                                getLocationByName(transArc.destination().name()),
 
419
                                                                guard, transition.name() + suffix + (first ? "!" : "?"), "");
 
420
                                                
 
421
                                                token.addTransition(e);
 
422
                                                saveGuard(transition.name(), transArc.source().name(), guard);
 
423
                                                first = false;
 
424
                                        }
 
425
                        } else {
 
426
                                for(TimedInputArc inputArc : transition.getInputArcs()) {
 
427
                                        if(isPartOfLockTemplate(inputArc.source().name()))
 
428
                                                continue;
 
429
                                        
 
430
                                        String guard = convertGuard(inputArc.interval());
 
431
                                        Edge e = new Edge(getLocationByName(inputArc.source().name()),
 
432
                                                        getLocationByName(pairing.getOutputArcFor(inputArc).destination().name()),
 
433
                                                        guard, transition.name() + "?",
 
434
                                                        createResetExpressionForNormalArc());
 
435
                                        token.addTransition(e);
 
436
                                        saveGuard(transition.name(), inputArc.source().name(), guard);
 
437
                                
 
438
                                }
 
439
                                
 
440
                                for(TransportArc transArc : transition.getTransportArcsGoingThrough()) {
 
441
                                        TimeInterval newGuard = transArc.interval().intersect(transArc.destination().invariant());
 
442
                                        String guard = convertGuard(newGuard);
 
443
                                        Edge e = new Edge(getLocationByName(transArc.source().name()),
 
444
                                                        getLocationByName(transArc.destination().name()),
 
445
                                                        guard, transition.name() + "?", "");
 
446
                                        
 
447
                                        token.addTransition(e);
 
448
                                        saveGuard(transition.name(), transArc.source().name(), guard);
 
449
                                }
417
450
                        }
418
 
                }               
 
451
                }
419
452
        }
420
453
 
421
 
        private void saveGuard(String transitionName, String inputPlaceName,
422
 
                        String guard) {
 
454
        
 
455
 
 
456
        private void saveGuard(String transitionName, String inputPlaceName, String guard) {
423
457
                String originalTransitionName = getOriginalTransitionName(transitionName);
424
 
                if(originalTransitionName != null && !originalTransitionName.isEmpty()){
425
 
                        if(!arcGuards.containsKey(originalTransitionName)){
426
 
                                arcGuards.put(originalTransitionName, new Hashtable<String, String>());
 
458
                if (originalTransitionName != null && !originalTransitionName.isEmpty()) {
 
459
                        if (!arcGuards.containsKey(originalTransitionName)) {
 
460
                                arcGuards.put(originalTransitionName,
 
461
                                                new Hashtable<String, String>());
427
462
                        }
428
463
 
429
464
                        arcGuards.get(originalTransitionName).put(inputPlaceName, guard);
434
469
                Pattern pattern = Pattern.compile("^([a-zA-Z_][a-zA-Z0-9_]*)_([0-9]*(?:_in)?)$");
435
470
 
436
471
                Matcher matcher = pattern.matcher(name);
437
 
                if(!matcher.find()){
 
472
                if (!matcher.find()) {
438
473
                        return null;
439
 
                }else{
 
474
                } else {
440
475
                        return matcher.group(1);
441
476
                }
442
477
        }
443
478
 
444
 
        private List<Pairing> CreatePairing(TAPNTransition t) {
445
 
                List<Pairing> pairing = new ArrayList<Pairing>();
446
 
                HashSet<Arc> usedPostSetArcs = new HashSet<Arc>();
447
 
 
448
 
                for(Arc inputArc : t.getPreset()){
449
 
                        for(Arc outputArc : t.getPostset()){
450
 
                                if(!usedPostSetArcs.contains(outputArc)){
451
 
                                        if(inputArc instanceof TAPNTransportArc && outputArc instanceof TAPNTransportArc && inputArc == outputArc){
452
 
                                                Pairing p = new Pairing((TAPNArc)inputArc,
453
 
                                                                ((TAPNArc)inputArc).getGuard(),
454
 
                                                                outputArc,
455
 
                                                                ArcType.TARC);
456
 
                                                pairing.add(p);
457
 
 
458
 
                                                usedPostSetArcs.add(outputArc);
459
 
                                                break;
460
 
                                        }else if(!(inputArc instanceof TAPNTransportArc) && !(outputArc instanceof TAPNTransportArc)){
461
 
                                                Pairing p = new Pairing((TAPNArc)inputArc,
462
 
                                                                ((TAPNArc)inputArc).getGuard(),
463
 
                                                                outputArc,
464
 
                                                                ArcType.NORMAL);
465
 
                                                pairing.add(p);
466
 
 
467
 
                                                usedPostSetArcs.add(outputArc);
468
 
                                                break;
469
 
                                        }
470
 
                                }
471
 
                        }
472
 
                }
473
 
 
474
 
                return pairing;
475
 
        }
476
 
 
477
 
        private Pairing createPairing(TAPNTransition transition, boolean isForTokenAutomaton) {
478
 
                Arc source = null;
479
 
                Arc dest = null;
480
 
 
481
 
                for(Arc presetArc : transition.getPreset()){
482
 
                        if(isForTokenAutomaton && !isPartOfLockTemplate(presetArc.getSource().getName()))
483
 
                        {
484
 
                                source = presetArc;
485
 
                                break;
486
 
                        }else if(!isForTokenAutomaton && isPartOfLockTemplate(presetArc.getSource().getName())){
487
 
                                source = presetArc;
488
 
                                break;
489
 
                        }
490
 
                }
491
 
 
492
 
                for(Arc postsetArc : transition.getPostset()){
493
 
                        if(isForTokenAutomaton && !isPartOfLockTemplate(postsetArc.getTarget().getName()))
494
 
                        {
495
 
                                dest = postsetArc;
496
 
                                break;
497
 
                        }else if(!isForTokenAutomaton && isPartOfLockTemplate(postsetArc.getTarget().getName())){
498
 
                                dest = postsetArc;
499
 
                                break;
500
 
                        }
501
 
                }
502
 
 
503
 
                boolean isTransportArc = source instanceof TAPNTransportArc;
504
 
                ArcType type = isTransportArc ? ArcType.TARC : ArcType.NORMAL;
505
 
 
506
 
                return new Pairing((TAPNArc)source,((TAPNArc)source).getGuard(), dest, type);
507
 
        }
508
 
 
509
479
        private void createTestingEdgesForTokenAutomata(TimedArcPetriNet originalModel, TimedAutomaton ta) throws Exception {
510
480
 
511
 
                for(TAPNTransition transition : originalModel.getTransitions()){
512
 
                        int size = transition.getPreset().size() + transition.getInhibitorArcs().size();
513
 
                        if(size > largestPresetSize) largestPresetSize = size;
 
481
                for (TimedTransition transition : originalModel.transitions()) {
 
482
                        int size = transition.presetSize() + transition.getInhibitorArcs().size();
 
483
                        if (size > largestPresetSize)
 
484
                                largestPresetSize = size;
 
485
                        
 
486
                        if(size == 0)
 
487
                                continue;
514
488
 
515
 
                        if(!transition.isDegree2() || transition.hasInhibitorArcs()){
 
489
                        if (!(isTransitionDegree1(transition) || isTransitionDegree2(transition)) || transition.hasInhibitorArcs()) {
516
490
                                int i = 0;
517
 
                                for(Arc arc : transition.getPreset()){
518
 
                                        String source = arc.getSource().getName();
519
 
                                        String counter = String.format(COUNTER_NAME, i);
520
 
                                        arcsToCounters.put(arc, counter);
521
 
 
522
 
                                        String guard = arcGuards.get(transition.getName()).get(source);
523
 
                                        if(guard == null && source.equals(P_CAPACITY)){
524
 
                                                guard = "";
525
 
                                        }else if(guard == null){
526
 
                                                if(arc instanceof TAPNInhibitorArc){
527
 
                                                        guard = createTransitionGuard((TAPNInhibitorArc)arc, null, false);
528
 
                                                }
529
 
                                                throw new Exception("guard was not precomputed");
530
 
                                        }
531
 
 
532
 
                                        //String guard = createGuardForTestingEdge(transition, arc);
533
 
                                        Edge e = new Edge(getLocationByName(source),
534
 
                                                        getLocationByName(source),
535
 
                                                        guard,
536
 
                                                        String.format(TEST_CHANNEL, transition.getName(), "?"),
537
 
                                                        String.format(COUNTER_UPDATE, counter, "= true"));
538
 
                                        ta.addTransition(e);            
539
 
                                        i++;
540
 
                                }
541
 
 
542
 
                                for(TAPNInhibitorArc arc : transition.getInhibitorArcs()){
543
 
                                        String source = arc.getSource().getName();
544
 
                                        String counter = String.format(COUNTER_NAME, i);
545
 
                                        arcsToCounters.put(arc, counter);
546
 
 
547
 
                                        Edge e = new Edge(getLocationByName(source),
548
 
                                                        getLocationByName(source),
549
 
                                                        createTransitionGuard(arc, null, false),
550
 
                                                        String.format(TEST_CHANNEL, arc.getTarget().getName(), "?"),
551
 
                                                        String.format(COUNTER_UPDATE, counter, "=true"));
 
491
                                for (TimedInputArc inputArc : transition.getInputArcs()) {
 
492
                                        String source = inputArc.source().name();
 
493
                                        String counter = String.format(COUNTER_NAME, i);
 
494
                                        inputArcsToCounters.put(inputArc, counter);
 
495
 
 
496
                                        String guard = arcGuards.get(transition.name()).get(source);
 
497
                                        if (guard == null && source.equals(P_CAPACITY)) {
 
498
                                                guard = "";
 
499
                                        } else if(guard == null)
 
500
                                                throw new Exception("guard was not precomputed");
 
501
 
 
502
                                        Edge e = new Edge(getLocationByName(source),
 
503
                                                        getLocationByName(source), guard, String.format(TEST_CHANNEL, transition.name(), "?"),
 
504
                                                        String.format(COUNTER_UPDATE, counter, "= true"));
 
505
                                        ta.addTransition(e);
 
506
                                        i++;
 
507
                                }
 
508
                                
 
509
                                for(TransportArc transArc : transition.getTransportArcsGoingThrough()) {
 
510
                                        String source = transArc.source().name();
 
511
                                        String counter = String.format(COUNTER_NAME, i);
 
512
                                        transportArcsToCounters.put(transArc, counter);
 
513
 
 
514
                                        String guard = arcGuards.get(transition.name()).get(source);
 
515
                                        if (guard == null && source.equals(P_CAPACITY)) {
 
516
                                                guard = "";
 
517
                                        } else if(guard == null)
 
518
                                                throw new Exception("guard was not precomputed");
 
519
 
 
520
                                        Edge e = new Edge(getLocationByName(source),
 
521
                                                        getLocationByName(source), guard, String.format(TEST_CHANNEL, transition.name(), "?"),
 
522
                                                        String.format(COUNTER_UPDATE, counter, "= true"));
 
523
                                        ta.addTransition(e);
 
524
                                        i++;
 
525
                                }
 
526
 
 
527
                                for (TimedInhibitorArc inhibArc : transition.getInhibitorArcs()) {
 
528
                                        String source = inhibArc.source().name();
 
529
                                        String counter = String.format(COUNTER_NAME, i);
 
530
                                        inhibitorArcsToCounters.put(inhibArc, counter);
 
531
 
 
532
                                        Edge e = new Edge(getLocationByName(source),
 
533
                                                        getLocationByName(source), convertGuard(inhibArc.interval()), 
 
534
                                                        String.format(TEST_CHANNEL, inhibArc.destination().name(),"?"), 
 
535
                                                        String.format(COUNTER_UPDATE,counter, "=true"));
552
536
                                        ta.addTransition(e);
553
537
                                        i++;
554
538
                                }
557
541
        }
558
542
 
559
543
        private void createInitialLocationsForTokenAutomata(TimedArcPetriNet degree2Net, TimedAutomaton ta) {
560
 
                for(TAPNPlace place: degree2Net.getPlaces()){                   
561
 
                        if(!isPartOfLockTemplate(place.getName())){
562
 
                                Location l = new Location(place.getName(), convertInvariant(place));
 
544
                for (TimedPlace place : degree2Net.places()) {
 
545
                        if (!isPartOfLockTemplate(place.name())) {
 
546
                                Location l = new Location(place.name(), convertInvariant(place));
563
547
                                ta.addLocation(l);
564
 
                                addLocationMapping(place.getName(), l);
 
548
                                addLocationMapping(place.name(), l);
565
549
                        }
566
550
                }
567
551
        }
568
552
 
569
 
        private String createInvariantForControl(TAPNTransition transition) {
 
553
        private String createInvariantForControl(TimedTransition transition) {
570
554
                return createBooleanExpressionForControl(transition, "==", "==");
571
555
        }
572
556
 
573
 
        private String createBooleanExpressionForControl(TAPNTransition transition, String comparison, String inhibComparison)
574
 
        {
 
557
        private String createBooleanExpressionForControl(TimedTransition transition, String comparison, String inhibComparison) {
575
558
                StringBuilder builder = new StringBuilder();
576
559
 
577
560
                boolean first = true;
578
561
 
579
 
                for(Arc presetArc : transition.getPreset()){
580
 
                        if(!first){
581
 
                                builder.append(" && ");
582
 
                        }
583
 
 
584
 
                        String counter = arcsToCounters.get(presetArc);
585
 
                        builder.append(counter);
586
 
                        builder.append(comparison);
587
 
                        builder.append("true");
588
 
                        first = false;
589
 
                }
590
 
 
591
 
                for(TAPNInhibitorArc inhib : transition.getInhibitorArcs()){
592
 
                        if(!first){
593
 
                                builder.append(" && ");
594
 
                        }
595
 
 
596
 
                        String counter = arcsToCounters.get(inhib);
 
562
                for (TimedInputArc presetArc : transition.getInputArcs()) {
 
563
                        if (!first) {
 
564
                                builder.append(" && ");
 
565
                        }
 
566
 
 
567
                        String counter = inputArcsToCounters.get(presetArc);
 
568
                        builder.append(counter);
 
569
                        builder.append(comparison);
 
570
                        builder.append("true");
 
571
                        first = false;
 
572
                }
 
573
                
 
574
                for (TransportArc transArc : transition.getTransportArcsGoingThrough()) {
 
575
                        if (!first) {
 
576
                                builder.append(" && ");
 
577
                        }
 
578
 
 
579
                        String counter = transportArcsToCounters.get(transArc);
 
580
                        builder.append(counter);
 
581
                        builder.append(comparison);
 
582
                        builder.append("true");
 
583
                        first = false;
 
584
                }
 
585
 
 
586
                for (TimedInhibitorArc inhib : transition.getInhibitorArcs()) {
 
587
                        if (!first) {
 
588
                                builder.append(" && ");
 
589
                        }
 
590
 
 
591
                        String counter = inhibitorArcsToCounters.get(inhib);
597
592
                        builder.append(counter);
598
593
                        builder.append(inhibComparison);
599
594
                        builder.append("false");
602
597
                return builder.toString();
603
598
        }
604
599
 
605
 
        private String createResetExpressionForControl(TAPNTransition transition) {
 
600
        private String createResetExpressionForControl(TimedTransition transition) {
606
601
                StringBuilder builder = new StringBuilder();
607
602
 
608
603
                boolean first = true;
609
604
 
610
 
                for(Arc presetArc : transition.getPreset()){
611
 
                        if(!first){
612
 
                                builder.append(", ");
613
 
                        }
614
 
 
615
 
                        String counter = arcsToCounters.get(presetArc);
616
 
                        builder.append(counter);
617
 
                        builder.append(":=false");
618
 
                        first = false;
619
 
                }
620
 
 
621
 
                for(TAPNInhibitorArc inhib : transition.getInhibitorArcs()){
622
 
                        if(!first){
623
 
                                builder.append(", ");
624
 
                        }
625
 
 
626
 
                        String counter = arcsToCounters.get(inhib);
627
 
                        builder.append(counter);
628
 
                        builder.append(":=false");
 
605
                for (TimedInputArc presetArc : transition.getInputArcs()) {
 
606
                        if (!first) {
 
607
                                builder.append(", ");
 
608
                        }
 
609
 
 
610
                        String counter = inputArcsToCounters.get(presetArc);
 
611
                        builder.append(counter);
 
612
                        builder.append(":=false");
 
613
                        first = false;
 
614
                }
 
615
                
 
616
                for (TransportArc transArc : transition.getTransportArcsGoingThrough()) {
 
617
                        if (!first) {
 
618
                                builder.append(", ");
 
619
                        }
 
620
 
 
621
                        String counter = transportArcsToCounters.get(transArc);
 
622
                        builder.append(counter);
 
623
                        builder.append(":=false");
 
624
                        first = false;
 
625
                }
 
626
 
 
627
                for (TimedInhibitorArc inhib : transition.getInhibitorArcs()) {
 
628
                        if (!first) {
 
629
                                builder.append(", ");
 
630
                        }
 
631
 
 
632
                        String counter = inhibitorArcsToCounters.get(inhib);
 
633
                        builder.append(counter);
 
634
                        builder.append(":=false");
 
635
                        first = false;
629
636
                }
630
637
 
631
638
                return builder.toString();
632
639
        }
633
640
 
634
 
        protected String createTransitionGuard(TAPNArc arc, TAPNPlace target, boolean isTransportArc) {
635
 
                String newGuard = PetriNetUtil.createGuard(arc.getGuard(), target, isTransportArc);
636
 
                return createTransitionGuard(newGuard);
637
 
        }
638
 
 
639
 
        protected String createTransitionGuardWithLock(TAPNArc arc, TAPNPlace target, boolean isTransportArc){
640
 
                String guard = createTransitionGuard(arc, target, isTransportArc);
641
 
 
642
 
                if(guard == null || guard.isEmpty()){
 
641
        protected String createTransitionGuardWithLock(TimedInputArc inputArc, TimedPlace targetPlace, boolean isTransportArc) {
 
642
                String guard = convertGuard(inputArc.interval());
 
643
 
 
644
                if (guard == null || guard.isEmpty()) {
643
645
                        guard = LOCK_BOOL + " == 0";
644
 
                }else{
 
646
                } else {
645
647
                        guard += " && " + LOCK_BOOL + " == 0";
646
648
                }
647
649
 
648
650
                return guard;
649
651
        }
650
 
 
651
 
        protected String createTransitionGuard(String guard) {
652
 
                if(guard.equals("false")) return guard;
653
 
                if(guard.equals("[0,inf)")) return "";
654
 
 
655
 
                String[] splitGuard = guard.substring(1, guard.length()-1).split(",");
656
 
                char firstDelim = guard.charAt(0);
657
 
                char secondDelim = guard.charAt(guard.length()-1);
658
 
 
 
652
        
 
653
        private String convertGuard(TimeInterval interval) {
 
654
                if(interval.equals(TimeInterval.ZERO_INF))
 
655
                        return "";
 
656
                
659
657
                StringBuilder builder = new StringBuilder();
660
658
                builder.append(CLOCK_NAME);
661
 
                builder.append(" ");
662
 
 
663
 
                if(firstDelim == '('){
664
 
                        builder.append(">");
665
 
                } else {
666
 
                        builder.append(">=");
667
 
                }
668
 
 
669
 
                builder.append(splitGuard[0]);
670
 
 
671
 
                if(!splitGuard[1].equals("inf")){
 
659
                if(interval.IsLowerBoundNonStrict())
 
660
                        builder.append(" >= ");
 
661
                else
 
662
                        builder.append(" > ");
 
663
                
 
664
                builder.append(interval.lowerBound().value());
 
665
                
 
666
                if(!interval.upperBound().equals(Bound.Infinity)) {
672
667
                        builder.append(" && ");
673
668
                        builder.append(CLOCK_NAME);
674
 
                        builder.append(" ");
675
 
 
676
 
                        if(secondDelim == ')'){
677
 
                                builder.append("<");
678
 
                        }else {
679
 
                                builder.append("<=");
680
 
                        }
681
 
                        builder.append(splitGuard[1]);
 
669
                        
 
670
                        if(interval.IsUpperBoundNonStrict())
 
671
                                builder.append(" <= ");
 
672
                        else
 
673
                                builder.append(" < ");
 
674
                        
 
675
                        builder.append(interval.upperBound().value());
682
676
                }
683
 
 
 
677
                
684
678
                return builder.toString();
685
 
        }       
 
679
        }
 
680
        
 
681
        private String createTransitionGuardWithLock(TransportArc transArc, TimedPlace targetPlace, boolean isTransportArc) {
 
682
                TimeInterval newGuard = transArc.interval().intersect(targetPlace.invariant());
 
683
                String guard = convertGuard(newGuard);
686
684
 
687
 
        protected String CreateResetExpressionIfNormalArc(Arc arc) {
688
 
                if(!(arc instanceof TAPNTransportArc)){
689
 
                        return String.format("%1s := 0", CLOCK_NAME);
690
 
                }else{
691
 
                        return "";
 
685
                if (guard == null || guard.isEmpty()) {
 
686
                        guard = LOCK_BOOL + " == 0";
 
687
                } else {
 
688
                        guard += " && " + LOCK_BOOL + " == 0";
692
689
                }
693
 
        }
694
 
 
695
 
        private boolean isPartOfLockTemplate(String name){
 
690
 
 
691
                return guard;
 
692
        }
 
693
 
 
694
        private String createResetExpressionForNormalArc() {
 
695
                return String.format("%1s := 0", CLOCK_NAME);
 
696
        }
 
697
 
 
698
        private boolean isPartOfLockTemplate(String name) {
696
699
                Pattern pattern = Pattern.compile("^(P_(?:[a-zA-Z][a-zA-Z0-9_]*)_(?:(?:[0-9]*_(?:in|out)|check))|P_lock|P_deadlock)$");
697
700
 
698
701
                Matcher matcher = pattern.matcher(name);
699
702
                return matcher.find();
700
703
        }
701
704
 
702
 
        protected String createUpdateExpressionForTokenInitialization(Token token) {
703
 
                return "";
704
 
        }
705
 
 
706
 
        public UPPAALQuery transformQuery(TAPNQuery tapnQuery) throws Exception {
707
 
                BroadcastTranslationQueryVisitor visitor = new BroadcastTranslationQueryVisitor(useSymmetry,tapnQuery.getTotalTokens());
 
705
        protected UPPAALQuery transformQuery(TAPNQuery tapnQuery, TimedArcPetriNet model) throws Exception {
 
706
                BroadcastTranslationQueryVisitor visitor = new BroadcastTranslationQueryVisitor(
 
707
                                useSymmetry, model.marking().size() + tapnQuery.getExtraTokens());
708
708
 
709
709
                return new StandardUPPAALQuery(visitor.getUppaalQueryFor(tapnQuery));
710
710
        }
711
711
 
712
 
        public TranslationNamingScheme namingScheme(){
 
712
        public TranslationNamingScheme namingScheme() {
713
713
                return new Degree2BroadcastNamingScheme();
714
714
        }
715
715
 
716
 
        protected class Degree2BroadcastNamingScheme implements TranslationNamingScheme {
 
716
        protected class Degree2BroadcastNamingScheme implements
 
717
                        TranslationNamingScheme {
717
718
                private static final int NOT_FOUND = -1;
718
719
                private final String START_OF_SEQUENCE_PATTERN = "^(\\w+)_(?:test|single|deg2)$";
719
720
                private Pattern startPattern = Pattern.compile(START_OF_SEQUENCE_PATTERN);
726
727
 
727
728
                        int startIndex = NOT_FOUND;
728
729
                        String originalTransitionName = null;
729
 
                        for(int i = 0; i < firingSequence.size(); i++){
 
730
                        for (int i = 0; i < firingSequence.size(); i++) {
730
731
                                String transitionName = firingSequence.get(i);
731
732
                                Matcher startMatcher = startPattern.matcher(transitionName);
732
733
 
733
734
                                boolean isStartTransition = startMatcher.matches();
734
735
 
735
 
                                if(isStartTransition){ 
736
 
                                        if(startIndex != NOT_FOUND){
737
 
                                                TransitionTranslation transitionTranslation = createTransitionTranslation(firingSequence.get(startIndex), startIndex, i-1, originalTransitionName);
 
736
                                if (isStartTransition) {
 
737
                                        if (startIndex != NOT_FOUND) {
 
738
                                                TransitionTranslation transitionTranslation = createTransitionTranslation(
 
739
                                                                firingSequence.get(startIndex), startIndex,
 
740
                                                                i - 1, originalTransitionName);
738
741
                                                transitionTranslations.add(transitionTranslation);
739
742
                                        }
740
 
                                        startIndex = i; 
741
 
                                        originalTransitionName = startMatcher.group(1); 
742
 
                                }                       
 
743
                                        startIndex = i;
 
744
                                        originalTransitionName = startMatcher.group(1);
 
745
                                }
743
746
                        }
744
 
                        
745
 
                        if(startIndex != NOT_FOUND){
746
 
                                TransitionTranslation transitionTranslation = createTransitionTranslation(firingSequence.get(startIndex), startIndex, firingSequence.size()-1, originalTransitionName);
 
747
 
 
748
                        if (startIndex != NOT_FOUND) {
 
749
                                TransitionTranslation transitionTranslation = createTransitionTranslation(
 
750
                                                firingSequence.get(startIndex), startIndex,
 
751
                                                firingSequence.size() - 1, originalTransitionName);
747
752
                                transitionTranslations.add(transitionTranslation);
748
753
                        }
749
754
                        TransitionTranslation[] array = new TransitionTranslation[transitionTranslations.size()];
751
756
                        return array;
752
757
                }
753
758
 
754
 
                private TransitionTranslation createTransitionTranslation(String startTransition, int startIndex, int endIndex, String originalTransitionName) {
755
 
                        if(testTransitionPattern.matcher(startTransition).matches()){
 
759
                private TransitionTranslation createTransitionTranslation(
 
760
                                String startTransition, int startIndex, int endIndex,
 
761
                                String originalTransitionName) {
 
762
                        if (testTransitionPattern.matcher(startTransition).matches()) {
756
763
                                startIndex += 1; // ignores _test transition
757
764
                        }
758
765
                        TransitionTranslation transitionTranslation = new TransitionTranslation(startIndex, endIndex, originalTransitionName, seqInfo);
768
775
                        return matcher.matches();
769
776
                }
770
777
 
771
 
                public boolean isIgnoredAutomata(String automata){
 
778
                public boolean isIgnoredAutomata(String automata) {
772
779
                        return automata.equals(CONTROL_TEMPLATE_NAME);
773
780
                }
774
781
        }