Merge lp:~tapaal-contributor/tapaal/boundedness-check into lp:tapaal

[Lena Ernstsen]

Boundedness check for verifypn uses different query and minimizing extra tokens is optional

[Jiri Srba (srba)]

Open the game-harddisk example and check for boundedness, it is broken.

review: Needs Fixing

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-03-02 16:02:35 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-08-25 10:24:16 +0000
@@ -84,7 +84,8 @@
 			result.append(" -a 10 ");
 		}
 		if (this.queryReductionTime == QueryReductionTime.NoTime) {
-			result.append(" -q 0 ");
+			result.append(
+			    " -q 0 ");
 		} else if (this.queryReductionTime == QueryReductionTime.ShortestTime) {
 		    //Run query reduction for 1 second, to avoid conflict with -s OverApprox argument, but also still not run the verification.
 		    result.append(" -q 1");

=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
--- src/pipe/gui/KBoundAnalyzer.java	2021-02-07 11:09:51 +0000
+++ src/pipe/gui/KBoundAnalyzer.java	2021-08-25 10:24:16 +0000
@@ -2,15 +2,18 @@
 
 import javax.swing.JSpinner;
 
+import dk.aau.cs.TCTL.*;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedPlace;
+import dk.aau.cs.util.Tuple;
+import dk.aau.cs.verification.NameMapping;
+import dk.aau.cs.verification.TAPNComposer;
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.dataLayer.TAPNQuery.AlgorithmOption;
 import pipe.dataLayer.TAPNQuery.QueryCategory;
 import pipe.gui.widgets.RunningVerificationDialog;
 import dk.aau.cs.Messenger;
-import dk.aau.cs.TCTL.TCTLAGNode;
-import dk.aau.cs.TCTL.TCTLAbstractProperty;
-import dk.aau.cs.TCTL.TCTLTrueNode;
 import dk.aau.cs.model.tapn.TAPNQuery;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 import dk.aau.cs.verification.ModelChecker;
@@ -22,6 +25,8 @@
 import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification;
 import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
 
+import java.util.ArrayList;
+
 public class KBoundAnalyzer {
 	protected TimedArcPetriNetNetwork tapnNetwork;
 	protected int k;
@@ -40,16 +45,24 @@
 	}
 
 	public void analyze() {
-		TAPNQuery query = getBoundednessQuery();
-		VerifyTAPNOptions options = verificationOptions();
-
-		RunKBoundAnalysis analyzer = new RunKBoundAnalysis(modelChecker, messenger, spinner);
-		RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), analyzer);
-
-		analyzer.execute(options, tapnNetwork, query, null);
-		dialog.setVisible(true);
+		analyze(verificationOptions());
 	}
 
+    public void analyze(VerifyTAPNOptions options) {
+        TAPNQuery query;
+        if (modelChecker instanceof VerifyPN) {
+            query = getPNBoundednessQuery();
+        } else {
+            query = getBoundednessQuery();
+        }
+
+        RunKBoundAnalysis analyzer = new RunKBoundAnalysis(modelChecker, messenger, spinner);
+        RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), analyzer);
+
+        analyzer.execute(options, tapnNetwork, query, null);
+        dialog.setVisible(true);
+    }
+
 	protected VerifyTAPNOptions verificationOptions() {
 		if(modelChecker instanceof VerifyPN){
 			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null, false);
@@ -62,10 +75,48 @@
 	}
 
 	protected TAPNQuery getBoundednessQuery() {
-		TCTLAbstractProperty property = null;
-
-		property = new TCTLAGNode(new TCTLTrueNode());
-
+		TCTLAbstractProperty property = new TCTLAGNode(new TCTLTrueNode());
 		return new TAPNQuery(property, k);
 	}
