From b1827d31cd954c7905b617517145d7fc86d9fc2e Mon Sep 17 00:00:00 2001 From: Mikkel Date: Thu, 28 Dec 2023 01:53:06 +0100 Subject: [PATCH 01/50] Fixed bug where raw verifications would be empty when creating new query --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 59fa06281..2d60bcf14 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -1527,8 +1527,10 @@ private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) initRawVerificationOptionsPanel(); initButtonPanel(option); - if(queryToCreateFrom != null) { + if (queryToCreateFrom != null) { setupFromQuery(queryToCreateFrom); + } else { + setupRawVerificationOptionsFromQuery(); } refreshTraceOptions(); @@ -1546,7 +1548,6 @@ private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) refreshUndoRedo(); setEnabledOptionsAccordingToCurrentReduction(); - //setVerificationOptionsEnabled(!queryToCreateFrom.getRawVerification()); makeShortcuts(); @@ -1589,6 +1590,11 @@ private void setupRawVerificationOptionsFromQuery(TAPNQuery queryToCreateFrom) { rawVerificationOptionsTextField.setText(queryToCreateFrom.getRawVerificationPrompt()); } + private void setupRawVerificationOptionsFromQuery() { + rawVerificationOptionsEnabled.setSelected(false); + rawVerificationOptionsTextField.setText("-x 1 "); + } + private void setupTraceListFromQuery(TAPNQuery queryToCreateFrom) { // First remove all elements (removes the default trace that was added) traceModel.removeAllElements(); From 7c90d9e7d87183f156f42b42008bc15bf3d9bf1e Mon Sep 17 00:00:00 2001 From: Mikkel Date: Thu, 28 Dec 2023 02:12:39 +0100 Subject: [PATCH 02/50] Fixed bug where query options would be disabled when using raw verification options --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 2d60bcf14..89024f5f4 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4641,10 +4641,10 @@ private void setAllEnabled(Container container, boolean isEnabled) { protected void setEnabledOptionsAccordingToCurrentReduction() { if (rawVerificationOptionsEnabled.isSelected()) { + refreshQueryEditingButtons(); return; } - refreshQueryEditingButtons(); refreshTraceOptions(); if (lens.isTimed()) { refreshSymmetryReduction(); From 375b87d98089a881bd463fa67f156a8c373b8888 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Thu, 28 Dec 2023 03:46:23 +0100 Subject: [PATCH 03/50] Fixed eof --- .../java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index b4cb555c2..5423bbb68 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -185,6 +185,8 @@ public String toString() { if (useRawVerification) { result.append(rawVerificationOptions); + result.append(" --write-reduced " +reducedModelPath); + return result.toString(); } From 93613d5cb2faef18f75b62b9e4fa67ac133616c1 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sat, 30 Dec 2023 18:10:31 +0100 Subject: [PATCH 04/50] And / or now enabled under ERK example, and also fixed issue where long text would expand the raw verification options field width upon opening and closing the query dialog --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 89024f5f4..1f7ccd340 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -692,7 +692,7 @@ public static TAPNQuery showQueryDialogue(QueryDialogueOption option, TAPNQuery return null; } guiDialog = new EscapableDialog(TAPAALGUI.getApp(), "Edit Query", true); - + Container contentPane = guiDialog.getContentPane(); // 1 Set layout @@ -822,10 +822,15 @@ private void updateQueryButtonsAccordingToSelection() { int selectedIndex = queryType.getSelectedIndex(); if (current instanceof LTLANode || current instanceof LTLENode || ((selectedIndex == 1 || selectedIndex == 2) && current instanceof TCTLPathPlaceHolder)) { + disjunctionButton.setEnabled(true); + conjunctionButton.setEnabled(true); negationButton.setEnabled(false); } else if (!lens.isGame()) { + disjunctionButton.setEnabled(true); + conjunctionButton.setEnabled(true); negationButton.setEnabled(true); } + if (lens.isGame()) { if (newProperty instanceof TCTLAbstractPathProperty && !(newProperty instanceof TCTLPathPlaceHolder)) { enableOnlyStateButtons(); @@ -4532,7 +4537,11 @@ private void initRawVerificationOptionsPanel() { rawVerificationOptionsTextField = new JTextField(); rawVerificationOptionsTextField.setEnabled(false); rawVerificationOptionsTextField.setToolTipText(TOOL_TIP_RAW_VERIFICATION_TEXT_FIELD); - + + Dimension dim = new Dimension(200, 20); + rawVerificationOptionsTextField.setPreferredSize(dim); + rawVerificationOptionsTextField.setMaximumSize(dim); + rawVerificationOptionsHelpButton = new JButton("Help on options"); rawVerificationOptionsHelpButton.setEnabled(false); rawVerificationOptionsHelpButton.setToolTipText(TOOL_TIP_RAW_VERIFICATION_HELP_BUTTON); From 9f1dbe228b5f56e35195919c1cece86b68d6326a Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sat, 30 Dec 2023 18:21:08 +0100 Subject: [PATCH 05/50] Now disables open reduced when using raw verifications --- .../java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 2 -- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 2 ++ 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 5423bbb68..b4cb555c2 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -185,8 +185,6 @@ public String toString() { if (useRawVerification) { result.append(rawVerificationOptions); - result.append(" --write-reduced " +reducedModelPath); - return result.toString(); } diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 59fa06281..7fc2a0c7a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4615,6 +4615,8 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); + openReducedNetButton.setEnabled(isEnabled); + // Reset to original values if (isEnabled) { setEnabledOptionsAccordingToCurrentReduction(); From 132a5b11e61783199b7d4a0d55078ebd03cea26a Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sat, 30 Dec 2023 20:49:13 +0100 Subject: [PATCH 06/50] Now evaluates if open reduced net button should be enabled/disabled correctlly when unchecking the use raw verification options checkbox --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 7fc2a0c7a..eb1e69033 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4620,6 +4620,7 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { // Reset to original values if (isEnabled) { setEnabledOptionsAccordingToCurrentReduction(); + openReducedNetButton.setEnabled(useReduction.isSelected() && getQueryComment().length() > 0 && !newProperty.containsPlaceHolder()); } } @@ -4636,10 +4637,6 @@ private void setAllEnabled(Container container, boolean isEnabled) { } protected void setEnabledOptionsAccordingToCurrentReduction() { - if (rawVerificationOptionsEnabled.isSelected()) { - return; - } - refreshQueryEditingButtons(); refreshTraceOptions(); if (lens.isTimed()) { From 044472d07ca6a21f4f96689f1ebcc09b7e608746 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sat, 30 Dec 2023 21:38:51 +0100 Subject: [PATCH 07/50] Fixed bug where raw verification options would appear when changing trace option, and now correctly refreshes the query button uppon selection --- .../gui/petrinet/dialog/QueryDialog.java | 24 ++++++------------- 1 file changed, 7 insertions(+), 17 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 1f7ccd340..d85fcae0f 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -821,9 +821,7 @@ private void updateQueryButtonsAccordingToSelection() { int selectedIndex = queryType.getSelectedIndex(); if (current instanceof LTLANode || current instanceof LTLENode || - ((selectedIndex == 1 || selectedIndex == 2) && current instanceof TCTLPathPlaceHolder)) { - disjunctionButton.setEnabled(true); - conjunctionButton.setEnabled(true); + ((selectedIndex == 1 || selectedIndex == 2) && current instanceof TCTLPathPlaceHolder)) {; negationButton.setEnabled(false); } else if (!lens.isGame()) { disjunctionButton.setEnabled(true); @@ -1570,12 +1568,12 @@ private void setupFromQuery(TAPNQuery queryToCreateFrom) { numberOfExtraTokensInNet.setValue(queryToCreateFrom.getCapacity()); if (lens.isTimed()) { - setupQuantificationFromQuery(queryToCreateFrom); setupApproximationOptionsFromQuery(queryToCreateFrom); - } - if(lens.isColored() && !lens.isTimed()){ + setupQuantificationFromQuery(queryToCreateFrom); + } else if (lens.isColored()) { setupUnfoldingOptionsFromQuery(queryToCreateFrom); } + setupQueryCategoryFromQuery(queryToCreateFrom); setupSearchOptionsFromQuery(queryToCreateFrom); setupReductionOptionsFromQuery(queryToCreateFrom); @@ -1583,7 +1581,7 @@ private void setupFromQuery(TAPNQuery queryToCreateFrom) { setupTarOptionsFromQuery(queryToCreateFrom); setupTarjanOptionsFromQuery(queryToCreateFrom); - if(queryToCreateFrom.getCategory() == TAPNQuery.QueryCategory.HyperLTL) { + if (queryToCreateFrom.getCategory() == TAPNQuery.QueryCategory.HyperLTL) { setupTraceListFromQuery(queryToCreateFrom); } @@ -4382,7 +4380,7 @@ private void initReductionOptionsPanel() { @Override public void itemStateChanged(ItemEvent e) { if (e.getStateChange() == ItemEvent.SELECTED) { - updateRawVerificationOptions(); + updateRawVerificationOptions(advancedView); guiDialog.pack(); } } @@ -4649,11 +4647,7 @@ private void setAllEnabled(Container container, boolean isEnabled) { } protected void setEnabledOptionsAccordingToCurrentReduction() { - if (rawVerificationOptionsEnabled.isSelected()) { - refreshQueryEditingButtons(); - return; - } - + refreshQueryEditingButtons(); refreshTraceOptions(); if (lens.isTimed()) { refreshSymmetryReduction(); @@ -4682,10 +4676,6 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { guiDialog.pack(); } - private void updateRawVerificationOptions() { - updateRawVerificationOptions(true); - } - private void updateRawVerificationOptions(boolean advancedView) { querySaved = true; TAPNQuery query = getQuery(); From 61f3fa2c2a9917b958b7c5f88de602e5cef8ce9d Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 3 Jan 2024 16:15:25 +0100 Subject: [PATCH 08/50] Fixed bug where buttons would enable again when changing queryType and using raw verification options --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 9b2b02430..3e3462fe5 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -1988,6 +1988,8 @@ private void toggleDialogType() { if (undoButton != null) undoButton.setEnabled(false); if (redoButton != null) redoButton.setEnabled(false); setEnabledOptionsAccordingToCurrentReduction(); + + setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); } private String checkLTLType() { @@ -4628,12 +4630,12 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); - openReducedNetButton.setEnabled(isEnabled); - // Reset to original values if (isEnabled) { setEnabledOptionsAccordingToCurrentReduction(); openReducedNetButton.setEnabled(useReduction.isSelected() && getQueryComment().length() > 0 && !newProperty.containsPlaceHolder()); + } else { + openReducedNetButton.setEnabled(true); } } From 16ac01e9fcfb4795988844348d2412491b4c6e48 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 3 Jan 2024 16:59:41 +0100 Subject: [PATCH 09/50] updated function name --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 3e3462fe5..5696ee3be 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -39,7 +39,6 @@ import dk.aau.cs.TCTL.HyperLTLParsing.TAPAALHyperLTLQueryParser; import dk.aau.cs.TCTL.LTLParsing.TAPAALLTLQueryParser; import dk.aau.cs.TCTL.visitors.*; -import dk.aau.cs.model.CPN.ExpressionSupport.ExprStringPosition; import net.tapaal.gui.petrinet.TAPNLens; import pipe.gui.petrinet.PetriNetTab; import dk.aau.cs.model.CPN.ColorType; @@ -1898,7 +1897,7 @@ private void toggleAdvancedSimpleView(boolean changeState){ } mergeNetComponentsButton.setVisible(advancedView); - updateRawVerificationOptions(advancedView); + showRawVerificationOptions(advancedView); if(advancedView){ advancedButton.setText("Simple view"); @@ -4382,7 +4381,7 @@ private void initReductionOptionsPanel() { @Override public void itemStateChanged(ItemEvent e) { if (e.getStateChange() == ItemEvent.SELECTED) { - updateRawVerificationOptions(advancedView); + showRawVerificationOptions(advancedView); guiDialog.pack(); } } @@ -4681,7 +4680,7 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { guiDialog.pack(); } - private void updateRawVerificationOptions(boolean advancedView) { + private void showRawVerificationOptions(boolean advancedView) { querySaved = true; TAPNQuery query = getQuery(); querySaved = false; From 769ee647ea62356d0feaf6a59f8e6284c3fba3a5 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 3 Jan 2024 17:04:18 +0100 Subject: [PATCH 10/50] Removed extra semi colon --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 5696ee3be..13e378420 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -820,7 +820,7 @@ private void updateQueryButtonsAccordingToSelection() { int selectedIndex = queryType.getSelectedIndex(); if (current instanceof LTLANode || current instanceof LTLENode || - ((selectedIndex == 1 || selectedIndex == 2) && current instanceof TCTLPathPlaceHolder)) {; + ((selectedIndex == 1 || selectedIndex == 2) && current instanceof TCTLPathPlaceHolder)) { negationButton.setEnabled(false); } else if (!lens.isGame()) { disjunctionButton.setEnabled(true); From 4aa0047e02debe96ef61f85937ce63044897f69b Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 4 Jan 2024 16:39:54 +0100 Subject: [PATCH 11/50] Now works for verifypn --- .../gui/petrinet/dialog/QueryDialog.java | 77 +++++++++++++++- .../gui/petrinet/verification/Verifier.java | 90 ++++++++++--------- 2 files changed, 121 insertions(+), 46 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 13e378420..47ad57644 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -51,6 +51,7 @@ import dk.aau.cs.io.NetWriter; import net.tapaal.gui.petrinet.verification.TAPNQuery; import net.tapaal.gui.petrinet.Template; +import net.tapaal.gui.petrinet.dialog.QueryDialog.QueryConstructionEdit; import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; import pipe.gui.*; @@ -455,6 +456,10 @@ public TAPNQuery getQuery() { String name = getQueryComment(); int capacity = getCapacity(); + System.out.println(reductionOption); + System.out.println(reductionOption.getItemCount()); + System.out.println(getReductionOption()); + TAPNQuery.TraceOption traceOption = getTraceOption(); TAPNQuery.SearchOption searchOption = getSearchOption(); ReductionOption reductionOptionToSet = getReductionOption(); @@ -605,7 +610,7 @@ private SearchOption getSearchOption() { } private ReductionOption getReductionOption() { - String reductionOptionString = (String)reductionOption.getSelectedItem(); + String reductionOptionString = getReductionOptionAsString(); if (reductionOptionString == null) return null; else if (reductionOptionString.equals(name_STANDARD)) @@ -1112,7 +1117,7 @@ private void setEnabledReductionOptions(){ } reductionOption.removeAllItems(); - + boolean selectedOptionStillAvailable = false; TraceOption trace = getTraceOption(); for (String s : options) { @@ -2416,6 +2421,9 @@ private void initBoundednessCheckPanel() { gridBagConstraints.gridy = 0; gridBagConstraints.weightx = 0; gridBagConstraints.fill = GridBagConstraints.BOTH; + + numberOfExtraTokensInNet.addChangeListener(e -> updateRawVerificationOptions()); + uppaalOptionsPanel.add(boundednessCheckPanel, gridBagConstraints); } @@ -4206,6 +4214,18 @@ private void initSearchOptionsPanel() { gridBagConstraints.weightx = 1; gridBagConstraints.insets = new Insets(0, 5, 0, 5); gridBagConstraints.fill = GridBagConstraints.BOTH; + + for (Component component : searchOptionsPanel.getComponents()) { + if (component instanceof JRadioButton) { + JRadioButton radioButton = (JRadioButton) component; + radioButton.addItemListener(new ItemListener() { + public void itemStateChanged(ItemEvent e) { + updateRawVerificationOptions(); + } + }); + } + } + uppaalOptionsPanel.add(searchOptionsPanel, gridBagConstraints); } @@ -4242,6 +4262,18 @@ private void initUnfoldingOptionsPanel() { gridBagConstraints.weightx = 1; gridBagConstraints.fill = GridBagConstraints.BOTH; gridBagConstraints.insets = new Insets(0, 0, 0, 5); + + for (Component component : unfoldingOptionsPanel.getComponents()) { + if (component instanceof JCheckBox) { + JCheckBox checkbox = (JCheckBox) component; + checkbox.addItemListener(new ItemListener() { + public void itemStateChanged(ItemEvent e) { + updateRawVerificationOptions(); + } + }); + } + } + verificationPanel.add(unfoldingOptionsPanel, gridBagConstraints); } @@ -4305,8 +4337,19 @@ private void initTraceOptionsPanel() { gridBagConstraints.gridy = 0; gridBagConstraints.weightx = 1; gridBagConstraints.fill = GridBagConstraints.BOTH; - uppaalOptionsPanel.add(traceOptionsPanel, gridBagConstraints); + for (Component component : traceOptionsPanel.getComponents()) { + if (component instanceof JRadioButton) { + JRadioButton radioButton = (JRadioButton) component; + radioButton.addItemListener(new ItemListener() { + public void itemStateChanged(ItemEvent e) { + updateRawVerificationOptions(); + } + }); + } + } + + uppaalOptionsPanel.add(traceOptionsPanel, gridBagConstraints); } private void initOverApproximationPanel() { @@ -4460,6 +4503,18 @@ public void itemStateChanged(ItemEvent e) { gbc.gridy = 0; gbc.weightx = 1; gbc.fill = GridBagConstraints.BOTH; + + for (Component component : reductionOptionsPanel.getComponents()) { + if (component instanceof JCheckBox) { + JCheckBox checkbox = (JCheckBox) component; + checkbox.addItemListener(new ItemListener() { + public void itemStateChanged(ItemEvent e) { + updateRawVerificationOptions(); + } + }); + } + } + verificationPanel.add(reductionOptionsPanel, gbc); } @@ -4695,6 +4750,22 @@ private void showRawVerificationOptions(boolean advancedView) { } } + private void updateRawVerificationOptions() { + querySaved = true; + TAPNQuery query = getQuery(); + querySaved = false; + + query = Verifier.convertQuery(query, lens); + + Verifier.createTempFile(); + + boolean isColored = (lens != null && lens.isColored() || tapnNetwork.isColored()); + VerifyTAPNOptions verifytapnOptions = Verifier.getVerificationOptions(query, isColored); + + System.out.println(verifytapnOptions.toString()); + rawVerificationOptionsTextField.setText(verifytapnOptions.toString()); + } + private void refreshTraceRefinement() { ReductionOption reduction = getReductionOption(); diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java b/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java index 02e0c1473..ad83a07fa 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java @@ -58,7 +58,7 @@ private static VerifyPN getVerifyPN() { return verifypn; } - private static TAPNQuery convertQuery(TAPNQuery query, TAPNLens lens) { + public static TAPNQuery convertQuery(TAPNQuery query, TAPNLens lens) { if (lens == null) return query; TAPNQuery newQuery = query; @@ -222,18 +222,9 @@ public static void runVerifyTAPNVerification( boolean onlyCreateReducedNet, TAPNLens lens) { query = convertQuery(query, lens); - ModelChecker verifytapn = getModelChecker(query); - - try { - reducedNetTempFile = File.createTempFile("reduced-", ".pnml"); - } catch (IOException e) { - new MessengerImpl().displayErrorMessage( - e.getMessage(), - "Error"); - return; - } + if (reducedNetTempFile == null) createTempFile(); if (!verifytapn.isCorrectVersion()) { new MessengerImpl().displayErrorMessage( @@ -244,12 +235,40 @@ public static void runVerifyTAPNVerification( TCTLAbstractProperty inputQuery = query.getProperty(); - int bound = query.getCapacity(); boolean isColored = (lens != null && lens.isColored() || tapnNetwork.isColored()); - VerifyTAPNOptions verifytapnOptions; + VerifyTAPNOptions verifytapnOptions = getVerificationOptions(query, isColored); + + if (inputQuery == null) { + return; + } + + if (tapnNetwork != null) { + RunVerificationBase thread; + if (reducedNetTempFile != null) { + thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, guiModels, reducedNetTempFile.getAbsolutePath(), onlyCreateReducedNet); + } else { + thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, guiModels); + } + + RunningVerificationDialog dialog = new RunningVerificationDialog(TAPAALGUI.getApp(), thread); + if (tapnNetwork.isColored() && query.getTraceOption() != TAPNQuery.TraceOption.NONE) { + SmartDrawDialog.setupWorkerListener(thread); + } + thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), query.getCapacity()), query, lens); + dialog.setVisible(true); + } else { + JOptionPane.showMessageDialog(TAPAALGUI.getApp(), + "There was an error converting the model.", + "Conversion error", JOptionPane.ERROR_MESSAGE); + } + + return; + } + + public static VerifyTAPNOptions getVerificationOptions(TAPNQuery query, boolean isColored) { if (query.getReductionOption() == ReductionOption.VerifyDTAPN) { - verifytapnOptions = new VerifyDTAPNOptions( - bound, + return new VerifyDTAPNOptions( + query.getCapacity(), query.getTraceOption(), query.getSearchOption(), query.useSymmetry(), @@ -271,10 +290,10 @@ public static void runVerifyTAPNVerification( isColored,// Unfold net query.getRawVerification(), query.getRawVerificationPrompt() - ); + ); } else if (query.getReductionOption() == ReductionOption.VerifyPN) { - verifytapnOptions = new VerifyPNOptions( - bound, + return new VerifyPNOptions( + query.getCapacity(), query.getTraceOption(), query.getSearchOption(), query.useOverApproximation(), @@ -300,8 +319,8 @@ public static void runVerifyTAPNVerification( query.getRawVerificationPrompt() ); } else { - verifytapnOptions = new VerifyTAPNOptions( - bound, + return new VerifyTAPNOptions( + query.getCapacity(), query.getTraceOption(), query.getSearchOption(), query.useSymmetry(), @@ -317,31 +336,16 @@ public static void runVerifyTAPNVerification( query.getRawVerificationPrompt() ); } + } - if (inputQuery == null) { + public static void createTempFile() { + try { + reducedNetTempFile = File.createTempFile("reduced-", ".pnml"); + } catch (IOException e) { + new MessengerImpl().displayErrorMessage( + e.getMessage(), + "Error"); return; } - - if (tapnNetwork != null) { - RunVerificationBase thread; - if (reducedNetTempFile != null) { - thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, guiModels, reducedNetTempFile.getAbsolutePath(), onlyCreateReducedNet); - } else { - thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, guiModels); - } - - RunningVerificationDialog dialog = new RunningVerificationDialog(TAPAALGUI.getApp(), thread); - if (tapnNetwork.isColored() && query.getTraceOption() != TAPNQuery.TraceOption.NONE) { - SmartDrawDialog.setupWorkerListener(thread); - } - thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query, lens); - dialog.setVisible(true); - } else { - JOptionPane.showMessageDialog(TAPAALGUI.getApp(), - "There was an error converting the model.", - "Conversion error", JOptionPane.ERROR_MESSAGE); - } - - return; } } From 3ace385ed199d37f9af420ba3e4a3d7902812dc2 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 4 Jan 2024 16:47:34 +0100 Subject: [PATCH 12/50] Now works for verifypn --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 47ad57644..6a6677e1d 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -611,6 +611,7 @@ private SearchOption getSearchOption() { private ReductionOption getReductionOption() { String reductionOptionString = getReductionOptionAsString(); + if (reductionOptionString == null) return null; else if (reductionOptionString.equals(name_STANDARD)) @@ -1638,7 +1639,6 @@ else if (queryToCreateFrom.isUnderApproximationEnabled()) private void setupReductionOptionsFromQuery(TAPNQuery queryToCreateFrom) { String reduction = ""; - boolean symmetry = queryToCreateFrom.useSymmetry(); if (queryToCreateFrom.getReductionOption() == ReductionOption.BROADCAST) { reduction = name_BROADCAST; @@ -1664,6 +1664,8 @@ private void setupReductionOptionsFromQuery(TAPNQuery queryToCreateFrom) { } } + System.out.println(reduction); + reductionOption.addItem(reduction); reductionOption.setSelectedItem(reduction); From ef6cfa8c58ec5bd13d84407d2f0775a9a58aa2a5 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 4 Jan 2024 17:52:58 +0100 Subject: [PATCH 13/50] Refactors --- .../VerifyTAPN/VerifyDTAPNOptions.java | 3 +- .../VerifyTAPN/VerifyPNOptions.java | 5 +- .../VerifyTAPN/VerifyTAPNOptions.java | 2 +- .../gui/petrinet/dialog/QueryDialog.java | 96 +++++++------------ 4 files changed, 42 insertions(+), 64 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 79c503cba..2c331f431 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -124,7 +124,8 @@ public VerifyDTAPNOptions( @Override public String toString() { StringBuilder result = new StringBuilder(); - + System.out.println(rawVerificationOptions); + if (useRawVerification) { result.append(rawVerificationOptions); return result.toString(); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index b4cb555c2..9df00f3f8 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -182,7 +182,7 @@ public VerifyPNOptions( @Override public String toString() { StringBuilder result = new StringBuilder(); - + System.out.println(rawVerificationOptions); if (useRawVerification) { result.append(rawVerificationOptions); return result.toString(); @@ -269,6 +269,9 @@ public String toString() { result.append(" --col-reduction 0 "); } + System.out.println(result); + System.out.println("tokens in model: " + tokensInModel); + return result.toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 26b0f41dd..72e352985 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -96,7 +96,7 @@ public String deadTokenArg() { @Override public String toString() { StringBuilder result = new StringBuilder(); - + System.out.println(rawVerificationOptions); if (useRawVerification) { result.append(rawVerificationOptions); return result.toString(); diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 6a6677e1d..3d32a37d2 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -456,10 +456,6 @@ public TAPNQuery getQuery() { String name = getQueryComment(); int capacity = getCapacity(); - System.out.println(reductionOption); - System.out.println(reductionOption.getItemCount()); - System.out.println(getReductionOption()); - TAPNQuery.TraceOption traceOption = getTraceOption(); TAPNQuery.SearchOption searchOption = getSearchOption(); ReductionOption reductionOptionToSet = getReductionOption(); @@ -1538,7 +1534,7 @@ private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) if (queryToCreateFrom != null) { setupFromQuery(queryToCreateFrom); } else { - setupRawVerificationOptionsFromQuery(); + setupRawVerificationOptions(); } refreshTraceOptions(); @@ -1565,8 +1561,13 @@ private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) useSiphonTrap.setSelected(false); useSiphonTrap.setEnabled(false); } - } + if (queryToCreateFrom != null) { + setupRawVerificationOptions(queryToCreateFrom.getRawVerification()); + } else { + setupRawVerificationOptions(); + } + } private void setupFromQuery(TAPNQuery queryToCreateFrom) { queryName.setText(queryToCreateFrom.getName()); @@ -1589,18 +1590,38 @@ private void setupFromQuery(TAPNQuery queryToCreateFrom) { if (queryToCreateFrom.getCategory() == TAPNQuery.QueryCategory.HyperLTL) { setupTraceListFromQuery(queryToCreateFrom); } + } - setupRawVerificationOptionsFromQuery(queryToCreateFrom); + private void setupRawVerificationOptions() { + setupRawVerificationOptions(false); } - private void setupRawVerificationOptionsFromQuery(TAPNQuery queryToCreateFrom) { - rawVerificationOptionsEnabled.setSelected(queryToCreateFrom.getRawVerification()); - rawVerificationOptionsTextField.setText(queryToCreateFrom.getRawVerificationPrompt()); + private void setupRawVerificationOptions(boolean isSelected) { + rawVerificationOptionsEnabled.setSelected(isSelected); + + addItemListeners(searchOptionsPanel); + addItemListeners(unfoldingOptionsPanel); + addItemListeners(traceOptionsPanel); + addItemListeners(reductionOptionsPanel); + + numberOfExtraTokensInNet.addChangeListener(e -> updateRawVerificationOptions()); + + updateRawVerificationOptions(); } - private void setupRawVerificationOptionsFromQuery() { - rawVerificationOptionsEnabled.setSelected(false); - rawVerificationOptionsTextField.setText("-x 1 "); + private void addItemListeners(JPanel panel) { + if (panel != null) { + for (Component component : panel.getComponents()) { + if (component instanceof JRadioButton || component instanceof JCheckBox) { + AbstractButton button = (AbstractButton) component; + button.addItemListener(new ItemListener() { + public void itemStateChanged(ItemEvent e) { + updateRawVerificationOptions(); + } + }); + } + } + } } private void setupTraceListFromQuery(TAPNQuery queryToCreateFrom) { @@ -1664,8 +1685,6 @@ private void setupReductionOptionsFromQuery(TAPNQuery queryToCreateFrom) { } } - System.out.println(reduction); - reductionOption.addItem(reduction); reductionOption.setSelectedItem(reduction); @@ -2424,8 +2443,6 @@ private void initBoundednessCheckPanel() { gridBagConstraints.weightx = 0; gridBagConstraints.fill = GridBagConstraints.BOTH; - numberOfExtraTokensInNet.addChangeListener(e -> updateRawVerificationOptions()); - uppaalOptionsPanel.add(boundednessCheckPanel, gridBagConstraints); } @@ -4217,17 +4234,6 @@ private void initSearchOptionsPanel() { gridBagConstraints.insets = new Insets(0, 5, 0, 5); gridBagConstraints.fill = GridBagConstraints.BOTH; - for (Component component : searchOptionsPanel.getComponents()) { - if (component instanceof JRadioButton) { - JRadioButton radioButton = (JRadioButton) component; - radioButton.addItemListener(new ItemListener() { - public void itemStateChanged(ItemEvent e) { - updateRawVerificationOptions(); - } - }); - } - } - uppaalOptionsPanel.add(searchOptionsPanel, gridBagConstraints); } @@ -4265,17 +4271,6 @@ private void initUnfoldingOptionsPanel() { gridBagConstraints.fill = GridBagConstraints.BOTH; gridBagConstraints.insets = new Insets(0, 0, 0, 5); - for (Component component : unfoldingOptionsPanel.getComponents()) { - if (component instanceof JCheckBox) { - JCheckBox checkbox = (JCheckBox) component; - checkbox.addItemListener(new ItemListener() { - public void itemStateChanged(ItemEvent e) { - updateRawVerificationOptions(); - } - }); - } - } - verificationPanel.add(unfoldingOptionsPanel, gridBagConstraints); } @@ -4340,17 +4335,6 @@ private void initTraceOptionsPanel() { gridBagConstraints.weightx = 1; gridBagConstraints.fill = GridBagConstraints.BOTH; - for (Component component : traceOptionsPanel.getComponents()) { - if (component instanceof JRadioButton) { - JRadioButton radioButton = (JRadioButton) component; - radioButton.addItemListener(new ItemListener() { - public void itemStateChanged(ItemEvent e) { - updateRawVerificationOptions(); - } - }); - } - } - uppaalOptionsPanel.add(traceOptionsPanel, gridBagConstraints); } @@ -4506,17 +4490,6 @@ public void itemStateChanged(ItemEvent e) { gbc.weightx = 1; gbc.fill = GridBagConstraints.BOTH; - for (Component component : reductionOptionsPanel.getComponents()) { - if (component instanceof JCheckBox) { - JCheckBox checkbox = (JCheckBox) component; - checkbox.addItemListener(new ItemListener() { - public void itemStateChanged(ItemEvent e) { - updateRawVerificationOptions(); - } - }); - } - } - verificationPanel.add(reductionOptionsPanel, gbc); } @@ -4766,6 +4739,7 @@ private void updateRawVerificationOptions() { System.out.println(verifytapnOptions.toString()); rawVerificationOptionsTextField.setText(verifytapnOptions.toString()); + rawVerificationOptionsTextField.setCaretPosition(0); } private void refreshTraceRefinement() { From 0865d31a46e6f337e8b2e58a65016b9643862a12 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 4 Jan 2024 18:39:24 +0100 Subject: [PATCH 14/50] Fixed k-bound bug --- .../VerifyTAPN/VerifyDTAPNOptions.java | 1 - .../verification/VerifyTAPN/VerifyPNOptions.java | 5 +---- .../VerifyTAPN/VerifyTAPNOptions.java | 2 +- .../tapaal/gui/petrinet/dialog/QueryDialog.java | 15 ++++++++++++--- 4 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 2c331f431..8e8a30beb 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -124,7 +124,6 @@ public VerifyDTAPNOptions( @Override public String toString() { StringBuilder result = new StringBuilder(); - System.out.println(rawVerificationOptions); if (useRawVerification) { result.append(rawVerificationOptions); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 9df00f3f8..1d111ec5e 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -182,7 +182,7 @@ public VerifyPNOptions( @Override public String toString() { StringBuilder result = new StringBuilder(); - System.out.println(rawVerificationOptions); + if (useRawVerification) { result.append(rawVerificationOptions); return result.toString(); @@ -269,9 +269,6 @@ public String toString() { result.append(" --col-reduction 0 "); } - System.out.println(result); - System.out.println("tokens in model: " + tokensInModel); - return result.toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 72e352985..8bdaaa196 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -96,7 +96,7 @@ public String deadTokenArg() { @Override public String toString() { StringBuilder result = new StringBuilder(); - System.out.println(rawVerificationOptions); + if (useRawVerification) { result.append(rawVerificationOptions); return result.toString(); diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 3d32a37d2..efd2b7ca2 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -1563,7 +1563,7 @@ private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) } if (queryToCreateFrom != null) { - setupRawVerificationOptions(queryToCreateFrom.getRawVerification()); + setupRawVerificationOptionsFromQuery(queryToCreateFrom); } else { setupRawVerificationOptions(); } @@ -1592,6 +1592,11 @@ private void setupFromQuery(TAPNQuery queryToCreateFrom) { } } + private void setupRawVerificationOptionsFromQuery(TAPNQuery queryToCreateFrom) { + rawVerificationOptionsTextField.setText(queryToCreateFrom.getRawVerificationPrompt()); + setupRawVerificationOptions(queryToCreateFrom.getRawVerification()); + } + private void setupRawVerificationOptions() { setupRawVerificationOptions(false); } @@ -1605,8 +1610,11 @@ private void setupRawVerificationOptions(boolean isSelected) { addItemListeners(reductionOptionsPanel); numberOfExtraTokensInNet.addChangeListener(e -> updateRawVerificationOptions()); + reductionOption.addActionListener(e -> updateRawVerificationOptions()); - updateRawVerificationOptions(); + if (reductionOption.getSelectedItem() != null) { + updateRawVerificationOptions(); + } } private void addItemListeners(JPanel panel) { @@ -2015,6 +2023,7 @@ private void toggleDialogType() { setEnabledOptionsAccordingToCurrentReduction(); setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); + updateRawVerificationOptions(); } private String checkLTLType() { @@ -4736,8 +4745,8 @@ private void updateRawVerificationOptions() { boolean isColored = (lens != null && lens.isColored() || tapnNetwork.isColored()); VerifyTAPNOptions verifytapnOptions = Verifier.getVerificationOptions(query, isColored); + verifytapnOptions.setTokensInModel(((TimedArcPetriNet) templateBox.getSelectedItem()).getNumberOfTokensInNet()); - System.out.println(verifytapnOptions.toString()); rawVerificationOptionsTextField.setText(verifytapnOptions.toString()); rawVerificationOptionsTextField.setCaretPosition(0); } From 04948f2071d1f5e0a48941a892446759a008eb2c Mon Sep 17 00:00:00 2001 From: mtygesen Date: Sun, 7 Jan 2024 16:48:02 +0100 Subject: [PATCH 15/50] Changed raw verification field into text area --- .../gui/petrinet/dialog/QueryDialog.java | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index efd2b7ca2..a8b1d5845 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -214,7 +214,7 @@ public enum QueryDialogueOption { private JCheckBox useTarjan; // Raw verification options panel private JPanel rawVerificationOptionsPanel; - private JTextField rawVerificationOptionsTextField; + private JTextArea rawVerificationOptionsTextArea; private JCheckBox rawVerificationOptionsEnabled; private JButton rawVerificationOptionsHelpButton; @@ -506,7 +506,7 @@ private TAPNQuery getTimedQuery(String name, int capacity, TraceOption traceOpti lens.isColored(), false, rawVerificationOptionsEnabled.isSelected(), - rawVerificationOptionsTextField.getText() + rawVerificationOptionsTextArea.getText() ); query.setUseStubbornReduction(useStubbornReduction.isSelected()); @@ -546,7 +546,7 @@ private TAPNQuery getUntimedQuery(String name, ArrayList traceList, int lens.isColored(), coloredReduction, rawVerificationOptionsEnabled.isSelected(), - rawVerificationOptionsTextField.getText() + rawVerificationOptionsTextArea.getText() ); if (queryType.getSelectedIndex() == 1) { query.setCategory(TAPNQuery.QueryCategory.LTL); @@ -1593,7 +1593,7 @@ private void setupFromQuery(TAPNQuery queryToCreateFrom) { } private void setupRawVerificationOptionsFromQuery(TAPNQuery queryToCreateFrom) { - rawVerificationOptionsTextField.setText(queryToCreateFrom.getRawVerificationPrompt()); + rawVerificationOptionsTextArea.setText(queryToCreateFrom.getRawVerificationPrompt()); setupRawVerificationOptions(queryToCreateFrom.getRawVerification()); } @@ -4572,13 +4572,13 @@ private void initRawVerificationOptionsPanel() { rawVerificationOptionsEnabled = new JCheckBox("Use"); rawVerificationOptionsEnabled.setToolTipText(TOOL_TIP_RAW_VERIFICATION_ENABLED_CHECKBOX); - rawVerificationOptionsTextField = new JTextField(); - rawVerificationOptionsTextField.setEnabled(false); - rawVerificationOptionsTextField.setToolTipText(TOOL_TIP_RAW_VERIFICATION_TEXT_FIELD); + rawVerificationOptionsTextArea = new JTextArea(); + rawVerificationOptionsTextArea.setEnabled(false); + rawVerificationOptionsTextArea.setToolTipText(TOOL_TIP_RAW_VERIFICATION_TEXT_FIELD); - Dimension dim = new Dimension(200, 20); - rawVerificationOptionsTextField.setPreferredSize(dim); - rawVerificationOptionsTextField.setMaximumSize(dim); + rawVerificationOptionsTextArea.setLineWrap(true); + rawVerificationOptionsTextArea.setWrapStyleWord(true); + rawVerificationOptionsTextArea.setRows(2); rawVerificationOptionsHelpButton = new JButton("Help on options"); rawVerificationOptionsHelpButton.setEnabled(false); @@ -4588,7 +4588,7 @@ private void initRawVerificationOptionsPanel() { @Override public void itemStateChanged(ItemEvent e) { setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); - rawVerificationOptionsTextField.setEnabled(rawVerificationOptionsEnabled.isSelected()); + rawVerificationOptionsTextArea.setEnabled(rawVerificationOptionsEnabled.isSelected()); rawVerificationOptionsHelpButton.setEnabled(rawVerificationOptionsEnabled.isSelected()); } }); @@ -4611,7 +4611,7 @@ public void itemStateChanged(ItemEvent e) { buttonGbc.insets = new Insets(0, 0, 0, 5); rawVerificationOptionsPanel.add(rawVerificationOptionsEnabled, checkBoxGbc); - rawVerificationOptionsPanel.add(rawVerificationOptionsTextField, textAreaGbc); + rawVerificationOptionsPanel.add(rawVerificationOptionsTextArea, textAreaGbc); rawVerificationOptionsPanel.add(rawVerificationOptionsHelpButton, buttonGbc); GridBagConstraints gbc = new GridBagConstraints(); @@ -4747,8 +4747,8 @@ private void updateRawVerificationOptions() { VerifyTAPNOptions verifytapnOptions = Verifier.getVerificationOptions(query, isColored); verifytapnOptions.setTokensInModel(((TimedArcPetriNet) templateBox.getSelectedItem()).getNumberOfTokensInNet()); - rawVerificationOptionsTextField.setText(verifytapnOptions.toString()); - rawVerificationOptionsTextField.setCaretPosition(0); + rawVerificationOptionsTextArea.setText(verifytapnOptions.toString()); + rawVerificationOptionsTextArea.setCaretPosition(0); } private void refreshTraceRefinement() { From 369d57f516d5582bc78acd4368789d31b89bacd3 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Sun, 7 Jan 2024 16:48:14 +0100 Subject: [PATCH 16/50] Changed raw verification field into text area --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index a8b1d5845..109bd96b6 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4578,7 +4578,6 @@ private void initRawVerificationOptionsPanel() { rawVerificationOptionsTextArea.setLineWrap(true); rawVerificationOptionsTextArea.setWrapStyleWord(true); - rawVerificationOptionsTextArea.setRows(2); rawVerificationOptionsHelpButton = new JButton("Help on options"); rawVerificationOptionsHelpButton.setEnabled(false); From 60660404fdae3b083fbdc8182818a85c0cdab19d Mon Sep 17 00:00:00 2001 From: mtygesen Date: Mon, 8 Jan 2024 17:27:08 +0100 Subject: [PATCH 17/50] updated text area in raw verification options --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 13 ++++++++----- .../net/tapaal/gui/petrinet/widgets/QueryPane.java | 2 +- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 109bd96b6..1995b08c0 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -51,7 +51,6 @@ import dk.aau.cs.io.NetWriter; import net.tapaal.gui.petrinet.verification.TAPNQuery; import net.tapaal.gui.petrinet.Template; -import net.tapaal.gui.petrinet.dialog.QueryDialog.QueryConstructionEdit; import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; import pipe.gui.*; @@ -1522,7 +1521,6 @@ private void updateTraceBox(TCTLAbstractPathProperty node) { // ///////////////////////////////////////////////////////////////////// private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) { - //setPreferredSize(new Dimension(942, 517)); initQueryNamePanel(); initQueryPanel(); initUppaalOptionsPanel(); @@ -1821,6 +1819,7 @@ public void changedUpdate(DocumentEvent e) { advancedButton = new JButton("Advanced view"); advancedButton.setToolTipText(TOOL_TIP_ADVANCED_VIEW_BUTTON); + advancedView = false; advancedButton.addActionListener(arg0 -> toggleAdvancedSimpleView(true)); JButton infoButton = new JButton("Help on the query options"); @@ -1940,7 +1939,7 @@ private void toggleAdvancedSimpleView(boolean changeState){ advancedButton.setText("Advanced view"); advancedButton.setToolTipText(TOOL_TIP_ADVANCED_VIEW_BUTTON); } - + guiDialog.pack(); guiDialog.setLocation(location); } @@ -4575,9 +4574,11 @@ private void initRawVerificationOptionsPanel() { rawVerificationOptionsTextArea = new JTextArea(); rawVerificationOptionsTextArea.setEnabled(false); rawVerificationOptionsTextArea.setToolTipText(TOOL_TIP_RAW_VERIFICATION_TEXT_FIELD); - rawVerificationOptionsTextArea.setLineWrap(true); rawVerificationOptionsTextArea.setWrapStyleWord(true); + rawVerificationOptionsTextArea.setRows(4); + + JScrollPane rawVerificationOptionsScrollPane = new JScrollPane(rawVerificationOptionsTextArea); rawVerificationOptionsHelpButton = new JButton("Help on options"); rawVerificationOptionsHelpButton.setEnabled(false); @@ -4610,7 +4611,7 @@ public void itemStateChanged(ItemEvent e) { buttonGbc.insets = new Insets(0, 0, 0, 5); rawVerificationOptionsPanel.add(rawVerificationOptionsEnabled, checkBoxGbc); - rawVerificationOptionsPanel.add(rawVerificationOptionsTextArea, textAreaGbc); + rawVerificationOptionsPanel.add(rawVerificationOptionsScrollPane, textAreaGbc); rawVerificationOptionsPanel.add(rawVerificationOptionsHelpButton, buttonGbc); GridBagConstraints gbc = new GridBagConstraints(); @@ -4731,6 +4732,8 @@ private void showRawVerificationOptions(boolean advancedView) { } else { rawVerificationOptionsPanel.setVisible(advancedView); } + + guiDialog.pack(); } private void updateRawVerificationOptions() { diff --git a/src/main/java/net/tapaal/gui/petrinet/widgets/QueryPane.java b/src/main/java/net/tapaal/gui/petrinet/widgets/QueryPane.java index 37e90df96..e314db851 100644 --- a/src/main/java/net/tapaal/gui/petrinet/widgets/QueryPane.java +++ b/src/main/java/net/tapaal/gui/petrinet/widgets/QueryPane.java @@ -450,7 +450,7 @@ public void selectFirst() { private void verifyQuery() { TAPNQuery query = queryList.getSelectedValue(); int NumberOfSelectedElements = queryList.getSelectedIndices().length; - + if (NumberOfSelectedElements == 1) { if (query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyDTAPN || query.getReductionOption() == ReductionOption.VerifyPN) Verifier.runVerifyTAPNVerification(tabContent.network(), query, null, tabContent.getGuiModels(), false, tabContent.lens); From bb75aefc5d00610908dd3cca0f3a1a86fab37f2c Mon Sep 17 00:00:00 2001 From: mtygesen Date: Mon, 8 Jan 2024 18:02:31 +0100 Subject: [PATCH 18/50] now opens in advanced view if query using raw verification options --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 1995b08c0..82e501c29 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -422,7 +422,6 @@ private QueryDialog(EscapableDialog me, QueryDialogueOption option, TAPNQuery qu setLayout(new GridBagLayout()); - init(option, queryToCreateFrom); makeShortcuts(); toggleAdvancedSimpleView(false); @@ -1593,6 +1592,10 @@ private void setupFromQuery(TAPNQuery queryToCreateFrom) { private void setupRawVerificationOptionsFromQuery(TAPNQuery queryToCreateFrom) { rawVerificationOptionsTextArea.setText(queryToCreateFrom.getRawVerificationPrompt()); setupRawVerificationOptions(queryToCreateFrom.getRawVerification()); + + if (rawVerificationOptionsEnabled.isSelected() && !advancedView) { + toggleAdvancedSimpleView(true); + } } private void setupRawVerificationOptions() { @@ -1819,7 +1822,6 @@ public void changedUpdate(DocumentEvent e) { advancedButton = new JButton("Advanced view"); advancedButton.setToolTipText(TOOL_TIP_ADVANCED_VIEW_BUTTON); - advancedView = false; advancedButton.addActionListener(arg0 -> toggleAdvancedSimpleView(true)); JButton infoButton = new JButton("Help on the query options"); From e077b9081625c373c46cabd0a49508165fa9d0e5 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 9 Jan 2024 17:33:22 +0100 Subject: [PATCH 19/50] Restructured raw verification layout --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 82e501c29..8c4ca922a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4604,13 +4604,14 @@ public void itemStateChanged(ItemEvent e) { textAreaGbc.gridx = 1; textAreaGbc.gridy = 0; textAreaGbc.weightx = 1; + textAreaGbc.gridheight = 2; textAreaGbc.fill = GridBagConstraints.HORIZONTAL; textAreaGbc.insets = new Insets(0, 10, 0, 10); GridBagConstraints buttonGbc = new GridBagConstraints(); - buttonGbc.gridx = 2; - buttonGbc.gridy = 0; - buttonGbc.insets = new Insets(0, 0, 0, 5); + buttonGbc.gridx = 0; + buttonGbc.gridy = 1; + buttonGbc.insets = new Insets(0, 5, 0, 0); rawVerificationOptionsPanel.add(rawVerificationOptionsEnabled, checkBoxGbc); rawVerificationOptionsPanel.add(rawVerificationOptionsScrollPane, textAreaGbc); @@ -4621,7 +4622,7 @@ public void itemStateChanged(ItemEvent e) { gbc.gridy = 6; gbc.weightx = 1; gbc.gridwidth = 2; - gbc.insets = new Insets(5,10,5,10); + gbc.insets = new Insets(5, 10, 5, 10); gbc.fill = GridBagConstraints.BOTH; add(rawVerificationOptionsPanel, gbc); } @@ -4673,9 +4674,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { // Reset to original values if (isEnabled) { setEnabledOptionsAccordingToCurrentReduction(); - openReducedNetButton.setEnabled(useReduction.isSelected() && getQueryComment().length() > 0 && !newProperty.containsPlaceHolder()); - } else { - openReducedNetButton.setEnabled(true); } } From 8cf62c285c62896ef34b0db39ff9ff20c5487978 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 9 Jan 2024 17:37:28 +0100 Subject: [PATCH 20/50] Removed redundant inset --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 8c4ca922a..18afe629c 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4598,7 +4598,6 @@ public void itemStateChanged(ItemEvent e) { GridBagConstraints checkBoxGbc = new GridBagConstraints(); checkBoxGbc.gridx = 0; checkBoxGbc.gridy = 0; - checkBoxGbc.insets = new Insets(0, 5, 0, 0); GridBagConstraints textAreaGbc = new GridBagConstraints(); textAreaGbc.gridx = 1; From 96ae244d88058915650884430f0727f61258647e Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 9 Jan 2024 19:56:30 +0100 Subject: [PATCH 21/50] Fixed mismatching tmp file names --- .../java/dk/aau/cs/verification/VerificationOptions.java | 5 +++-- .../aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 3 +-- .../java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java | 2 +- .../dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 3 +-- .../aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java | 7 +++---- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 2 +- .../net/tapaal/gui/petrinet/verification/Verifier.java | 4 ++-- 7 files changed, 12 insertions(+), 14 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerificationOptions.java b/src/main/java/dk/aau/cs/verification/VerificationOptions.java index b97b8e0d2..ecc7193b9 100644 --- a/src/main/java/dk/aau/cs/verification/VerificationOptions.java +++ b/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(); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 8e8a30beb..f7219e398 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -126,8 +126,7 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - result.append(rawVerificationOptions); - return result.toString(); + return result.append(rawVerificationOptions).toString(); } result.append(kBoundArg()); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java index 898987a79..64e5c54e3 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java @@ -337,7 +337,7 @@ private VerificationResult 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()); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 1d111ec5e..24c44ae61 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -184,8 +184,7 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - result.append(rawVerificationOptions); - return result.toString(); + return result.append(rawVerificationOptions).toString(); } result.append("--k-bound "); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 8bdaaa196..437c2ae0f 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -29,7 +29,7 @@ public class VerifyTAPNOptions extends VerificationOptions{ private static final Map traceMap = createTraceOptionsMap(); private static final Map searchMap = createSearchOptionsMap(); - + 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); } @@ -44,7 +44,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(); @@ -98,8 +98,7 @@ 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) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 18afe629c..85a349ee8 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4748,8 +4748,8 @@ private void updateRawVerificationOptions() { VerifyTAPNOptions verifytapnOptions = Verifier.getVerificationOptions(query, isColored); verifytapnOptions.setTokensInModel(((TimedArcPetriNet) templateBox.getSelectedItem()).getNumberOfTokensInNet()); + System.out.println(verifytapnOptions.toString()); rawVerificationOptionsTextArea.setText(verifytapnOptions.toString()); - rawVerificationOptionsTextArea.setCaretPosition(0); } private void refreshTraceRefinement() { diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java b/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java index ad83a07fa..56caf8f0e 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java @@ -287,7 +287,7 @@ public static VerifyTAPNOptions getVerificationOptions(TAPNQuery query, boolean reducedNetTempFile.getAbsolutePath(), query.usePartitioning(), query.useColorFixpoint(), - isColored,// Unfold net + isColored && !query.getRawVerification(),// Unfold net query.getRawVerification(), query.getRawVerificationPrompt() ); @@ -310,7 +310,7 @@ public static VerifyTAPNOptions getVerificationOptions(TAPNQuery query, boolean query.isTarOptionEnabled(), query.isTarjan(), isColored, - isColored && query.getTraceOption() != TAPNQuery.TraceOption.NONE, + isColored && query.getTraceOption() != TAPNQuery.TraceOption.NONE && !query.getRawVerification(), query.usePartitioning(), query.useColorFixpoint(), query.useSymmetricVars(), From 5e87acb69a62ba171cee6cbdc48a87ebfe072b7b Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 9 Jan 2024 19:59:30 +0100 Subject: [PATCH 22/50] removed log --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 85a349ee8..6c8595094 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4748,7 +4748,6 @@ private void updateRawVerificationOptions() { VerifyTAPNOptions verifytapnOptions = Verifier.getVerificationOptions(query, isColored); verifytapnOptions.setTokensInModel(((TimedArcPetriNet) templateBox.getSelectedItem()).getNumberOfTokensInNet()); - System.out.println(verifytapnOptions.toString()); rawVerificationOptionsTextArea.setText(verifytapnOptions.toString()); } From af292bc258c606132a307d3af1870510664865a8 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 9 Jan 2024 20:08:58 +0100 Subject: [PATCH 23/50] Made code more clear --- .../dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 2 +- .../dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 2 +- .../java/net/tapaal/gui/petrinet/verification/Verifier.java | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index f7219e398..302686e8f 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -110,7 +110,7 @@ public VerifyDTAPNOptions( this.colorFixpoint = colorFixpoint; this.unfold = unfoldNet; - 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(); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 24c44ae61..1f03d1944 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -118,7 +118,7 @@ public VerifyPNOptions( this.symmetricVars = useSymmetricVars; this.useColoredReduction = useColoredReduction; - if(unfold) { + if(unfold && !useRawVerification) { try { unfoldedModelPath = File.createTempFile("unfolded-", ".pnml").getAbsolutePath(); unfoldedQueriesPath = File.createTempFile("unfoldedQueries-", ".xml").getAbsolutePath(); diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java b/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java index 56caf8f0e..ad83a07fa 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/Verifier.java @@ -287,7 +287,7 @@ public static VerifyTAPNOptions getVerificationOptions(TAPNQuery query, boolean reducedNetTempFile.getAbsolutePath(), query.usePartitioning(), query.useColorFixpoint(), - isColored && !query.getRawVerification(),// Unfold net + isColored,// Unfold net query.getRawVerification(), query.getRawVerificationPrompt() ); @@ -310,7 +310,7 @@ public static VerifyTAPNOptions getVerificationOptions(TAPNQuery query, boolean query.isTarOptionEnabled(), query.isTarjan(), isColored, - isColored && query.getTraceOption() != TAPNQuery.TraceOption.NONE && !query.getRawVerification(), + isColored && query.getTraceOption() != TAPNQuery.TraceOption.NONE, query.usePartitioning(), query.useColorFixpoint(), query.useSymmetricVars(), From 8a2cee3441e5c46a5b116992f5f5570bb6e4826f Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 11 Jan 2024 17:16:08 +0100 Subject: [PATCH 24/50] Fixed bug where state of useRawVerification was firstly updated second time --- .../VerifyTAPN/VerifyDTAPNOptions.java | 33 +++--------------- .../VerifyTAPN/VerifyPNOptions.java | 34 ++----------------- .../BatchProcessingWorker.java | 2 +- 3 files changed, 8 insertions(+), 61 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 302686e8f..4a71277e9 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -43,7 +43,7 @@ public VerifyDTAPNOptions( boolean colorFixpoint, boolean 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); + this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction, null, partition, colorFixpoint, unfoldNet, true, null); this.dontUseDeadPlaces = dontUseDeadPlaces; } @@ -69,34 +69,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,6 +82,8 @@ public VerifyDTAPNOptions( this.partition = partition; this.colorFixpoint = colorFixpoint; this.unfold = unfoldNet; + this.useRawVerification = useRawVerification; + this.rawVerificationOptions = rawVerificationOptions; if(unfold && trace() != TraceOption.NONE && !useRawVerification) // we only force unfolding when traces are involved { diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 1f03d1944..29d82050b 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/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,6 +87,8 @@ public VerifyPNOptions( this.reducedModelPath = pathToReducedNet; this.symmetricVars = useSymmetricVars; this.useColoredReduction = useColoredReduction; + this.useRawVerification = useRawVerification; + this.rawVerificationOptions = rawVerificationOptions; if(unfold && !useRawVerification) { try { @@ -151,7 +123,7 @@ 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( diff --git a/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java b/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java index 1e1aaf151..87f3aac7c 100644 --- a/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java +++ b/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java @@ -297,7 +297,7 @@ public VerificationOptions getVerificationOptionsFromQuery(net.tapaal.gui.petrin 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 } 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(), true, null); } 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()); } else { From f7828afcd928df304e853128c86640b5d0daeafb Mon Sep 17 00:00:00 2001 From: mtygesen Date: Fri, 12 Jan 2024 17:07:52 +0100 Subject: [PATCH 25/50] Now correctly disables/enables components when selecting parts of a query --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 6c8595094..b54146f9f 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -780,7 +780,6 @@ private void updateSelection() { queryField.select(position.getStart(), position.getEnd()); currentSelection = position; setEnabledOptionsAccordingToCurrentReduction(); - updateQueryButtonsAccordingToSelection(); } // update selection based on some change to the query. @@ -2018,12 +2017,12 @@ private void toggleDialogType() { wasLTLType = false; wasHyperLTLType = false; } + if (undoManager != null) undoManager.discardAllEdits(); if (undoButton != null) undoButton.setEnabled(false); if (redoButton != null) redoButton.setEnabled(false); - setEnabledOptionsAccordingToCurrentReduction(); - setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); + setEnabledOptionsAccordingToCurrentReduction(); updateRawVerificationOptions(); } @@ -4669,11 +4668,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(boundednessCheckPanel, isEnabled); setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); - - // Reset to original values - if (isEnabled) { - setEnabledOptionsAccordingToCurrentReduction(); - } } // Enables or disables the container + all children recursively @@ -4715,6 +4709,8 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { updateSearchStrategies(); refreshExportButtonText(); + setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); + guiDialog.pack(); } From 84fb967db8cbf0a6235b494196acd3ca6ba72fa8 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Sat, 13 Jan 2024 21:04:12 +0100 Subject: [PATCH 26/50] Now correctly enables/disables options when opening new query and when changing query type --- .../tapaal/gui/petrinet/dialog/QueryDialog.java | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index b54146f9f..a9a01eeff 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -1529,8 +1529,6 @@ private void init(QueryDialogueOption option, final TAPNQuery queryToCreateFrom) if (queryToCreateFrom != null) { setupFromQuery(queryToCreateFrom); - } else { - setupRawVerificationOptions(); } refreshTraceOptions(); @@ -1786,10 +1784,8 @@ private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) { } private void initQueryNamePanel() { - JPanel splitter = new JPanel(new BorderLayout()); - namePanel = new JPanel(new FlowLayout()); namePanel.add(new JLabel("Query name: ")); @@ -1799,22 +1795,19 @@ private void initQueryNamePanel() { namePanel.add(queryName); queryName.getDocument().addDocumentListener(new DocumentListener() { - public void removeUpdate(DocumentEvent e) { setSaveButtonsEnabled(); - } public void insertUpdate(DocumentEvent e) { setSaveButtonsEnabled(); - } public void changedUpdate(DocumentEvent e) { setSaveButtonsEnabled(); - } }); + queryType = new JComboBox(new String[]{"CTL/Reachability", "LTL","HyperLTL"}); queryType.setToolTipText(TOOL_TIP_QUERY_TYPE); queryType.addActionListener(arg0 -> toggleDialogType()); @@ -2916,6 +2909,7 @@ private void showCTLButtons(boolean isVisible) { } private void updateSiphonTrap(boolean isLTL) { + useSiphonTrap.setSelected(!isLTL); useSiphonTrap.setEnabled(!isLTL); } @@ -4668,6 +4662,8 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(boundednessCheckPanel, isEnabled); setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); + + setEnabledOptionsAccordingToCurrentReduction(); } // Enables or disables the container + all children recursively @@ -4709,8 +4705,6 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { updateSearchStrategies(); refreshExportButtonText(); - setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); - guiDialog.pack(); } From 0487d6fefbd6700d758f0606b8eaf9788d753890 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Mon, 15 Jan 2024 23:59:25 +0100 Subject: [PATCH 27/50] Fixed NPE --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index a9a01eeff..7ca7884c3 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -509,7 +509,7 @@ private TAPNQuery getTimedQuery(String name, int capacity, TraceOption traceOpti query.setUseStubbornReduction(useStubbornReduction.isSelected()); - if(reductionOptionToSet.equals(ReductionOption.VerifyTAPN)){ + if (reductionOptionToSet != null && reductionOptionToSet.equals(ReductionOption.VerifyTAPN)) { query.setDiscreteInclusion(discreteInclusion.isSelected()); } return query; @@ -1609,7 +1609,7 @@ private void setupRawVerificationOptions(boolean isSelected) { numberOfExtraTokensInNet.addChangeListener(e -> updateRawVerificationOptions()); reductionOption.addActionListener(e -> updateRawVerificationOptions()); - + if (reductionOption.getSelectedItem() != null) { updateRawVerificationOptions(); } @@ -2909,7 +2909,6 @@ private void showCTLButtons(boolean isVisible) { } private void updateSiphonTrap(boolean isLTL) { - useSiphonTrap.setSelected(!isLTL); useSiphonTrap.setEnabled(!isLTL); } From 859af021360aa2fdb0859e38f32ab5aa1975f0ec Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 16 Jan 2024 21:54:28 +0100 Subject: [PATCH 28/50] fix --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 7ca7884c3..44cc9dea9 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -779,7 +779,8 @@ private void updateSelection() { queryField.select(position.getStart(), position.getEnd()); currentSelection = position; - setEnabledOptionsAccordingToCurrentReduction(); + + refreshQueryEditingButtons(); } // update selection based on some change to the query. @@ -4662,7 +4663,7 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); - setEnabledOptionsAccordingToCurrentReduction(); + //setEnabledOptionsAccordingToCurrentReduction(); } // Enables or disables the container + all children recursively From 90046f0ab17593f7b47449f431bf87fa35ecf66c Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 16 Jan 2024 21:57:00 +0100 Subject: [PATCH 29/50] fixed issue where not all options would be disabled correctly when using raw verifications --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 44cc9dea9..27b59337d 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4662,8 +4662,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(boundednessCheckPanel, isEnabled); setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); - - //setEnabledOptionsAccordingToCurrentReduction(); } // Enables or disables the container + all children recursively From d70e3b088636faf808c5f1dda42fb29aa7ad6698 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 17 Jan 2024 00:12:22 +0100 Subject: [PATCH 30/50] now correctly enables the options again when toggling the use button on/off --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 27b59337d..5fb4eba71 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4662,6 +4662,10 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(boundednessCheckPanel, isEnabled); setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); + + if (isEnabled) { + setEnabledOptionsAccordingToCurrentReduction(); + } } // Enables or disables the container + all children recursively From c9fd4cbd839c1849d38f49e439186c382aadc750 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 17 Jan 2024 19:02:29 +0100 Subject: [PATCH 31/50] Added guard to refreshOverApproximationOption so it exits immediatly if raw verifications is selected --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 5fb4eba71..5f2461d37 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4663,9 +4663,7 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(searchOptionsPanel, isEnabled); setAllEnabled(overApproximationOptionsPanel, isEnabled); - if (isEnabled) { - setEnabledOptionsAccordingToCurrentReduction(); - } + setEnabledOptionsAccordingToCurrentReduction(); } // Enables or disables the container + all children recursively @@ -4681,6 +4679,10 @@ private void setAllEnabled(Container container, boolean isEnabled) { } protected void setEnabledOptionsAccordingToCurrentReduction() { + if (rawVerificationOptionsEnabled.isSelected()) { + return; + } + refreshQueryEditingButtons(); refreshTraceOptions(); if (lens.isTimed()) { @@ -4866,6 +4868,10 @@ else if((reductionOption.getSelectedItem().equals(name_COMBI) || } private void refreshOverApproximationOption() { + if (rawVerificationOptionsEnabled.isSelected()) { + return; + } + if (queryHasDeadlock() || newProperty.toString().contains("EG") || newProperty.toString().contains("AF")){ skeletonAnalysis.setSelected(false); skeletonAnalysis.setEnabled(false); From e4132cbb4d14f304ced2b0dba10d94a40126ceb1 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 18 Jan 2024 14:55:18 +0100 Subject: [PATCH 32/50] Fixed issue with siphon trap and use color reductions --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 5f2461d37..d9bffa2da 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4699,12 +4699,15 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { traceBoxQuantification.setEnabled(traceBoxQuantification.getModel().getSize() > 0); } } + if (!lens.isColored()) { useColoredReduction.setSelected(false); useColoredReduction.setEnabled(false); - } else { - useColoredReduction.setEnabled(true); } + + wasLTLType = queryType.getSelectedIndex() == 1; + updateSiphonTrap(wasLTLType); + updateStubbornReduction(); updateSearchStrategies(); refreshExportButtonText(); From e93b4d816e9527c1f953e5f12f757b6db2bbe8de Mon Sep 17 00:00:00 2001 From: mtygesen Date: Sat, 20 Jan 2024 23:33:15 +0100 Subject: [PATCH 33/50] Fixed unfolded paths being added to non-colored nets using DTAPN --- .../dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 4a71277e9..16fdd1c78 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -107,7 +107,7 @@ public String 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); From 977084c7db97c5213ecf594857079b7c6f8098b1 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Mon, 22 Jan 2024 16:27:19 +0100 Subject: [PATCH 34/50] use colored reduction now only visible for colored nets --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index d9bffa2da..8ff7964b9 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4540,9 +4540,13 @@ private void initUntimedReductionOptions() { reductionOptionsPanel.add(useReduction, gbc); gbc.gridx = 0; gbc.gridy = 2; - reductionOptionsPanel.add(useColoredReduction, gbc); - gbc.gridx = 0; - gbc.gridy = 3; + + if (lens.isColored()) { + reductionOptionsPanel.add(useColoredReduction, gbc); + gbc.gridx = 0; + gbc.gridy = 3; + } + reductionOptionsPanel.add(useQueryReduction, gbc); gbc.gridx = 1; gbc.gridy = 1; From 3895112da2bbb3ab61bfea93d250a4a4c07e2285 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Tue, 23 Jan 2024 18:49:55 +0100 Subject: [PATCH 35/50] Fixed issue with verifying multiple queries at once, and "use stubborn reduction" --- .../java/dk/aau/cs/verification/ProcessRunner.java | 1 - .../batchProcessing/BatchProcessingWorker.java | 6 +++--- .../gui/petrinet/dialog/BatchProcessingDialog.java | 1 - .../tapaal/gui/petrinet/dialog/QueryDialog.java | 14 ++------------ 4 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/ProcessRunner.java b/src/main/java/dk/aau/cs/verification/ProcessRunner.java index d2280b864..833ee19e5 100644 --- a/src/main/java/dk/aau/cs/verification/ProcessRunner.java +++ b/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 { diff --git a/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java b/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java index 87f3aac7c..899d8204d 100644 --- a/src/main/java/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java +++ b/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(), true, null); + 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()); } diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/BatchProcessingDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/BatchProcessingDialog.java index e8522abba..44af9665f 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/BatchProcessingDialog.java +++ b/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 -> { diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 8ff7964b9..a3c87ed54 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -2913,16 +2913,6 @@ private void updateSiphonTrap(boolean isLTL) { useSiphonTrap.setEnabled(!isLTL); } - private void updateStubbornReduction() { - int selectedIndex = queryType.getSelectedIndex(); - if(selectedIndex == 2) { - useStubbornReduction.setEnabled(false); - useStubbornReduction.setSelected(false); - } else { - useStubbornReduction.setEnabled(true); - } - } - private void addPropertyToQuery(TCTLAbstractPathProperty property) { TCTLAbstractProperty selection = currentSelection.getObject(); if (selection instanceof TCTLAbstractStateProperty) { @@ -4689,6 +4679,7 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { refreshQueryEditingButtons(); refreshTraceOptions(); + if (lens.isTimed()) { refreshSymmetryReduction(); refreshStubbornReduction(); @@ -4711,8 +4702,7 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { wasLTLType = queryType.getSelectedIndex() == 1; updateSiphonTrap(wasLTLType); - - updateStubbornReduction(); + updateSearchStrategies(); refreshExportButtonText(); From 76e9cf2cd4d4e5511a1b946f94f4c16d1175cb61 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 24 Jan 2024 17:02:34 +0100 Subject: [PATCH 36/50] Use trace refinement and siphon trap analysis now only available for CTL --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index a3c87ed54..f1d00580d 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -2909,8 +2909,8 @@ private void showCTLButtons(boolean isVisible) { existsUntil.setVisible(isVisible); } - private void updateSiphonTrap(boolean isLTL) { - useSiphonTrap.setEnabled(!isLTL); + private void updateSiphonTrap(boolean isCTL) { + useSiphonTrap.setEnabled(isCTL); } private void addPropertyToQuery(TCTLAbstractPathProperty property) { @@ -4700,8 +4700,8 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { useColoredReduction.setEnabled(false); } - wasLTLType = queryType.getSelectedIndex() == 1; - updateSiphonTrap(wasLTLType); + wasCTLType = queryType.getSelectedIndex() == 0; + updateSiphonTrap(wasCTLType); updateSearchStrategies(); refreshExportButtonText(); @@ -4745,7 +4745,7 @@ private void updateRawVerificationOptions() { private void refreshTraceRefinement() { ReductionOption reduction = getReductionOption(); - if (queryType.getSelectedIndex() != 1 && !lens.isGame() && + if (queryType.getSelectedIndex() == 0 && !lens.isGame() && reduction != null && reduction.equals(ReductionOption.VerifyPN) && (newProperty.toString().startsWith("AG") || newProperty.toString().startsWith("EF")) && !hasInhibitorArcs && !newProperty.hasNestedPathQuantifiers()) { From 143dd7ea2ba6a71f9bacbaf33e385da809ae2b68 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 24 Jan 2024 22:38:05 +0100 Subject: [PATCH 37/50] Fixes Kbound analysis and LTL / HyperLTL focus --- .../VerifyTAPN/VerifyDTAPNOptions.java | 6 ++-- .../VerifyTAPN/VerifyPNOptions.java | 28 +++++++++++++++++++ .../VerifyTAPN/VerifyTAPNOptions.java | 4 ++- .../gui/petrinet/dialog/QueryDialog.java | 4 ++- .../petrinet/verification/KBoundAnalyzer.java | 6 ++-- 5 files changed, 41 insertions(+), 7 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 16fdd1c78..db38d98b9 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/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, true, null); + 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; } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 29d82050b..677dc19da 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -126,6 +126,34 @@ public VerifyPNOptions( 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( int extraTokens, TraceOption traceOption, diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 437c2ae0f..85b0b507e 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -30,8 +30,10 @@ public class VerifyTAPNOptions extends VerificationOptions{ private static final Map traceMap = createTraceOptionsMap(); private static final Map 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) { diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index f1d00580d..4efbbde2a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4673,11 +4673,12 @@ private void setAllEnabled(Container container, boolean isEnabled) { } protected void setEnabledOptionsAccordingToCurrentReduction() { + refreshQueryEditingButtons(); + if (rawVerificationOptionsEnabled.isSelected()) { return; } - refreshQueryEditingButtons(); refreshTraceOptions(); if (lens.isTimed()) { @@ -4813,6 +4814,7 @@ private void refreshExportButtonText() { } private void refreshQueryEditingButtons() { + System.out.println("here"); if (currentSelection != null) { if (lens.isGame()) { if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) { diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/KBoundAnalyzer.java b/src/main/java/net/tapaal/gui/petrinet/verification/KBoundAnalyzer.java index 609bcf519..7cd482e9c 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/KBoundAnalyzer.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/KBoundAnalyzer.java @@ -77,15 +77,15 @@ public void analyze(VerifyTAPNOptions options, boolean resultShown) { protected VerifyTAPNOptions verificationOptions() { if(modelChecker instanceof VerifyPN){ - return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.CTL, AlgorithmOption.CERTAIN_ZERO, false, QueryReductionTime.NoTime,false, null, false, true, tapnNetwork.isColored(), false, true, true, true); + return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.CTL, AlgorithmOption.CERTAIN_ZERO, false, QueryReductionTime.NoTime,false, null, false, true, tapnNetwork.isColored(), false, true, true, true, dataLayerQuery.getRawVerification(), dataLayerQuery.getRawVerificationPrompt()); } else if(modelChecker instanceof VerifyTAPN){ - return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1); + return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1, dataLayerQuery.getRawVerification(), dataLayerQuery.getRawVerificationPrompt()); } else if(modelChecker instanceof VerifyDTAPN){ //gdc and dart can be used together with game boolean gcd = !lens.isGame(); boolean dart = !tapnNetwork.hasUrgentTransitions() && !lens.isGame(); - return new VerifyDTAPNOptions(true, k, TraceOption.NONE, SearchOption.BFS, true, gcd, dart, true, false, false, 1, false, true, true, tapnNetwork.isColored()); + return new VerifyDTAPNOptions(true, k, TraceOption.NONE, SearchOption.BFS, true, gcd, dart, true, false, false, 1, false, true, true, tapnNetwork.isColored(), dataLayerQuery.getRawVerification(), dataLayerQuery.getRawVerificationPrompt()); } return null; } From c270579ce15ce4040169165623250f37d4802f89 Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 25 Jan 2024 01:32:52 +0100 Subject: [PATCH 38/50] removed debug log --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 4efbbde2a..fab521362 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4814,7 +4814,6 @@ private void refreshExportButtonText() { } private void refreshQueryEditingButtons() { - System.out.println("here"); if (currentSelection != null) { if (lens.isGame()) { if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) { From 65a32ea3b13fc6ccef1930c4b5ba4ec6f6ed38bd Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 25 Jan 2024 14:50:23 +0100 Subject: [PATCH 39/50] Fixed bug with add predicates button --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index fab521362..a379da71a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -800,12 +800,14 @@ private void updateSelection(TCTLAbstractProperty newSelection) { queryField.select(position.getStart(), position.getEnd()); currentSelection = position; + + updateQueryButtonsAccordingToSelection(); + if (currentSelection != null) { setEnabledOptionsAccordingToCurrentReduction(); } else { disableAllQueryButtons(); } - updateQueryButtonsAccordingToSelection(); } private void updateQueryButtonsAccordingToSelection() { From d3d863728aac319c2ca63bf08ee27c014c349353 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Fri, 26 Jan 2024 12:32:01 +0100 Subject: [PATCH 40/50] Now logic buttons should be enabled/disabled correctly --- .../gui/petrinet/dialog/QueryDialog.java | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index a379da71a..b6c989875 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -835,15 +835,16 @@ private void updateQueryButtonsAccordingToSelection() { enableOnlyStateButtons(); negationButton.setEnabled(false); } - if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { - disjunctionButton.setEnabled(false); - conjunctionButton.setEnabled(false); - negationButton.setEnabled(false); - } else { - disjunctionButton.setEnabled(true); - conjunctionButton.setEnabled(true); - negationButton.setEnabled(true); - } + } + + if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { + disjunctionButton.setEnabled(false); + conjunctionButton.setEnabled(false); + negationButton.setEnabled(false); + } else { + disjunctionButton.setEnabled(true); + conjunctionButton.setEnabled(true); + negationButton.setEnabled(true); } } @@ -1249,7 +1250,6 @@ private void disableAllLTLButtons() { untilButton.setEnabled(false); aButton.setEnabled(false); eButton.setEnabled(false); - conjunctionButton.setEnabled(false); disjunctionButton.setEnabled(false); negationButton.setEnabled(false); From 5b9add66b27d9746e8a1770d9691d65a9be0c817 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sat, 27 Jan 2024 01:47:03 +0100 Subject: [PATCH 41/50] Now allows multiple quantifiers for non-game untimed nets --- .../gui/petrinet/dialog/QueryDialog.java | 20 ++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index b6c989875..58882103d 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -830,18 +830,20 @@ private void updateQueryButtonsAccordingToSelection() { negationButton.setEnabled(true); } - if (lens.isGame()) { - if (newProperty instanceof TCTLAbstractPathProperty && !(newProperty instanceof TCTLPathPlaceHolder)) { + if (lens.isGame() && + newProperty instanceof TCTLAbstractPathProperty && + !(newProperty instanceof TCTLPathPlaceHolder)) { enableOnlyStateButtons(); - negationButton.setEnabled(false); - } } - if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { - disjunctionButton.setEnabled(false); - conjunctionButton.setEnabled(false); - negationButton.setEnabled(false); - } else { + if (lens.isGame() || lens.isTimed()) { + if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { + disjunctionButton.setEnabled(false); + conjunctionButton.setEnabled(false); + negationButton.setEnabled(false); + return; + } + disjunctionButton.setEnabled(true); conjunctionButton.setEnabled(true); negationButton.setEnabled(true); From 8584b40ea3c37bb88028827ca031226b4ee879ff Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sat, 27 Jan 2024 17:29:12 +0100 Subject: [PATCH 42/50] Updated when logic buttons are enabled --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 58882103d..8408a0624 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -836,10 +836,16 @@ private void updateQueryButtonsAccordingToSelection() { enableOnlyStateButtons(); } - if (lens.isGame() || lens.isTimed()) { + if (lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) { if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { disjunctionButton.setEnabled(false); conjunctionButton.setEnabled(false); + + if (!lens.isGame() && lens.isTimed()) { + negationButton.setEnabled(true); + return; + } + negationButton.setEnabled(false); return; } From 5bb553d14517d104411115afed92ac84734ab2bf Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 28 Jan 2024 01:56:41 +0100 Subject: [PATCH 43/50] Now allows boolean operators for until quantifier --- .../net/tapaal/gui/petrinet/dialog/QueryDialog.java | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 8408a0624..b32e3720d 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -838,15 +838,10 @@ private void updateQueryButtonsAccordingToSelection() { if (lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) { if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { - disjunctionButton.setEnabled(false); - conjunctionButton.setEnabled(false); + disjunctionButton.setEnabled(current instanceof LTLUNode); + conjunctionButton.setEnabled(current instanceof LTLUNode); + negationButton.setEnabled(!lens.isGame() && lens.isTimed()); - if (!lens.isGame() && lens.isTimed()) { - negationButton.setEnabled(true); - return; - } - - negationButton.setEnabled(false); return; } From 170d6135f1952174a1eff3e95dc5956ee23d4f49 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 28 Jan 2024 02:27:05 +0100 Subject: [PATCH 44/50] Now also enables boolean operators for X, G, and F --- .../gui/petrinet/dialog/QueryDialog.java | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index b32e3720d..d2b057692 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -820,16 +820,6 @@ private void updateQueryButtonsAccordingToSelection() { setEnablednessOfOperatorAndMarkingBoxes(); } - int selectedIndex = queryType.getSelectedIndex(); - if (current instanceof LTLANode || current instanceof LTLENode || - ((selectedIndex == 1 || selectedIndex == 2) && current instanceof TCTLPathPlaceHolder)) { - negationButton.setEnabled(false); - } else if (!lens.isGame()) { - disjunctionButton.setEnabled(true); - conjunctionButton.setEnabled(true); - negationButton.setEnabled(true); - } - if (lens.isGame() && newProperty instanceof TCTLAbstractPathProperty && !(newProperty instanceof TCTLPathPlaceHolder)) { @@ -838,9 +828,11 @@ private void updateQueryButtonsAccordingToSelection() { if (lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) { if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { - disjunctionButton.setEnabled(current instanceof LTLUNode); - conjunctionButton.setEnabled(current instanceof LTLUNode); - negationButton.setEnabled(!lens.isGame() && lens.isTimed()); + boolean enableBooleanOperators = !(current instanceof LTLANode || current instanceof LTLENode) && queryType.getSelectedIndex() != 0; + + disjunctionButton.setEnabled(enableBooleanOperators); + conjunctionButton.setEnabled(enableBooleanOperators); + negationButton.setEnabled(enableBooleanOperators || !lens.isGame() && lens.isTimed()); return; } From 50cae6ac19fd612d1d8c0f033ac60dc3caace05c Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 28 Jan 2024 02:38:24 +0100 Subject: [PATCH 45/50] Simplified logic --- .../gui/petrinet/dialog/QueryDialog.java | 22 +++++++------------ 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index d2b057692..640b719d4 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -826,20 +826,14 @@ private void updateQueryButtonsAccordingToSelection() { enableOnlyStateButtons(); } - if (lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) { - if (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { - boolean enableBooleanOperators = !(current instanceof LTLANode || current instanceof LTLENode) && queryType.getSelectedIndex() != 0; - - disjunctionButton.setEnabled(enableBooleanOperators); - conjunctionButton.setEnabled(enableBooleanOperators); - negationButton.setEnabled(enableBooleanOperators || !lens.isGame() && lens.isTimed()); - - return; - } - - disjunctionButton.setEnabled(true); - conjunctionButton.setEnabled(true); - negationButton.setEnabled(true); + if ((lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) && + current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { + + boolean enableBooleanOperators = !(current instanceof LTLANode || current instanceof LTLENode) && queryType.getSelectedIndex() != 0; + + disjunctionButton.setEnabled(enableBooleanOperators); + conjunctionButton.setEnabled(enableBooleanOperators); + negationButton.setEnabled(enableBooleanOperators || !lens.isGame() && lens.isTimed()); } } From 09a1d9b363a4ea4d93825570a1f2678241e445b6 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 28 Jan 2024 20:25:15 +0100 Subject: [PATCH 46/50] Fixed boolean operators not enabled in some cases --- .../dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 1 + .../dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 1 + .../dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java | 1 + src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 4 ++-- 4 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index db38d98b9..8d518a2e2 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -139,6 +139,7 @@ public String toString() { result.append(gcd ? " --gcd-lower " : ""); // GCD optimization is not sound for workflow analysis } + result.append(" --bindings"); return result.toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 677dc19da..c67eeadff 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -268,6 +268,7 @@ public String toString() { result.append(" --col-reduction 0 "); } + result.append(" --bindings"); return result.toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 85b0b507e..2e637b42b 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -122,6 +122,7 @@ public String toString() { result.append(' '); result.append(discreteInclusion ? " --inclusion-check 1" : ""); result.append(discreteInclusion ? " --inclusion-places " + generateDiscretePlacesList() : ""); + result.append(" --bindings"); return result.toString(); } diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 640b719d4..48f7356e6 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -827,13 +827,13 @@ private void updateQueryButtonsAccordingToSelection() { } if ((lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) && - current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder) { + (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder)) { boolean enableBooleanOperators = !(current instanceof LTLANode || current instanceof LTLENode) && queryType.getSelectedIndex() != 0; disjunctionButton.setEnabled(enableBooleanOperators); conjunctionButton.setEnabled(enableBooleanOperators); - negationButton.setEnabled(enableBooleanOperators || !lens.isGame() && lens.isTimed()); + negationButton.setEnabled(enableBooleanOperators); } } From ba3c35a28d7c77cc6e3ea1dd0a73b01ef83da417 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 28 Jan 2024 20:31:59 +0100 Subject: [PATCH 47/50] Enable buttons if the condition is not met to ensure correct state in the case of future changes --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 48f7356e6..fcdd5b986 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -834,6 +834,10 @@ private void updateQueryButtonsAccordingToSelection() { disjunctionButton.setEnabled(enableBooleanOperators); conjunctionButton.setEnabled(enableBooleanOperators); negationButton.setEnabled(enableBooleanOperators); + } else { + disjunctionButton.setEnabled(true); + conjunctionButton.setEnabled(true); + negationButton.setEnabled(true); } } From 61a63495237144eec2c6bff7da625336761bd555 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 28 Jan 2024 21:10:09 +0100 Subject: [PATCH 48/50] Removed binding flag --- .../dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 1 - .../java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 1 - .../dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java | 1 - 3 files changed, 3 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 8d518a2e2..db38d98b9 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -139,7 +139,6 @@ public String toString() { result.append(gcd ? " --gcd-lower " : ""); // GCD optimization is not sound for workflow analysis } - result.append(" --bindings"); return result.toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index c67eeadff..677dc19da 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -268,7 +268,6 @@ public String toString() { result.append(" --col-reduction 0 "); } - result.append(" --bindings"); return result.toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 2e637b42b..85b0b507e 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -122,7 +122,6 @@ public String toString() { result.append(' '); result.append(discreteInclusion ? " --inclusion-check 1" : ""); result.append(discreteInclusion ? " --inclusion-places " + generateDiscretePlacesList() : ""); - result.append(" --bindings"); return result.toString(); } From f496b1c6ae543b22cce3f3ff352d044eb80d7bb3 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Mon, 29 Jan 2024 21:42:32 +0100 Subject: [PATCH 49/50] Fixed problems with LTL/hyperLTL --- .../gui/petrinet/dialog/QueryDialog.java | 39 +++++++++++++------ 1 file changed, 28 insertions(+), 11 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index fcdd5b986..c72a77b36 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -828,16 +828,15 @@ private void updateQueryButtonsAccordingToSelection() { if ((lens.isGame() || lens.isTimed() || queryType.getSelectedIndex() != 0) && (current instanceof TCTLAbstractPathProperty || newProperty instanceof TCTLPathPlaceHolder)) { - - boolean enableBooleanOperators = !(current instanceof LTLANode || current instanceof LTLENode) && queryType.getSelectedIndex() != 0; - + boolean enableBooleanOperators = !(current instanceof LTLANode || current instanceof LTLENode) && queryType.getSelectedIndex() != 0 && isValidLTL(); + disjunctionButton.setEnabled(enableBooleanOperators); conjunctionButton.setEnabled(enableBooleanOperators); negationButton.setEnabled(enableBooleanOperators); - } else { + } else if (queryType.getSelectedIndex() == 0) { disjunctionButton.setEnabled(true); conjunctionButton.setEnabled(true); - negationButton.setEnabled(true); + negationButton.setEnabled(true); } } @@ -1945,8 +1944,9 @@ private boolean isHyperLTL(TCTLAbstractProperty property) { private void toggleDialogType() { if (queryType.getSelectedIndex() == 2 && (wasCTLType || wasLTLType)) { - if (!isHyperLTL(newProperty) && !(newProperty instanceof TCTLPathPlaceHolder)) { + if (!isHyperLTL(newProperty) && !(newProperty instanceof TCTLPathPlaceHolder) || !isValidLTL() && !queryField.getText().trim().equals((new TCTLPathPlaceHolder()).toString())) { if (showWarningMessage() == JOptionPane.YES_OPTION) { + newProperty = new TCTLPathPlaceHolder(); deleteProperty(); } else { int changeTo = wasCTLType ? 0 : 1; @@ -1959,6 +1959,7 @@ private void toggleDialogType() { showHyperLTL(true); updateSiphonTrap(true); queryChanged(); + wasCTLType = false; wasLTLType = false; wasHyperLTLType = true; @@ -1979,6 +1980,18 @@ private void toggleDialogType() { } else if (ltlType.equals("E")) { addExistsPathsToProperty(newProperty, null); } + + // Check again after conversion + if (!isValidLTL() && !queryField.getText().trim().equals((new TCTLPathPlaceHolder()).toString())) { + if (showWarningMessage() == JOptionPane.YES_OPTION) { + deleteProperty(); + } else { + int changeTo = wasCTLType ? 0 : 2; + queryType.setSelectedIndex(changeTo); + return; + } + } + showLTLButtons(true); updateSiphonTrap(true); showHyperLTL(false); @@ -1993,7 +2006,7 @@ private void toggleDialogType() { deleteProperty(); newProperty = removeExistsAllPathsFromProperty(newProperty); } else { - int changeTo = wasLTLType ? 1 : 2; + int changeTo = wasCTLType ? 1 : 2; queryType.setSelectedIndex(changeTo); return; } @@ -2002,6 +2015,7 @@ private void toggleDialogType() { showLTLButtons(false); showHyperLTL(false); updateSiphonTrap(false); + wasCTLType = true; wasLTLType = false; wasHyperLTLType = false; @@ -2015,6 +2029,11 @@ private void toggleDialogType() { updateRawVerificationOptions(); } + private boolean isValidLTL() { + String queryText = queryField.getText().trim(); + return queryText.startsWith("A") || queryText.startsWith("E"); + } + private String checkLTLType() { if (newProperty.toString().equals("<*>")) return "placeholder"; @@ -2240,7 +2259,6 @@ private void addAllPathsToProperty(TCTLAbstractProperty oldProperty, TCTLAbstrac int selectedIndex = queryType.getSelectedIndex(); boolean isHyperLTL = selectedIndex == 2; String trace = isHyperLTL ? traceBoxQuantification.getSelectedItem().toString() : ""; - if (oldProperty instanceof LTLANode) { if(!(selectedIndex == 2)) { property = oldProperty; @@ -2810,7 +2828,6 @@ private void addUntimedQuantificationListeners() { aButton.addActionListener(e -> { TCTLAbstractProperty oldProperty = newProperty; - if (!(queryType.getSelectedIndex() == 2)) { newProperty = removeExistsAllPathsFromProperty(newProperty); addAllPathsToProperty(newProperty, null); @@ -4696,8 +4713,8 @@ protected void setEnabledOptionsAccordingToCurrentReduction() { useColoredReduction.setEnabled(false); } - wasCTLType = queryType.getSelectedIndex() == 0; - updateSiphonTrap(wasCTLType); + boolean isCTL = queryType.getSelectedIndex() == 0; + updateSiphonTrap(isCTL); updateSearchStrategies(); refreshExportButtonText(); From f1a5ec1b7982337ce1bb6668445f72b47ff11b41 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Mon, 29 Jan 2024 21:44:47 +0100 Subject: [PATCH 50/50] Small correction --- src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index c72a77b36..bd9594eac 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -2006,7 +2006,7 @@ private void toggleDialogType() { deleteProperty(); newProperty = removeExistsAllPathsFromProperty(newProperty); } else { - int changeTo = wasCTLType ? 1 : 2; + int changeTo = wasLTLType ? 1 : 2; queryType.setSelectedIndex(changeTo); return; }