Merge lp:~tapaal-contributor/tapaal/remove-ghost-place into lp:tapaal

[Lena Ernstsen]

Removed ghost places and fixed support for untimed game lenses with verifypn engine

[Kenneth Yrke Jørgensen (yrke)]

Requires new engine and changing all engine options, abandon

Unmerged revisions

1141. By Lena Ernstsen on 2022-06-15

Fixed GUI not supporting gamed nets for verifypn

1140. By Lena Ernstsen on 2022-06-15

Merged with trunk

1139. By Lena Ernstsen on 2021-08-18

Fixed logic

1138. By Lena Ernstsen on 2021-08-18

Changed the engines that can be selected

1137. By Lena Ernstsen on 2021-08-18

Fixed spacing

1136. By Lena Ernstsen on 2021-08-18

Removed unnecessary ghost place

=== 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	2022-06-15 13:47:31 +0000
@@ -11,7 +11,6 @@
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
-import dk.aau.cs.TCTL.*;
 import dk.aau.cs.gui.TabContent;
 import net.tapaal.Preferences;
 import net.tapaal.TAPAAL;
@@ -25,6 +24,8 @@
 import pipe.gui.widgets.InclusionPlaces;
 import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
 import dk.aau.cs.Messenger;
+import dk.aau.cs.TCTL.TCTLAFNode;
+import dk.aau.cs.TCTL.TCTLEGNode;
 import dk.aau.cs.model.tapn.LocalTimedPlace;
 import dk.aau.cs.model.tapn.TAPNQuery;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
@@ -332,16 +333,7 @@
 				} else {
 					ctlOutput = queryResult.value1().isCTL;
 					boolean approximationResult = queryResult.value2().discoveredStates() == 0;	// Result is from over-approximation
-                    TimedArcPetriNetTrace tapnTrace;
-                    if (!errorOutput.contains("Trace") && standardOutput.contains("<trace>")) {
-                        String trace = "Trace:\n";
-                        trace += (standardOutput.split("(?=<trace>)")[1]);
-                        trace = trace.split("(?<=</trace>)")[0];
-					    tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1());
-                    } else {
-                        tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
-
-                    }
+					TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
 					return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput);
 				}
 			}
@@ -404,13 +396,6 @@
 		}
 	
 		public boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options) {
-			if(query.getCategory() == QueryCategory.CTL || query.getCategory() == QueryCategory.LTL){
-				return true;
-			}
-			if(query.getProperty() instanceof TCTLEGNode || query.getProperty() instanceof TCTLAFNode) {
-				return false;
-			}
-			
 			return true;
 		}
 		

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-12-17 21:03:12 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2022-06-15 13:47:31 +0000
@@ -273,9 +273,6 @@
 		//throw new UnsupportedQueryException("Discrete inclusion check only supports upward closed queries.");
 
 		if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
-		if (CreateGui.getCurrentTab().getLens().isGame() && !CreateGui.getCurrentTab().getLens().isTimed()) {
-		    addGhostPlace(model.value1());
-        }
 
 		VerifyTAPNExporter exporter = new VerifyTAPNExporter();
 		ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens(), model.value2());
@@ -287,13 +284,6 @@
 		return verify(options, model, exportedModel, query);
 	}
 
-	//An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics.
-	private void addGhostPlace(TimedArcPetriNet net) {
-	    TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)));
-	    net.add(place);
-        place.addToken(new TimedToken(place, new BigDecimal(0)));
-    }
-
 	private void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
 		VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
 

=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2022-06-03 07:36:58 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2022-06-15 13:47:31 +0000
@@ -924,10 +924,8 @@
                     options.add(engine.nameString);
                 }
             }
-        } else if (!lens.isGame()) {
+        } else {
             options.add(name_UNTIMED);
-        } else {
-            options.add(name_DISCRETE);
         }
 
 		reductionOption.removeAllItems();