Merge lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 into lp:tapaal/3.9

[Lena Ernstsen]

Considers LTL nodes when selecting icons for verification

[lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234]

1177. By Lena Ernstsen on 2023-01-19

Reverted change to avoid NPE

1178. By Lena Ernstsen on 2023-01-19

Added 'show raw query results' button for state equation results

1179. By Lena Ernstsen on 2023-01-23

Fixed wrong statistics for CTL queries

[Jiri Srba (srba)]

Tested and works fine.

review: Approve

=== modified file 'src/dk/aau/cs/model/tapn/TAPNQuery.java'
--- src/dk/aau/cs/model/tapn/TAPNQuery.java	2016-04-14 20:09:47 +0000
+++ src/dk/aau/cs/model/tapn/TAPNQuery.java	2023-01-23 10:20:36 +0000
@@ -1,9 +1,6 @@
 package dk.aau.cs.model.tapn;
 
-import dk.aau.cs.TCTL.TCTLAFNode;
-import dk.aau.cs.TCTL.TCTLAbstractProperty;
-import dk.aau.cs.TCTL.TCTLEFNode;
-import dk.aau.cs.TCTL.TCTLEGNode;
+import dk.aau.cs.TCTL.*;
 import dk.aau.cs.TCTL.visitors.HasDeadlockVisitor;
 import dk.aau.cs.verification.QueryType;
 import pipe.dataLayer.TAPNQuery.QueryCategory;
@@ -27,9 +24,11 @@
 	}
 	
 	public QueryType queryType(){
-		if(property instanceof TCTLEFNode) return QueryType.EF;
-		else if(property instanceof TCTLEGNode) return QueryType.EG;
-		else if(property instanceof TCTLAFNode) return QueryType.AF;
+		if (property instanceof TCTLEFNode) return QueryType.EF;
+		else if (property instanceof TCTLEGNode) return QueryType.EG;
+        else if (property instanceof LTLENode) return QueryType.E;
+        else if (property instanceof LTLANode) return QueryType.A;
+		else if (property instanceof TCTLAFNode) return QueryType.AF;
 		else return QueryType.AG;
 	}
 	

=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
--- src/dk/aau/cs/verification/QueryResult.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/QueryResult.java	2023-01-23 10:20:36 +0000
@@ -61,6 +61,8 @@
 		|| (queryType().equals(QueryType.EG)) // && !isQuerySatisfied()) 
 		|| (queryType().equals(QueryType.AF)) // && isQuerySatisfied())
 		|| (queryType().equals(QueryType.AG) && isQuerySatisfied())
+        || (queryType().equals(QueryType.A))
+        || (queryType().equals(QueryType.E))
 		|| (hasDeadlock() && 
 				(!isQuerySatisfied() && queryType().equals(QueryType.EF)) || 
 				(isQuerySatisfied() && queryType().equals(QueryType.AG))

=== modified file 'src/dk/aau/cs/verification/QueryType.java'
--- src/dk/aau/cs/verification/QueryType.java	2011-05-21 13:00:05 +0000
+++ src/dk/aau/cs/verification/QueryType.java	2023-01-23 10:20:36 +0000
@@ -4,5 +4,7 @@
 	EF,
 	EG,
 	AF,
-	AG
+	AG,
+    A,
+    E
 }

=== modified file 'src/dk/aau/cs/verification/Stats.java'
--- src/dk/aau/cs/verification/Stats.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/Stats.java	2023-01-23 10:20:36 +0000
@@ -137,15 +137,15 @@
 	@Override
 	public String toString() {
 		StringBuilder buffer = new StringBuilder();
-		buffer.append("Discovered markings: ");
+		buffer.append("Discovered configurations: ");
 		buffer.append(discovered);
 		buffer.append(System.getProperty("line.separator"));
 		
-		buffer.append("Explored markings: ");
+		buffer.append("Explored configurations: ");
 		buffer.append(explored);
 		buffer.append(System.getProperty("line.separator"));
 		
-		buffer.append("Stored markings: ");
+		buffer.append("Stored configurations: ");
 		buffer.append(stored);
 		return buffer.toString();
 	}

=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2021-10-13 18:51:36 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2023-01-23 10:20:36 +0000
@@ -4,6 +4,8 @@
 import java.util.ArrayList;
 import java.util.Comparator;
 import java.util.List;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 import dk.aau.cs.model.tapn.NetworkMarking;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
