← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/verification/UPPAAL/UppaalExporter.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/verification/UPPAAL/UppaalExporter.java
1
1
package dk.aau.cs.verification.UPPAAL;
2
2
 
3
3
import java.io.File;
4
 
import java.io.FileNotFoundException;
5
4
import java.io.IOException;
6
5
import java.io.PrintStream;
7
6
 
8
 
import dk.aau.cs.TA.NTA;
9
 
import dk.aau.cs.TA.UPPAALQuery;
10
 
import dk.aau.cs.petrinet.TAPN;
11
 
import dk.aau.cs.petrinet.TAPNQuery;
12
 
import dk.aau.cs.petrinet.TimedArcPetriNet;
13
 
import dk.aau.cs.petrinet.colors.ColoredTimedArcPetriNet;
14
 
import dk.aau.cs.petrinet.degree2converters.NaiveDegree2Converter;
15
 
import dk.aau.cs.translations.ColoredTranslationNamingScheme;
 
7
import dk.aau.cs.model.tapn.TAPNQuery;
16
8
import dk.aau.cs.translations.ModelTranslator;
17
 
import dk.aau.cs.translations.QueryTranslator;
18
9
import dk.aau.cs.translations.ReductionOption;
19
 
import dk.aau.cs.translations.TranslationNamingScheme;
20
 
import dk.aau.cs.translations.coloredtapn.ColoredBroadcastTranslation;
21
 
import dk.aau.cs.translations.coloredtapn.ColoredDegree2BroadcastKBoundOptimizationTransformer;
22
 
import dk.aau.cs.translations.coloredtapn.ColoredDegree2BroadcastTranslation;
23
10
import dk.aau.cs.translations.tapn.BroadcastTranslation;
24
11
import dk.aau.cs.translations.tapn.Degree2BroadcastKBoundOptimizeTranslation;
25
12
import dk.aau.cs.translations.tapn.Degree2BroadcastTranslation;
26
 
import dk.aau.cs.translations.tapn.OptimizedStandardNamingScheme;
27
 
import dk.aau.cs.translations.tapn.OptimizedStandardSymmetryTranslation;
28
13
import dk.aau.cs.translations.tapn.OptimizedStandardTranslation;
29
 
import dk.aau.cs.translations.tapn.StandardNamingScheme;
30
 
import dk.aau.cs.translations.tapn.StandardSymmetryTranslation;
31
14
import dk.aau.cs.translations.tapn.StandardTranslation;
 
15
import dk.aau.cs.util.Tuple;
32
16
 
33
17
public class UppaalExporter {
34
 
