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

Proposed by Lena Said
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.
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
1=== modified file 'src/dk/aau/cs/approximation/ApproximationWorker.java'
2--- src/dk/aau/cs/approximation/ApproximationWorker.java 2020-03-26 12:31:31 +0000
3+++ src/dk/aau/cs/approximation/ApproximationWorker.java 2020-12-16 21:23:18 +0000
4@@ -308,7 +308,8 @@
5 decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
6 result.verificationTime(),
7 result.stats(),
8- result.isSolvedUsingStateEquation());
9+ result.isSolvedUsingStateEquation(),
10+ result.getRawOutput());
11 toReturn.setNameMapping(transformedModel.value2());
12 }
13
14@@ -468,7 +469,6 @@
15 verificationResult.stats(),
16 verificationResult.isSolvedUsingStateEquation());
17 value.setNameMapping(composedModel.value2());
18-
19 }
20 }
21 }
22
23=== modified file 'src/dk/aau/cs/verification/ModelChecker.java'
24--- src/dk/aau/cs/verification/ModelChecker.java 2020-05-25 08:40:31 +0000
25+++ src/dk/aau/cs/verification/ModelChecker.java 2020-12-16 21:23:18 +0000
26@@ -26,4 +26,5 @@
27 boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options);
28
29 String[] getStatsExplanations();
30+
31 }
32
33=== modified file 'src/dk/aau/cs/verification/UPPAAL/Verifyta.java'
34--- src/dk/aau/cs/verification/UPPAAL/Verifyta.java 2020-05-25 08:40:31 +0000
35+++ src/dk/aau/cs/verification/UPPAAL/Verifyta.java 2020-12-16 21:23:18 +0000
36@@ -340,7 +340,7 @@
37 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
38 } else {
39 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult);
40- return new VerificationResult<TimedArcPetriNetTrace>(queryResult, tapnTrace, runner.getRunningTime());
41+ return new VerificationResult<TimedArcPetriNetTrace>(queryResult, tapnTrace, runner.getRunningTime(), standardOutput);
42 }
43 }
44 }
45
46=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
47--- src/dk/aau/cs/verification/VerificationResult.java 2020-07-22 09:47:17 +0000
48+++ src/dk/aau/cs/verification/VerificationResult.java 2020-12-16 21:23:18 +0000
49@@ -15,6 +15,7 @@
50 private QueryResult queryResult;
51 private TTrace trace;
52 private String errorMessage = null;
53+ private String rawOutput = null;
54 private long verificationTime = 0;
55 private Stats stats;
56 private NameMapping nameMapping;
57@@ -25,20 +26,26 @@
58 return queryResult.isQuerySatisfied();
59 }
60
61- public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats){
62+ public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, String rawOutput){
63 this.queryResult = queryResult;
64 this.trace = trace;
65 this.verificationTime = verificationTime;
66 this.stats = stats;
67+ this.rawOutput = rawOutput;
68 }
69+
70+ public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
71+ this(queryResult, trace, verificationTime, stats, null);
72+ this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
73+ }
74
75- public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
76- this(queryResult, trace, verificationTime, stats);
77+ public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation, String rawOutput){
78+ this(queryResult, trace, verificationTime, stats, rawOutput);
79 this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
80 }
81
82- public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime) {
83- this(queryResult, trace, verificationTime, new NullStats());
84+ public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, String rawOutput) {
85+ this(queryResult, trace, verificationTime, new NullStats(), rawOutput);
86 }
87
88 public VerificationResult(String outputMessage, long verificationTime) {
89@@ -51,10 +58,19 @@
90 TTrace secondaryTrace2, long runningTime,
91 Stats value2,
92 boolean isSolvedUsingStateEquation) {
93- this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation);
94+ this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation, null);
95 this.secondaryTrace = secondaryTrace2;
96 }
97
98+ public VerificationResult(QueryResult value1,
99+ TTrace tapnTrace,
100+ TTrace secondaryTrace2, long runningTime,
101+ Stats value2,
102+ boolean isSolvedUsingStateEquation, String rawOutput) {
103+ this(value1, tapnTrace, runningTime, value2, isSolvedUsingStateEquation, rawOutput);
104+ this.secondaryTrace = secondaryTrace2;
105+ }
106+
107 public NameMapping getNameMapping() {
108 return nameMapping;
109 }
110@@ -206,4 +222,8 @@
111 buffer.append(stats.getEdges());
112 return buffer.toString();
113 }
114+
115+ public String getRawOutput() {
116+ return rawOutput;
117+ }
118 }
119
120=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
121--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2020-08-07 11:05:29 +0000
122+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2020-12-16 21:23:18 +0000
123@@ -333,7 +333,7 @@
124 ctlOutput = queryResult.value1().isCTL;
125 boolean approximationResult = queryResult.value2().discoveredStates() == 0; // Result is from over-approximation
126 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
127- return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult);
128+ return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput);
129 }
130 }
131 }
132
133=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
134--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2020-08-06 13:48:04 +0000
135+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2020-12-16 21:23:18 +0000
136@@ -318,7 +318,7 @@
137 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
138 } else {
139 TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
140- return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2());
141+ return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), standardOutput);
142 }
143 }
144 }
145
146=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
147--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-09-27 13:29:09 +0000
148+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-12-16 21:23:18 +0000
149@@ -340,7 +340,7 @@
150 }
151
152 TimedArcPetriNetTrace tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
153- return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false);
154+ return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, secondaryTrace, runner.getRunningTime(), queryResult.value2(), false, standardOutput);
155 }
156 }
157 }
158
159=== modified file 'src/pipe/gui/RunVerification.java'
160--- src/pipe/gui/RunVerification.java 2020-07-20 07:19:51 +0000
161+++ src/pipe/gui/RunVerification.java 2020-12-16 21:23:18 +0000
162@@ -11,13 +11,7 @@
163 import java.util.Comparator;
164 import java.util.List;
165
166-import javax.swing.JButton;
167-import javax.swing.JLabel;
168-import javax.swing.JOptionPane;
169-import javax.swing.JPanel;
170-import javax.swing.JScrollPane;
171-import javax.swing.JTable;
172-import javax.swing.SwingUtilities;
173+import javax.swing.*;
174 import javax.swing.table.DefaultTableModel;
175 import javax.swing.table.TableModel;
176 import javax.swing.table.TableRowSorter;
177@@ -220,6 +214,43 @@
178 return fullPanel;
179 }
180
181+ private JPanel createRawQueryPanel(final String rawOutput) {
182+ final JPanel fullPanel = new JPanel(new GridBagLayout());
183+
184+ JTextArea rawQueryLabel = new JTextArea(rawOutput);
185+ rawQueryLabel.setEditable(false); // set textArea non-editable
186+ JScrollPane scroll = new JScrollPane(rawQueryLabel);
187+ scroll.setHorizontalScrollBarPolicy(ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS);
188+ scroll.setPreferredSize(new Dimension(640,400));
189+
190+ GridBagConstraints gbc = new GridBagConstraints();
191+ gbc.fill = GridBagConstraints.HORIZONTAL;
192+ gbc.weightx = 0;
193+ gbc.weighty = 0;
194+ gbc.gridx = 0;
195+ gbc.gridy = 0;
196+ gbc.anchor = GridBagConstraints.WEST;
197+ fullPanel.add(scroll, gbc);
198+
199+ // Make window resizeable
200+ fullPanel.addHierarchyListener(new HierarchyListener() {
201+ public void hierarchyChanged(HierarchyEvent e) {
202+ //when the hierarchy changes get the ancestor for the message
203+ Window window = SwingUtilities.getWindowAncestor(fullPanel);
204+ //check to see if the ancestor is an instance of Dialog and isn't resizable
205+ if (window instanceof Dialog) {
206+ Dialog dialog = (Dialog) window;
207+ if (!dialog.isResizable()) {
208+ //set resizable to true
209+ dialog.setResizable(true);
210+ }
211+ }
212+ }
213+ });
214+
215+ return fullPanel;
216+ }
217+
218 private Object[][] extractArrayFromTransitionStatistics(final VerificationResult<TAPNNetworkTrace> result) {
219 List<Tuple<String, Integer>> transistionStats = result.getTransitionStatistics();
220 Object[][] out = new Object[transistionStats.size()][2];
221@@ -283,11 +314,23 @@
222 JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));
223 gbc = new GridBagConstraints();
224 gbc.gridx = 0;
225- gbc.gridy = 5;
226+ gbc.gridy = 6;
227 gbc.insets = new Insets(0,0,20,-90);
228 gbc.anchor = GridBagConstraints.WEST;
229 panel.add(reductionStatsLabet, gbc);
230 }
231+ if (result.getRawOutput() != null) {
232+ JButton showRawQueryButton = new JButton("Show raw query results");
233+ showRawQueryButton.addActionListener(arg0 -> {
234+ JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);
235+ });
236+ gbc = new GridBagConstraints();
237+ gbc.gridx = 0;
238+ gbc.gridy = 5;
239+ gbc.insets = new Insets(10,0,10,0);
240+ gbc.anchor = GridBagConstraints.WEST;
241+ panel.add(showRawQueryButton, gbc);
242+ }
243 } else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){
244 displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations());
245
246@@ -296,7 +339,7 @@
247 if(result.isSolvedUsingStateEquation()){
248 gbc = new GridBagConstraints();
249 gbc.gridx = 0;
250- gbc.gridy = 5;
251+ gbc.gridy = 6;
252 gbc.insets = new Insets(0,0,15,0);
253 gbc.anchor = GridBagConstraints.WEST;
254 panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
255@@ -304,14 +347,14 @@
256
257 gbc = new GridBagConstraints();
258 gbc.gridx = 0;
259- gbc.gridy = 6;
260+ gbc.gridy = 7;
261 gbc.gridwidth = 2;
262 gbc.anchor = GridBagConstraints.WEST;
263 panel.add(new JLabel(result.getVerificationTimeString()), gbc);
264
265 gbc = new GridBagConstraints();
266 gbc.gridx = 0;
267- gbc.gridy = 7;
268+ gbc.gridy = 8;
269 gbc.gridwidth = 2;
270 gbc.anchor = GridBagConstraints.WEST;
271 panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);

Subscribers

People subscribed via source and target branches