+
+	protected TAPNQuery getPNBoundednessQuery() {
+        int totalTokens = k + tapnNetwork.marking().size();
+
+        TCTLAtomicPropositionNode child = new TCTLAtomicPropositionNode(new TCTLTermListNode(getFactors()), "<=", new TCTLConstNode(totalTokens));
+        TCTLAbstractProperty property = new TCTLAGNode(child);
+
+        TAPNQuery query = new TAPNQuery(property, k);
+        query.setCategory(QueryCategory.CTL);
+
+        return query;
+    }
+
+    private ArrayList<TCTLAbstractStateProperty> getFactors() {
+        TimedArcPetriNet net = mergeNetComponents();
+        ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<>();
+
+        tapnNetwork.sharedPlaces().forEach(o -> {
+            if (net.getPlaceByName(o.name()) != null && !net.getPlaceByName(o.name()).name().contains("Shared_")) {
+                net.getPlaceByName(o.name()).setName("Shared_" + o.name());
+            }
+        });
+        tapnNetwork.allTemplates().forEach(o -> o.places().forEach(x -> {
+            if (net.getPlaceByName(x.name()) != null) net.getPlaceByName(x.name()).setName(o.name() + "_" + x.name());
+        }));
+
+        for (TimedPlace place : net.places()) {
+            factors.add(new TCTLPlaceNode(place.name()));
+            factors.add(new AritmeticOperator("+"));
+        }
+        if (factors.get(factors.size()-1) instanceof AritmeticOperator) factors.remove(factors.size()-1);
+
+        return factors;
+    }
+
+    private TimedArcPetriNet mergeNetComponents() {
+        TAPNComposer composer = new TAPNComposer(new MessengerImpl(), CreateGui.getCurrentTab().getGuiModels(), true, true);
+        Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(tapnNetwork);
+
+        return transformedModel.value1();
+    }
 }

=== modified file 'src/pipe/gui/RunKBoundAnalysis.java'
--- src/pipe/gui/RunKBoundAnalysis.java	2020-05-27 12:59:31 +0000
+++ src/pipe/gui/RunKBoundAnalysis.java	2021-08-25 10:24:16 +0000
@@ -4,33 +4,47 @@
 import javax.swing.JSpinner;
 
 import dk.aau.cs.Messenger;
+import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
 import net.tapaal.resourcemanager.ResourceManager;
 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
 import dk.aau.cs.verification.Boundedness;
 import dk.aau.cs.verification.ModelChecker;
 import dk.aau.cs.verification.VerificationResult;
 
+import java.util.ArrayList;
+
 public class RunKBoundAnalysis extends RunVerificationBase {
 
 	private final JSpinner spinner;
 
 	public RunKBoundAnalysis(ModelChecker modelChecker, Messenger messenger,JSpinner spinner) {
-		super(modelChecker, messenger);
+		super(modelChecker, messenger, spinner);
 		this.spinner = spinner;
 	}
 
 	@Override
-	protected void showResult(VerificationResult<TAPNNetworkTrace> result) {
+	protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {
 		if(result != null && !result.error()) {
 			if (!result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
 				JOptionPane.showMessageDialog(CreateGui.getApp(),
 						getAnswerNotBoundedString(), "Analysis Result",
 						JOptionPane.INFORMATION_MESSAGE);
 			} else {
-				spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet());
-				JOptionPane.showMessageDialog(CreateGui.getApp(),
-						getAnswerBoundedString(), "Analysis Result",
-						JOptionPane.INFORMATION_MESSAGE, ResourceManager.satisfiedIcon());
+			    if (modelChecker instanceof VerifyPN && !result.getRawOutput().contains("max tokens:")) {
+                    Object[] options = {"Ok", "Minimize extra tokens"};
+                    int answer = JOptionPane.showOptionDialog(CreateGui.getApp(),
+                        getPNAnswerBoundedString(), "Analysis Result,",
+                        JOptionPane.OK_CANCEL_OPTION, JOptionPane.INFORMATION_MESSAGE,
+                        ResourceManager.satisfiedIcon(), options, JOptionPane.OK_OPTION);
+                    return answer != JOptionPane.OK_OPTION;
+                } else if (modelChecker instanceof VerifyPN) {
+                    spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet());
+                } else {
+                    spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet());
+                    JOptionPane.showMessageDialog(CreateGui.getApp(),
+                        getAnswerBoundedString(), "Analysis Result",
+                        JOptionPane.INFORMATION_MESSAGE, ResourceManager.satisfiedIcon());
+                }
 			}
 		} else {						
 			String message = "An error occured during the verification." +
@@ -40,6 +54,7 @@
 			
 			messenger.displayWrappedErrorMessage(message,"Error during verification");
 		}
