Merge lp:~tapaal-contributor/tapaal/add-export-options into lp:tapaal

[Lena Ernstsen]

Added different export formats in the batch dialog

Added the options to export to verifyTAPN and verifyDTAPN by selecting the engine in a drop down menu

[Kenneth Yrke Jørgensen (yrke)]

I don't seen any major issues, but I added a few code styling comments that could be fixed.

review: Approve (code)

[Jiri Srba (srba)]

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"

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/add-export-options]

1120. By Lena Ernstsen on 2020-12-14

Fixed names and query files + cleaned up

[Lena Ernstsen (lsaid)]

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

review: Needs Resubmitting

[Jiri Srba (srba)]

Tested and works very well.

review: Approve

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2020-08-06 13:48:04 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2020-12-14 17:15:10 +0000
@@ -30,10 +30,10 @@
 		}
 		
 
-		return export(model, query, modelFile, queryFile, null, lens);
+		return export(model, query, modelFile, queryFile, lens);
 	}
 
-	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, pipe.dataLayer.TAPNQuery dataLayerQuery, TabContent.TAPNLens lens) {
+	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, TabContent.TAPNLens lens) {
 		if (modelFile == null || queryFile == null)
 			return null;
 
@@ -44,16 +44,16 @@
 			modelStream.close();
 
 			PrintStream queryStream = new PrintStream(queryFile);
-			if (query.getCategory() == QueryCategory.CTL){
-			    CTLQueryVisitor XMLVisitor = new CTLQueryVisitor();
-			    queryStream.append(XMLVisitor.getXMLQueryFor(query.getProperty(), null));
-			} else if (lens != null && lens.isGame()) {
-			    queryStream.append("control: " + query.getProperty().toString());
+            if (query == null) {
+                throw new FileNotFoundException(null);
+            } else if (query.getCategory() == QueryCategory.CTL) {
+                CTLQueryVisitor XMLVisitor = new CTLQueryVisitor();
+                queryStream.append(XMLVisitor.getXMLQueryFor(query.getProperty(), null));
+            } else if (lens != null && lens.isGame()) {
+                queryStream.append("control: " + query.getProperty().toString());
             } else {
                 queryStream.append(query.getProperty().toString());
             }
-
-			
 			queryStream.close();
 		} catch(FileNotFoundException e) {
 			System.err.append("An error occurred while exporting the model to verifytapn. Verification cancelled.");
 
=== modified file 'src/pipe/gui/Export.java'
--- src/pipe/gui/Export.java	2020-04-18 13:45:34 +0000
+++ src/pipe/gui/Export.java	2020-12-14 17:15:10 +0000
@@ -19,7 +19,8 @@
 import java.io.FileOutputStream;
 import java.io.IOException;
 import java.io.PrintStream;
-import java.util.Iterator;
+import java.lang.reflect.Array;
+import java.util.*;
 
 import javax.imageio.ImageIO;
 import javax.imageio.ImageWriter;
@@ -33,6 +34,13 @@
 import javax.xml.transform.TransformerConfigurationException;
 import javax.xml.transform.TransformerException;
 
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.util.Tuple;
+import dk.aau.cs.verification.VerifyTAPN.ExportedVerifyTAPNModel;
+import dk.aau.cs.verification.VerifyTAPN.VerifyPNExporter;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter;
+import org.jetbrains.annotations.NotNull;
 import org.w3c.dom.DOMException;
 
 import dk.aau.cs.TCTL.visitors.CTLQueryVisitor;
@@ -49,6 +57,7 @@
 import pipe.dataLayer.NetWriter;
 import pipe.dataLayer.TAPNQuery;
 import pipe.gui.canvas.DrawingSurfaceImpl;
+import pipe.gui.widgets.QueryDialog;
 import pipe.gui.widgets.filebrowser.FileBrowser;
 
 /**
@@ -58,69 +67,92 @@
  */
 public class Export {
 
-	public static final int PNG = 1;
-	public static final int POSTSCRIPT = 2;
-	public static final int PRINTER = 3;
-	public static final int TIKZ = 5;
-	public static final int PNML = 6;
-	public static final int QUERY = 7;	
-
-	private static void toPnml(DrawingSurfaceImpl g, String filename)
-			throws NullPointerException, DOMException, TransformerConfigurationException, 
-			IOException, ParserConfigurationException, TransformerException {
-		TabContent currentTab = CreateGui.getCurrentTab();
-		NetworkMarking currentMarking = null;
-		if(CreateGui.getCurrentTab().isInAnimationMode()){
-			currentMarking = currentTab.network().marking();
-			currentTab.network().setMarking(CreateGui.getAnimator().getInitialMarking());
-		}
-
-		NetWriter tapnWriter = new PNMLWriter(
-				currentTab.network(),
-				currentTab.getGuiModels()
-				);
-
-		tapnWriter.savePNML(new File(filename));
-
-		if(CreateGui.getCurrentTab().isInAnimationMode()){
-			currentTab.network().setMarking(currentMarking);
-		}
-	}
-	
-	private static void toQueryXML(String filename){
-		toQueryXML(CreateGui.getCurrentTab().network(), filename, CreateGui.getCurrentTab().queries());
-		
-	}
-	
-	public static void toQueryXML(TimedArcPetriNetNetwork network, String filename, Iterable<TAPNQuery> queries){
-		try{
-	            ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), true);
-	            NameMapping mapping = composer.transformModel(network).value2();
-	            Iterator<TAPNQuery> queryIterator = queries.iterator();
-	            PrintStream queryStream = new PrintStream(filename);
-	            CTLQueryVisitor XMLVisitor = new CTLQueryVisitor();
-	            
-	            while(queryIterator.hasNext()){
-	                TAPNQuery clonedQuery = queryIterator.next().copy();
-
-                            // Attempt to parse and possibly transform the string query using the manual edit parser
-                            TCTLAbstractProperty newProperty;
-                            try {
-                                newProperty = TAPAALCTLQueryParser.parse(clonedQuery.getProperty().toString());
-                            } catch (Throwable ex) {
-                                newProperty = clonedQuery == null ? new TCTLPathPlaceHolder() : clonedQuery.getProperty();
-                            }
-                            newProperty.accept(new RenameAllPlacesVisitor(mapping), null);
-                            newProperty.accept(new RenameAllTransitionsVisitor(mapping), null);
-                            XMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName());
-	            }
-	            queryStream.print(XMLVisitor.getFormatted());
-				
-				queryStream.close();
-		} catch(FileNotFoundException e) {
-			System.err.append("An error occurred while exporting the queries to XML.");
-		}
-	}
+    public static final int PNG = 1;
+    public static final int POSTSCRIPT = 2;
+    public static final int PRINTER = 3;
+    public static final int TIKZ = 5;
+    public static final int PNML = 6;
+    public static final int QUERY = 7;
+
+    private static void toPnml(DrawingSurfaceImpl g, String filename)
+        throws NullPointerException, DOMException, TransformerConfigurationException,
+        IOException, ParserConfigurationException, TransformerException {
+        TabContent currentTab = CreateGui.getCurrentTab();
+        NetworkMarking currentMarking = null;
+        if (CreateGui.getCurrentTab().isInAnimationMode()) {
+            currentMarking = currentTab.network().marking();
+            currentTab.network().setMarking(CreateGui.getAnimator().getInitialMarking());
+        }
+
+        NetWriter tapnWriter = new PNMLWriter(
+            currentTab.network(),
+            currentTab.getGuiModels()
+        );
+
+        tapnWriter.savePNML(new File(filename));
+
+        if (CreateGui.getCurrentTab().isInAnimationMode()) {
+            currentTab.network().setMarking(currentMarking);
+        }
+    }
+
+    private static void toQueryXML(String filename) {
+        toQueryXML(CreateGui.getCurrentTab().network(), filename, CreateGui.getCurrentTab().queries());
+
+    }
+
+    public static void toQueryXML(TimedArcPetriNetNetwork network, String filename, Iterable<TAPNQuery> queries) {
+        try {
+            ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), true);
+            NameMapping mapping = composer.transformModel(network).value2();
+            Iterator<TAPNQuery> queryIterator = queries.iterator();
+            PrintStream queryStream = new PrintStream(filename);
+            CTLQueryVisitor XMLVisitor = new CTLQueryVisitor();
+
+            while (queryIterator.hasNext()) {
+                TAPNQuery clonedQuery = queryIterator.next().copy();
+
+                // Attempt to parse and possibly transform the string query using the manual edit parser
+                TCTLAbstractProperty newProperty;
+                try {
+                    newProperty = TAPAALCTLQueryParser.parse(clonedQuery.getProperty().toString());
+                } catch (Throwable ex) {
+                    newProperty = clonedQuery == null ? new TCTLPathPlaceHolder() : clonedQuery.getProperty();
+                }
+                newProperty.accept(new RenameAllPlacesVisitor(mapping), null);
+                newProperty.accept(new RenameAllTransitionsVisitor(mapping), null);
+                XMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName());
+            }
+            queryStream.print(XMLVisitor.getFormatted());
+
+            queryStream.close();
+        } catch (FileNotFoundException e) {
+            System.err.append("An error occurred while exporting the queries to XML.");
+        }
+    }
+
+	public static void toVerifyTAPN(TimedArcPetriNetNetwork network, Iterable<TAPNQuery> queries, String modelFile, String queryFile, boolean isDTAPN) {
+        VerifyTAPNExporter exporter = new VerifyTAPNExporter();
+
+        ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false);
+        Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(network);
+        TimedArcPetriNet model = transformedModel.value1();
+
+        TabContent.TAPNLens lens = new TabContent.TAPNLens(!model.isUntimed(), model.hasUncontrollableTransitions());
+
+        RenameAllPlacesVisitor visitor = new RenameAllPlacesVisitor(transformedModel.value2());
+        int i = 0;
+        for (TAPNQuery query : queries) {
+            query.getProperty().accept(visitor, null);
+            i++;
+
+            if (lens.isGame() && isDTAPN) {
+                exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), lens);
+            } else {
+                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));
+            }
+        }
+    }
 
 	public static void toPostScript(Object g, String filename)
 			throws PrintException, IOException {
@@ -187,24 +219,23 @@
 				// dot is for extension
 				filename = filename.substring(0, dotpos + 1);
 				switch (format) {
-				case PNG:
-					filename += "png";
-					break;
-				case POSTSCRIPT:
-					filename += "ps";
-					break;
-				case TIKZ:
-					filename += "tex";
-					break;
-				case PNML:
-					filename += "pnml";
-					break;
-				case QUERY:
-					filename = filename.substring(0, dotpos);
-					filename += "-queries.xml";
-					break;
-				}
-				
+                    case PNG:
+                        filename += "png";
+                        break;
+                    case POSTSCRIPT:
+                        filename += "ps";
+                        break;
+                    case TIKZ:
+                        filename += "tex";
+                        break;
+                    case PNML:
+                        filename += "pnml";
+                        break;
+                    case QUERY:
+                        filename = filename.substring(0, dotpos);
+                        filename += "-queries.xml";
+                        break;
+                }
 			}
 		}
 
