Merge lp:~tapaal-contributor/tapaal/cpn-gui-TikZ-support into lp:~tapaal-contributor/tapaal/cpn-gui-dev

[Kristian Morsing Pedersen]

Added TikZ support for colored nets.
Added a framed box to the Tikz output for global variables/constants/color types.

The TikZ export now shows all of the new features associated with colored nets.
Also added a framed box that contains all the global variables, constants and/or color types for a given net.

[lp:~tapaal-contributor/tapaal/cpn-gui-TikZ-support]

1572. By Kristian Morsing Pedersen <email address hidden> on 2022-02-09

Removed subscripting from place- and transition names, and changed \mathrm to \mathit

1573. By Kristian Morsing Pedersen <email address hidden> on 2022-02-17

Added new adjustment options for labels on arcs, places and transitions

1574. By Kristian Morsing Pedersen <email address hidden> on 2022-02-17

Merged with cpn-gui-dev

1575. By Kristian Morsing Pedersen <email address hidden> on 2022-02-21

Labels with multiple lines on arcs now displays correctly

1576. By Kristian Morsing Pedersen <email address hidden> on 2022-03-06

Changed default pos of arc labels to 0.5

1577. By Kristian Morsing Pedersen <email address hidden> on 2022-03-06

Resolved merge conflicts

1578. By Kristian Morsing Pedersen <email address hidden> on 2022-03-07

Removed redundant \\ and changed 0,0 -> 0.0 for age of tokens in initial markings

1579. By Kristian Morsing Pedersen <email address hidden> on 2022-03-09

Changed x -> \times in inhibitor arcs

Unmerged revisions

=== modified file 'src/net/tapaal/export/TikZExporter.java'
--- src/net/tapaal/export/TikZExporter.java	2022-01-07 17:05:54 +0000
+++ src/net/tapaal/export/TikZExporter.java	2022-02-09 20:32:33 +0000
@@ -3,22 +3,27 @@
 import java.io.FileWriter;
 import java.io.IOException;
 import java.io.PrintWriter;
-import java.util.List;
+import java.util.*;
+import java.util.stream.Collectors;
 
+import dk.aau.cs.model.CPN.Color;
+import dk.aau.cs.model.CPN.ColorType;
+import dk.aau.cs.model.CPN.Variable;
+import dk.aau.cs.model.tapn.Constant;
 import dk.aau.cs.model.tapn.TimedToken;
 
+import net.tapaal.gui.petrinet.Context;
 import pipe.gui.petrinet.dataLayer.DataLayer;
 import pipe.gui.TAPAALGUI;
-import pipe.gui.petrinet.graphicElements.Arc;
-import pipe.gui.petrinet.graphicElements.ArcPathPoint;
-import pipe.gui.petrinet.graphicElements.Place;
-import pipe.gui.petrinet.graphicElements.Transition;
+import pipe.gui.petrinet.graphicElements.*;
 import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent;
 import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent;
 import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent;
 import pipe.gui.petrinet.graphicElements.tapn.TimedTransitionComponent;
 import pipe.gui.petrinet.graphicElements.tapn.TimedTransportArcComponent;
 
