Merge lp:~tapaal-contributor/tapaal/raw-query-output into lp:tapaal

[Lena Ernstsen]

Added button in "verification result" to display raw query output

[Jiri Srba (srba)]

Tested and works fine.

review: Approve

=== modified file 'src/dk/aau/cs/approximation/ApproximationWorker.java'
--- src/dk/aau/cs/approximation/ApproximationWorker.java	2020-03-26 12:31:31 +0000
+++ src/dk/aau/cs/approximation/ApproximationWorker.java	2020-12-16 21:23:18 +0000
@@ -308,7 +308,8 @@
 					decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
 					result.verificationTime(),
 					result.stats(),
-					result.isSolvedUsingStateEquation());
+					result.isSolvedUsingStateEquation(),
+                    result.getRawOutput());
 			toReturn.setNameMapping(transformedModel.value2());
 		}
 		
@@ -468,7 +469,6 @@
 						verificationResult.stats(),
 						verificationResult.isSolvedUsingStateEquation());
 				    value.setNameMapping(composedModel.value2());
-					
 				}
 	        }
 	    } 

=== modified file 'src/dk/aau/cs/verification/ModelChecker.java'
--- src/dk/aau/cs/verification/ModelChecker.java	2020-05-25 08:40:31 +0000
+++ src/dk/aau/cs/verification/ModelChecker.java	2020-12-16 21:23:18 +0000
@@ -26,4 +26,5 @@
 	boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options);
 
 	String[] getStatsExplanations();
+
 }

=== modified file 'src/dk/aau/cs/verification/UPPAAL/Verifyta.java'
--- src/dk/aau/cs/verification/UPPAAL/Verifyta.java	2020-05-25 08:40:31 +0000
+++ src/dk/aau/cs/verification/UPPAAL/Verifyta.java	2020-12-16 21:23:18 +0000
@@ -340,7 +340,7 @@
 				return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
 			} else {
 				TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult);
-				return new VerificationResult<TimedArcPetriNetTrace>(queryResult, tapnTrace, runner.getRunningTime());
+				return new VerificationResult<TimedArcPetriNetTrace>(queryResult, tapnTrace, runner.getRunningTime(), standardOutput);
 			}
 		}
 	}

=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2020-07-22 09:47:17 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2020-12-16 21:23:18 +0000
@@ -15,6 +15,7 @@
 	private QueryResult queryResult;
 	private TTrace trace;
 	private String errorMessage = null;
+	private String rawOutput = null;
 	private long verificationTime = 0;
 	private Stats stats;
 	private NameMapping nameMapping;
@@ -25,20 +26,26 @@
 		return queryResult.isQuerySatisfied();
 	}
 
-	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats){
+	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, String rawOutput){
 		this.queryResult = queryResult;
 		this.trace = trace;
 		this.verificationTime = verificationTime;
 		this.stats = stats;
+		this.rawOutput = rawOutput;
 	}
+
+    public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
+        this(queryResult, trace, verificationTime, stats, null);
+        this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
+    }
 	
-	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
-		this(queryResult, trace, verificationTime, stats);
+	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation, String rawOutput){
+		this(queryResult, trace, verificationTime, stats, rawOutput);
 		this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
 	}
 
-	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime) {
-		this(queryResult, trace, verificationTime, new NullStats());
+	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, String rawOutput) {
+		this(queryResult, trace, verificationTime, new NullStats(), rawOutput);
 	}
 
 	public VerificationResult(String outputMessage, long verificationTime) {
@@ -51,10 +58,19 @@
 			TTrace secondaryTrace2, long runningTime,
 			Stats value2,
 			boolean isSolvedUsingStateEquation) {
-		this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation);
+		this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation, null);
 		this.secondaryTrace = secondaryTrace2;
 	}
 
+    public VerificationResult(QueryResult value1,
+                              TTrace tapnTrace,
+                              TTrace secondaryTrace2, long runningTime,
+                              Stats value2,
+                              boolean isSolvedUsingStateEquation, String rawOutput) {
+        this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation, rawOutput);
+        this.secondaryTrace = secondaryTrace2;
+    }
+
 	public NameMapping getNameMapping() {
 		return nameMapping;
 	}
@@ -206,4 +222,8 @@
 		buffer.append(stats.getEdges());
 		return buffer.toString();
 	}
+
+	public String getRawOutput() {
+	    return rawOutput;
+    }
 }

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2020-08-07 11:05:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2020-12-16 21:23:18 +0000
@@ -333,7 +333,7 @@
 					ctlOutput = queryResult.value1().isCTL;
 					boolean approximationResult = queryResult.value2().discoveredStates() == 0;	// Result is from over-approximation
 					TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
-					return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult);
+					return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput);
 				}
 			}
 		}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java	2020-08-06 13:48:04 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java	2020-12-16 21:23:18 +0000