@@ -266,7 +297,7 @@
 				}
 				break;
 			}
-		} catch (Exception e) {
+        } catch (Exception e) {
 			// There was some problem with the action
 			JOptionPane.showMessageDialog(CreateGui.getApp(),
 					"There were errors performing the requested action:\n" + e,
 
=== modified file 'src/pipe/gui/ExportBatchDialog.java'
--- src/pipe/gui/ExportBatchDialog.java	2020-07-20 08:09:36 +0000
+++ src/pipe/gui/ExportBatchDialog.java	2020-12-14 17:15:10 +0000
@@ -24,19 +24,7 @@
 import java.util.Comparator;
 import java.util.HashMap;
 import java.util.List;
-import javax.swing.BorderFactory;
-import javax.swing.DefaultListModel;
-import javax.swing.JButton;
-import javax.swing.JCheckBox;
-import javax.swing.JDialog;
-import javax.swing.JLabel;
-import javax.swing.JList;
-import javax.swing.JPanel;
-import javax.swing.JProgressBar;
-import javax.swing.JScrollPane;
-import javax.swing.JTable;
-import javax.swing.JTextField;
-import javax.swing.ListSelectionModel;
+import javax.swing.*;
 import javax.swing.border.Border;
 import javax.swing.event.DocumentEvent;
 import javax.swing.event.DocumentListener;
@@ -46,6 +34,7 @@
 import javax.xml.parsers.ParserConfigurationException;
 import javax.xml.transform.TransformerConfigurationException;
 import javax.xml.transform.TransformerException;
+
 import org.w3c.dom.DOMException;
 import dk.aau.cs.gui.FileNameCellRenderer;
 import dk.aau.cs.gui.components.ExportBatchResultTableModel;
@@ -55,6 +44,7 @@
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.util.StringComparator;
 import pipe.dataLayer.DataLayer;
+import pipe.dataLayer.TAPNQuery;
 import pipe.gui.widgets.filebrowser.FileBrowser;
 
 public class ExportBatchDialog extends JDialog {
@@ -62,8 +52,9 @@
 	private final static String TOOL_TIP_AddFilesButton = "Press to add nets to batch export";
 	private final static String TOOL_TIP_RemoveFilesButton = "Press to remove the currently selected nets";
 	private final static String TOOL_TIP_ClearFilesButton = "Press to remove all nets from list";
-	private final static String TOOL_TIP_ExportFilesButton = "Press to export all nets in PNML and XML format";
-	private final static String TOOL_TIP_UniqueQueryNamesCheckbox = "Give queries unique names when exporting";
+	private final static String TOOL_TIP_ExportFilesButton = "Press to export all nets in the selected format";
+    private final static String TOOL_TIP_SelectedEngineComboBox = "Select the engine in which the format of the net should be compatible with";
+    private final static String TOOL_TIP_UniqueQueryNamesCheckbox = "Give queries unique names when exporting";
 	private final static String NAME_SuccesString = "Succeeded";
 	private final static String NAME_SuccesStringOrphanTransitionsRemoved = "Succeeded, orphan transitions removed";
 	private final static String NAME_FailStringFolderExists = "Failed as the subfolder already exists";
@@ -83,7 +74,8 @@
 	private final List<File> files = new ArrayList<File>();
 	private String lastExportPath;
 	private String lastSelectPath;
-	private JCheckBox uniqueQueryNames;
+    private JCheckBox uniqueQueryNames;
+    private JComboBox selectedEngine;
 	private File destinationFile;
 	private ExportBatchResultTableModel tableModel;
 	
@@ -243,14 +235,28 @@
 			enableButtons();
 		});
 		chooserPanel.add(destinationPathSelector, gbc);
-		
+
+        final String[] options = new String[] {
+            "PNML and XML queries (verifypn)",
+            "Continuous Engine model and queries (verifytapn)",
+            "Discrete Engine model and queries (verifydtapn)"
+        };
+		selectedEngine = new JComboBox(options);
+		selectedEngine.setToolTipText(TOOL_TIP_SelectedEngineComboBox);
+
+        gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 1;
+        gbc.anchor = GridBagConstraints.NORTHWEST;
+        gbc.insets = new Insets(10, 0, 0, 0);
+        chooserPanel.add(selectedEngine, gbc);
 
 		uniqueQueryNames = new JCheckBox("Use unique query names", true);
 		uniqueQueryNames.setToolTipText(TOOL_TIP_UniqueQueryNamesCheckbox);
 		
 		gbc = new GridBagConstraints();
 		gbc.gridx = 0;
-		gbc.gridy = 1;
+		gbc.gridy = 2;
 		gbc.anchor = GridBagConstraints.NORTHWEST;
 		gbc.insets = new Insets(10, 0, 0, 0);
 		chooserPanel.add(uniqueQueryNames, gbc);
@@ -459,7 +465,7 @@
 		}
 		else return;
 	}
