Merge lp:~tapaal-contributor/tapaal/fix-tikz-export-1945642 into lp:tapaal

[Kristian Morsing Pedersen]

Improved quality of Tikz export and various fixes

1. Fixed transition rotation
2. Added support for dots (replaces marking #1-5 with dots, like in the GUI)
3. Now correctly shows a place's marking (#1-2) like in the GUI
4. Improved location of place labels
5. Improved location of transition labels
6. Improved location of arc labels
7. Improved scaling so that some nets are no longer 'squished' together
8. Now currecly exports curved arcs

Other comments:
In some nets, labels for places, transitions and arcs are not positioned optimally like in the GUI. It has been difficult to find a solution to this, as some ways works for some of the nets while making other nets looks significantly worse. I'm not sure why this is. I have a suspicion it is due to the X- and Y coordinates of the labels somehow not being correct, or due to some other unintentional sideeffects. I have tried a lot of different ways to place these labels as close as possible, and have settled on the current result.

[lp:~tapaal-contributor/tapaal/fix-tikz-export-1945642]

1156. By Kristian Morsing Pedersen <email address hidden> on 2021-10-14

Now correctly show transition rotations for 45 degree angles

1157. By <email address hidden> on 2021-10-17

merged with trunk

1158. By Kristian Morsing Pedersen <email address hidden> on 2021-10-17

Changed unit from px to pt

Unmerged revisions

=== modified file 'src/pipe/gui/TikZExporter.java'
--- src/pipe/gui/TikZExporter.java	2020-08-04 08:19:44 +0000
+++ src/pipe/gui/TikZExporter.java	2021-10-14 20:24:42 +0000
@@ -27,11 +27,6 @@
 	private final DataLayer net;
 	private final String fullpath;
 	private final TikZOutputOption option;
-	private final double scale = 1.0 / 55.0;
-        
-        private double RoundCoordinate(double position) {
-            return Math.round(position * scale * 10)/10.0d;
-        }
 
 	public TikZExporter(DataLayer net, String fullpath, TikZOutputOption option) {
 		this.net = net;
@@ -75,37 +70,44 @@
 		} catch (IOException e) {
 
 		} finally {
-			if (out != null)
-				out.close();
-			if (outFile != null)
-				try {
-					outFile.close();
-				} catch (IOException e2) {
+			if (out != null) {
+                out.close();
+            }
+			if (outFile != null) {
+                try {
+                    outFile.close();
+                } catch (IOException e2) {
 
-				}
+                }
+            }
 		}
 	}
 
 	private StringBuffer exportArcs(Arc[] arcs) {
 		StringBuffer out = new StringBuffer();
+
 		for (Arc arc : arcs) {
 			String arcPoints = "";
+
 			for (int i = 1; i < arc.getArcPath().getEndIndex(); i++) {
-				ArcPathPoint point = arc.getArcPath().getArcPathPoint(i);
-				arcPoints += "to[bend right=0] (" + RoundCoordinate(point.getX()) + "," + RoundCoordinate(point.getY() * (-1)) + ") ";
-			}
-
-			String arrowType = "";
-			if (arc instanceof TimedInhibitorArcComponent) {
-				arrowType = "inhibArc";
-			} else if (arc instanceof TimedTransportArcComponent) {
-				arrowType = "transportArc";
-			} else if (arc instanceof TimedInputArcComponent) {
-				arrowType = "arc";
-			} else {
-				arrowType = "arc";
-			}
-
+                ArcPathPoint currentPoint = arc.getArcPath().getArcPathPoint(i);
+
+                if(currentPoint.getPointType() == ArcPathPoint.STRAIGHT) {
+                    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));
+                    double xCtrl2 = Math.round(currentPoint.getControl2().getX());
+                    double yCtrl2 = Math.round(currentPoint.getControl2().getY() * (-1));
+
+                    arcPoints += " .. controls(" + xCtrl1 + "," + yCtrl1 + ")";
+                    arcPoints += " and ";
+                    arcPoints += "(" + xCtrl2 + "," + yCtrl2 + ") .. ";
+                    arcPoints += "(" + currentPoint.getX() + "," + currentPoint.getY() * (-1) + ") ";
+                }
+			}
+
+			String arrowType = getArcArrowType(arc);
 			String arcLabel = getArcLabels(arc);
 
 			out.append("\\draw[");
@@ -115,7 +117,6 @@
 			out.append(") ");
 			out.append(arcPoints);
 			out.append("to[bend right=0]");
-			//out.append(arcLabel);
 			out.append(" (");
 			out.append(arc.getTarget().getId());
 			out.append(") {};\n");
@@ -126,9 +127,23 @@
 		return out;
 	}
 
