Merge lp:~tapaal-contributor/tapaal/colorTraceFix into lp:~tapaal-contributor/tapaal/cpn-gui-dev
- colorTraceFix
- Merge into cpn-gui-dev
Proposed by
Kenneth Yrke Jørgensen
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 1568 |
Merged at revision: | 1570 |
Proposed branch: | lp:~tapaal-contributor/tapaal/colorTraceFix |
Merge into: | lp:~tapaal-contributor/tapaal/cpn-gui-dev |
Diff against target: |
271 lines (+97/-77) 3 files modified
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java (+30/-24) src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+45/-49) src/net/tapaal/gui/petrinet/verification/RunVerification.java (+22/-4) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/colorTraceFix |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+414856@code.launchpad.net |
Commit message
Description of the change
To post a comment you must log in.
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote : | # |
Revision history for this message
Jiri Srba (srba) : | # |
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/verification/VerifyTAPN/VerifyDTAPN.java' |
2 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-01-28 09:46:10 +0000 |
3 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java 2022-02-01 10:04:11 +0000 |
4 | @@ -5,14 +5,33 @@ |
5 | import dk.aau.cs.TCTL.TCTLAGNode; |
6 | import dk.aau.cs.TCTL.TCTLEFNode; |
7 | import dk.aau.cs.TCTL.TCTLEGNode; |
8 | -import pipe.gui.petrinet.PetriNetTab; |
9 | import dk.aau.cs.io.LoadedModel; |
10 | import dk.aau.cs.io.TapnEngineXmlLoader; |
11 | -import dk.aau.cs.model.tapn.*; |
12 | +import dk.aau.cs.model.tapn.LocalTimedPlace; |
13 | +import dk.aau.cs.model.tapn.TAPNQuery; |
14 | +import dk.aau.cs.model.tapn.TimedArcPetriNet; |
15 | +import dk.aau.cs.model.tapn.TimedPlace; |
16 | import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace; |
17 | -import dk.aau.cs.util.*; |
18 | +import dk.aau.cs.util.FormatException; |
19 | +import dk.aau.cs.util.Tuple; |
20 | +import dk.aau.cs.util.UnsupportedModelException; |
21 | +import dk.aau.cs.util.UnsupportedQueryException; |
22 | import dk.aau.cs.verification.*; |
23 | +import net.tapaal.Preferences; |
24 | +import net.tapaal.TAPAAL; |
25 | +import net.tapaal.gui.petrinet.verification.InclusionPlaces; |
26 | +import net.tapaal.gui.petrinet.verification.InclusionPlaces.InclusionPlacesOption; |
27 | +import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; |
28 | +import net.tapaal.gui.petrinet.verification.TAPNQuery.WorkflowMode; |
29 | +import net.tapaal.gui.petrinet.verification.UnfoldNet; |
30 | +import pipe.gui.Constants; |
31 | +import pipe.gui.FileFinder; |
32 | +import pipe.gui.MessengerImpl; |
33 | +import pipe.gui.TAPAALGUI; |
34 | +import pipe.gui.petrinet.PetriNetTab; |
35 | +import pipe.gui.petrinet.dataLayer.DataLayer; |
36 | |
37 | +import javax.swing.*; |
38 | import java.io.BufferedReader; |
39 | import java.io.File; |
40 | import java.io.IOException; |
41 | @@ -20,18 +39,6 @@ |
42 | import java.util.ArrayList; |
43 | import java.util.List; |
44 | |
45 | -import net.tapaal.Preferences; |
46 | -import net.tapaal.TAPAAL; |
47 | -import pipe.gui.petrinet.dataLayer.DataLayer; |
48 | -import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; |
49 | -import net.tapaal.gui.petrinet.verification.TAPNQuery.WorkflowMode; |
50 | -import pipe.gui.*; |
51 | -import net.tapaal.gui.petrinet.verification.UnfoldNet; |
52 | -import net.tapaal.gui.petrinet.verification.InclusionPlaces; |
53 | -import net.tapaal.gui.petrinet.verification.InclusionPlaces.InclusionPlacesOption; |
54 | - |
55 | -import javax.swing.*; |
56 | - |
57 | public class VerifyDTAPN implements ModelChecker{ |
58 | |
59 | private static final String NEED_TO_LOCATE_VERIFYDTAPN_MSG = "TAPAAL needs to know the location of the file verifydtapn.\n\n" |
60 | @@ -274,9 +281,13 @@ |
61 | |
62 | TimedArcPetriNetTrace tapnTrace = null; |
63 | |
64 | - |
65 | boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored()); |
66 | - if(options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) { |
67 | + boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) || |
68 | + (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) || |
69 | + (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) || |
70 | + (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied())); |
71 | + |
72 | + if(options.traceOption() != TraceOption.NONE && isColored && showTrace) { |
73 | TapnEngineXmlLoader tapnLoader = new TapnEngineXmlLoader(); |
74 | File fileOut = new File(options.unfoldedModelPath()); |
75 | File queriesOut = new File(options.unfoldedQueriesPath()); |
76 | @@ -291,11 +302,7 @@ |
77 | tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1()); |
78 | } |
79 | |
80 | - if(tapnTrace == null){ |
81 | - String message = "No trace could be generated.\n\n"; |
82 | - message += "Model checker output:\n" + standardOutput; |
83 | - messenger.displayWrappedErrorMessage(message,"No trace found"); |
84 | - } else { |
85 | + if (tapnTrace != null) { |
86 | int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION); |
87 | if (dialogResult == JOptionPane.OK_OPTION) { |
88 | newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false)); |
89 | @@ -312,6 +319,7 @@ |
90 | options.setTraceOption(TraceOption.NONE); |
91 | } |
92 | } |
93 | + |
94 | } catch (FormatException e) { |
95 | e.printStackTrace(); |
96 | return null; |
97 | @@ -352,8 +360,6 @@ |
98 | (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) || |
99 | (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) { |
100 | return null; |
101 | - } else { |
102 | - messenger.displayErrorMessage("Verifydtapn cannot generate the requested trace for the model. Try another trace option."); |
103 | } |
104 | } |
105 | } |
106 | |
107 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java' |
108 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2022-01-28 12:27:29 +0000 |
109 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2022-02-01 10:04:11 +0000 |
110 | @@ -287,48 +287,54 @@ |
111 | |
112 | Tuple<QueryResult, Stats> queryResult = parseQueryResult(standardOutput, model.value1().marking().size() + query.getExtraTokens(), query.getExtraTokens(), query); |
113 | |
114 | - boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored()); |
115 | - if (options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) { |
116 | - PNMLoader tapnLoader = new PNMLoader(); |
117 | - File fileOut = new File(options.unfoldedModelPath()); |
118 | - File queriesOut = new File(options.unfoldedQueriesPath()); |
119 | - PetriNetTab newTab; |
120 | - LoadedModel loadedModel = null; |
121 | - try { |
122 | - loadedModel = tapnLoader.load(fileOut); |
123 | - TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true); |
124 | - model = newComposer.transformModel(loadedModel.network()); |
125 | - |
126 | - if (queryResult != null && queryResult.value1() != null) { |
127 | - tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1(), true); |
128 | - } |
129 | - |
130 | - if (!(tapnTrace == null)) { |
131 | - int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION); |
132 | - if (dialogResult == JOptionPane.OK_OPTION) { |
133 | - newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false)); |
134 | - |
135 | - //The query being verified should be the only query |
136 | - for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) { |
137 | - newTab.setInitialName(loadedQuery.getName() + " - unfolded"); |
138 | - loadedQuery.copyOptions(dataLayerQuery); |
139 | - newTab.addQuery(loadedQuery); |
140 | - } |
141 | - TAPAALGUI.openNewTabFromStream(newTab); |
142 | - } else { |
143 | - options.setTraceOption(TraceOption.NONE); |
144 | - } |
145 | - } |
146 | - } catch (FormatException e) { |
147 | - e.printStackTrace(); |
148 | - } catch (ThreadDeath d) { |
149 | - return null; |
150 | - } |
151 | - } |
152 | - |
153 | if (queryResult == null || queryResult.value1() == null) { |
154 | return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime()); |
155 | } else { |
156 | + |
157 | + boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored()); |
158 | + boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) || |
159 | + (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) || |
160 | + (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) || |
161 | + (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied())); |
162 | + |
163 | + if (options.traceOption() != TraceOption.NONE && isColored && showTrace) { |
164 | + PNMLoader tapnLoader = new PNMLoader(); |
165 | + File fileOut = new File(options.unfoldedModelPath()); |
166 | + File queriesOut = new File(options.unfoldedQueriesPath()); |
167 | + PetriNetTab newTab; |
168 | + LoadedModel loadedModel = null; |
169 | + try { |
170 | + loadedModel = tapnLoader.load(fileOut); |
171 | + TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true); |
172 | + model = newComposer.transformModel(loadedModel.network()); |
173 | + |
174 | + if (queryResult != null && queryResult.value1() != null) { |
175 | + tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1()); |
176 | + } |
177 | + |
178 | + if (!(tapnTrace == null)) { |
179 | + int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION); |
180 | + if (dialogResult == JOptionPane.OK_OPTION) { |
181 | + newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false)); |
182 | + |
183 | + //The query being verified should be the only query |
184 | + for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) { |
185 | + newTab.setInitialName(loadedQuery.getName() + " - unfolded"); |
186 | + loadedQuery.copyOptions(dataLayerQuery); |
187 | + newTab.addQuery(loadedQuery); |
188 | + } |
189 | + TAPAALGUI.openNewTabFromStream(newTab); |
190 | + } else { |
191 | + options.setTraceOption(TraceOption.NONE); |
192 | + } |
193 | + } |
194 | + } catch (FormatException e) { |
195 | + e.printStackTrace(); |
196 | + } catch (ThreadDeath d) { |
197 | + return null; |
198 | + } |
199 | + } |
200 | + |
201 | ctlOutput = queryResult.value1().isCTL; |
202 | boolean approximationResult = queryResult.value2().discoveredStates() == 0; // Result is from over-approximation |
203 | |
204 | @@ -348,11 +354,6 @@ |
205 | } |
206 | |
207 | private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult) { |
208 | - return parseTrace(output, options, model, exportedModel, query, queryResult, false); |
209 | - } |
210 | - //XXX: this noWarning thinks is a huge hack to avoid warning shown twice for color nets, the warning should not be shown |
211 | - // in this methods in the first case |
212 | - private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult, boolean noWarning) { |
213 | if (((VerifyTAPNOptions) options).trace() == TraceOption.NONE) return null; |
214 | |
215 | VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1()); |
216 | @@ -367,11 +368,6 @@ |
217 | (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) || |
218 | (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) { |
219 | return null; |
220 | - } else { |
221 | - if (!noWarning) { |
222 | - String message = "No trace could be generated.\n\n"; |
223 | - messenger.displayWrappedErrorMessage(message, "No trace found"); |
224 | - } |
225 | } |
226 | } |
227 | } |
228 | |
229 | === modified file 'src/net/tapaal/gui/petrinet/verification/RunVerification.java' |
230 | --- src/net/tapaal/gui/petrinet/verification/RunVerification.java 2022-01-09 19:10:28 +0000 |
231 | +++ src/net/tapaal/gui/petrinet/verification/RunVerification.java 2022-02-01 10:04:11 +0000 |
232 | @@ -19,6 +19,11 @@ |
233 | import javax.swing.table.DefaultTableModel; |
234 | import javax.swing.table.TableModel; |
235 | import javax.swing.table.TableRowSorter; |
236 | + |
237 | +import dk.aau.cs.TCTL.TCTLAFNode; |
238 | +import dk.aau.cs.TCTL.TCTLAGNode; |
239 | +import dk.aau.cs.TCTL.TCTLEFNode; |
240 | +import dk.aau.cs.TCTL.TCTLEGNode; |
241 | import pipe.gui.petrinet.PetriNetTab; |
242 | import dk.aau.cs.Messenger; |
243 | import dk.aau.cs.model.tapn.TimedArcPetriNet; |
244 | @@ -76,10 +81,23 @@ |
245 | JOptionPane.INFORMATION_MESSAGE, |
246 | iconSelector.getIconFor(result) |
247 | ); |
248 | - |
249 | - if (!reducedNetOpened && result.getTrace() != null) { |
250 | - TAPAALGUI.getAnimator().setTrace(result.getTrace()); |
251 | - } |
252 | + |
253 | + if (options.traceOption() != TAPNQuery.TraceOption.NONE && |
254 | + ((query.getProperty() instanceof TCTLEFNode && result.isQuerySatisfied()) || |
255 | + (query.getProperty() instanceof TCTLAGNode && !result.isQuerySatisfied()) || |
256 | + (query.getProperty() instanceof TCTLEGNode && result.isQuerySatisfied()) || |
257 | + (query.getProperty() instanceof TCTLAFNode && !result.isQuerySatisfied()))) { |
258 | + // We have a trace to show) |
259 | + |
260 | + if (!reducedNetOpened && result.getTrace() != null) { |
261 | + TAPAALGUI.getAnimator().setTrace(result.getTrace()); |
262 | + } else { |
263 | + String message = "A trace exists but could not be generated by the engine.\n\n"; |
264 | + messenger.displayWrappedErrorMessage(message, "No trace generated"); |
265 | + } |
266 | + } |
267 | + |
268 | + |
269 | } |
270 | } else { |
271 | //Check if the is something like |
Use with the new version of verifypn to avoid issue where the opend tab does not have a name.