From 43e0895731db8f6396bf891c343478211906c275 Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 3 Mar 2019 17:10:31 +0100 Subject: [PATCH 01/13] Added basic elements for token limits on places --- .gitignore | 1 + src/org/pneditor/petrinet/Place.java | 36 +++++++++++++++++-- src/org/pneditor/petrinet/PlaceNode.java | 13 +++++++ src/org/pneditor/petrinet/ReferencePlace.java | 13 +++++++ 4 files changed, 61 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index d6648aa..6df6619 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,4 @@ nbproject/private/ out/ .idea/workspace.xml .idea/tasks.xml +/bin/ diff --git a/src/org/pneditor/petrinet/Place.java b/src/org/pneditor/petrinet/Place.java index 33c84bf..3f627f1 100644 --- a/src/org/pneditor/petrinet/Place.java +++ b/src/org/pneditor/petrinet/Place.java @@ -16,6 +16,8 @@ */ package org.pneditor.petrinet; +import org.pneditor.editor.PNEditor; + /** * Represents place in Petri net * @@ -24,7 +26,9 @@ public class Place extends PlaceNode implements Cloneable { private boolean isStatic = false; - + + private int tokenLimit = 0; + @Override public boolean isStatic() { return isStatic; @@ -32,6 +36,34 @@ public boolean isStatic() { @Override public void setStatic(boolean isStatic) { - this.isStatic = isStatic; + if (this.getTokenLimit()==0) { + this.isStatic = isStatic; + } + } + + @Override + public int getTokenLimit() { + return tokenLimit; + } + + @Override + public void setTokenLimit (int tokenLimit) { + //if there are already some tokens on the place, and they are in greater amount + // than the wanted invariant, the number of tokens will be set to the invariant + if (isStatic == false) { + if (tokenLimit != 0) { + int currentTokens = PNEditor.getRoot().getCurrentMarking().getTokens(this); + if (currentTokens> tokenLimit) { + PNEditor.getRoot().getCurrentMarking().setTokens(this, tokenLimit); + } + this.tokenLimit = tokenLimit; + } + else if (tokenLimit == 0) { + this.tokenLimit = tokenLimit; + } + + } } + + } diff --git a/src/org/pneditor/petrinet/PlaceNode.java b/src/org/pneditor/petrinet/PlaceNode.java index aa0901c..8330b71 100644 --- a/src/org/pneditor/petrinet/PlaceNode.java +++ b/src/org/pneditor/petrinet/PlaceNode.java @@ -61,12 +61,19 @@ public Set getConnectedArcs(Transition transition) { abstract public boolean isStatic(); abstract public void setStatic(boolean isStatic); + + abstract public int getTokenLimit(); + + abstract public void setTokenLimit(int tokenLimit); @Override public void draw(Graphics g, DrawingOptions drawingOptions) { if (isStatic()) { drawStaticShadow(g); } + if (getTokenLimit()!=0) { + drawTokenLimit(g); + } drawPlaceBackground(g); drawPlaceBorder(g); drawLabel(g); @@ -78,6 +85,12 @@ protected void drawStaticShadow(Graphics g) { final int phase = 4; g.fillOval(getStart().x + phase, getStart().y + phase, getWidth() - 1, getHeight() - 1); } + + protected void drawTokenLimit(Graphics g) { + if (getTokenLimit()!=0) { + GraphicsTools.drawString(g, Integer.toString(getTokenLimit()), getCenter().x, getStart().y , HorizontalAlignment.center, VerticalAlignment.bottom); + } + } protected void drawPlaceBackground(Graphics g) { g.setColor(Color.white); diff --git a/src/org/pneditor/petrinet/ReferencePlace.java b/src/org/pneditor/petrinet/ReferencePlace.java index 341e542..2900018 100644 --- a/src/org/pneditor/petrinet/ReferencePlace.java +++ b/src/org/pneditor/petrinet/ReferencePlace.java @@ -104,6 +104,19 @@ public void setStatic(boolean isStatic) { connectedPlaceNode.setStatic(isStatic); } + @Override + public int getTokenLimit() { + if (connectedPlaceNode == null) { + return 0; + } + return connectedPlaceNode.getTokenLimit(); + } + + @Override + public void setTokenLimit(int tokenLimit) { + connectedPlaceNode.setTokenLimit(tokenLimit); + } + @Override protected void drawPlaceBorder(Graphics g) { GraphicsTools.setDashedStroke(g); From c6eb1f80ed1c0ffde4533402919a6797a0d704e4 Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 3 Mar 2019 17:13:59 +0100 Subject: [PATCH 02/13] Added modifications in Marking.java to manage fire operations. Static and Token limits are mutually exclusives. places have to be one or another --- src/org/pneditor/petrinet/Marking.java | 30 ++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/src/org/pneditor/petrinet/Marking.java b/src/org/pneditor/petrinet/Marking.java index bdaa94e..4977af6 100644 --- a/src/org/pneditor/petrinet/Marking.java +++ b/src/org/pneditor/petrinet/Marking.java @@ -127,7 +127,9 @@ public void setTokens(PlaceNode placeNode, int tokens) { if (place.isStatic()) { petriNet.getInitialMarking().map.put(place, tokens); } else { - this.map.put(place, tokens); + if (tokenLimitCompliant(placeNode, tokens)) { + this.map.put(place, tokens); + } } } @@ -158,6 +160,12 @@ public boolean isEnabled(Transition transition) { } } } + } else { // arc is from transition to place + int tokens = getTokens(arc.getPlaceNode()); + if (!tokenLimitCompliant(arc.getPlaceNode(), tokens + arc.getMultiplicity())) { + isEnabled = false; + break; + } } } } finally { @@ -165,6 +173,23 @@ public boolean isEnabled(Transition transition) { } return isEnabled; } + + /** + * Check that a given token number is valid on a given place + * + * @param placeNode placeNode to do the check on + * @param requestedTokens number of tokens wanted to be checked + * @return false if the given numbers of token is invalid, otherwise true + */ + public boolean tokenLimitCompliant(PlaceNode placeNode, int requestedTokens) { + boolean compliant = true; + if (placeNode.getTokenLimit()> 0) { + if (requestedTokens > placeNode.getTokenLimit()) { + compliant = false; + } + } + return compliant; + } /** * Fires a transition in this marking. Changes this marking. @@ -204,7 +229,8 @@ public boolean fire(Transition transition) { } return success; } - + + //TODO: Check for token limit ? public boolean canBeUnfired(Transition transition) { boolean canBeUnfired = true; lock.readLock().lock(); From 2f5e2efc779cf30bdcda7225f57efe105f07ff0e Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 3 Mar 2019 17:17:36 +0100 Subject: [PATCH 03/13] Added actions and commands so that toke limits can be assigned from the user interface --- src/org/pneditor/editor/Root.java | 20 ++++- .../editor/actions/SetPlaceStaticAction.java | 5 +- .../editor/actions/SetTokenLimitAction.java | 85 +++++++++++++++++++ .../editor/commands/SetTokenLimitCommand.java | 64 ++++++++++++++ 4 files changed, 171 insertions(+), 3 deletions(-) create mode 100644 src/org/pneditor/editor/actions/SetTokenLimitAction.java create mode 100644 src/org/pneditor/editor/commands/SetTokenLimitCommand.java diff --git a/src/org/pneditor/editor/Root.java b/src/org/pneditor/editor/Root.java index 7fbdd07..7a853ed 100644 --- a/src/org/pneditor/editor/Root.java +++ b/src/org/pneditor/editor/Root.java @@ -285,7 +285,7 @@ public JPopupMenu getCanvasPopup() { //per application private JToggleButton select, place, transition, arc, token; - private Action setLabel, setTokens, setArcMultiplicity, setArcInhibitory, setArcReset, delete; + private Action setLabel, setTokens, setArcMultiplicity, setArcInhibitory, setArcReset, delete, setTokenLimit; private Action setPlaceStatic; private Action addSelectedTransitionsToSelectedRoles; private Action removeSelectedTransitionsFromSelectedRoles; @@ -335,6 +335,15 @@ private void enableOnlyPossibleActions() { boolean roleSelected = !roleEditor.getSelectedElements().isEmpty(); boolean isParent = !document.petriNet.isCurrentSubnetRoot(); boolean isPtoT = false; + boolean isStaticPlaceNode = false; + boolean isLimitedPlaceNode = false; + + if (isPlaceNode) { + isStaticPlaceNode = ((PlaceNode) clickedElement).isStatic(); + isLimitedPlaceNode = ((PlaceNode) clickedElement).getTokenLimit()!=0; + } + + if (isArc) { Arc test; @@ -352,6 +361,7 @@ private void enableOnlyPossibleActions() { setArcReset.setEnabled(isPtoT); setTokens.setEnabled(isPlaceNode); setLabel.setEnabled(isPlaceNode || isTransitionNode); + setTokenLimit.setEnabled(!isStaticPlaceNode); addSelectedTransitionsToSelectedRoles.setEnabled((isTransitionNode || areTransitionNodes) && roleSelected); removeSelectedTransitionsFromSelectedRoles.setEnabled((isTransitionNode || areTransitionNodes) && roleSelected); convertTransitionToSubnet.setEnabled(isTransition || areTransitions || isSubnet || areSubnets); @@ -361,7 +371,7 @@ private void enableOnlyPossibleActions() { closeSubnet.setEnabled(isParent); undo.setEnabled(getUndoManager().isUndoable()); redo.setEnabled(getUndoManager().isRedoable()); - setPlaceStatic.setEnabled(isPlaceNode); + setPlaceStatic.setEnabled(!isLimitedPlaceNode); } @Override @@ -450,6 +460,7 @@ private void setupMainFrame() { Action quit = new QuitAction(this); setLabel = new SetLabelAction(this); setTokens = new SetTokensAction(this); + setTokenLimit = new SetTokenLimitAction(this); setPlaceStatic = new SetPlaceStaticAction(this); setArcMultiplicity = new SetArcMultiplicityAction(this); setArcInhibitory = new SetArcInhibitoryAction(this); @@ -582,6 +593,7 @@ private void setupMainFrame() { elementMenu.add(setLabel); elementMenu.addSeparator(); elementMenu.add(setTokens); + elementMenu.add(setTokenLimit); elementMenu.add(setPlaceStatic); elementMenu.addSeparator(); elementMenu.add(setArcMultiplicity); @@ -606,6 +618,7 @@ private void setupMainFrame() { placePopup = new JPopupMenu(); placePopup.add(setLabel); + placePopup.add(setTokenLimit); placePopup.add(setTokens); placePopup.add(setPlaceStatic); placePopup.addSeparator(); @@ -613,8 +626,10 @@ private void setupMainFrame() { placePopup.add(copyAction); placePopup.add(delete); + transitionPopup = new JPopupMenu(); transitionPopup.add(setLabel); + transitionPopup.add(convertTransitionToSubnet); transitionPopup.add(addSelectedTransitionsToSelectedRoles); transitionPopup.add(removeSelectedTransitionsFromSelectedRoles); @@ -632,6 +647,7 @@ private void setupMainFrame() { subnetPopup = new JPopupMenu(); subnetPopup.add(openSubnet).setFont(boldFont); subnetPopup.add(setLabel); + //subnetPopup.add(setTokenLimit); subnetPopup.add(replaceSubnet); subnetPopup.add(saveSubnetAs); subnetPopup.add(convertTransitionToSubnet); diff --git a/src/org/pneditor/editor/actions/SetPlaceStaticAction.java b/src/org/pneditor/editor/actions/SetPlaceStaticAction.java index 6501268..631c3cf 100644 --- a/src/org/pneditor/editor/actions/SetPlaceStaticAction.java +++ b/src/org/pneditor/editor/actions/SetPlaceStaticAction.java @@ -43,7 +43,10 @@ public SetPlaceStaticAction(Root root) { public void actionPerformed(ActionEvent e) { if (root.getClickedElement() instanceof PlaceNode) { PlaceNode placeNode = (PlaceNode) root.getClickedElement(); - root.getUndoManager().executeCommand(new SetUnsetPlaceStaticCommand(placeNode)); + if (placeNode.getTokenLimit()==0) + { + root.getUndoManager().executeCommand(new SetUnsetPlaceStaticCommand(placeNode)); + } } } diff --git a/src/org/pneditor/editor/actions/SetTokenLimitAction.java b/src/org/pneditor/editor/actions/SetTokenLimitAction.java new file mode 100644 index 0000000..c7bdeef --- /dev/null +++ b/src/org/pneditor/editor/actions/SetTokenLimitAction.java @@ -0,0 +1,85 @@ +/* + * Copyright (C) 2008-2010 Martin Riesz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + */ +package org.pneditor.editor.actions; + +import java.awt.event.ActionEvent; +import java.awt.event.KeyEvent; +import javax.swing.AbstractAction; +import javax.swing.JOptionPane; +import javax.swing.KeyStroke; +import org.pneditor.editor.Root; +import org.pneditor.editor.commands.SetTokenLimitCommand; +import org.pneditor.petrinet.Marking; +import org.pneditor.petrinet.Place; +import org.pneditor.petrinet.PlaceNode; +import org.pneditor.util.GraphicsTools; + +/** + * + * @author Martin Riesz + */ + +/* + * + * S'inspirer de setTokenAction ? + * Notamment pour cas de mauvais input + */ +public class SetTokenLimitAction extends AbstractAction { + + private Root root; + + public SetTokenLimitAction(Root root) { + this.root = root; + String name = "Set token limit"; + putValue(NAME, name); + putValue(SMALL_ICON, GraphicsTools.getIcon("pneditor/tokenLimit.gif")); + putValue(SHORT_DESCRIPTION, name); +// putValue(MNEMONIC_KEY, KeyEvent.VK_R); +// putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke("R")); + setEnabled(false); + } + + + public void actionPerformed(ActionEvent e) { + Marking initialMarking = root.getDocument().petriNet.getInitialMarking(); + if (root.getClickedElement() != null) { + if (root.getClickedElement() instanceof PlaceNode) { + PlaceNode placeNode = (PlaceNode) root.getClickedElement(); + int tokenLimit = placeNode.getTokenLimit(); + String response = JOptionPane.showInputDialog(root.getParentFrame(), "Token limit (0 = no limit) :", tokenLimit); + if (response != null) { + try { + tokenLimit = Integer.parseInt(response); + } catch (NumberFormatException exception) { + JOptionPane.showMessageDialog(root.getParentFrame(), exception.getMessage() + " is not a number"); + } + + if (tokenLimit < 0) { + tokenLimit = placeNode.getTokenLimit(); // restore old value + JOptionPane.showMessageDialog(root.getParentFrame(), "Token limit must be non-negative"); + } + } + + if (placeNode.getTokenLimit() != tokenLimit) { + //placeNode.setTokenLimit(tokenLimit); + root.getUndoManager().executeCommand(new SetTokenLimitCommand(placeNode, tokenLimit, initialMarking)); + } + } + } + } + +} diff --git a/src/org/pneditor/editor/commands/SetTokenLimitCommand.java b/src/org/pneditor/editor/commands/SetTokenLimitCommand.java new file mode 100644 index 0000000..912c298 --- /dev/null +++ b/src/org/pneditor/editor/commands/SetTokenLimitCommand.java @@ -0,0 +1,64 @@ +/* + * Copyright (C) 2008-2010 Martin Riesz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + */ +package org.pneditor.editor.commands; + +import org.pneditor.petrinet.Marking; +import org.pneditor.petrinet.PlaceNode; +import org.pneditor.util.Command; + +/** + * + * @author Martin Riesz + */ +public class SetTokenLimitCommand implements Command { + + private PlaceNode placeNode; + private int newLimitValue; + private Marking marking; + + + public SetTokenLimitCommand(PlaceNode placeNode, int limit, Marking marking) { + this.placeNode = placeNode; + this.newLimitValue = limit; + this.marking = marking; + } + + private int oldLimitValue; + private int oldTokenValue; + + + public void execute() { + this.oldTokenValue = marking.getTokens(placeNode); + this.oldLimitValue = placeNode.getTokenLimit(); + + placeNode.setTokenLimit(newLimitValue); + } + + public void undo() { + this.placeNode.setTokenLimit(oldLimitValue); + this.marking.setTokens(this.placeNode, this.oldTokenValue); + } + + public void redo() { + execute(); + } + + @Override + public String toString() { + return "Set/unset place node token limit"; + } +} From a07ebef94e974946f32ca9e165b72fbe752ab5cf Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 3 Mar 2019 17:22:13 +0100 Subject: [PATCH 04/13] Modified the xml model and save/load xslt files so that toke limits can be saved and load now This still allows previous saves to load --- src/org/pneditor/petrinet/xml/DocumentExporter.java | 1 + src/org/pneditor/petrinet/xml/DocumentImporter.java | 1 + src/org/pneditor/petrinet/xml/XmlPlace.java | 2 ++ src/xslt/load.xslt | 3 ++- src/xslt/save.xslt | 3 ++- 5 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/org/pneditor/petrinet/xml/DocumentExporter.java b/src/org/pneditor/petrinet/xml/DocumentExporter.java index fd2204c..da9a290 100644 --- a/src/org/pneditor/petrinet/xml/DocumentExporter.java +++ b/src/org/pneditor/petrinet/xml/DocumentExporter.java @@ -131,6 +131,7 @@ private XmlPlace getXmlPlace(Place place, Marking initialMarking) { xmlPlace.x = place.getCenter().x; xmlPlace.y = place.getCenter().y; xmlPlace.isStatic = place.isStatic(); + xmlPlace.tokenLimit = place.getTokenLimit(); xmlPlace.label = place.getLabel(); xmlPlace.tokens = initialMarking.getTokens(place); return xmlPlace; diff --git a/src/org/pneditor/petrinet/xml/DocumentImporter.java b/src/org/pneditor/petrinet/xml/DocumentImporter.java index 5620195..4e1e650 100644 --- a/src/org/pneditor/petrinet/xml/DocumentImporter.java +++ b/src/org/pneditor/petrinet/xml/DocumentImporter.java @@ -189,6 +189,7 @@ private Place getNewPlace(XmlPlace xmlPlace) { place.setId(xmlPlace.id); place.setLabel(xmlPlace.label); place.setStatic(xmlPlace.isStatic); + place.setTokenLimit(xmlPlace.tokenLimit); place.setCenter(xmlPlace.x, xmlPlace.y); return place; } diff --git a/src/org/pneditor/petrinet/xml/XmlPlace.java b/src/org/pneditor/petrinet/xml/XmlPlace.java index 4500fbd..9c2937f 100644 --- a/src/org/pneditor/petrinet/xml/XmlPlace.java +++ b/src/org/pneditor/petrinet/xml/XmlPlace.java @@ -33,4 +33,6 @@ public class XmlPlace extends XmlNode { @XmlElement(name = "isStatic") public boolean isStatic; + @XmlElement(name = "tokenLimit") + public int tokenLimit; } diff --git a/src/xslt/load.xslt b/src/xslt/load.xslt index 7a99aa0..620113b 100644 --- a/src/xslt/load.xslt +++ b/src/xslt/load.xslt @@ -39,7 +39,8 @@ along with this program. If not, see . - + + diff --git a/src/xslt/save.xslt b/src/xslt/save.xslt index 8c6a634..e10a660 100644 --- a/src/xslt/save.xslt +++ b/src/xslt/save.xslt @@ -39,7 +39,8 @@ along with this program. If not, see . - + + From 108cae6265c2acdf86262acb0e5342c7926c96d8 Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 3 Mar 2019 17:24:28 +0100 Subject: [PATCH 05/13] Modified the Boundedness algorithm bounded network detected as unbounded. --- .../editor/actions/algorithms/BoundednessAction.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java index f89442f..ef0ce3d 100644 --- a/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java +++ b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java @@ -112,7 +112,7 @@ private boolean isOmega(Marking newMarking, Marking oldMarking) { Place oldMarkingPlace = null; for (Place place : oldMarkingPlaces) { - if (place.equals(newMarkingPlace)) { + if (place.equals(newMarkingPlace)) { oldMarkingPlace = place; break; } @@ -123,7 +123,12 @@ private boolean isOmega(Marking newMarking, Marking oldMarking) { if (!(newTokens >= oldTokens)) { return false; } else if (newTokens > oldTokens) { - isOneSharplyHigher = true; + if (newMarkingPlace.getTokenLimit()==0) { + // If a place has a token limit, it means that this specific place + // is assured to be bounded ; thus, even if the tokens can raise + // inquantity here, it has to stop. + isOneSharplyHigher = true; + } } } From f166245e65d36b8199da0a3e1a25c56a4d7916b3 Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 3 Mar 2019 17:28:47 +0100 Subject: [PATCH 06/13] Added the icon for the token limit in the context menu --- src/resources/pneditor/tokenLimit.gif | Bin 0 -> 866 bytes 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 src/resources/pneditor/tokenLimit.gif diff --git a/src/resources/pneditor/tokenLimit.gif b/src/resources/pneditor/tokenLimit.gif new file mode 100644 index 0000000000000000000000000000000000000000..93a05ab55daaf4550febbd11bb8b912612adbf76 GIT binary patch literal 866 zcmZ?wbhEHb6krfw_|56TXK0V7I N+sNcZae@PbH2~>VB254Q literal 0 HcmV?d00001 From df08610fd4f0f71cf89033f48ab0faf24dff9874 Mon Sep 17 00:00:00 2001 From: lducerf Date: Fri, 8 Mar 2019 17:41:06 +0100 Subject: [PATCH 07/13] Fixed a bug where using the + token tool on a place with already max tokens and then undoing last action would remove a token on that place AddTokenCommand now register number of tokens on node and put that value when undoing instead of removing a token --- src/org/pneditor/editor/commands/AddTokenCommand.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/org/pneditor/editor/commands/AddTokenCommand.java b/src/org/pneditor/editor/commands/AddTokenCommand.java index 9b725c9..479d732 100644 --- a/src/org/pneditor/editor/commands/AddTokenCommand.java +++ b/src/org/pneditor/editor/commands/AddTokenCommand.java @@ -34,12 +34,15 @@ public AddTokenCommand(PlaceNode placeNode, Marking marking) { this.marking = marking; } + private int oldValue; + public void execute() { + oldValue = marking.getTokens(placeNode); marking.setTokens(placeNode, marking.getTokens(placeNode) + 1); } public void undo() { - new RemoveTokenCommand(placeNode, marking).execute(); + marking.setTokens(placeNode, oldValue); } public void redo() { From 12a099ccaf5171e0f97557c71099286fc6ac4baf Mon Sep 17 00:00:00 2001 From: lducerf Date: Sun, 10 Mar 2019 22:09:40 +0100 Subject: [PATCH 08/13] updtated author of created methods --- src/org/pneditor/editor/actions/SetTokenLimitAction.java | 4 +--- src/org/pneditor/editor/commands/SetTokenLimitCommand.java | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/org/pneditor/editor/actions/SetTokenLimitAction.java b/src/org/pneditor/editor/actions/SetTokenLimitAction.java index c7bdeef..6efe2a7 100644 --- a/src/org/pneditor/editor/actions/SetTokenLimitAction.java +++ b/src/org/pneditor/editor/actions/SetTokenLimitAction.java @@ -30,7 +30,7 @@ /** * - * @author Martin Riesz + * @author Ladislas Ducerf */ /* @@ -48,8 +48,6 @@ public SetTokenLimitAction(Root root) { putValue(NAME, name); putValue(SMALL_ICON, GraphicsTools.getIcon("pneditor/tokenLimit.gif")); putValue(SHORT_DESCRIPTION, name); -// putValue(MNEMONIC_KEY, KeyEvent.VK_R); -// putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke("R")); setEnabled(false); } diff --git a/src/org/pneditor/editor/commands/SetTokenLimitCommand.java b/src/org/pneditor/editor/commands/SetTokenLimitCommand.java index 912c298..4e045f7 100644 --- a/src/org/pneditor/editor/commands/SetTokenLimitCommand.java +++ b/src/org/pneditor/editor/commands/SetTokenLimitCommand.java @@ -22,7 +22,7 @@ /** * - * @author Martin Riesz + * @author Ladislas Ducerf */ public class SetTokenLimitCommand implements Command { From f2631a34dacc527e0c077620d74d6a6ab17cd7a6 Mon Sep 17 00:00:00 2001 From: lducerf Date: Tue, 12 Mar 2019 23:15:47 +0100 Subject: [PATCH 09/13] Solved a bug that occurred when a place had both an outgoing and incoming arc for the same transition and a limit --- .../actions/algorithms/BoundednessAction.java | 51 ++++++++++--------- src/org/pneditor/petrinet/Marking.java | 32 ++++++++++-- 2 files changed, 56 insertions(+), 27 deletions(-) diff --git a/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java index ef0ce3d..3796eb0 100644 --- a/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java +++ b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java @@ -107,29 +107,34 @@ private boolean isOmega(Marking newMarking, Marking oldMarking) { boolean isOneSharplyHigher = false; for (Place newMarkingPlace : newMarkingPlaces) { - - int newTokens = newMarking.getTokens(newMarkingPlace); - - Place oldMarkingPlace = null; - for (Place place : oldMarkingPlaces) { - if (place.equals(newMarkingPlace)) { - oldMarkingPlace = place; - break; - } - } - - int oldTokens = oldMarking.getTokens(oldMarkingPlace); - - if (!(newTokens >= oldTokens)) { - return false; - } else if (newTokens > oldTokens) { - if (newMarkingPlace.getTokenLimit()==0) { - // If a place has a token limit, it means that this specific place - // is assured to be bounded ; thus, even if the tokens can raise - // inquantity here, it has to stop. - isOneSharplyHigher = true; - } - } + + if (newMarkingPlace.getTokenLimit()==0) { + + + int newTokens = newMarking.getTokens(newMarkingPlace); + + Place oldMarkingPlace = null; + for (Place place : oldMarkingPlaces) { + if (place.equals(newMarkingPlace)) { + oldMarkingPlace = place; + break; + } + } + + int oldTokens = oldMarking.getTokens(oldMarkingPlace); + + if (!(newTokens >= oldTokens)) { + return false; + } else if (newTokens > oldTokens) { + isOneSharplyHigher = true; + /*if (newMarkingPlace.getTokenLimit()==0) { + // If a place has a token limit, it means that this specific place + // is assured to be bounded ; thus, even if the tokens can raise + // in quantity here, it has to stop. + isOneSharplyHigher = true; + }*/ + } + } } diff --git a/src/org/pneditor/petrinet/Marking.java b/src/org/pneditor/petrinet/Marking.java index 4977af6..074d50a 100644 --- a/src/org/pneditor/petrinet/Marking.java +++ b/src/org/pneditor/petrinet/Marking.java @@ -141,9 +141,15 @@ public void setTokens(PlaceNode placeNode, int tokens) { */ public boolean isEnabled(Transition transition) { boolean isEnabled = true; + ArrayList originPlaces = new ArrayList(); + ArrayList originPlacesArcMultiplicity = new ArrayList(); + int tokens = 0; + int index = -6; + PlaceNode place = null; + int arcMul = 0; lock.readLock().lock(); try { - for (Arc arc : transition.getConnectedArcs()) { + for (Arc arc : transition.getConnectedArcs()) {// first it iterates over incoming arcs if (arc.isPlaceToTransition()) { if (arc.getType().equals(Arc.RESET)) {//reset arc is always fireable continue; //but can be blocked by other arcs @@ -152,6 +158,10 @@ public boolean isEnabled(Transition transition) { if (getTokens(arc.getPlaceNode()) < arc.getMultiplicity()) { //normal arc isEnabled = false; break; + } else { + originPlaces.add(arc.getPlaceNode()); + originPlacesArcMultiplicity.add(arc.getMultiplicity()); + //this construct a list of the places that will lose tokens and how many } } else { if (getTokens(arc.getPlaceNode()) >= arc.getMultiplicity()) {//inhibitory arc @@ -160,8 +170,23 @@ public boolean isEnabled(Transition transition) { } } } - } else { // arc is from transition to place - int tokens = getTokens(arc.getPlaceNode()); + } + } + for(Arc arc : transition.getConnectedArcs()) { // then it iterates over outcoming arcs + if(!arc.isPlaceToTransition()) { // arc is from transition to place + place = arc.getPlaceNode(); + System.out.println(place); + //we can now use the list to see if the node will consume token with the firing + tokens = getTokens(place); + index = originPlaces.indexOf(place); + System.out.println(index); + if(index>=0) { + arcMul = originPlacesArcMultiplicity.get(index); + tokens = tokens - arcMul; + //thus, is this transition will be fired, it will consume arcMul tokens so we update that number + // it is always a non-negative integer ; otherwise, this would have detected the transition as + // not enabled in the previous for loop + } if (!tokenLimitCompliant(arc.getPlaceNode(), tokens + arc.getMultiplicity())) { isEnabled = false; break; @@ -230,7 +255,6 @@ public boolean fire(Transition transition) { return success; } - //TODO: Check for token limit ? public boolean canBeUnfired(Transition transition) { boolean canBeUnfired = true; lock.readLock().lock(); From 32ef673b4866c59dc1c81ca979588da0628e00ed Mon Sep 17 00:00:00 2001 From: lducerf Date: Tue, 12 Mar 2019 23:21:39 +0100 Subject: [PATCH 10/13] updated README.md --- README.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/README.md b/README.md index 95d6ad8..96ffc80 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,18 @@ PNEditor (Petri Net editor) ======== +Status of the different branches : +Invariant : adds a token limit on places +MacroRecorder : abandonned branche (a version of macro that had modifications from invariant) +MacroRecorderClean : adds a macro manager +MacroLimit : integrates the token limit and the macro manager +macroAndTokenLimit : integrates the token limit, the macro manager and the fire N modification +from https://github.com/e17goudi/pneditor. due to some modifications on the marking class there, +this version compile but has some bugs (try to find them !) + + + +======== You can download PNEditor from [www.pneditor.org](http://www.pneditor.org/) Features: From 5bda790d55ef41b52eaa33ebca93114de6cb6690 Mon Sep 17 00:00:00 2001 From: lducerf Date: Tue, 12 Mar 2019 23:26:33 +0100 Subject: [PATCH 11/13] updated README.md --- README.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 96ffc80..d0bffdf 100644 --- a/README.md +++ b/README.md @@ -2,17 +2,16 @@ PNEditor (Petri Net editor) ======== Status of the different branches : -Invariant : adds a token limit on places -MacroRecorder : abandonned branche (a version of macro that had modifications from invariant) -MacroRecorderClean : adds a macro manager -MacroLimit : integrates the token limit and the macro manager -macroAndTokenLimit : integrates the token limit, the macro manager and the fire N modification +- Invariant : adds a token limit on places +- MacroRecorder : abandonned branche (a version of macro that had modifications from invariant) +- MacroRecorderClean : adds a macro manager +- MacroLimit : integrates the token limit and the macro manager +- macroAndTokenLimit : integrates the token limit, the macro manager and the fire N modification from https://github.com/e17goudi/pneditor. due to some modifications on the marking class there, this version compile but has some bugs (try to find them !) -======== You can download PNEditor from [www.pneditor.org](http://www.pneditor.org/) Features: From 8ee77a0e4b06c642a55d9854c7ec7de96e63cd2a Mon Sep 17 00:00:00 2001 From: lducerf Date: Tue, 12 Mar 2019 23:56:30 +0100 Subject: [PATCH 12/13] The BoundednessAction is now back to the previous (unaltered by me) version Proving the boundedness on a Petri Net with token limit on places seems difficult and out of my league Now, the output precises that the rsults ignore token limits. --- .../actions/algorithms/BoundednessAction.java | 51 ++++++++----------- 1 file changed, 20 insertions(+), 31 deletions(-) diff --git a/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java index 3796eb0..7c29e69 100644 --- a/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java +++ b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java @@ -61,9 +61,9 @@ public void actionPerformed(ActionEvent e) { } if (isUnboundedness) { - JOptionPane.showMessageDialog(root.getParentFrame(), "PetriNet is NOT bounded ", "Algorithm output", JOptionPane.INFORMATION_MESSAGE); + JOptionPane.showMessageDialog(root.getParentFrame(), "PetriNet is NOT bounded \n(This ignore token limits)", "Algorithm output", JOptionPane.INFORMATION_MESSAGE); } else { - JOptionPane.showMessageDialog(root.getParentFrame(), "PetriNet is bounded", "Algorithm output", JOptionPane.INFORMATION_MESSAGE); + JOptionPane.showMessageDialog(root.getParentFrame(), "PetriNet is bounded \n(This ignore token limits)", "Algorithm output", JOptionPane.INFORMATION_MESSAGE); } } @@ -107,36 +107,25 @@ private boolean isOmega(Marking newMarking, Marking oldMarking) { boolean isOneSharplyHigher = false; for (Place newMarkingPlace : newMarkingPlaces) { - - if (newMarkingPlace.getTokenLimit()==0) { - - - int newTokens = newMarking.getTokens(newMarkingPlace); - - Place oldMarkingPlace = null; - for (Place place : oldMarkingPlaces) { - if (place.equals(newMarkingPlace)) { - oldMarkingPlace = place; - break; - } - } - - int oldTokens = oldMarking.getTokens(oldMarkingPlace); - - if (!(newTokens >= oldTokens)) { - return false; - } else if (newTokens > oldTokens) { - isOneSharplyHigher = true; - /*if (newMarkingPlace.getTokenLimit()==0) { - // If a place has a token limit, it means that this specific place - // is assured to be bounded ; thus, even if the tokens can raise - // in quantity here, it has to stop. - isOneSharplyHigher = true; - }*/ - } - } - } + int newTokens = newMarking.getTokens(newMarkingPlace); + + Place oldMarkingPlace = null; + for (Place place : oldMarkingPlaces) { + if (place.equals(newMarkingPlace)) { + oldMarkingPlace = place; + break; + } + } + + int oldTokens = oldMarking.getTokens(oldMarkingPlace); + + if (!(newTokens >= oldTokens)) { + return false; + } else if (newTokens > oldTokens) { + isOneSharplyHigher = true; + } + } if (isOneSharplyHigher) { return true; From 5c415f0e8013c172bfb2ff64104408c0f039ed86 Mon Sep 17 00:00:00 2001 From: lducerf Date: Wed, 13 Mar 2019 00:08:20 +0100 Subject: [PATCH 13/13] removed system.out.println --- src/org/pneditor/petrinet/Marking.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/org/pneditor/petrinet/Marking.java b/src/org/pneditor/petrinet/Marking.java index 074d50a..56b4cdf 100644 --- a/src/org/pneditor/petrinet/Marking.java +++ b/src/org/pneditor/petrinet/Marking.java @@ -175,11 +175,9 @@ public boolean isEnabled(Transition transition) { for(Arc arc : transition.getConnectedArcs()) { // then it iterates over outcoming arcs if(!arc.isPlaceToTransition()) { // arc is from transition to place place = arc.getPlaceNode(); - System.out.println(place); //we can now use the list to see if the node will consume token with the firing tokens = getTokens(place); index = originPlaces.indexOf(place); - System.out.println(index); if(index>=0) { arcMul = originPlacesArcMultiplicity.get(index); tokens = tokens - arcMul;