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

[Lena Ernstsen]

Added -tar option to the query dialog

[lp:~tapaal-contributor/tapaal/add-tar-option]

1116. By Lena Ernstsen on 2021-02-07

Merged lp:tapaal

[Kenneth Yrke Jørgensen (yrke)]

review: Approve (code)

[Jiri Srba (srba)]

The detection if a query is a reachability query must be improved - tar can only be offered for EF or AG queries that do not contain any other temporal operators.

E.g. for the query

E ((AG true) U false)

the TAR option is offered as well, which should not be the case.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/add-tar-option]

1117. By Lena Ernstsen on 2021-02-19

Only possible to use tar when either 'AG' or 'EF' is chosen

[Jiri Srba (srba)]

I just made a simple untimed net and a query:

A (TAPN1.P0 = 1 U (EF TAPN1.P0 = 1))

and it still offers to use the tar option in the query dialog.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/add-tar-option]

1118. By Lena Ernstsen on 2021-02-22

Fixed tar only possible with AG and EF

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2020-10-15 15:44:06 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-02-22 22:26:13 +0000
@@ -19,26 +19,28 @@
 	private boolean useSiphontrap = false; 
 	private QueryReductionTime queryReductionTime;
 	private boolean useStubbornReduction = true;
+	private boolean useTarOption;
 	private String pathToReducedNet;
 	
 	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
                            boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
-                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet) {
-		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
+                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet, boolean useTarOption) {
+		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, useTarOption);
 		this.modelReduction = modelReduction;
 		this.queryCategory = queryCategory;
 		this.algorithmOption = algorithmOption;
 		this.useSiphontrap = siphontrap;
 		this.queryReductionTime = queryReduction;
 		this.useStubbornReduction = stubbornReduction;
+		this.useTarOption = useTarOption;
 		this.pathToReducedNet = pathToReducedNet;
 	}
-	
+
 	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) {
 		this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, 
-			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null);
+			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false);
 	}
 
 	@Override
@@ -83,6 +85,9 @@
 		if (!this.useStubbornReduction) {
 			result.append(" -p ");
 		}
+		if (this.useTarOption) {
+		    result.append(" -tar ");
+        }
 		return result.toString();
 	}
 
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2021-02-22 22:26:13 +0000
@@ -16,6 +16,7 @@
 	protected int tokensInModel;
 	private final boolean symmetry;
 	private final boolean discreteInclusion;
+	private final boolean tarOption;
 	private InclusionPlaces inclusionPlaces;
 	
 	//only used for boundedness analysis
@@ -27,8 +28,12 @@
 	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
 		this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
+
+    public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+        this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, false);
+    }
 	
