From 3ac2873c76beac5d1397b47681cabae8846d57ed Mon Sep 17 00:00:00 2001 From: mtygesen Date: Wed, 31 Jan 2024 16:44:29 +0100 Subject: [PATCH] Fixed issues with k-bound when using raw verification --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 5 ++++- 1 file changed, 4 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 e5fe9a59c..08819f2de 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4770,7 +4770,10 @@ private void updateRawVerificationOptions() { boolean isColored = (lens != null && lens.isColored() || tapnNetwork.isColored()); VerifyTAPNOptions verifytapnOptions = Verifier.getVerificationOptions(query, isColored); - verifytapnOptions.setTokensInModel(((TimedArcPetriNet) templateBox.getSelectedItem()).getNumberOfTokensInNet()); + + ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false); + Tuple transformedModel = composer.transformModel(QueryDialog.this.tapnNetwork); + verifytapnOptions.setTokensInModel(transformedModel.value1().getNumberOfTokensInNet()); rawVerificationOptionsTextArea.setText(verifytapnOptions.toString()); }