-
Notifications
You must be signed in to change notification settings - Fork 2
/
index.html
executable file
·430 lines (408 loc) · 19.3 KB
/
index.html
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
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Stargazer: A Pi-Calculus Simulator</title>
<meta name="description" content="A Visual Pi-Calculus Simulator">
<meta name="author" content="Emanuele D'Osualdo">
<link rel="icon" type="image/png" href="http://emanueledosualdo.com/images/favicon.png">
<meta name="viewport" content="width=device-width, initial-scale=1">
<link rel="stylesheet" href="lib/semantic/semantic.min.css">
<link rel="stylesheet" href="lib/color-picker.min.css">
<link rel="stylesheet" href="stargazer.min.css">
<link rel="stylesheet" href="app.min.css">
<script src="lib/jquery.js"></script>
<script src="lib/semantic/semantic.min.js"></script>
<script src="lib/d3.min.js"></script>
<script src="lib/color-picker.min.js"></script>
<script data-goatcounter="https://emanueledosualdo.goatcounter.com/count"
async src="/js/count.js"></script>
<script src="stargazer.min.js"></script>
</head>
<body>
<div id="sourcecode" class="ui left wide vertical sidebar">
<div class="ui tiny program-menu secondary menu">
<div class="ui dropdown item">
<div class="ui transparent strong input">
<input id="program-name" type="text" value="Counters">
</div>
<i class="dropdown icon"></i>
<div class="menu" id="program-select"></div>
</div>
<div class="right menu">
<a class="ui compact del icon button item" title="Delete program">
<i class="trash icon"></i>
</a>
<a class="ui compact new icon button item" title="Add new program">
<i class="add circle icon"></i>
</a>
<a class="ui compact close icon button item" title="Close panel">
<i class="remove grey icon"></i>
</a>
</div>
</div>
<div id="source-panel">
<textarea id="code-editor" spellcheck="false" name="program"></textarea>
<div class="ui hidden error message" id="validate-code">
<i class="close icon"></i>
<div class="header"></div>
<p></p>
</div>
<button class="ui compact mini button" id="reload-code"><i class="ui icon refresh"></i>Apply</button>
</div>
<div id="config-panel">
<div class="ui pointing top attached secondary tabular menu">
<div class="active item" data-tab="tab-init">Initial</div>
<div class="item" data-tab="tab-legend">Legend</div>
<div class="item" data-tab="tab-config">Config</div>
</div>
<div class="ui tab" data-tab="tab-legend">
<div id="legend"></div>
</div>
<div class="ui tab" data-tab="tab-config">
<div class="config" id="current-config"></div>
<div id="addcalls" class="ui icon button" title="Add sequential processes"><i class="add icon"></i></div>
</div>
<div class="ui active tab" data-tab="tab-init">
<div class="config" id="initial-config"></div>
</div>
</div>
</div>
<div id="redex" class="ui right inverted vertical menu sidebar"></div>
<div id="simulation" class="pusher">
<div id="search-bar" class="ui icon mini input">
<input placeholder="Search..." type="text">
<i class="remove circle link icon"></i>
</div>
<div class="ui active dimmer">
<div class="ui text loader">Loading...</div>
</div>
<svg id="graph" class="stargazer-viz"></svg>
</div>
<div id="simulator-controls" class="ui icon buttons">
<div id="toggle-simulation" class="ui icon button" title="Run/Pause"><i class="play icon"></i></div>
<div id="step-simulation" class="ui icon button" title="Pick Reaction"><i class="unordered list icon"></i></div>
<!-- <div id="step-simulation" class="ui icon button" title="Step"><i class="counterclockwise rotated sitemap icon"></i></div> -->
<!-- <div id="speed-control" class="ui icon bottom left pointing dropdown button" title="Speed">
<i class="dashboard icon"></i>
<div class="ui menu">
<a id="faster-speed" class="item" title="Faster"><i class="caret up icon"></i></a>
<div class="item"><small id="speed-val"></small></div>
<a id="slower-speed" class="item" title="Slower"><i class="caret down icon"></i></a>
</div>
</div> -->
<div id="slower-speed" class="ui icon left-half button inessential" title="Slower"><i class="angle double down icon"></i></div>
<div class="ui mid button inessential" title="Speed"><small id="speed-val"></small></div>
<div id="faster-speed" class="ui icon right-half button inessential" title="Faster"><i class="angle double up icon"></i></div>
<div id="source" class="ui icon button" title="Source"><i class="file text icon"></i></div>
<div id="show-globals" class="ui icon button inessential" title="Hide globally free names"><i class="hide icon"></i></div>
<div id="show-labels" class="ui icon button inessential" title="Show labels"><i class="tags icon"></i></div>
<div id="gravity" class="ui active icon button inessential" title="Gravity switch"><i class="magnet icon"></i></div>
<div id="collapse" class="ui icon experimental button inessential" title="Collapse matching"><i class="asterisk icon"></i></div>
<div id="shock" class="ui icon experimental button inessential" title="Collapse matching"><i class="lightning icon"></i></div>
<div id="suite" class="ui floating upward dropdown icon button" title="Code"><i class="code icon"></i><div class="menu"></div></div>
<div id="screenshot" class="ui floating upward dropdown icon button inessential" title="Capture Screenshot">
<i class="camera retro icon"></i>
<div class="menu">
<div class="item" id="take-screenshot">
<i class="blue camera retro icon"></i>
<strong>Take new screenshot</strong>
</div>
</div>
</div>
<div id="open" class="ui icon button" title="Open suite"><i class="folder open icon"></i></div>
<div id="share" class="ui floating upward dropdown icon button" title="Save/Share suite">
<i class="share alternate icon"></i>
<div class="menu">
<a class="item" id="save" title="Save suite" download="program-suite.stargazer">
<i class="download icon"></i>
Download a copy
</a>
<div class="item" id="save-gist">
<i class="alternate github icon"></i>
Save to a new Gist
</div>
<div class="item" id="share-prog">
<i class="linkify icon"></i>
Share as link
</div>
</div>
</div>
<div id="help" class="ui icon button" title="Help"><i class="help icon"></i></div>
<!-- <div id="settings" class="ui icon button" title="Settings"><i class="settings icon"></i></div> -->
</div>
<div class="ui mini modal" id="message-dialog">
<div class="header"></div>
<div class="content"></div>
<div class="actions">
<div onclick="location.reload()" class="ui negative button">Try Reload</div>
<div onclick="location = '?new&showCode=1'" class="ui cancel button">Cancel</div>
</div>
</div>
<div class="ui small modal" id="open-suite">
<i class="dialog close icon"></i>
<div class="header">Open program suite</div>
<div class="content">
<div class="ui info small icon message">
<i class="idea icon"></i>
<i class="close icon"></i>
<div class="content">
<a class="ui blue action button" href="?gist=6e54093b297c0f9df01d0c82f65b89f6">Examples</a>
<div class="header">
Not sure what to do?
</div>
<p>Open the example programs and start playing!</p>
</div>
</div>
<div class="ui header">Open suite from Gist</div>
<div class="from-gist ui fluid search">
<div class="ui labeled action fluid input">
<div class="ui label">
Url/Hash
</div>
<input type="text" class="prompt" placeholder="6e54093b297c0f9df01d0c82f65b89f6">
<button class="ui positive right labeled icon button">
<i class="icon github"></i>
Load
</button>
</div>
<div class="results"></div>
</div>
<!-- <div class="ui horizontal fitted divider"> Or </div> -->
<div class="ui header">Load suite from file</div>
<div class="from-file">
<div class="ui negative message">
<div class="header">
Not supported
</div>
<p>Your browser does not support the File API.</p>
</div>
<div class="ui labeled action fluid input">
<div class="ui label">
File
</div>
<input type="file">
<button class="ui brown right labeled icon button">
<i class="icon open folder"></i>
Open
</button>
</div>
</div>
</div>
<div class="actions">
<a href="?new&showCode=1" class="ui icon labeled blue new button"><i class="plus icon"></i>New empty suite</a>
<div class="ui cancel button">Cancel</div>
</div>
<!-- <div class="ui positive button">Open</div> -->
</div>
</div>
<div class="ui tiny modal" id="share-link-dialog">
<div class="header">
Share this program
</div>
<i class="close icon"></i>
<div class="content">
<div class="ui grid">
<div class="twelve wide column">
<div class="ui action fluid small input">
<input type="text">
<div class="ui basic dropdown button">
<div class="text">All</div>
<i class="dropdown icon"></i>
</div>
</div>
</div>
<div class="four wide column">
<a class="ui facebook icon button" target="_blank">
<i class="facebook icon"></i>
</a>
<a class="ui twitter icon button" target="_blank">
<i class="twitter icon"></i>
</a>
</div>
</div>
</div>
</div>
<div class="ui small modal" id="new-gist-dialog">
<i class="close icon"></i>
<div class="header">
Save suite to Gist
</div>
<div class="ui active dimmer">
<div class="ui text loader">Creating Gist...</div>
</div>
<div class="content">
<div class="ui fluid input icon">
<input type="text">
</div>
</div>
<div class="actions">
<a class="ui icon load labeled blue button"><i class="open folder icon"></i>Load from new Gist</a>
<a class="ui icon open labeled green button" target="_blank"><i class="world icon"></i>Open on GitHub</a>
<div class="ui cancel button">Close</div>
</div>
</div>
<div class="ui modal" id="help-dialog">
<i class="close icon"></i>
<div class="header">
Help
</div>
<div class="content">
<div class="description">
<div class="ui header">Welcome to the Stargazer π-calculus simulator!</div>
<p>Hi! This π-calculus simulator has been brought to you by</p>
<div class="ui blue segment items">
<div class="item">
<div class="content">
<img class="right floated ui tiny image" style="margin-bottom:0pt!important" src="http://www.emanueledosualdo.com/images/portrait-small.jpg" />
<div class="header">Emanuele D'Osualdo</div>
<div class="meta">
<span class="eml gm" onclick="window.open('mailto:' + (['', 'manu', 'l', '.dos'].join('e')) + 'ualdo\x40gm' + (['com','ail'].reverse().join('.')))">emanuele.dosualdo</span>
</div>
<div class="description">
<p>Visit <a href="http://www.emanueledosualdo.com/">emanueledosualdo.com</a> for details.</p>
</div>
</div>
</div>
</div>
<div class="ui message">
<div class="header">License</div>
<p>
<a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">
<img alt="Creative Commons License" class="left floated ui image" style="padding-top:5px" src="https://i.creativecommons.org/l/by-sa/4.0/88x31.png" />
</a>
<span xmlns:dct="http://purl.org/dc/terms/" href="http://purl.org/dc/dcmitype/InteractiveResource" property="dct:title" rel="dct:type">Stargazer</span>
by <a xmlns:cc="http://creativecommons.org/ns#" href="http://emanueledosualdo.com" property="cc:attributionName" rel="cc:attributionURL">Emanuele D'Osualdo</a>
is licensed under a
<a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">Creative Commons Attribution-ShareAlike 4.0 International License</a>.
</p>
<p>
I would appreciate if you contacted me before using the simulator in presentations/other material.
Note that the current version is experimental. A new, open-sourced version will be released at some point.
</p>
</div>
<div class="ui header">How to write a program</div>
<p>
You can use the syntax of π-calculus with the ascii notation:
<ul>
<li>Actions <code>α.P</code>
<ul>
<li>Output: <code>x<y<sub>1</sub>,...,y<sub>n</sub>>.P</code></li>
<li>Input: <code>x(y<sub>1</sub>,...,y<sub>n</sub>).P</code></li>
<li>Internal: <code>tau.P</code></li>
</ul>
</li>
<li>The inactive process: <code>0</code> or <code>zero</code> (it can be omitted after an action: <code>α.zero</code> can be abbreviated <code>α</code>)</li>
<li>Parallel: <code>P | Q</code></li>
<li>Guarded Sum (<code>M</code>):
<code>α<sub>1</sub>.P<sub>1</sub> + … + α<sub>n</sub>.P<sub>n</sub></code>
</li>
<li>Process call: <code>P[y<sub>1</sub>,...,y<sub>n</sub>]</code></li>
<li>Restriction: <code>new y<sub>1</sub>,...,y<sub>n</sub>.P</code></li>
<li>Process definition: <code>P[y<sub>1</sub>,...,y<sub>n</sub>] := M</code></li>
</ul>
</p>
<p>Parentheses can be used to group actions, for example:
<code>x(y).x(z) + x<a></code> is different from
<code>x(y).(x(z) + x<a>)</code>.
</p>
<p>
Your program should have the form
<pre class="ui green segment"><code>INIT<br/>DEFS</code></pre>
Where <code>INIT</code> is a process and <code>DEFS</code>
is a sequence of definitions.
</p>
<p>
You should write <em>normalised</em> programs:
the initial term should not contain sums and only the top-level
of each definition should be a sum.
For example:
<pre class="ui green segment"><code>new x,y.(A[x] | B[x,y])
A[x] := x(u).new z.(A[u] | B[u,x] | C[z,u])
B[x,y] := x<y></code></pre>
is normalised, but
<pre class="ui green segment"><code>new x,y.(A[x] | x<y>)
A[x] := new z.x(u).(A[u] | u<x>| C[z,u])</code></pre>
is not since the initial term contains a sum <code>x<y></code>,
and so does the continuation in the definition of <code>A[x]</code>.
Moreover the definition of <code>A[x]</code> contains a restriction at top level which is not allowed: if you need it there, move it outside in the call of <code>A[x]</code>, otherwise consider if you meant to use it under a prefix.
</p>
<p>Process calls <code>A[x]</code> where <code>A</code> is not defined, will be treated as if the definition was <code>A[x] := 0</code>.</p>
<p>Another important restriction:
the free names of the body of a definition <strong>have to be bound by the definition's head!</strong>
This means that the definition <code>A[x] := x(y).(z<y> | A[y])</code>
is not valid because <code>z</code> occurs free in the body but is not in the argument list. To fix the definition you have to include it as in <code>A[x,z] := x(y).(z<y> | A[y,z])</code>.
</p>
<p>Note that the initial process can contain free names.
They will however be treated as top-level restrictions in displaying the communication topology, unless the "Hide globally free names" (<i class="hide icon"></i>) option is selected.</p>
<div class="ui header">How to use the simulator</div>
<p>Here is an explanation for the controls:</p>
<div class="ui segment">
<div class="ui relaxed list">
<div class="item">
<i class="large play icon"></i>
<div class="content">Runs the simulation by picking random reductions.
</div></div>
<div class="item">
<i class="large unordered-list icon"></i>
<div class="content">Displays the list of available reductions.
Click on a reduction in the list to fire it.
Hovering on reductions will highlight the subjects involved.
</div></div>
<div class="item">
<i class="large angle double down icon"></i>
<i class="large angle double up icon"></i>
<div class="content">Adjust the speed of the simulation.
Clicking on the percentage will restore it to 50%.
</div></div>
<div class="item">
<i class="large file text icon"></i>
<div class="content">Show the code editor panel.
</div></div>
<div class="item">
<i class="large hide icon"></i>
<div class="content">Toggle the visibility of the globally free names (if any).
</div></div>
<div class="item">
<i class="large tags icon"></i>
<div class="content">Toggle the visibility of the labels displaying the names and the process identifiers in the topology.
Hovering on an element will also reveal its complete label.
</div></div>
<div class="item">
<i class="large magnet icon"></i>
<div class="content">Toggle gravity in the layout.
</div></div>
<div class="item">
<i class="large asterisk icon"></i>
<div class="content">Toggle collapse of names selected through search.
Experimental.
</div></div>
<div class="item">
<i class="large add icon"></i>
<div class="content">(Config panel) Add some sequential processes to the current configuration.
The syntax is a parallel composition of process calls.
Any name of the current configuration can be used,
unknown names will be interpreted as new top-level restrictions.
</div></div>
<div class="item">
<i class="large code icon"></i>
<div class="content">Show a list of preloaded examples.
</div></div>
<div class="item">
<i class="large camera retro icon"></i>
<div class="content">Take a screenshot.
Screenshots are vectorial SVG files that will be added to the menu
and can be downloaded by selecting the menu entry.
</div></div>
<div class="item">
<i class="large help icon"></i>
<div class="content">Shows this help.
</div></div>
</div>
</div>
</div>
</div>
</div>
<script src="app.min.js"></script>
</body>
</html>