-	
+
 	private void exportFiles() {
 		//loading bar
 		initProgressBar();
@@ -509,13 +515,27 @@
 	}
 	
 	private void exportModel(File file, Path path) throws Exception {
-			LoadedModel loadedModel = loader.load(file);
-			exportPNML(path, loadedModel);
-			if(!uniqueQueryNames.isSelected())
-				Export.toQueryXML(loadedModel.network(), path.toString() + "/query.xml", loadedModel.queries());
-			else {
-				Export.toQueryXML(loadedModel.network(), path.toString() + "/query.xml", renameQueries(file.getName(), loadedModel.queries()));
-			}
+        LoadedModel loadedModel = loader.load(file);
+        Collection<TAPNQuery> queries;
+
+        if (uniqueQueryNames.isSelected()) {
+            queries =  renameQueries(file.getName(), loadedModel.queries());
+        } else {
+            queries = loadedModel.queries();
+        }
+
+        switch (selectedEngine.getSelectedIndex()) {
+            case 0:
+                exportPNML(path, loadedModel);
+                Export.toQueryXML(loadedModel.network(), path.toString() + "/query.xml", queries);
+                break;
+            case 1:
+                Export.toVerifyTAPN(loadedModel.network(), queries, path.toString() + "/model.xml", path.toString() + "/query", false);
+                break;
+            case 2:
+                Export.toVerifyTAPN(loadedModel.network(), queries, path.toString() + "/model.xml", path.toString() + "/query", true);
+                break;
+        }
 	}
 	
 	private void exportPNML(Path path, LoadedModel loadedModel) throws DOMException, TransformerConfigurationException, IOException, ParserConfigurationException, TransformerException {
 
=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java	2020-10-30 12:24:35 +0000
+++ src/pipe/gui/GuiFrame.java	2020-12-14 17:15:10 +0000
@@ -18,8 +18,10 @@
 
 import com.sun.jna.Platform;
 import dk.aau.cs.gui.*;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.util.JavaUtil;
 import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter;
 import net.tapaal.Preferences;
 import net.tapaal.TAPAAL;
 import net.tapaal.helpers.Reference.MutableReference;
@@ -27,6 +29,7 @@
 import net.tapaal.swinghelpers.ExtendedJTabbedPane;
 import net.tapaal.swinghelpers.ToggleButtonWithoutText;
 import org.jetbrains.annotations.NotNull;
+import pipe.dataLayer.TAPNQuery;
 import pipe.gui.Pipe.ElementType;
 import pipe.gui.action.GuiAction;
 import pipe.gui.widgets.WorkflowDialog;
@@ -173,7 +176,7 @@
             currentTab.ifPresent(TabContentActions::importTrace);
         }
     };
