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.
Removed subscripiting from transition- and place names
Changed \mathrm to \mathit
Added more adjustment options for transitions, places and arcs
Merged with cpn-gui-dev

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.
Subscripting from transition- and place names have been removed, so it looks more like the GUI.
\mathrm has also been replaces with \mathit.

[Kenneth Yrke Jørgensen (yrke)]

review: Approve (code)

[Jiri Srba (srba)]

It would be nice if instead of (in referendum colored timed):

1′v[1, 2]Voters1 → [1, 4]

one would print:

1′v
[1, 2]
Voters1 → [1, 4]

(on three sepratate lines).

review: Needs Fixing

[Jiri Srba (srba)]

Please, set the default position for arc lables to pos=0.5

review: Needs Fixing

[Jiri Srba (srba)]

At the end of the labels, there is a redundant \\ that makes the spacing look ugly. E.g. in

\node[place, label={[align=left,label distance=0cm]270:$\mathrm{voting} ... $\mathit{4}$ \\}] at (390,-345) (voting) {};

The label should finish with just ... $\mathit{4}$ }] without the extra \\

review: Needs Fixing

[Jiri Srba (srba)]

Also, when exporting age of tokens in the initial marking, please write 0.0 instead of 0,0

review: Needs Fixing

[Jiri Srba (srba)]

In the tikz export of weights, please use 10\times instead of 10x.

Also, nets that are not colored seem to be exported without the relative label positions. Could all nets be exported to Tikz using the same relative positions as for CPNs?

review: Needs Fixing

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

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

Changed x -> \times in inhibitor arcs

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/net/tapaal/export/TikZExporter.java'
--- src/net/tapaal/export/TikZExporter.java	2022-02-21 19:46:59 +0000
+++ src/net/tapaal/export/TikZExporter.java	2022-03-09 14:15:46 +0000
@@ -3,16 +3,17 @@
 import java.io.FileWriter;
 import java.io.IOException;
 import java.io.PrintWriter;
-import java.util.List;
+import java.util.*;
 
+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;
@@ -45,7 +46,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 +63,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}");
@@ -94,7 +97,7 @@
                 ArcPathPoint currentPoint = arc.getArcPath().getArcPathPoint(i);
 
                 if(currentPoint.getPointType() == ArcPathPoint.STRAIGHT) {
-                    arcPoints += "to[bend right=0] (" + (currentPoint.getX()) + "," + (currentPoint.getY() * (-1)) + ") ";
+                    arcPoints += "to [bend right=0] (" + (currentPoint.getX()) + "," + (currentPoint.getY() * (-1)) + ") ";
                 } else if (currentPoint.getPointType() == ArcPathPoint.CURVED) {
                     double xCtrl1 = Math.round(currentPoint.getControl1().getX());
                     double yCtrl1 = Math.round(currentPoint.getControl1().getY() * (-1));
@@ -109,21 +112,25 @@
 			}
 
 			String arrowType = getArcArrowType(arc);
-			String arcLabel = getArcLabels(arc);
 
+            out.append("% Arc between " + arc.getSource().getName() + " and " + arc.getTarget().getName() + "\n");
 			out.append("\\draw[");
 			out.append(arrowType);
-			out.append("] (");
+			out.append(",pos=0.5] (");
 			out.append(arc.getSource().getId());
 			out.append(") ");
 			out.append(arcPoints);
-			out.append("to[bend right=0]");
-			out.append(" (");
-			out.append(arc.getTarget().getId());
-			out.append(") {};\n");
-			if(!arcLabel.equals(""))
-				out.append("%% Label for arc between " + arc.getSource().getName() + " and " + arc.getTarget().getName() + "\n");
-			out.append(arcLabel);
+			out.append("to node[bend right=0,auto,align=left]");
+			out.append(" {");
+
+			if(arrowType.equals("inhibArc")) {
+                out.append(handleNameLabel(arc.getNameLabel().getText().replace("x","\\times")));
+            } else {
+                out.append(handleNameLabel(arc.getNameLabel().getText()));
+            }
+
+            out.append("} ");
+			out.append("(" + arc.getTarget().getId() + ");\n");
 		}
 		return out;
 	}
@@ -142,50 +149,6 @@
         return arrowType;
     }
 