+import static java.util.stream.Collectors.toList;
+
 public class TikZExporter {
 
 	public enum TikZOutputOption {
@@ -45,7 +50,7 @@
 			if (option == TikZOutputOption.FULL_LATEX) {
 				out.println("\\documentclass[a4paper]{article}");
 				out.println("\\usepackage{tikz}");
-				out.println("\\usetikzlibrary{petri,arrows}");
+				out.println("\\usetikzlibrary{petri,arrows,positioning}");
 				out.println("\\usepackage{amstext}");
 				out.println();
 				out.println("\\begin{document}");
@@ -62,6 +67,8 @@
 			out.print(exportTransitions(net.getTransitions()));
 			out.print(exportArcs(net.getArcs()));
 
+            out.println(exportGlobalVariables());
+
 			out.println("\\end{tikzpicture}");
 			if (option == TikZOutputOption.FULL_LATEX) {
 				out.println("\\end{document}");
@@ -144,48 +151,22 @@
 
 	protected String getArcLabels(Arc arc) {
 		String arcLabel = "";
-		String arcLabelPositionString = "\\draw (" + (arc.getNameLabel().getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node {";
-
-		if (arc instanceof TimedInputArcComponent) {
-            if (!(arc.getSource() instanceof TimedTransitionComponent)) {
-				arcLabel = arcLabelPositionString;
-                if (arc.getWeight().value() > 1) {
-                        arcLabel += "$" + arc.getWeight().value() + "\\times$\\ ";
-                }
-
-                if(TAPAALGUI.getApp().getCurrentTab().getLens().isTimed()) {
-                    arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$";
-                    if (arc instanceof TimedTransportArcComponent)
-                        arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr();
-                    arcLabel += "};\n";
-                } else {
-                    arcLabel += "};\n";
-                }
-
-			} else {
-				arcLabel = arcLabelPositionString;
-                if (arc.getWeight().value() > 1) {
-                        arcLabel += "$" + arc.getWeight().value() + "\\times$\\ ";
-                }
-				arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr() + "};\n";
-			}
-
-		} else {
-            if (arc.getWeight().value() > 1) {
-                arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n";
-            }
-    	}
+		String arcLabelPositionString = "\\draw (" + (arc.getArcPath().midPoint.getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node[align=left,xshift=0pt,yshift=0pt] {";
+
+        if(!arc.getNameLabel().getText().isEmpty()) {
+            arcLabel += arcLabelPositionString;
+            arcLabel += "\\\\" + handleNameLabel(arc.getNameLabel().getText()) + "";
+        }
+
+        if(!arcLabel.isEmpty()) {
+            arcLabel += "};\n";
+        } else {
+            arcLabel += "{};\n";
+        }
+
 		return arcLabel;
 	}
 
-	private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) {
-        if (!TAPAALGUI.getApp().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){
-			return "";
-		} else {
-			return arc.getGuardAsString();
-		}
-	}
-
 	private StringBuffer exportTransitions(Transition[] transitions) {
 		StringBuffer out = new StringBuffer();
 		for (Transition trans : transitions) {
@@ -234,9 +215,10 @@
 				out.append("%% label for transition " + trans.getName() + "\n");
 				out.append("\\draw (");
 				out.append(trans.getNameLabel().getX() + xOffset + "," + (trans.getNameLabel().getY() * -1) + ")");
-				out.append(" node ");
+				out.append(" node[align=left,xshift=0pt,yshift=0pt]");
 				out.append(" {");
-				out.append(exportMathName(trans.getName()));
+				out.append("$\\mathit{" + (trans.getName().replace("_","\\_")) + "}$");
+				out.append(handleNameLabel(trans.getNameLabel().getText()));
 				out.append("};\n");
 			}	
 		}
@@ -247,7 +229,7 @@
 		StringBuffer out = new StringBuffer();
 
 		for (Place place : places) {
-			String invariant = getPlaceInvariantString(place);
+			String invariant = "$" + getPlaceInvariantString(place) + "$";
 			String tokensInPlace = getTokenListStringFor(place);
 
 			out.append("\\node[place");
@@ -269,30 +251,58 @@
 			if (place.getAttributesVisible() || !invariant.equals("")){
 			    boolean isLabelAbovePlace = place.getY() > place.getNameLabel().getY();
 			    boolean isLabelBehindPlace = place.getX() < place.getNameLabel().getX();
-			    double xOffset = place.getName().length() > 6 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0;
-			    double yOffset = isLabelAbovePlace ? (place.getNameLabel().getHeight() / 2) : 0;
+                int longestString = 0;
+                List<String> listStringNameLabel = place.getNameLabel().getText().lines().collect(toList());
+                for(int i = 0; i < listStringNameLabel.size(); i++) {
+                    if(listStringNameLabel.get(i).length() > longestString) {
+                        longestString = listStringNameLabel.get(i).length();
+                    }
+                }
+			    double xOffset = longestString > 8 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0;
+			    double yOffset = place.getNameLabel().getText().lines().count() * 5;
+
+			    String nameLabel = place.getNameLabel().getText();
 
 				out.append("%% label for place " + place.getName() + "\n");
 				out.append("\\draw (");
-				out.append((place.getNameLabel().getX() + xOffset)  + "," + ((place.getNameLabel().getY() * -1) + yOffset) +")");
-				out.append(" node[align=left] ");
+				out.append((place.getNameLabel().getX() + xOffset)  + "," + ((place.getNameLabel().getY() + yOffset) * -1) +")");
+				out.append(" node[align=left,xshift=0pt,yshift=0pt] ");
 				out.append("{");
-				if(place.getAttributesVisible())
-					out.append(exportMathName(place.getName()));					
-				if(!invariant.equals("")) {
-					if((place.getAttributesVisible()))
-						out.append("\\\\");
-					out.append(invariant);
-				}else {
-					out.append("};\n");
-				}
-					
+				if(place.getAttributesVisible()) {
+                    out.append("$\\mathit{" + (place.getName().replace("_","\\_")) + "}$");
+                    if (!place.getNameLabel().getText().isEmpty()) {
+                        out.append(handleNameLabel(nameLabel));
+                    }
+                }
+                out.append("};\n");
 			}
 		}
-
 		return out;
 	}
 
+	private String handleNameLabel(String nameLabel) {
+	    String nameLabelsString = "";
+        String[] labelsInName = nameLabel.split("\n");
+        for(int i = 0; i < labelsInName.length; i++) {
+
+            if(labelsInName[i].contains("[")) {
+                nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i]));
+                nameLabelsString += "\\\\";
+            }
+            else if(!labelsInName[i].isEmpty()){
+                nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i]));
+                nameLabelsString += "\\\\";
+            } else {
+                nameLabelsString += "\\\\";
+            }
+        }
+        return nameLabelsString;
+    }
+
+    private String escapeSpacesInAndOrNot(String str) {
+        return str.replace(" and ", "\\ and\\ ").replace(" or", "\\ or\\ ").replace(" not", "\\ not\\ ");
+    }
+
 	private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) {
         // Dot radius
         final double tRadius = 1;
@@ -437,6 +447,116 @@
         }
     }
 
