diff --git a/.gitignore b/.gitignore index 7056b34ea..c1744b973 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ .gradle .idea +.vscode .r .bzr-repo build diff --git a/src/main/java/dk/aau/cs/io/LoadTACPN.java b/src/main/java/dk/aau/cs/io/LoadTACPN.java index 62e1a35af..7996bcf24 100644 --- a/src/main/java/dk/aau/cs/io/LoadTACPN.java +++ b/src/main/java/dk/aau/cs/io/LoadTACPN.java @@ -171,7 +171,7 @@ private void parseNamedSort(Node node, TimedArcPetriNetNetwork network) throws F // Parse prodcut types last as they can used color types not yet declared productTypes.add(node); } else { - ColorType ct = new ColorType(name, id); + ColorType ct = new ColorType(name); if (typetag.equals("dot")) { return; } else if (typetag.equals("finiteintrange")){ diff --git a/src/main/java/dk/aau/cs/model/CPN/ColorType.java b/src/main/java/dk/aau/cs/model/CPN/ColorType.java index bffb2e5ae..354c5a22d 100644 --- a/src/main/java/dk/aau/cs/model/CPN/ColorType.java +++ b/src/main/java/dk/aau/cs/model/CPN/ColorType.java @@ -137,7 +137,7 @@ public boolean contains(Color color){ } return false; } - + public Color getColorByName(String name){ for (Color c : colors) { if(c.getColorName().equals(name)){ diff --git a/src/main/java/dk/aau/cs/model/CPN/Expressions/TupleExpression.java b/src/main/java/dk/aau/cs/model/CPN/Expressions/TupleExpression.java index 24b124dee..ea2466e1a 100644 --- a/src/main/java/dk/aau/cs/model/CPN/Expressions/TupleExpression.java +++ b/src/main/java/dk/aau/cs/model/CPN/Expressions/TupleExpression.java @@ -48,17 +48,15 @@ public List eval(ExpressionContext context) { @Override public boolean containsColor(Color color) { boolean containsColor = false; - Vector tuple = color.getTuple(); - if (tuple != null && tuple.size() == colors.size()) { - containsColor = true; - for (int i = 0; i < tuple.size(); i++) { - if (!colors.get(i).containsColor(tuple.get(i))) { - containsColor = false; - break; - } + + for (int i = 0; i < colors.size(); ++i) { + if (colors.get(i).containsColor(color)) { + containsColor = true; + break; } } - return containsColor || equals(color); + + return containsColor; } @Override 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 f51c92997..f859d8de7 100644 --- a/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java +++ b/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java @@ -10,7 +10,6 @@ import dk.aau.cs.model.tapn.Bound.InfBound; import dk.aau.cs.util.IntervalOperations; import dk.aau.cs.util.Require; -import net.tapaal.gui.petrinet.TAPNLens; public class TimedArcPetriNet { private String name; 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 1c895ca44..cd27d01fe 100644 --- a/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java +++ b/src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java @@ -836,43 +836,50 @@ private void isColorTypeUsedInVariable(ColorType colorType, List message } } - public boolean canColorBeRemoved(Color color, ArrayList messages) { - isColorTypeUsedInProduct(color.getColorType(), messages); + public boolean canColorBeRemoved(Color color, List messages) { for (TimedArcPetriNet tapn : allTemplates()) { for (TimedPlace p : tapn.places()) { - if (p.getTokensAsExpression() != null && p.getTokensAsExpression().containsColor(color)) { + if (p.getTokensAsExpression() != null && + p.getTokensAsExpression().containsColor(color)) { messages.add(color.getName() + " is used in a token in place " + p.name() + " \n"); } + for (ColoredTimeInvariant invariant : p.getCtiList()) { if (invariant.getColor().equals(color)) { messages.add(color.getName() + " is used in an invariant in place " + p.name() + " \n"); } } } + for (TimedTransition t : tapn.transitions()) { if (t.getGuard() != null && t.getGuard().containsColor(color)) { messages.add(color.getName() + " of color type is used in transition " + t.name() + "\n"); } } + for (TransportArc arc : tapn.transportArcs()) { if (arc.getInputExpression().containsColor(color)) { messages.add(color.getName() + " is used on transport arc from " + arc.source().name() + " to " + arc.transition() + "\n"); } + if (arc.getOutputExpression().containsColor(color)) { messages.add(color.getName() + " is used on transport arc from " + arc.transition()+ " to " + arc.destination().name() + "\n"); } } + for (TimedInputArc arc : tapn.inputArcs()) { if (arc.getArcExpression().containsColor(color)) { messages.add(color.getName() + " is used on arc from " + arc.source().name() + " to " + arc.destination().name() + "\n"); } } + for (TimedOutputArc arc : tapn.outputArcs()) { if (arc.getExpression().containsColor(color)) { messages.add(color.getName() + " is used on arc from " + arc.source().name() + " to " + arc.destination().name() + "\n"); } } } + return messages.isEmpty(); } diff --git a/src/main/java/net/tapaal/gui/petrinet/editor/ColorComboboxPanel.java b/src/main/java/net/tapaal/gui/petrinet/editor/ColorComboboxPanel.java index 121b148eb..376d6803a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/editor/ColorComboboxPanel.java +++ b/src/main/java/net/tapaal/gui/petrinet/editor/ColorComboboxPanel.java @@ -36,7 +36,6 @@ public JComboBox[] getColorTypeComboBoxesArray() { private void initPanel() { colorcomboBoxPanel = new JPanel(); colorcomboBoxPanel.setLayout(new GridBagLayout()); - //This panel contains all comboboxes, there can be more than one with ProductTypes comboBoxPanel = new JPanel(new GridBagLayout()); //In case it is a really large product type we have a scrollPane diff --git a/src/main/java/net/tapaal/gui/petrinet/undo/Command.java b/src/main/java/net/tapaal/gui/petrinet/undo/Command.java index 00b6d6552..d1d7f2ece 100644 --- a/src/main/java/net/tapaal/gui/petrinet/undo/Command.java +++ b/src/main/java/net/tapaal/gui/petrinet/undo/Command.java @@ -2,5 +2,5 @@ public interface Command { void undo(); - void redo(); + void redo(); } diff --git a/src/main/javacc/dk/aau/cs/model/CPN/ConstantsParser/ConstantsParser.jj b/src/main/javacc/dk/aau/cs/model/CPN/ConstantsParser/ConstantsParser.jj index eedfe4e9a..84781bac1 100644 --- a/src/main/javacc/dk/aau/cs/model/CPN/ConstantsParser/ConstantsParser.jj +++ b/src/main/javacc/dk/aau/cs/model/CPN/ConstantsParser/ConstantsParser.jj @@ -7,10 +7,22 @@ package dk.aau.cs.model.CPN.ConstantsParser; import java.io.StringReader; import java.util.ArrayList; import java.util.List; + +import dk.aau.cs.model.CPN.Color; import dk.aau.cs.model.CPN.ColorType; +import dk.aau.cs.model.CPN.ColoredTimeInvariant; +import dk.aau.cs.model.tapn.TimedInputArc; +import dk.aau.cs.model.tapn.TimedOutputArc; +import dk.aau.cs.model.tapn.TimedTransition; import dk.aau.cs.model.tapn.Constant; +import dk.aau.cs.model.tapn.TimedArcPetriNet; import dk.aau.cs.model.CPN.Variable; import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.model.tapn.TimedPlace; +import dk.aau.cs.model.CPN.Expressions.ArcExpression; +import dk.aau.cs.model.tapn.TimedToken; +import dk.aau.cs.model.CPN.ColorMultiset; + import java.util.HashMap; import java.util.Map; import java.util.LinkedHashMap; @@ -80,29 +92,79 @@ public class ConstantsParser { for (Variable v : network.variables()) { List messagesList = new ArrayList(); constantsMap.put(v.getName(), v); - boolean canBeEdited = !(variables.containsKey(v.getName()) && !variables.get(v.getName()).getColorType().equals(v.getColorType())); + boolean canBeEdited = true; + if (variables.containsKey(v.getName())) { + ColorType ct = variables.get(v.getName()).getColorType(); + canBeEdited = ct.equals(v.getColorType()); + } + canBeRemovedBitMap.put(v.getName(), network.canVariableBeRemoved(v, messagesList) && canBeEdited); messages.put(v.getName(), messagesList); } // Generate error messages for (String key : canBeRemovedBitMap.keySet()) { - boolean skip = false; if (constants.containsKey(key) || variables.containsKey(key) && canBeRemovedBitMap.get(key) || - key.equals("dot") || - colorTypes.containsKey(key) && - colorTypes.get(key).equals(constantsMap.get(key))) { + key.equals("dot")) { continue; } else if (variables.containsKey(key) && !canBeRemovedBitMap.get(key)) { + boolean skip = false; for (Variable v : network.variables()) { if (v.getName().equals(key)) { - skip = v.getColorType().equals(variables.get(key).getColorType()); + skip = v.getColorType().getName().equals(variables.get(key).getColorType().getName()); + break; } } - } - if (skip) continue; + if (skip) continue; + } else if (colorTypes.containsKey(key)) { + if (colorTypes.get(key).equals(constantsMap.get(key))) continue; + + ColorType newCt = colorTypes.get(key); + ColorType ct = (ColorType)constantsMap.get(key); + + if (ct instanceof ProductType) { + ProductType pct = (ProductType)ct; + ProductType newPct = (ProductType)newCt; + + // Update product color types to new color types + for (ColorType colorType : pct.getProductColorTypes()) { + newPct.replaceColorType(colorType, (ColorType)colorTypes.get(colorType.getName())); + } + + boolean isSimiliar = pct.getProductColorTypes().size() == newPct.getProductColorTypes().size() && pct.containsTypes(newPct.getColorTypes()); + if (isSimiliar) { + updateColorTypes(pct, newPct); + continue; + } + } else { + List removedColors = new ArrayList(); + for (Color color : ct.getColorList()) { + if (!newCt.contains(color)) { + removedColors.add(color); + } + } + + int removeableColors = 0; + for (Color c : removedColors) { + List newMessagesList = new ArrayList(); + boolean colorCanBeRemoved = network.canColorBeRemoved(c, newMessagesList); + if (colorCanBeRemoved) { + ++removeableColors; + } else { + List messagesList = new ArrayList(); + messagesList.addAll(newMessagesList); + messages.put(key, messagesList); + } + } + + if (removeableColors == removedColors.size()) { + updateColorTypes(ct, newCt); + continue; + } + } + } Object obj = constantsMap.get(key); if (!canBeRemovedBitMap.get(key)) { @@ -131,7 +193,7 @@ public class ConstantsParser { if (!(obj instanceof Constant)) { message += " for the following reasons: \n\n"; - message += String.join("\n", messages.get(key)); + message += String.join("", messages.get(key)); } else { message += " because it is in use"; } @@ -169,6 +231,81 @@ public class ConstantsParser { throw new ParseException("Variable with name \"" + id + "\" already exists"); } } + + private static void updateColorTypes(ColorType ct, ColorType newCt) { + for (TimedArcPetriNet tapn : network.allTemplates()) { + for (TimedPlace place : tapn.places()) { + if (place.getColorType().equals(ct)) { + if (place.getTokensAsExpression() != null) { + place.setTokenExpression(place.getTokensAsExpression().getExprConverted(ct, newCt)); + } + + List oldTokens = new ArrayList(place.tokens()); + place.setColorType(newCt); + for (TimedToken token : oldTokens) { + if (token.getColor() != null && newCt.contains(token.getColor())) { + place.addToken(new TimedToken(place, token.age(), newCt.getColorByName(token.getColor().getName()))); + } + } + } + + ArcExpression expression = place.getExprWithNewColorType(newCt); + if (expression != place.getTokensAsExpression()) { + ColorMultiset cm = expression.eval(network.getContext()); + if (cm != null) { + List tokensToAdd = new ArrayList(place.tokens()); + for (TimedToken token : cm.getTokens(place)) { + tapn.marking().remove(token); + } +; + place.updateTokens(tokensToAdd, expression); + } + } + + List invariantsToAdd = new ArrayList(); + for (ColoredTimeInvariant invariant : place.getCtiList()) { + if (ct.contains(invariant.getColor())) { + invariantsToAdd.add(new ColoredTimeInvariant(invariant.isUpperNonstrict(), invariant.upperBound(), ct.getColorByName(invariant.getColor().getColorName()))); + } else { + invariantsToAdd.add(invariant); + } + } + + place.setCtiList(invariantsToAdd); + } + + for (TimedInputArc arc : tapn.inputArcs()) { + if (arc.getArcExpression() != null) { + arc.setExpression(arc.getArcExpression().getExprWithNewColorType(ct)); + } + } + + for (TimedOutputArc arc : tapn.outputArcs()) { + if (arc.getExpression() != null) { + arc.setExpression(arc.getExpression().getExprWithNewColorType(ct)); + } + } + + for (TimedTransition transition : tapn.transitions()) { + if (transition.getGuard() != null) { + transition.getGuard().setColorType(ct); + } + } + } + + for (ColorType networkCt : network.colorTypes()) { + if (networkCt instanceof ProductType) { + ProductType networkPct = (ProductType)networkCt; + networkPct.replaceColorType(ct, newCt); + } + } + + for (Variable var : network.variables()) { + if (var.getColorType().equals(newCt)) { + var.setColorType(ct); + } + } + } } PARSER_END(ConstantsParser) @@ -263,7 +400,6 @@ void colorTypes() : if (product.equals("dot")) { ColorType dot = new ColorType("dot"); dot.addColor("dot"); - pct.addType(dot); continue; } @@ -276,7 +412,19 @@ void colorTypes() : } ct = pct; - } else if (!isProductList.value) { + } else if (isIntList.value) { + ct = new ColorType(id.image); + int lowerBound = Integer.parseInt(values.get(0)); + int upperBound = Integer.parseInt(values.get(1)); + + if (lowerBound > upperBound) { + throw new ParseException("Lower bound must be lower than or equal to upper bound"); + } + + for (int i = lowerBound; i <= upperBound; ++i) { + ct.addColor(Integer.toString(i)); + } + } else { ct = new ColorType(id.image); Set uniqueVals = new HashSet(); for (String color : values) {