← Back to branch summary

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

« back to all changes in this revision

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

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

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/Export.java
8
8
 
9
9
import java.awt.image.BufferedImage;
10
10
import java.io.File;
11
 
import java.io.FileNotFoundException;
12
11
import java.io.FileOutputStream;
13
12
import java.io.IOException;
14
 
import java.io.PrintStream;
15
13
import java.util.Iterator;
16
14
 
17
15
import javax.imageio.ImageIO;
34
32
 
35
33
import pipe.dataLayer.DataLayer;
36
34
import pipe.dataLayer.PetriNetObject;
37
 
import pipe.dataLayer.TAPNQuery;
38
 
import pipe.dataLayer.TAPNQuery.SearchOption;
39
 
import pipe.dataLayer.TAPNQuery.TraceOption;
40
35
import pipe.gui.widgets.FileBrowser;
41
 
import dk.aau.cs.debug.Logger;
42
 
import dk.aau.cs.petrinet.PipeTapnToAauTapnTransformer;
43
 
import dk.aau.cs.petrinet.TAPN;
44
 
import dk.aau.cs.petrinet.colors.ColoredPipeTapnToColoredAauTapnTransformer;
45
 
import dk.aau.cs.petrinet.degree2converters.NaiveDegree2Converter;
46
 
import dk.aau.cs.translations.ReductionOption;
47
 
import dk.aau.cs.translations.tapn.BroadcastTranslation;
48
 
import dk.aau.cs.translations.tapn.Degree2BroadcastTranslation;
49
 
import dk.aau.cs.translations.tapn.OptimizedStandardSymmetryTranslation;
50
 
import dk.aau.cs.translations.tapn.OptimizedStandardTranslation;
51
 
import dk.aau.cs.translations.tapn.StandardSymmetryTranslation;
52
 
import dk.aau.cs.translations.tapn.StandardTranslation;
53
 
 
54
 
 
55
36
 
56
37
/**
57
38
 * Class for exporting things to other formats, as well as printing.
 
39
 * 
58
40
 * @author Maxim
59
41
 */
60
42
public class Export {
64
46
        public static final int PRINTER = 3;
65
47
        public static final int TIKZ = 5;
66
48
 
67
 
 
68
 
        public static void toPostScript(Object g,String filename) 
69
 
