Merge lp:~tapaal-contributor/tapaal/cpn-gui-TikZ-support into lp:~tapaal-contributor/tapaal/cpn-gui-dev
- cpn-gui-TikZ-support
- Merge into cpn-gui-dev
Status: | Superseded |
---|---|
Proposed branch: | lp:~tapaal-contributor/tapaal/cpn-gui-TikZ-support |
Merge into: | lp:~tapaal-contributor/tapaal/cpn-gui-dev |
Diff against target: |
411 lines (+204/-98) 1 file modified
src/net/tapaal/export/TikZExporter.java (+204/-98) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/cpn-gui-TikZ-support |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Pending | ||
Review via email: mp+415332@code.launchpad.net |
This proposal has been superseded by a proposal from 2022-02-09.
Commit message
Added TikZ support for colored nets.
Added a framed box to the Tikz output for global variables/
Description of the change
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.
- 1572. By Kristian Morsing Pedersen <email address hidden>
-
Removed subscripting from place- and transition names, and changed \mathrm to \mathit
- 1573. By Kristian Morsing Pedersen <email address hidden>
-
Added new adjustment options for labels on arcs, places and transitions
- 1574. By Kristian Morsing Pedersen <email address hidden>
-
Merged with cpn-gui-dev
- 1575. By Kristian Morsing Pedersen <email address hidden>
-
Labels with multiple lines on arcs now displays correctly
- 1576. By Kristian Morsing Pedersen <email address hidden>
-
Changed default pos of arc labels to 0.5
- 1577. By Kristian Morsing Pedersen <email address hidden>
-
Resolved merge conflicts
- 1578. By Kristian Morsing Pedersen <email address hidden>
-
Removed redundant \\ and changed 0,0 -> 0.0 for age of tokens in initial markings
- 1579. By Kristian Morsing Pedersen <email address hidden>
-
Changed x -> \times in inhibitor arcs
Unmerged revisions
Preview Diff
1 | === modified file 'src/net/tapaal/export/TikZExporter.java' |
2 | --- src/net/tapaal/export/TikZExporter.java 2022-01-07 17:05:54 +0000 |
3 | +++ src/net/tapaal/export/TikZExporter.java 2022-02-09 20:32:33 +0000 |
4 | @@ -3,22 +3,27 @@ |
5 | import java.io.FileWriter; |
6 | import java.io.IOException; |
7 | import java.io.PrintWriter; |
8 | -import java.util.List; |
9 | +import java.util.*; |
10 | +import java.util.stream.Collectors; |
11 | |
12 | +import dk.aau.cs.model.CPN.Color; |
13 | +import dk.aau.cs.model.CPN.ColorType; |
14 | +import dk.aau.cs.model.CPN.Variable; |
15 | +import dk.aau.cs.model.tapn.Constant; |
16 | import dk.aau.cs.model.tapn.TimedToken; |
17 | |
18 | +import net.tapaal.gui.petrinet.Context; |
19 | import pipe.gui.petrinet.dataLayer.DataLayer; |
20 | import pipe.gui.TAPAALGUI; |
21 | -import pipe.gui.petrinet.graphicElements.Arc; |
22 | -import pipe.gui.petrinet.graphicElements.ArcPathPoint; |
23 | -import pipe.gui.petrinet.graphicElements.Place; |
24 | -import pipe.gui.petrinet.graphicElements.Transition; |
25 | +import pipe.gui.petrinet.graphicElements.*; |
26 | import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent; |
27 | import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent; |
28 | import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent; |
29 | import pipe.gui.petrinet.graphicElements.tapn.TimedTransitionComponent; |
30 | import pipe.gui.petrinet.graphicElements.tapn.TimedTransportArcComponent; |
31 | |
32 | +import static java.util.stream.Collectors.toList; |
33 | + |
34 | public class TikZExporter { |
35 | |
36 | public enum TikZOutputOption { |
37 | @@ -45,7 +50,7 @@ |
38 | if (option == TikZOutputOption.FULL_LATEX) { |
39 | out.println("\\documentclass[a4paper]{article}"); |
40 | out.println("\\usepackage{tikz}"); |
41 | - out.println("\\usetikzlibrary{petri,arrows}"); |
42 | + out.println("\\usetikzlibrary{petri,arrows,positioning}"); |
43 | out.println("\\usepackage{amstext}"); |
44 | out.println(); |
45 | out.println("\\begin{document}"); |
46 | @@ -62,6 +67,8 @@ |
47 | out.print(exportTransitions(net.getTransitions())); |
48 | out.print(exportArcs(net.getArcs())); |
49 | |
50 | + out.println(exportGlobalVariables()); |
51 | + |
52 | out.println("\\end{tikzpicture}"); |
53 | if (option == TikZOutputOption.FULL_LATEX) { |
54 | out.println("\\end{document}"); |
55 | @@ -144,48 +151,22 @@ |
56 | |
57 | protected String getArcLabels(Arc arc) { |
58 | String arcLabel = ""; |
59 | - String arcLabelPositionString = "\\draw (" + (arc.getNameLabel().getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node {"; |
60 | - |
61 | - if (arc instanceof TimedInputArcComponent) { |
62 | - if (!(arc.getSource() instanceof TimedTransitionComponent)) { |
63 | - arcLabel = arcLabelPositionString; |
64 | - if (arc.getWeight().value() > 1) { |
65 | - arcLabel += "$" + arc.getWeight().value() + "\\times$\\ "; |
66 | - } |
67 | - |
68 | - if(TAPAALGUI.getApp().getCurrentTab().getLens().isTimed()) { |
69 | - arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$"; |
70 | - if (arc instanceof TimedTransportArcComponent) |
71 | - arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr(); |
72 | - arcLabel += "};\n"; |
73 | - } else { |
74 | - arcLabel += "};\n"; |
75 | - } |
76 | - |
77 | - } else { |
78 | - arcLabel = arcLabelPositionString; |
79 | - if (arc.getWeight().value() > 1) { |
80 | - arcLabel += "$" + arc.getWeight().value() + "\\times$\\ "; |
81 | - } |
82 | - arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr() + "};\n"; |
83 | - } |
84 | - |
85 | - } else { |
86 | - if (arc.getWeight().value() > 1) { |
87 | - arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n"; |
88 | - } |
89 | - } |
90 | + String arcLabelPositionString = "\\draw (" + (arc.getArcPath().midPoint.getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node[align=left,xshift=0pt,yshift=0pt] {"; |
91 | + |
92 | + if(!arc.getNameLabel().getText().isEmpty()) { |
93 | + arcLabel += arcLabelPositionString; |
94 | + arcLabel += "\\\\" + handleNameLabel(arc.getNameLabel().getText()) + ""; |
95 | + } |
96 | + |
97 | + if(!arcLabel.isEmpty()) { |
98 | + arcLabel += "};\n"; |
99 | + } else { |
100 | + arcLabel += "{};\n"; |
101 | + } |
102 | + |
103 | return arcLabel; |
104 | } |
105 | |
106 | - private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) { |
107 | - if (!TAPAALGUI.getApp().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){ |
108 | - return ""; |
109 | - } else { |
110 | - return arc.getGuardAsString(); |
111 | - } |
112 | - } |
113 | - |
114 | private StringBuffer exportTransitions(Transition[] transitions) { |
115 | StringBuffer out = new StringBuffer(); |
116 | for (Transition trans : transitions) { |
117 | @@ -234,9 +215,10 @@ |
118 | out.append("%% label for transition " + trans.getName() + "\n"); |
119 | out.append("\\draw ("); |
120 | out.append(trans.getNameLabel().getX() + xOffset + "," + (trans.getNameLabel().getY() * -1) + ")"); |
121 | - out.append(" node "); |
122 | + out.append(" node[align=left,xshift=0pt,yshift=0pt]"); |
123 | out.append(" {"); |
124 | - out.append(exportMathName(trans.getName())); |
125 | + out.append("$\\mathit{" + (trans.getName().replace("_","\\_")) + "}$"); |
126 | + out.append(handleNameLabel(trans.getNameLabel().getText())); |
127 | out.append("};\n"); |
128 | } |
129 | } |
130 | @@ -247,7 +229,7 @@ |
131 | StringBuffer out = new StringBuffer(); |
132 | |
133 | for (Place place : places) { |
134 | - String invariant = getPlaceInvariantString(place); |
135 | + String invariant = "$" + getPlaceInvariantString(place) + "$"; |
136 | String tokensInPlace = getTokenListStringFor(place); |
137 | |
138 | out.append("\\node[place"); |
139 | @@ -269,30 +251,58 @@ |
140 | if (place.getAttributesVisible() || !invariant.equals("")){ |
141 | boolean isLabelAbovePlace = place.getY() > place.getNameLabel().getY(); |
142 | boolean isLabelBehindPlace = place.getX() < place.getNameLabel().getX(); |
143 | - double xOffset = place.getName().length() > 6 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0; |
144 | - double yOffset = isLabelAbovePlace ? (place.getNameLabel().getHeight() / 2) : 0; |
145 | + int longestString = 0; |
146 | + List<String> listStringNameLabel = place.getNameLabel().getText().lines().collect(toList()); |
147 | + for(int i = 0; i < listStringNameLabel.size(); i++) { |
148 | + if(listStringNameLabel.get(i).length() > longestString) { |
149 | + longestString = listStringNameLabel.get(i).length(); |
150 | + } |
151 | + } |
152 | + double xOffset = longestString > 8 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0; |
153 | + double yOffset = place.getNameLabel().getText().lines().count() * 5; |
154 | + |
155 | + String nameLabel = place.getNameLabel().getText(); |
156 | |
157 | out.append("%% label for place " + place.getName() + "\n"); |
158 | out.append("\\draw ("); |
159 | - out.append((place.getNameLabel().getX() + xOffset) + "," + ((place.getNameLabel().getY() * -1) + yOffset) +")"); |
160 | - out.append(" node[align=left] "); |
161 | + out.append((place.getNameLabel().getX() + xOffset) + "," + ((place.getNameLabel().getY() + yOffset) * -1) +")"); |
162 | + out.append(" node[align=left,xshift=0pt,yshift=0pt] "); |
163 | out.append("{"); |
164 | - if(place.getAttributesVisible()) |
165 | - out.append(exportMathName(place.getName())); |
166 | - if(!invariant.equals("")) { |
167 | - if((place.getAttributesVisible())) |
168 | - out.append("\\\\"); |
169 | - out.append(invariant); |
170 | - }else { |
171 | - out.append("};\n"); |
172 | - } |
173 | - |
174 | + if(place.getAttributesVisible()) { |
175 | + out.append("$\\mathit{" + (place.getName().replace("_","\\_")) + "}$"); |
176 | + if (!place.getNameLabel().getText().isEmpty()) { |
177 | + out.append(handleNameLabel(nameLabel)); |
178 | + } |
179 | + } |
180 | + out.append("};\n"); |
181 | } |
182 | } |
183 | - |
184 | return out; |
185 | } |
186 | |
187 | + private String handleNameLabel(String nameLabel) { |
188 | + String nameLabelsString = ""; |
189 | + String[] labelsInName = nameLabel.split("\n"); |
190 | + for(int i = 0; i < labelsInName.length; i++) { |
191 | + |
192 | + if(labelsInName[i].contains("[")) { |
193 | + nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i])); |
194 | + nameLabelsString += "\\\\"; |
195 | + } |
196 | + else if(!labelsInName[i].isEmpty()){ |
197 | + nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i])); |
198 | + nameLabelsString += "\\\\"; |
199 | + } else { |
200 | + nameLabelsString += "\\\\"; |
201 | + } |
202 | + } |
203 | + return nameLabelsString; |
204 | + } |
205 | + |
206 | + private String escapeSpacesInAndOrNot(String str) { |
207 | + return str.replace(" and ", "\\ and\\ ").replace(" or", "\\ or\\ ").replace(" not", "\\ not\\ "); |
208 | + } |
209 | + |
210 | private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) { |
211 | // Dot radius |
212 | final double tRadius = 1; |
213 | @@ -437,6 +447,116 @@ |
214 | } |
215 | } |
216 | |
217 | + private StringBuffer exportGlobalVariables() { |
218 | + StringBuffer out = new StringBuffer(); |
219 | + |
220 | + Context context = new Context(TAPAALGUI.getCurrentTab()); |
221 | + List<ColorType> listColorTypes = context.network().colorTypes(); |
222 | + List<Constant> constantsList = new ArrayList<>(context.network().constants()); |
223 | + List<Variable> variableList = context.network().variables(); |
224 | + |
225 | + if(!context.network().isColored() || (listColorTypes.isEmpty() && constantsList.isEmpty() && variableList.isEmpty())) { |
226 | + out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {"); |
227 | + exportConstants(constantsList, out); |
228 | + out.append("};"); |
229 | + return out; |
230 | + } |
231 | + |
232 | + out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {"); |
233 | + |
234 | + exportColorTypes(listColorTypes, out); |
235 | + |
236 | + if(listColorTypes.size() > 0 && (variableList.size() > 0 || constantsList.size() > 0)) { |
237 | + out.append("\\\\"); |
238 | + } |
239 | + |
240 | + exportVariables(variableList, out); |
241 | + |
242 | + if(variableList.size() > 0 && !constantsList.isEmpty()) { |
243 | + out.append("\\\\"); |
244 | + } |
245 | + |
246 | + exportConstants(constantsList, out); |
247 | + |
248 | + out.append("};"); |
249 | + |
250 | + return out; |
251 | + } |
252 | + |
253 | + private void exportColorTypes(List<ColorType> listColorTypes, StringBuffer out) { |
254 | + String stringColorList = ""; |
255 | + for(int i = 0; i < listColorTypes.size(); i++) { |
256 | + if(i == 0) { |
257 | + out.append("Color Types:\\\\"); |
258 | + } |
259 | + out.append("$\\mathit{" + listColorTypes.get(i).getName() + "}$ \\textbf{is} "); |
260 | + |
261 | + if(listColorTypes.get(i).isProductColorType()) { |
262 | + out.append("$\\mathit{<"); |
263 | + for(int x = 0; x < listColorTypes.get(i).getProductColorTypes().size(); x++) { |
264 | + stringColorList += listColorTypes.get(i).getProductColorTypes().get(x).getName().replace("_", "\\_"); |
265 | + |
266 | + if(x != listColorTypes.get(i).getProductColorTypes().size() - 1){ |
267 | + stringColorList += ", "; |
268 | + } |
269 | + } |
270 | + out.append(stringColorList + ">}$\\\\"); |
271 | + stringColorList = ""; |
272 | + |
273 | + } else if(listColorTypes.get(i).isIntegerRange()) { |
274 | + out.append("$\\mathit{"); |
275 | + if(listColorTypes.get(i).size() > 1) { |
276 | + int listSize = listColorTypes.get(i).size(); |
277 | + out.append("[" + listColorTypes.get(i).getColors().get(0).getColorName().replace("_","\\_") + ".." + listColorTypes.get(i).getColors().get(listSize - 1).getColorName().replace("_","\\_") + "]"); |
278 | + } else { |
279 | + out.append("[" + listColorTypes.get(i).getFirstColor().getColorName().replace("_","\\_") + "]"); |
280 | + } |
281 | + out.append("}$\\\\"); |
282 | + |
283 | + } else { |
284 | + out.append("$\\mathit{["); |
285 | + for(int x = 0; x < listColorTypes.get(i).getColors().size(); x++) { |
286 | + stringColorList += listColorTypes.get(i).getColors().get(x).getName().replace("_","\\_"); |
287 | + |
288 | + if(x != listColorTypes.get(i).getColors().size() - 1){ |
289 | + stringColorList += ", "; |
290 | + } |
291 | + } |
292 | + out.append(stringColorList + "]}$\\\\"); |
293 | + stringColorList = ""; |
294 | + } |
295 | + } |
296 | + } |
297 | + |
298 | + private void exportVariables(List<Variable> variableList, StringBuffer out) { |
299 | + String result = ""; |
300 | + for(int i = 0; i < variableList.size(); i++) { |
301 | + if (i == 0) { |
302 | + result += "Variables:\\\\ "; |
303 | + } |
304 | + result += "$\\mathit{" + variableList.get(i).getName().replace("_","\\_") + " \\textbf{ in } " + variableList.get(i).getColorType().getName().replace("_","\\_") + "}$"; |
305 | + if(i != variableList.size() - 1) { |
306 | + result += "\\\\"; |
307 | + } |
308 | + } |
309 | + out.append(result); |
310 | + } |
311 | + |
312 | + private void exportConstants(List<Constant> constantsList, StringBuffer out) { |
313 | + String result = ""; |
314 | + |
315 | + for(int i = 0; i < constantsList.size(); i++) { |
316 | + if(i == 0) { |
317 | + result += "Constants:\\\\"; |
318 | + } |
319 | + result += "$\\mathit{" + constantsList.get(i).toString().replace("_","\\_") + "}$"; |
320 | + if(i != constantsList.size() - 1) { |
321 | + result += "\\\\"; |
322 | + } |
323 | + } |
324 | + out.append(result); |
325 | + } |
326 | + |
327 | protected String getTokenListStringFor(Place place) { |
328 | List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens(); |
329 | |
330 | @@ -455,7 +575,7 @@ |
331 | String invariant = ""; |
332 | |
333 | if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf")) |
334 | - invariant = "$\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$};\n"; |
335 | + invariant = replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "};\n"; |
336 | return invariant; |
337 | } |
338 | |
339 | @@ -480,12 +600,13 @@ |
340 | StringBuffer out = new StringBuffer(); |
341 | |
342 | out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n"); |
343 | - out.append("%% the figure can be scaled by changing xscale and yscale\n"); |
344 | + out.append("%% the figure can be scaled by changing xscale and yscale or the size of the x- and y-coordinates\n"); |
345 | out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n"); |
346 | out.append("%% can be adjusted so that they do not cover arcs\n"); |
347 | out.append("%% similarly the curving of arcs can be done by adjusting bend left/right=XX\n"); |
348 | - out.append("%% labels may be slightly skewed compared to the tapaal drawing due to rounding.\n"); |
349 | - out.append("%% This can be adjusted by tuning the coordinates of the label\n"); |
350 | + out.append("%% labels may be slightly skewed compared to the Tapaal drawing due to rounding.\n"); |
351 | + out.append("%% This can be adjusted by tuning the coordinates of the label or adjusting the x- and y-shift for the label\n"); |
352 | + 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"); |
353 | out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n"); |
354 | |
355 | out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n"); |
356 | @@ -496,39 +617,24 @@ |
357 | out.append("\\tikzstyle{every token}=[fill=white,text=black]\n"); |
358 | out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n"); |
359 | out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n"); |
360 | - out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]"); |
361 | - out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]"); |
362 | + out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]\n"); |
363 | + out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]\n"); |
364 | + out.append("\\tikzstyle{globalBox} = [draw,thick,align=left]"); |
365 | return out; |
366 | } |
367 | |
368 | protected String replaceWithMathLatex(String text) { |
369 | - return text.replace("inf", "\\infty").replace("<=", "\\leq ").replace("*", "\\cdot "); |
370 | - } |
371 | - |
372 | - private String exportMathName(String name) { |
373 | - StringBuilder out = new StringBuilder("$\\mathrm{"); |
374 | - int subscripts = 0; |
375 | - for (int i = 0; i < name.length() - 1; i++) { |
376 | - char c = name.charAt(i); |
377 | - if (c == '_') { |
378 | - out.append("_{"); |
379 | - subscripts++; |
380 | - } else { |
381 | - out.append(c); |
382 | - } |
383 | - } |
384 | - |
385 | - char last = name.charAt(name.length() - 1); |
386 | - if (last == '_') { |
387 | - out.append("\\_"); |
388 | - } else |
389 | - out.append(last); |
390 | - |
391 | - for (int i = 0; i < subscripts; i++) { |
392 | - out.append('}'); |
393 | - } |
394 | - out.append("}$"); |
395 | - return out.toString(); |
396 | - } |
397 | - |
398 | + String[] stringList = text.split(" "); |
399 | + String result = ""; |
400 | + |
401 | + for(int i = 0; i < stringList.length; i++) { |
402 | + result += "$\\mathit{" + replaceSpecialSymbols(stringList[i]) + "}$ "; |
403 | + } |
404 | + return result; |
405 | + } |
406 | + |
407 | + protected String replaceSpecialSymbols(String text) { |
408 | + return text.replace("inf", "\\infty").replace("<=", "\\leq").replace("*", "\\cdot") |
409 | + .replace("\u2192", "\\rightarrow").replace("\u221E", "\\infty"); |
410 | + } |
411 | } |