Raw verification options issues - fix 2046945

src/main/java/dk/aau/cs/verification/ProcessRunner.java

@@ -7,7 +7,6 @@
 
 import dk.aau.cs.debug.Logger;
 import dk.aau.cs.util.MemoryMonitor;
-import dk.aau.cs.verification.VerifyTAPN.VerifyDTAPN;
 
 public class ProcessRunner {
 

src/main/java/dk/aau/cs/verification/VerificationOptions.java

@@ -12,9 +12,10 @@ public abstract class VerificationOptions {
 	protected int approximationDenominator;
 	protected boolean useStateequationCheck;
 	protected int extraTokens;
+
 	protected String reducedModelPath;
-    protected String unfoldedModelPath;
-    protected String unfoldedQueriesPath;
+    protected static String unfoldedModelPath;
+    protected static String unfoldedQueriesPath;
 
 	public abstract String toString();
 

src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java

@@ -41,9 +41,11 @@ public VerifyDTAPNOptions(
 			boolean stubbornReduction,
             boolean partition,
             boolean colorFixpoint,
-            boolean unfoldNet
+            boolean unfoldNet,
+			boolean useRawVerification,
+			String rawVerificationOptions
 	) {
-		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction, null, partition, colorFixpoint, unfoldNet);
+		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction, null, partition, colorFixpoint, unfoldNet, useRawVerification, rawVerificationOptions);
 		this.dontUseDeadPlaces = dontUseDeadPlaces;
 	}
 
