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

[Kenneth Yrke Jørgensen]

[Kenneth Yrke Jørgensen (yrke)]

Made the following changes:

Renamed untimed state equation to preproces using skeleton analysis, and result is displayed independently from general state equation.

Not will report the solution method (if output by engine)
  - query reduction
  - TAR

[lp:~tapaal-contributor/tapaal/cpn-solvedBy]

1575. By Kenneth Yrke Jørgensen on 2022-02-07

Fixed placement of show raw query btn and fixed detection of solved siphon-trap.

Also removed old solved by state-equation (covered by query simplification)

1576. By Kenneth Yrke Jørgensen on 2022-02-08

Updated skeleton analysis text

[Jiri Srba (srba)]

review: Approve

[lp:~tapaal-contributor/tapaal/cpn-solvedBy]

1577. By Kenneth Yrke Jørgensen on 2022-02-08

Merged cpn branch into solvedBy

=== modified file 'src/dk/aau/cs/approximation/ApproximationWorker.java'
--- src/dk/aau/cs/approximation/ApproximationWorker.java	2022-01-28 12:08:30 +0000
+++ src/dk/aau/cs/approximation/ApproximationWorker.java	2022-02-08 09:07:46 +0000
@@ -82,7 +82,7 @@
                     decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
                     result.verificationTime(),
                     result.stats(),
-                    result.isSolvedUsingStateEquation(),
+                    false,
                     result.getUnfoldedModel());
                 toReturn.setNameMapping(transformedModel.value2());
 
@@ -103,7 +103,7 @@
                             decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
                             approxResult.verificationTime(),
                             approxResult.stats(),
-                            approxResult.isSolvedUsingStateEquation(),
+                            false,
                             approxResult.getUnfoldedModel());
                         toReturn.setNameMapping(nameMapping);
 
@@ -151,7 +151,7 @@
                             decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
                             approxResult.verificationTime() + result.verificationTime(),
                             approxResult.stats(),
-                            approxResult.isSolvedUsingStateEquation(),
+                            false,
                             approxResult.getUnfoldedModel());
                         toReturn.setNameMapping(nameMapping);
 
@@ -176,7 +176,7 @@
                             decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
                             approxResult.verificationTime(),
                             approxResult.stats(),
-                            approxResult.isSolvedUsingStateEquation(),
+                            false,
                             approxResult.getUnfoldedModel());
                         toReturn.setNameMapping(nameMapping);
 
@@ -196,7 +196,7 @@
                         decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
                         approxResult.verificationTime(),
                         approxResult.stats(),
-                        approxResult.isSolvedUsingStateEquation(),
+                        false,
                         approxResult.getUnfoldedModel());
                     toReturn.setNameMapping(nameMapping);
 
@@ -231,7 +231,7 @@
                     decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
                     result.verificationTime(),
                     result.stats(),
-                    result.isSolvedUsingStateEquation(),
+                    false,
                     result.getUnfoldedModel());
                 toReturn.setNameMapping(nameMapping);
 
@@ -252,7 +252,7 @@
                         decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
                         result.verificationTime(),
                         result.stats(),
-                        result.isSolvedUsingStateEquation(),
+                        false,
                         result.getUnfoldedModel());
                     toReturn.setNameMapping(nameMapping);
 
@@ -271,7 +271,7 @@
                             decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
                             approxResult.verificationTime(),
                             approxResult.stats(),
-                            result.isSolvedUsingStateEquation(),
+                            false,
                             result.getUnfoldedModel());
                         toReturn.setNameMapping(nameMapping);
 
@@ -323,7 +323,7 @@
 								decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
 								approxResult.verificationTime() + result.verificationTime(),
 								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation(),
+								false,
                                 approxResult.getUnfoldedModel());
 						toReturn.setNameMapping(transformedModel.value2());
 					}
@@ -342,7 +342,7 @@
 								decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
 								approxResult.verificationTime(),
 								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation(),
+								false,
                                 approxResult.getUnfoldedModel());
 						toReturn.setNameMapping(nameMapping);
 					}
@@ -359,7 +359,7 @@
 					decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
 					result.verificationTime(),
 					result.stats(),
