Merge lp:~tapaal-contributor/tapaal/tikz-export-label-placement-1820528 into lp:tapaal

[Peter Haahr Taankvist]

Label placement for places and transitions when exporting to tikz now functions the same as for arcs, meaning that there is still a slight rounding issue where the label positions are skewed.

[Jiri Srba (srba)]

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/pipe/gui/TikZExporter.java'
--- src/pipe/gui/TikZExporter.java	2019-03-16 13:01:21 +0000
+++ src/pipe/gui/TikZExporter.java	2019-03-18 17:00:20 +0000
@@ -120,6 +120,8 @@
 			out.append(" (");
 			out.append(arc.getTarget().getId());
 			out.append(") {};\n");
+			if(arcLabel != "")
+				out.append("%% Label for arc between " + arc.getSource().getName() + " and " + arc.getTarget().getName() + "\n");
 			out.append(arcLabel);
 		}
 		return out;
@@ -168,11 +170,7 @@
 				angle = ",rotate=" + String.valueOf(trans.getAngle() + 90);
 
 			out.append("\\node[transition");
-			out.append(angle);
-			if (trans.getAttributesVisible()){
-				out.append(",label=135:");
-				out.append(exportMathName(trans.getName()));
-			}			
+			out.append(angle);		
 			out.append("] at (");
 			out.append(RoundCoordinate(trans.getPositionX()));
 			out.append(',');
@@ -189,13 +187,22 @@
 				out.append(".center) { };\n");
 			}
                         
-                        if(((TimedTransitionComponent)trans).underlyingTransition().isUrgent()){
+			if(((TimedTransitionComponent)trans).underlyingTransition().isUrgent()){
 				out.append("\\node[urgenttransition");
 				out.append(angle);
 				out.append("] at (");
 				out.append(trans.getId());
 				out.append(".center) { };\n");
 			}
+			if (trans.getAttributesVisible()){
+				out.append("%% label for transition " + trans.getName() + "\n");
+				out.append("\\draw (");
+				out.append(RoundCoordinate(trans.getNameLabel().getXPosition()) + "," + (RoundCoordinate(trans.getNameLabel().getYPosition()) * -1) + ")");
+				out.append(" node ");
+				out.append(" {");
+				out.append(exportMathName(trans.getName()));
+				out.append("};\n");
+			}	
 		}
 		return out;
 	}
@@ -207,12 +214,6 @@
 			String tokensInPlace = getTokenListStringFor(place);
 
 			out.append("\\node[place");
-			if (place.getAttributesVisible()){
-				out.append(",label=135:");
-				out.append(exportMathName(place.getName()));
-			}	
-			out.append(',');
-			out.append(invariant);
 			out.append(tokensInPlace);
 			out.append("] at (");
 			out.append(RoundCoordinate(place.getPositionX()));
@@ -227,6 +228,23 @@
 				out.append(place.getId());
 				out.append(".center) { };\n");
 			}
+			if (place.getAttributesVisible() || invariant != ""){
+				out.append("%% label for place " + place.getName() + "\n");
+				out.append("\\draw (");
+				out.append(RoundCoordinate(place.getNameLabel().getXPosition()) + "," + (RoundCoordinate(place.getNameLabel().getYPosition()) * -1) + ")");
+				out.append(" node[align=left] ");
+				out.append("{");
+				if(place.getAttributesVisible())
+					out.append(exportMathName(place.getName()));					
+				if(invariant != "") {
+					if((place.getAttributesVisible()))
+						out.append("\\\\");
+					out.append(invariant);
+				}else {
+					out.append("};\n");
+				}
+					
+			}	
 		}
 
 		return out;
@@ -239,7 +257,7 @@
 		String tokensInPlace = "";
 		if (tokens.size() > 0) {
 			if (tokens.size() == 1 && !net.netType().equals(NetType.UNTIMED)) {
-				tokensInPlace = "structured tokens={" + tokens.get(0).age().setScale(1) + "},";
+				tokensInPlace = ", structured tokens={" + tokens.get(0).age().setScale(1) + "},";
 			} else {
 				tokensInPlace = exportMultipleTokens(tokens);
 			}
@@ -252,14 +270,14 @@
 		String invariant = "";
 
 		if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf"))
-			invariant = "label=315:inv: $\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$,";
+			invariant = "$\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$};\n";
 		return invariant;
 	}
 
 	private String exportMultipleTokens(List<TimedToken> tokens) {
 		StringBuffer out = new StringBuffer();
 
-		out.append("structured tokens={\\#");
+		out.append(", structured tokens={\\#");
 		out.append(String.valueOf(tokens.size()));
 		out.append("},");
 		if (!net.netType().equals(NetType.UNTIMED)) {
@@ -282,8 +300,8 @@
                 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("%% arc 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 of the respective arc\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("\\tikzstyle{arc}=[->,>=stealth,thick]\n");
 
 		if (!net.netType().equals(NetType.UNTIMED)) out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n");
@@ -294,7 +312,7 @@
 		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{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]");
 		return out;
 	}