-    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))) {
+    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))) {
         public void actionPerformed(ActionEvent e) {
             ExportBatchDialog.ShowExportBatchDialog();
         }
@@ -1380,13 +1383,10 @@
 
         exportMenu.add(exportPSAction);
 
-
         exportMenu.add(exportToTikZAction);
 
-
         exportMenu.add(exportToPNMLAction);
 
-
         exportMenu.add(exportToXMLAction);
 
         exportMenu.add(exportBatchAction);
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2020-11-06 13:15:11 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2020-12-14 17:15:10 +0000
@@ -3049,10 +3049,10 @@
                         }
 						if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {
 							VerifyTAPNExporter exporter = new VerifyTAPNExporter();
-							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens);
+							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);
 						} else if(reduction == ReductionOption.VerifyPN){
 							VerifyPNExporter exporter = new VerifyPNExporter();
-							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens);
+							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);
 						} else {
 							UppaalExporter exporter = new UppaalExporter();
 							try {
 
=== modified file 'src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java'
--- src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java	2020-05-05 18:15:47 +0000
+++ src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java	2020-12-14 17:15:10 +0000
@@ -29,7 +29,7 @@
 		//if(path == null) path = lastPath;
 
 		this.ext = ext;
-                this.optionalExt = optionalExt;
+        this.optionalExt = optionalExt;
 		//fc.setDirectory(path);
 
 		// Setup filter if extension specified