Merge lp:~tapaal-contributor/tapaal/add-export-options into lp:tapaal
- add-export-options
- Merge into trunk
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 1120 |
Merged at revision: | 1114 |
Proposed branch: | lp:~tapaal-contributor/tapaal/add-export-options |
Merge into: | lp:tapaal |
Diff against target: |
497 lines (+176/-125) 6 files modified
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java (+9/-9) src/pipe/gui/Export.java (+114/-83) src/pipe/gui/ExportBatchDialog.java (+46/-26) src/pipe/gui/GuiFrame.java (+4/-4) src/pipe/gui/widgets/QueryDialog.java (+2/-2) src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java (+1/-1) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/add-export-options |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Lena Ernstsen (community) | Needs Resubmitting | ||
Kenneth Yrke Jørgensen | code | Approve | |
Review via email: mp+394850@code.launchpad.net |
Commit message
Added different export formats in the batch dialog
Description of the change
Added the options to export to verifyTAPN and verifyDTAPN by selecting the engine in a drop down menu
Jiri Srba (srba) wrote : | # |
Two other things to fix:
1. when exporting to verifytapn and verifydtapn and model that has more than one query, it creates a single query.q file that does not parse by the engines (each query needs to get a separate query file, number them for example as query-1.q query-2.q etc).
2. In the batch export dropdown menu, add "model and queries" for the verifytapn and verifydtapn description.
3. The Export menu name should be: "Batch export of models and queries"
- 1120. By Lena Ernstsen
-
Fixed names and query files + cleaned up
Lena Ernstsen (lsaid) : | # |
Lena Ernstsen (lsaid) wrote : | # |
Fixed code styling and naming of elements in the UI. Also changed the way the queries are saved, so each query gets a query file
Jiri Srba (srba) wrote : | # |
Tested and works very well.
Preview Diff
1 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java' | |||
2 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2020-08-06 13:48:04 +0000 | |||
3 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2020-12-14 17:15:10 +0000 | |||
4 | @@ -30,10 +30,10 @@ | |||
5 | 30 | } | 30 | } |
6 | 31 | 31 | ||
7 | 32 | 32 | ||
9 | 33 | return export(model, query, modelFile, queryFile, null, lens); | 33 | return export(model, query, modelFile, queryFile, lens); |
10 | 34 | } | 34 | } |
11 | 35 | 35 | ||
13 | 36 | public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, pipe.dataLayer.TAPNQuery dataLayerQuery, TabContent.TAPNLens lens) { | 36 | public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, TabContent.TAPNLens lens) { |
14 | 37 | if (modelFile == null || queryFile == null) | 37 | if (modelFile == null || queryFile == null) |
15 | 38 | return null; | 38 | return null; |
16 | 39 | 39 | ||
17 | @@ -44,16 +44,16 @@ | |||
18 | 44 | modelStream.close(); | 44 | modelStream.close(); |
19 | 45 | 45 | ||
20 | 46 | PrintStream queryStream = new PrintStream(queryFile); | 46 | PrintStream queryStream = new PrintStream(queryFile); |
26 | 47 | if (query.getCategory() == QueryCategory.CTL){ | 47 | if (query == null) { |
27 | 48 | CTLQueryVisitor XMLVisitor = new CTLQueryVisitor(); | 48 | throw new FileNotFoundException(null); |
28 | 49 | queryStream.append(XMLVisitor.getXMLQueryFor(query.getProperty(), null)); | 49 | } else if (query.getCategory() == QueryCategory.CTL) { |
29 | 50 | } else if (lens != null && lens.isGame()) { | 50 | CTLQueryVisitor XMLVisitor = new CTLQueryVisitor(); |
30 | 51 | queryStream.append("control: " + query.getProperty().toString()); | 51 | queryStream.append(XMLVisitor.getXMLQueryFor(query.getProperty(), null)); |
31 | 52 | } else if (lens != null && lens.isGame()) { | ||
32 | 53 | queryStream.append("control: " + query.getProperty().toString()); | ||
33 | 52 | } else { | 54 | } else { |
34 | 53 | queryStream.append(query.getProperty().toString()); | 55 | queryStream.append(query.getProperty().toString()); |
35 | 54 | } | 56 | } |
36 | 55 | |||
37 | 56 | |||
38 | 57 | queryStream.close(); | 57 | queryStream.close(); |
39 | 58 | } catch(FileNotFoundException e) { | 58 | } catch(FileNotFoundException e) { |
40 | 59 | System.err.append("An error occurred while exporting the model to verifytapn. Verification cancelled."); | 59 | System.err.append("An error occurred while exporting the model to verifytapn. Verification cancelled."); |
41 | 60 | 60 | ||
42 | === modified file 'src/pipe/gui/Export.java' | |||
43 | --- src/pipe/gui/Export.java 2020-04-18 13:45:34 +0000 | |||
44 | +++ src/pipe/gui/Export.java 2020-12-14 17:15:10 +0000 | |||
45 | @@ -19,7 +19,8 @@ | |||
46 | 19 | import java.io.FileOutputStream; | 19 | import java.io.FileOutputStream; |
47 | 20 | import java.io.IOException; | 20 | import java.io.IOException; |
48 | 21 | import java.io.PrintStream; | 21 | import java.io.PrintStream; |
50 | 22 | import java.util.Iterator; | 22 | import java.lang.reflect.Array; |
51 | 23 | import java.util.*; | ||
52 | 23 | 24 | ||
53 | 24 | import javax.imageio.ImageIO; | 25 | import javax.imageio.ImageIO; |
54 | 25 | import javax.imageio.ImageWriter; | 26 | import javax.imageio.ImageWriter; |
55 | @@ -33,6 +34,13 @@ | |||
56 | 33 | import javax.xml.transform.TransformerConfigurationException; | 34 | import javax.xml.transform.TransformerConfigurationException; |
57 | 34 | import javax.xml.transform.TransformerException; | 35 | import javax.xml.transform.TransformerException; |
58 | 35 | 36 | ||
59 | 37 | import dk.aau.cs.model.tapn.TimedArcPetriNet; | ||
60 | 38 | import dk.aau.cs.util.Tuple; | ||
61 | 39 | import dk.aau.cs.verification.VerifyTAPN.ExportedVerifyTAPNModel; | ||
62 | 40 | import dk.aau.cs.verification.VerifyTAPN.VerifyPNExporter; | ||
63 | 41 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN; | ||
64 | 42 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter; | ||
65 | 43 | import org.jetbrains.annotations.NotNull; | ||
66 | 36 | import org.w3c.dom.DOMException; | 44 | import org.w3c.dom.DOMException; |
67 | 37 | 45 | ||
68 | 38 | import dk.aau.cs.TCTL.visitors.CTLQueryVisitor; | 46 | import dk.aau.cs.TCTL.visitors.CTLQueryVisitor; |
69 | @@ -49,6 +57,7 @@ | |||
70 | 49 | import pipe.dataLayer.NetWriter; | 57 | import pipe.dataLayer.NetWriter; |
71 | 50 | import pipe.dataLayer.TAPNQuery; | 58 | import pipe.dataLayer.TAPNQuery; |
72 | 51 | import pipe.gui.canvas.DrawingSurfaceImpl; | 59 | import pipe.gui.canvas.DrawingSurfaceImpl; |
73 | 60 | import pipe.gui.widgets.QueryDialog; | ||
74 | 52 | import pipe.gui.widgets.filebrowser.FileBrowser; | 61 | import pipe.gui.widgets.filebrowser.FileBrowser; |
75 | 53 | 62 | ||
76 | 54 | /** | 63 | /** |
77 | @@ -58,69 +67,92 @@ | |||
78 | 58 | */ | 67 | */ |
79 | 59 | public class Export { | 68 | public class Export { |
80 | 60 | 69 | ||
144 | 61 | public static final int PNG = 1; | 70 | public static final int PNG = 1; |
145 | 62 | public static final int POSTSCRIPT = 2; | 71 | public static final int POSTSCRIPT = 2; |
146 | 63 | public static final int PRINTER = 3; | 72 | public static final int PRINTER = 3; |
147 | 64 | public static final int TIKZ = 5; | 73 | public static final int TIKZ = 5; |
148 | 65 | public static final int PNML = 6; | 74 | public static final int PNML = 6; |
149 | 66 | public static final int QUERY = 7; | 75 | public static final int QUERY = 7; |
150 | 67 | 76 | ||
151 | 68 | private static void toPnml(DrawingSurfaceImpl g, String filename) | 77 | private static void toPnml(DrawingSurfaceImpl g, String filename) |
152 | 69 | throws NullPointerException, DOMException, TransformerConfigurationException, | 78 | throws NullPointerException, DOMException, TransformerConfigurationException, |
153 | 70 | IOException, ParserConfigurationException, TransformerException { | 79 | IOException, ParserConfigurationException, TransformerException { |
154 | 71 | TabContent currentTab = CreateGui.getCurrentTab(); | 80 | TabContent currentTab = CreateGui.getCurrentTab(); |
155 | 72 | NetworkMarking currentMarking = null; | 81 | NetworkMarking currentMarking = null; |
156 | 73 | if(CreateGui.getCurrentTab().isInAnimationMode()){ | 82 | if (CreateGui.getCurrentTab().isInAnimationMode()) { |
157 | 74 | currentMarking = currentTab.network().marking(); | 83 | currentMarking = currentTab.network().marking(); |
158 | 75 | currentTab.network().setMarking(CreateGui.getAnimator().getInitialMarking()); | 84 | currentTab.network().setMarking(CreateGui.getAnimator().getInitialMarking()); |
159 | 76 | } | 85 | } |
160 | 77 | 86 | ||
161 | 78 | NetWriter tapnWriter = new PNMLWriter( | 87 | NetWriter tapnWriter = new PNMLWriter( |
162 | 79 | currentTab.network(), | 88 | currentTab.network(), |
163 | 80 | currentTab.getGuiModels() | 89 | currentTab.getGuiModels() |
164 | 81 | ); | 90 | ); |
165 | 82 | 91 | ||
166 | 83 | tapnWriter.savePNML(new File(filename)); | 92 | tapnWriter.savePNML(new File(filename)); |
167 | 84 | 93 | ||
168 | 85 | if(CreateGui.getCurrentTab().isInAnimationMode()){ | 94 | if (CreateGui.getCurrentTab().isInAnimationMode()) { |
169 | 86 | currentTab.network().setMarking(currentMarking); | 95 | currentTab.network().setMarking(currentMarking); |
170 | 87 | } | 96 | } |
171 | 88 | } | 97 | } |
172 | 89 | 98 | ||
173 | 90 | private static void toQueryXML(String filename){ | 99 | private static void toQueryXML(String filename) { |
174 | 91 | toQueryXML(CreateGui.getCurrentTab().network(), filename, CreateGui.getCurrentTab().queries()); | 100 | toQueryXML(CreateGui.getCurrentTab().network(), filename, CreateGui.getCurrentTab().queries()); |
175 | 92 | 101 | ||
176 | 93 | } | 102 | } |
177 | 94 | 103 | ||
178 | 95 | public static void toQueryXML(TimedArcPetriNetNetwork network, String filename, Iterable<TAPNQuery> queries){ | 104 | public static void toQueryXML(TimedArcPetriNetNetwork network, String filename, Iterable<TAPNQuery> queries) { |
179 | 96 | try{ | 105 | try { |
180 | 97 | ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), true); | 106 | ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), true); |
181 | 98 | NameMapping mapping = composer.transformModel(network).value2(); | 107 | NameMapping mapping = composer.transformModel(network).value2(); |
182 | 99 | Iterator<TAPNQuery> queryIterator = queries.iterator(); | 108 | Iterator<TAPNQuery> queryIterator = queries.iterator(); |
183 | 100 | PrintStream queryStream = new PrintStream(filename); | 109 | PrintStream queryStream = new PrintStream(filename); |
184 | 101 | CTLQueryVisitor XMLVisitor = new CTLQueryVisitor(); | 110 | CTLQueryVisitor XMLVisitor = new CTLQueryVisitor(); |
185 | 102 | 111 | ||
186 | 103 | while(queryIterator.hasNext()){ | 112 | while (queryIterator.hasNext()) { |
187 | 104 | TAPNQuery clonedQuery = queryIterator.next().copy(); | 113 | TAPNQuery clonedQuery = queryIterator.next().copy(); |
188 | 105 | 114 | ||
189 | 106 | // Attempt to parse and possibly transform the string query using the manual edit parser | 115 | // Attempt to parse and possibly transform the string query using the manual edit parser |
190 | 107 | TCTLAbstractProperty newProperty; | 116 | TCTLAbstractProperty newProperty; |
191 | 108 | try { | 117 | try { |
192 | 109 | newProperty = TAPAALCTLQueryParser.parse(clonedQuery.getProperty().toString()); | 118 | newProperty = TAPAALCTLQueryParser.parse(clonedQuery.getProperty().toString()); |
193 | 110 | } catch (Throwable ex) { | 119 | } catch (Throwable ex) { |
194 | 111 | newProperty = clonedQuery == null ? new TCTLPathPlaceHolder() : clonedQuery.getProperty(); | 120 | newProperty = clonedQuery == null ? new TCTLPathPlaceHolder() : clonedQuery.getProperty(); |
195 | 112 | } | 121 | } |
196 | 113 | newProperty.accept(new RenameAllPlacesVisitor(mapping), null); | 122 | newProperty.accept(new RenameAllPlacesVisitor(mapping), null); |
197 | 114 | newProperty.accept(new RenameAllTransitionsVisitor(mapping), null); | 123 | newProperty.accept(new RenameAllTransitionsVisitor(mapping), null); |
198 | 115 | XMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName()); | 124 | XMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName()); |
199 | 116 | } | 125 | } |
200 | 117 | queryStream.print(XMLVisitor.getFormatted()); | 126 | queryStream.print(XMLVisitor.getFormatted()); |
201 | 118 | 127 | ||
202 | 119 | queryStream.close(); | 128 | queryStream.close(); |
203 | 120 | } catch(FileNotFoundException e) { | 129 | } catch (FileNotFoundException e) { |
204 | 121 | System.err.append("An error occurred while exporting the queries to XML."); | 130 | System.err.append("An error occurred while exporting the queries to XML."); |
205 | 122 | } | 131 | } |
206 | 123 | } | 132 | } |
207 | 133 | |||
208 | 134 | public static void toVerifyTAPN(TimedArcPetriNetNetwork network, Iterable<TAPNQuery> queries, String modelFile, String queryFile, boolean isDTAPN) { | ||
209 | 135 | VerifyTAPNExporter exporter = new VerifyTAPNExporter(); | ||
210 | 136 | |||
211 | 137 | ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false); | ||
212 | 138 | Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(network); | ||
213 | 139 | TimedArcPetriNet model = transformedModel.value1(); | ||
214 | 140 | |||
215 | 141 | TabContent.TAPNLens lens = new TabContent.TAPNLens(!model.isUntimed(), model.hasUncontrollableTransitions()); | ||
216 | 142 | |||
217 | 143 | RenameAllPlacesVisitor visitor = new RenameAllPlacesVisitor(transformedModel.value2()); | ||
218 | 144 | int i = 0; | ||
219 | 145 | for (TAPNQuery query : queries) { | ||
220 | 146 | query.getProperty().accept(visitor, null); | ||
221 | 147 | i++; | ||
222 | 148 | |||
223 | 149 | if (lens.isGame() && isDTAPN) { | ||
224 | 150 | exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), lens); | ||
225 | 151 | } else { | ||
226 | 152 | exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), new TabContent.TAPNLens(true, false)); | ||
227 | 153 | } | ||
228 | 154 | } | ||
229 | 155 | } | ||
230 | 124 | 156 | ||
231 | 125 | public static void toPostScript(Object g, String filename) | 157 | public static void toPostScript(Object g, String filename) |
232 | 126 | throws PrintException, IOException { | 158 | throws PrintException, IOException { |
233 | @@ -187,24 +219,23 @@ | |||
234 | 187 | // dot is for extension | 219 | // dot is for extension |
235 | 188 | filename = filename.substring(0, dotpos + 1); | 220 | filename = filename.substring(0, dotpos + 1); |
236 | 189 | switch (format) { | 221 | switch (format) { |
255 | 190 | case PNG: | 222 | case PNG: |
256 | 191 | filename += "png"; | 223 | filename += "png"; |
257 | 192 | break; | 224 | break; |
258 | 193 | case POSTSCRIPT: | 225 | case POSTSCRIPT: |
259 | 194 | filename += "ps"; | 226 | filename += "ps"; |
260 | 195 | break; | 227 | break; |
261 | 196 | case TIKZ: | 228 | case TIKZ: |
262 | 197 | filename += "tex"; | 229 | filename += "tex"; |
263 | 198 | break; | 230 | break; |
264 | 199 | case PNML: | 231 | case PNML: |
265 | 200 | filename += "pnml"; | 232 | filename += "pnml"; |
266 | 201 | break; | 233 | break; |
267 | 202 | case QUERY: | 234 | case QUERY: |
268 | 203 | filename = filename.substring(0, dotpos); | 235 | filename = filename.substring(0, dotpos); |
269 | 204 | filename += "-queries.xml"; | 236 | filename += "-queries.xml"; |
270 | 205 | break; | 237 | break; |
271 | 206 | } | 238 | } |
254 | 207 | |||
272 | 208 | } | 239 | } |
273 | 209 | } | 240 | } |
274 | 210 | 241 | ||
275 | @@ -266,7 +297,7 @@ | |||
276 | 266 | } | 297 | } |
277 | 267 | break; | 298 | break; |
278 | 268 | } | 299 | } |
280 | 269 | } catch (Exception e) { | 300 | } catch (Exception e) { |
281 | 270 | // There was some problem with the action | 301 | // There was some problem with the action |
282 | 271 | JOptionPane.showMessageDialog(CreateGui.getApp(), | 302 | JOptionPane.showMessageDialog(CreateGui.getApp(), |
283 | 272 | "There were errors performing the requested action:\n" + e, | 303 | "There were errors performing the requested action:\n" + e, |
284 | 273 | 304 | ||
285 | === modified file 'src/pipe/gui/ExportBatchDialog.java' | |||
286 | --- src/pipe/gui/ExportBatchDialog.java 2020-07-20 08:09:36 +0000 | |||
287 | +++ src/pipe/gui/ExportBatchDialog.java 2020-12-14 17:15:10 +0000 | |||
288 | @@ -24,19 +24,7 @@ | |||
289 | 24 | import java.util.Comparator; | 24 | import java.util.Comparator; |
290 | 25 | import java.util.HashMap; | 25 | import java.util.HashMap; |
291 | 26 | import java.util.List; | 26 | import java.util.List; |
305 | 27 | import javax.swing.BorderFactory; | 27 | import javax.swing.*; |
293 | 28 | import javax.swing.DefaultListModel; | ||
294 | 29 | import javax.swing.JButton; | ||
295 | 30 | import javax.swing.JCheckBox; | ||
296 | 31 | import javax.swing.JDialog; | ||
297 | 32 | import javax.swing.JLabel; | ||
298 | 33 | import javax.swing.JList; | ||
299 | 34 | import javax.swing.JPanel; | ||
300 | 35 | import javax.swing.JProgressBar; | ||
301 | 36 | import javax.swing.JScrollPane; | ||
302 | 37 | import javax.swing.JTable; | ||
303 | 38 | import javax.swing.JTextField; | ||
304 | 39 | import javax.swing.ListSelectionModel; | ||
306 | 40 | import javax.swing.border.Border; | 28 | import javax.swing.border.Border; |
307 | 41 | import javax.swing.event.DocumentEvent; | 29 | import javax.swing.event.DocumentEvent; |
308 | 42 | import javax.swing.event.DocumentListener; | 30 | import javax.swing.event.DocumentListener; |
309 | @@ -46,6 +34,7 @@ | |||
310 | 46 | import javax.xml.parsers.ParserConfigurationException; | 34 | import javax.xml.parsers.ParserConfigurationException; |
311 | 47 | import javax.xml.transform.TransformerConfigurationException; | 35 | import javax.xml.transform.TransformerConfigurationException; |
312 | 48 | import javax.xml.transform.TransformerException; | 36 | import javax.xml.transform.TransformerException; |
313 | 37 | |||
314 | 49 | import org.w3c.dom.DOMException; | 38 | import org.w3c.dom.DOMException; |
315 | 50 | import dk.aau.cs.gui.FileNameCellRenderer; | 39 | import dk.aau.cs.gui.FileNameCellRenderer; |
316 | 51 | import dk.aau.cs.gui.components.ExportBatchResultTableModel; | 40 | import dk.aau.cs.gui.components.ExportBatchResultTableModel; |
317 | @@ -55,6 +44,7 @@ | |||
318 | 55 | import dk.aau.cs.model.tapn.TimedArcPetriNet; | 44 | import dk.aau.cs.model.tapn.TimedArcPetriNet; |
319 | 56 | import dk.aau.cs.util.StringComparator; | 45 | import dk.aau.cs.util.StringComparator; |
320 | 57 | import pipe.dataLayer.DataLayer; | 46 | import pipe.dataLayer.DataLayer; |
321 | 47 | import pipe.dataLayer.TAPNQuery; | ||
322 | 58 | import pipe.gui.widgets.filebrowser.FileBrowser; | 48 | import pipe.gui.widgets.filebrowser.FileBrowser; |
323 | 59 | 49 | ||
324 | 60 | public class ExportBatchDialog extends JDialog { | 50 | public class ExportBatchDialog extends JDialog { |
325 | @@ -62,8 +52,9 @@ | |||
326 | 62 | private final static String TOOL_TIP_AddFilesButton = "Press to add nets to batch export"; | 52 | private final static String TOOL_TIP_AddFilesButton = "Press to add nets to batch export"; |
327 | 63 | private final static String TOOL_TIP_RemoveFilesButton = "Press to remove the currently selected nets"; | 53 | private final static String TOOL_TIP_RemoveFilesButton = "Press to remove the currently selected nets"; |
328 | 64 | private final static String TOOL_TIP_ClearFilesButton = "Press to remove all nets from list"; | 54 | private final static String TOOL_TIP_ClearFilesButton = "Press to remove all nets from list"; |
331 | 65 | private final static String TOOL_TIP_ExportFilesButton = "Press to export all nets in PNML and XML format"; | 55 | private final static String TOOL_TIP_ExportFilesButton = "Press to export all nets in the selected format"; |
332 | 66 | private final static String TOOL_TIP_UniqueQueryNamesCheckbox = "Give queries unique names when exporting"; | 56 | private final static String TOOL_TIP_SelectedEngineComboBox = "Select the engine in which the format of the net should be compatible with"; |
333 | 57 | private final static String TOOL_TIP_UniqueQueryNamesCheckbox = "Give queries unique names when exporting"; | ||
334 | 67 | private final static String NAME_SuccesString = "Succeeded"; | 58 | private final static String NAME_SuccesString = "Succeeded"; |
335 | 68 | private final static String NAME_SuccesStringOrphanTransitionsRemoved = "Succeeded, orphan transitions removed"; | 59 | private final static String NAME_SuccesStringOrphanTransitionsRemoved = "Succeeded, orphan transitions removed"; |
336 | 69 | private final static String NAME_FailStringFolderExists = "Failed as the subfolder already exists"; | 60 | private final static String NAME_FailStringFolderExists = "Failed as the subfolder already exists"; |
337 | @@ -83,7 +74,8 @@ | |||
338 | 83 | private final List<File> files = new ArrayList<File>(); | 74 | private final List<File> files = new ArrayList<File>(); |
339 | 84 | private String lastExportPath; | 75 | private String lastExportPath; |
340 | 85 | private String lastSelectPath; | 76 | private String lastSelectPath; |
342 | 86 | private JCheckBox uniqueQueryNames; | 77 | private JCheckBox uniqueQueryNames; |
343 | 78 | private JComboBox selectedEngine; | ||
344 | 87 | private File destinationFile; | 79 | private File destinationFile; |
345 | 88 | private ExportBatchResultTableModel tableModel; | 80 | private ExportBatchResultTableModel tableModel; |
346 | 89 | 81 | ||
347 | @@ -243,14 +235,28 @@ | |||
348 | 243 | enableButtons(); | 235 | enableButtons(); |
349 | 244 | }); | 236 | }); |
350 | 245 | chooserPanel.add(destinationPathSelector, gbc); | 237 | chooserPanel.add(destinationPathSelector, gbc); |
352 | 246 | 238 | ||
353 | 239 | final String[] options = new String[] { | ||
354 | 240 | "PNML and XML queries (verifypn)", | ||
355 | 241 | "Continuous Engine model and queries (verifytapn)", | ||
356 | 242 | "Discrete Engine model and queries (verifydtapn)" | ||
357 | 243 | }; | ||
358 | 244 | selectedEngine = new JComboBox(options); | ||
359 | 245 | selectedEngine.setToolTipText(TOOL_TIP_SelectedEngineComboBox); | ||
360 | 246 | |||
361 | 247 | gbc = new GridBagConstraints(); | ||
362 | 248 | gbc.gridx = 0; | ||
363 | 249 | gbc.gridy = 1; | ||
364 | 250 | gbc.anchor = GridBagConstraints.NORTHWEST; | ||
365 | 251 | gbc.insets = new Insets(10, 0, 0, 0); | ||
366 | 252 | chooserPanel.add(selectedEngine, gbc); | ||
367 | 247 | 253 | ||
368 | 248 | uniqueQueryNames = new JCheckBox("Use unique query names", true); | 254 | uniqueQueryNames = new JCheckBox("Use unique query names", true); |
369 | 249 | uniqueQueryNames.setToolTipText(TOOL_TIP_UniqueQueryNamesCheckbox); | 255 | uniqueQueryNames.setToolTipText(TOOL_TIP_UniqueQueryNamesCheckbox); |
370 | 250 | 256 | ||
371 | 251 | gbc = new GridBagConstraints(); | 257 | gbc = new GridBagConstraints(); |
372 | 252 | gbc.gridx = 0; | 258 | gbc.gridx = 0; |
374 | 253 | gbc.gridy = 1; | 259 | gbc.gridy = 2; |
375 | 254 | gbc.anchor = GridBagConstraints.NORTHWEST; | 260 | gbc.anchor = GridBagConstraints.NORTHWEST; |
376 | 255 | gbc.insets = new Insets(10, 0, 0, 0); | 261 | gbc.insets = new Insets(10, 0, 0, 0); |
377 | 256 | chooserPanel.add(uniqueQueryNames, gbc); | 262 | chooserPanel.add(uniqueQueryNames, gbc); |
378 | @@ -459,7 +465,7 @@ | |||
379 | 459 | } | 465 | } |
380 | 460 | else return; | 466 | else return; |
381 | 461 | } | 467 | } |
383 | 462 | 468 | ||
384 | 463 | private void exportFiles() { | 469 | private void exportFiles() { |
385 | 464 | //loading bar | 470 | //loading bar |
386 | 465 | initProgressBar(); | 471 | initProgressBar(); |
387 | @@ -509,13 +515,27 @@ | |||
388 | 509 | } | 515 | } |
389 | 510 | 516 | ||
390 | 511 | private void exportModel(File file, Path path) throws Exception { | 517 | private void exportModel(File file, Path path) throws Exception { |
398 | 512 | LoadedModel loadedModel = loader.load(file); | 518 | LoadedModel loadedModel = loader.load(file); |
399 | 513 | exportPNML(path, loadedModel); | 519 | Collection<TAPNQuery> queries; |
400 | 514 | if(!uniqueQueryNames.isSelected()) | 520 | |
401 | 515 | Export.toQueryXML(loadedModel.network(), path.toString() + "/query.xml", loadedModel.queries()); | 521 | if (uniqueQueryNames.isSelected()) { |
402 | 516 | else { | 522 | queries = renameQueries(file.getName(), loadedModel.queries()); |
403 | 517 | Export.toQueryXML(loadedModel.network(), path.toString() + "/query.xml", renameQueries(file.getName(), loadedModel.queries())); | 523 | } else { |
404 | 518 | } | 524 | queries = loadedModel.queries(); |
405 | 525 | } | ||
406 | 526 | |||
407 | 527 | switch (selectedEngine.getSelectedIndex()) { | ||
408 | 528 | case 0: | ||
409 | 529 | exportPNML(path, loadedModel); | ||
410 | 530 | Export.toQueryXML(loadedModel.network(), path.toString() + "/query.xml", queries); | ||
411 | 531 | break; | ||
412 | 532 | case 1: | ||
413 | 533 | Export.toVerifyTAPN(loadedModel.network(), queries, path.toString() + "/model.xml", path.toString() + "/query", false); | ||
414 | 534 | break; | ||
415 | 535 | case 2: | ||
416 | 536 | Export.toVerifyTAPN(loadedModel.network(), queries, path.toString() + "/model.xml", path.toString() + "/query", true); | ||
417 | 537 | break; | ||
418 | 538 | } | ||
419 | 519 | } | 539 | } |
420 | 520 | 540 | ||
421 | 521 | private void exportPNML(Path path, LoadedModel loadedModel) throws DOMException, TransformerConfigurationException, IOException, ParserConfigurationException, TransformerException { | 541 | private void exportPNML(Path path, LoadedModel loadedModel) throws DOMException, TransformerConfigurationException, IOException, ParserConfigurationException, TransformerException { |
422 | 522 | 542 | ||
423 | === modified file 'src/pipe/gui/GuiFrame.java' | |||
424 | --- src/pipe/gui/GuiFrame.java 2020-10-30 12:24:35 +0000 | |||
425 | +++ src/pipe/gui/GuiFrame.java 2020-12-14 17:15:10 +0000 | |||
426 | @@ -18,8 +18,10 @@ | |||
427 | 18 | 18 | ||
428 | 19 | import com.sun.jna.Platform; | 19 | import com.sun.jna.Platform; |
429 | 20 | import dk.aau.cs.gui.*; | 20 | import dk.aau.cs.gui.*; |
430 | 21 | import dk.aau.cs.model.tapn.TimedArcPetriNet; | ||
431 | 21 | import dk.aau.cs.util.JavaUtil; | 22 | import dk.aau.cs.util.JavaUtil; |
432 | 22 | import dk.aau.cs.verification.VerifyTAPN.VerifyPN; | 23 | import dk.aau.cs.verification.VerifyTAPN.VerifyPN; |
433 | 24 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter; | ||
434 | 23 | import net.tapaal.Preferences; | 25 | import net.tapaal.Preferences; |
435 | 24 | import net.tapaal.TAPAAL; | 26 | import net.tapaal.TAPAAL; |
436 | 25 | import net.tapaal.helpers.Reference.MutableReference; | 27 | import net.tapaal.helpers.Reference.MutableReference; |
437 | @@ -27,6 +29,7 @@ | |||
438 | 27 | import net.tapaal.swinghelpers.ExtendedJTabbedPane; | 29 | import net.tapaal.swinghelpers.ExtendedJTabbedPane; |
439 | 28 | import net.tapaal.swinghelpers.ToggleButtonWithoutText; | 30 | import net.tapaal.swinghelpers.ToggleButtonWithoutText; |
440 | 29 | import org.jetbrains.annotations.NotNull; | 31 | import org.jetbrains.annotations.NotNull; |
441 | 32 | import pipe.dataLayer.TAPNQuery; | ||
442 | 30 | import pipe.gui.Pipe.ElementType; | 33 | import pipe.gui.Pipe.ElementType; |
443 | 31 | import pipe.gui.action.GuiAction; | 34 | import pipe.gui.action.GuiAction; |
444 | 32 | import pipe.gui.widgets.WorkflowDialog; | 35 | import pipe.gui.widgets.WorkflowDialog; |
445 | @@ -173,7 +176,7 @@ | |||
446 | 173 | currentTab.ifPresent(TabContentActions::importTrace); | 176 | currentTab.ifPresent(TabContentActions::importTrace); |
447 | 174 | } | 177 | } |
448 | 175 | }; | 178 | }; |
450 | 176 | private final GuiAction exportBatchAction = new GuiAction("Batch Export to PNML and XML Queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", KeyStroke.getKeyStroke('D', (shortcutkey + InputEvent.SHIFT_DOWN_MASK))) { | 179 | private final GuiAction exportBatchAction = new GuiAction("Batch Export of model and queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", KeyStroke.getKeyStroke('D', (shortcutkey + InputEvent.SHIFT_DOWN_MASK))) { |
451 | 177 | public void actionPerformed(ActionEvent e) { | 180 | public void actionPerformed(ActionEvent e) { |
452 | 178 | ExportBatchDialog.ShowExportBatchDialog(); | 181 | ExportBatchDialog.ShowExportBatchDialog(); |
453 | 179 | } | 182 | } |
454 | @@ -1380,13 +1383,10 @@ | |||
455 | 1380 | 1383 | ||
456 | 1381 | exportMenu.add(exportPSAction); | 1384 | exportMenu.add(exportPSAction); |
457 | 1382 | 1385 | ||
458 | 1383 | |||
459 | 1384 | exportMenu.add(exportToTikZAction); | 1386 | exportMenu.add(exportToTikZAction); |
460 | 1385 | 1387 | ||
461 | 1386 | |||
462 | 1387 | exportMenu.add(exportToPNMLAction); | 1388 | exportMenu.add(exportToPNMLAction); |
463 | 1388 | 1389 | ||
464 | 1389 | |||
465 | 1390 | exportMenu.add(exportToXMLAction); | 1390 | exportMenu.add(exportToXMLAction); |
466 | 1391 | 1391 | ||
467 | 1392 | exportMenu.add(exportBatchAction); | 1392 | exportMenu.add(exportBatchAction); |
468 | 1393 | 1393 | ||
469 | === modified file 'src/pipe/gui/widgets/QueryDialog.java' | |||
470 | --- src/pipe/gui/widgets/QueryDialog.java 2020-11-06 13:15:11 +0000 | |||
471 | +++ src/pipe/gui/widgets/QueryDialog.java 2020-12-14 17:15:10 +0000 | |||
472 | @@ -3049,10 +3049,10 @@ | |||
473 | 3049 | } | 3049 | } |
474 | 3050 | if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) { | 3050 | if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) { |
475 | 3051 | VerifyTAPNExporter exporter = new VerifyTAPNExporter(); | 3051 | VerifyTAPNExporter exporter = new VerifyTAPNExporter(); |
477 | 3052 | exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens); | 3052 | exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens); |
478 | 3053 | } else if(reduction == ReductionOption.VerifyPN){ | 3053 | } else if(reduction == ReductionOption.VerifyPN){ |
479 | 3054 | VerifyPNExporter exporter = new VerifyPNExporter(); | 3054 | VerifyPNExporter exporter = new VerifyPNExporter(); |
481 | 3055 | exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens); | 3055 | exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens); |
482 | 3056 | } else { | 3056 | } else { |
483 | 3057 | UppaalExporter exporter = new UppaalExporter(); | 3057 | UppaalExporter exporter = new UppaalExporter(); |
484 | 3058 | try { | 3058 | try { |
485 | 3059 | 3059 | ||
486 | === modified file 'src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java' | |||
487 | --- src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java 2020-05-05 18:15:47 +0000 | |||
488 | +++ src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java 2020-12-14 17:15:10 +0000 | |||
489 | @@ -29,7 +29,7 @@ | |||
490 | 29 | //if(path == null) path = lastPath; | 29 | //if(path == null) path = lastPath; |
491 | 30 | 30 | ||
492 | 31 | this.ext = ext; | 31 | this.ext = ext; |
494 | 32 | this.optionalExt = optionalExt; | 32 | this.optionalExt = optionalExt; |
495 | 33 | //fc.setDirectory(path); | 33 | //fc.setDirectory(path); |
496 | 34 | 34 | ||
497 | 35 | // Setup filter if extension specified | 35 | // Setup filter if extension specified |
I don't seen any major issues, but I added a few code styling comments that could be fixed.