TAPAAL

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

  1. raw-query-output
  2. Merge into trunk
Proposed by Lena Ernstsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1115
Merged at revision: 1116
Proposed branch: lp:~tapaal-contributor/tapaal/raw-query-output
Merge into: lp:tapaal
Diff against target: 271 lines (+87/-23)
8 files modified
src/dk/aau/cs/approximation/ApproximationWorker.java (+2/-2)
src/dk/aau/cs/verification/ModelChecker.java (+1/-0)
src/dk/aau/cs/verification/UPPAAL/Verifyta.java (+1/-1)
src/dk/aau/cs/verification/VerificationResult.java (+26/-6)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java (+1/-1)
src/pipe/gui/RunVerification.java (+54/-11)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/raw-query-output
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+395465@code.launchpad.net

Commit message

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

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

Tested and works fine.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== 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 @@
308 decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),308 decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
309 result.verificationTime(),309 result.verificationTime(),
310 result.stats(),310 result.stats(),
311 result.isSolvedUsingStateEquation());311 result.isSolvedUsingStateEquation(),
312 result.getRawOutput());
312 toReturn.setNameMapping(transformedModel.value2());313 toReturn.setNameMapping(transformedModel.value2());
313 }314 }
314 315
@@ -468,7 +469,6 @@
468 verificationResult.stats(),469 verificationResult.stats(),
469 verificationResult.isSolvedUsingStateEquation());470 verificationResult.isSolvedUsingStateEquation());
470 value.setNameMapping(composedModel.value2());471 value.setNameMapping(composedModel.value2());
471
472 }472 }
473 }473 }
474 } 474 }
475475
=== 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 @@
26 boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options);26 boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options);
2727
28 String[] getStatsExplanations();28 String[] getStatsExplanations();
29
29}30}
3031
=== 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 @@
340 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());340 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
341 } else {341 } else {
342 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult);342 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult);
343 return new VerificationResult<TimedArcPetriNetTrace>(queryResult, tapnTrace, runner.getRunningTime());343 return new VerificationResult<TimedArcPetriNetTrace>(queryResult, tapnTrace, runner.getRunningTime(), standardOutput);
344 }344 }
345 }345 }
346 }346 }
347347
=== 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 @@
15 private QueryResult queryResult;15 private QueryResult queryResult;
16 private TTrace trace;16 private TTrace trace;
17 private String errorMessage = null;17 private String errorMessage = null;
18 private String rawOutput = null;
18 private long verificationTime = 0;19 private long verificationTime = 0;
19 private Stats stats;20 private Stats stats;
20 private NameMapping nameMapping;21 private NameMapping nameMapping;
@@ -25,20 +26,26 @@
25 return queryResult.isQuerySatisfied();26 return queryResult.isQuerySatisfied();
26 }27 }
2728
28 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats){29 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, String rawOutput){
29 this.queryResult = queryResult;30 this.queryResult = queryResult;
30 this.trace = trace;31 this.trace = trace;
31 this.verificationTime = verificationTime;32 this.verificationTime = verificationTime;
32 this.stats = stats;33 this.stats = stats;
34 this.rawOutput = rawOutput;
33 }35 }
36
37 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
38 this(queryResult, trace, verificationTime, stats, null);
39 this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
40 }
34 41
35 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){42 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation, String rawOutput){
36 this(queryResult, trace, verificationTime, stats);43 this(queryResult, trace, verificationTime, stats, rawOutput);
37 this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;44 this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
38 }45 }
3946
40 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime) {47 public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, String rawOutput) {
41 this(queryResult, trace, verificationTime, new NullStats());48 this(queryResult, trace, verificationTime, new NullStats(), rawOutput);
42 }49 }
4350
44 public VerificationResult(String outputMessage, long verificationTime) {51 public VerificationResult(String outputMessage, long verificationTime) {
@@ -51,10 +58,19 @@
51 TTrace secondaryTrace2, long runningTime,58 TTrace secondaryTrace2, long runningTime,
52 Stats value2,59 Stats value2,
53 boolean isSolvedUsingStateEquation) {60 boolean isSolvedUsingStateEquation) {
54 this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation);61 this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation, null);
55 this.secondaryTrace = secondaryTrace2;62 this.secondaryTrace = secondaryTrace2;
56 }63 }
5764
65 public VerificationResult(QueryResult value1,
66 TTrace tapnTrace,
67 TTrace secondaryTrace2, long runningTime,
68 Stats value2,
69 boolean isSolvedUsingStateEquation, String rawOutput) {
70 this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation, rawOutput);
71 this.secondaryTrace = secondaryTrace2;
72 }
73
58 public NameMapping getNameMapping() {74 public NameMapping getNameMapping() {
59 return nameMapping;75 return nameMapping;
60 }76 }
@@ -206,4 +222,8 @@
206 buffer.append(stats.getEdges());222 buffer.append(stats.getEdges());
207 return buffer.toString();223 return buffer.toString();
208 }224 }
225
226 public String getRawOutput() {
227 return rawOutput;
228 }
209}229}
210230
=== 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 @@
333 ctlOutput = queryResult.value1().isCTL;333 ctlOutput = queryResult.value1().isCTL;
334 boolean approximationResult = queryResult.value2().discoveredStates() == 0; // Result is from over-approximation334 boolean approximationResult = queryResult.value2().discoveredStates() == 0; // Result is from over-approximation
335 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());335 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
336 return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult);336 return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput);
337 }337 }
338 }338 }
339 }339 }
340340
=== 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 @@
318 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());318 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
319 } else {319 } else {
320 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());320 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
321 return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2()); 321 return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), standardOutput);
322 }322 }
323 }323 }
324 }324 }
325325
=== 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 @@
340 }340 }
341341
342 TimedArcPetriNetTrace tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());342 TimedArcPetriNetTrace tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
343 return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false);343 return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false, standardOutput);
344 }344 }
345 }345 }
346 }346 }
347347
=== 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 @@
11import java.util.Comparator;11import java.util.Comparator;
12import java.util.List;12import java.util.List;
1313
14import javax.swing.JButton;14import javax.swing.*;
15import javax.swing.JLabel;
16import javax.swing.JOptionPane;
17import javax.swing.JPanel;
18import javax.swing.JScrollPane;
19import javax.swing.JTable;
20import javax.swing.SwingUtilities;
21import javax.swing.table.DefaultTableModel;15import javax.swing.table.DefaultTableModel;
22import javax.swing.table.TableModel;16import javax.swing.table.TableModel;
23import javax.swing.table.TableRowSorter;17import javax.swing.table.TableRowSorter;
@@ -220,6 +214,43 @@
220 return fullPanel;214 return fullPanel;
221 }215 }
222216
217 private JPanel createRawQueryPanel(final String rawOutput) {
218 final JPanel fullPanel = new JPanel(new GridBagLayout());
219
220 JTextArea rawQueryLabel = new JTextArea(rawOutput);
221 rawQueryLabel.setEditable(false); // set textArea non-editable
222 JScrollPane scroll = new JScrollPane(rawQueryLabel);
223 scroll.setHorizontalScrollBarPolicy(ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS);
224 scroll.setPreferredSize(new Dimension(640,400));
225
226 GridBagConstraints gbc = new GridBagConstraints();
227 gbc.fill = GridBagConstraints.HORIZONTAL;
228 gbc.weightx = 0;
229 gbc.weighty = 0;
230 gbc.gridx = 0;
231 gbc.gridy = 0;
232 gbc.anchor = GridBagConstraints.WEST;
233 fullPanel.add(scroll, gbc);
234
235 // Make window resizeable
236 fullPanel.addHierarchyListener(new HierarchyListener() {
237 public void hierarchyChanged(HierarchyEvent e) {
238 //when the hierarchy changes get the ancestor for the message
239 Window window = SwingUtilities.getWindowAncestor(fullPanel);
240 //check to see if the ancestor is an instance of Dialog and isn't resizable
241 if (window instanceof Dialog) {
242 Dialog dialog = (Dialog) window;
243 if (!dialog.isResizable()) {
244 //set resizable to true
245 dialog.setResizable(true);
246 }
247 }
248 }
249 });
250
251 return fullPanel;
252 }
253
223 private Object[][] extractArrayFromTransitionStatistics(final VerificationResult<TAPNNetworkTrace> result) {254 private Object[][] extractArrayFromTransitionStatistics(final VerificationResult<TAPNNetworkTrace> result) {
224 List<Tuple<String, Integer>> transistionStats = result.getTransitionStatistics();255 List<Tuple<String, Integer>> transistionStats = result.getTransitionStatistics();
225 Object[][] out = new Object[transistionStats.size()][2];256 Object[][] out = new Object[transistionStats.size()][2];
@@ -283,11 +314,23 @@
283 JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));314 JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));
284 gbc = new GridBagConstraints();315 gbc = new GridBagConstraints();
285 gbc.gridx = 0;316 gbc.gridx = 0;
286 gbc.gridy = 5;317 gbc.gridy = 6;
287 gbc.insets = new Insets(0,0,20,-90);318 gbc.insets = new Insets(0,0,20,-90);
288 gbc.anchor = GridBagConstraints.WEST;319 gbc.anchor = GridBagConstraints.WEST;
289 panel.add(reductionStatsLabet, gbc);320 panel.add(reductionStatsLabet, gbc);
290 }321 }
322 if (result.getRawOutput() != null) {
323 JButton showRawQueryButton = new JButton("Show raw query results");
324 showRawQueryButton.addActionListener(arg0 -> {
325 JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);
326 });
327 gbc = new GridBagConstraints();
328 gbc.gridx = 0;
329 gbc.gridy = 5;
330 gbc.insets = new Insets(10,0,10,0);
331 gbc.anchor = GridBagConstraints.WEST;
332 panel.add(showRawQueryButton, gbc);
333 }
291 } else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){334 } else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){
292 displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations());335 displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations());
293336
@@ -296,7 +339,7 @@
296 if(result.isSolvedUsingStateEquation()){339 if(result.isSolvedUsingStateEquation()){
297 gbc = new GridBagConstraints();340 gbc = new GridBagConstraints();
298 gbc.gridx = 0;341 gbc.gridx = 0;
299 gbc.gridy = 5;342 gbc.gridy = 6;
300 gbc.insets = new Insets(0,0,15,0);343 gbc.insets = new Insets(0,0,15,0);
301 gbc.anchor = GridBagConstraints.WEST;344 gbc.anchor = GridBagConstraints.WEST;
302 panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);345 panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
@@ -304,14 +347,14 @@
304 347
305 gbc = new GridBagConstraints();348 gbc = new GridBagConstraints();
306 gbc.gridx = 0;349 gbc.gridx = 0;
307 gbc.gridy = 6;350 gbc.gridy = 7;
308 gbc.gridwidth = 2;351 gbc.gridwidth = 2;
309 gbc.anchor = GridBagConstraints.WEST;352 gbc.anchor = GridBagConstraints.WEST;
310 panel.add(new JLabel(result.getVerificationTimeString()), gbc);353 panel.add(new JLabel(result.getVerificationTimeString()), gbc);
311 354
312 gbc = new GridBagConstraints();355 gbc = new GridBagConstraints();
313 gbc.gridx = 0;356 gbc.gridx = 0;
314 gbc.gridy = 7;357 gbc.gridy = 8;
315 gbc.gridwidth = 2;358 gbc.gridwidth = 2;
316 gbc.anchor = GridBagConstraints.WEST;359 gbc.anchor = GridBagConstraints.WEST;
317 panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);360 panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);

Subscribers

People subscribed via source and target branches