@@ -318,7 +318,7 @@
 				return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
 			} else {
 				TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
-				return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2()); 
+				return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), standardOutput);
 			}
 		}
 	}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-09-27 13:29:09 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-12-16 21:23:18 +0000
@@ -340,7 +340,7 @@
 				}
 
 				TimedArcPetriNetTrace tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
-				return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false);
+				return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false, standardOutput);
 			}
 		}
 	}

=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java	2020-07-20 07:19:51 +0000
+++ src/pipe/gui/RunVerification.java	2020-12-16 21:23:18 +0000
@@ -11,13 +11,7 @@
 import java.util.Comparator;
 import java.util.List;
 
-import javax.swing.JButton;
-import javax.swing.JLabel;
-import javax.swing.JOptionPane;
-import javax.swing.JPanel;
-import javax.swing.JScrollPane;
-import javax.swing.JTable;
-import javax.swing.SwingUtilities;
+import javax.swing.*;
 import javax.swing.table.DefaultTableModel;
 import javax.swing.table.TableModel;
 import javax.swing.table.TableRowSorter;
@@ -220,6 +214,43 @@
 		return fullPanel;
 	}
 
+    private JPanel createRawQueryPanel(final String rawOutput) {
+        final JPanel fullPanel = new JPanel(new GridBagLayout());
+
+        JTextArea rawQueryLabel = new JTextArea(rawOutput);
+        rawQueryLabel.setEditable(false); // set textArea non-editable
+        JScrollPane scroll = new JScrollPane(rawQueryLabel);
+        scroll.setHorizontalScrollBarPolicy(ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS);
+        scroll.setPreferredSize(new Dimension(640,400));
+
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.fill = GridBagConstraints.HORIZONTAL;
+        gbc.weightx = 0;
+        gbc.weighty = 0;
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        fullPanel.add(scroll, gbc);
+
+        // Make window resizeable
+        fullPanel.addHierarchyListener(new HierarchyListener() {
+            public void hierarchyChanged(HierarchyEvent e) {
+                //when the hierarchy changes get the ancestor for the message
+                Window window = SwingUtilities.getWindowAncestor(fullPanel);
+                //check to see if the ancestor is an instance of Dialog and isn't resizable
+                if (window instanceof Dialog) {
+                    Dialog dialog = (Dialog) window;
+                    if (!dialog.isResizable()) {
+                        //set resizable to true
+                        dialog.setResizable(true);
+                    }
+                }
+            }
+        });
+
+        return fullPanel;
+    }
+
 	private Object[][] extractArrayFromTransitionStatistics(final VerificationResult<TAPNNetworkTrace> result) {
 		List<Tuple<String, Integer>> transistionStats = result.getTransitionStatistics();
 		Object[][] out = new Object[transistionStats.size()][2];
@@ -283,11 +314,23 @@
 				JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));
 				gbc = new GridBagConstraints();
 				gbc.gridx = 0;
-				gbc.gridy = 5;
+				gbc.gridy = 6;
 				gbc.insets = new Insets(0,0,20,-90);
 				gbc.anchor = GridBagConstraints.WEST;
 				panel.add(reductionStatsLabet, gbc);
 			}
+            if (result.getRawOutput() != null) {
+                JButton showRawQueryButton = new JButton("Show raw query results");
+                showRawQueryButton.addActionListener(arg0 -> {
+                        JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);
+                });
+                gbc = new GridBagConstraints();
+                gbc.gridx = 0;
+                gbc.gridy = 5;
+                gbc.insets = new Insets(10,0,10,0);
+                gbc.anchor = GridBagConstraints.WEST;
+                panel.add(showRawQueryButton, gbc);
+            }
 		} else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){
             displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations());
 
@@ -296,7 +339,7 @@
 		if(result.isSolvedUsingStateEquation()){
 			gbc = new GridBagConstraints();
 			gbc.gridx = 0;
-			gbc.gridy = 5;
+			gbc.gridy = 6;
 			gbc.insets = new Insets(0,0,15,0);
 			gbc.anchor = GridBagConstraints.WEST;
 			panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
@@ -304,14 +347,14 @@
 		
 		gbc = new GridBagConstraints();
 		gbc.gridx = 0;
-		gbc.gridy = 6;
+		gbc.gridy = 7;
 		gbc.gridwidth = 2;
 		gbc.anchor = GridBagConstraints.WEST;
 		panel.add(new JLabel(result.getVerificationTimeString()), gbc);
 		
 		gbc = new GridBagConstraints();
 		gbc.gridx = 0;
-		gbc.gridy = 7;
+		gbc.gridy = 8;
 		gbc.gridwidth = 2;
 		gbc.anchor = GridBagConstraints.WEST;
 		panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);