+		return false;
 	}
 
 	protected String getAnswerNotBoundedString() {
@@ -58,4 +73,12 @@
 				+ "The number of extra tokens was automatically lowered to the\n"
 				+ "minimum number of tokens needed for an exact analysis.";
 	}
+
+	protected String getPNAnswerBoundedString() {
+        return "The net with the specified extra number of tokens is bounded.\n\n"
+            + "This means that the analysis will be exact and always give \n"
+            + "the correct answer.\n\n"
+            + "The number of extra tokens can be lowered to the minimum number\n"
+            + "of tokens needed for an exact analysis.";
+    }
 }

=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java	2021-02-22 22:56:50 +0000
+++ src/pipe/gui/RunVerification.java	2021-08-25 10:24:16 +0000
@@ -31,7 +31,7 @@
 	private final IconSelector iconSelector;
 	private final VerificationCallback callback;
 	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, String reducedNetFilePath, boolean reduceNetOnly) {
-		super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly);
+		super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly, null);
 		iconSelector = selector;
 		this.callback = callback;
 	}
@@ -45,7 +45,7 @@
 	}
 
 	@Override
-	protected void showResult(VerificationResult<TAPNNetworkTrace> result) {
+	protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {
 		if (result != null && !result.error()) {
 			if(callback != null){
 				callback.run(result);
@@ -98,6 +98,7 @@
 			messenger.displayWrappedErrorMessage(message,"Error during verification");
 
 		}
+		return false;
 	}
 
 	private String toHTML(String string){

=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java	2021-02-07 11:09:51 +0000
+++ src/pipe/gui/RunVerificationBase.java	2021-08-25 10:24:16 +0000
@@ -3,9 +3,9 @@
 import java.io.File;
 import java.util.concurrent.ExecutionException;
 
-import javax.swing.SwingUtilities;
-import javax.swing.SwingWorker;
+import javax.swing.*;
 
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import dk.aau.cs.Messenger;
 import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
@@ -43,20 +43,25 @@
 	protected String reducedNetFilePath;
 	protected boolean reduceNetOnly;
 	protected boolean reducedNetOpened = false;
-	
-	
+	protected JSpinner spinner;
+
 	protected Messenger messenger;
 
-	public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly) {
+	public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly, JSpinner spinner) {
 		super();
 		this.modelChecker = modelChecker;
 		this.messenger = messenger;
 		this.reducedNetFilePath = reducedNetFilePath;
 		this.reduceNetOnly = reduceNetOnly;
-	}
+        this.spinner = spinner;
+    }
 
     public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
-        this(modelChecker, messenger, null, false);
+        this(modelChecker, messenger, null, false, null);
+    }
+
+    public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, JSpinner spinner) {
+        this(modelChecker, messenger, null, false, spinner);
     }
 
 	
@@ -212,8 +217,12 @@
 				return;
 			}
 			firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
-			showResult(result);
 
+			if (showResult(result) && spinner != null) {
+			    options = new VerifyPNOptions(options.extraTokens(), pipe.dataLayer.TAPNQuery.TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, pipe.dataLayer.TAPNQuery.QueryCategory.Default, pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime, false, null, false);
+                KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner);
+                optimizer.analyze((VerifyTAPNOptions) options);
+            }
 		} else {
 			modelChecker.kill();
 			messenger.displayInfoMessage("Verification was interrupted by the user. No result found!", "Verification Cancelled");
@@ -231,5 +240,5 @@
 		});
 	}
 
-	protected abstract void showResult(VerificationResult<TAPNNetworkTrace> result);
+	protected abstract boolean showResult(VerificationResult<TAPNNetworkTrace> result);
 }