Merge lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn into lp:~tapaal-contributor/tapaal/cpn-gui-dev

[Lena Ernstsen]

Calls the verifypn engine when the net is untimed and game

Removed ghost node when the net is untimed and game

[Jiri Srba (srba)]

Approximation options should not be available when the lens is untimed and the state-equation options cannot be enabled and partial-order reduction option is missing.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/redirect-game-engine-cpn]

1552. By Lena Ernstsen on 2022-01-13

Changed visibility of some query options for game nets

1553. By Lena Ernstsen on 2022-01-13

Corrected minor spelling mistake

1554. By Lena Ernstsen on 2022-01-14

Disabled some options for untimed game net queries

Unmerged revisions

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java	2022-01-09 18:33:52 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTACPN.java	2022-01-14 07:59:07 +0000
@@ -31,9 +31,6 @@
         }
 
         if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
-        if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed() && !TAPAALGUI.getCurrentTab().getLens().isColored()) {
-            addGhostPlace(model.value1());
-        }
 
         VerifyTAPNExporter exporter = new VerifyTACPNExporter();
 
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java	2022-01-09 18:33:52 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java	2022-01-14 07:59:07 +0000
@@ -218,9 +218,6 @@
 		}
 
 		if (((VerifyTAPNOptions) options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
-		if (TAPAALGUI.getCurrentTab().getLens().isGame() && !TAPAALGUI.getCurrentTab().getLens().isTimed()) {
-		    addGhostPlace(model.value1());
-        }
 
 		VerifyTAPNExporter exporter = new VerifyTAPNExporter();
 
@@ -233,13 +230,6 @@
 		return verify(options, model, exportedModel, query, dataLayerQuery);
 	}
 
-    //An extra place is added before verifying the query so the timed engine is able to mimic the untimed game semantics.
-	protected void addGhostPlace(TimedArcPetriNet net) {
-	    TimedPlace place = new LocalTimedPlace("ghost", new TimeInvariant(true, new IntBound(0)), ColorType.COLORTYPE_DOT);
-	    net.add(place);
-        place.addToken(new TimedToken(place, new BigDecimal(0), ColorType.COLORTYPE_DOT.getFirstColor()));
-    }
-
 	protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
 		VerifyTAPNOptions verificationOptions = (VerifyTAPNOptions) options;
 
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2022-01-09 14:56:00 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2022-01-14 07:59:07 +0000
@@ -125,14 +125,9 @@
 
 	protected void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
         //remove the net prefix from the place name
-        String placeName;
+        String placeName = mapping.map(p.name()).value2();
         Place guiPlace = null;
 
-        if (mapping.map(p.name()) == null) {
-            placeName = "ghost";
-        } else {
-            placeName = mapping.map(p.name()).value2();
-        }
         for (DataLayer guiModel : guiModels ) {
             guiPlace = guiModel.getPlaceById(placeName);
             if (guiPlace != null) {
 
=== modified file 'src/net/tapaal/TAPAAL.java'
--- src/net/tapaal/TAPAAL.java	2022-01-09 19:10:28 +0000
+++ src/net/tapaal/TAPAAL.java	2022-01-14 07:59:07 +0000
@@ -120,7 +120,7 @@
 		TAPAALGUI.getApp().setVisible(false);
 
 		System.out.println("=============================================================");
-		System.out.println("Batch Porcessing");
+		System.out.println("Batch Processing");
 		System.out.println("=============================================================");
 
 		System.out.println("Running in batch mode for " + batchFolder.getAbsolutePath());
 
=== modified file 'src/net/tapaal/gui/petrinet/dialog/QueryDialog.java'
--- src/net/tapaal/gui/petrinet/dialog/QueryDialog.java	2022-01-10 11:04:27 +0000
+++ src/net/tapaal/gui/petrinet/dialog/QueryDialog.java	2022-01-14 07:59:07 +0000
@@ -159,9 +159,6 @@
 	private JRadioButton randomSearch;
 	private JRadioButton heuristicSearch;
 
-
-
-
 	// Trace options panel
 	private JPanel traceOptionsPanel;
 
@@ -170,8 +167,6 @@
 	private JRadioButton someTraceRadioButton;
 	private JRadioButton fastestTraceRadioButton;
 
-
-
     // Unfolding options panel
     private JPanel verificationPanel;
     private JPanel unfoldingOptionsPanel;
@@ -416,7 +411,7 @@
 		TAPNQuery.SearchOption searchOption = getSearchOption();
 		ReductionOption reductionOptionToSet = getReductionOption();
 
-        if (!lens.isGame() && !lens.isTimed()) {
+        if (!lens.isTimed()) {
             return getUntimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
         } else {
             return getTimedQuery(name, capacity, traceOption, searchOption, reductionOptionToSet);
@@ -749,7 +744,7 @@
                     templateBox.setSelectedItem(tapnNetwork.getTAPNByName(placeNode.getTemplate()));
                 }
             }
-            if (!lens.isGame() && !lens.isTimed()) {
+            if (!lens.isTimed()) {
                 updateUntimedQueryButtons(node);
             } else {
                 updateTimedQueryButtons(node);
@@ -765,7 +760,7 @@
             placeTransitionBox.setSelectedItem(transitionNode.getTransition());
             userChangedAtomicPropSelection = true;
         }
-        if (!lens.isTimed() && !lens.isGame()) {
+        if (!lens.isTimed()) {
             setEnablednessOfOperatorAndMarkingBoxes();
         }
         if (current instanceof LTLANode || current instanceof LTLENode ||
@@ -956,10 +951,8 @@
                     options.add(engine.nameString);
                 }
             }
-        } else if (!lens.isGame()) {
+        } else {
             options.add(name_UNTIMED);
-        } else {
-            options.add(name_DISCRETE);
         }
 
 		reductionOption.removeAllItems();
@@ -1307,13 +1300,20 @@
 
 		setEnabledOptionsAccordingToCurrentReduction();
 		makeShortcuts();
+
+        if (lens.isGame() && !lens.isTimed()) {
+            useReduction.setSelected(false);
+            useReduction.setEnabled(false);
+            useSiphonTrap.setSelected(false);
+            useSiphonTrap.setEnabled(false);
+        }
 	}
 
 	private void setupFromQuery(TAPNQuery queryToCreateFrom) {
 		queryName.setText(queryToCreateFrom.getName());
 		numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity());
 
-        if (lens.isTimed() || lens.isGame()) {
+        if (lens.isTimed()) {
             setupQuantificationFromQuery(queryToCreateFrom);
             setupApproximationOptionsFromQuery(queryToCreateFrom);
         }
@@ -1382,7 +1382,7 @@
         reductionOption.addItem(reduction);
         reductionOption.setSelectedItem(reduction);
 
-        if (lens.isTimed() || lens.isGame()) {
+        if (lens.isTimed()) {
             setupTimedReductionOptions(queryToCreateFrom);
         } else {
             setupUntimedReductionOptions(queryToCreateFrom);
@@ -1458,7 +1458,7 @@
 	}
 
 	private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) {
-        if (!lens.isTimed() && !lens.isGame()) {
+        if (!lens.isTimed()) {
             TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory();
             if (category.equals(TAPNQuery.QueryCategory.CTL)) {
                 queryType.setSelectedIndex(0);
@@ -1605,7 +1605,7 @@
         }
 
 		reductionOptionsPanel.setVisible(advancedView);
-		if (lens.isTimed() || lens.isGame()) {
+		if (lens.isTimed()) {
 		    saveUppaalXMLButton.setVisible(advancedView);
             // Disabled approximation options for colored models, because they are not supported yet (will generate error)
 		    overApproximationOptionsPanel.setVisible(advancedView && !lens.isColored());
@@ -2515,7 +2515,7 @@
 		});
 
 		negationButton.addActionListener(e -> {
-            if (lens.isTimed() || lens.isGame()) {
+            if (lens.isTimed()) {
                 TCTLNotNode property = new TCTLNotNode(getStateProperty(currentSelection.getObject()));
                 addPropertyToQuery(property);
             } else {
@@ -2619,7 +2619,7 @@
 								placeNames.add(place.name());
 							}
 						}
-                        if (!lens.isTimed() && !lens.isGame()) {
+                        if (!lens.isTimed()) {
                             for (TimedTransition transition : tapn.transitions()) {
                                 if (!transition.isShared()) {
                                     placeNames.add(transition.name());
@@ -2641,7 +2641,7 @@
 					for (SharedPlace place : tapnNetwork.sharedPlaces()) {
 						placeNames.add(place.name());
 					}
-                    if (lens.isTimed() || lens.isGame()) {
+                    if (lens.isTimed()) {
                         for (SharedTransition transition : tapnNetwork.sharedTransitions()) {
                             placeNames.add(transition.name());
                         }
@@ -2655,7 +2655,7 @@
                         updateQueryOnAtomicPropositionChange();
                     }
 				}
-                if (!lens.isTimed() && !lens.isGame()) setEnablednessOfOperatorAndMarkingBoxes();
+                if (!lens.isTimed()) setEnablednessOfOperatorAndMarkingBoxes();
 
 			}
 		});
@@ -2692,7 +2692,7 @@
 
         transitionIsEnabledLabel = new JLabel(" is enabled");
         transitionIsEnabledLabel.setPreferredSize(new Dimension(165, 27));
-        if (!lens.isTimed() && !lens.isGame()) placeRow.add(transitionIsEnabledLabel);
+        if (!lens.isTimed()) placeRow.add(transitionIsEnabledLabel);
 
         JPanel addPredicateRow = new JPanel(new FlowLayout(FlowLayout.CENTER));
         gbc.gridy = 2;
@@ -2754,7 +2754,7 @@
 				String template = templateBox.getSelectedItem().toString();
 				if(template.equals(SHARED)) template = "";
 
-                if ((!lens.isTimed() && !lens.isGame()) && transitionIsSelected()) {
+                if ((!lens.isTimed()) && transitionIsSelected()) {
                     addPropertyToQuery(new TCTLTransitionNode(template, (String) placeTransitionBox.getSelectedItem()));
                 } else {
                     TCTLAtomicPropositionNode property = new TCTLAtomicPropositionNode(
@@ -2791,7 +2791,7 @@
 			if (userChangedAtomicPropSelection) {
 				updateQueryOnAtomicPropositionChange();
 			}
-			if (!lens.isTimed() && !lens.isGame()) {
+			if (!lens.isTimed()) {
                 setEnablednessOfOperatorAndMarkingBoxes();
             }
 		});
@@ -2913,7 +2913,7 @@
 
                         boolean isResultFalse;
 
-                        if (lens.isTimed() || lens.isGame()) {
+                        if (lens.isTimed()) {
                             isResultFalse = !placeContext.getResult();
                         } else {
                             isResultFalse = !transitionContext.getResult() || !placeContext.getResult();
@@ -3027,7 +3027,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() || lens.isGame()) {
+                if (lens.isTimed() || !p.isShared()) {
                     templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
                 }
             }
@@ -3047,7 +3047,7 @@
         ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>();
         for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
             for (TimedTransition t : tapn.transitions()) {
-                if (lens.isTimed() || !t.isShared() || lens.isGame()) {
+                if (lens.isTimed() || !t.isShared()) {
                     templateTransitionNames.add(new Tuple<>(tapn.name(), t.name()));
                 }
             }
@@ -3229,7 +3229,7 @@
 		gridBagConstraints.anchor = GridBagConstraints.WEST;
 		traceOptionsPanel.add(fastestTraceRadioButton, gridBagConstraints);
 
-		if (lens.isTimed() || lens.isGame()) {
+		if (lens.isTimed()) {
             gridBagConstraints.gridy = 2;
             gridBagConstraints.weightx = 1;
             gridBagConstraints.anchor = GridBagConstraints.WEST;
@@ -3372,7 +3372,7 @@
 
         useTarjan.addActionListener(e -> updateSearchStrategies());
 
-        if (lens.isTimed() || lens.isGame()) {
+        if (lens.isTimed()) {
             initTimedReductionOptions();
         } else {
             useReduction.addActionListener(new ActionListener() {
@@ -3467,7 +3467,7 @@
 	protected void setEnabledOptionsAccordingToCurrentReduction() {
 		refreshQueryEditingButtons();
 		refreshTraceOptions();
-        if (lens.isTimed() || lens.isGame()) {
+        if (lens.isTimed()) {
             refreshSymmetryReduction();
             refreshStubbornReduction();
             refreshDiscreteOptions();