-	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, boolean tarOption) {
 		this.extraTokens = extraTokens;
 		this.traceOption = traceOption;
 		searchOption = search;
@@ -39,6 +44,7 @@
 		this.enabledOverApproximation = enableOverApproximation;
 		this.enabledUnderApproximation = enableUnderApproximation;
 		this.approximationDenominator = approximationDenominator;
+		this.tarOption = tarOption;
 	}
 
 	public TraceOption trace() {
 
=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java	2020-11-06 19:41:50 +0000
+++ src/pipe/dataLayer/TAPNQuery.java	2021-02-22 22:26:13 +0000
@@ -72,6 +72,7 @@
 	private boolean useSiphontrap = false; 
 	private boolean useQueryReduction = true; 
 	private boolean useStubbornReduction = true;
+	private boolean useTarOption = false;
 
 	/**
 	 * @param name
@@ -108,6 +109,14 @@
 		return this.useStubbornReduction;
 	}
 
+	public boolean isTarOptionEnabled() {
+	    return this.useTarOption;
+    }
+
+    public void setUseTarOption(boolean useTarOption) {
+	    this.useTarOption = useTarOption;
+    }
+
 	public int approximationDenominator() {
 		return this.denominator;
 	}
@@ -361,6 +370,7 @@
 		useSiphontrap = newQuery.isSiphontrapEnabled();
 		useQueryReduction = newQuery.isQueryReductionEnabled();
 		useStubbornReduction = newQuery.isStubbornReductionEnabled();
+		useTarOption = newQuery.isTarOptionEnabled();
 	}
 
 	public InclusionPlaces inclusionPlaces() {
 
=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
--- src/pipe/gui/KBoundAnalyzer.java	2020-10-15 15:44:06 +0000
+++ src/pipe/gui/KBoundAnalyzer.java	2021-02-22 22:26:13 +0000
@@ -52,7 +52,7 @@
 
 	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);
+			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);
 		} else if(modelChecker instanceof VerifyTAPN){
 			return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
 		} else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
 
=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java	2020-11-11 07:55:24 +0000
+++ src/pipe/gui/RunVerificationBase.java	2021-02-22 22:26:13 +0000
@@ -122,7 +122,8 @@
 										dataLayerQuery.isSiphontrapEnabled(),
 										dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
 										dataLayerQuery.isStubbornReductionEnabled(),
-                                        reducedNetFilePath
+                                        reducedNetFilePath,
+                                        dataLayerQuery.isTarOptionEnabled()
 								),
 								transformedModel,
 								clonedQuery
@@ -143,7 +144,8 @@
 										false,
                                         pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
 										false,
-                                        reducedNetFilePath
+                                        reducedNetFilePath,
+                                        false
 								),
 								transformedModel,
 								clonedQuery
 
=== modified file 'src/pipe/gui/Verifier.java'
--- src/pipe/gui/Verifier.java	2020-11-13 10:08:54 +0000
+++ src/pipe/gui/Verifier.java	2021-02-22 22:26:13 +0000
@@ -176,7 +176,6 @@
 					query.isStubbornReductionEnabled()
 			);
 		} else if(query.getReductionOption() == ReductionOption.VerifyPN){
-
             try {
                 reducedNetTempFile = File.createTempFile("reduced-", ".pnml");
             } catch (IOException e) {
@@ -202,7 +201,8 @@
                     query.isSiphontrapEnabled(),
                     TAPNQuery.QueryReductionTime.NoTime,
                     query.isStubbornReductionEnabled(),
-                    reducedNetTempFile.getAbsolutePath()
+                    reducedNetTempFile.getAbsolutePath(),
+                    query.isTarOptionEnabled()
                 );
             } else {
                 verifytapnOptions = new VerifyPNOptions(
@@ -219,10 +219,10 @@
                     query.isSiphontrapEnabled(),
                     query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
                     query.isStubbornReductionEnabled(),
-                    reducedNetTempFile.getAbsolutePath()
+                    reducedNetTempFile.getAbsolutePath(),
+                    query.isTarOptionEnabled()
                 );
             }
-
 		} else {
 			verifytapnOptions = new VerifyTAPNOptions(
 					bound,
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2020-12-17 21:03:12 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2021-02-22 22:26:13 +0000
@@ -165,6 +165,7 @@
     private JCheckBox useQueryReduction;
     private JCheckBox useReduction;
 	private JCheckBox useStubbornReduction;
+	private JCheckBox useTraceRefinement;
 
 	// Approximation options panel
 	private JPanel overApproximationOptionsPanel;
@@ -293,6 +294,7 @@
     private final static String TOOL_TIP_USE_STRUCTURALREDUCTION = "Apply structural reductions to reduce the size of the net.";
     private final static String TOOL_TIP_USE_SIPHONTRAP = "For a deadlock query, attempt to prove deadlock-freedom by using siphon-trap analysis via linear programming.";
     private final static String TOOL_TIP_USE_QUERY_REDUCTION = "Use query rewriting rules and linear programming (state equations) to reduce the size of the query.";
+    private final static String TOOL_TIP_USE_TRACE_REFINEMENT = "Enables Trace Abstraction Refinement for reachability properties";
 
 	//Tool tips for search options panel
 	private final static String TOOL_TIP_HEURISTIC_SEARCH = "<html>Uses a heuristic method in state space exploration.<br />" +
@@ -322,8 +324,7 @@
 	private final static String TOOL_TIP_APPROXIMATION_METHOD_UNDER = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";
 	private final static String TOOL_TIP_APPROXIMATION_CONSTANT = "Choose approximation constant";
 
-	public QueryDialog(EscapableDialog me, QueryDialogueOption option,
-                       TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
+	public QueryDialog(EscapableDialog me, QueryDialogueOption option, TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
 		this.tapnNetwork = tapnNetwork;
 		this.guiModels = guiModels;
 		this.lens = lens;
@@ -442,6 +443,7 @@
         query.setUseSiphontrap(useSiphonTrap.isSelected());
         query.setUseQueryReduction(useQueryReduction.isSelected());
         query.setUseStubbornReduction(useStubbornReduction.isSelected());
+        query.setUseTarOption(useTraceRefinement.isSelected());
         return query;
     }
 
@@ -1210,8 +1212,15 @@
 		setupSearchOptionsFromQuery(queryToCreateFrom);
 		setupReductionOptionsFromQuery(queryToCreateFrom);
 		setupTraceOptionsFromQuery(queryToCreateFrom);
+		setupTarOptionsFromQuery(queryToCreateFrom);
 	}
 
+	private void setupTarOptionsFromQuery(TAPNQuery queryToCreateFrom) {
+	    if (queryToCreateFrom.isTarOptionEnabled()) {
+	        useTraceRefinement.setSelected(true);
+        }
+    }
+
 	private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {
 		if (queryToCreateFrom.isOverApproximationEnabled())
 			overApproximationEnable.setSelected(true);
@@ -2656,6 +2665,7 @@
         useGCD = new JCheckBox("Use GCD");
         usePTrie = new JCheckBox("Use PTrie");
         useOverApproximation = new JCheckBox("Use untimed state-equations check");
+        useTraceRefinement = new JCheckBox("Use trace abstraction refinement");
 
         useReduction.setSelected(true);
         useSiphonTrap.setSelected(false);
@@ -2668,6 +2678,7 @@
         useGCD.setSelected(true);
         usePTrie.setSelected(true);
         useOverApproximation.setSelected(true);
+        useTraceRefinement.setSelected(false);
 
         useReduction.setToolTipText(TOOL_TIP_USE_STRUCTURALREDUCTION);
         useSiphonTrap.setToolTipText(TOOL_TIP_USE_SIPHONTRAP);
@@ -2680,6 +2691,7 @@
         useGCD.setToolTipText(TOOL_TIP_GCD);
         usePTrie.setToolTipText(TOOL_TIP_PTRIE);
         useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
+        useTraceRefinement.setToolTipText(TOOL_TIP_USE_TRACE_REFINEMENT);
 
         if (lens.isTimed() || lens.isGame()) {
             initTimedReductionOptions();
@@ -2765,6 +2777,9 @@
         gbc.gridx = 2;
         gbc.gridy = 3;
         reductionOptionsPanel.add(useStubbornReduction, gbc);
+        gbc.gridx = 3;
+        gbc.gridy = 0;
+        reductionOptionsPanel.add(useTraceRefinement, gbc);
     }
 
 	protected void setEnabledOptionsAccordingToCurrentReduction() {
@@ -2776,11 +2791,24 @@
             refreshDiscreteOptions();
             refreshDiscreteInclusion();
             refreshOverApproximationOption();
+        } else if (!lens.isTimed()) {
+            refreshTraceRefinement();
         }
 		updateSearchStrategies();
 		refreshExportButtonText();
 	}
 
+	private void refreshTraceRefinement() {
+	    ReductionOption reduction = getReductionOption();
+	    useTraceRefinement.setEnabled(false);
+
+	    if (reduction != null && reduction.equals(ReductionOption.VerifyPN) && !hasInhibitorArcs &&
+            (newProperty.toString().startsWith("AG") || newProperty.toString().startsWith("EF")) &&
+            !newProperty.hasNestedPathQuantifiers()) {
+	        useTraceRefinement.setEnabled(true);
+        }
+    }
+
 	private void refreshDiscreteInclusion() {
 		ReductionOption reduction = getReductionOption();
 		if(reduction == null){
 
=== modified file 'src/resources/Example nets/train-level-crossing.tapn'
--- src/resources/Example nets/train-level-crossing.tapn	2018-07-13 18:16:32 +0000
+++ src/resources/Example nets/train-level-crossing.tapn	2021-02-22 22:26:13 +0000
@@ -112,6 +112,6 @@
 <arcpath arcPointType="false" id="1" xCoord="117" yCoord="147"/>
 </arc>
 </net>
-<query active="true" approximationDenominator="2" capacity="5" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="null" gcd="true" hashTableSize="null" inclusionPlaces="*NONE*" name="Crossing is Save" overApproximation="true" pTrie="true" query="AG (!(Train.DangerZone &gt; 0) or TraficLight.Red = 1)" reduction="true" reductionOption="VerifyTAPN" searchOption="HEURISTIC" symmetry="true" timeDarts="true" traceOption="NONE"/>
+<query active="true" approximationDenominator="2" capacity="5" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="null" gcd="true" hashTableSize="null" inclusionPlaces="*NONE*" name="Crossing is Safe" overApproximation="true" pTrie="true" query="AG (!(Train.DangerZone &gt; 0) or TraficLight.Red = 1)" reduction="true" reductionOption="VerifyTAPN" searchOption="HEURISTIC" symmetry="true" timeDarts="true" traceOption="NONE"/>
 <k-bound bound="3"/>
 </pnml>