Merge lp:~tapaal-contributor/tapaal/add-discrete-to-untimed into lp:tapaal

[Lena Ernstsen]

Added the discrete engine to untimed, gamed nets

[Kenneth Yrke Jørgensen (yrke)]

Please check comments for one possible minior issue, just double check that the logic is as intended

review: Needs Fixing

[Jiri Srba (srba)]

I create a simple net for untimed and game lens, ask a simple AF query and the verification ends with error in query parsing. When I save the file and open again, the GUI hals and becomes unresponsive.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/add-discrete-to-untimed]

1102. By lsaid <email address hidden> on 2020-09-17

Fixed logic

1103. By lsaid <email address hidden> on 2020-09-18

Fixed query issue

1104. By lsaid <email address hidden> on 2020-09-18

clean up

[Lena Ernstsen (lsaid)]

Fixed some logic that created bugs in the querydialog

review: Needs Resubmitting

[Jiri Srba (srba)]

In order to make this work, before the untimed game net is sent to verifydtapn engine
there should be added new isolated place, with one token in it and age invariant <=0.
Then the timed engine will be able to mimick the untimed game semantics.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/add-discrete-to-untimed]

1105. By lsaid <email address hidden> on 2020-09-26

Adds an extra place when verifying game/untimed net

1106. By lsaid <email address hidden> on 2020-09-26

Added comment

[Lena Ernstsen (lsaid)]

review: Needs Resubmitting

[lp:~tapaal-contributor/tapaal/add-discrete-to-untimed]

1107. By lsaid <email address hidden> on 2020-09-27

Added token to the ghost place

[Kenneth Yrke Jørgensen (yrke)]

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2020-09-16 19:30:40 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2020-09-27 13:29:30 +0000
@@ -680,6 +680,10 @@
                 q.setReductionOption(ReductionOption.VerifyTAPNdiscreteVerification);
                 q.setUseOverApproximationEnabled(false);
                 q.setUseUnderApproximationEnabled(false);
+            } else if (!tab.lens.isTimed()) {
+                q.setReductionOption(ReductionOption.VerifyPN);
+                q.setUseOverApproximationEnabled(false);
+                q.setUseUnderApproximationEnabled(false);
             }
         }
         String message = "";
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-08-06 13:48:04 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-09-27 13:29:30 +0000
@@ -5,10 +5,8 @@
 import dk.aau.cs.TCTL.TCTLAGNode;
 import dk.aau.cs.TCTL.TCTLEFNode;
 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;
-import dk.aau.cs.model.tapn.TimedPlace;
+import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.model.tapn.*;
 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
 import dk.aau.cs.util.ExecutabilityChecker;
 import dk.aau.cs.util.Tuple;
@@ -27,6 +25,7 @@
 import java.io.InputStream;
 import java.io.InputStreamReader;
 import java.io.StringReader;
+import java.math.BigDecimal;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.regex.Matcher;
@@ -274,6 +273,9 @@
 		//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());
@@ -285,6 +287,13 @@
 		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;
 
@@ -308,7 +317,8 @@
 
 	private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
 		((VerifyTAPNOptions) options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
-		runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
+
+        runner = new ProcessRunner(verifydtapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
 		runner.run();
 
 		if (runner.error()) {
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2020-09-23 11:37:19 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2020-09-27 13:29:30 +0000
@@ -371,10 +371,10 @@
 		TAPNQuery.SearchOption searchOption = getSearchOption();
 		ReductionOption reductionOptionToSet = getReductionOption();
 
-        if (lens.isTimed()) {
+        if (!lens.isGame() && !lens.isTimed()) {
+            return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
+        } else {
             return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
-        } else {
-            return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
         }
     }
 
@@ -690,10 +690,10 @@
                     templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
                 }
             }
-            if (lens.isTimed()) {
+            if (!lens.isGame() && !lens.isTimed()) {
+                updateUntimedQueryButtons(node);
+            } else {
                 updateTimedQueryButtons(node);
-            } else {
-                updateUntimedQueryButtons(node);
             }
         } else if (current instanceof TCTLTransitionNode) {
             TCTLTransitionNode transitionNode = (TCTLTransitionNode) current;
@@ -891,6 +891,8 @@
             }
         } else if (!lens.isGame()) {
             options.add(name_UNTIMED);
+        } else {
+            options.add(name_DISCRETE);
         }
 
 		reductionOption.removeAllItems();
