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

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.

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

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-17 17:11:33 +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] (");
 			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]");
+			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.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";
-            }
-    	}
-		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) {
@@ -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,38 @@
             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]));
+                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 +395,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 +531,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 +556,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 +574,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");
+    }
 }