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

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

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-02-21 19:46:59 +0000
+++ src/net/tapaal/export/TikZExporter.java	2022-03-07 14:26:18 +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,19 @@
 			}
 
 			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(" {");
+			out.append(handleNameLabel(arc.getNameLabel().getText()));
+            out.append("} ");
+			out.append("(" + arc.getTarget().getId() + ");\n");
 		}
 		return out;
 	}
@@ -142,50 +143,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 +152,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 +184,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 +219,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 +273,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 +288,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 +393,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 +529,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 +554,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 +572,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");
+    }
 }