tutorial.txt
49.9 KB
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
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
SNAKES: a tutorial
==================
////////////////////////////////////////////////////////////////
This file is formatted in order to be processed by AsciiDoc
(http://www.methods.co.nz/asciidoc). It will be more comfortable
to render it or to read the HTML version available at:
http://www.univ-paris12.fr/pommereau/soft/snakes/tutorial.html
////////////////////////////////////////////////////////////////
The first example is a simple coloured Petri net with a single
transition that increments an integer valued (so 0 is the _value_ of
the token, not a number of tokens) token held by a single place, the
incrementation stops when the value is $5$ thanks to a guard on the
transition.
image:tutorial.png[]
To define this net, we must load SNAKES, define a Petri net (lets call
it 'First net'), add the place (called 'p'), add the transition
(called 't') and then connect them with arcs.
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> from snakes.nets import *
>>> n1 = PetriNet('First net')
>>> n1.add_place(Place('p', [0]))
>>> n1.add_transition(Transition('t', Expression('x<5')))
>>> n1.add_input('p', 't', Variable('x'))
>>> n1.add_output('p', 't', Expression('x+1'))
^^^^^^^^^^^^^^^^^^^^^^
On the third line, the net is added a place, which could equivalently
be written as:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> p = Place('p', [0])
>>> n1.add_place(p)
^^^^^^^^^^^^^^^^^^^^^^
However, having a variable for the place is not necessary as it can be
retrieved from $n1$ using its name with $n1.place('p')$.
The instruction $Place('p', [0])$ is the construction of a new
instance of the class $Place$ that expects the name of the place as
its first argument. The second argument is optional and is the initial
marking of the place, that can be given as a list, set, tuple or
multiset of tokens (the class for multisets is defined in the module
$snakes.data$). A third optional argument is a constraint for the
tokens that the place can hold (also known as its type); the default
value allows any token to mark the place. The typing of the places
will be detailed later on.
In order to build the transition, we create an instance of the class
$Transition$ whose constructor expects first the name of the
transition and the, optionally, the guard of it that is true by
default. A guard is otherwise specified as $Expression('...')$ where
$...$ is an arbitrary Python expression, like $Expression('x<5')$ in
our example. We will details latter on how this expression is
evaluated.
Arcs are added using one of the methods $add_input$ or $add_output$ of
$PetriNet$; both expect a place name, a transition name and the arc
annotation as arguments (always in this order). An input arc is
directed from a place toward a transition, an output arc is outgoing a
transition; so arcs are considered from the point of view of the
transition to which they are connected. Valid arc annotations are:
values:: They are instances of the class $Value$ whose constructor
simply expects the value that can be any Python object. For instances,
$Value(1)$ is the integer $1$.
variables:: These are names that are bound to token values when a
transition if executed. A variable is created by instantiating the
class $Variable$ whose constructor expects the name of the variable as
a Python string (valid names are those matching the Python regexp:
$'[a-zA-Z]\w*'$). For instance, $Variable('x')$, $Variable('count')
and $Variable('x_1')$ are valid but $Variable('x-1')$ and
$Variable('1x') are not.
expressions:: They are used to compute new values. An expression is an
instance of the class $Expression$ whose constructor expects any
Python expression as a string. How this expression is evaluated is
explained in the next section. In our example, $Expression('x+1')$ as
been used on the output arc.
tests:: The class $Test$ is used to implement a test arc: it
encapsulates another arc annotation and behaves exactly like it,
except that no token is transported by the arc when the attached
transition fires. The constructor expects another arc annotation as
its sole argument, for instance: $Test(Variable('x'))$ on an input arc
allows to test for a token in a place, its value being usable as $x$.
On a output arc, $Test(Expression('x+1'))$ may be used to test that
the value of $x+1$ is accepted by the connected place, without
actually producing it.
multi-arcs:: When an arc needs to transport several values, the class
$MultiArc$ may be used. Its constructor expects a list (or tuple) of
other annotations that are simultaneously transported on the arc. For
instance, $MultiArc([Variable('x'), Variable('y')])$ on an input arcs
allows to consume two tokens, binding them to the variables $x$ and
$y$.
Executing transitions
---------------------
The first step to execute a transition is to bind the variables
labelling the arcs to actual token values. This is possible by calling
the method $modes()$ of a transition. It returns a list of
$Substitution$ instances (this class is defined in $snakes.data$). A
$Substitution$ is a $dict$-like object that maps variable names to
other variables names or to values. The method $modes$ returns the
list of substitutions that are acceptable in order to fire the
transition, _i.e._, those that respect the usual following conditions:
* each input arc, evaluated through the substitution, corresponds to
a multiset of tokens that is less or equal to the current marking
of the connected place;
* each output arc, evaluated through the substitution, results in a
multiset of tokens that respects the type constraint of the
connected place;
* the guard of the transition, evaluates to $True$ through the
substitution.
For instance, with our net:
[python]
^^^^^^^^^^^^^^^^^^
>>> n1.transition('t').modes()
[Substitution(x=0)]
^^^^^^^^^^^^^^^^^^
The only way to fire the transition is to bind $x$ to $0$. Other may
have been tried, but do not respect at least one of the above
conditions. For instance, choosing $x=1$ respects the guard and place
types but not the marking (the token $1$ is missing):
[python]
^^^^^^^^^^^^^^^^^^
>>> from snakes.data import Substitution
>>> s = Substitution(x=1)
>>> n1.transition('t').enabled(s)
False
^^^^^^^^^^^^^^^^^^
In order to fire a transition, we have to call its method $fire$ with
an enabling substitution as argument (_i.e._, one of those returned by
$modes()$). In our example, we could run:
[python]
^^^^^^^^^^^^^^^^^^
>>> n1.transition('t').fire(Substitution(x=0))
>>> n1.place('p').tokens
MultiSet([1])
^^^^^^^^^^^^^^^^^^
It is important to understand how the firing is performed: the
substitution is used as a Python environment to evaluate the
annotations on the arcs and the guard of the transition in order to
check that the conditions above are respected. For instance, the guard
$Expression('x<5')$ can be evaluated to $true$ because $x$ is bound to
$0$ through the substitution. Similarly, the output arc
$Expression('x+1')$ is evaluated to $1$. The environment used to
evaluate the guard and output arcs is built using the input arcs, this
means that all the variables used during the firing must have been
bound through one of these input arcs. For instance, we could use
$Expression('x<5 and y==x+1')$ for the guard and $Variable('y')$ for the
output arc, and $Substitution(x=0, y=1)$ for the firing:
[python]
^^^^^^^^^^^^^^^^^^
>>> n2 = PetriNet('Second net')
>>> n2.add_place(Place('p', [0]))
>>> n2.add_transition(Transition('t', Expression('x<5 and y==x+1')))
>>> n2.add_input('p', 't', Variable('x'))
>>> n2.add_output('p', 't', Variable('y'))
>>> n2.transition('t').fire(Substitution(x=0, y=1))
>>> n2.place('p').tokens
MultiSet([1])
^^^^^^^^^^^^^^^^^^
This example is correct as long as the substitution is provided by the
user. But the method $modes$ is unable to deduce the value for $y$, it
would require to solve the equation $x<5 and y==x+1$ in the guard.
This is easy here but impossible in general, so, the modes are
computed only with respect to the input arcs. This is why $Expression$
instances are not allowed on input arcs, neither directly nor when
encapsulated in $Test$ or $MultiArc$ instances. So, in this second
example, if we call $modes()$, we get an error since $y$ in cannot be
evaluated:
[python]
^^^^^^^^^^^^^^^^^^
>>> n2.transition('t').modes()
Traceback (most recent call last):
...
NameError: name 'y' is not defined
^^^^^^^^^^^^^^^^^^
Declarations
------------
There is one more aspect about the evaluation of the expression that
should be known: it is possible to declare names that are global to a
Petri net, for instance constants or functions. To do so, we shall use
the method $declare$ of a $PetriNet$ instance, that expects as its
argument a Python statement in a string. This statement is executed
and its effect is remembered in order to be used as a global execution
environment when expressions are evaluated. For instance, lets
construct a Petri net that generates random tokens using the standard
Python function $random.randint$:
[python]
^^^^^^^^^^^^^^^^^^
>>> n3 = PetriNet('Thirs net')
>>> n3.add_place(Place('p', [0]))
>>> n3.add_transition(Transition('t'))
>>> n3.add_input('p', 't', Variable('x'))
>>> n3.add_output('p', 't', Expression('random.randint(0, 100)'))
>>> n3.transition('t').fire(Substitution(x=0))
Traceback (most recent call last):
...
NameError: name 'random' is not defined
^^^^^^^^^^^^^^^^^^
This result is not surprising as the module as not been imported. This
must be made with the statements (the second line is to initialise the
random generator):
[python]
^^^^^^^^^^^^^^^^^^
>>> n3.declare('import random')
>>> n3.declare('random.seed()')
^^^^^^^^^^^^^^^^^^
Then, the transition can fire; of course, the resulting marking will
be different from one execution to another since it is random:
//hide 93
[python]
^^^^^^^^^^^^^^^^^^
>>> n3.transition('t').fire(Substitution(x=0))
>>> n3.place('p').tokens
MultiSet([93])
^^^^^^^^^^^^^^^^^^
The effect of the $n3.declare(statement)$ method is to call $exec
statement in n3.globals$, where $n3.globals$ is a dictionary shared by
all the expression embedded in the net (in guards or arcs). So,
another way to influence the evaluation of these expressions is to
directly assign values to the dictionary $n3.globals$, for instance:
//doc >>> n3.place('p').reset([93])
//hide 18
[python]
^^^^^^^^^^^^^^^^^^
>>> n3.add_place(Place('x'))
>>> n3.add_output('x', 't', Expression('y+1'))
>>> n3.transition('t').fire(Substitution(x=93))
Traceback (most recent call last):
...
NameError: name 'y' is not defined
>>> n3.globals['y'] = 42
>>> n3.transition('t').fire(Substitution(x=93))
>>> n3.get_marking()
Marking({'p': MultiSet([18]), 'x': MultiSet([43])})
^^^^^^^^^^^^^^^^^^
The first error is expected as $y$ as not been declared and is not
bound to any token value through an input arc. After assigning it to
$n3.globals$, it becomes defined so $Expression('y+1')$ can be
evaluated. The same effect could have been achieved using
$n3.declare('y=42')$.
The last instruction gets the marking of the net, lets detail now what
we can do with marking objects.
Markings, marking graph
-----------------------
An instance of $PetriNet$ has methods to get and set its marking,
which are respectively $get_marking$ and $set_marking$. There are also
the methods $add_marking$ and $remove_marking$ to increase or decrease
the current marking.
[NOTE]
========================
The marking of an individual place can also be directly manipulated,
either though its attribute $tokens$ (we used it above) that is a
multiset, or through the following methods:
$add(toks)$:: adds the tokens in $toks$ to the place ($toks$ can be
any collection of values: $set$, $list$, $tuple$, $MultiSet$, ...)
$remove(toks)$:: does just the contrary
$reset(toks)$:: replaces the marking with the tokens in $toks$
$empty()$:: removes all the tokens from the place
$is_empty()$:: returns a Boolean indicating whether the place is empty
or not
========================
A marking is an instance of the class $snakes.nets.Marking$ and is
basically a mapping from place names to multisets of values. It has
been chosen that a marking is independent of any particular Petri net,
so, empty places are not listed in a marking and when assigning a
marking to a net, places that are present in the marking but absent
from the net are simply ignored. Markings can be added with the $+$
operator, subtracted with $-$ or compared with the usual operators
$>$, $<=$, $==$, etc. In order to know the marking of a particular
place, we can use it as a function taking the place name as argument:
[python]
^^^^^^^^^^^^^^^^
>>> m = Marking(p1=MultiSet([1, 2, 3]), p2=MultiSet([5]))
>>> m('p1')
MultiSet([1, 2, 3])
>>> m('p')
MultiSet([])
^^^^^^^^^^^^^^^^
The last result shows that a place that is not listed in a marking is
considered empty, which is consistent with the fact that empty places
are not listed in a marking extracted from a net. If we use the
marking as a $dict$ instead of a function, we will get errors on non
existing places:
[python]
^^^^^^^^^^^^^^^^
>>> m['p1']
MultiSet([1, 2, 3])
>>> m['p']
Traceback (most recent call last):
...
KeyError: 'p'
^^^^^^^^^^^^^^^^
The marking graph of a net can be manipulated using the class
$StateGraph$. Lets take an example to see how it works:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> n4 = PetriNet('Fourth net')
>>> n4.add_place(Place('p', [-1]))
>>> n4.add_transition(Transition('t'))
>>> n4.add_input('p', 't', Variable('x'))
>>> n4.add_output('p', 't', Expression('(x+1) % 5'))
^^^^^^^^^^^^^^^^^^^^^^
This example runs infinitely, incrementing modulo 5 the token in the
place $'p'$. Its markings can be computed using a simple loop:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> while True:
... print n4.get_marking()
... modes = n4.transition('t').modes()
... if len(modes) == 0 :
... break
... n4.transition('t').fire(modes[0])
...
Marking({'p': MultiSet([-1])})
Marking({'p': MultiSet([0])})
Marking({'p': MultiSet([1])})
Marking({'p': MultiSet([2])})
Marking({'p': MultiSet([3])})
Marking({'p': MultiSet([4])})
Marking({'p': MultiSet([0])})
Marking({'p': MultiSet([1])})
^^^^^^^^^^^^^^^^^^^^^^
Unfortunately, this loop runs forever as the net has no deadlock.
Moreover, if in a state there exist several modes, only the first one
will be used in the exploration. To avoid building ourselves the
marking graph, we can use instead:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> s = StateGraph(n4)
>>> s.build()
>>> for state in s :
... print state, s.net.get_marking()
... print " =>", s.successors()
... print " <=", s.predecessors()
...
0 Marking({'p': MultiSet([-1])})
=> {1: (Transition('t', Expression('True')), Substitution(x=-1))}
<= {}
1 Marking({'p': MultiSet([0])})
=> {2: (Transition('t', Expression('True')), Substitution(x=0))}
<= {0: (Transition('t', Expression('True')), Substitution(x=-1)), 5: (Transition('t', Expression('True')), Substitution(x=4))}
2 Marking({'p': MultiSet([1])})
=> {3: (Transition('t', Expression('True')), Substitution(x=1))}
<= {1: (Transition('t', Expression('True')), Substitution(x=0))}
3 Marking({'p': MultiSet([2])})
=> {4: (Transition('t', Expression('True')), Substitution(x=2))}
<= {2: (Transition('t', Expression('True')), Substitution(x=1))}
4 Marking({'p': MultiSet([3])})
=> {5: (Transition('t', Expression('True')), Substitution(x=3))}
<= {3: (Transition('t', Expression('True')), Substitution(x=2))}
5 Marking({'p': MultiSet([4])})
=> {1: (Transition('t', Expression('True')), Substitution(x=4))}
<= {4: (Transition('t', Expression('True')), Substitution(x=3))}
^^^^^^^^^^^^^^^^^^^^^^
The second statement computes the graph, then, for each state, we
print its number, the corresponding marking and successors and
predecessors states that include the state number as well as the
transition (and its mode) that changed the marking. For instance, the
state $1$ can be reached from $0$ or $5$ by firing $'t'$ with $x=-1$
in and $x=4$ respectively.
A marking graph is computed (an thus iterated) in a breadth first
search. It may be iterated before it has been built completely; in
this case, successors states are computed on the fly as each state is
yield by the iteration. However, this results in having wrong
predecessors states as a state not yet explored may lead to one
already visited. This is the case here for the state $5$ that can lead
to $1$ but this is not yet known when we are visiting $1$. This error
is noticeable when the state $1$ is displayed while running:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> s2 = StateGraph(n4)
>>> for state in s2 :
... print state, s2.net.get_marking()
... print " =>", s2.successors()
... print " <=", s2.predecessors()
...
0 Marking({'p': MultiSet([-1])})
=> {1: (Transition('t', Expression('True')), Substitution(x=-1))}
<= {}
1 Marking({'p': MultiSet([0])})
=> {2: (Transition('t', Expression('True')), Substitution(x=0))}
<= {0: (Transition('t', Expression('True')), Substitution(x=-1))}
2 Marking({'p': MultiSet([1])})
=> {3: (Transition('t', Expression('True')), Substitution(x=1))}
<= {1: (Transition('t', Expression('True')), Substitution(x=0))}
3 Marking({'p': MultiSet([2])})
=> {4: (Transition('t', Expression('True')), Substitution(x=2))}
<= {2: (Transition('t', Expression('True')), Substitution(x=1))}
4 Marking({'p': MultiSet([3])})
=> {5: (Transition('t', Expression('True')), Substitution(x=3))}
<= {3: (Transition('t', Expression('True')), Substitution(x=2))}
5 Marking({'p': MultiSet([4])})
=> {1: (Transition('t', Expression('True')), Substitution(x=4))}
<= {4: (Transition('t', Expression('True')), Substitution(x=3))}
^^^^^^^^^^^^^^^^^^^^^^
Finally, it is worth noting that no check is performed in order to
ensure that a marking graph is finite. The method $build$ may run
forever until it fills the computer memory and crash the program.
Moreover, if we use strange constructs like random numbers generators,
the state graph obtained may be partial as the program cannot known
when all the possibilities have been explored.
Places types
------------
The places defined until now did accept any token value in their
marking. It is possible to restrict that by providing a type to place
when it is constructed. A typing system is defined in the module
$typing$ to provide the flexibility for defining any place type. In
this context, a type is understood as a set of values that can be
infinite. Types can be combined to by the usual set operation
(examples are given below). Several basic types are already defined:
$tAll$:: allows any value, this is the type assigned to a constructed
place when no other type is given.
$tNothing$:: is the type with no value.
$tInteger$:: is the type of integer values.
$tNatural$:: is a restriction of $tInteger$ to non-negative values.
$tPositive$:: is a restriction of $tInteger$ to strictly positive
values.
$tFloat$:: is the type of floating point numbers.
$tNumber$:: is the union of $tFloat$ and $tInteger$.
$tString$:: is the type for Python $str$ instances.
$tBoolean$:: is the set holding the two values $False$ and $True$.
$tNone$:: holds the only value $None$.
$tBlackToken$:: holds the only value $dot$ that stands for the usual
Petri net black token.
$tList$:: allows for values that are instances of the Python class
$list$.
$tDict$:: allows for values that are instances of the Python class
$dict$.
$tTuple$:: allows for values that are instances of the Python class
$tuple$.
$tPair$:: is a restriction of $tTuple$ to tuples of length 2.
The module typing also provides with type constructors, allowing to
create new types. Moreover, types can be combined using various
operators, for instance, the module $typing$ makes the following
definitions:
[python]
^^^^^^^^^^^^^^^^^
tInteger = Instance(int)
# an instance of int
tNatural = tInteger & GreaterOrEqual(0)
# an instance of int and a value greater than or equal to zero
tPositive = tInteger & Greater(0)
# an instance of int and a value strictly positive
tFloat = Instance(float)
tNumber = tInteger|tFloat
# an instance of int or of float
tBoolean = OneOf(False, True)
# one value of False and True
tNone = OneOf(None)
# only the value None
tBlackToken = OneOf(dot)
# only the value dot
tTuple = Tuple(tAll)
# an instance of tuple holding any value
tPair = Tuple(tAll, min=2, max=2)
# an instance of tuple holding exactly two items of any type
^^^^^^^^^^^^^^^^^
A type can be called as a function in which case it returns $True$ if
all its argument belong to the type and $False$ otherwise, for
instance:
[python]
^^^^^^^^^^^^^^^^^
>>> from snakes.typing import *
>>> tNatural(2, 3, 4, 0)
True
>>> tNatural(-1)
False
^^^^^^^^^^^^^^^^^
When a place is constructed a third argument can be given to define
its type. If later on a token that does not respect the type is added
to the place, an exception is raised.
[python]
^^^^^^^^^^^^^^^^^
>>> from snakes.typing import *
>>> tNatural(2)
True
>>> tNatural(-1)
False
>>> p = Place('p', [0, 1, 2, 3], tNatural)
>>> p.add(3)
>>> p.tokens
MultiSet([0, 1, 2, 3, 3])
>>> p.add(-1)
Traceback (most recent call last):
...
ValueError: forbidden token '-1'
^^^^^^^^^^^^^^^^^
When no type is given at construction time, $tAll$ is actually used,
which explains why a place accepts any token by default.
Plugins
-------
A system a plugins allow to extend SNAKES. In order to plug the module
$foo$ into the module $snakes.nets$, one as to use:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^^
import snakes.plugins
snakes.plugins.load('snakes.plugins.foo', 'snakes.nets', 'my_nets')
^^^^^^^^^^^^^^^^^^^^^^^
Intuitively, this (correct) statements have the effect of the
(incorrect) statement:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^^
import 'snakes.nets extended by snakes.plugins.foo' as my_nets
^^^^^^^^^^^^^^^^^^^^^^^
So, one could now use:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^^
from my_nets import *
^^^^^^^^^^^^^^^^^^^^^^^
Several plugins may be loaded at the same time:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^^
snakes.plugins.load(['snakes.plugins.foo, 'snakes.plugins.bar],
'snakes.nets', 'my_nets')
^^^^^^^^^^^^^^^^^^^^^^^
This has the effect to load the plugin $foo$ on the top of
$snakes.nets$ resulting in a module on the top of which $bar$ is then
loaded.
=== Giving positions to the nodes
The plugin $snakes.plugins.pos$ is a very simple one that allows to
give _x_/_y_ positions to the nodes of a Petri net.
First we load the plugin:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> import snakes.plugins
>>> snakes.plugins.load('snakes.plugins.pos', 'snakes.nets', 'nets')
<module 'nets' from '...'>
>>> from nets import PetriNet, Place, Transition
^^^^^^^^^^^^^^^^^^^^^^
A place can be added without specifying a position for it, in which
case it will be positioned at $(0,0)$. The position is stored in an
attribute $pos$ of the place as well as in $pos.x$ and $pos.y$:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> n = PetriNet('N')
>>> p = Place('p00')
>>> n.add_place(p)
>>> p.pos
Position(0, 0)
>>> p.pos.x, p.pos.y
(0, 0)
^^^^^^^^^^^^^^^^^^^^^^
The position can be defined when the node is created or when it is
added to a net.
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> t10 = Transition('t10', pos=(1, 0))
>>> n.add_transition(t10)
>>> t10.pos
Position(1, 0)
>>> t = Transition('t01')
>>> t.pos
Position(0, 0)
>>> n.add_transition(t, pos=(0, 1))
>>> t.pos
Position(0, 1)
^^^^^^^^^^^^^^^^^^^^^^
The last statement above shows that the node is copied when added to a
net and thus $t$ keeps its position $(0,0)$ but its copy in $n$ as
been positioned at $(0,1)$.
Nodes can be moved using the $shift$ or $moveto$ method, but not by
directly assigning their attributes $pos.x$ of $pos.y$:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> t = n.transition('t01')
>>> t.pos
Position(0, 1)
>>> t.pos.moveto(1, 2)
>>> t.pos
Position(1, 2)
>>> t.pos.shift(1, -1)
>>> t.pos
Position(2, 1)
>>> t.pos.x = 0
Traceback (most recent call last):
...
AttributeError: readonly attribute
^^^^^^^^^^^^^^^^^^^^^^
A net extended by $snakes.plugins.pos$ has a method to compute its
bounding box that is a tuple $((xmin, ymin), (xmax, ymax))$ where
$xmin$ is the $x$ coordinate of the left-most node, and so on. A
method $shift$ also allows to shift all the nodes of the net and a
method $transpose$ rotates a whole net by 90° (_i.e._, the top-down
direction becomes the left-right).
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> n.bbox()
((0, 0), (2, 1))
>>> n.shift(10, 10)
>>> n.bbox()
((10, 10), (12, 11))
>>> t.pos
Position(12, 11)
>>> n.transpose()
>>> t.pos
Position(-11, 12)
>>> n.bbox()
((-11, 10), (-10, 12))
^^^^^^^^^^^^^^^^^^^^^^
Finally, notice that when nodes are merged, the position of the result
can be defined by giving an argument $pos$ to the $merge_transitions$
or $merge_places$ method. If no such argument is given, the position
of the new node is computed as the barycentre of the positions of the
merged nodes.
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> n.merge_transitions('t11', ['t01', 't10'], pos=(1,1))
>>> n.transition('t11').pos
Position(1, 1)
>>> n.transition('t01').pos
Position(-11, 12)
>>> n.transition('t10').pos
Position(-10, 11)
>>> n.merge_transitions('t', ['t01', 't10'])
>>> n.transition('t').pos
Position(-10.5, 11.5)
^^^^^^^^^^^^^^^^^^^^^^
=== Drawing nets and marking graphs
The plugin $graphviz$ can be used in order to produce a graphical
rendering of $PetriNet$ and $StateGraph$ objects. It add to them a
method $draw$ that saves a picture in various formats (those supported
by http://www.graphviz.org[GraphViz]), in particular: PNG, JPEG, EPS,
DOT. For a Petri net, the positions of the nodes is fixed using the
plugin $pos$ (that is automatically loaded). For a stage graph, the
nodes are automatically positioned by GraphViz.
[WARNING]
===========================
In order to produce a graphical rendering in a format other than DOT,
the plugin $graphviz$ calls the program $dot$ or $neato$. It is
possible that a specially crafted file name will result in executing
arbitrary commands on the system. So, take care when you run a SNAKES
script that you did not program yourself. (In general, take care when
your run any script from an unsafe source.)
===========================
Let's consider a simple example:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> import snakes.plugins
>>> snakes.plugins.load('snakes.plugins.graphviz', 'snakes.nets', 'nets')
<module 'nets' from '...'>
>>> from nets import *
>>> n = PetriNet('N')
>>> n.add_place(Place('p00', [0]))
>>> n.add_transition(Transition('t10', pos=(1, 0)))
>>> n.add_place(Place('p11', pos=(1, 1)))
>>> n.add_transition(Transition('t01', pos=(0, 1)))
>>> n.add_input('p00', 't10', Variable('x'))
>>> n.add_output('p11', 't10', Expression('(x+1) % 3'))
>>> n.add_input('p11', 't01', Variable('y'))
>>> n.add_output('p00', 't01', Expression('(y+2) % 4'))
>>> n.draw('graphviz-net.png')
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This produces the following picture:
image:graphviz-net.png[GraphViz net]
The rendering is not very beautiful but should be useful in many
cases. Transitions are labelled with their name and guard, places with
their marking (inside), name and type (top-right), arcs are labelled
with their inscription. The picture format is chosen using the
extension of the created file: $.png$, $.jpg$, $.eps$, $.dot$...
The marking graph can then be built and drawn also:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> s = StateGraph(n)
>>> s.draw('graphviz-graph.png', landscape=False)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Which produces the picture:
image:graphviz-graph.png[GraphViz stage graph]
Each state is labelled with its number and the corresponding marking,
arcs are labelled by the transition and binding that produce one
marking from another.
Notice that the option $landscape$ has been used in order to ask
GraphViz to produce a vertical layout (it is horizontal by default).
Other options exist, given here with their default value:
$scale=72.0$:: a scale factor for the whole picture. The greater it is,
the larger will be the space between the nodes. This option applies to
both $PetriNet.draw$ and $StateGraoh.draw$.
$nodesize=0.5$:: the size of the nodes (places, transitions or
states). The greater it is, the wider the nodes are. This option
applies to both $PetriNet.draw$ and $StateGraoh.draw$.
$engine$:: the rendering program to use (one of $"neato"$, $dot$,
$"circo"$, $"twopi"$, $"fdp"$). The default for $PetriNet$ objects is
$"neato"$, the default for $StateGraph$ objects is $dot$.
$layout=False$:: for $PetriNet.draw$ only, controls whether the
rendering program is allowed to move nodes or not. This only works for
$"neato"$, other programs are always allowed to move nodes.
$print_state=None$:: for $StateGraph.draw$ only, defines the text
printed inside each state. If $None$, the number of the state is
printed with the corresponding marking. Otherwise, a function should
be provided, taking the state number as its first argument and the
state graph as its second argument, and returning the string to print.
$print_arc=None$:: for $StateGraph.draw$, similarly to $print_state$,
defines the text printed on the arcs. The function to provide must
take five arguments: the source state, the target state, the name of
the transition fired, its mode (_i.e._ the substitution used), and the
state graph. For $PetriNet.draw$, the function must take five
arguments: the label of the arc, the place connected to it, the
transition connected to it, a Boolean indicating whether this is an
input (if $True$) or output arc (if $False$) and the Petri net.
$print_trans=None$:: for $PetriNet.draw$ only, the function should
take as arguments the transition and the net.
$print_place=None$:: for $PetriNet.draw$ only, the function should
take as arguments the place and the net. This corresponds to the label
that is drawn outside of the place.
$print_tokens=None$:: for $PetriNet.draw$ only, the function should
take as arguments the multiset of tokens, the place and the net. This
corresponds to the label that is drawn inside the place.
=== Merging nodes using name-based rules
The plugin $status$ extends Petri nets nodes with an attribute called
$status$ that is composed of a _name_ and _value_. The former
corresponds to a class of similar statuses (_e.g._, $entry$,
$internal$, $exit$, $buffer$ or $tick$) and the latter to a particular
subset of this class. The idea is to be able to merge nodes that have
the same status (name and value). Each status uses its own merge rule.
[NOTE]
====================
The principle of places status is well known in PBC and M-nets, see
for instance the paper
http://www.univ-paris12.fr/lacl/pommereau/publis/2003-fi.html[Asynchronous
Box Calculus] where they are used in order to perform compositions
of Petri net. The plugin extends this notion to transitions.
====================
For instance, the plugin defines a function $buffer(id)$ that creates
a status $('buffer', id)$. If several places with the status $buffer$
and the same $id$ are present in the net, they can be automatically
merged. Concretely, let's define a net wit three buffer places:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^
>>> import snakes.plugins
>>> snakes.plugins.load('snakes.plugins.status', 'snakes.nets', 'nets')
<module 'nets' from ...>
>>> from nets import *
>>> import snakes.plugins.status as status
>>> n = PetriNet('N')
>>> n.add_place(Place('p1', [1], status=status.buffer('foo')))
>>> n.add_place(Place('p2', [2]), status=status.buffer('foo'))
>>> n.add_place(Place('p3', [3]), status=status.buffer('bar'))
>>> n.add_place(Place('p4', [4]))
^^^^^^^^^^^^^^^^^^^^^^^^
Notice that the status can be assigned when the place is created (as
for $p1$) or when it is added to the net (as for $p2$ and $p3$). A
status has not been specified for $p4$ that thus receives the empty
status $(None, None)$.
It is now possible to list all the places that have the same status:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.status(status.buffer('foo'))
('p2', 'p1')
>>> n.status(status.buffer('bar'))
('p3',)
^^^^^^^^^^^^^^^^^^^^^^^^
Moreover, it is possible to merge the places that have the same
status:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.status.merge(status.buffer('foo'))
>>> n.place()
[Place('p3', MultiSet([3]), tAll, status=Buffer('buffer','bar')),
Place('(p1+p2)', MultiSet([1, 2]), tAll, status=Buffer('buffer','foo')),
Place('p4', MultiSet([4]), tAll)]
^^^^^^^^^^^^^^^^^^^^^^^^
The places $p1$ and $p2$ has been merged (and then removed), yielding
a place $p1+p2$ whose marking is the sum of the marking of $p1$ and
$p2$. This treatment of the marking is specific to buffer status,
other status may use other methods.
A Petri net is also enriched with a method in order to change the
status of a node:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.set_status('(p1+p2)', status.buffer(None))
>>> n.place()
[Place('p3', MultiSet([3]), tAll, status=Buffer('buffer','bar')),
Place('(p1+p2)', MultiSet([1, 2]), tAll, status=Buffer('buffer')),
Place('p4', MultiSet([4]), tAll)]
^^^^^^^^^^^^^^^^^^^^^^^^
A buffer status with a value $None$ is particular in that it will be
ignored by $PetriNet.status.merge$ ans thus not merged (it is a
private buffer).
One may have noticed that buffer status are actually instances of the
class $Buffer$ that is itself a subclass of $Status$. In order to
create a status, one just has to extend the class $Status$ and
redefine the method $merge$ (with its arguments as below), for example
the $Buffer$ class is defined as:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^^^
class Buffer (Status) :
def merge (self, net, nodes, name=None) :
# net: the net in which the merge occurs
# nodes: the nodes to merge
# name: the name of the resulting node
if self._value is None :
return # private buffers are ignored
if name is None : # create a name if none has been given
name = "(%s)" % "+".join(sorted(nodes))
net.merge_places(name, nodes, status=self) # merge the places
for src in nodes : # remove the merged places
net.remove_place(src)
^^^^^^^^^^^^^^^^^^^^^^^^
[NOTE]
==========================
Using this class $Buffer$, a helper function $buffer$ is defined as:
//skip
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
def buffer (name) :
return Buffer('buffer', name)
^^^^^^^^^^^^^^^^^^^^^^^^^^
==========================
The plugin defines other statuses:
$variable(id)$:: is similar to $buffer$ except that when places are
merged, they must all have the same marking. So, $variable$ places are
like variables in a program that store a single value (possibly
structured).
$tick(id)$:: is a transition status. When $tick$ transitions are
merged, their guards are and-ed.
$entry$, $internal$ and $exit$:: are the traditional place status
allowing to define control flow operations between Petri nets in PBC
and its successors.
=== PBC/M-nets control flow operations
The plugin $ops$ defines the control flow operations usually defined
for PBC and M-nets. To do so, it relies on places status (the plugin
$status$ is automatically loaded) and in particular on the $entry$,
$internal$ and $exit$ statuses. Indeed, it is expected that a Petri
net starts its execution with one token in each entry place (entry
marking) and evolves until it reaches a marking with one token in each
exit place (exit marking). In order to produce the expected control
flow, the operations use combinations of the entry and exit places of
the composed nets. All the details about these operations can be found
in the paper
http://www.univ-paris12.fr/lacl/pommereau/publis/2003-fi.html[Asynchronous
Box Calculus].
[NOTE]
======================
There are basically two approaches for such combinations. The PBC
approach relies on cross-products of sets of places with simple types
(low-level places). This has the advantage to be simple but may
produce a large number of places. On the other hand, the M-nets
approach relies on building fewer high-level places whose type are
cross-products of the types of the combined places (this is a
simplification). This has the advantage to produce less places than
in PBC but their types are very complicated and the resulting transition
rule is hard to implement (it is necessary to match tree-structured
tokens against tree-structures annotations). Because of this
complexity, we have chosen to implement to PBC approach which is also
what is used in the most recent models of the family.
======================
The plugin defines four control flow operations. Let $n1$ and $n2$ be
two nets:
* the _sequence_ $n1 & n2$ is obtained by combining the exit places
of $n1$ with the entry places of $n2$ so that when $n1$ reaches its
exit marking, it corresponds to the entry marking of $n2$. As a
result, $n1$ is executed first and is followed by the execution of
$n2$;
* the _choice_ $n1 + n2$ combines the entry places of $n1$ and $n2$
on the one hand, and their exit places on the other hand. As a
result, either $n1$ or $n2$ is executed and they have the same exit
marking;
* the _iteration_ $n1 * n2$ combines the entry and exit places of
$n1$ with the $entry$ places of $n2$. As a result, $n1$ can be
executed an arbitrary number of time (including zero) and is
followed by one execution of $n2$;
* the _parallel_ composition $n1 | n2$ does not combine any place so
that $n1$ and $n2$ can evolve concurrently.
When two nets are combined using one of these operators, their nodes
are automatically merged according to their status, in particular:
buffer or variables places, and tick transitions are merged using the
method that is defined by each status.
Two operations that are not related to control flow are also defined:
* the node hiding $n1.hide(old)$ gives the empty status to all the
nodes in $n1$ that used to have the status $old$ before. It may be
called with a second argument in order to choose the new status.
For instance $n1.hide(buffer('foo'), buffer(None))$ makes private
all the buffer places with the status $('buffer', 'foo')$;
* a variant of the node hiding is $n1 / val$. Its right argument must
be a status value, the result is a copy of $n1$ in which all the
nodes with a status $(x,val)$ are given the status $(x,None)$.
This has the effect to disable further merges of, _e.g._, buffer
places if the net is later combined with another one.
The plugin $posops$ is a combination of $pos$ and $ops$ that tries to
take into account the positions of the nodes when nets are composed.
It avoids overlapping the composed nets and tries to distribute evenly
the combined places in order to have a acceptable result (as far as
possible). Let's see it in action:
[python]
^^^^^^^^^^^^^^^^^^^^^^
>>> import snakes.plugins
>>> snakes.plugins.load(['snakes.plugins.posops', 'snakes.plugins.graphviz'], 'snakes.nets', 'nets')
<module 'nets' from ...>
>>> from nets import *
>>> from snakes.plugins.status import entry, internal, exit, safebuffer
>>> n = PetriNet('basic')
>>> n.add_place(Place('e', status=entry, pos=(0, 2)))
>>> n.add_place(Place('x', status=exit, pos=(0, 0)))
>>> n.add_transition(Transition('t', pos=(0, 1)))
>>> n.add_input('e', 't', Value(dot))
>>> n.add_output('x', 't', Value(dot))
>>> n.add_place(Place('v', [0], status=safebuffer('var'), pos=(1,1)))
>>> n.add_input('v', 't', Variable('x'))
>>> n.add_output('v', 't', Expression('x+1'))
>>> n.draw('basic.png')
^^^^^^^^^^^^^^^^^^^^^^
This basic net is as follows:
image:basic.png[Basic net]
It can be composed with itself in order to produce a more complex net,
for instance:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> complex = n & (n * (n + n))
>>> var = complex.status(safebuffer('var'))[0]
>>> complex.place(var).pos.moveto(-1,-1)
>>> complex.draw('complex.png', scale=60)
^^^^^^^^^^^^^^^^^^^^^^^^^^
On the second line, the new name of the variable place is retrieved
from its status. Then the place is moved in order to have a prettier
result:
image:complex.png[Complex net]
=== PBC/M-nets synchronisation
Another important operation featured by the models in the PBC and
M-nets family is the synchronization. This operation is similar to the
CCS synchronization but operates on multi-actions (_i.e_, several
synchronizations may take place at the same transition). In PBC,
actions have no parameters while the have in M-nets (which implies the
unification of these parameters). With respect to CCS, the
synchronization is here a static operation that builds all the
possible transitions corresponding to synchronized actions. The plugin
$synchro$ implements a generalisation of the M-nets synchronisation.
It is generalised in that it does not impose a fixed arity associated
to each action name. For more information about M-nets
synchronisation, see for instance the section 4 of the paper
http://www.univ-paris12.fr/lacl/pommereau/publis/2002-mtcs.html[Petri
nets with causal time for system verification].
Let's consider a simple example: three transitions have to
synchronize, doing so, one transition can receive a value from each
other transition. To do this with SNAKES, one may run the following
code:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> import snakes.plugins
>>> snakes.plugins.load(['snakes.plugins.synchro', 'snakes.plugins.graphviz'], 'snakes.nets', 'nets')
<module 'nets' from ...>
>>> from nets import *
>>> from snakes.plugins.synchro import Action
>>> n = PetriNet('N')
>>> n.add_place(Place('e1', [dot], pos=(0,2)))
>>> n.add_place(Place('e2', [dot], pos=(1,2)))
>>> n.add_place(Place('e3', [dot], pos=(2,2)))
>>> n.add_place(Place('x1', [], pos=(0,0)))
>>> n.add_place(Place('x2', [], pos=(1,0)))
>>> n.add_place(Place('x3', [], pos=(2,0)))
>>> n.add_transition(Transition('t1', pos=(0,1),
... actions=[Action('a', True, [Value(2)])]))
>>> n.add_transition(Transition('t2', pos=(1,1),
... actions=[Action('a', False, [Variable('x')]),
... Action('a', False, [Variable('y')])]))
>>> n.add_transition(Transition('t3', pos=(2,1),
... actions=[Action('a', True, [Value(3)])]))
>>> n.add_input("e1", "t1", Value(dot))
>>> n.add_input("e2", "t2", Value(dot))
>>> n.add_input("e3", "t3", Value(dot))
>>> n.add_output("x1", "t1", Value(dot))
>>> n.add_output("x2", "t2", Value(dot))
>>> n.add_output("x3", "t3", Value(dot))
>>> def pt (trans, net) :
... return "%s\\n%s" % (trans.name, str(trans.actions))
>>> n.draw('synchro-1.png', print_trans=pt)
^^^^^^^^^^^^^^^^^^^^^^^^^^
The resulting picture is the following:
image:synchro-1.png[Before synchronisation]
Applying the synchronisation is possible by calling the method
$synchronise$ that expects an action name as parameter. The code below
performs the synchronisation then draws the net with a new layout in
order to make it more readable (by default, a synchronised transition
is place in the middle of the transition that participated to the
synchronisation).
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.synchronise('a')
>>> n.draw('synchro-2.png', print_trans=pt, layout=True, engine='circo')
^^^^^^^^^^^^^^^^^^^^^^^^^^
image:synchro-2.png[After synchronisation]
The result is not really readable, but let's see what happened:
- $t1$ has two ways to synchronise with $t2$, which results in
building two transitions, that still hold one receive action $a$;
- this is the same for $t3$ and $t2$, we have so far created 4 new
transitions;
- then, both $t1$ and $t3$ can synchronise with the 4 new
transitions, which results in 8 new transitions.
So their are now 15 transitions in the net. The names of the new
transitions correspond to how they were obtained. For instance, the
one on the left of $x1$ (on the top) has the name
$(t1{x->2}+t2{x->2}[a(2)]$, which means that is was obtained from the
synchronisation of $t1$ and $t2$ for which the variable $x$ was bound
to $2$ (the two substitutions are the way to unify the synchronised
actions) that communicated the value $2$ on the action $a$.
It may be observed that only the last 8 transitions correspond to the
full synchronisation of $t2$ with both $t1$ and $t3$ (and each of
these 8 transition corresponds to one way of achieving the
synchronisation, some being equivalent). But if the net is executed,
it is possible to fire $t1$, $t2$, $t3$ or any of the partially
synchronised transitions. In order to force the execution of the full
synchronisation, one can call the method $restrict$ that remove all
the transitions that still hold an action $a$. Most of time, a
restriction always follows a synchronisation; so, there is also a
method $scope$ that perform both in turn.
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.restrict('a')
>>> n.draw('synchro-3.png', print_trans=pt, layout=True, engine='circo')
^^^^^^^^^^^^^^^^^^^^^^^^^^
This results in the following picture where only 8 transitions are
remaining:
image:synchro-3.png[After restriction]
On this last picture, one may notice that some transitions consume or
produce two tokens. This is the case for instance for the top-left
transition that results from the synchronisation of $t1$ with $t2$
which was then synchronised again with $t1$. In a model of safe or
colour-safe Petri nets like PBC or M-nets, this is a dead transition
that could be removed. This can be made easily with the following
code, resulting in the picture below:
[python]
^^^^^^^^^^^^^^^^^^^^^^^
>>> for trans in n.transition() :
... for place, label in trans.pre.items() :
... if label == MultiArc([Value(dot), Value(dot)]) :
... n.remove_transition(trans.name)
... break
>>> n.draw('synchro-4.png', print_trans=pt, layout=True, engine='circo')
^^^^^^^^^^^^^^^^^^^^^^^
image:synchro-4.png[After removing the dead transitions]
It may be interesting also to remove the duplicated transitions, but
this is beyond the scope of this tutorial.
=== Representing infinite data domains
[NOTE]
=======================
This section describes the implementation that corresponds to the
paper
http://www.univ-paris12.fr/lacl/pommereau/publis/2007-infinity.html[Efficient
reachability graph representation of Petri nets with unbounded
counters]. The only difference with respect to the paper is that
SNAKES is not limited to P/T nets but happily handles high-level nets
together with Lash data. The rest of the section uses the example
developed in the paper, taking $omega=8$.
=======================
The first thing to do is to load the plugin $lashdata$ do that we are
able to store data in Lash, we also import load $graphviz$ in order to
draw the resulting graphs:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> import snakes.plugins
>>> nets = snakes.plugins.load(["snakes.plugins.graphviz",
... "snakes.plugins.lashdata"],
... "snakes.nets", "nets")
>>> from nets import *
>>> from snakes.typing import *
>>> from snakes.data import *
>>> from snakes.plugins.lashdata import Data
^^^^^^^^^^^^^^^^^^^^^^^^^^
$Data$ is a class that allows to store integer variables into Lash.
This library actually store data under the form of sets of vectors of
integers but the class $Data$ hides this under the usual concept of
variables. When we build a Petri net, we must give a $lash$ argument
that is one instance of $Data$. Its constructor simply takes a list of
variables with their initial values:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> n = PetriNet("N", lash=Data(x=0))
^^^^^^^^^^^^^^^^^^^^^^^^^^
Then we add the places:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.add_place(Place("s_1", [dot], tBlackToken, pos=(0, 0)))
>>> n.add_place(Place("s_2", [], tBlackToken, pos=(2, 0)))
^^^^^^^^^^^^^^^^^^^^^^^^^^
And last the transitions. Each transition is given a $condition$ under
the form of a linear Python expression ($or$, $not$ nor $=!$ allowed).
An $update$ is also provided in order to modify the variables, this a
single assignment of one variable with a linear expression (several
assignment may be combined using $;$).
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> n.add_transition(Transition("t_3", pos=(1, -1)),
... condition="x<8",
... update="x=x+1")
>>> n.add_input("s_2", "t_3", Value(dot))
>>> n.add_output("s_1", "t_3", Value(dot))
>>> n.add_transition(Transition("t_2", pos=(1, 1)),
... condition="x>0", update="x=x-1")
>>> n.add_input("s_1", "t_2", Value(dot))
>>> n.add_output("s_2", "t_2", Value(dot))
>>> n.add_transition(Transition("t_5", pos=(3, 1)),
... condition="x>0", update="x=x-1")
>>> n.add_input("s_2", "t_5", Value(dot))
>>> n.add_output("s_2", "t_5", Value(dot))
>>> n.add_transition(Transition("t_4", pos=(3, -1)),
... condition="x<8",
... update="x=x+1")
>>> n.add_input("s_2", "t_4", Value(dot))
>>> n.add_output("s_2", "t_4", Value(dot))
>>> n.add_transition(Transition("t_1", pos=(-1, 0)),
... condition="x<4",
... update="x=x+1")
>>> n.add_input("s_1", "t_1", Value(dot))
>>> n.add_output("s_1", "t_1", Value(dot))
^^^^^^^^^^^^^^^^^^^^^^^^^^
Then, we can build four different marking graph. The first one is the
full, usual, marking graph:
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> m = StateGraph(n)
>>> m.build()
>>> def ps (state, graph) :
... return str(state)
>>> def pa (source, target, trans, mode, graph) :
... return trans
>>> m.draw("lash-full.png", landscape=True, print_state=ps, print_arc=pa)
^^^^^^^^^^^^^^^^^^^^^^^^^^
That results in the following picture:
image:lash-full.png[Full marking graph]
Then come the compact graphs. First we can ask SNAKES to add a meta
transition for each detected side-loop (a transition that does not
change the marking).
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> m = StateGraph(n, loops=True)
>>> m.build()
>>> m.draw("lash-loops.png", landscape=True, print_state=ps, print_arc=pa)
^^^^^^^^^^^^^^^^^^^^^^^^^^
That results in:
image:lash-loops.png[First compact marking graph]
We can then ask to add a meta transition when cycles are detected (a
new state that covers an existing one). We can further ask to remove
states that are covered when cycles are detected.
[python]
^^^^^^^^^^^^^^^^^^^^^^^^^^
>>> m = StateGraph(n, cycles=True)
>>> m.build()
>>> m.draw("lash-cycles.png", landscape=True, print_state=ps, print_arc=pa)
>>> m = StateGraph(n, remove=True)
>>> m.build()
>>> m.draw("lash-remove.png", landscape=True, print_state=ps, print_arc=pa)
^^^^^^^^^^^^^^^^^^^^^^^^^^
In this particular example, exploiting cycles results in
link:lash-cycles.png[the same graph as above], but with the $remove$
option, we get a more compact graph:
image:lash-remove.png[The most compact graph]
Finally, note that using the $cycles$ option automatically turns on
the $loops$ option, and using the $remove$ option turns on the
$cycles$ option (and thus also the $loops$ one).
Exporting to PNML and other formats
-----------------------------------
To do...
Writing a plugin
----------------
To do...