+    private String getArcArrowType(Arc arc) {
+        String arrowType = "";
+        if (arc instanceof TimedInhibitorArcComponent) {
+            arrowType = "inhibArc";
+        } else if (arc instanceof TimedTransportArcComponent) {
+            arrowType = "transportArc";
+        } else if (arc instanceof TimedInputArcComponent) {
+            arrowType = "arc";
+        } else {
+            arrowType = "arc";
+        }
+        return arrowType;
+    }
+
 	protected String getArcLabels(Arc arc) {
 		String arcLabel = "";
-		String arcLabelPositionString = "\\draw (" + RoundCoordinate(arc.getNameLabel().getXPosition())+ "," + (RoundCoordinate(arc.getNameLabel().getYPosition())*(-1)) + ") node {";
+		String arcLabelPositionString = "\\draw (" + (arc.getNameLabel().getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node {";
 
 		if (arc instanceof TimedInputArcComponent) {
             if (!(arc.getSource() instanceof TimedTransitionComponent)) {
@@ -136,10 +151,16 @@
                 if (arc.getWeight().value() > 1) {
                         arcLabel += "$" + arc.getWeight().value() + "\\times$\\ ";
                 }
-				arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$";
-				if (arc instanceof TimedTransportArcComponent)
-					arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr();
-				arcLabel += "};\n";
+
+                if(CreateGui.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) {
@@ -147,16 +168,17 @@
                 }
 				arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr() + "};\n";
 			}
+
 		} else {
             if (arc.getWeight().value() > 1) {
-                    arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n";
+                arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n";
             }
     	}
 		return arcLabel;
 	}
 
 	private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) {
-        if (!CreateGui.getApp().showZeroToInfinityIntervals() &&  arc.getGuardAsString().equals("[0,inf)")){
+        if (!CreateGui.getApp().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){
 			return "";
 		} else {
 			return arc.getGuardAsString();
@@ -168,14 +190,15 @@
 		for (Transition trans : transitions) {
 			String angle = "";
 			if (trans.getAngle() != 0)
-				angle = ",rotate=" + (trans.getAngle() + 90);
+				angle = ",rotate=-" + (trans.getAngle());
+
 
 			out.append("\\node[transition");
 			out.append(angle);		
 			out.append("] at (");
-			out.append(RoundCoordinate(trans.getPositionX()));
+			out.append((trans.getPositionX()));
 			out.append(',');
-			out.append(RoundCoordinate(trans.getPositionY() * (-1)));
+			out.append((trans.getPositionY() * (-1)));
 			out.append(") (");
 			out.append(trans.getId());
 			out.append(") {};\n");
@@ -203,9 +226,13 @@
                 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(RoundCoordinate(trans.getNameLabel().getXPosition()) + "," + (RoundCoordinate(trans.getNameLabel().getYPosition()) * -1) + ")");
+				out.append(trans.getNameLabel().getX() + xOffset + "," + (trans.getNameLabel().getY() * -1) + ")");
 				out.append(" node ");
 				out.append(" {");
 				out.append(exportMathName(trans.getName()));
@@ -217,19 +244,21 @@
 
 	private StringBuffer exportPlacesWithTokens(Place[] places) {
 		StringBuffer out = new StringBuffer();
+
 		for (Place place : places) {
 			String invariant = getPlaceInvariantString(place);
 			String tokensInPlace = getTokenListStringFor(place);
 
 			out.append("\\node[place");
-			out.append(tokensInPlace);
 			out.append("] at (");
-			out.append(RoundCoordinate(place.getPositionX()));
+			out.append(place.getPositionX());
 			out.append(',');
-			out.append(RoundCoordinate(place.getPositionY() * (-1)));
+			out.append(place.getPositionY() * (-1));
 			out.append(") (");
 			out.append(place.getId());
 			out.append(") {};\n");
+
+            exportPlaceTokens(place, out, ((TimedPlaceComponent) place).underlyingPlace().tokens().size());
 			
 			if(((TimedPlaceComponent)place).underlyingPlace().isShared()){
 				out.append("\\node[sharedplace] at (");
@@ -237,9 +266,14 @@
 				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(RoundCoordinate(place.getNameLabel().getXPosition()) + "," + (RoundCoordinate(place.getNameLabel().getYPosition()) * -1) + ")");
+				out.append((place.getNameLabel().getX() + xOffset)  + "," + ((place.getNameLabel().getY() * -1) + yOffset) +")");
 				out.append(" node[align=left] ");
 				out.append("{");
 				if(place.getAttributesVisible())
@@ -252,16 +286,159 @@
 					out.append("};\n");
 				}
 					
-			}	
+			}
 		}
 
 		return out;
 	}
 
+	private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) {
+        // Dot radius
+        final double tRadius = 1;
+
+        // Token dot position offsets
+        final double tLeftX = 7;
+        final double tRightX = 7;
+        final double tTopY = 7;
+        final double tBotY = 7;
+
+        boolean isTimed = CreateGui.getApp().getCurrentTab().getLens().isTimed();
+
+        double placeXpos = (place.getPositionX());
+        double placeYpos = (place.getPositionY() * (-1));
+        double xPos, yPos;
+
+        if(isTimed && numOfTokens > 0) {
+            switch (numOfTokens) {
+                case 2:
+                    out.append("\\node at ("); // Top
+                    out.append(placeXpos);
+                    out.append(",");
+                    out.append(placeYpos + 4);
+                    out.append(")");
+                    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");
+                    return;
+                case 1:
+                    out.append("\\node at ("); // Top
+                    out.append(placeXpos);
+                    out.append(",");
+                    out.append(placeYpos);
+                    out.append(")");
+                    out.append("{0,0};\n");
+                    return;
+                default:
+                    out.append("\\node at (");
+                    out.append(placeXpos);
+                    out.append(",");
+                    out.append(placeYpos);
+                    out.append(")");
+                    out.append("{$\\mathrm{");
+                    out.append("\\#" + numOfTokens + "}$};\n");
+                    return;
+            }
+        } else if(numOfTokens > 5 && !isTimed ) {
+            out.append("\\node at (");
+            out.append(placeXpos);
+            out.append(",");
+            out.append(placeYpos);
+            out.append(")");
+            out.append("{$\\mathrm{");
+            out.append("\\#" + numOfTokens + "}$};\n");
+            return;
+        }
+
+        switch (numOfTokens) {
+            case 5: // middle
+                out.append("\\node at (");
+                out.append(placeXpos);
+                out.append(",");
+                out.append(placeYpos);
+                out.append(")");
+                out.append("[circle,fill,inner sep=");
+                out.append(tRadius);
+                out.append("pt]{};\n");
+                /* falls through */
+            case 4: // top left
+                out.append("\\node at (");
+                out.append(placeXpos - tLeftX);
+                out.append(",");
+                out.append(placeYpos + tTopY);
+                out.append(")");
+                out.append("[circle,fill,inner sep=");
+                out.append(tRadius);
+                out.append("pt]{};\n");
+                /* falls through */
+            case 3:
+                if(numOfTokens == 5 || numOfTokens == 4) { // top right
+                    xPos = placeXpos + tRightX;
+                    yPos = placeYpos + tTopY;
+                } else { // top left
+                    xPos = placeXpos - tLeftX;
+                    yPos = placeYpos + tTopY;
+                }
+                out.append("\\node at (");
+                out.append(xPos);
+                out.append(",");
+                out.append(yPos);
+                out.append(")");
+                out.append("[circle,fill,inner sep=");
+                out.append(tRadius);
+                out.append("pt]{};\n");
+                /* falls through */
+            case 2:
+                if(numOfTokens == 5 || numOfTokens == 4) { // bottom left
+                    xPos = placeXpos - tLeftX;
+                    yPos = placeYpos - tBotY;
+                } else if (numOfTokens == 3){ // middle
+                    xPos = placeXpos;
+                    yPos = placeYpos;
+                } else { // left middle
+                    xPos = placeXpos - tLeftX;
+                    yPos = placeYpos;
+                }
+                out.append("\\node at (");
+                out.append(xPos);
+                out.append(",");
+                out.append(yPos);
+                out.append(")");
+                out.append("[circle,fill,inner sep=");
+                out.append(tRadius);
+                out.append("pt]{};\n");
+                /* falls through */
+            case 1:
+                if(numOfTokens == 5 || numOfTokens == 4 || numOfTokens == 3) { // bottom right
+                    xPos = placeXpos + tRightX;
+                    yPos = placeYpos - tBotY;
+                } else if (numOfTokens == 2){ // right middle
+                    xPos = placeXpos + tRightX;
+                    yPos = placeYpos;
+                } else { // middle
+                    xPos = placeXpos;
+                    yPos = placeYpos;
+                }
+                out.append("\\node at (");
+                out.append(xPos);
+                out.append(",");
+                out.append(yPos);
+                out.append(")");
+                out.append("[circle,fill,inner sep=");
+                out.append(tRadius);
+                out.append("pt]{};\n");
+            default:
+                break;
+        }
+    }
+
 	protected String getTokenListStringFor(Place place) {
-		
 		List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens();
-		
+
 		String tokensInPlace = "";
 		if (tokens.size() > 0) {
             if (tokens.size() == 1) {
@@ -301,7 +478,7 @@
 	private StringBuffer exportTikZstyle() {
 		StringBuffer out = new StringBuffer();
 
-		out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=1, yscale=1]\n");
+		out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33px, y=1.33px]\n");
                 out.append("%% the figure can be scaled by changing xscale and yscale\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");