Merge lp:~tapaal-contributor/tapaal/colorTraceFix into lp:~tapaal-contributor/tapaal/cpn-gui-dev

[Kenneth Yrke Jørgensen]

[Kenneth Yrke Jørgensen (yrke)]

Use with the new version of verifypn to avoid issue where the opend tab does not have a name.

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java	2022-01-28 09:46:10 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java	2022-02-01 10:04:11 +0000
@@ -5,14 +5,33 @@
 import dk.aau.cs.TCTL.TCTLAGNode;
 import dk.aau.cs.TCTL.TCTLEFNode;
 import dk.aau.cs.TCTL.TCTLEGNode;
-import pipe.gui.petrinet.PetriNetTab;
 import dk.aau.cs.io.LoadedModel;
 import dk.aau.cs.io.TapnEngineXmlLoader;
-import dk.aau.cs.model.tapn.*;
+import dk.aau.cs.model.tapn.LocalTimedPlace;
+import dk.aau.cs.model.tapn.TAPNQuery;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedPlace;
 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
-import dk.aau.cs.util.*;
+import dk.aau.cs.util.FormatException;
+import dk.aau.cs.util.Tuple;
+import dk.aau.cs.util.UnsupportedModelException;
+import dk.aau.cs.util.UnsupportedQueryException;
 import dk.aau.cs.verification.*;
+import net.tapaal.Preferences;
+import net.tapaal.TAPAAL;
+import net.tapaal.gui.petrinet.verification.InclusionPlaces;
+import net.tapaal.gui.petrinet.verification.InclusionPlaces.InclusionPlacesOption;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.WorkflowMode;
+import net.tapaal.gui.petrinet.verification.UnfoldNet;
+import pipe.gui.Constants;
+import pipe.gui.FileFinder;
+import pipe.gui.MessengerImpl;
+import pipe.gui.TAPAALGUI;
+import pipe.gui.petrinet.PetriNetTab;
+import pipe.gui.petrinet.dataLayer.DataLayer;
 
+import javax.swing.*;
 import java.io.BufferedReader;
 import java.io.File;
 import java.io.IOException;
@@ -20,18 +39,6 @@
 import java.util.ArrayList;
 import java.util.List;
 
-import net.tapaal.Preferences;
-import net.tapaal.TAPAAL;
-import pipe.gui.petrinet.dataLayer.DataLayer;
-import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
-import net.tapaal.gui.petrinet.verification.TAPNQuery.WorkflowMode;
-import pipe.gui.*;
-import net.tapaal.gui.petrinet.verification.UnfoldNet;
-import net.tapaal.gui.petrinet.verification.InclusionPlaces;
-import net.tapaal.gui.petrinet.verification.InclusionPlaces.InclusionPlacesOption;
-
-import javax.swing.*;
-
 public class VerifyDTAPN implements ModelChecker{
 
 	private static final String NEED_TO_LOCATE_VERIFYDTAPN_MSG = "TAPAAL needs to know the location of the file verifydtapn.\n\n"
@@ -274,9 +281,13 @@
 
                 TimedArcPetriNetTrace tapnTrace = null;
 
-
                 boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
-                if(options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
+                boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied()));
+
+                if(options.traceOption() != TraceOption.NONE && isColored && showTrace) {
                     TapnEngineXmlLoader tapnLoader = new TapnEngineXmlLoader();
                     File fileOut = new File(options.unfoldedModelPath());
                     File queriesOut = new File(options.unfoldedQueriesPath());
@@ -291,11 +302,7 @@
                             tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
                         }
 
-                        if(tapnTrace == null){
-                            String message = "No trace could be generated.\n\n";
-                            message += "Model checker output:\n" + standardOutput;
-                            messenger.displayWrappedErrorMessage(message,"No trace found");
-                        } else {
+                        if (tapnTrace != null) {
                             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);
                             if (dialogResult == JOptionPane.OK_OPTION) {
                                 newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
@@ -312,6 +319,7 @@
                                 options.setTraceOption(TraceOption.NONE);
                             }
                         }
+
                     } catch (FormatException e) {
                         e.printStackTrace();
                         return null;
@@ -352,8 +360,6 @@
 						(query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) ||
 						(query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) {
 					return null;
-				} else {
-					messenger.displayErrorMessage("Verifydtapn cannot generate the requested trace for the model. Try another trace option.");
 				}
 			}
 		}
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2022-01-28 12:27:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2022-02-01 10:04:11 +0000
@@ -287,48 +287,54 @@
 
             Tuple<QueryResult, Stats> queryResult = parseQueryResult(standardOutput, model.value1().marking().size() + query.getExtraTokens(), query.getExtraTokens(), query);
 