-					result.isSolvedUsingStateEquation(),
+					false,
                     result.getRawOutput(),
                     result.getUnfoldedModel());
 			toReturn.setNameMapping(nameMapping);
@@ -428,7 +428,7 @@
 					verificationResult.getSecondaryTrace(),
 					verificationResult.verificationTime(),
 					verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation(),
+					false,
                    verificationResult.getUnfoldedModel());
 				value.setNameMapping(composedModel.value2());
 	        } else {
@@ -446,7 +446,7 @@
 	                            decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
 	                            approxResult.verificationTime(),
 	                            approxResult.stats(),
-	        					verificationResult.isSolvedUsingStateEquation(),
+	        					false,
                                 verificationResult.getUnfoldedModel());
 	                valueNetwork.setNameMapping(nameMapping);
 	                
@@ -488,7 +488,7 @@
 	                        approxResult.getSecondaryTrace(),
 	                        approxResult.verificationTime() + verificationResult.verificationTime(),
 	                        approxResult.stats(),
-	    					verificationResult.isSolvedUsingStateEquation(),
+	    					false,
                             verificationResult.getUnfoldedModel());
 	                value.setNameMapping(composedModel.value2());
 	            }
@@ -508,7 +508,7 @@
 						verificationResult.getSecondaryTrace(),
 						verificationResult.verificationTime(),
 						verificationResult.stats(),
-						verificationResult.isSolvedUsingStateEquation(),
+						false,
                         verificationResult.getUnfoldedModel());
 				    value.setNameMapping(composedModel.value2());
 	            }
@@ -525,7 +525,7 @@
 						verificationResult.getSecondaryTrace(),
 						verificationResult.verificationTime(),
 						verificationResult.stats(),
-						verificationResult.isSolvedUsingStateEquation(),
+						false,
                         verificationResult.getUnfoldedModel());
 				    value.setNameMapping(composedModel.value2());
 				}
@@ -544,7 +544,7 @@
                     verificationResult.getSecondaryTrace(),
                     verificationResult.verificationTime(),
                     verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation(),
+					false,
                     verificationResult.getUnfoldedModel());
                 value.setNameMapping(composedModel.value2());
 	        }
@@ -562,7 +562,7 @@
                             verificationResult.getSecondaryTrace(),
                             verificationResult.verificationTime(),
                             verificationResult.stats(),
-        					verificationResult.isSolvedUsingStateEquation(),
+        					false,
                             verificationResult.getUnfoldedModel());
                     value.setNameMapping(composedModel.value2());
 	                    
@@ -584,7 +584,7 @@
                             decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
                             approxResult.verificationTime(),
                             approxResult.stats(),
-                            approxResult.isSolvedUsingStateEquation(),
+                            false,
                             verificationResult.getUnfoldedModel());
                         valueNetwork.setNameMapping(nameMapping);
 
@@ -631,7 +631,7 @@
 	                            verificationResult.getSecondaryTrace(),
 	                            verificationResult.verificationTime() + approxResult.verificationTime(),
 	                            verificationResult.stats(),
-	        					verificationResult.isSolvedUsingStateEquation(),
+	        					false,
                                 verificationResult.getUnfoldedModel());
 	                    value.setNameMapping(composedModel.value2());
 	                }
@@ -646,7 +646,7 @@
 							verificationResult.getSecondaryTrace(),
 							verificationResult.verificationTime(),
 							verificationResult.stats(),
-							verificationResult.isSolvedUsingStateEquation(),
+							false,
                             verificationResult.getUnfoldedModel());
 					    value.setNameMapping(composedModel.value2());
 	                }
@@ -660,7 +660,7 @@
 	                verificationResult.getSecondaryTrace(),
 	                verificationResult.verificationTime(),
 	                verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation(),
+					false,
                     verificationResult.getUnfoldedModel());
 	        value.setNameMapping(composedModel.value2());
 	    }
 
=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
--- src/dk/aau/cs/verification/QueryResult.java	2022-02-02 14:59:29 +0000
+++ src/dk/aau/cs/verification/QueryResult.java	2022-02-08 09:07:46 +0000
@@ -26,14 +26,6 @@
         this.solvedUsingTraceAbstractRefinement = solvedUsingTraceAbstractRefinement;
     }
 