        public ExportedModel export(ColoredTimedArcPetriNet model, TAPNQuery query, ReductionOption reduction){
35
 
                File xmlfile = createTempFile(".xml");
36
 
                File qfile = createTempFile(".q");
37
 
                if(xmlfile == null || qfile == null) return null;
38
 
 
39
 
                int extraTokens = query.getTotalTokens() - model.getNumberOfTokens();
40
 
 
41
 
                ModelTranslator<TimedArcPetriNet, NTA> modelTransformer = null;
42
 
                QueryTranslator<TAPNQuery, UPPAALQuery> queryTransformer = null;
43
 
                ColoredTranslationNamingScheme namingScheme = null;
44
 
                if(reduction == ReductionOption.BROADCAST || reduction == ReductionOption.BROADCASTSYMMETRY){
45
 
                        ColoredBroadcastTranslation transformer = new ColoredBroadcastTranslation(extraTokens, reduction == ReductionOption.BROADCASTSYMMETRY);
46
 
                        modelTransformer = transformer;
47
 
                        queryTransformer = transformer;
48
 
                        namingScheme = transformer.namingScheme();
49
 
                }  else if(reduction == ReductionOption.KBOUNDANALYSIS){
50
 
                        Degree2BroadcastTranslation broadcastTransformer = new ColoredDegree2BroadcastTranslation(extraTokens, true);
51
 
                        modelTransformer = broadcastTransformer;
52
 
                        queryTransformer = broadcastTransformer;
53
 
                }else if(reduction == ReductionOption.KBOUNDOPTMIZATION){
54
 
                        Degree2BroadcastTranslation broadcastTransformer = new ColoredDegree2BroadcastKBoundOptimizationTransformer(extraTokens);
55
 
                        modelTransformer = broadcastTransformer;
56
 
                        queryTransformer = broadcastTransformer;
57
 
                }else{
58
 
                        ColoredDegree2BroadcastTranslation broadcastTransformer = new ColoredDegree2BroadcastTranslation(extraTokens, reduction == ReductionOption.DEGREE2BROADCASTSYMMETRY);
59
 
                        modelTransformer = broadcastTransformer;
60
 
                        queryTransformer = broadcastTransformer;
61
 
                        namingScheme = broadcastTransformer.namingScheme();
 
18
        public ExportedModel export(dk.aau.cs.model.tapn.TimedArcPetriNet model, TAPNQuery query, ReductionOption reduction) {
 
19
                File modelFile = createTempFile(".xml");
 
20
                File queryFile = createTempFile(".q");
 
21
 
 
22
                return export(model, query, reduction, modelFile, queryFile);
 
23
        }
 
24
 
 
25
        public ExportedModel export(dk.aau.cs.model.tapn.TimedArcPetriNet model, TAPNQuery query, ReductionOption reduction, File modelFile, File queryFile) {
 
26
                if (modelFile == null || queryFile == null) return null;
 
27
 
 
28
                ModelTranslator<dk.aau.cs.model.tapn.TimedArcPetriNet, TAPNQuery, dk.aau.cs.model.NTA.NTA, dk.aau.cs.model.NTA.UPPAALQuery> translator = null;
 
29
                        
 
30
                if (reduction == ReductionOption.STANDARD || reduction == ReductionOption.STANDARDSYMMETRY) {
 
31
                        translator = new StandardTranslation(reduction == ReductionOption.STANDARDSYMMETRY); 
 
32
                } else if (reduction == ReductionOption.OPTIMIZEDSTANDARD 
 
33
                                || reduction == ReductionOption.OPTIMIZEDSTANDARDSYMMETRY
 
34
                                || (reduction == ReductionOption.KBOUNDANALYSIS && !model.hasInhibitorArcs())) {
 
35
                        translator = new OptimizedStandardTranslation(reduction == ReductionOption.OPTIMIZEDSTANDARDSYMMETRY || reduction == ReductionOption.KBOUNDANALYSIS);
 
36
                } else if (reduction == ReductionOption.BROADCAST || reduction == ReductionOption.BROADCASTSYMMETRY) {
 
37
                        translator = new BroadcastTranslation(reduction == ReductionOption.BROADCASTSYMMETRY);
 
38
                } else if (reduction == ReductionOption.DEGREE2BROADCASTSYMMETRY || reduction == ReductionOption.DEGREE2BROADCAST || (reduction == ReductionOption.KBOUNDANALYSIS && model.hasInhibitorArcs())) {
 
39
                        translator = new Degree2BroadcastTranslation(reduction == ReductionOption.DEGREE2BROADCASTSYMMETRY);
 
40
                } else if (reduction == ReductionOption.KBOUNDOPTMIZATION) {
 
41
                        translator = new Degree2BroadcastKBoundOptimizeTranslation();
 
42
                } else {
 
43
                        throw new RuntimeException("Invalid reduction selected. Please try again");
62
44
                }
63
45
                
64
 
                try{
65
 
                        NTA nta = modelTransformer.transformModel(model);
66
 
                        nta.outputToUPPAALXML(new PrintStream(xmlfile));
67
 
                        UPPAALQuery uppaalQuery = queryTransformer.transformQuery(query);
68
 
                        uppaalQuery.output(new PrintStream(qfile));
69
 
                }catch(FileNotFoundException e){
70
 
                        e.printStackTrace();
71
 
                        return null;
 
46
                try { 
 
47
                        Tuple<dk.aau.cs.model.NTA.NTA, dk.aau.cs.model.NTA.UPPAALQuery> translatedModel = translator.translate(model, query);
 
48
                        translatedModel.value1().outputToUPPAALXML(new PrintStream(modelFile));
 
49
                        translatedModel.value2().output(new PrintStream(queryFile));
72
50
                } catch (Exception e) {
73
51
                        e.printStackTrace();
74
52
                        return null;
75
53
                }
76
 
 
77
 
                return new ExportedModel(xmlfile.getAbsolutePath(), qfile.getAbsolutePath(), namingScheme);
78
 
        }
79
 
 
80
 
        public ExportedModel export(TimedArcPetriNet model, TAPNQuery query, ReductionOption reduction){
81
 
                File xmlfile = createTempFile(".xml");
82
 
                File qfile = createTempFile(".q");
83
 
                if(xmlfile == null || qfile == null) return null;
84
 
 
85
 
                int extraTokens = query.getTotalTokens() - model.getNumberOfTokens();
86
 
                TranslationNamingScheme namingScheme = null;
87
 
                if (reduction == ReductionOption.STANDARDSYMMETRY){
88
 
 
89
 
                        StandardSymmetryTranslation t = new StandardSymmetryTranslation();
90
 
                        try {
91
 
                                t.autoTransform((TAPN)model, new PrintStream(xmlfile), new PrintStream(qfile), query, extraTokens);
92
 
                        } catch (FileNotFoundException e) {
93
 
                                e.printStackTrace();
94
 
                                return null;
95
 
                        }
96
 
 
97
 
                } else if (reduction == ReductionOption.OPTIMIZEDSTANDARDSYMMETRY || (reduction == ReductionOption.KBOUNDANALYSIS && !((TAPN)model).hasInhibitorArcs())){
98
 
                        OptimizedStandardSymmetryTranslation t = new OptimizedStandardSymmetryTranslation();
99
 
                        try {
100
 
                                t.autoTransform((TAPN)model, new PrintStream(xmlfile), new PrintStream(qfile), query, extraTokens);
101
 
                        } catch (FileNotFoundException e) {
102
 
                                e.printStackTrace();
103
 
                                return null;
104
 
                        }
105
 
                }else if (reduction == ReductionOption.OPTIMIZEDSTANDARD){
106
 
                        OptimizedStandardTranslation t = new OptimizedStandardTranslation();
107
 
                        try {
108
 
                                t.autoTransform((TAPN)model, new PrintStream(xmlfile), new PrintStream(qfile), query, extraTokens);
109
 
                        } catch (FileNotFoundException e) {
110
 
                                e.printStackTrace();
111
 
                                return null;
112
 
                        }       
113
 
                        namingScheme = new OptimizedStandardNamingScheme();
114
 
                } else if(reduction == ReductionOption.BROADCAST || reduction == ReductionOption.BROADCASTSYMMETRY){
115
 
                        BroadcastTranslation broadcastTransformer = new BroadcastTranslation(extraTokens, reduction == ReductionOption.BROADCASTSYMMETRY);
116
 
                        namingScheme = broadcastTransformer.namingScheme();
117
 
                        try{
118
 
                                dk.aau.cs.TA.NTA nta = broadcastTransformer.transformModel(model);
119
 
                                nta.outputToUPPAALXML(new PrintStream(xmlfile));
120
 
                                dk.aau.cs.TA.UPPAALQuery uppaalQuery = broadcastTransformer.transformQuery(query);
121
 
                                uppaalQuery.output(new PrintStream(qfile));
122
 
                        }catch(FileNotFoundException e){
123
 
                                e.printStackTrace();
124
 
                                return null;
125
 
                        } catch (Exception e) {
126
 
                                e.printStackTrace();
127
 
                                return null;
128
 
                        }
129
 
                } else if(reduction == ReductionOption.DEGREE2BROADCASTSYMMETRY || reduction == ReductionOption.DEGREE2BROADCAST || (reduction == ReductionOption.KBOUNDANALYSIS && ((TAPN)model).hasInhibitorArcs())){
130
 
                        Degree2BroadcastTranslation broadcastTransformer = new Degree2BroadcastTranslation(extraTokens, reduction == ReductionOption.DEGREE2BROADCASTSYMMETRY);
131
 
                        namingScheme = broadcastTransformer.namingScheme();
132
 
                        try{
133
 
                                dk.aau.cs.TA.NTA nta = broadcastTransformer.transformModel(model);
134
 
                                nta.outputToUPPAALXML(new PrintStream(xmlfile));
135
 
                                dk.aau.cs.TA.UPPAALQuery uppaalQuery = broadcastTransformer.transformQuery(query);
136
 
                                uppaalQuery.output(new PrintStream(qfile));
137
 
                        }catch(FileNotFoundException e){
138
 
                                e.printStackTrace();
139
 
                                return null;
140
 
                        } catch (Exception e) {
141
 
                                e.printStackTrace();
142
 
                                return null;
143
 
                        }
144
 
                } else if(reduction == ReductionOption.KBOUNDOPTMIZATION){
145
 
                        Degree2BroadcastKBoundOptimizeTranslation transformer = new Degree2BroadcastKBoundOptimizeTranslation(extraTokens);
146
 
 
147
 
                        try{
148
 
                                dk.aau.cs.TA.NTA nta = transformer.transformModel(model);
149
 
                                nta.outputToUPPAALXML(new PrintStream(xmlfile));
150
 
                                dk.aau.cs.TA.UPPAALQuery uppaalQuery = transformer.transformQuery(query);
151
 
                                uppaalQuery.output(new PrintStream(qfile));
152
 
                        }catch(FileNotFoundException e){
153
 
                                e.printStackTrace();
154
 
                                return null;
155
 
                        } catch (Exception e) {
156
 
                                e.printStackTrace();
157
 
                                return null;
158
 
                        }
159
 
                }else {
160
 
 
161
 
                        try {
162
 
                                model.convertToConservative();
163
 
                        } catch (Exception e1) {
164
 
                                e1.printStackTrace();
165
 
                                return null;
166
 
                        }
167
 
 
168
 
                        try {
169
 
                                NaiveDegree2Converter deg2Converter = new NaiveDegree2Converter();
170
 
                                model = deg2Converter.transform((TAPN)model);
171
 
                        } catch (Exception e1) {
172
 
                                e1.printStackTrace();
173
 
                                return null;
174
 
                        }
175
 
 
176
 
 
177
 
 
178
 
                        //Create uppaal xml file
179
 
                        try {
180
 
                                StandardTranslation t2 = new StandardTranslation((TAPN)model, new PrintStream(xmlfile), extraTokens);
181
 
                                t2.transform();
182
 
                                t2.transformQueriesToUppaal(extraTokens, query, new PrintStream(qfile));
183
 
                        } catch (FileNotFoundException e) {
184
 
                                e.printStackTrace();
185
 
                                return null;
186
 
                        } catch (Exception e) {
187
 
                                e.printStackTrace();
188
 
                                return null;
189
 
                        }
190
 
 
191
 
                        namingScheme = new StandardNamingScheme();
192
 
                }
193
 
                return new ExportedModel(xmlfile.getAbsolutePath(), qfile.getAbsolutePath(), namingScheme);
 
54
                
 
55
                return new ExportedModel(modelFile.getAbsolutePath(), queryFile.getAbsolutePath(), translator.namingScheme());
 
56
 
194
57
        }
195
58
 
196
59
        private File createTempFile(String ending) {
197
 
                File file=null;
 
60
                File file = null;
198
61
                try {
199
62
                        file = File.createTempFile("verifyta", ending);
200
63