-            boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
-            if (options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
-                PNMLoader tapnLoader = new PNMLoader();
-                File fileOut = new File(options.unfoldedModelPath());
-                File queriesOut = new File(options.unfoldedQueriesPath());
-                PetriNetTab newTab;
-                LoadedModel loadedModel = null;
-                try {
-                    loadedModel = tapnLoader.load(fileOut);
-                    TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true);
-                    model = newComposer.transformModel(loadedModel.network());
-
-                    if (queryResult != null && queryResult.value1() != null) {
-                        tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1(), true);
-                    }
-
-                    if (!(tapnTrace == null)) {
-                        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);
-                        if (dialogResult == JOptionPane.OK_OPTION) {
-                            newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
-
-                            //The query being verified should be the only query
-                            for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) {
-                                newTab.setInitialName(loadedQuery.getName() + " - unfolded");
-                                loadedQuery.copyOptions(dataLayerQuery);
-                                newTab.addQuery(loadedQuery);
-                            }
-                            TAPAALGUI.openNewTabFromStream(newTab);
-                        } else {
-                            options.setTraceOption(TraceOption.NONE);
-                        }
-                    }
-                } catch (FormatException e) {
-                    e.printStackTrace();
-                } catch (ThreadDeath d) {
-                    return null;
-                }
-            }
-
             if (queryResult == null || queryResult.value1() == null) {
                 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
             } else {
+
+                boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
+                boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied()));
+
+                if (options.traceOption() != TraceOption.NONE && isColored && showTrace) {
+                    PNMLoader tapnLoader = new PNMLoader();
+                    File fileOut = new File(options.unfoldedModelPath());
+                    File queriesOut = new File(options.unfoldedQueriesPath());
+                    PetriNetTab newTab;
+                    LoadedModel loadedModel = null;
+                    try {
+                        loadedModel = tapnLoader.load(fileOut);
+                        TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true);
+                        model = newComposer.transformModel(loadedModel.network());
+
+                        if (queryResult != null && queryResult.value1() != null) {
+                            tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
+                        }
+
+                        if (!(tapnTrace == null)) {
+                            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);
+                            if (dialogResult == JOptionPane.OK_OPTION) {
+                                newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
+
+                                //The query being verified should be the only query
+                                for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) {
+                                    newTab.setInitialName(loadedQuery.getName() + " - unfolded");
+                                    loadedQuery.copyOptions(dataLayerQuery);
+                                    newTab.addQuery(loadedQuery);
+                                }
+                                TAPAALGUI.openNewTabFromStream(newTab);
+                            } else {
+                                options.setTraceOption(TraceOption.NONE);
+                            }
+                        }
+                    } catch (FormatException e) {
+                        e.printStackTrace();
+                    } catch (ThreadDeath d) {
+                        return null;
+                    }
+                }
+
                 ctlOutput = queryResult.value1().isCTL;
                 boolean approximationResult = queryResult.value2().discoveredStates() == 0;    // Result is from over-approximation
 
@@ -348,11 +354,6 @@
     }
 
     private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult) {
-        return parseTrace(output, options, model, exportedModel, query, queryResult, false);
-    }
-    //XXX: this noWarning thinks is a huge hack to avoid warning shown twice for color nets, the warning should not be shown
-    // in this methods in the first case
-    private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult, boolean noWarning) {
         if (((VerifyTAPNOptions) options).trace() == TraceOption.NONE) return null;
 
         VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1());
@@ -367,11 +368,6 @@
                     (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) ||
                     (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) {
                     return null;
-                } else {
-                    if (!noWarning) {
-                        String message = "No trace could be generated.\n\n";
-                        messenger.displayWrappedErrorMessage(message, "No trace found");
-                    }
                 }
             }
         }
 
=== modified file 'src/net/tapaal/gui/petrinet/verification/RunVerification.java'
--- src/net/tapaal/gui/petrinet/verification/RunVerification.java	2022-01-09 19:10:28 +0000
+++ src/net/tapaal/gui/petrinet/verification/RunVerification.java	2022-02-01 10:04:11 +0000
@@ -19,6 +19,11 @@
 import javax.swing.table.DefaultTableModel;
 import javax.swing.table.TableModel;
 import javax.swing.table.TableRowSorter;
+
+import dk.aau.cs.TCTL.TCTLAFNode;
+import dk.aau.cs.TCTL.TCTLAGNode;
+import dk.aau.cs.TCTL.TCTLEFNode;
+import dk.aau.cs.TCTL.TCTLEGNode;
 import pipe.gui.petrinet.PetriNetTab;
 import dk.aau.cs.Messenger;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
@@ -76,10 +81,23 @@
 						JOptionPane.INFORMATION_MESSAGE,
 						iconSelector.getIconFor(result)
 				);
-	
-				if (!reducedNetOpened && result.getTrace() != null) {
-					TAPAALGUI.getAnimator().setTrace(result.getTrace());
-				}
+
+                if (options.traceOption() != TAPNQuery.TraceOption.NONE &&
+                    ((query.getProperty() instanceof TCTLEFNode && result.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !result.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && result.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !result.isQuerySatisfied()))) {
+                    // We have a trace to show)
+
+                    if (!reducedNetOpened && result.getTrace() != null) {
+                        TAPAALGUI.getAnimator().setTrace(result.getTrace());
+                    } else {
+                        String message = "A trace exists but could not be generated by the engine.\n\n";
+                        messenger.displayWrappedErrorMessage(message, "No trace generated");
+                    }
+                }
+
+
 			}
 		} else {
 			//Check if the is something like