GUI passes constants to verifydtapn - fix 2046038 (#125)

Fixes: https://bugs.launchpad.net/tapaal/+bug/2046038
TAPAAL · Dec 20, 2023 · 8b9858c · 8b9858c
2 parents cb85057 + d8f6a59
commit 8b9858c
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 6 deletions.
diff --git a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java b/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java
@@ -61,6 +61,7 @@ public class TimedArcPetriNetNetworkWriter implements NetWriter {
     private boolean secondTransport = false;
     private int transporCountID = 0;
     private final TAPNLens lens;
+	private boolean saveConstantNames;
 
     public TimedArcPetriNetNetworkWriter(
 			TimedArcPetriNetNetwork network, 
@@ -131,6 +132,12 @@ public ByteArrayOutputStream savePNML() throws ParserConfigurationException, DOM
 	}
 
 	public void savePNML(File file) throws IOException, ParserConfigurationException, DOMException, TransformerException {
+		savePNML(file, true);
+	}
+
+	public void savePNML(File file, boolean saveConstantNames) throws IOException, ParserConfigurationException, DOMException, TransformerException {
+		this.saveConstantNames = saveConstantNames;
+
 		Require.that(file != null, "Error: file to save to was null");
 
 		try {
@@ -539,7 +546,7 @@ private void createColoredInvariants(TimedPlace inputPlace, Document document, E
             Element colortype = document.createElement("colortype");
             colortype.setAttribute("name", coloredTimeInvariant.getColor().getColorType().getName());
             if (coloredTimeInvariant.equalsOnlyColor(ColoredTimeInvariant.LESS_THAN_INFINITY_AND_STAR)) {
-                placeElement.setAttribute("inscription", coloredTimeInvariant.getInvariantString());
+                placeElement.setAttribute("inscription", coloredTimeInvariant.getInvariantString(saveConstantNames));
             } else {
                 if (coloredTimeInvariant.getColor().getTuple() != null) {
                     for (Color color : coloredTimeInvariant.getColor().getTuple()) {
@@ -552,7 +559,8 @@ private void createColoredInvariants(TimedPlace inputPlace, Document document, E
                     colorEle.setAttribute("value", coloredTimeInvariant.getColor().getColorName());
                     colortype.appendChild(colorEle);
                 }
-                inscription.setAttribute("inscription", coloredTimeInvariant.getInvariantString());
+
+                inscription.setAttribute("inscription", coloredTimeInvariant.getInvariantString(saveConstantNames));
                 invariant.appendChild(inscription);
                 invariant.appendChild(colortype);
                 placeElement.appendChild(invariant);
@@ -627,6 +635,7 @@ private Element createArcElement(Arc inputArc, DataLayer guiModel, Document docu
                         secondTransport = true;
                     }
                 }
+
 				arcElement.setAttribute("type", getInputArcTypeAsString((TimedInputArcComponent)inputArc));
 				arcElement.setAttribute("inscription", getGuardAsString((TimedInputArcComponent)inputArc));	
 				arcElement.setAttribute("weight", inputArc.getWeight().nameForSaving(true)+"");
@@ -655,12 +664,12 @@ private void appendArcIntervals(TimedInputArcComponent inputArc, Document docume
 
         for (ColoredTimeInterval cti : ctiList) {
             if (cti.equalsOnlyColor(ColoredTimeInterval.ZERO_INF_DYN_COLOR(Color.STAR_COLOR))) {
-                arcElement.setAttribute("inscription", cti.getInterval());
+                arcElement.setAttribute("inscription", cti.getInterval(saveConstantNames));
             } else {
                 Element interval = document.createElement("colorinterval");
                 Element inscription = document.createElement("inscription");
                 Element colortype = document.createElement("colortype");
-                inscription.setAttribute("inscription", cti.getInterval());
+                inscription.setAttribute("inscription", cti.getInterval(saveConstantNames));
                 colortype.setAttribute("name", cti.getColor().getColorType().getName());
                 if (cti.getColor().getTuple() != null) {
                     for (Color color : cti.getColor().getTuple()) {

diff --git a/src/main/java/dk/aau/cs/model/CPN/ColoredTimeInterval.java b/src/main/java/dk/aau/cs/model/CPN/ColoredTimeInterval.java
@@ -104,6 +104,10 @@ public String getInterval() {
         return super.toString();
     }
 
+    public String getInterval(boolean displayConstantNames) {
+        return super.toString(displayConstantNames);
+    }
+
     @Override
     public boolean equals(Object o) {
         ColoredTimeInterval cti;

diff --git a/src/main/java/dk/aau/cs/model/CPN/ColoredTimeInvariant.java b/src/main/java/dk/aau/cs/model/CPN/ColoredTimeInvariant.java
@@ -68,6 +68,11 @@ public String getInvariantString() {
         return super.toString();
     }
 
+    public String getInvariantString(boolean displayConstantNames) {
+        return super.toString(displayConstantNames);
+    }
+
+
     @Override
     public boolean equals(Object o) {
         ColoredTimeInvariant cti;

diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTACPNExporter.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTACPNExporter.java
@@ -43,7 +43,7 @@ protected void outputModel(TimedArcPetriNet model, File modelFile, NameMapping m
         TimedArcPetriNetNetworkWriter writerTACPN = new TimedArcPetriNetNetworkWriter(model.parentNetwork(), templates, queries, model.parentNetwork().constants());
 
         try {
-            writerTACPN.savePNML(modelFile);
+            writerTACPN.savePNML(modelFile, false);
         } catch (IOException | ParserConfigurationException | TransformerException e) {
             e.printStackTrace();
         }

diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java b/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java
@@ -108,7 +108,7 @@ protected String doInBackground() throws Exception {
             templates.add(new Template(transformedModel.value1(), composer.getGuiModel(), new Zoomer()));
             if(lens.isTimed()){
                 TimedArcPetriNetNetworkWriter writerTACPN = new TimedArcPetriNetNetworkWriter(network, templates, queries, model.constants());
-                writerTACPN.savePNML(modelFile);
+                writerTACPN.savePNML(modelFile, false);
             } else{
                 var guiModels = new HashMap<TimedArcPetriNet, DataLayer>();
                 guiModels.put(transformedModel.value1(),composer.getGuiModel());