-	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.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";
-            }
-    	}
-		return arcLabel;
-	}
-
-	private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) {
-        if (!TAPAALGUI.getAppGui().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){
-			return "";
-		} else {
-			return arc.getGuardAsString();
-		}
-	}
-
 	private StringBuffer exportTransitions(Transition[] transitions) {
 		StringBuffer out = new StringBuffer();
 		for (Transition trans : transitions) {
@@ -195,7 +158,8 @@
 
 
 			out.append("\\node[transition");
-			out.append(angle);		
+			out.append(angle);
+			out.append(handlePlaceAndTransitionLabel(trans.getNameLabel().getText(), trans.getName(), trans.getAttributesVisible()));
 			out.append("] at (");
 			out.append((trans.getPositionX()));
 			out.append(',');
@@ -226,31 +190,30 @@
                 out.append(trans.getId());
                 out.append(".center) { };\n");
             }
-			if (trans.getAttributesVisible()){
-                boolean isLabelAboveTransition = trans.getY() > trans.getNameLabel().getY();
-                boolean isLabelBehindTrans = trans.getX() < trans.getNameLabel().getX();
-                double xOffset = trans.getName().length() > 5 && !isLabelAboveTransition && !isLabelBehindTrans ? trans.getLayerOffset() : 0;
-
-				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(" {");
-				out.append(exportMathName(trans.getName()));
-				out.append("};\n");
-			}	
 		}
 		return out;
 	}
 
+	private String handlePlaceAndTransitionLabel(String nameLabelText, String name, boolean isVisible) {
+	    if(!isVisible)
+	        return "";
+
+	    String result = ", label={[align=left,label distance=0cm]90:";
+	    result += "$\\mathrm{" + (name.replace("_","\\_")) + "}$";
+	    result += handleNameLabel(nameLabelText);
+	    result += "}";
+	    return result;
+    }
+
 	private StringBuffer exportPlacesWithTokens(Place[] places) {
 		StringBuffer out = new StringBuffer();
 
 		for (Place place : places) {
-			String invariant = getPlaceInvariantString(place);
+			String invariant = "$" + getPlaceInvariantString(place) + "$";
 			String tokensInPlace = getTokenListStringFor(place);
 
 			out.append("\\node[place");
+			out.append(handlePlaceAndTransitionLabel(place.getNameLabel().getText(), place.getName(), place.getAttributesVisible()));
 			out.append("] at (");
 			out.append(place.getPositionX());
 			out.append(',');
@@ -262,37 +225,36 @@
             exportPlaceTokens(place, out, ((TimedPlaceComponent) place).underlyingPlace().tokens().size());
 			
 			if(((TimedPlaceComponent)place).underlyingPlace().isShared()){
-				out.append("\\node[sharedplace] at (");
+				out.append("\\node[sharedplace ");
+                out.append("] at (");
 				out.append(place.getId());
 				out.append(".center) { };\n");
 			}
-			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;
-
-				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("{");
-				if(place.getAttributesVisible())
-					out.append(exportMathName(place.getName()));					
-				if(!invariant.equals("")) {
-					if((place.getAttributesVisible()))
-						out.append("\\\\");
-					out.append(invariant);
-				}else {
-					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]));
+            }
+            else if(!labelsInName[i].isEmpty()){
+                nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i]));
+            }
+            if(i != labelsInName.length - 1) {
+                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;
@@ -317,14 +279,14 @@
                     out.append(",");
                     out.append(placeYpos + 4);
                     out.append(")");
-                    out.append("{0,0};\n");
+                    out.append("{0.0};\n");
 
                     out.append("\\node at ("); // Bottom
                     out.append(placeXpos);
                     out.append(",");
                     out.append(placeYpos - 5);
                     out.append(")");
-                    out.append("{0,0};\n");
+                    out.append("{0.0};\n");
                     return;
                 case 1:
                     out.append("\\node at ("); // Top
@@ -332,7 +294,7 @@
                     out.append(",");
                     out.append(placeYpos);
                     out.append(")");
-                    out.append("{0,0};\n");
+                    out.append("{0.0};\n");
                     return;
                 default:
                     out.append("\\node at (");
@@ -437,6 +399,124 @@
         }
     }
 
+    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()) {
+            if(constantsList.isEmpty()) {
+                return out;
+            }
+            out.append("%%Global box which contains global color types, variables and/or constants.\n");
+            out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {");
+            exportConstants(constantsList, out);
+            out.append("};");
+            return out;
+        }
+
+        if((listColorTypes.isEmpty() && constantsList.isEmpty() && variableList.isEmpty()))
+            return out;
+
+        out.append("%%Global box which contains global color types, variables and/or constants.\n");
+        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 +535,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 +560,14 @@
 		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("%% these can be adjusted by adjusting either the coordinates, the label distance or the label degree\n");
+                out.append("%% that is placed right after the 'label-distance'. 90: is above (default), 180 is left, 270 is below etc.\n");
+                out.append("%% 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, or the degree (see above)\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 +578,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");
+    }
 }