Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Issues when using manual edit with color types - fix 2081345 #179

Merged
merged 13 commits into from
Oct 10, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
.gradle
.idea
.vscode
.r
.bzr-repo
build
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/dk/aau/cs/io/LoadTACPN.java
Original file line number Diff line number Diff line change
Expand Up @@ -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")){
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/dk/aau/cs/model/CPN/ColorType.java
Original file line number Diff line number Diff line change
Expand Up @@ -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)){
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -48,17 +48,15 @@ public List<Color> eval(ExpressionContext context) {
@Override
public boolean containsColor(Color color) {
boolean containsColor = false;
Vector<Color> 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
Expand Down
1 change: 0 additions & 1 deletion src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNet.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
13 changes: 10 additions & 3 deletions src/main/java/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java
Original file line number Diff line number Diff line change
Expand Up @@ -836,43 +836,50 @@ private void isColorTypeUsedInVariable(ColorType colorType, List<String> message
}
}

public boolean canColorBeRemoved(Color color, ArrayList<String> messages) {
isColorTypeUsedInProduct(color.getColorType(), messages);
public boolean canColorBeRemoved(Color color, List<String> 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();
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/net/tapaal/gui/petrinet/undo/Command.java
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@

public interface Command {
void undo();
void redo();
void redo();
}
170 changes: 159 additions & 11 deletions src/main/javacc/dk/aau/cs/model/CPN/ConstantsParser/ConstantsParser.jj
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -80,29 +92,79 @@ public class ConstantsParser {
for (Variable v : network.variables()) {
List<String> messagesList = new ArrayList<String>();
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<Color> removedColors = new ArrayList<Color>();
for (Color color : ct.getColorList()) {
if (!newCt.contains(color)) {
removedColors.add(color);
}
}

int removeableColors = 0;
for (Color c : removedColors) {
List<String> newMessagesList = new ArrayList<String>();
boolean colorCanBeRemoved = network.canColorBeRemoved(c, newMessagesList);
if (colorCanBeRemoved) {
++removeableColors;
} else {
List<String> messagesList = new ArrayList<String>();
messagesList.addAll(newMessagesList);
messages.put(key, messagesList);
}
}

if (removeableColors == removedColors.size()) {
updateColorTypes(ct, newCt);
continue;
}
}
}

Object obj = constantsMap.get(key);
if (!canBeRemovedBitMap.get(key)) {
Expand Down Expand Up @@ -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";
}
Expand Down Expand Up @@ -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<TimedToken> oldTokens = new ArrayList<TimedToken>(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<TimedToken> tokensToAdd = new ArrayList<TimedToken>(place.tokens());
for (TimedToken token : cm.getTokens(place)) {
tapn.marking().remove(token);
}
;
place.updateTokens(tokensToAdd, expression);
}
}

List<ColoredTimeInvariant> invariantsToAdd = new ArrayList<ColoredTimeInvariant>();
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)
Expand Down Expand Up @@ -263,7 +400,6 @@ void colorTypes() :
if (product.equals("dot")) {
ColorType dot = new ColorType("dot");
dot.addColor("dot");

pct.addType(dot);
continue;
}
Expand All @@ -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<String> uniqueVals = new HashSet<String>();
for (String color : values) {
Expand Down
Loading