From ea99678eddaeb1bbcf223a70d277caaa0b618b03 Mon Sep 17 00:00:00 2001 From: Tanguy Dubois Date: Mon, 29 Apr 2024 09:31:12 +0200 Subject: [PATCH 001/138] Stochastic Lens, and rate edit menu for transitions --- src/main/java/dk/aau/cs/io/LoadedModel.java | 5 +- src/main/java/dk/aau/cs/io/PNMLoader.java | 2 +- .../dk/aau/cs/io/TapnEngineXmlLoader.java | 10 ++- src/main/java/dk/aau/cs/io/TapnXmlLoader.java | 10 ++- .../cs/io/TimedArcPetriNetNetworkWriter.java | 10 ++- .../aau/cs/model/tapn/SharedTransition.java | 19 +++++ .../aau/cs/model/tapn/TimedArcPetriNet.java | 9 ++ .../model/tapn/TimedArcPetriNetNetwork.java | 9 ++ .../dk/aau/cs/model/tapn/TimedTransition.java | 23 +++++ .../dk/aau/cs/verification/QueryType.java | 4 +- .../verification/VerifyTAPN/VerifyDTAPN.java | 2 +- .../cs/verification/VerifyTAPN/VerifyPN.java | 2 +- .../verification/VerifyTAPN/VerifyTAPN.java | 2 +- .../VerifyTAPN/VerifyTAPNExporter.java | 3 + src/main/java/net/tapaal/gui/TabActions.java | 2 + .../net/tapaal/gui/petrinet/TAPNLens.java | 12 ++- .../tapaal/gui/petrinet/TabTransformer.java | 9 ++ .../gui/petrinet/dialog/NewTAPNPanel.java | 83 +++++++++++++++++-- .../gui/petrinet/editor/ConstantsPane.java | 3 + .../undo/ChangeTransitionRateCommand.java | 31 +++++++ .../gui/petrinet/verification/UnfoldNet.java | 2 +- src/main/java/pipe/gui/GuiFrame.java | 51 ++++++++++-- src/main/java/pipe/gui/petrinet/Export.java | 4 +- .../java/pipe/gui/petrinet/PetriNetTab.java | 49 ++++++++--- .../petrinet/editor/TAPNTransitionEditor.java | 34 +++++++- .../graphicElements/PetriNetObject.java | 4 + 26 files changed, 349 insertions(+), 45 deletions(-) create mode 100644 src/main/java/net/tapaal/gui/petrinet/undo/ChangeTransitionRateCommand.java diff --git a/src/main/java/dk/aau/cs/io/LoadedModel.java b/src/main/java/dk/aau/cs/io/LoadedModel.java index dd07ce3a7..21a44ea25 100644 --- a/src/main/java/dk/aau/cs/io/LoadedModel.java +++ b/src/main/java/dk/aau/cs/io/LoadedModel.java @@ -35,9 +35,10 @@ public TAPNLens getLens(){ } else { boolean isNetTimed = !network().isUntimed(); boolean isNetGame = network().hasUncontrollableTransitions(); - boolean isNetColored = network.isColored(); + boolean isNetColored = network().isColored(); + boolean isNetStochastic = network().isStochastic(); - return new TAPNLens(isNetTimed, isNetGame, isNetColored); + return new TAPNLens(isNetTimed, isNetGame, isNetColored, isNetStochastic); } } public boolean isColored(){ diff --git a/src/main/java/dk/aau/cs/io/PNMLoader.java b/src/main/java/dk/aau/cs/io/PNMLoader.java index f01d0d895..252d23e71 100644 --- a/src/main/java/dk/aau/cs/io/PNMLoader.java +++ b/src/main/java/dk/aau/cs/io/PNMLoader.java @@ -113,7 +113,7 @@ private LoadedModel parse(Document doc) throws FormatException { Node pnmlElement = doc.getElementsByTagName("pnml").item(0); Node netNode = getFirstDirectChild(pnmlElement, "net"); - lens = new TAPNLens(false, false, getFirstDirectChild(netNode, "declaration") != null); + lens = new TAPNLens(false, false, getFirstDirectChild(netNode, "declaration") != null, false); String name = getTAPNName(netNode); diff --git a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java index 46b8eb2da..d5606ddf7 100644 --- a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java @@ -140,7 +140,10 @@ private void parseFeature(Document doc, TimedArcPetriNetNetwork network) { var isColoredElement = nodeList.item(0).getAttributes().getNamedItem("isColored"); boolean isColored = isColoredElement == null ? network.isColored() : Boolean.parseBoolean(isColoredElement.getNodeValue()); - lens = new TAPNLens(isTimed, isGame, isColored); + var isStochasticElement = nodeList.item(0).getAttributes().getNamedItem("isColored"); + boolean isStochastic = isStochasticElement == null ? network.isStochastic() : Boolean.parseBoolean(isStochasticElement.getNodeValue()); + + lens = new TAPNLens(isTimed, isGame, isColored, isStochastic); } } @@ -154,7 +157,10 @@ private void parseFeature(Document doc) { var isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue()); var isColored = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isColored").getNodeValue()); - lens = new TAPNLens(isTimed, isGame, isColored); + var stochasticEl = nodeList.item(0).getAttributes().getNamedItem("isStochastic"); + var isStochastic = stochasticEl != null && Boolean.parseBoolean(stochasticEl.getNodeValue()); + + lens = new TAPNLens(isTimed, isGame, isColored, isStochastic); } } diff --git a/src/main/java/dk/aau/cs/io/TapnXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnXmlLoader.java index 70668e83e..613d00536 100644 --- a/src/main/java/dk/aau/cs/io/TapnXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnXmlLoader.java @@ -197,7 +197,10 @@ private void parseFeature(Document doc, TimedArcPetriNetNetwork network) { var isColoredElement = nodeList.item(0).getAttributes().getNamedItem("isColored"); boolean isColored = isColoredElement == null ? network.isColored() : Boolean.parseBoolean(isColoredElement.getNodeValue()); - lens = new TAPNLens(isTimed, isGame, isColored); + var isStochasticElement = nodeList.item(0).getAttributes().getNamedItem("isStochastic"); + boolean isStochastic = isStochasticElement == null ? network.isStochastic() : Boolean.parseBoolean(isStochasticElement.getNodeValue()); + + lens = new TAPNLens(isTimed, isGame, isColored, isStochastic); } } @@ -211,7 +214,10 @@ private void parseFeature(Document doc) { var isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue()); var isColored = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isColored").getNodeValue()); - lens = new TAPNLens(isTimed, isGame, isColored); + var stochasticElement = nodeList.item(0).getAttributes().getNamedItem("isStochastic"); + var isStochastic = stochasticElement != null && Boolean.parseBoolean(stochasticElement.getNodeValue()); + + lens = new TAPNLens(isTimed, isGame, isColored, isStochastic); } } diff --git a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java b/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java index 42044eeca..532518b46 100644 --- a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java +++ b/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java @@ -173,6 +173,7 @@ private void appendFeature(Document document, Element root) { String isTimed = "true"; String isGame = "true"; String isColored = "true"; + String isStochastic = "true"; if (!lens.isTimed()) { isTimed = "false"; } @@ -182,17 +183,20 @@ private void appendFeature(Document document, Element root) { if(!lens.isColored()){ isColored = "false"; } - - root.appendChild(createFeatureElement(isTimed, isGame, isColored, document)); + if(!lens.isStochastic()) { + isStochastic = "false"; + } + root.appendChild(createFeatureElement(isTimed, isGame, isColored, isStochastic, document)); } - private Element createFeatureElement(String isTimed, String isGame, String isColored, Document document) { + private Element createFeatureElement(String isTimed, String isGame, String isColored, String isStochastic, Document document) { Require.that(document != null, "Error: document was null"); Element feature = document.createElement("feature"); feature.setAttribute("isTimed", isTimed); feature.setAttribute("isGame", isGame); feature.setAttribute("isColored", isColored); + feature.setAttribute("isStochastic", isStochastic); return feature; } diff --git a/src/main/java/dk/aau/cs/model/tapn/SharedTransition.java b/src/main/java/dk/aau/cs/model/tapn/SharedTransition.java index b2c6b61ac..78095d563 100644 --- a/src/main/java/dk/aau/cs/model/tapn/SharedTransition.java +++ b/src/main/java/dk/aau/cs/model/tapn/SharedTransition.java @@ -18,6 +18,7 @@ public class SharedTransition { private final List transitions = new ArrayList(); private boolean isUrgent = false; private boolean isUncontrollable = false; + private float rate = 0.5f; private GuardExpression guard = null; private TimedArcPetriNetNetwork network; @@ -56,6 +57,24 @@ public void setUncontrollable(boolean isUncontrollable) { } } + public boolean hasCustomRate() { return rate > 0; } + + public void removeCustomRate() { + this.rate = -1.0f; + for (TimedTransition transition : transitions) { + transition.setRate(-1.0f, false); + } + } + + public float getRate() { return rate; } + + public void setRate(float rate) { + this.rate = rate; + for (TimedTransition transition : transitions) { + transition.setRate(rate, false); + } + } + public GuardExpression getGuard() { return guard; } diff --git a/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java b/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java index dc87898f4..3618d17f6 100644 --- a/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java +++ b/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java @@ -108,6 +108,15 @@ public boolean isColored(){ return false; } + public boolean isStochastic() { + for(TimedTransition t : transitions) { + if(t.hasCustomRate()) { + return true; + } + } + return false; + } + public void add(TimedTransition transition) { Require.that(transition != null, "Argument must be a non-null transition"); Require.that(!isNameUsed(transition.name()) || transition.isShared(), "A place or transition with the specified name, "+transition.name()+", already exists in the petri net."); diff --git a/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java b/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java index d6d9a4e22..46258e322 100644 --- a/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java +++ b/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java @@ -458,6 +458,15 @@ public boolean isColored() { return colorTypes.size() > 1 || variables.size() > 0; } + public boolean isStochastic() { + for (TimedArcPetriNet tapn : tapns) { + if(tapn.isStochastic()) { + return true; + } + } + return false; + } + public boolean isUntimed(){ for(TimedArcPetriNet t : tapns){ if(!t.isUntimed()){ diff --git a/src/main/java/dk/aau/cs/model/tapn/TimedTransition.java b/src/main/java/dk/aau/cs/model/tapn/TimedTransition.java index e537a6897..af076003a 100644 --- a/src/main/java/dk/aau/cs/model/tapn/TimedTransition.java +++ b/src/main/java/dk/aau/cs/model/tapn/TimedTransition.java @@ -28,6 +28,7 @@ public class TimedTransition extends TAPNElement { private boolean isUrgent = false; private boolean isUncontrollable = false; + private float rate = -1.0f; private GuardExpression guard; private SharedTransition sharedTransition; @@ -48,6 +49,13 @@ public TimedTransition(String name, boolean isUrgent, GuardExpression guard) { this.guard = guard; } + public TimedTransition(String name, boolean isUrgent, GuardExpression guard, float rate) { + setName(name); + setUrgent(isUrgent); + setRate(rate); + this.guard = guard; + } + public void addTimedTransitionListener(TimedTransitionListener listener){ Require.that(listener != null, "listener cannot be null"); listeners.add(listener); @@ -87,6 +95,21 @@ public void setUncontrollable(boolean isUncontrollable, boolean cascade) { sharedTransition.setUncontrollable(isUncontrollable); } } + + public boolean hasCustomRate() { return rate > 0; } + + public void removeCustomRate() { setRate(-1.0f, true); } + + public float getRate() { return rate; } + + public void setRate(float rate) { setRate(rate, true); } + + public void setRate(float rate, boolean cascade) { + this.rate = rate; + if(isShared() && cascade) { + sharedTransition.setRate(rate); + } + } public boolean hasUntimedPreset(){ return hasUntimedPreset(true); diff --git a/src/main/java/dk/aau/cs/verification/QueryType.java b/src/main/java/dk/aau/cs/verification/QueryType.java index e812ae451..e48f39c6d 100644 --- a/src/main/java/dk/aau/cs/verification/QueryType.java +++ b/src/main/java/dk/aau/cs/verification/QueryType.java @@ -6,5 +6,7 @@ public enum QueryType { AF, AG, E, - A + A, + PF, + PG } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java index 75d4eca39..99218d89f 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java @@ -344,7 +344,7 @@ protected VerificationResult verify(VerificationOptions o } if (tapnTrace != null) { - newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(lens.isTimed(), lens.isGame(), false)); + newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(lens.isTimed(), lens.isGame(), false, lens.isStochastic())); //The query being verified should be the only query for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network(), query.getCategory())) { 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 a5ec1d9b0..2c86711bb 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java @@ -354,7 +354,7 @@ private VerificationResult verify(VerificationOptions opt } if (tapnTrace != null) { - newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(lens.isTimed(), lens.isGame(), false)); + newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(lens.isTimed(), lens.isGame(), false, lens.isStochastic())); //The query being verified should be the only query for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network(), query.getCategory())) { diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java index e17b3f44c..ab6aafb37 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java @@ -344,7 +344,7 @@ protected VerificationResult verify(VerificationOptions o } if (tapnTrace != null) { - newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(lens.isTimed(), lens.isGame(), false)); + newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(lens.isTimed(), lens.isGame(), false, lens.isStochastic())); //The query being verified should be the only query for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network(), query.getCategory())) { diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java index 306639135..a88879ae5 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java @@ -161,6 +161,9 @@ protected void outputTransition(TimedTransition t, PrintStream modelStream, Data modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" "); modelStream.append("id=\"" + t.name() + "\" "); modelStream.append("name=\"" + t.name() + "\" "); + if(t.hasCustomRate()) { + modelStream.append("rate=\"" + t.getRate() + "\" "); + } modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\""); modelStream.append(">\n"); diff --git a/src/main/java/net/tapaal/gui/TabActions.java b/src/main/java/net/tapaal/gui/TabActions.java index 89299ce45..e8d2df7c7 100644 --- a/src/main/java/net/tapaal/gui/TabActions.java +++ b/src/main/java/net/tapaal/gui/TabActions.java @@ -94,6 +94,8 @@ public interface TabActions { void changeColorFeature(boolean isColor); + void changeStochasticFeature(boolean isStochastic); + void exportPNG(); void exportPS(); diff --git a/src/main/java/net/tapaal/gui/petrinet/TAPNLens.java b/src/main/java/net/tapaal/gui/petrinet/TAPNLens.java index c55d4f40c..dd028ab17 100644 --- a/src/main/java/net/tapaal/gui/petrinet/TAPNLens.java +++ b/src/main/java/net/tapaal/gui/petrinet/TAPNLens.java @@ -1,7 +1,7 @@ package net.tapaal.gui.petrinet; public final class TAPNLens { - public static final TAPNLens Default = new TAPNLens(true, true, true); + public static final TAPNLens Default = new TAPNLens(true, true, true, false); public boolean isTimed() { return timed; @@ -15,13 +15,21 @@ public boolean isColored() { return colored; } + public boolean isStochastic() { return stochastic; } + + public boolean canBeStochastic() { + return timed && (!game) && (!colored); + } + private final boolean timed; private final boolean game; private final boolean colored; + private final boolean stochastic; - public TAPNLens(boolean timed, boolean game, boolean colored) { + public TAPNLens(boolean timed, boolean game, boolean colored, boolean stochastic) { this.timed = timed; this.game = game; this.colored = colored; + this.stochastic = stochastic && canBeStochastic(); } } diff --git a/src/main/java/net/tapaal/gui/petrinet/TabTransformer.java b/src/main/java/net/tapaal/gui/petrinet/TabTransformer.java index c0beb4aec..344ce94c4 100644 --- a/src/main/java/net/tapaal/gui/petrinet/TabTransformer.java +++ b/src/main/java/net/tapaal/gui/petrinet/TabTransformer.java @@ -185,6 +185,15 @@ static public void removeGameInformation(PetriNetTab tab) { } } } + static public void removeRateInformation(PetriNetTab tab) { + for (Template template : tab.allTemplates()) { + for (TimedTransition transition : template.model().transitions()) { + if (transition.hasCustomRate()) { + transition.removeCustomRate(); + } + } + } + } static public void removeColorInformation(PetriNetTab tab) { tab.network().setColorTypes(List.of(ColorType.COLORTYPE_DOT)); tab.network().setVariables(new ArrayList()); diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/NewTAPNPanel.java b/src/main/java/net/tapaal/gui/petrinet/dialog/NewTAPNPanel.java index cbe10ce29..bcc9f3330 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/NewTAPNPanel.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/NewTAPNPanel.java @@ -17,8 +17,12 @@ public class NewTAPNPanel extends EscapableDialog { private final GuiFrame frame; private JTextField nameTextBox; private JRadioButton timedNet; + private JRadioButton untimedNet; private JRadioButton gameNet; + private JRadioButton nonGameNet; private JRadioButton coloredNet; + private JRadioButton nonColorNet; + private JRadioButton stochasticNet; private static int newNameCounter = 1; static NewTAPNPanel newTAPNPanel; private final static String COLORED_GAMES_NOT_SUPPORTED = "There exists no verification engine for colored games, we only allow modelling.\n\n Do you wish to continue?"; @@ -84,7 +88,7 @@ private void initButtonPanel() { gbc.anchor = GridBagConstraints.EAST; buttonPanel.add(cancelButton,gbc); - okButton.addActionListener(e -> createNewTAPNBasedOnSelection(nameTextBox.getText(), timedNet.isSelected(), gameNet.isSelected(), coloredNet.isSelected())); + okButton.addActionListener(e -> createNewTAPNBasedOnSelection(nameTextBox.getText(), timedNet.isSelected(), gameNet.isSelected(), coloredNet.isSelected(), stochasticNet.isSelected())); rootPane.setDefaultButton(okButton); @@ -102,7 +106,7 @@ protected void exit() { rootPane.getParent().setVisible(false); } - protected void createNewTAPNBasedOnSelection(String name, boolean isTimed, boolean isGame, boolean isColored) { + protected void createNewTAPNBasedOnSelection(String name, boolean isTimed, boolean isGame, boolean isColored, boolean isStochastic) { if (!name.endsWith(".tapn")) { name = name + ".tapn"; } @@ -115,7 +119,7 @@ protected void createNewTAPNBasedOnSelection(String name, boolean isTimed, boole } try { - PetriNetTab tab = PetriNetTab.createNewEmptyTab(name, isTimed, isGame, isColored); + PetriNetTab tab = PetriNetTab.createNewEmptyTab(name, isTimed, isGame, isColored, isStochastic); TAPAALGUI.openNewTabFromStream(tab); } catch (Exception e) { JOptionPane @@ -169,6 +173,7 @@ private void initSelectionPanel() { initTimeOptions(selectionPanel); initGameOptions(selectionPanel); initColorOptions(selectionPanel); + initStochasticOptions(selectionPanel); GridBagConstraints gbc = new GridBagConstraints(); gbc.gridx = 0; @@ -192,7 +197,7 @@ private void initTimeOptions(JPanel selectionPanel) { gbc.insets = new Insets(3, 3, 3, 3); isTimedPanel.add(timedText, gbc); - JRadioButton untimedNet = new JRadioButton("No"); + untimedNet = new JRadioButton("No"); untimedNet.setSelected(true); gbc = new GridBagConstraints(); gbc.gridx = 1; @@ -235,7 +240,7 @@ private void initGameOptions(JPanel selectionPanel) { gbc.insets = new Insets(3, 3, 3, 3); isGamePanel.add(gameText, gbc); - JRadioButton nonGameNet = new JRadioButton("No"); + nonGameNet = new JRadioButton("No"); nonGameNet.setSelected(true); gbc = new GridBagConstraints(); gbc.gridx = 1; @@ -276,7 +281,7 @@ private void initColorOptions(JPanel selectionPanel) { gbc.insets = new Insets(3, 3, 3, 3); isColorPanel.add(colorText, gbc); - JRadioButton nonColorNet = new JRadioButton("No"); + nonColorNet = new JRadioButton("No"); nonColorNet.setSelected(true); gbc = new GridBagConstraints(); gbc.gridx = 1; @@ -305,6 +310,72 @@ private void initColorOptions(JPanel selectionPanel) { selectionPanel.add(isColorPanel, gbc); } + private void initStochasticOptions(JPanel selectionPanel) { + JPanel isStochasticPanel = new JPanel(new GridBagLayout()); + ButtonGroup isStochasticRadioButtonGroup = new ButtonGroup(); + + JLabel colorText = new JLabel("Use stochastic semantics :"); + GridBagConstraints gbc = new GridBagConstraints(); + gbc.gridx = 0; + gbc.gridy = 0; + gbc.weightx = 0; + gbc.anchor = GridBagConstraints.WEST; + gbc.insets = new Insets(3, 3, 3, 3); + isStochasticPanel.add(colorText, gbc); + + JRadioButton nonStochasticNet = new JRadioButton("No"); + nonStochasticNet.setSelected(true); + gbc = new GridBagConstraints(); + gbc.gridx = 1; + gbc.gridy = 0; + gbc.weightx = 0; + gbc.anchor = GridBagConstraints.WEST; + gbc.insets = new Insets(3, 3, 3, 3); + isStochasticPanel.add(nonStochasticNet, gbc); + isStochasticRadioButtonGroup.add(nonStochasticNet); + + stochasticNet = new JRadioButton("Yes"); + gbc = new GridBagConstraints(); + gbc.gridx = 2; + gbc.gridy = 0; + gbc.weightx = 0; + gbc.anchor = GridBagConstraints.WEST; + gbc.insets = new Insets(3, 3, 3, 3); + isStochasticPanel.add(stochasticNet, gbc); + isStochasticRadioButtonGroup.add(stochasticNet); + stochasticNet.setEnabled(false); + + gbc = new GridBagConstraints(); + gbc.gridx = 0; + gbc.gridy = 4; + gbc.anchor = GridBagConstraints.WEST; + gbc.insets = new Insets(5, 5, 5, 5); + selectionPanel.add(isStochasticPanel, gbc); + + var refreshOthers = new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + gameNet.setEnabled(!stochasticNet.isSelected()); + coloredNet.setEnabled(!stochasticNet.isSelected()); + untimedNet.setEnabled(!stochasticNet.isSelected()); + } + }; + var refreshStochastic = new ActionListener() { + public void actionPerformed(ActionEvent actionEvent) { + stochasticNet.setEnabled( + timedNet.isSelected() && nonGameNet.isSelected() && nonColorNet.isSelected() + ); + } + }; + stochasticNet.addActionListener(refreshOthers); + nonStochasticNet.addActionListener(refreshOthers); + timedNet.addActionListener(refreshStochastic); + untimedNet.addActionListener(refreshStochastic); + gameNet.addActionListener(refreshStochastic); + nonGameNet.addActionListener(refreshStochastic); + coloredNet.addActionListener(refreshStochastic); + nonColorNet.addActionListener(refreshStochastic); + } + public void setName(String name){ nameTextBox.setText(name); } diff --git a/src/main/java/net/tapaal/gui/petrinet/editor/ConstantsPane.java b/src/main/java/net/tapaal/gui/petrinet/editor/ConstantsPane.java index 1a27eb392..26418c756 100644 --- a/src/main/java/net/tapaal/gui/petrinet/editor/ConstantsPane.java +++ b/src/main/java/net/tapaal/gui/petrinet/editor/ConstantsPane.java @@ -60,12 +60,15 @@ public class ConstantsPane extends JPanel implements SidePane { private static final String titleBorder = "Global constants, Color types and Variables"; private static final String titleBorderNoColor = "Global constants"; + private static final String titleBorderSMC = "Global constants and SMC Settings"; private static final String titleBorderToolTip = "Declaration of colors types, color variables and global integer constants.
To see a summary list press SHIFT + F"; private static final String titleBorderToolTipNoColor = "Declaration of global constants that can be used in intervals and age invariants"; + private static final String titleBorderToolTipSmc = "Declaration of global constants that can be used in intervals and age invariants, and editing of SMC engine settings"; private static final String CONSTANTS = "Constants"; private static final String COLORTYPES = "Color type"; private static final String VARIABLES = "Variables"; + private static final String SMC_SETTINGS = "SMC Settings"; private final JComboBox constantsColorTypesVariablesComboBox = new JComboBox<>(new String[]{COLORTYPES, VARIABLES, CONSTANTS}); diff --git a/src/main/java/net/tapaal/gui/petrinet/undo/ChangeTransitionRateCommand.java b/src/main/java/net/tapaal/gui/petrinet/undo/ChangeTransitionRateCommand.java new file mode 100644 index 000000000..291b0c78d --- /dev/null +++ b/src/main/java/net/tapaal/gui/petrinet/undo/ChangeTransitionRateCommand.java @@ -0,0 +1,31 @@ +package net.tapaal.gui.petrinet.undo; + +import dk.aau.cs.model.tapn.TimedTransition; +import pipe.gui.petrinet.PetriNetTab; + +public class ChangeTransitionRateCommand extends Command { + private final TimedTransition transition; + private final float oldValue; + private final float newValue; + private final PetriNetTab tab; + + public ChangeTransitionRateCommand(TimedTransition transition, PetriNetTab tab, float newRate){ + this.transition = transition; + oldValue = transition.getRate(); + newValue = newRate; + this.tab = tab; + } + + @Override + public void redo() { + transition.setRate(newValue); + tab.repaint(); + } + + @Override + public void undo() { + transition.setRate(oldValue); + tab.repaint(); + } + +} diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java b/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java index e69f24f00..0df89204c 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java @@ -185,7 +185,7 @@ protected String doInBackground() throws Exception { loadedModel = new PNMLoader().load(fileOut); } // addLocation(loadedModel, composer); // We can not get coords from server - newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(oldTab.getLens().isTimed(), oldTab.getLens().isGame(), false)); + newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new TAPNLens(oldTab.getLens().isTimed(), oldTab.getLens().isGame(), false, oldTab.getLens().isStochastic())); newTab.setInitialName(oldTab.getTabTitle().replace(".tapn", "") + "-unfolded"); Thread thread = new Thread(() -> TAPAALGUI.getAppGuiController().openTab(newTab)); diff --git a/src/main/java/pipe/gui/GuiFrame.java b/src/main/java/pipe/gui/GuiFrame.java index 9b664b397..5f026cad9 100644 --- a/src/main/java/pipe/gui/GuiFrame.java +++ b/src/main/java/pipe/gui/GuiFrame.java @@ -68,6 +68,7 @@ public class GuiFrame extends JFrame implements GuiFrameActions, SafeGuiFrameAct private final JComboBox timeFeatureOptions = new JComboBox<>(new String[]{"No", "Yes"}); private final JComboBox gameFeatureOptions = new JComboBox<>(new String[]{"No", "Yes"}); private final JComboBox colorFeatureOptions = new JComboBox<>(new String[]{"No", "Yes"}); + private final JComboBox stochasticFeatureOptions = new JComboBox<>(new String[]{"No", "Yes"}); private JComboBox zoomComboBox; @@ -449,6 +450,7 @@ public void actionPerformed(ActionEvent e) { public void actionPerformed(ActionEvent e) { boolean isTime = timeFeatureOptions.getSelectedIndex() != 0; currentTab.ifPresent(o -> o.changeTimeFeature(isTime)); + refreshLensConstraints(); } }; @@ -456,6 +458,7 @@ public void actionPerformed(ActionEvent e) { public void actionPerformed(ActionEvent e) { boolean isGame = gameFeatureOptions.getSelectedIndex() != 0; currentTab.ifPresent(o -> o.changeGameFeature(isGame)); + refreshLensConstraints(); } }; @@ -463,6 +466,15 @@ public void actionPerformed(ActionEvent e) { public void actionPerformed(ActionEvent e) { boolean isColor = colorFeatureOptions.getSelectedIndex() != 0; currentTab.ifPresent(o -> o.changeColorFeature(isColor)); + refreshLensConstraints(); + } + }; + + private final GuiAction changeStochasticFeatureAction = new GuiAction("Stochastic", "Change stochastic semantics") { + public void actionPerformed(ActionEvent actionEvent) { + boolean isStochastic = stochasticFeatureOptions.getSelectedIndex() != 0; + currentTab.ifPresent(o -> o.changeStochasticFeature(isStochastic)); + refreshLensConstraints(); } }; @@ -523,9 +535,12 @@ protected void closeTab(PetriNetTab tab) { featurePanel.add(gameFeatureOptions); featurePanel.add(new JLabel(" Color: ")); featurePanel.add(colorFeatureOptions); + featurePanel.add(new JLabel(" Stochastic: ")); + featurePanel.add(stochasticFeatureOptions); timeFeatureOptions.addActionListener(changeTimeFeatureAction); gameFeatureOptions.addActionListener(changeGameFeatureAction); colorFeatureOptions.addActionListener(changeColorFeatureAction); + stochasticFeatureOptions.addActionListener(changeStochasticFeatureAction); JPanel bottomPanel = new JPanel(); bottomPanel.setLayout(new GridLayout(1, 2)); @@ -1004,6 +1019,8 @@ private void enableGUIActions(GUIMode mode) { timeFeatureOptions.setEnabled(true); gameFeatureOptions.setEnabled(true); colorFeatureOptions.setEnabled(true); + stochasticFeatureOptions.setEnabled(true); + refreshLensConstraints(); //Enable editor focus traversal policy setFocusTraversalPolicy(new EditorFocusTraversalPolicy()); @@ -1043,6 +1060,7 @@ private void enableGUIActions(GUIMode mode) { timeFeatureOptions.setEnabled(false); gameFeatureOptions.setEnabled(false); colorFeatureOptions.setEnabled(false); + stochasticFeatureOptions.setEnabled(false); //Enable simulator focus traversal policy setFocusTraversalPolicy(new SimulatorFocusTraversalPolicy(getCurrentTab().getAnimationController().TimeDelayField)); @@ -1074,6 +1092,7 @@ private void enableGUIActions(GUIMode mode) { timeFeatureOptions.setEnabled(false); gameFeatureOptions.setEnabled(false); colorFeatureOptions.setEnabled(false); + stochasticFeatureOptions.setEnabled(false); enableAllActions(false); @@ -1537,12 +1556,13 @@ private JMenu buildExampleMenu() { // .xml file the Example x counter is not incremented when that file // is ignored if (nets != null && nets.length > 0) { - TAPNLens untimedLens = new TAPNLens(false, false, false); - TAPNLens timedLens = new TAPNLens(true, false, false); - TAPNLens untimedGameLens = new TAPNLens(false, true, false); - TAPNLens timedGameLens = new TAPNLens(true, true, false); - TAPNLens untimedColorLens = new TAPNLens(false, false, true); - TAPNLens timedColorLens = new TAPNLens(true, false, true); + TAPNLens untimedLens = new TAPNLens(false, false, false, false); + TAPNLens timedLens = new TAPNLens(true, false, false, false); + TAPNLens untimedGameLens = new TAPNLens(false, true, false, false); + TAPNLens timedGameLens = new TAPNLens(true, true, false, false); + TAPNLens untimedColorLens = new TAPNLens(false, false, true, false); + TAPNLens timedColorLens = new TAPNLens(true, false, true, false); + TAPNLens timedStochasticLens = new TAPNLens(true, false, false, true); HashMap> netMap = new HashMap<>(){{ put(untimedLens, new ArrayList<>()); @@ -1551,6 +1571,7 @@ private JMenu buildExampleMenu() { put(timedGameLens, new ArrayList<>()); put(untimedColorLens, new ArrayList<>()); put(timedColorLens, new ArrayList<>()); + put(timedStochasticLens, new ArrayList<>()); }}; for (String filename : nets) { @@ -1562,11 +1583,11 @@ private JMenu buildExampleMenu() { try { lens = PetriNetTab.getFileLens(file); if (lens == null) { - lens = new TAPNLens(true, false, false); + lens = new TAPNLens(true, false, false, false); } TAPNLens tmp = lens; netMap.forEach((v, k) -> { - if (v.isTimed() == tmp.isTimed() && v.isGame() == tmp.isGame() && v.isColored() == tmp.isColored()) k.add(filename); + if (v.isTimed() == tmp.isTimed() && v.isGame() == tmp.isGame() && v.isColored() == tmp.isColored() && v.isStochastic() == tmp.isStochastic()) k.add(filename); }); } catch (Exception e) { if (netMap.containsKey(timedLens)) netMap.get(timedLens).add(filename); @@ -1803,6 +1824,20 @@ public void setFeatureInfoText(boolean[] features) { timeFeatureOptions.setSelectedIndex(features[0] ? 1 : 0); gameFeatureOptions.setSelectedIndex(features[1] ? 1 : 0); colorFeatureOptions.setSelectedIndex(features[2] ? 1 : 0); + stochasticFeatureOptions.setSelectedIndex(features[3] ? 1 : 0); } + refreshLensConstraints(); + } + + public void refreshLensConstraints() { + boolean stochasticEnabled = stochasticFeatureOptions.getSelectedIndex() != 0; + timeFeatureOptions.setEnabled(!stochasticEnabled); + gameFeatureOptions.setEnabled(!stochasticEnabled); + colorFeatureOptions.setEnabled(!stochasticEnabled); + stochasticFeatureOptions.setEnabled( + timeFeatureOptions.getSelectedIndex() != 0 && + gameFeatureOptions.getSelectedIndex() == 0 && + colorFeatureOptions.getSelectedIndex() == 0 + ); } } diff --git a/src/main/java/pipe/gui/petrinet/Export.java b/src/main/java/pipe/gui/petrinet/Export.java index d94949fc6..40d9b1f31 100644 --- a/src/main/java/pipe/gui/petrinet/Export.java +++ b/src/main/java/pipe/gui/petrinet/Export.java @@ -149,7 +149,7 @@ public static void toVerifyTAPN(TimedArcPetriNetNetwork network, Iterable transformedModel = composer.transformModel(network); TimedArcPetriNet model = transformedModel.value1(); - TAPNLens lens = new TAPNLens(!model.isUntimed(), model.hasUncontrollableTransitions(), model.isColored()); + TAPNLens lens = new TAPNLens(!model.isUntimed(), model.hasUncontrollableTransitions(), model.isColored(), model.isStochastic()); RenameAllPlacesVisitor visitor = new RenameAllPlacesVisitor(transformedModel.value2()); int i = 0; @@ -160,7 +160,7 @@ public static void toVerifyTAPN(TimedArcPetriNetNetwork network, Iterable(), new TAPNLens(isTimed, isGame, isColored)); + private PetriNetTab(boolean isTimed, boolean isGame, boolean isColored, boolean isStochastic) { + this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(isTimed, isGame, isColored, isStochastic)); } private PetriNetTab(TimedArcPetriNetNetwork network, Collection