+    private StringBuffer exportGlobalVariables() {
+        StringBuffer out = new StringBuffer();
+
+	    Context context = new Context(TAPAALGUI.getCurrentTab());
+        List<ColorType> listColorTypes = context.network().colorTypes();
+        List<Constant> constantsList = new ArrayList<>(context.network().constants());
+        List<Variable> variableList = context.network().variables();
+
+        if(!context.network().isColored() || (listColorTypes.isEmpty() && constantsList.isEmpty() && variableList.isEmpty())) {
+            out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {");
+            exportConstants(constantsList, out);
+            out.append("};");
+            return out;
+        }
+
+        out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {");
+
+        exportColorTypes(listColorTypes, out);
+
+        if(listColorTypes.size() > 0 && (variableList.size() > 0 || constantsList.size() > 0)) {
+            out.append("\\\\");
+        }
+
+        exportVariables(variableList, out);
+
+        if(variableList.size() > 0 && !constantsList.isEmpty()) {
+            out.append("\\\\");
+        }
+
+        exportConstants(constantsList, out);
+
+        out.append("};");
+
+        return out;
+    }
+
+    private void exportColorTypes(List<ColorType> listColorTypes, StringBuffer out) {
+	    String stringColorList = "";
+        for(int i = 0; i < listColorTypes.size(); i++) {
+            if(i == 0) {
+                out.append("Color Types:\\\\");
+            }
+            out.append("$\\mathit{" + listColorTypes.get(i).getName() + "}$ \\textbf{is} ");
+
+            if(listColorTypes.get(i).isProductColorType()) {
+                out.append("$\\mathit{<");
+                for(int x = 0; x < listColorTypes.get(i).getProductColorTypes().size(); x++) {
+                    stringColorList += listColorTypes.get(i).getProductColorTypes().get(x).getName().replace("_", "\\_");
+
+                    if(x != listColorTypes.get(i).getProductColorTypes().size() - 1){
+                        stringColorList += ", ";
+                    }
+                }
+                out.append(stringColorList + ">}$\\\\");
+                stringColorList = "";
+
+            } else if(listColorTypes.get(i).isIntegerRange()) {
+                out.append("$\\mathit{");
+                if(listColorTypes.get(i).size() > 1) {
+                    int listSize = listColorTypes.get(i).size();
+                    out.append("[" + listColorTypes.get(i).getColors().get(0).getColorName().replace("_","\\_") + ".." + listColorTypes.get(i).getColors().get(listSize - 1).getColorName().replace("_","\\_") + "]");
+                } else {
+                    out.append("[" + listColorTypes.get(i).getFirstColor().getColorName().replace("_","\\_") + "]");
+                }
+                out.append("}$\\\\");
+
+            } else {
+                out.append("$\\mathit{[");
+                for(int x = 0; x < listColorTypes.get(i).getColors().size(); x++) {
+                    stringColorList += listColorTypes.get(i).getColors().get(x).getName().replace("_","\\_");
+
+                    if(x != listColorTypes.get(i).getColors().size() - 1){
+                        stringColorList += ", ";
+                    }
+                }
+                out.append(stringColorList + "]}$\\\\");
+                stringColorList = "";
+            }
+        }
+    }
+
+    private void exportVariables(List<Variable> variableList, StringBuffer out) {
+	    String result = "";
+        for(int i = 0; i < variableList.size(); i++) {
+            if (i == 0) {
+                result += "Variables:\\\\ ";
+            }
+            result += "$\\mathit{" + variableList.get(i).getName().replace("_","\\_") + " \\textbf{ in } " + variableList.get(i).getColorType().getName().replace("_","\\_") + "}$";
+            if(i != variableList.size() - 1) {
+                result += "\\\\";
+            }
+        }
+        out.append(result);
+    }
+
+    private void exportConstants(List<Constant> constantsList, StringBuffer out) {
+        String result = "";
+
+        for(int i = 0; i < constantsList.size(); i++) {
+            if(i == 0) {
+                result += "Constants:\\\\";
+            }
+            result += "$\\mathit{" + constantsList.get(i).toString().replace("_","\\_") + "}$";
+            if(i != constantsList.size() - 1) {
+                result += "\\\\";
+            }
+        }
+        out.append(result);
+    }
+
 	protected String getTokenListStringFor(Place place) {
 		List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens();
 
@@ -455,7 +575,7 @@
         String invariant = "";
 
 		if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf"))
-			invariant = "$\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$};\n";
+			invariant = replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "};\n";
 		return invariant;
 	}
 
@@ -480,12 +600,13 @@
 		StringBuffer out = new StringBuffer();
 
 		out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n");
-                out.append("%% the figure can be scaled by changing xscale and yscale\n");
+                out.append("%% the figure can be scaled by changing xscale and yscale or the size of the x- and y-coordinates\n");
                 out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n");
                 out.append("%% can be adjusted so that they do not cover arcs\n");
                 out.append("%% similarly the curving of arcs can be done by adjusting bend left/right=XX\n");
-                out.append("%% labels may be slightly skewed compared to the tapaal drawing due to rounding.\n");
-                out.append("%% This can be adjusted by tuning the coordinates of the label\n");
+                out.append("%% labels may be slightly skewed compared to the Tapaal drawing due to rounding.\n");
+                out.append("%% This can be adjusted by tuning the coordinates of the label or adjusting the x- and y-shift for the label\n");
+                out.append("%% The box containing global variables can also be moved by adjusting the anchor points / bounding box in the [globalBox] node at the end of the Tikz document\n");
 		out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n");
 
         out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n");
@@ -496,39 +617,24 @@
 		out.append("\\tikzstyle{every token}=[fill=white,text=black]\n");
 		out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n");
 		out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n");
-		out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]");
-        out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]");
+		out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]\n");
+        out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]\n");
+        out.append("\\tikzstyle{globalBox} = [draw,thick,align=left]");
         return out;
 	}
 
 	protected String replaceWithMathLatex(String text) {
-		return text.replace("inf", "\\infty").replace("<=", "\\leq ").replace("*", "\\cdot ");
-	}
-
-	private String exportMathName(String name) {
-		StringBuilder out = new StringBuilder("$\\mathrm{");
-		int subscripts = 0;
-		for (int i = 0; i < name.length() - 1; i++) {
-			char c = name.charAt(i);
-			if (c == '_') {
-				out.append("_{");
-				subscripts++;
-			} else {
-				out.append(c);
-			}
-		}
-
-		char last = name.charAt(name.length() - 1);
-		if (last == '_') {
-			out.append("\\_");
-		} else
-			out.append(last);
-
-		for (int i = 0; i < subscripts; i++) {
-			out.append('}');
-		}
-		out.append("}$");
-		return out.toString();
-	}
-
+	    String[] stringList = text.split(" ");
+	    String result = "";
+
+	    for(int i = 0; i < stringList.length; i++) {
+	        result += "$\\mathit{" + replaceSpecialSymbols(stringList[i]) + "}$ ";
+        }
+	    return result;
+	}
+
+	protected String replaceSpecialSymbols(String text) {
+	    return text.replace("inf", "\\infty").replace("<=", "\\leq").replace("*", "\\cdot")
+                   .replace("\u2192", "\\rightarrow").replace("\u221E", "\\infty");
+    }
 }