@@ -21,6 +23,7 @@
 	private NameMapping nameMapping;
 	private TTrace secondaryTrace;
 	private boolean isSolvedUsingStateEquation = false;
+	private int bound;
 	
 	public boolean isQuerySatisfied() {
 		return queryResult.isQuerySatisfied();
@@ -32,6 +35,15 @@
 		this.verificationTime = verificationTime;
 		this.stats = stats;
 		this.rawOutput = rawOutput;
+
+		String[] lines = rawOutput.split(System.getProperty("line.separator"));
+		for (String line : lines) {
+            Matcher matcher = Pattern.compile("\\s*-k\\s*(\\d+)\\s*").matcher(line);
+            if (matcher.find()) {
+                this.bound = Integer.parseInt(matcher.group(1));
+                break;
+            }
+        }
 	}
 
     public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
@@ -231,4 +243,8 @@
 	public String getRawOutput() {
 	    return rawOutput;
     }
+
+    public int getBound() {
+	    return bound;
+    }
 }

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2021-07-16 20:39:22 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2023-01-23 10:20:36 +0000
@@ -340,7 +340,6 @@
 					    tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1());
                     } else {
                         tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
-
                     }
 					return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput);
 				}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java	2020-07-13 14:30:00 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java	2023-01-23 10:20:36 +0000
@@ -13,15 +13,16 @@
 	private static final String Query_IS_NOT_SATISFIED_STRING = "Query is NOT satisfied";
 	private static final String Query_IS_SATISFIED_STRING = "Query is satisfied";
 
-    private static final Pattern configurationsPattern = Pattern.compile("\\s*Configurations:\\s*(\\d+)\\s*");
-    private static final Pattern markingsPattern = Pattern.compile("\\s*Markings:\\s*(\\d+)\\s*");
-    private static final Pattern edgesPattern = Pattern.compile("\\t+Edges:\\s*(\\d+)\\s*");
-
-    private static final Pattern processedEdgesPattern = Pattern.compile("\\s*Processed Edges:\\s*(\\d+)\\s*");
-    private static final Pattern processedNEdgesPattern = Pattern.compile("\\s*Processed N. Edges:\\s*(\\d+)\\s*");
-    private static final Pattern exploredConfigurationsPattern = Pattern.compile("\\s*Explored Configs:\\s*(\\d+)\\s*");
-
-    private static final Pattern maxUsedTokensPattern = Pattern.compile("\\s*Max number of tokens found in any reachable marking:\\s*(>)?(\\d+)\\s*");
+    private static final Pattern configurationsPattern = Pattern.compile("\\s*Configurations\\s*:\\s*(\\d+)\\s*");
+    private static final Pattern markingsPattern = Pattern.compile("\\s*Markings\\s*:\\s*(\\d+)\\s*");
+    private static final Pattern edgesPattern = Pattern.compile("\\t+Edges\\s*:\\s*(\\d+)\\s*");
+
+    private static final Pattern processedEdgesPattern = Pattern.compile("\\s*Processed Edges\\s*:\\s*(\\d+)\\s*");
+    private static final Pattern processedNEdgesPattern = Pattern.compile("\\s*Processed N. Edges\\s*:\\s*(\\d+)\\s*");
+    private static final Pattern exploredConfigurationsPattern = Pattern.compile("\\s*Explored Configs\\s*:\\s*(\\d+)\\s*");
+
+    private static final Pattern maxUsedTokensPattern = Pattern.compile("\\s*Max number of tokens found in any reachable marking\\s*:\\s*(>)?(\\d+)\\s*");
+    private static final Pattern maxTokensPattern = Pattern.compile("\\s*max tokens\\s*:\\s*(>)?(\\d+)\\s*");
 
 	public VerifyPNCTLOutputParser(int totalTokens, int extraTokens, TAPNQuery queryType) {
         super(totalTokens, extraTokens, queryType);
@@ -76,7 +77,14 @@
 
                     matcher = maxUsedTokensPattern.matcher(line);
                     if(matcher.find()){
-                        maxUsedTokens = Integer.parseInt(matcher.group(1));
+                        maxUsedTokens += Integer.parseInt(matcher.group(2));
+                        String operator = matcher.group(1) == null ? "" : matcher.group(1);
+                        if(operator.equals(">")) maxUsedTokens += 1; // Indicate non-k-boundedness by encoding that an extra token was used.
+                    }
+
+                    matcher = maxTokensPattern.matcher(line);
+                    if(matcher.find()){
+                        maxUsedTokens += Integer.parseInt(matcher.group(2));
                         String operator = matcher.group(1) == null ? "" : matcher.group(1);
                         if(operator.equals(">")) maxUsedTokens += 1; // Indicate non-k-boundedness by encoding that an extra token was used.
                     }

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java	2019-03-22 10:13:18 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java	2023-01-23 10:20:36 +0000
@@ -15,27 +15,47 @@
 		switch(result.getQueryResult().queryType())
 		{
 		case EF:
-			if(result.isQuerySatisfied()){
+			if (result.isQuerySatisfied()) {
 				return satisfiedIcon;
-			}else if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
+			} else if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
 				return notSatisfiedIcon;
 			}
 			break;
 		case AG:
-			if(!result.isQuerySatisfied()) return notSatisfiedIcon;
-			else if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;
+			if (!result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) {
+			    return notSatisfiedIcon;
+            } else if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
+			    return satisfiedIcon;
+            }
 			break;
 		case AF:
