-
Notifications
You must be signed in to change notification settings - Fork 37
/
SVG.tla
181 lines (165 loc) · 11 KB
/
SVG.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
----------------------------- MODULE SVG -----------------------------
LOCAL INSTANCE Naturals
LOCAL INSTANCE Sequences
LOCAL INSTANCE Integers
LOCAL INSTANCE TLC
LOCAL INSTANCE FiniteSets
(******************************************************************************)
(* Helper Operators *)
(******************************************************************************)
LOCAL Merge(r1, r2) ==
(**************************************************************************)
(* Merge two records. *)
(* *)
(* If a field appears in both records, then the value from 'r1' is kept. *)
(**************************************************************************)
LET D1 == DOMAIN r1
D2 == DOMAIN r2 IN
[k \in (D1 \cup D2) |-> IF k \in D1 THEN r1[k] ELSE r2[k]]
LOCAL SVGElem(_name, _attrs, _children, _innerText) ==
(**************************************************************************)
(* SVG element constructor. *)
(* *)
(* An SVG element like: *)
(* *)
(* [name |-> "elem", attrs |-> [k1 |-> "0", k2 |-> "1"], children |-> *)
(* <<>>, innerText |-> ""] *)
(* *)
(* would represent the SVG element '<elem k1="0" k2="1"></elem>' *)
(**************************************************************************)
[name |-> _name,
attrs |-> _attrs,
children |-> _children,
innerText |-> _innerText ]
(******************************************************************************)
(* *)
(* Core Graphic Elements. *)
(* *)
(* These primitives are TLA+ wrappers around SVG elements. We base them on *)
(* SVG since it is a widely used format and provides good features for *)
(* representing and laying out vector graphics. Each primitive below should *)
(* roughly correspond to a standard SVG element type. We represent a graphic *)
(* element as a record with the fields 'name', 'attrs', 'children', and *)
(* 'innerText'. 'name' is the name of the SVG element, 'attrs' is a record *)
(* mapping SVG attribute names to values, 'children' is a tuple containing *)
(* any children elements, and 'innerText' is a string that represents any raw *)
(* text that is contained directly inside the SVG element. The 'innerText' *)
(* field is only meaningful for text elements. *)
(* *)
(* All elements accept an 'attrs' argument, which must be a function mapping *)
(* string keys to string values. These key-value pairs describe any *)
(* additional SVG attributes of the element. To pass no attributes, just *)
(* pass attrs=<<>>. *)
(* *)
(******************************************************************************)
Line(x1, y1, x2, y2, attrs) ==
(**************************************************************************)
(* Line element. 'x1', 'y1', 'x2', and 'y2' should be given as integers. *)
(**************************************************************************)
LET svgAttrs == [x1 |-> ToString(x1),
y1 |-> ToString(y1),
x2 |-> ToString(x2),
y2 |-> ToString(y2)] IN
SVGElem("line", Merge(svgAttrs, attrs), <<>>, "")
Circle(cx, cy, r, attrs) ==
(**************************************************************************)
(* Circle element. 'cx', 'cy', and 'r' should be given as integers. *)
(**************************************************************************)
LET svgAttrs == [cx |-> ToString(cx),
cy |-> ToString(cy),
r |-> ToString(r)] IN
SVGElem("circle", Merge(svgAttrs, attrs), <<>>, "")
Rect(x, y, w, h, attrs) ==
(**************************************************************************)
(* Rectangle element. 'x', 'y', 'w', and 'h' should be given as *)
(* integers. *)
(**************************************************************************)
LET svgAttrs == [x |-> ToString(x),
y |-> ToString(y),
width |-> ToString(w),
height |-> ToString(h)] IN
SVGElem("rect", Merge(svgAttrs, attrs), <<>>, "")
Text(x, y, text, attrs) ==
(**************************************************************************)
(* Text element.'x' and 'y' should be given as integers, and 'text' given *)
(* as a string. *)
(**************************************************************************)
LET svgAttrs == [x |-> ToString(x),
y |-> ToString(y)] IN
SVGElem("text", Merge(svgAttrs, attrs), <<>>, text)
Group(children, attrs) ==
(**************************************************************************)
(* Group element. 'children' is a sequence of elements that will be *)
(* contained in this group. *)
(**************************************************************************)
SVGElem("g", attrs, children, "")
Svg(children, attrs) ==
(**************************************************************************)
(* Svg container. 'children' is a sequence of elements that will be *)
(* contained in this svg container. *)
(**************************************************************************)
SVGElem("svg", attrs, children, "")
SVGElemToString(elem) ==
(**************************************************************************)
(* Convert an SVG element record into its string representation. *)
(* *)
(* This operator is expected to be replaced by a Java module override. *)
(* We do not implement it in pure TLA+ because doing non-trivial string *)
(* manipulation in TLA+ is tedious. Also, the performance of *)
(* implementing this in TLA+ has been demonstrated to be prohibitively *)
(* slow. *)
(**************************************************************************)
TRUE
-------------------------------------------------------------------------------
NodeOfRingNetwork(cx, cy, r, n, m) ==
(**************************************************************************)
(* Equals the Cartesian coordinates of the n-th of m nodes in a ring *)
(* (https://en.wikipedia.org/wiki/Ring_network), such that the circle *)
(* on which the nodes are placed has radius r and is centered at the *)
(* coordinates cx, cy. *)
(* *)
(* ASSUME /\ n \in 0..360 /\ m \in 0..360 /\ n <= m *)
(* /\ cx \in Nat /\ cy \in Nat /\ r \in Nat *)
(* *)
(* Example to create a ring network of M nodes (Rects with dimension 15) *)
(* with center (10,10) and radius 5: *)
(* *)
(* ASSUME M \in Nat *)
(* *)
(* RN[ n \in 1..M ] == *)
(* LET c == NodeOfRingNetwork(10, 10, 5, n, M) *)
(* node == Rect(c.x, c.y, 15, 15, <<>>) *)
(* IN Group(<<node>>, <<>>) *)
(* *)
(* Note: It would have been more elegant to provide the basic geometric *)
(* operators, such as polar to Cartesian conversion. However, *)
(* TLC's lack of floats makes this impractical due to intermediate *)
(* rounding errors. *)
(* *)
(* For this operator's actual definition, please consult the Java module *)
(* override at: *)
(* modules/tlc2/overrides/SVG.java#ringNetwork *)
(**************************************************************************)
[ x |-> 0, y |-> 0 ]
NodesOfDirectedMultiGraph(nodes, edges, options) ==
(**************************************************************************)
(* Example to layout a graph with the given Nodes and Edges: *)
(* *)
(* Nodes == {"v1", "v2", "v3"} \* v3 is not connected *)
(* Edges == {<<"v1", "v2">>, <<"v2", "v1">>} *)
(* Graph == NodesOfDirectedMultiGraph(Nodes, Edges, [algo |-> ...]) *)
(* *)
(* RN[ n \in Nodes ] == *)
(* LET c == Graph[n] *)
(* node == Rect(c.x, c.y, 23, 42, <<>>) *)
(* IN Group(<<node>>, <<>>) *)
(* *)
(* For this operator's actual definition, please consult the Java module *)
(* override at: *)
(* modules/tlc2/overrides/SVG.java#directedMultiGraph *)
(**************************************************************************)
CHOOSE f \in [ nodes -> [x: Int, y: Int] ]: TRUE
PointOnLine(from, to, segment) ==
[x |-> from.x + ((to.x - from.x) \div segment),
y |-> from.y + ((to.y - from.y) \div segment)]
=============================================================================