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: |
485 lines (+200/-139) 1 file modified
src/net/tapaal/export/TikZExporter.java (+200/-139) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/cpn-gui-TikZ-support |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Needs Fixing | ||
Kenneth Yrke Jørgensen | code | Pending | |
Review via email:
|
This proposal supersedes a proposal from 2022-02-21.
This proposal has been superseded by a proposal from 2022-03-07.
Commit message
Added TikZ support for colored nets.
Added a framed box to the Tikz output for global variables/
Removed subscripiting from transition- and place names
Changed \mathrm to \mathit
Added more adjustment options for transitions, places and arcs
Merged with cpn-gui-dev
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.
Subscripting from transition- and place names have been removed, so it looks more like the GUI.
\mathrm has also been replaces with \mathit.
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Kenneth Yrke Jørgensen (yrke) : Posted in a previous version of this proposal | # |
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
Please, set the default position for arc lables to pos=0.5
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jiri Srba (srba) wrote : | # |
At the end of the labels, there is a redundant \\ that makes the spacing look ugly. E.g. in
\node[place, label={
The label should finish with just ... $\mathit{4}$ }] without the extra \\
![](/+icing/build/overlay/assets/skins/sam/images/close.gif)
Jiri Srba (srba) wrote : | # |
Also, when exporting age of tokens in the initial marking, please write 0.0 instead of 0,0
Unmerged revisions
Preview Diff
1 | === modified file 'src/net/tapaal/export/TikZExporter.java' | |||
2 | --- src/net/tapaal/export/TikZExporter.java 2022-02-21 19:46:59 +0000 | |||
3 | +++ src/net/tapaal/export/TikZExporter.java 2022-03-07 14:26:18 +0000 | |||
4 | @@ -3,16 +3,17 @@ | |||
5 | 3 | import java.io.FileWriter; | 3 | import java.io.FileWriter; |
6 | 4 | import java.io.IOException; | 4 | import java.io.IOException; |
7 | 5 | import java.io.PrintWriter; | 5 | import java.io.PrintWriter; |
9 | 6 | import java.util.List; | 6 | import java.util.*; |
10 | 7 | 7 | ||
11 | 8 | import dk.aau.cs.model.CPN.ColorType; | ||
12 | 9 | import dk.aau.cs.model.CPN.Variable; | ||
13 | 10 | import dk.aau.cs.model.tapn.Constant; | ||
14 | 8 | import dk.aau.cs.model.tapn.TimedToken; | 11 | import dk.aau.cs.model.tapn.TimedToken; |
15 | 9 | 12 | ||
16 | 13 | import net.tapaal.gui.petrinet.Context; | ||
17 | 10 | import pipe.gui.petrinet.dataLayer.DataLayer; | 14 | import pipe.gui.petrinet.dataLayer.DataLayer; |
18 | 11 | import pipe.gui.TAPAALGUI; | 15 | import pipe.gui.TAPAALGUI; |
23 | 12 | import pipe.gui.petrinet.graphicElements.Arc; | 16 | import pipe.gui.petrinet.graphicElements.*; |
20 | 13 | import pipe.gui.petrinet.graphicElements.ArcPathPoint; | ||
21 | 14 | import pipe.gui.petrinet.graphicElements.Place; | ||
22 | 15 | import pipe.gui.petrinet.graphicElements.Transition; | ||
24 | 16 | import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent; | 17 | import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent; |
25 | 17 | import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent; | 18 | import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent; |
26 | 18 | import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent; | 19 | import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent; |
27 | @@ -45,7 +46,7 @@ | |||
28 | 45 | if (option == TikZOutputOption.FULL_LATEX) { | 46 | if (option == TikZOutputOption.FULL_LATEX) { |
29 | 46 | out.println("\\documentclass[a4paper]{article}"); | 47 | out.println("\\documentclass[a4paper]{article}"); |
30 | 47 | out.println("\\usepackage{tikz}"); | 48 | out.println("\\usepackage{tikz}"); |
32 | 48 | out.println("\\usetikzlibrary{petri,arrows}"); | 49 | out.println("\\usetikzlibrary{petri,arrows,positioning}"); |
33 | 49 | out.println("\\usepackage{amstext}"); | 50 | out.println("\\usepackage{amstext}"); |
34 | 50 | out.println(); | 51 | out.println(); |
35 | 51 | out.println("\\begin{document}"); | 52 | out.println("\\begin{document}"); |
36 | @@ -62,6 +63,8 @@ | |||
37 | 62 | out.print(exportTransitions(net.getTransitions())); | 63 | out.print(exportTransitions(net.getTransitions())); |
38 | 63 | out.print(exportArcs(net.getArcs())); | 64 | out.print(exportArcs(net.getArcs())); |
39 | 64 | 65 | ||
40 | 66 | out.println(exportGlobalVariables()); | ||
41 | 67 | |||
42 | 65 | out.println("\\end{tikzpicture}"); | 68 | out.println("\\end{tikzpicture}"); |
43 | 66 | if (option == TikZOutputOption.FULL_LATEX) { | 69 | if (option == TikZOutputOption.FULL_LATEX) { |
44 | 67 | out.println("\\end{document}"); | 70 | out.println("\\end{document}"); |
45 | @@ -94,7 +97,7 @@ | |||
46 | 94 | ArcPathPoint currentPoint = arc.getArcPath().getArcPathPoint(i); | 97 | ArcPathPoint currentPoint = arc.getArcPath().getArcPathPoint(i); |
47 | 95 | 98 | ||
48 | 96 | if(currentPoint.getPointType() == ArcPathPoint.STRAIGHT) { | 99 | if(currentPoint.getPointType() == ArcPathPoint.STRAIGHT) { |
50 | 97 | arcPoints += "to[bend right=0] (" + (currentPoint.getX()) + "," + (currentPoint.getY() * (-1)) + ") "; | 100 | arcPoints += "to [bend right=0] (" + (currentPoint.getX()) + "," + (currentPoint.getY() * (-1)) + ") "; |
51 | 98 | } else if (currentPoint.getPointType() == ArcPathPoint.CURVED) { | 101 | } else if (currentPoint.getPointType() == ArcPathPoint.CURVED) { |
52 | 99 | double xCtrl1 = Math.round(currentPoint.getControl1().getX()); | 102 | double xCtrl1 = Math.round(currentPoint.getControl1().getX()); |
53 | 100 | double yCtrl1 = Math.round(currentPoint.getControl1().getY() * (-1)); | 103 | double yCtrl1 = Math.round(currentPoint.getControl1().getY() * (-1)); |
54 | @@ -109,21 +112,19 @@ | |||
55 | 109 | } | 112 | } |
56 | 110 | 113 | ||
57 | 111 | String arrowType = getArcArrowType(arc); | 114 | String arrowType = getArcArrowType(arc); |
58 | 112 | String arcLabel = getArcLabels(arc); | ||
59 | 113 | 115 | ||
60 | 116 | out.append("% Arc between " + arc.getSource().getName() + " and " + arc.getTarget().getName() + "\n"); | ||
61 | 114 | out.append("\\draw["); | 117 | out.append("\\draw["); |
62 | 115 | out.append(arrowType); | 118 | out.append(arrowType); |
64 | 116 | out.append("] ("); | 119 | out.append(",pos=0.5] ("); |
65 | 117 | out.append(arc.getSource().getId()); | 120 | out.append(arc.getSource().getId()); |
66 | 118 | out.append(") "); | 121 | out.append(") "); |
67 | 119 | out.append(arcPoints); | 122 | out.append(arcPoints); |
75 | 120 | out.append("to[bend right=0]"); | 123 | out.append("to node[bend right=0,auto,align=left]"); |
76 | 121 | out.append(" ("); | 124 | out.append(" {"); |
77 | 122 | out.append(arc.getTarget().getId()); | 125 | out.append(handleNameLabel(arc.getNameLabel().getText())); |
78 | 123 | out.append(") {};\n"); | 126 | out.append("} "); |
79 | 124 | if(!arcLabel.equals("")) | 127 | out.append("(" + arc.getTarget().getId() + ");\n"); |
73 | 125 | out.append("%% Label for arc between " + arc.getSource().getName() + " and " + arc.getTarget().getName() + "\n"); | ||
74 | 126 | out.append(arcLabel); | ||
80 | 127 | } | 128 | } |
81 | 128 | return out; | 129 | return out; |
82 | 129 | } | 130 | } |
83 | @@ -142,50 +143,6 @@ | |||
84 | 142 | return arrowType; | 143 | return arrowType; |
85 | 143 | } | 144 | } |
86 | 144 | 145 | ||
87 | 145 | protected String getArcLabels(Arc arc) { | ||
88 | 146 | String arcLabel = ""; | ||
89 | 147 | String arcLabelPositionString = "\\draw (" + (arc.getNameLabel().getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node {"; | ||
90 | 148 | |||
91 | 149 | if (arc instanceof TimedInputArcComponent) { | ||
92 | 150 | if (!(arc.getSource() instanceof TimedTransitionComponent)) { | ||
93 | 151 | arcLabel = arcLabelPositionString; | ||
94 | 152 | if (arc.getWeight().value() > 1) { | ||
95 | 153 | arcLabel += "$" + arc.getWeight().value() + "\\times$\\ "; | ||
96 | 154 | } | ||
97 | 155 | |||
98 | 156 | if(TAPAALGUI.getCurrentTab().getLens().isTimed()) { | ||
99 | 157 | arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$"; | ||
100 | 158 | if (arc instanceof TimedTransportArcComponent) | ||
101 | 159 | arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr(); | ||
102 | 160 | arcLabel += "};\n"; | ||
103 | 161 | } else { | ||
104 | 162 | arcLabel += "};\n"; | ||
105 | 163 | } | ||
106 | 164 | |||
107 | 165 | } else { | ||
108 | 166 | arcLabel = arcLabelPositionString; | ||
109 | 167 | if (arc.getWeight().value() > 1) { | ||
110 | 168 | arcLabel += "$" + arc.getWeight().value() + "\\times$\\ "; | ||
111 | 169 | } | ||
112 | 170 | arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr() + "};\n"; | ||
113 | 171 | } | ||
114 | 172 | |||
115 | 173 | } else { | ||
116 | 174 | if (arc.getWeight().value() > 1) { | ||
117 | 175 | arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n"; | ||
118 | 176 | } | ||
119 | 177 | } | ||
120 | 178 | return arcLabel; | ||
121 | 179 | } | ||
122 | 180 | |||
123 | 181 | private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) { | ||
124 | 182 | if (!TAPAALGUI.getAppGui().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){ | ||
125 | 183 | return ""; | ||
126 | 184 | } else { | ||
127 | 185 | return arc.getGuardAsString(); | ||
128 | 186 | } | ||
129 | 187 | } | ||
130 | 188 | |||
131 | 189 | private StringBuffer exportTransitions(Transition[] transitions) { | 146 | private StringBuffer exportTransitions(Transition[] transitions) { |
132 | 190 | StringBuffer out = new StringBuffer(); | 147 | StringBuffer out = new StringBuffer(); |
133 | 191 | for (Transition trans : transitions) { | 148 | for (Transition trans : transitions) { |
134 | @@ -195,7 +152,8 @@ | |||
135 | 195 | 152 | ||
136 | 196 | 153 | ||
137 | 197 | out.append("\\node[transition"); | 154 | out.append("\\node[transition"); |
139 | 198 | out.append(angle); | 155 | out.append(angle); |
140 | 156 | out.append(handlePlaceAndTransitionLabel(trans.getNameLabel().getText(), trans.getName(), trans.getAttributesVisible())); | ||
141 | 199 | out.append("] at ("); | 157 | out.append("] at ("); |
142 | 200 | out.append((trans.getPositionX())); | 158 | out.append((trans.getPositionX())); |
143 | 201 | out.append(','); | 159 | out.append(','); |
144 | @@ -226,31 +184,30 @@ | |||
145 | 226 | out.append(trans.getId()); | 184 | out.append(trans.getId()); |
146 | 227 | out.append(".center) { };\n"); | 185 | out.append(".center) { };\n"); |
147 | 228 | } | 186 | } |
148 | 229 | if (trans.getAttributesVisible()){ | ||
149 | 230 | boolean isLabelAboveTransition = trans.getY() > trans.getNameLabel().getY(); | ||
150 | 231 | boolean isLabelBehindTrans = trans.getX() < trans.getNameLabel().getX(); | ||
151 | 232 | double xOffset = trans.getName().length() > 5 && !isLabelAboveTransition && !isLabelBehindTrans ? trans.getLayerOffset() : 0; | ||
152 | 233 | |||
153 | 234 | out.append("%% label for transition " + trans.getName() + "\n"); | ||
154 | 235 | out.append("\\draw ("); | ||
155 | 236 | out.append(trans.getNameLabel().getX() + xOffset + "," + (trans.getNameLabel().getY() * -1) + ")"); | ||
156 | 237 | out.append(" node "); | ||
157 | 238 | out.append(" {"); | ||
158 | 239 | out.append(exportMathName(trans.getName())); | ||
159 | 240 | out.append("};\n"); | ||
160 | 241 | } | ||
161 | 242 | } | 187 | } |
162 | 243 | return out; | 188 | return out; |
163 | 244 | } | 189 | } |
164 | 245 | 190 | ||
165 | 191 | private String handlePlaceAndTransitionLabel(String nameLabelText, String name, boolean isVisible) { | ||
166 | 192 | if(!isVisible) | ||
167 | 193 | return ""; | ||
168 | 194 | |||
169 | 195 | String result = ", label={[align=left,label distance=0cm]90:"; | ||
170 | 196 | result += "$\\mathrm{" + (name.replace("_","\\_")) + "}$"; | ||
171 | 197 | result += handleNameLabel(nameLabelText); | ||
172 | 198 | result += "}"; | ||
173 | 199 | return result; | ||
174 | 200 | } | ||
175 | 201 | |||
176 | 246 | private StringBuffer exportPlacesWithTokens(Place[] places) { | 202 | private StringBuffer exportPlacesWithTokens(Place[] places) { |
177 | 247 | StringBuffer out = new StringBuffer(); | 203 | StringBuffer out = new StringBuffer(); |
178 | 248 | 204 | ||
179 | 249 | for (Place place : places) { | 205 | for (Place place : places) { |
181 | 250 | String invariant = getPlaceInvariantString(place); | 206 | String invariant = "$" + getPlaceInvariantString(place) + "$"; |
182 | 251 | String tokensInPlace = getTokenListStringFor(place); | 207 | String tokensInPlace = getTokenListStringFor(place); |
183 | 252 | 208 | ||
184 | 253 | out.append("\\node[place"); | 209 | out.append("\\node[place"); |
185 | 210 | out.append(handlePlaceAndTransitionLabel(place.getNameLabel().getText(), place.getName(), place.getAttributesVisible())); | ||
186 | 254 | out.append("] at ("); | 211 | out.append("] at ("); |
187 | 255 | out.append(place.getPositionX()); | 212 | out.append(place.getPositionX()); |
188 | 256 | out.append(','); | 213 | out.append(','); |
189 | @@ -262,37 +219,36 @@ | |||
190 | 262 | exportPlaceTokens(place, out, ((TimedPlaceComponent) place).underlyingPlace().tokens().size()); | 219 | exportPlaceTokens(place, out, ((TimedPlaceComponent) place).underlyingPlace().tokens().size()); |
191 | 263 | 220 | ||
192 | 264 | if(((TimedPlaceComponent)place).underlyingPlace().isShared()){ | 221 | if(((TimedPlaceComponent)place).underlyingPlace().isShared()){ |
194 | 265 | out.append("\\node[sharedplace] at ("); | 222 | out.append("\\node[sharedplace "); |
195 | 223 | out.append("] at ("); | ||
196 | 266 | out.append(place.getId()); | 224 | out.append(place.getId()); |
197 | 267 | out.append(".center) { };\n"); | 225 | out.append(".center) { };\n"); |
198 | 268 | } | 226 | } |
199 | 269 | if (place.getAttributesVisible() || !invariant.equals("")){ | ||
200 | 270 | boolean isLabelAbovePlace = place.getY() > place.getNameLabel().getY(); | ||
201 | 271 | boolean isLabelBehindPlace = place.getX() < place.getNameLabel().getX(); | ||
202 | 272 | double xOffset = place.getName().length() > 6 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0; | ||
203 | 273 | double yOffset = isLabelAbovePlace ? (place.getNameLabel().getHeight() / 2) : 0; | ||
204 | 274 | |||
205 | 275 | out.append("%% label for place " + place.getName() + "\n"); | ||
206 | 276 | out.append("\\draw ("); | ||
207 | 277 | out.append((place.getNameLabel().getX() + xOffset) + "," + ((place.getNameLabel().getY() * -1) + yOffset) +")"); | ||
208 | 278 | out.append(" node[align=left] "); | ||
209 | 279 | out.append("{"); | ||
210 | 280 | if(place.getAttributesVisible()) | ||
211 | 281 | out.append(exportMathName(place.getName())); | ||
212 | 282 | if(!invariant.equals("")) { | ||
213 | 283 | if((place.getAttributesVisible())) | ||
214 | 284 | out.append("\\\\"); | ||
215 | 285 | out.append(invariant); | ||
216 | 286 | }else { | ||
217 | 287 | out.append("};\n"); | ||
218 | 288 | } | ||
219 | 289 | |||
220 | 290 | } | ||
221 | 291 | } | 227 | } |
222 | 292 | |||
223 | 293 | return out; | 228 | return out; |
224 | 294 | } | 229 | } |
225 | 295 | 230 | ||
226 | 231 | private String handleNameLabel(String nameLabel) { | ||
227 | 232 | String nameLabelsString = ""; | ||
228 | 233 | String[] labelsInName = nameLabel.split("\n"); | ||
229 | 234 | for(int i = 0; i < labelsInName.length; i++) { | ||
230 | 235 | if(labelsInName[i].contains("[")) { | ||
231 | 236 | nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i])); | ||
232 | 237 | } | ||
233 | 238 | else if(!labelsInName[i].isEmpty()){ | ||
234 | 239 | nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i])); | ||
235 | 240 | } | ||
236 | 241 | if(i != labelsInName.length - 1) { | ||
237 | 242 | nameLabelsString += "\\\\"; | ||
238 | 243 | } | ||
239 | 244 | } | ||
240 | 245 | return nameLabelsString; | ||
241 | 246 | } | ||
242 | 247 | |||
243 | 248 | private String escapeSpacesInAndOrNot(String str) { | ||
244 | 249 | return str.replace(" and ", "\\ and\\ ").replace(" or", "\\ or\\ ").replace(" not", "\\ not\\ "); | ||
245 | 250 | } | ||
246 | 251 | |||
247 | 296 | private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) { | 252 | private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) { |
248 | 297 | // Dot radius | 253 | // Dot radius |
249 | 298 | final double tRadius = 1; | 254 | final double tRadius = 1; |
250 | @@ -317,14 +273,14 @@ | |||
251 | 317 | out.append(","); | 273 | out.append(","); |
252 | 318 | out.append(placeYpos + 4); | 274 | out.append(placeYpos + 4); |
253 | 319 | out.append(")"); | 275 | out.append(")"); |
255 | 320 | out.append("{0,0};\n"); | 276 | out.append("{0.0};\n"); |
256 | 321 | 277 | ||
257 | 322 | out.append("\\node at ("); // Bottom | 278 | out.append("\\node at ("); // Bottom |
258 | 323 | out.append(placeXpos); | 279 | out.append(placeXpos); |
259 | 324 | out.append(","); | 280 | out.append(","); |
260 | 325 | out.append(placeYpos - 5); | 281 | out.append(placeYpos - 5); |
261 | 326 | out.append(")"); | 282 | out.append(")"); |
263 | 327 | out.append("{0,0};\n"); | 283 | out.append("{0.0};\n"); |
264 | 328 | return; | 284 | return; |
265 | 329 | case 1: | 285 | case 1: |
266 | 330 | out.append("\\node at ("); // Top | 286 | out.append("\\node at ("); // Top |
267 | @@ -332,7 +288,7 @@ | |||
268 | 332 | out.append(","); | 288 | out.append(","); |
269 | 333 | out.append(placeYpos); | 289 | out.append(placeYpos); |
270 | 334 | out.append(")"); | 290 | out.append(")"); |
272 | 335 | out.append("{0,0};\n"); | 291 | out.append("{0.0};\n"); |
273 | 336 | return; | 292 | return; |
274 | 337 | default: | 293 | default: |
275 | 338 | out.append("\\node at ("); | 294 | out.append("\\node at ("); |
276 | @@ -437,6 +393,124 @@ | |||
277 | 437 | } | 393 | } |
278 | 438 | } | 394 | } |
279 | 439 | 395 | ||
280 | 396 | private StringBuffer exportGlobalVariables() { | ||
281 | 397 | StringBuffer out = new StringBuffer(); | ||
282 | 398 | |||
283 | 399 | Context context = new Context(TAPAALGUI.getCurrentTab()); | ||
284 | 400 | List<ColorType> listColorTypes = context.network().colorTypes(); | ||
285 | 401 | List<Constant> constantsList = new ArrayList<>(context.network().constants()); | ||
286 | 402 | List<Variable> variableList = context.network().variables(); | ||
287 | 403 | |||
288 | 404 | if(!context.network().isColored()) { | ||
289 | 405 | if(constantsList.isEmpty()) { | ||
290 | 406 | return out; | ||
291 | 407 | } | ||
292 | 408 | out.append("%%Global box which contains global color types, variables and/or constants.\n"); | ||
293 | 409 | out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {"); | ||
294 | 410 | exportConstants(constantsList, out); | ||
295 | 411 | out.append("};"); | ||
296 | 412 | return out; | ||
297 | 413 | } | ||
298 | 414 | |||
299 | 415 | if((listColorTypes.isEmpty() && constantsList.isEmpty() && variableList.isEmpty())) | ||
300 | 416 | return out; | ||
301 | 417 | |||
302 | 418 | out.append("%%Global box which contains global color types, variables and/or constants.\n"); | ||
303 | 419 | out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {"); | ||
304 | 420 | |||
305 | 421 | exportColorTypes(listColorTypes, out); | ||
306 | 422 | |||
307 | 423 | if(listColorTypes.size() > 0 && (variableList.size() > 0 || constantsList.size() > 0)) { | ||
308 | 424 | out.append("\\\\"); | ||
309 | 425 | } | ||
310 | 426 | |||
311 | 427 | exportVariables(variableList, out); | ||
312 | 428 | |||
313 | 429 | if(variableList.size() > 0 && !constantsList.isEmpty()) { | ||
314 | 430 | out.append("\\\\"); | ||
315 | 431 | } | ||
316 | 432 | |||
317 | 433 | exportConstants(constantsList, out); | ||
318 | 434 | |||
319 | 435 | out.append("};"); | ||
320 | 436 | |||
321 | 437 | return out; | ||
322 | 438 | } | ||
323 | 439 | |||
324 | 440 | private void exportColorTypes(List<ColorType> listColorTypes, StringBuffer out) { | ||
325 | 441 | String stringColorList = ""; | ||
326 | 442 | for(int i = 0; i < listColorTypes.size(); i++) { | ||
327 | 443 | if(i == 0) { | ||
328 | 444 | out.append("Color Types:\\\\"); | ||
329 | 445 | } | ||
330 | 446 | out.append("$\\mathit{" + listColorTypes.get(i).getName() + "}$ \\textbf{is} "); | ||
331 | 447 | |||
332 | 448 | if(listColorTypes.get(i).isProductColorType()) { | ||
333 | 449 | out.append("$\\mathit{<"); | ||
334 | 450 | for(int x = 0; x < listColorTypes.get(i).getProductColorTypes().size(); x++) { | ||
335 | 451 | stringColorList += listColorTypes.get(i).getProductColorTypes().get(x).getName().replace("_", "\\_"); | ||
336 | 452 | |||
337 | 453 | if(x != listColorTypes.get(i).getProductColorTypes().size() - 1){ | ||
338 | 454 | stringColorList += ", "; | ||
339 | 455 | } | ||
340 | 456 | } | ||
341 | 457 | out.append(stringColorList + ">}$\\\\"); | ||
342 | 458 | stringColorList = ""; | ||
343 | 459 | |||
344 | 460 | } else if(listColorTypes.get(i).isIntegerRange()) { | ||
345 | 461 | out.append("$\\mathit{"); | ||
346 | 462 | if(listColorTypes.get(i).size() > 1) { | ||
347 | 463 | int listSize = listColorTypes.get(i).size(); | ||
348 | 464 | out.append("[" + listColorTypes.get(i).getColors().get(0).getColorName().replace("_","\\_") + ".." + listColorTypes.get(i).getColors().get(listSize - 1).getColorName().replace("_","\\_") + "]"); | ||
349 | 465 | } else { | ||
350 | 466 | out.append("[" + listColorTypes.get(i).getFirstColor().getColorName().replace("_","\\_") + "]"); | ||
351 | 467 | } | ||
352 | 468 | out.append("}$\\\\"); | ||
353 | 469 | |||
354 | 470 | } else { | ||
355 | 471 | out.append("$\\mathit{["); | ||
356 | 472 | for(int x = 0; x < listColorTypes.get(i).getColors().size(); x++) { | ||
357 | 473 | stringColorList += listColorTypes.get(i).getColors().get(x).getName().replace("_","\\_"); | ||
358 | 474 | |||
359 | 475 | if(x != listColorTypes.get(i).getColors().size() - 1){ | ||
360 | 476 | stringColorList += ", "; | ||
361 | 477 | } | ||
362 | 478 | } | ||
363 | 479 | out.append(stringColorList + "]}$\\\\"); | ||
364 | 480 | stringColorList = ""; | ||
365 | 481 | } | ||
366 | 482 | } | ||
367 | 483 | } | ||
368 | 484 | |||
369 | 485 | private void exportVariables(List<Variable> variableList, StringBuffer out) { | ||
370 | 486 | String result = ""; | ||
371 | 487 | for(int i = 0; i < variableList.size(); i++) { | ||
372 | 488 | if (i == 0) { | ||
373 | 489 | result += "Variables:\\\\ "; | ||
374 | 490 | } | ||
375 | 491 | result += "$\\mathit{" + variableList.get(i).getName().replace("_","\\_") + " \\textbf{ in } " + variableList.get(i).getColorType().getName().replace("_","\\_") + "}$"; | ||
376 | 492 | if(i != variableList.size() - 1) { | ||
377 | 493 | result += "\\\\"; | ||
378 | 494 | } | ||
379 | 495 | } | ||
380 | 496 | out.append(result); | ||
381 | 497 | } | ||
382 | 498 | |||
383 | 499 | private void exportConstants(List<Constant> constantsList, StringBuffer out) { | ||
384 | 500 | String result = ""; | ||
385 | 501 | |||
386 | 502 | for(int i = 0; i < constantsList.size(); i++) { | ||
387 | 503 | if(i == 0) { | ||
388 | 504 | result += "Constants:\\\\"; | ||
389 | 505 | } | ||
390 | 506 | result += "$\\mathit{" + constantsList.get(i).toString().replace("_","\\_") + "}$"; | ||
391 | 507 | if(i != constantsList.size() - 1) { | ||
392 | 508 | result += "\\\\"; | ||
393 | 509 | } | ||
394 | 510 | } | ||
395 | 511 | out.append(result); | ||
396 | 512 | } | ||
397 | 513 | |||
398 | 440 | protected String getTokenListStringFor(Place place) { | 514 | protected String getTokenListStringFor(Place place) { |
399 | 441 | List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens(); | 515 | List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens(); |
400 | 442 | 516 | ||
401 | @@ -455,7 +529,7 @@ | |||
402 | 455 | String invariant = ""; | 529 | String invariant = ""; |
403 | 456 | 530 | ||
404 | 457 | if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf")) | 531 | if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf")) |
406 | 458 | invariant = "$\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$};\n"; | 532 | invariant = replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "};\n"; |
407 | 459 | return invariant; | 533 | return invariant; |
408 | 460 | } | 534 | } |
409 | 461 | 535 | ||
410 | @@ -480,12 +554,14 @@ | |||
411 | 480 | StringBuffer out = new StringBuffer(); | 554 | StringBuffer out = new StringBuffer(); |
412 | 481 | 555 | ||
413 | 482 | out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n"); | 556 | out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n"); |
415 | 483 | out.append("%% the figure can be scaled by changing xscale and yscale\n"); | 557 | out.append("%% the figure can be scaled by changing xscale and yscale or the size of the x- and y-coordinates\n"); |
416 | 484 | out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n"); | 558 | out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n"); |
421 | 485 | out.append("%% can be adjusted so that they do not cover arcs\n"); | 559 | out.append("%% these can be adjusted by adjusting either the coordinates, the label distance or the label degree\n"); |
422 | 486 | out.append("%% similarly the curving of arcs can be done by adjusting bend left/right=XX\n"); | 560 | out.append("%% that is placed right after the 'label-distance'. 90: is above (default), 180 is left, 270 is below etc.\n"); |
423 | 487 | out.append("%% labels may be slightly skewed compared to the tapaal drawing due to rounding.\n"); | 561 | out.append("%% The curving of arcs can be done by adjusting bend left/right=XX\n"); |
424 | 488 | out.append("%% This can be adjusted by tuning the coordinates of the label\n"); | 562 | out.append("%% labels may be slightly skewed compared to the Tapaal drawing due to rounding.\n"); |
425 | 563 | out.append("%% This can be adjusted by tuning the coordinates of the label, or the degree (see above)\n"); | ||
426 | 564 | 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"); | ||
427 | 489 | out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n"); | 565 | out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n"); |
428 | 490 | 566 | ||
429 | 491 | out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n"); | 567 | out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n"); |
430 | @@ -496,39 +572,24 @@ | |||
431 | 496 | out.append("\\tikzstyle{every token}=[fill=white,text=black]\n"); | 572 | out.append("\\tikzstyle{every token}=[fill=white,text=black]\n"); |
432 | 497 | out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n"); | 573 | out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n"); |
433 | 498 | out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n"); | 574 | out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n"); |
436 | 499 | out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]"); | 575 | out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]\n"); |
437 | 500 | out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]"); | 576 | out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]\n"); |
438 | 577 | out.append("\\tikzstyle{globalBox} = [draw,thick,align=left]"); | ||
439 | 501 | return out; | 578 | return out; |
440 | 502 | } | 579 | } |
441 | 503 | 580 | ||
442 | 504 | protected String replaceWithMathLatex(String text) { | 581 | protected String replaceWithMathLatex(String text) { |
472 | 505 | return text.replace("inf", "\\infty").replace("<=", "\\leq ").replace("*", "\\cdot "); | 582 | String[] stringList = text.split(" "); |
473 | 506 | } | 583 | String result = ""; |
474 | 507 | 584 | ||
475 | 508 | private String exportMathName(String name) { | 585 | for(int i = 0; i < stringList.length; i++) { |
476 | 509 | StringBuilder out = new StringBuilder("$\\mathrm{"); | 586 | result += "$\\mathit{" + replaceSpecialSymbols(stringList[i]) + "}$ "; |
477 | 510 | int subscripts = 0; | 587 | } |
478 | 511 | for (int i = 0; i < name.length() - 1; i++) { | 588 | return result; |
479 | 512 | char c = name.charAt(i); | 589 | } |
480 | 513 | if (c == '_') { | 590 | |
481 | 514 | out.append("_{"); | 591 | protected String replaceSpecialSymbols(String text) { |
482 | 515 | subscripts++; | 592 | return text.replace("inf", "\\infty").replace("<=", "\\leq").replace("*", "\\cdot") |
483 | 516 | } else { | 593 | .replace("\u2192", "\\rightarrow").replace("\u221E", "\\infty"); |
484 | 517 | out.append(c); | 594 | } |
456 | 518 | } | ||
457 | 519 | } | ||
458 | 520 | |||
459 | 521 | char last = name.charAt(name.length() - 1); | ||
460 | 522 | if (last == '_') { | ||
461 | 523 | out.append("\\_"); | ||
462 | 524 | } else | ||
463 | 525 | out.append(last); | ||
464 | 526 | |||
465 | 527 | for (int i = 0; i < subscripts; i++) { | ||
466 | 528 | out.append('}'); | ||
467 | 529 | } | ||
468 | 530 | out.append("}$"); | ||
469 | 531 | return out.toString(); | ||
470 | 532 | } | ||
471 | 533 | |||
485 | 534 | } | 595 | } |
It would be nice if instead of (in referendum colored timed):
1′v[1, 2]Voters1 → [1, 4]
one would print:
1′v
[1, 2]
Voters1 → [1, 4]
(on three sepratate lines).