Merge lp:~tapaal-contributor/tapaal/save-tar-option into lp:tapaal

[Lena Ernstsen]

The trace refinement option is saved in the .tapn file

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/BatchProcessingDialog.java'
--- src/dk/aau/cs/gui/BatchProcessingDialog.java	2020-07-20 07:55:49 +0000
+++ src/dk/aau/cs/gui/BatchProcessingDialog.java	2021-03-02 20:12:24 +0000
@@ -1577,6 +1577,10 @@
 			s.append("Stubborn Reduction: ");
 			s.append(query.isStubbornReductionEnabled() ? "Yes\n\n" : "No\n\n");
 
+            s.append("\n\n");
+            s.append("Trace Abstract Refinement: ");
+            s.append(query.isTarOptionEnabled() ? "Yes\n\n" : "No\n\n");
+
 			s.append("Query Property:\n");
                         s.append(query.getProperty().toString());
 			
 
=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2020-08-11 13:25:25 +0000
+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2021-03-02 20:12:24 +0000
@@ -320,7 +320,8 @@
 		queryElement.setAttribute("enableOverApproximation", "" + query.isOverApproximationEnabled());
 		queryElement.setAttribute("enableUnderApproximation", "" + query.isUnderApproximationEnabled());
 		queryElement.setAttribute("approximationDenominator", "" + query.approximationDenominator());
-		queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
+        queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
+        queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled());
 
 		return queryElement;
 	}
@@ -358,6 +359,7 @@
 		queryElement.setAttribute("useSiphonTrapAnalysis", "" + query.isSiphontrapEnabled());
 		queryElement.setAttribute("useQueryReduction", "" + query.isQueryReductionEnabled());
 		queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
+		queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled());
 		
 		return queryElement;
 	}
 
=== modified file 'src/dk/aau/cs/io/queries/TAPNQueryLoader.java'
--- src/dk/aau/cs/io/queries/TAPNQueryLoader.java	2020-10-31 17:27:18 +0000
+++ src/dk/aau/cs/io/queries/TAPNQueryLoader.java	2021-03-02 20:12:24 +0000
@@ -91,6 +91,7 @@
 		boolean siphontrap = getReductionOption(queryElement, "useSiphonTrapAnalysis", false);
 		boolean queryReduction = getReductionOption(queryElement, "useQueryReduction", true);
 		boolean stubborn = getReductionOption(queryElement, "useStubbornReduction", true);
+		boolean useTar = getTarOption(queryElement, "useTarOption", false);
 
 		TCTLAbstractProperty query;
 		if (queryElement.getElementsByTagName("formula").item(0) != null){
@@ -107,6 +108,7 @@
 			parsedQuery.setUseSiphontrap(siphontrap);
 			parsedQuery.setUseQueryReduction(queryReduction);
 			parsedQuery.setUseStubbornReduction(stubborn);
+			parsedQuery.setUseTarOption(useTar);
 			if (parsedQuery.getCategory() == QueryCategory.CTL && algorithmOption != null){
 				parsedQuery.setAlgorithmOption(AlgorithmOption.valueOf(algorithmOption));
 //				RenameTemplateVisitor rt = new RenameTemplateVisitor("", 
@@ -229,6 +231,19 @@
 		}
 		return result;	
 	}
+
+	private boolean getTarOption(Element queryElement, String attributeName, boolean defaultValue) {
+        if(!queryElement.hasAttribute(attributeName)){
+            return defaultValue;
+        }
+        boolean result;
+        try {
+            result = queryElement.getAttribute(attributeName).equals("true");
+        } catch(Exception e) {
+            result = defaultValue;
+        }
+        return result;
+    }
 	
 	private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
 	{
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-02-07 11:09:51 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-03-02 20:12:24 +0000
@@ -43,6 +43,13 @@
 			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false);
 	}
 
+    public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
+                           boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
+                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, boolean useTarOption) {
+        this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
+            enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, useTarOption);
+    }
+
 	@Override
 	public String toString() {
 		StringBuilder result = new StringBuilder();
 
=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2020-10-15 15:44:06 +0000
+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2021-03-02 20:12:24 +0000
@@ -356,6 +356,7 @@
 				boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions();
 				boolean overApproximation = query.isOverApproximationEnabled();
 				boolean underApproximation = query.isUnderApproximationEnabled();
+				boolean useTar = query.isTarOptionEnabled();
 				int approximationDenominator = query.approximationDenominator();
 				if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) {
 					overApproximation = false;
@@ -381,6 +382,7 @@
 				changedQuery.setUseSiphontrap(query.isSiphontrapEnabled());
 				changedQuery.setUseQueryReduction(query.isQueryReductionEnabled());
 				changedQuery.setUseStubbornReduction(stubbornReduction);
+				changedQuery.setUseTarOption(useTar);
 				return changedQuery;
 			} else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness) {
 				isSoundnessCheck = true;
@@ -623,9 +625,9 @@
 			return new VerifyDTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), false,  query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode(), 0, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.isStubbornReductionEnabled());
 		else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
 			if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){
-			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false);
+			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false, query.isTarOptionEnabled());
 			} else {
-			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled()? QueryReductionTime.UnlimitedTime: QueryReductionTime.NoTime, query.isStubbornReductionEnabled());
+			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled()? QueryReductionTime.UnlimitedTime: QueryReductionTime.NoTime, query.isStubbornReductionEnabled(), query.isTarOptionEnabled());
 			}
 		else
 			return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 
=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java	2021-02-07 11:09:51 +0000
+++ src/pipe/dataLayer/TAPNQuery.java	2021-03-02 20:12:24 +0000
@@ -393,6 +393,7 @@
 		copy.setUseSiphontrap(this.isQueryReductionEnabled());
 		copy.setUseQueryReduction(this.isQueryReductionEnabled());
 		copy.setUseStubbornReduction(this.isStubbornReductionEnabled());
+		copy.setUseTarOption(this.isTarOptionEnabled());
 		
 		return copy;
 	}
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2021-02-22 22:26:01 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2021-03-02 20:12:24 +0000
@@ -1292,6 +1292,7 @@
         useQueryReduction.setSelected(queryToCreateFrom.isQueryReductionEnabled());
         useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
         useReduction.setSelected(queryToCreateFrom.useReduction());
+        useTraceRefinement.setSelected(queryToCreateFrom.isTarOptionEnabled());
     }
 
 	private void setupTraceOptionsFromQuery(TAPNQuery queryToCreateFrom) {