        throws PrintException, IOException {
 
49
        public static void toPostScript(Object g, String filename)
 
50
                        throws PrintException, IOException {
70
51
                // Input document type
71
52
                DocFlavor flavour = DocFlavor.SERVICE_FORMATTED.PRINTABLE;
72
53
                // Output stream MIME type
73
54
                String psMimeType = DocFlavor.BYTE_ARRAY.POSTSCRIPT.getMimeType();
74
55
 
75
56
                // Look up a print service factory that can handle this job
76
 
                StreamPrintServiceFactory[] factories = 
77
 
                        StreamPrintServiceFactory.lookupStreamPrintServiceFactories(
78
 
                                        flavour, psMimeType);
 
57
                StreamPrintServiceFactory[] factories = StreamPrintServiceFactory
 
58
                                .lookupStreamPrintServiceFactories(flavour, psMimeType);
79
59
                if (factories.length == 0) {
80
 
                        throw new RuntimeException("No suitable factory found for export to PS");
 
60
                        throw new RuntimeException(
 
61
                                        "No suitable factory found for export to PS");
81
62
                }
82
63
 
83
64
                FileOutputStream f = new FileOutputStream(filename);
88
69
                f.close();
89
70
        }
90
71
 
91
 
 
92
 
        public static void toPNG(JComponent g,String filename) throws IOException {
 
72
        public static void toPNG(JComponent g, String filename) throws IOException {
93
73
                Iterator<ImageWriter> i = ImageIO.getImageWritersBySuffix("png");
94
74
                if (!i.hasNext()) {
95
75
                        throw new RuntimeException("No ImageIO exporters can handle PNG");
96
76
                }
97
77
 
98
78
                File f = new File(filename);
99
 
                BufferedImage img = new BufferedImage(g.getPreferredSize().width,
100
 
                                g.getPreferredSize().height,
101
 
                                BufferedImage.TYPE_3BYTE_BGR);
 
79
                BufferedImage img = new BufferedImage(g.getPreferredSize().width, g.getPreferredSize().height, BufferedImage.TYPE_3BYTE_BGR);
102
80
                g.print(img.getGraphics());
103
81
                ImageIO.write(img, "png", f);
104
82
        }
105
83
 
106
84
        private static void toPrinter(Object g) throws PrintException {
107
 
                ///* The Swing way
 
85
                // /* The Swing way
108
86
                PrintRequestAttributeSet pras = new HashPrintRequestAttributeSet();
109
87
                DocFlavor flavour = DocFlavor.SERVICE_FORMATTED.PRINTABLE;
110
 
                PrintService printService[] = PrintServiceLookup.lookupPrintServices(flavour, pras);
 
88
                PrintService printService[] = PrintServiceLookup.lookupPrintServices(
 
89
                                flavour, pras);
111
90
 
112
91
                if (printService.length == 0) {
113
 
                        throw new PrintException("\nUnable to locate a compatible printer service." +
114
 
                        "\nTry exporting to PostScript.");
 
92
                        throw new PrintException(
 
93
                                        "\nUnable to locate a compatible printer service."
 
94
                                                        + "\nTry exporting to PostScript.");
115
95
                }
116
 
                PrintService defaultService = PrintServiceLookup.lookupDefaultPrintService();
117
 
                PrintService service = 
118
 
                        ServiceUI.printDialog(null, 200, 200, printService, defaultService, flavour, pras);
 
96
                PrintService defaultService = PrintServiceLookup
 
97
                                .lookupDefaultPrintService();
 
98
                PrintService service = ServiceUI.printDialog(null, 200, 200,
 
99
                                printService, defaultService, flavour, pras);
119
100
                if (service != null) {
120
101
                        DocPrintJob job = service.createPrintJob();
121
102
                        DocAttributeSet das = new HashDocAttributeSet();
122
103
                        Doc doc = new SimpleDoc(g, flavour, das);
123
104
                        job.print(doc, pras);
124
105
                }
125
 
                //*/
126
 
                /* The AWT way:
127
 
    PrinterJob pjob = PrinterJob.getPrinterJob();
128
 
    PageFormat pf = pjob.defaultPage();
129
 
    pjob.setPrintable(g, pf);
130
 
    try {
131
 
      if (pjob.printDialog()) pjob.print();
132
 
    } catch (PrinterException e) {
133
 
      error=e.toString();
134
 
    }
135
 
    //*/
 
106
                // */
 
107
                /*
 
108
                 * The AWT way: PrinterJob pjob = PrinterJob.getPrinterJob(); PageFormat
 
109
                 * pf = pjob.defaultPage(); pjob.setPrintable(g, pf); try { if
 
110
                 * (pjob.printDialog()) pjob.print(); } catch (PrinterException e) {
 
111
                 * error=e.toString(); } //
 
112
                 */
136
113
        }
137
114
 
138
 
 
139
 
        public static void exportGuiView(GuiView g,int format, DataLayer model) {
 
115
        public static void exportGuiView(DrawingSurfaceImpl g, int format,
 
116
                        DataLayer model) {
140
117
                if (g.getComponentCount() == 0) {
141
118
                        return;
142
119
                }
143
120
 
144
121
                String filename = null;
145
122
                if (CreateGui.getFile() != null) {
146
 
                        filename=CreateGui.getFile().getAbsolutePath();
 
123
                        filename = CreateGui.getFile().getAbsolutePath();
147
124
                        // change file extension
148
125
                        int dotpos = filename.lastIndexOf('.');
149
126
                        if (dotpos > filename.lastIndexOf(System.getProperty("file.separator"))) {
150
127
                                // dot is for extension
151
 
                                filename = filename.substring(0,dotpos+1);
 
128
                                filename = filename.substring(0, dotpos + 1);
152
129
                                switch (format) {
153
 
                                case PNG:        
154
 
                                        filename += "png"; 
 
130
                                case PNG:
 
131
                                        filename += "png";
155
132
                                        break;
156
 
                                case POSTSCRIPT: 
 
133
                                case POSTSCRIPT:
157
134
                                        filename += "ps";
158
 
                                        break;  
 
135
                                        break;
159
136
                                case TIKZ:
160
137
                                        filename += "tex";
161
138
                                }
168
145
                try {
169
146
                        switch (format) {
170
147
                        case PNG:
171
 
                                filename = new FileBrowser("PNG image","png",filename).saveFile();
 
148
                                filename = new FileBrowser("PNG image", "png", filename).saveFile();
172
149
                                if (filename != null) {
173
150
                                        toPNG(g, filename);
174
151
                                }
175
152
                                break;
176
153
                        case POSTSCRIPT:
177
 
                                filename = new FileBrowser("PostScript file","ps",filename).saveFile();
 
154
                                filename = new FileBrowser("PostScript file", "ps", filename)
 
155
                                                .saveFile();
178
156
                                if (filename != null) {
179
157
                                        toPostScript(g, filename);
180
158
                                }
181
159
                                break;
182
160
                        case PRINTER:
183
161
                                toPrinter(g);
184
 
                                break;  
 
162
                                break;
185
163
                        case TIKZ:
186
 
                                Object[] possibilities = {"Only the TikZ figure", "Full compilable LaTex including your figure"};
187
 
                                String figureOptions = (String)JOptionPane.showInputDialog(
188
 
                                                CreateGui.getApp(),
189
 
                                                "Choose how you would like your TikZ figure outputted: \n",
190
 
                                                "Export to TikZ",
191
 
                                                JOptionPane.PLAIN_MESSAGE,
192
 
                                                null,
193
 
                                                possibilities,
194
 
                                                "Only the TikZ figure");
195
 
                                TikZExporter.TikZOutputOption tikZOption  = TikZExporter.TikZOutputOption.FIGURE_ONLY;
196
 
                                if(figureOptions == null)
 
164
                                Object[] possibilities = { "Only the TikZ figure",
 
165
                                                "Full compilable LaTex including your figure" };
 
166
                                String figureOptions = (String) JOptionPane.showInputDialog(
 
167
                                                                CreateGui.getApp(),
 
168
                                                                "Choose how you would like your TikZ figure outputted: \n",
 
169
                                                                "Export to TikZ", JOptionPane.PLAIN_MESSAGE,
 
170
                                                                null, possibilities, "Only the TikZ figure");
 
171
                                TikZExporter.TikZOutputOption tikZOption = TikZExporter.TikZOutputOption.FIGURE_ONLY;
 
172
                                if (figureOptions == null)
197
173
                                        return;
198
174
 
199
 
                                if(figureOptions == possibilities[0])
 
175
                                if (figureOptions == possibilities[0])
200
176
                                        tikZOption = TikZExporter.TikZOutputOption.FIGURE_ONLY;
201
 
                                if(figureOptions == possibilities[1])
 
177
                                if (figureOptions == possibilities[1])
202
178
                                        tikZOption = TikZExporter.TikZOutputOption.FULL_LATEX;
203
179
 
204
 
                                filename=new FileBrowser("TikZ figure","tex",filename).saveFile();
205
 
                                if (filename!=null) {
206
 
                                        TikZExporter output;
207
 
                                        if(!model.isUsingColors()){
208
 
                                                output = new TikZExporter(model,filename,tikZOption);
209
 
                                        }else{
210
 
                                                output = new TikZExporterForColoredTAPN(model, filename, tikZOption);
211
 
                                        }
 
180
                                filename = new FileBrowser("TikZ figure", "tex", filename).saveFile();
 
181
                                if (filename != null) {
 
182
                                        TikZExporter output = new TikZExporter(model, filename, tikZOption);
212
183
                                        output.ExportToTikZ();
213
184
                                }
214
185
                        }
216
187
                        // There was some problem with the action
217
188
                        JOptionPane.showMessageDialog(CreateGui.getApp(),
218
189
                                        "There were errors performing the requested action:\n" + e,
219
 
                                        "Error", JOptionPane.ERROR_MESSAGE
220
 
                        );
 
190
                                        "Error", JOptionPane.ERROR_MESSAGE);
221
191
                }
222
192
 
223
193
                resetViewAfterExport(g, gridEnabled);
225
195
                return;
226
196
        }
227
197
 
228
 
 
229
 
        private static void resetViewAfterExport(GuiView g, boolean gridEnabled) {
 
198
        private static void resetViewAfterExport(DrawingSurfaceImpl g,
 
199
                        boolean gridEnabled) {
230
200
                if (gridEnabled) {
231
201
                        Grid.enableGrid();
232
202
                }
234
204
                g.repaint();
235
205
        }
236
206
 
237
 
 
238
 
        private static void setupViewForExport(GuiView g, boolean gridEnabled) {
 
207
        private static void setupViewForExport(DrawingSurfaceImpl g, boolean gridEnabled) {
239
208
                // Stuff to make it export properly
240
209
                g.updatePreferredSize();
241
210
                PetriNetObject.ignoreSelection(true);
243
212
                        Grid.disableGrid();
244
213
                }
245
214
        }
246
 
 
247
 
        
248
 
        public static void exportUppaalXMLFromQuery(DataLayer appModel, TAPNQuery input, String modelFile, String queryFile) {
249
 
                File xmlfile=null, qfile=null;
250
 
                try {
251
 
                        xmlfile = new File(modelFile);
252
 
                        qfile = new File(queryFile);
253
 
                } catch (NullPointerException e2) {
254
 
                        // TODO Auto-generated catch block
255
 
                        e2.printStackTrace();
256
 
                        return;
257
 
                }
258
 
        
259
 
                //Create transformer
260
 
                PipeTapnToAauTapnTransformer transformer = null;
261
 
 
262
 
                if(appModel.isUsingColors()){
263
 
                        transformer = new ColoredPipeTapnToColoredAauTapnTransformer();
264
 
                }else{
265
 
                        transformer = new PipeTapnToAauTapnTransformer();
266
 
                }
267
 
 
268
 
                TAPN model=null;
269
 
                try {
270
 
                        model = transformer.getAAUTAPN(appModel, 0);
271
 
                } catch (Exception e) {
272
 
                        e.printStackTrace();
273
 
                }
274
 
 
275
 
                if (CreateGui.getApp().getComponentCount() == 0) {
276
 
                        return;
277
 
                }
278
 
 
279
 
 
280
 
                int capacity;
281
 
                capacity = input.getCapacity();
282
 
                String inputQuery = input.getQuery();
283
 
                TraceOption traceOption = input.getTraceOption();
284
 
                SearchOption searchOption = input.getSearchOption();
285
 
                String verifytaOptions = "";
286
 
 
287
 
                if (traceOption == TraceOption.SOME){
288
 
                        verifytaOptions = "-t0";
289
 
                }else if (traceOption == TraceOption.FASTEST){
290
 
                        verifytaOptions = "-t2";
291
 
                }else if (traceOption == TraceOption.NONE){
292
 
                        verifytaOptions = "";
293
 
                }
294
 
 
295
 
                if (searchOption == SearchOption.BFS){
296
 
                        verifytaOptions += "-o0";
297
 
                }else if (searchOption == SearchOption.DFS ){
298
 
                        verifytaOptions += "-o1";
299
 
                }else if (searchOption == SearchOption.RDFS ){
300
 
                        verifytaOptions += "-o2";
301
 
                }else if (searchOption == SearchOption.CLOSE_TO_TARGET_FIRST){
302
 
                        verifytaOptions += "-o6";
303
 
                }
304
 
 
305
 
                if (inputQuery == null) {return;}
306
 
 
307
 
                // TODO: Refactor so translation to dk.aau.cs.petrinet.TAPNQuery happens exactly once
308
 
                
309
 
                // Select the model based on selected export option.
310
 
                if (input.getReductionOption() == ReductionOption.STANDARDSYMMETRY){
311
 
 
312
 
                        StandardSymmetryTranslation t = new StandardSymmetryTranslation();
313
 
                        try {
314
 
                                t.autoTransform(model, new PrintStream(xmlfile), new PrintStream(qfile), new dk.aau.cs.petrinet.TAPNQuery(input.getProperty(), 0), capacity);
315
 
                        } catch (FileNotFoundException e) {
316
 
                                // TODO Auto-generated catch block
317
 
                                e.printStackTrace();
318
 
                        }
319
 
 
320
 
                } else if (input.getReductionOption() == ReductionOption.OPTIMIZEDSTANDARDSYMMETRY){
321
 
 
322
 
                        OptimizedStandardSymmetryTranslation t = new OptimizedStandardSymmetryTranslation();
323
 
                        try {
324
 
                                t.autoTransform(model, new PrintStream(xmlfile), new PrintStream(qfile), new dk.aau.cs.petrinet.TAPNQuery(input.getProperty(), 0), capacity);
325
 
                        } catch (FileNotFoundException e) {
326
 
                                // TODO Auto-generated catch block
327
 
                                e.printStackTrace();
328
 
                        }
329
 
                }else if (input.getReductionOption() == ReductionOption.OPTIMIZEDSTANDARD){
330
 
                        Logger.log("Using ADV_NOSYMQ");
331
 
                        OptimizedStandardTranslation t = new OptimizedStandardTranslation();
332
 
                        try {
333
 
                                t.autoTransform(model, new PrintStream(xmlfile), new PrintStream(qfile), new dk.aau.cs.petrinet.TAPNQuery(input.getProperty(), 0), capacity);
334
 
                        } catch (FileNotFoundException e) {
335
 
                                // TODO Auto-generated catch block
336
 
                                e.printStackTrace();
337
 
                        }       
338
 
 
339
 
 
340
 
                } else if(input.getReductionOption() == ReductionOption.BROADCAST || input.getReductionOption() == ReductionOption.BROADCASTSYMMETRY){
341
 
                        BroadcastTranslation broadcastTransformer = null;
342
 
                        if(appModel.isUsingColors()){
343
 
                                broadcastTransformer = new dk.aau.cs.translations.coloredtapn.ColoredBroadcastTranslation(capacity, input.getReductionOption() == ReductionOption.BROADCASTSYMMETRY);
344
 
                        }else{
345
 
                                broadcastTransformer = new dk.aau.cs.translations.tapn.BroadcastTranslation(capacity, input.getReductionOption() == ReductionOption.BROADCASTSYMMETRY);
346
 
                        }
347
 
                        try{
348
 
                                dk.aau.cs.TA.NTA nta = broadcastTransformer.transformModel(model);
349
 
                                nta.outputToUPPAALXML(new PrintStream(xmlfile));
350
 
                                dk.aau.cs.TA.UPPAALQuery query = broadcastTransformer.transformQuery(new dk.aau.cs.petrinet.TAPNQuery(input.getProperty(), capacity + 1 + model.getTokens().size()));
351
 
                                query.output(new PrintStream(qfile));
352
 
                        }catch(FileNotFoundException e){
353
 
                                e.printStackTrace();
354
 
                        } catch (Exception e) {
355
 
                                // TODO Auto-generated catch block
356
 
                                e.printStackTrace();
357
 
                        }
358
 
                } else if(input.getReductionOption() == ReductionOption.DEGREE2BROADCASTSYMMETRY || input.getReductionOption() == ReductionOption.DEGREE2BROADCAST){
359
 
                        Degree2BroadcastTranslation broadcastTransformer = null;
360
 
                        if(appModel.isUsingColors()){
361
 
                                broadcastTransformer = new dk.aau.cs.translations.coloredtapn.ColoredDegree2BroadcastTranslation(capacity, input.getReductionOption() == ReductionOption.DEGREE2BROADCASTSYMMETRY);
362
 
                        }else{
363
 
                                broadcastTransformer = new dk.aau.cs.translations.tapn.Degree2BroadcastTranslation(capacity, input.getReductionOption() == ReductionOption.DEGREE2BROADCASTSYMMETRY);
364
 
                        }
365
 
                        try{
366
 
                                dk.aau.cs.TA.NTA nta = broadcastTransformer.transformModel(model);
367
 
                                nta.outputToUPPAALXML(new PrintStream(xmlfile));
368
 
                                dk.aau.cs.TA.UPPAALQuery query = broadcastTransformer.transformQuery(new dk.aau.cs.petrinet.TAPNQuery(input.getProperty(), capacity + 1 + model.getTokens().size()));
369
 
                                query.output(new PrintStream(qfile));
370
 
                        }catch(FileNotFoundException e){
371
 
                                e.printStackTrace();
372
 
                        } catch (Exception e) {
373
 
                                // TODO Auto-generated catch block
374
 
                                e.printStackTrace();
375
 
                        }
376
 
                }
377
 
                else {
378
 
 
379
 
                        try {
380
 
                                model.convertToConservative();
381
 
                        } catch (Exception e1) {
382
 
                                // TODO Auto-generated catch block
383
 
                                e1.printStackTrace();
384
 
                        }
385
 
 
386
 
                        try {
387
 
                                NaiveDegree2Converter deg2Converter = new NaiveDegree2Converter();
388
 
                                model = deg2Converter.transform(model);
389
 
                        } catch (Exception e1) {
390
 
                                // TODO Auto-generated catch block
391
 
                                e1.printStackTrace();
392
 
                        }
393
 
 
394
 
 
395
 
 
396
 
                        //Create uppaal xml file
397
 
                        try {
398
 
                                StandardTranslation t2 = new StandardTranslation(model, new PrintStream(xmlfile), capacity);
399
 
                                t2.transform();
400
 
                                t2.transformQueriesToUppaal(capacity, new dk.aau.cs.petrinet.TAPNQuery(input.getProperty(), 0), new PrintStream(qfile));
401
 
                        } catch (FileNotFoundException e) {
402
 
                                // TODO Auto-generated catch block
403
 
                                e.printStackTrace();
404
 
                        } catch (Exception e) {
405
 
                                // TODO Auto-generated catch block
406
 
                                e.printStackTrace();
407
 
                        }
408
 
                }
409
 
        }       
410
215
}