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: |
461 lines (+199/-136) 1 file modified
src/net/tapaal/export/TikZExporter.java (+199/-136) |
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 | Approve | |
Review via email: mp+415749@code.launchpad.net |
This proposal supersedes a proposal from 2022-02-17.
This proposal has been superseded by a proposal from 2022-02-21.
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.
Kenneth Yrke Jørgensen (yrke) : | # |
- 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-21 15:45:21 +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.0] ("); |
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.getApp().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.getApp().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,38 @@ | |||
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 | |||
231 | 236 | if(labelsInName[i].contains("[")) { | ||
232 | 237 | nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i])); | ||
233 | 238 | nameLabelsString += "\\\\"; | ||
234 | 239 | } | ||
235 | 240 | else if(!labelsInName[i].isEmpty()){ | ||
236 | 241 | nameLabelsString += escapeSpacesInAndOrNot(replaceWithMathLatex(labelsInName[i])); | ||
237 | 242 | nameLabelsString += "\\\\"; | ||
238 | 243 | } else { | ||
239 | 244 | nameLabelsString += "\\\\"; | ||
240 | 245 | } | ||
241 | 246 | } | ||
242 | 247 | return nameLabelsString; | ||
243 | 248 | } | ||
244 | 249 | |||
245 | 250 | private String escapeSpacesInAndOrNot(String str) { | ||
246 | 251 | return str.replace(" and ", "\\ and\\ ").replace(" or", "\\ or\\ ").replace(" not", "\\ not\\ "); | ||
247 | 252 | } | ||
248 | 253 | |||
249 | 296 | private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) { | 254 | private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) { |
250 | 297 | // Dot radius | 255 | // Dot radius |
251 | 298 | final double tRadius = 1; | 256 | final double tRadius = 1; |
252 | @@ -437,6 +395,124 @@ | |||
253 | 437 | } | 395 | } |
254 | 438 | } | 396 | } |
255 | 439 | 397 | ||
256 | 398 | private StringBuffer exportGlobalVariables() { | ||
257 | 399 | StringBuffer out = new StringBuffer(); | ||
258 | 400 | |||
259 | 401 | Context context = new Context(TAPAALGUI.getCurrentTab()); | ||
260 | 402 | List<ColorType> listColorTypes = context.network().colorTypes(); | ||
261 | 403 | List<Constant> constantsList = new ArrayList<>(context.network().constants()); | ||
262 | 404 | List<Variable> variableList = context.network().variables(); | ||
263 | 405 | |||
264 | 406 | if(!context.network().isColored()) { | ||
265 | 407 | if(constantsList.isEmpty()) { | ||
266 | 408 | return out; | ||
267 | 409 | } | ||
268 | 410 | out.append("%%Global box which contains global color types, variables and/or constants.\n"); | ||
269 | 411 | out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {"); | ||
270 | 412 | exportConstants(constantsList, out); | ||
271 | 413 | out.append("};"); | ||
272 | 414 | return out; | ||
273 | 415 | } | ||
274 | 416 | |||
275 | 417 | if((listColorTypes.isEmpty() && constantsList.isEmpty() && variableList.isEmpty())) | ||
276 | 418 | return out; | ||
277 | 419 | |||
278 | 420 | out.append("%%Global box which contains global color types, variables and/or constants.\n"); | ||
279 | 421 | out.append("\\node [globalBox] (globalBox) at (current bounding box.north west) [anchor=south west] {"); | ||
280 | 422 | |||
281 | 423 | exportColorTypes(listColorTypes, out); | ||
282 | 424 | |||
283 | 425 | if(listColorTypes.size() > 0 && (variableList.size() > 0 || constantsList.size() > 0)) { | ||
284 | 426 | out.append("\\\\"); | ||
285 | 427 | } | ||
286 | 428 | |||
287 | 429 | exportVariables(variableList, out); | ||
288 | 430 | |||
289 | 431 | if(variableList.size() > 0 && !constantsList.isEmpty()) { | ||
290 | 432 | out.append("\\\\"); | ||
291 | 433 | } | ||
292 | 434 | |||
293 | 435 | exportConstants(constantsList, out); | ||
294 | 436 | |||
295 | 437 | out.append("};"); | ||
296 | 438 | |||
297 | 439 | return out; | ||
298 | 440 | } | ||
299 | 441 | |||
300 | 442 | private void exportColorTypes(List<ColorType> listColorTypes, StringBuffer out) { | ||
301 | 443 | String stringColorList = ""; | ||
302 | 444 | for(int i = 0; i < listColorTypes.size(); i++) { | ||
303 | 445 | if(i == 0) { | ||
304 | 446 | out.append("Color Types:\\\\"); | ||
305 | 447 | } | ||
306 | 448 | out.append("$\\mathit{" + listColorTypes.get(i).getName() + "}$ \\textbf{is} "); | ||
307 | 449 | |||
308 | 450 | if(listColorTypes.get(i).isProductColorType()) { | ||
309 | 451 | out.append("$\\mathit{<"); | ||
310 | 452 | for(int x = 0; x < listColorTypes.get(i).getProductColorTypes().size(); x++) { | ||
311 | 453 | stringColorList += listColorTypes.get(i).getProductColorTypes().get(x).getName().replace("_", "\\_"); | ||
312 | 454 | |||
313 | 455 | if(x != listColorTypes.get(i).getProductColorTypes().size() - 1){ | ||
314 | 456 | stringColorList += ", "; | ||
315 | 457 | } | ||
316 | 458 | } | ||
317 | 459 | out.append(stringColorList + ">}$\\\\"); | ||
318 | 460 | stringColorList = ""; | ||
319 | 461 | |||
320 | 462 | } else if(listColorTypes.get(i).isIntegerRange()) { | ||
321 | 463 | out.append("$\\mathit{"); | ||
322 | 464 | if(listColorTypes.get(i).size() > 1) { | ||
323 | 465 | int listSize = listColorTypes.get(i).size(); | ||
324 | 466 | out.append("[" + listColorTypes.get(i).getColors().get(0).getColorName().replace("_","\\_") + ".." + listColorTypes.get(i).getColors().get(listSize - 1).getColorName().replace("_","\\_") + "]"); | ||
325 | 467 | } else { | ||
326 | 468 | out.append("[" + listColorTypes.get(i).getFirstColor().getColorName().replace("_","\\_") + "]"); | ||
327 | 469 | } | ||
328 | 470 | out.append("}$\\\\"); | ||
329 | 471 | |||
330 | 472 | } else { | ||
331 | 473 | out.append("$\\mathit{["); | ||
332 | 474 | for(int x = 0; x < listColorTypes.get(i).getColors().size(); x++) { | ||
333 | 475 | stringColorList += listColorTypes.get(i).getColors().get(x).getName().replace("_","\\_"); | ||
334 | 476 | |||
335 | 477 | if(x != listColorTypes.get(i).getColors().size() - 1){ | ||
336 | 478 | stringColorList += ", "; | ||
337 | 479 | } | ||
338 | 480 | } | ||
339 | 481 | out.append(stringColorList + "]}$\\\\"); | ||
340 | 482 | stringColorList = ""; | ||
341 | 483 | } | ||
342 | 484 | } | ||
343 | 485 | } | ||
344 | 486 | |||
345 | 487 | private void exportVariables(List<Variable> variableList, StringBuffer out) { | ||
346 | 488 | String result = ""; | ||
347 | 489 | for(int i = 0; i < variableList.size(); i++) { | ||
348 | 490 | if (i == 0) { | ||
349 | 491 | result += "Variables:\\\\ "; | ||
350 | 492 | } | ||
351 | 493 | result += "$\\mathit{" + variableList.get(i).getName().replace("_","\\_") + " \\textbf{ in } " + variableList.get(i).getColorType().getName().replace("_","\\_") + "}$"; | ||
352 | 494 | if(i != variableList.size() - 1) { | ||
353 | 495 | result += "\\\\"; | ||
354 | 496 | } | ||
355 | 497 | } | ||
356 | 498 | out.append(result); | ||
357 | 499 | } | ||
358 | 500 | |||
359 | 501 | private void exportConstants(List<Constant> constantsList, StringBuffer out) { | ||
360 | 502 | String result = ""; | ||
361 | 503 | |||
362 | 504 | for(int i = 0; i < constantsList.size(); i++) { | ||
363 | 505 | if(i == 0) { | ||
364 | 506 | result += "Constants:\\\\"; | ||
365 | 507 | } | ||
366 | 508 | result += "$\\mathit{" + constantsList.get(i).toString().replace("_","\\_") + "}$"; | ||
367 | 509 | if(i != constantsList.size() - 1) { | ||
368 | 510 | result += "\\\\"; | ||
369 | 511 | } | ||
370 | 512 | } | ||
371 | 513 | out.append(result); | ||
372 | 514 | } | ||
373 | 515 | |||
374 | 440 | protected String getTokenListStringFor(Place place) { | 516 | protected String getTokenListStringFor(Place place) { |
375 | 441 | List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens(); | 517 | List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens(); |
376 | 442 | 518 | ||
377 | @@ -455,7 +531,7 @@ | |||
378 | 455 | String invariant = ""; | 531 | String invariant = ""; |
379 | 456 | 532 | ||
380 | 457 | if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf")) | 533 | if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf")) |
382 | 458 | invariant = "$\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$};\n"; | 534 | invariant = replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "};\n"; |
383 | 459 | return invariant; | 535 | return invariant; |
384 | 460 | } | 536 | } |
385 | 461 | 537 | ||
386 | @@ -480,12 +556,14 @@ | |||
387 | 480 | StringBuffer out = new StringBuffer(); | 556 | StringBuffer out = new StringBuffer(); |
388 | 481 | 557 | ||
389 | 482 | out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n"); | 558 | out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n"); |
391 | 483 | out.append("%% the figure can be scaled by changing xscale and yscale\n"); | 559 | out.append("%% the figure can be scaled by changing xscale and yscale or the size of the x- and y-coordinates\n"); |
392 | 484 | out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n"); | 560 | out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n"); |
397 | 485 | out.append("%% can be adjusted so that they do not cover arcs\n"); | 561 | out.append("%% these can be adjusted by adjusting either the coordinates, the label distance or the label degree\n"); |
398 | 486 | out.append("%% similarly the curving of arcs can be done by adjusting bend left/right=XX\n"); | 562 | out.append("%% that is placed right after the 'label-distance'. 90: is above (default), 180 is left, 270 is below etc.\n"); |
399 | 487 | out.append("%% labels may be slightly skewed compared to the tapaal drawing due to rounding.\n"); | 563 | out.append("%% The curving of arcs can be done by adjusting bend left/right=XX\n"); |
400 | 488 | out.append("%% This can be adjusted by tuning the coordinates of the label\n"); | 564 | out.append("%% labels may be slightly skewed compared to the Tapaal drawing due to rounding.\n"); |
401 | 565 | out.append("%% This can be adjusted by tuning the coordinates of the label, or the degree (see above)\n"); | ||
402 | 566 | 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"); | ||
403 | 489 | out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n"); | 567 | out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n"); |
404 | 490 | 568 | ||
405 | 491 | out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n"); | 569 | out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n"); |
406 | @@ -496,39 +574,24 @@ | |||
407 | 496 | out.append("\\tikzstyle{every token}=[fill=white,text=black]\n"); | 574 | out.append("\\tikzstyle{every token}=[fill=white,text=black]\n"); |
408 | 497 | out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n"); | 575 | out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n"); |
409 | 498 | out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n"); | 576 | out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n"); |
412 | 499 | out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]"); | 577 | out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]\n"); |
413 | 500 | out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]"); | 578 | out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]\n"); |
414 | 579 | out.append("\\tikzstyle{globalBox} = [draw,thick,align=left]"); | ||
415 | 501 | return out; | 580 | return out; |
416 | 502 | } | 581 | } |
417 | 503 | 582 | ||
418 | 504 | protected String replaceWithMathLatex(String text) { | 583 | protected String replaceWithMathLatex(String text) { |
448 | 505 | return text.replace("inf", "\\infty").replace("<=", "\\leq ").replace("*", "\\cdot "); | 584 | String[] stringList = text.split(" "); |
449 | 506 | } | 585 | String result = ""; |
450 | 507 | 586 | ||
451 | 508 | private String exportMathName(String name) { | 587 | for(int i = 0; i < stringList.length; i++) { |
452 | 509 | StringBuilder out = new StringBuilder("$\\mathrm{"); | 588 | result += "$\\mathit{" + replaceSpecialSymbols(stringList[i]) + "}$ "; |
453 | 510 | int subscripts = 0; | 589 | } |
454 | 511 | for (int i = 0; i < name.length() - 1; i++) { | 590 | return result; |
455 | 512 | char c = name.charAt(i); | 591 | } |
456 | 513 | if (c == '_') { | 592 | |
457 | 514 | out.append("_{"); | 593 | protected String replaceSpecialSymbols(String text) { |
458 | 515 | subscripts++; | 594 | return text.replace("inf", "\\infty").replace("<=", "\\leq").replace("*", "\\cdot") |
459 | 516 | } else { | 595 | .replace("\u2192", "\\rightarrow").replace("\u221E", "\\infty"); |
460 | 517 | out.append(c); | 596 | } |
432 | 518 | } | ||
433 | 519 | } | ||
434 | 520 | |||
435 | 521 | char last = name.charAt(name.length() - 1); | ||
436 | 522 | if (last == '_') { | ||
437 | 523 | out.append("\\_"); | ||
438 | 524 | } else | ||
439 | 525 | out.append(last); | ||
440 | 526 | |||
441 | 527 | for (int i = 0; i < subscripts; i++) { | ||
442 | 528 | out.append('}'); | ||
443 | 529 | } | ||
444 | 530 | out.append("}$"); | ||
445 | 531 | return out.toString(); | ||
446 | 532 | } | ||
447 | 533 | |||
461 | 534 | } | 597 | } |
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).