@@ -1199,7 +1201,7 @@
 		queryName.setText(queryToCreateFrom.getName());
 		numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
 
-        if (lens.isTimed()) {
+        if (lens.isTimed() || lens.isGame()) {
             setupQuantificationFromQuery(queryToCreateFrom);
             setupApproximationOptionsFromQuery(queryToCreateFrom);
         }
@@ -1252,7 +1254,7 @@
         reductionOption.addItem(reduction);
         reductionOption.setSelectedItem(reduction);
 
-        if (lens.isTimed()) {
+        if (lens.isTimed() || lens.isGame()) {
             setupTimedReductionOptions(queryToCreateFrom);
         } else {
             setupUntimedReductionOptions(queryToCreateFrom);
@@ -1449,7 +1451,7 @@
 
 		searchOptionsPanel.setVisible(advancedView);
 		reductionOptionsPanel.setVisible(advancedView);
-		if (lens.isTimed()) {
+		if (lens.isTimed() || lens.isGame()) {
 		    saveUppaalXMLButton.setVisible(advancedView);
 		    overApproximationOptionsPanel.setVisible(advancedView);
         }
@@ -1682,7 +1684,7 @@
 		gbc.fill = GridBagConstraints.VERTICAL;
 		queryPanel.add(quantificationPanel, gbc);
 
-		if (lens.isTimed()) {
+		if (lens.isTimed()|| lens.isGame()) {
             addTimedQuantificationListeners();
         } else {
             addUntimedQuantificationListeners();
@@ -1924,7 +1926,7 @@
 		});
 
 		negationButton.addActionListener(e -> {
-            if (lens.isTimed()) {
+            if (lens.isTimed() || lens.isGame()) {
                 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
                 addPropertyToQuery(property);
             } else {
@@ -2045,7 +2047,7 @@
 					for (SharedPlace place : tapnNetwork.sharedPlaces()) {
 						placeNames.add(place.name());
 					}
-                    if (lens.isTimed()) {
+                    if (lens.isTimed() || lens.isGame()) {
                         for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
                             placeNames.add(transition.name());
                         }
@@ -2158,7 +2160,7 @@
 				String template = templateBox.getSelectedItem().toString();
 				if(template.equals(SHARED)) template = "";
 
-                if (lens.isTimed() && transitionIsSelected()) {
+                if ((lens.isTimed() || lens.isGame()) && transitionIsSelected()) {
                     addPropertyToQuery(new TCTLTransitionNode(template, (String) placesBox.getSelectedItem()));
                 } else {
                     TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
@@ -2293,7 +2295,7 @@
 						ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
 						for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
 							for(TimedPlace p : tapn.places()) {
-                                if (lens.isTimed() || !p.isShared()) {
+                                if (lens.isTimed() || !p.isShared() || lens.isGame()) {
                                     templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
                                 }
 							}
@@ -2309,7 +2311,7 @@
 
                         boolean isResultFalse;
 
-                        if (lens.isTimed()) {
+                        if (lens.isTimed() || lens.isGame()) {
                             isResultFalse = !c.getResult();
                         } else {
                             isResultFalse = checkUntimedResult(newQuery) && !c.getResult();
@@ -2535,7 +2537,7 @@
 		gridBagConstraints.anchor = GridBagConstraints.WEST;
 		traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
 
-		if (lens.isTimed()) {
+		if (lens.isTimed() || lens.isGame()) {
             gridBagConstraints.gridy = 2;
             gridBagConstraints.weightx = 1;
             gridBagConstraints.anchor = GridBagConstraints.WEST;
@@ -2671,7 +2673,7 @@
         usePTrie.setToolTipText(TOOL_TIP_PTRIE);
         useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
 
-        if (lens.isTimed()) {
+        if (lens.isTimed() || lens.isGame()) {
             initTimedReductionOptions();
         } else {
             initUntimedReductionOptions();
@@ -2753,7 +2755,7 @@
 	protected void setEnabledOptionsAccordingToCurrentReduction() {
 		refreshQueryEditingButtons();
 		refreshTraceOptions();
-        if (lens.isTimed()) {
+        if (lens.isTimed() || lens.isGame()) {
             refreshSymmetryReduction();
             refreshStubbornReduction();
             refreshDiscreteOptions();