TAPAAL

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

  1. fix-tikz-export-1945642
  2. Merge into trunk
Proposed by Kristian Morsing Pedersen
Status: Superseded
Proposed branch: lp:~tapaal-contributor/tapaal/fix-tikz-export-1945642
Merge into: lp:tapaal
Diff against target: 403 lines (+224/-47)
1 file modified
src/pipe/gui/TikZExporter.java (+224/-47)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/fix-tikz-export-1945642
Reviewer Review Type Date Requested Status
Jiri Srba Pending
Review via email: mp+410240@code.launchpad.net

This proposal supersedes a proposal from 2021-10-10.

This proposal has been superseded by a proposal from 2021-10-14.

Commit message

Improved quality of Tikz export and various fixes

Description of the change

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.

To post a comment you must log in.
lp:~tapaal-contributor/tapaal/fix-tikz-export-1945642 updated
1156. By Kristian Morsing Pedersen <email address hidden>

Now correctly show transition rotations for 45 degree angles

1157. By <email address hidden>

merged with trunk

1158. By Kristian Morsing Pedersen <email address hidden>

Changed unit from px to pt

Unmerged revisions

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/pipe/gui/TikZExporter.java'
2--- src/pipe/gui/TikZExporter.java 2020-08-04 08:19:44 +0000
3+++ src/pipe/gui/TikZExporter.java 2021-10-14 20:24:42 +0000
4@@ -27,11 +27,6 @@
5 private final DataLayer net;
6 private final String fullpath;
7 private final TikZOutputOption option;
8- private final double scale = 1.0 / 55.0;
9-
10- private double RoundCoordinate(double position) {
11- return Math.round(position * scale * 10)/10.0d;
12- }
13
14 public TikZExporter(DataLayer net, String fullpath, TikZOutputOption option) {
15 this.net = net;
16@@ -75,37 +70,44 @@
17 } catch (IOException e) {
18
19 } finally {
20- if (out != null)
21- out.close();
22- if (outFile != null)
23- try {
24- outFile.close();
25- } catch (IOException e2) {
26+ if (out != null) {
27+ out.close();
28+ }
29+ if (outFile != null) {
30+ try {
31+ outFile.close();
32+ } catch (IOException e2) {
33
34- }
35+ }
36+ }
37 }
38 }
39
40 private StringBuffer exportArcs(Arc[] arcs) {
41 StringBuffer out = new StringBuffer();
42+
43 for (Arc arc : arcs) {
44 String arcPoints = "";
45+
46 for (int i = 1; i < arc.getArcPath().getEndIndex(); i++) {
47- ArcPathPoint point = arc.getArcPath().getArcPathPoint(i);
48- arcPoints += "to[bend right=0] (" + RoundCoordinate(point.getX()) + "," + RoundCoordinate(point.getY() * (-1)) + ") ";
49- }
50-
51- String arrowType = "";
52- if (arc instanceof TimedInhibitorArcComponent) {
53- arrowType = "inhibArc";
54- } else if (arc instanceof TimedTransportArcComponent) {
55- arrowType = "transportArc";
56- } else if (arc instanceof TimedInputArcComponent) {
57- arrowType = "arc";
58- } else {
59- arrowType = "arc";
60- }
61-
62+ ArcPathPoint currentPoint = arc.getArcPath().getArcPathPoint(i);
63+
64+ if(currentPoint.getPointType() == ArcPathPoint.STRAIGHT) {
65+ arcPoints += "to[bend right=0] (" + (currentPoint.getX()) + "," + (currentPoint.getY() * (-1)) + ") ";
66+ } else if (currentPoint.getPointType() == ArcPathPoint.CURVED) {
67+ double xCtrl1 = Math.round(currentPoint.getControl1().getX());
68+ double yCtrl1 = Math.round(currentPoint.getControl1().getY() * (-1));
69+ double xCtrl2 = Math.round(currentPoint.getControl2().getX());
70+ double yCtrl2 = Math.round(currentPoint.getControl2().getY() * (-1));
71+
72+ arcPoints += " .. controls(" + xCtrl1 + "," + yCtrl1 + ")";
73+ arcPoints += " and ";
74+ arcPoints += "(" + xCtrl2 + "," + yCtrl2 + ") .. ";
75+ arcPoints += "(" + currentPoint.getX() + "," + currentPoint.getY() * (-1) + ") ";
76+ }
77+ }
78+
79+ String arrowType = getArcArrowType(arc);
80 String arcLabel = getArcLabels(arc);
81
82 out.append("\\draw[");
83@@ -115,7 +117,6 @@
84 out.append(") ");
85 out.append(arcPoints);
86 out.append("to[bend right=0]");
87- //out.append(arcLabel);
88 out.append(" (");
89 out.append(arc.getTarget().getId());
90 out.append(") {};\n");
91@@ -126,9 +127,23 @@
92 return out;
93 }
94
95+ private String getArcArrowType(Arc arc) {
96+ String arrowType = "";
97+ if (arc instanceof TimedInhibitorArcComponent) {
98+ arrowType = "inhibArc";
99+ } else if (arc instanceof TimedTransportArcComponent) {
100+ arrowType = "transportArc";
101+ } else if (arc instanceof TimedInputArcComponent) {
102+ arrowType = "arc";
103+ } else {
104+ arrowType = "arc";
105+ }
106+ return arrowType;
107+ }
108+
109 protected String getArcLabels(Arc arc) {
110 String arcLabel = "";
111- String arcLabelPositionString = "\\draw (" + RoundCoordinate(arc.getNameLabel().getXPosition())+ "," + (RoundCoordinate(arc.getNameLabel().getYPosition())*(-1)) + ") node {";
112+ String arcLabelPositionString = "\\draw (" + (arc.getNameLabel().getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node {";
113
114 if (arc instanceof TimedInputArcComponent) {
115 if (!(arc.getSource() instanceof TimedTransitionComponent)) {
116@@ -136,10 +151,16 @@
117 if (arc.getWeight().value() > 1) {
118 arcLabel += "$" + arc.getWeight().value() + "\\times$\\ ";
119 }
120- arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$";
121- if (arc instanceof TimedTransportArcComponent)
122- arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr();
123- arcLabel += "};\n";
124+
125+ if(CreateGui.getApp().getCurrentTab().getLens().isTimed()) {
126+ arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$";
127+ if (arc instanceof TimedTransportArcComponent)
128+ arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr();
129+ arcLabel += "};\n";
130+ } else {
131+ arcLabel += "};\n";
132+ }
133+
134 } else {
135 arcLabel = arcLabelPositionString;
136 if (arc.getWeight().value() > 1) {
137@@ -147,16 +168,17 @@
138 }
139 arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr() + "};\n";
140 }
141+
142 } else {
143 if (arc.getWeight().value() > 1) {
144- arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n";
145+ arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n";
146 }
147 }
148 return arcLabel;
149 }
150
151 private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) {
152- if (!CreateGui.getApp().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){
153+ if (!CreateGui.getApp().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){
154 return "";
155 } else {
156 return arc.getGuardAsString();
157@@ -168,14 +190,15 @@
158 for (Transition trans : transitions) {
159 String angle = "";
160 if (trans.getAngle() != 0)
161- angle = ",rotate=" + (trans.getAngle() + 90);
162+ angle = ",rotate=-" + (trans.getAngle());
163+
164
165 out.append("\\node[transition");
166 out.append(angle);
167 out.append("] at (");
168- out.append(RoundCoordinate(trans.getPositionX()));
169+ out.append((trans.getPositionX()));
170 out.append(',');
171- out.append(RoundCoordinate(trans.getPositionY() * (-1)));
172+ out.append((trans.getPositionY() * (-1)));
173 out.append(") (");
174 out.append(trans.getId());
175 out.append(") {};\n");
176@@ -203,9 +226,13 @@
177 out.append(".center) { };\n");
178 }
179 if (trans.getAttributesVisible()){
180+ boolean isLabelAboveTransition = trans.getY() > trans.getNameLabel().getY();
181+ boolean isLabelBehindTrans = trans.getX() < trans.getNameLabel().getX();
182+ double xOffset = trans.getName().length() > 5 && !isLabelAboveTransition && !isLabelBehindTrans ? trans.getLayerOffset() : 0;
183+
184 out.append("%% label for transition " + trans.getName() + "\n");
185 out.append("\\draw (");
186- out.append(RoundCoordinate(trans.getNameLabel().getXPosition()) + "," + (RoundCoordinate(trans.getNameLabel().getYPosition()) * -1) + ")");
187+ out.append(trans.getNameLabel().getX() + xOffset + "," + (trans.getNameLabel().getY() * -1) + ")");
188 out.append(" node ");
189 out.append(" {");
190 out.append(exportMathName(trans.getName()));
191@@ -217,19 +244,21 @@
192
193 private StringBuffer exportPlacesWithTokens(Place[] places) {
194 StringBuffer out = new StringBuffer();
195+
196 for (Place place : places) {
197 String invariant = getPlaceInvariantString(place);
198 String tokensInPlace = getTokenListStringFor(place);
199
200 out.append("\\node[place");
201- out.append(tokensInPlace);
202 out.append("] at (");
203- out.append(RoundCoordinate(place.getPositionX()));
204+ out.append(place.getPositionX());
205 out.append(',');
206- out.append(RoundCoordinate(place.getPositionY() * (-1)));
207+ out.append(place.getPositionY() * (-1));
208 out.append(") (");
209 out.append(place.getId());
210 out.append(") {};\n");
211+
212+ exportPlaceTokens(place, out, ((TimedPlaceComponent) place).underlyingPlace().tokens().size());
213
214 if(((TimedPlaceComponent)place).underlyingPlace().isShared()){
215 out.append("\\node[sharedplace] at (");
216@@ -237,9 +266,14 @@
217 out.append(".center) { };\n");
218 }
219 if (place.getAttributesVisible() || !invariant.equals("")){
220+ boolean isLabelAbovePlace = place.getY() > place.getNameLabel().getY();
221+ boolean isLabelBehindPlace = place.getX() < place.getNameLabel().getX();
222+ double xOffset = place.getName().length() > 6 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0;
223+ double yOffset = isLabelAbovePlace ? (place.getNameLabel().getHeight() / 2) : 0;
224+
225 out.append("%% label for place " + place.getName() + "\n");
226 out.append("\\draw (");
227- out.append(RoundCoordinate(place.getNameLabel().getXPosition()) + "," + (RoundCoordinate(place.getNameLabel().getYPosition()) * -1) + ")");
228+ out.append((place.getNameLabel().getX() + xOffset) + "," + ((place.getNameLabel().getY() * -1) + yOffset) +")");
229 out.append(" node[align=left] ");
230 out.append("{");
231 if(place.getAttributesVisible())
232@@ -252,16 +286,159 @@
233 out.append("};\n");
234 }
235
236- }
237+ }
238 }
239
240 return out;
241 }
242
243+ private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) {
244+ // Dot radius
245+ final double tRadius = 1;
246+
247+ // Token dot position offsets
248+ final double tLeftX = 7;
249+ final double tRightX = 7;
250+ final double tTopY = 7;
251+ final double tBotY = 7;
252+
253+ boolean isTimed = CreateGui.getApp().getCurrentTab().getLens().isTimed();
254+
255+ double placeXpos = (place.getPositionX());
256+ double placeYpos = (place.getPositionY() * (-1));
257+ double xPos, yPos;
258+
259+ if(isTimed && numOfTokens > 0) {
260+ switch (numOfTokens) {
261+ case 2:
262+ out.append("\\node at ("); // Top
263+ out.append(placeXpos);
264+ out.append(",");
265+ out.append(placeYpos + 4);
266+ out.append(")");
267+ out.append("{0,0};\n");
268+
269+ out.append("\\node at ("); // Bottom
270+ out.append(placeXpos);
271+ out.append(",");
272+ out.append(placeYpos - 5);
273+ out.append(")");
274+ out.append("{0,0};\n");
275+ return;
276+ case 1:
277+ out.append("\\node at ("); // Top
278+ out.append(placeXpos);
279+ out.append(",");
280+ out.append(placeYpos);
281+ out.append(")");
282+ out.append("{0,0};\n");
283+ return;
284+ default:
285+ out.append("\\node at (");
286+ out.append(placeXpos);
287+ out.append(",");
288+ out.append(placeYpos);
289+ out.append(")");
290+ out.append("{$\\mathrm{");
291+ out.append("\\#" + numOfTokens + "}$};\n");
292+ return;
293+ }
294+ } else if(numOfTokens > 5 && !isTimed ) {
295+ out.append("\\node at (");
296+ out.append(placeXpos);
297+ out.append(",");
298+ out.append(placeYpos);
299+ out.append(")");
300+ out.append("{$\\mathrm{");
301+ out.append("\\#" + numOfTokens + "}$};\n");
302+ return;
303+ }
304+
305+ switch (numOfTokens) {
306+ case 5: // middle
307+ out.append("\\node at (");
308+ out.append(placeXpos);
309+ out.append(",");
310+ out.append(placeYpos);
311+ out.append(")");
312+ out.append("[circle,fill,inner sep=");
313+ out.append(tRadius);
314+ out.append("pt]{};\n");
315+ /* falls through */
316+ case 4: // top left
317+ out.append("\\node at (");
318+ out.append(placeXpos - tLeftX);
319+ out.append(",");
320+ out.append(placeYpos + tTopY);
321+ out.append(")");
322+ out.append("[circle,fill,inner sep=");
323+ out.append(tRadius);
324+ out.append("pt]{};\n");
325+ /* falls through */
326+ case 3:
327+ if(numOfTokens == 5 || numOfTokens == 4) { // top right
328+ xPos = placeXpos + tRightX;
329+ yPos = placeYpos + tTopY;
330+ } else { // top left
331+ xPos = placeXpos - tLeftX;
332+ yPos = placeYpos + tTopY;
333+ }
334+ out.append("\\node at (");
335+ out.append(xPos);
336+ out.append(",");
337+ out.append(yPos);
338+ out.append(")");
339+ out.append("[circle,fill,inner sep=");
340+ out.append(tRadius);
341+ out.append("pt]{};\n");
342+ /* falls through */
343+ case 2:
344+ if(numOfTokens == 5 || numOfTokens == 4) { // bottom left
345+ xPos = placeXpos - tLeftX;
346+ yPos = placeYpos - tBotY;
347+ } else if (numOfTokens == 3){ // middle
348+ xPos = placeXpos;
349+ yPos = placeYpos;
350+ } else { // left middle
351+ xPos = placeXpos - tLeftX;
352+ yPos = placeYpos;
353+ }
354+ out.append("\\node at (");
355+ out.append(xPos);
356+ out.append(",");
357+ out.append(yPos);
358+ out.append(")");
359+ out.append("[circle,fill,inner sep=");
360+ out.append(tRadius);
361+ out.append("pt]{};\n");
362+ /* falls through */
363+ case 1:
364+ if(numOfTokens == 5 || numOfTokens == 4 || numOfTokens == 3) { // bottom right
365+ xPos = placeXpos + tRightX;
366+ yPos = placeYpos - tBotY;
367+ } else if (numOfTokens == 2){ // right middle
368+ xPos = placeXpos + tRightX;
369+ yPos = placeYpos;
370+ } else { // middle
371+ xPos = placeXpos;
372+ yPos = placeYpos;
373+ }
374+ out.append("\\node at (");
375+ out.append(xPos);
376+ out.append(",");
377+ out.append(yPos);
378+ out.append(")");
379+ out.append("[circle,fill,inner sep=");
380+ out.append(tRadius);
381+ out.append("pt]{};\n");
382+ default:
383+ break;
384+ }
385+ }
386+
387 protected String getTokenListStringFor(Place place) {
388-
389 List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens();
390-
391+
392 String tokensInPlace = "";
393 if (tokens.size() > 0) {
394 if (tokens.size() == 1) {
395@@ -301,7 +478,7 @@
396 private StringBuffer exportTikZstyle() {
397 StringBuffer out = new StringBuffer();
398
399- out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=1, yscale=1]\n");
400+ out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33px, y=1.33px]\n");
401 out.append("%% the figure can be scaled by changing xscale and yscale\n");
402 out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n");
403 out.append("%% can be adjusted so that they do not cover arcs\n");

Subscribers

People subscribed via source and target branches