-    public boolean isSolvedUsingStateEquation() {
-        return solvedUsingStateEquation;
-    }
-
-    public void setSolvedUsingStateEquation(boolean solvedUsingStateEquation) {
-        this.solvedUsingStateEquation = solvedUsingStateEquation;
-    }
-
     public boolean isSolvedUsingSiphonTrap() {
         return solvedUsingSiphonTrap;
     }
@@ -44,7 +36,6 @@
 
     private boolean solvedUsingQuerySimplification;
     private boolean solvedUsingTraceAbstractRefinement;
-    private boolean solvedUsingStateEquation;
     private boolean solvedUsingSiphonTrap;
 
 	public boolean isCTL = false;
 
=== modified file 'src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java'
--- src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java	2020-04-18 15:55:51 +0000
+++ src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java	2022-02-08 09:07:46 +0000
@@ -11,7 +11,7 @@
 	@Override
 	public ImageIcon getIconFor(VerificationResult<?> result){
 		if (result.getQueryResult().isApproximationInconclusive()) return rerunIcon;
-		if(result.isSolvedUsingStateEquation())	return result.isQuerySatisfied()? satisfiedIcon:notSatisfiedIcon;	// If we got a result from over-approximation, this is always conclusive.
+		if(result.isResolvedUsingSkeletonPreprocessor())	return result.isQuerySatisfied()? satisfiedIcon:notSatisfiedIcon;	// If we got a result from over-approximation, this is always conclusive.
 		if(result.getQueryResult().hasDeadlock()) return inconclusiveIcon;
 		
 		switch(result.getQueryResult().queryType())
 
=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2022-02-02 14:59:29 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2022-02-08 09:07:46 +0000
@@ -30,10 +30,6 @@
         return queryResult.isSolvedUsingTraceAbstractRefinement();
     }
 
-    public boolean isSolvedUsingStateEquation() {
-        return queryResult.isSolvedUsingStateEquation();
-    }
-
     public boolean isSolvedUsingSiphonTrap() {
         return queryResult.isSolvedUsingSiphonTrap();
     }
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2022-02-08 08:56:59 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2022-02-08 09:07:46 +0000
@@ -347,10 +347,9 @@
                         tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
                     }
                 }
+
                 var result = new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), false, standardOutput + "\n\n" + errorOutput, model);
-                if (queryResult.value1().isSolvedUsingStateEquation()) {
 
-                }
                 return result;
             }
         }
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java	2022-02-02 14:59:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java	2022-02-08 09:07:46 +0000
@@ -90,7 +90,6 @@
             BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);
             var qr = new QueryResult(result, boundedAnalysis, query, false);
             qr.setSolvedUsingQuerySimplification(solvedUsingQuerySimplification);
-            qr.setSolvedUsingStateEquation(solvedUsingStateEquation);
             qr.setSolvedUsingTraceAbstractRefinement(solvedUsingTraceAbstractRefinement);
             qr.setSolvedUsingSiphonTrap(solvedUsingSiphonTrap);
 
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java	2022-02-02 14:59:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java	2022-02-08 09:07:46 +0000
@@ -177,7 +177,6 @@
 
             var qr = new QueryResult(result, boundedAnalysis, query, false);
             qr.setSolvedUsingQuerySimplification(solvedUsingQuerySimplification);
-            qr.setSolvedUsingStateEquation(solvedUsingStateEquation);
             qr.setSolvedUsingTraceAbstractRefinement(solvedUsingTraceAbstractRefinement);
             qr.setSolvedUsingSiphonTrap(solvedUsingSiphonTrap);
 			return new Tuple<QueryResult, Stats>(qr, new Stats(discovered, explored, explored, transitionStats, placeBoundStats, reductionStats));
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java	2022-02-02 14:59:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java	2022-02-08 09:07:46 +0000
@@ -38,9 +38,7 @@
     boolean solvedUsingQuerySimplification = false;
     private static final String solvedUsingTraceAbstractRefinement_STRING = "Solved using Trace Abstraction Refinement";
     boolean solvedUsingTraceAbstractRefinement = false;