@@ -69,34 +71,7 @@ public VerifyDTAPNOptions(
             boolean colorFixpoint,
             boolean unfoldNet,
 			boolean useRawVerification,
-			String rawVerificationOptions) {
-				this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction, null, partition, colorFixpoint, unfoldNet);
-
-				this.useRawVerification = useRawVerification;
-				this.rawVerificationOptions = rawVerificationOptions;
-			}
-
-	public VerifyDTAPNOptions(
-			int extraTokens,
-			TraceOption traceOption,
-			SearchOption search,
-			boolean symmetry,
-			boolean gcd,
-			boolean timeDarts,
-			boolean pTrie,
-			boolean useStateequationCheck,
-			boolean discreteInclusion,
-			InclusionPlaces inclusionPlaces,
-			WorkflowMode workflow,
-			long workflowbound,
-			boolean enableOverApproximation,
-			boolean enableUnderApproximation,
-			int approximationDenominator,
-			boolean stubbornReduction,
-            String reducedModelPath,
-            boolean partition,
-            boolean colorFixpoint,
-            boolean unfoldNet
+			String rawVerificationOptions
 	) {
 		super(extraTokens, traceOption, search, symmetry, useStateequationCheck, discreteInclusion, inclusionPlaces, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.timeDarts = timeDarts;
@@ -109,8 +84,10 @@ public VerifyDTAPNOptions(
 		this.partition = partition;
 		this.colorFixpoint = colorFixpoint;
         this.unfold = unfoldNet;
+		this.useRawVerification = useRawVerification;
+		this.rawVerificationOptions = rawVerificationOptions;
 
-        if(unfold && trace() != TraceOption.NONE) // we only force unfolding when traces are involved
+        if(unfold && trace() != TraceOption.NONE && !useRawVerification) // we only force unfolding when traces are involved
         {
             try {
                 unfoldedModelPath = File.createTempFile("unfolded-", ".pnml").getAbsolutePath();
@@ -124,16 +101,15 @@ public VerifyDTAPNOptions(
 	@Override
 	public String toString() {
 		StringBuilder result = new StringBuilder();
-
+	
 		if (useRawVerification) {
-            result.append(rawVerificationOptions);
-            return result.toString();
+            return result.append(rawVerificationOptions).toString();
         }
 
         result.append(kBoundArg());
         result.append(deadTokenArg());
         result.append(traceArg(traceOption));
-        if(trace() != TraceOption.NONE)
+        if(unfold && trace() != TraceOption.NONE)
         {
             result.append(" --write-unfolded-net ");
             result.append(unfoldedModelPath);

src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java

@@ -337,7 +337,7 @@ private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions opt
                     (query.getProperty() instanceof LTLENode && queryResult.value1().isQuerySatisfied()) ||
                     (query.getProperty() instanceof LTLANode && !queryResult.value1().isQuerySatisfied());
 
-                if (options.traceOption() != TraceOption.NONE && isColored && showTrace) {
+                if (options.traceOption() != TraceOption.NONE && isColored && showTrace && options.unfoldedModelPath() != null) {
                     PNMLoader tapnLoader = new PNMLoader();
                     File fileOut = new File(options.unfoldedModelPath());
                     File queriesOut = new File(options.unfoldedQueriesPath());

src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java

@@ -69,36 +69,6 @@ public VerifyPNOptions(
         boolean useColoredReduction,
         boolean useRawVerification,
         String rawVerificationOptions
-    ) {
-        this(extraTokens, traceOption, search, useOverApproximation, modelReduction, enableOverApproximation, enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, pathToReducedNet, useTarOption, useTarjan, colored, unfold, partition, colorFixpoint, useSymmetricVars, useColoredReduction);
-
-        this.useRawVerification = useRawVerification;
-        this.rawVerificationOptions = rawVerificationOptions;
-    }
-
-    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,
-        boolean useTarOption,
-        boolean useTarjan,
-        boolean colored,
-        boolean unfold,
-        boolean partition,
-        boolean colorFixpoint,
-        boolean useSymmetricVars,
-        boolean useColoredReduction
     ) {
 		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, useTarOption);
 
@@ -117,8 +87,10 @@ public VerifyPNOptions(
 		this.reducedModelPath = pathToReducedNet;
 		this.symmetricVars = useSymmetricVars;
 		this.useColoredReduction = useColoredReduction;
+        this.useRawVerification = useRawVerification;
+        this.rawVerificationOptions = rawVerificationOptions;
 
-        if(unfold) {
+        if(unfold && !useRawVerification) {
             try {
                 unfoldedModelPath = File.createTempFile("unfolded-", ".pnml").getAbsolutePath();
                 unfoldedQueriesPath = File.createTempFile("unfoldedQueries-", ".xml").getAbsolutePath();
@@ -151,7 +123,35 @@ public VerifyPNOptions(
         boolean colorFixpoint,
         boolean useSymmetricVars
     ) {
-        this(extraTokens, traceOption, search, useOverApproximation, modelReduction, enableOverApproximation, enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, pathToReducedNet, useTarOption, useTarjan, colored, false, partition, colorFixpoint, useSymmetricVars, false);
+        this(extraTokens, traceOption, search, useOverApproximation, modelReduction, enableOverApproximation, enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, pathToReducedNet, useTarOption, useTarjan, colored, false, partition, colorFixpoint, useSymmetricVars, false, true, null);
+    }
+
+    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,
+        boolean useTarOption,
+        boolean useTarjan,
+        boolean colored,
+        boolean unfold,
+        boolean partition,
+        boolean colorFixpoint,
+        boolean useSymmetricVars,
+        boolean useRawVerification,
+        String rawVerificationOptions
+    ) {
+        this(extraTokens, traceOption, search, useOverApproximation, modelReduction, enableOverApproximation, enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, pathToReducedNet, useTarOption, useTarjan, colored, false, partition, colorFixpoint, useSymmetricVars, false, useRawVerification, rawVerificationOptions);
     }
 
     public VerifyPNOptions(
@@ -182,10 +182,9 @@ public VerifyPNOptions(
     @Override
 	public String toString() {
 		StringBuilder result = new StringBuilder();
-
+    
         if (useRawVerification) {
-            result.append(rawVerificationOptions);
-            return result.toString();
+            return result.append(rawVerificationOptions).toString();
         }
 
 		result.append("--k-bound ");

src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java

@@ -29,9 +29,11 @@ public class VerifyTAPNOptions extends VerificationOptions{
 
 	private static final Map<TraceOption, String> traceMap = createTraceOptionsMap();
 	private static final Map<SearchOption, String> searchMap = createSearchOptionsMap();
-	
-	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+
+	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, boolean useRawVerification, String rawVerificationOptions) {
 		this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
+		this.rawVerificationOptions = rawVerificationOptions;
+		this.useRawVerification = useRawVerification;
 	}
 
     public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
@@ -44,7 +46,7 @@ public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption
 		this.useRawVerification = useRawVerification;
 		this.rawVerificationOptions = rawVerificationOptions;
 
-        if(isColor && trace() != TraceOption.NONE) // we only force unfolding when traces are involved
+        if(isColor && trace() != TraceOption.NONE && !useRawVerification) // we only force unfolding when traces are involved
         {
             try {
                 unfoldedModelPath = File.createTempFile("unfolded-", ".pnml").getAbsolutePath();
@@ -96,10 +98,9 @@ public String deadTokenArg() {
 	@Override
 	public String toString() {
 		StringBuilder result = new StringBuilder();
-
+		
 		if (useRawVerification) {
-            result.append(rawVerificationOptions);
-            return result.toString();
+            return result.append(rawVerificationOptions).toString();
         }
 
         if(unfoldedModelPath != null && unfoldedQueriesPath != null)

src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java

@@ -295,11 +295,11 @@ else if (reductionOption == ReductionOption.VerifyPN || reductionOption == Reduc
 
 	public VerificationOptions getVerificationOptionsFromQuery(net.tapaal.gui.petrinet.verification.TAPNQuery query) {
         if (query.getReductionOption() == ReductionOption.VerifyTAPN) {
-            return new VerifyTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), false, query.discreteInclusion(), query.inclusionPlaces(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());    // XXX DISABLES OverApprox
+            return new VerifyTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), false, query.discreteInclusion(), query.inclusionPlaces(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.isColored(), false, query.getRawVerification(), query.getRawVerificationPrompt());    // XXX DISABLES OverApprox
         } else if (query.getReductionOption() == ReductionOption.VerifyDTAPN) {
-            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(), null, query.usePartitioning(), query.useColorFixpoint(), query.isColored());
+            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(), null, query.usePartitioning(), query.useColorFixpoint(), query.isColored(), query.getRawVerification(), query.getRawVerificationPrompt());
         } else if (query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce) {
-            return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction() ? ModelReduction.AGGRESSIVE : ModelReduction.NO_REDUCTION, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled() ? QueryReductionTime.UnlimitedTime : QueryReductionTime.NoTime, query.isStubbornReductionEnabled(), null, query.isTarOptionEnabled(), query.isTarjan(), query.isColored(), query.usePartitioning(), query.useColorFixpoint(), query.useSymmetricVars());
+            return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction() ? ModelReduction.AGGRESSIVE : ModelReduction.NO_REDUCTION, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled() ? QueryReductionTime.UnlimitedTime : QueryReductionTime.NoTime, query.isStubbornReductionEnabled(), null, query.isTarOptionEnabled(), query.isTarjan(), query.isColored(), false, query.usePartitioning(), query.useColorFixpoint(), query.useSymmetricVars(), query.useColoredReduction(), query.getRawVerification(), query.getRawVerificationPrompt());
         } else {
             return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
         }

src/main/java/net/tapaal/gui/petrinet/dialog/BatchProcessingDialog.java

@@ -1065,7 +1065,6 @@ private void initMonitorPanel() {
 
 	private void process() {
 		tableModel.clear();
-
         currentWorker = new BatchProcessingWorker(files, tableModel, getVerificationOptions());
 
 		currentWorker.addPropertyChangeListener(evt -> {