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/README.md b/README.md index 95d6ad8..d0bffdf 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,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 +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/) 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..6efe2a7 --- /dev/null +++ b/src/org/pneditor/editor/actions/SetTokenLimitAction.java @@ -0,0 +1,83 @@ +/* + * 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 Ladislas Ducerf + */ + +/* + * + * 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); + 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/actions/algorithms/BoundednessAction.java b/src/org/pneditor/editor/actions/algorithms/BoundednessAction.java index f89442f..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); } } @@ -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,10 +123,9 @@ private boolean isOmega(Marking newMarking, Marking oldMarking) { if (!(newTokens >= oldTokens)) { return false; } else if (newTokens > oldTokens) { - isOneSharplyHigher = true; + isOneSharplyHigher = true; } - - } + } if (isOneSharplyHigher) { return true; 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() { diff --git a/src/org/pneditor/editor/commands/SetTokenLimitCommand.java b/src/org/pneditor/editor/commands/SetTokenLimitCommand.java new file mode 100644 index 0000000..4e045f7 --- /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 Ladislas Ducerf + */ +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"; + } +} diff --git a/src/org/pneditor/petrinet/Marking.java b/src/org/pneditor/petrinet/Marking.java index bdaa94e..56b4cdf 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); + } } } @@ -139,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 @@ -150,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 @@ -158,6 +170,25 @@ 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(); + //we can now use the list to see if the node will consume token with the firing + tokens = getTokens(place); + index = originPlaces.indexOf(place); + 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; + } } } } finally { @@ -165,6 +196,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 +252,7 @@ public boolean fire(Transition transition) { } return success; } - + public boolean canBeUnfired(Transition transition) { boolean canBeUnfired = true; lock.readLock().lock(); 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); 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/resources/pneditor/tokenLimit.gif b/src/resources/pneditor/tokenLimit.gif new file mode 100644 index 0000000..93a05ab Binary files /dev/null and b/src/resources/pneditor/tokenLimit.gif differ 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 . - + +