-    private static final String solvedUsingStateEquation_STRING = "Solved using Trace Abstraction Refinement";
-    boolean solvedUsingStateEquation = false;
-    private static final String solvedUsingSiphonTrap_STRING = "Solved using Siphon Trap";
+    private static final String solvedUsingSiphonTrap_STRING = "Query solved by Siphon-Trap Analysis.";
     boolean solvedUsingSiphonTrap  = false;
 
     void parseSolvedMethod(String line) {
@@ -48,8 +46,6 @@
             solvedUsingQuerySimplification = true;
         } else if (line.contains(solvedUsingTraceAbstractRefinement_STRING)) {
             solvedUsingTraceAbstractRefinement = true;
-        } else if (line.contains(solvedUsingStateEquation_STRING)) {
-            solvedUsingStateEquation = true;
         } else if (line.contains(solvedUsingSiphonTrap_STRING)) {
             solvedUsingSiphonTrap = true;
         }
 
=== modified file 'src/net/tapaal/gui/petrinet/verification/RunVerification.java'
--- src/net/tapaal/gui/petrinet/verification/RunVerification.java	2022-02-03 12:31:00 +0000
+++ src/net/tapaal/gui/petrinet/verification/RunVerification.java	2022-02-08 09:07:46 +0000
@@ -382,34 +382,32 @@
         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 = GridBagHelper.as(1, 5, WEST, new Insets(0,0,10,0));
+            gbc = GridBagHelper.as(1, rowOffset+1, WEST, new Insets(0,0,10,0));
             panel.add(showRawQueryButton, gbc);
         }
 
         if (result.isResolvedUsingSkeletonPreprocessor()) {
-            gbc = GridBagHelper.as(0, rowOffset+1, GridBagHelper.Anchor.WEST, new Insets(0,0,15,0));
+            gbc = GridBagHelper.as(0, rowOffset+2, GridBagHelper.Anchor.WEST, new Insets(0,0,15,0));
             gbc.gridwidth = 2;
-            panel.add(new JLabel(toHTML("The query was resolved using Skeleton Analysis preprocessing")), gbc);
+            panel.add(new JLabel(toHTML("The query was answered by Skeleton Analysis preprocessing.")), gbc);
         }
 
 
-        gbc = GridBagHelper.as(0, rowOffset+2, WEST, new Insets(0,0,15,0));
+        gbc = GridBagHelper.as(0, rowOffset+3, WEST, new Insets(0,0,15,0));
         gbc.gridwidth = 2;
 		if(result.isSolvedUsingQuerySimplification()){
 			panel.add(new JLabel(toHTML("The query was resolved using Query Simplification.")), gbc);
 		} else if (result.isSolvedUsingTraceAbstractRefinement()){
-            panel.add(new JLabel(toHTML("The query was not resolved using Trace Abstraction Refinement.")), gbc);
-        } else if (result.isSolvedUsingStateEquation()) {
-            panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
+            panel.add(new JLabel(toHTML("The query was resolved using Trace Abstraction Refinement.")), gbc);
         } else if (result.isSolvedUsingSiphonTrap()) {
             panel.add(new JLabel(toHTML("The query was resolved using Siphon Trap.")), gbc);
         }
 		
-		gbc = GridBagHelper.as(0, rowOffset+3, WEST);
+		gbc = GridBagHelper.as(0, rowOffset+4, WEST);
     	gbc.gridwidth = 2;
 		panel.add(new JLabel(result.getVerificationTimeString()), gbc);
 
-        gbc = GridBagHelper.as(0, rowOffset+4, WEST);
+        gbc = GridBagHelper.as(0, rowOffset+5, WEST);
         gbc.gridwidth = 2;
 		panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);
 		
@@ -421,7 +419,7 @@
             (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied()))
             && modelChecker.useDiscreteSemantics()) {
 
-            gbc = GridBagHelper.as(0, rowOffset+7, WEST);
+            gbc = GridBagHelper.as(0, rowOffset+8, WEST);
             gbc.gridwidth = 2;
             panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
         }