-			if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
+			if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
 				return notSatisfiedIcon;
-			} else if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
+			} else if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
 				return satisfiedIcon;
 			}
 			break;
 		case EG:
-			if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;
-			else if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return notSatisfiedIcon;
+			if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
+			    return satisfiedIcon;
+            } else if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
+			    return notSatisfiedIcon;
+            }
 			break;
+        case A:
+            if (!result.isQuerySatisfied()) {
+                return notSatisfiedIcon;
+            } else if (result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) {
+                return satisfiedIcon;
+            }
+            break;
+        case E:
+            if (!result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) {
+                return notSatisfiedIcon;
+            } else if (result.isQuerySatisfied()) {
+                return satisfiedIcon;
+            }
+            break;
 		default:
 			return null;
 		}

=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java	2021-10-13 18:51:36 +0000
+++ src/pipe/gui/RunVerification.java	2023-01-23 10:20:36 +0000
@@ -298,11 +298,20 @@
 		gbc.anchor = GridBagConstraints.WEST;		
 		panel.add(new JLabel(toHTML(result.getResultString())), gbc);
 
+        if (result.getBound() < result.getQueryResult().boundednessAnalysis().usedTokens() &&
+            !result.getQueryResult().toString().toLowerCase().contains("only markings with")) {
+            gbc = new GridBagConstraints();
+            gbc.gridx = 0;
+            gbc.gridy = 0;
+            gbc.gridwidth = 2;
+            gbc.anchor = GridBagConstraints.WEST;
+            panel.add(new JLabel("<html><br/><br/>Only markings with at most " + result.getBound() + " tokens were explored<br/><br/></html>"), gbc);
+        }
+
 		// TODO remove this when the engine outputs statistics
 		boolean isCTLQuery = result.getQueryResult().isCTL;
 
 		if(modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && !isCTLQuery){
-
             displayStats(panel, result.getStatsAsString(), modelChecker.getStatsExplanations());
 			
 			if(!result.getTransitionStatistics().isEmpty()){
@@ -383,15 +392,40 @@
 		} else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){
             displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations());
 
+            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 = new GridBagConstraints();
+                gbc.gridx = 0;
+                gbc.gridy = 4;
+                gbc.insets = new Insets(0,0,10,0);
+                gbc.anchor = GridBagConstraints.WEST;
+                panel.add(showRawQueryButton, gbc);
+            }
 		}
 
 		if(result.isSolvedUsingStateEquation()){
 			gbc = new GridBagConstraints();
 			gbc.gridx = 0;
-			gbc.gridy = 6;
+			gbc.gridy = 4;
 			gbc.insets = new Insets(0,0,15,0);
 			gbc.anchor = GridBagConstraints.WEST;
 			panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
+
+            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 = new GridBagConstraints();
+                gbc.gridx = 0;
+                gbc.gridy = 5;
+                gbc.insets = new Insets(0,0,10,0);
+                gbc.anchor = GridBagConstraints.WEST;
+                panel.add(showRawQueryButton, gbc);
+            }
 		}
 		
 		gbc = new GridBagConstraints();