← Back to branch summary

~tapaal-ltl/verifypn/rule-D-fix

« back to all changes in this revision

Viewing changes to test_models/discrete-test005/model.pnml

  • Committer: Peter G. Jensen
  • Date: 2020-07-03 09:19:50 UTC
  • mto: This revision was merged to the branch mainline in revision 225.
  • Revision ID: root@petergjoel.dk-20200703091950-0wdbe4bezt4obe0t
added simple test-script and test models

Show diffs side-by-side

added added

removed removed

Lines of Context:
test_models/discrete-test005/model.pnml
 
1
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
 
2
<pnml xmlns="http://www.pnml.org/version-2009/grammar/pnml">
 
3
    <net id="ComposedModel" type="http://www.pnml.org/version-2009/grammar/ptnet">
 
4
        <page id="page0">
 
5
            <place id="T1_P0">
 
6
                <graphics>
 
7
                    <position x="570" y="120"/>
 
8
                </graphics>
 
9
                <name>
 
10
                    <graphics>
 
11
                        <offset x="-5" y="35"/>
 
12
                    </graphics>
 
13
                    <text>T1_P0</text>
 
14
                </name>
 
15
                <initialMarking>
 
16
                    <text>1</text>
 
17
                </initialMarking>
 
18
            </place>
 
19
            <place id="T1_P1">
 
20
                <graphics>
 
21
                    <position x="210" y="540"/>
 
22
                </graphics>
 
23
                <name>
 
24
                    <graphics>
 
25
                        <offset x="-5" y="35"/>
 
26
                    </graphics>
 
27
                    <text>T1_P1</text>
 
28
                </name>
 
29
                <initialMarking>
 
30
                    <text>1</text>
 
31
                </initialMarking>
 
32
            </place>
 
33
            <place id="T1_DoneP">
 
34
                <graphics>
 
35
                    <position x="585" y="540"/>
 
36
                </graphics>
 
37
                <name>
 
38
                    <graphics>
 
39
                        <offset x="-5" y="35"/>
 
40
                    </graphics>
 
41
                    <text>T1_DoneP</text>
 
42
                </name>
 
43
                <initialMarking>
 
44
                    <text>0</text>
 
45
                </initialMarking>
 
46
            </place>
 
47
            <place id="C1_P0">
 
48
                <graphics>
 
49
                    <position x="1395" y="240"/>
 
50
                </graphics>
 
51
                <name>
 
52
                    <graphics>
 
53
                        <offset x="-5" y="35"/>
 
54
                    </graphics>
 
55
                    <text>C1_P0</text>
 
56
                </name>
 
57
                <initialMarking>
 
58
                    <text>1</text>
 
59
                </initialMarking>
 
60
            </place>
 
61
            <place id="C1_P1">
 
62
                <graphics>
 
63
                    <position x="1410" y="345"/>
 
64
                </graphics>
 
65
                <name>
 
66
                    <graphics>
 
67
                        <offset x="-5" y="35"/>
 
68
                    </graphics>
 
69
                    <text>C1_P1</text>
 
70
                </name>
 
71
                <initialMarking>
 
72
                    <text>1</text>
 
73
                </initialMarking>
 
74
            </place>
 
75
            <place id="C1_P2">
 
76
                <graphics>
 
77
                    <position x="1380" y="435"/>
 
78
                </graphics>
 
79
                <name>
 
80
                    <graphics>
 
81
                        <offset x="-5" y="35"/>
 
82
                    </graphics>
 
83
                    <text>C1_P2</text>
 
84
                </name>
 
85
                <initialMarking>
 
86
                    <text>1</text>
 
87
                </initialMarking>
 
88
            </place>
 
89
            <place id="C1_P3">
 
90
                <graphics>
 
91
                    <position x="1725" y="345"/>
 
92
                </graphics>
 
93
                <name>
 
94
                    <graphics>
 
95
                        <offset x="-5" y="35"/>
 
96
                    </graphics>
 
97
                    <text>C1_P3</text>
 
98
                </name>
 
99
                <initialMarking>
 
100
                    <text>0</text>
 
101
                </initialMarking>
 
102
            </place>
 
103
            <place id="C1_P4">
 
104
                <graphics>
 
105
                    <position x="2040" y="390"/>
 
106
                </graphics>
 
107
                <name>
 
108
                    <graphics>
 
109
                        <offset x="-5" y="35"/>
 
110
                    </graphics>
 
111
                    <text>C1_P4</text>
 
112
                </name>
 
113
                <initialMarking>
 
114
                    <text>0</text>
 
115
                </initialMarking>
 
116
            </place>
 
117
            <place id="C1_P6">
 
118
                <graphics>
 
119
                    <position x="2280" y="390"/>
 
120
                </graphics>
 
121
                <name>
 
122
                    <graphics>
 
123
                        <offset x="-5" y="35"/>
 
124
                    </graphics>
 
125
                    <text>C1_P6</text>
 
126
                </name>
 
127
                <initialMarking>
 
128
                    <text>0</text>
 
129
                </initialMarking>
 
130
            </place>
 
131
            <place id="C1Copy_P0">
 
132
                <graphics>
 
133
                    <position x="240" y="780"/>
 
134
                </graphics>
 
135
                <name>
 
136
                    <graphics>
 
137
                        <offset x="-5" y="35"/>
 
138
                    </graphics>
 
139
                    <text>C1Copy_P0</text>
 
140
                </name>
 
141
                <initialMarking>
 
142
                    <text>1</text>
 
143
                </initialMarking>
 
144
            </place>
 
145
            <place id="C1Copy_P1">
 
146
                <graphics>
 
147
                    <position x="255" y="885"/>
 
148
                </graphics>
 
149
                <name>
 
150
                    <graphics>
 
151
                        <offset x="-5" y="35"/>
 
152
                    </graphics>
 
153
                    <text>C1Copy_P1</text>
 
154
                </name>
 
155
                <initialMarking>
 
156
                    <text>1</text>
 
157
                </initialMarking>
 
158
            </place>
 
159
            <place id="C1Copy_P2">
 
160
                <graphics>
 
161
                    <position x="225" y="975"/>
 
162
                </graphics>
 
163
                <name>
 
164
                    <graphics>
 
165
                        <offset x="-5" y="35"/>
 
166
                    </graphics>
 
167
                    <text>C1Copy_P2</text>
 
168
                </name>
 
169
                <initialMarking>
 
170
                    <text>1</text>
 
171
                </initialMarking>
 
172
            </place>
 
173
            <place id="C1Copy_P3">
 
174
                <graphics>
 
175
                    <position x="570" y="885"/>
 
176
                </graphics>
 
177
                <name>
 
178
                    <graphics>
 
179
                        <offset x="-5" y="35"/>
 
180
                    </graphics>
 
181
                    <text>C1Copy_P3</text>
 
182
                </name>
 
183
                <initialMarking>
 
184
                    <text>0</text>
 
185
                </initialMarking>
 
186
            </place>
 
187
            <place id="C1Copy_P4">
 
188
                <graphics>
 
189
                    <position x="885" y="930"/>
 
190
                </graphics>
 
191
                <name>
 
192
                    <graphics>
 
193
                        <offset x="-5" y="35"/>
 
194
                    </graphics>
 
195
                    <text>C1Copy_P4</text>
 
196
                </name>
 
197
                <initialMarking>
 
198
                    <text>0</text>
 
199
                </initialMarking>
 
200
            </place>
 
201
            <place id="C1Copy_P6">
 
202
                <graphics>
 
203
                    <position x="1125" y="930"/>
 
204
                </graphics>
 
205
                <name>
 
206
                    <graphics>
 
207
                        <offset x="-5" y="35"/>
 
208
                    </graphics>
 
209
                    <text>C1Copy_P6</text>
 
210
                </name>
 
211
                <initialMarking>
 
212
                    <text>0</text>
 
213
                </initialMarking>
 
214
            </place>
 
215
            <place id="C1CopyCopy_P0">
 
216
                <graphics>
 
217
                    <position x="1395" y="780"/>
 
218
                </graphics>
 
219
                <name>
 
220
                    <graphics>
 
221
                        <offset x="-5" y="35"/>
 
222
                    </graphics>
 
223
                    <text>C1CopyCopy_P0</text>
 
224
                </name>
 
225
                <initialMarking>
 
226
                    <text>1</text>
 
227
                </initialMarking>
 
228
            </place>
 
229
            <place id="C1CopyCopy_P1">
 
230
                <graphics>
 
231
                    <position x="1410" y="885"/>
 
232
                </graphics>
 
233
                <name>
 
234
                    <graphics>
 
235
                        <offset x="-5" y="35"/>
 
236
                    </graphics>
 
237
                    <text>C1CopyCopy_P1</text>
 
238
                </name>
 
239
                <initialMarking>
 
240
                    <text>1</text>
 
241
                </initialMarking>
 
242
            </place>
 
243
            <place id="C1CopyCopy_P2">
 
244
                <graphics>
 
245
                    <position x="1380" y="975"/>
 
246
                </graphics>
 
247
                <name>
 
248
                    <graphics>
 
249
                        <offset x="-5" y="35"/>
 
250
                    </graphics>
 
251
                    <text>C1CopyCopy_P2</text>
 
252
                </name>
 
253
                <initialMarking>
 
254
                    <text>1</text>
 
255
                </initialMarking>
 
256
            </place>
 
257
            <place id="C1CopyCopy_P3">
 
258
                <graphics>
 
259
                    <position x="1725" y="885"/>
 
260
                </graphics>
 
261
                <name>
 
262
                    <graphics>
 
263
                        <offset x="-5" y="35"/>
 
264
                    </graphics>
 
265
                    <text>C1CopyCopy_P3</text>
 
266
                </name>
 
267
                <initialMarking>
 
268
                    <text>0</text>
 
269
                </initialMarking>
 
270
            </place>
 
271
            <place id="C1CopyCopy_P4">
 
272
                <graphics>
 
273
                    <position x="2040" y="930"/>
 
274
                </graphics>
 
275
                <name>
 
276
                    <graphics>
 
277
                        <offset x="-5" y="35"/>
 
278
                    </graphics>
 
279
                    <text>C1CopyCopy_P4</text>
 
280
                </name>
 
281
                <initialMarking>
 
282
                    <text>0</text>
 
283
                </initialMarking>
 
284
            </place>
 
285
            <place id="C1CopyCopy_P6">
 
286
                <graphics>
 
287
                    <position x="2280" y="930"/>
 
288
                </graphics>
 
289
                <name>
 
290
                    <graphics>
 
291
                        <offset x="-5" y="35"/>
 
292
                    </graphics>
 
293
                    <text>C1CopyCopy_P6</text>
 
294
                </name>
 
295
                <initialMarking>
 
296
                    <text>0</text>
 
297
                </initialMarking>
 
298
            </place>
 
299
            <transition id="Shared_Done">
 
300
                <name>
 
301
                    <graphics>
 
302
                        <offset x="-5" y="35"/>
 
303
                    </graphics>
 
304
                    <text>Shared_Done</text>
 
305
                </name>
 
306
                <graphics>
 
307
                    <position x="390" y="540"/>
 
308
                </graphics>
 
309
            </transition>
 
310
            <transition id="Shared_T">
 
311
                <name>
 
312
                    <graphics>
 
313
                        <offset x="-5" y="35"/>
 
314
                    </graphics>
 
315
                    <text>Shared_T</text>
 
316
                </name>
 
317
                <graphics>
 
318
                    <position x="1875" y="375"/>
 
319
                </graphics>
 
320
            </transition>
 
321
            <transition id="C1_T1">
 
322
                <name>
 
323
                    <graphics>
 
324
                        <offset x="-5" y="35"/>
 
325
                    </graphics>
 
326
                    <text>C1_T1</text>
 
327
                </name>
 
328
                <graphics>
 
329
                    <position x="1590" y="255"/>
 
330
                </graphics>
 
331
            </transition>
 
332
            <transition id="C1_T2">
 
333
                <name>
 
334
                    <graphics>
 
335
                        <offset x="-5" y="35"/>
 
336
                    </graphics>
 
337
                    <text>C1_T2</text>
 
338
                </name>
 
339
                <graphics>
 
340
                    <position x="1590" y="315"/>
 
341
                </graphics>
 
342
            </transition>
 
343
            <transition id="C1_T3">
 
344
                <name>
 
345
                    <graphics>
 
346
                        <offset x="-5" y="35"/>
 
347
                    </graphics>
 
348
                    <text>C1_T3</text>
 
349
                </name>
 
350
                <graphics>
 
351
                    <position x="1575" y="420"/>
 
352
                </graphics>
 
353
            </transition>
 
354
            <transition id="C1_T4">
 
355
                <name>
 
356
                    <graphics>
 
357
                        <offset x="-5" y="35"/>
 
358
                    </graphics>
 
359
                    <text>C1_T4</text>
 
360
                </name>
 
361
                <graphics>
 
362
                    <position x="2130" y="375"/>
 
363
                </graphics>
 
364
            </transition>
 
365
            <transition id="C1Copy_T1">
 
366
                <name>
 
367
                    <graphics>
 
368
                        <offset x="-5" y="35"/>
 
369
                    </graphics>
 
370
                    <text>C1Copy_T1</text>
 
371
                </name>
 
372
                <graphics>
 
373
                    <position x="435" y="795"/>
 
374
                </graphics>
 
375
            </transition>
 
376
            <transition id="C1Copy_T2">
 
377
                <name>
 
378
                    <graphics>
 
379
                        <offset x="-5" y="35"/>
 
380
                    </graphics>
 
381
                    <text>C1Copy_T2</text>
 
382
                </name>
 
383
                <graphics>
 
384
                    <position x="435" y="855"/>
 
385
                </graphics>
 
386
            </transition>
 
387
            <transition id="C1Copy_T3">
 
388
                <name>
 
389
                    <graphics>
 
390
                        <offset x="-5" y="35"/>
 
391
                    </graphics>
 
392
                    <text>C1Copy_T3</text>
 
393
                </name>
 
394
                <graphics>
 
395
                    <position x="420" y="960"/>
 
396
                </graphics>
 
397
            </transition>
 
398
            <transition id="C1Copy_T4">
 
399
                <name>
 
400
                    <graphics>
 
401
                        <offset x="-5" y="35"/>
 
402
                    </graphics>
 
403
                    <text>C1Copy_T4</text>
 
404
                </name>
 
405
                <graphics>
 
406
                    <position x="975" y="915"/>
 
407
                </graphics>
 
408
            </transition>
 
409
            <transition id="C1CopyCopy_T1">
 
410
                <name>
 
411
                    <graphics>
 
412
                        <offset x="-5" y="35"/>
 
413
                    </graphics>
 
414
                    <text>C1CopyCopy_T1</text>
 
415
                </name>
 
416
                <graphics>
 
417
                    <position x="1590" y="795"/>
 
418
                </graphics>
 
419
            </transition>
 
420
            <transition id="C1CopyCopy_T2">
 
421
                <name>
 
422
                    <graphics>
 
423
                        <offset x="-5" y="35"/>
 
424
                    </graphics>
 
425
                    <text>C1CopyCopy_T2</text>
 
426
                </name>
 
427
                <graphics>
 
428
                    <position x="1590" y="855"/>
 
429
                </graphics>
 
430
            </transition>
 
431
            <transition id="C1CopyCopy_T3">
 
432
                <name>
 
433
                    <graphics>
 
434
                        <offset x="-5" y="35"/>
 
435
                    </graphics>
 
436
                    <text>C1CopyCopy_T3</text>
 
437
                </name>
 
438
                <graphics>
 
439
                    <position x="1575" y="960"/>
 
440
                </graphics>
 
441
            </transition>
 
442
            <transition id="C1CopyCopy_T4">
 
443
                <name>
 
444
                    <graphics>
 
445
                        <offset x="-5" y="35"/>
 
446
                    </graphics>
 
447
                    <text>C1CopyCopy_T4</text>
 
448
                </name>
 
449
                <graphics>
 
450
                    <position x="2130" y="915"/>
 
451
                </graphics>
 
452
            </transition>
 
453
            <arc id="T1_P1_to_Shared_Done" source="T1_P1" target="Shared_Done" type="normal"/>
 
454
            <arc id="C1_P0_to_C1_T1" source="C1_P0" target="C1_T1" type="normal"/>
 
455
            <arc id="C1_P1_to_C1_T2" source="C1_P1" target="C1_T2" type="normal"/>
 
456
            <arc id="C1_P2_to_C1_T3" source="C1_P2" target="C1_T3" type="normal"/>
 
457
            <arc id="C1_P6_to_Shared_Done" source="C1_P6" target="Shared_Done" type="normal"/>
 
458
            <arc id="C1Copy_P0_to_C1Copy_T1" source="C1Copy_P0" target="C1Copy_T1" type="normal"/>
 
459
            <arc id="C1Copy_P1_to_C1Copy_T2" source="C1Copy_P1" target="C1Copy_T2" type="normal"/>
 
460
            <arc id="C1Copy_P2_to_C1Copy_T3" source="C1Copy_P2" target="C1Copy_T3" type="normal"/>
 
461
            <arc id="C1Copy_P6_to_Shared_Done" source="C1Copy_P6" target="Shared_Done" type="normal"/>
 
462
            <arc id="C1CopyCopy_P0_to_C1CopyCopy_T1" source="C1CopyCopy_P0" target="C1CopyCopy_T1" type="normal"/>
 
463
            <arc id="C1CopyCopy_P1_to_C1CopyCopy_T2" source="C1CopyCopy_P1" target="C1CopyCopy_T2" type="normal"/>
 
464
            <arc id="C1CopyCopy_P2_to_C1CopyCopy_T3" source="C1CopyCopy_P2" target="C1CopyCopy_T3" type="normal"/>
 
465
            <arc id="C1CopyCopy_P6_to_Shared_Done" source="C1CopyCopy_P6" target="Shared_Done" type="normal"/>
 
466
            <arc id="Shared_Done_to_T1_DoneP" source="Shared_Done" target="T1_DoneP" type="normal"/>
 
467
            <arc id="C1_T2_to_C1_P3" source="C1_T2" target="C1_P3" type="normal"/>
 
468
            <arc id="C1_T3_to_C1_P3" source="C1_T3" target="C1_P3" type="normal"/>
 
469
            <arc id="C1_T1_to_C1_P3" source="C1_T1" target="C1_P3" type="normal"/>
 
470
            <arc id="C1Copy_T2_to_C1Copy_P3" source="C1Copy_T2" target="C1Copy_P3" type="normal"/>
 
471
            <arc id="C1Copy_T3_to_C1Copy_P3" source="C1Copy_T3" target="C1Copy_P3" type="normal"/>
 
472
            <arc id="C1Copy_T1_to_C1Copy_P3" source="C1Copy_T1" target="C1Copy_P3" type="normal"/>
 
473
            <arc id="C1CopyCopy_T2_to_C1CopyCopy_P3" source="C1CopyCopy_T2" target="C1CopyCopy_P3" type="normal"/>
 
474
            <arc id="C1CopyCopy_T3_to_C1CopyCopy_P3" source="C1CopyCopy_T3" target="C1CopyCopy_P3" type="normal"/>
 
475
            <arc id="C1CopyCopy_T1_to_C1CopyCopy_P3" source="C1CopyCopy_T1" target="C1CopyCopy_P3" type="normal"/>
 
476
            <arc id="C1_P3_to_Shared_T" source="C1_P3" target="Shared_T" type="normal"/>
 
477
            <arc id="Shared_T_to_C1_P4" source="Shared_T" target="C1_P4" type="normal"/>
 
478
            <arc id="C1_P4_to_C1_T4" source="C1_P4" target="C1_T4" type="normal"/>
 
479
            <arc id="C1_T4_to_C1_P6" source="C1_T4" target="C1_P6" type="normal"/>
 
480
            <arc id="C1Copy_P3_to_Shared_T" source="C1Copy_P3" target="Shared_T" type="normal"/>
 
481
            <arc id="Shared_T_to_C1Copy_P4" source="Shared_T" target="C1Copy_P4" type="normal"/>
 
482
            <arc id="C1Copy_P4_to_C1Copy_T4" source="C1Copy_P4" target="C1Copy_T4" type="normal"/>
 
483
            <arc id="C1Copy_T4_to_C1Copy_P6" source="C1Copy_T4" target="C1Copy_P6" type="normal"/>
 
484
            <arc id="C1CopyCopy_P3_to_Shared_T" source="C1CopyCopy_P3" target="Shared_T" type="normal"/>
 
485
            <arc id="Shared_T_to_C1CopyCopy_P4" source="Shared_T" target="C1CopyCopy_P4" type="normal"/>
 
486
            <arc id="C1CopyCopy_P4_to_C1CopyCopy_T4" source="C1CopyCopy_P4" target="C1CopyCopy_T4" type="normal"/>
 
487
            <arc id="C1CopyCopy_T4_to_C1CopyCopy_P6" source="C1CopyCopy_T4" target="C1CopyCopy_P6" type="normal">
 
488
                <graphics>
 
489
                    <position x="2147" y="932"/>
 
490
                </graphics>
 
491
            </arc>
 
492
            <arc id="C1_P0_to_Shared_T" source="C1_P0" target="Shared_T" type="inhibitor">
 
493
                <graphics>
 
494
                    <position x="1592" y="167"/>
 
495
                </graphics>
 
496
            </arc>
 
497
            <arc id="C1_P1_to_Shared_T" source="C1_P1" target="Shared_T" type="inhibitor">
 
498
                <graphics>
 
499
                    <position x="1262" y="257"/>
 
500
                    <position x="1472" y="107"/>
 
501
                    <position x="1742" y="92"/>
 
502
                </graphics>
 
503
            </arc>
 
504
            <arc id="C1_P2_to_Shared_T" source="C1_P2" target="Shared_T" type="inhibitor">
 
505
                <graphics>
 
506
                    <position x="1532" y="572"/>
 
507
                    <position x="1802" y="572"/>
 
508
                </graphics>
 
509
            </arc>
 
510
            <arc id="C1_P6_to_C1_T4" source="C1_P6" target="C1_T4" type="inhibitor">
 
511
                <graphics>
 
512
                    <position x="2222" y="452"/>
 
513
                </graphics>
 
514
            </arc>
 
515
            <arc id="C1Copy_P0_to_Shared_T" source="C1Copy_P0" target="Shared_T" type="inhibitor">
 
516
                <graphics>
 
517
                    <position x="437" y="707"/>
 
518
                </graphics>
 
519
            </arc>
 
520
            <arc id="C1Copy_P1_to_Shared_T" source="C1Copy_P1" target="Shared_T" type="inhibitor">
 
521
                <graphics>
 
522
                    <position x="107" y="797"/>
 
523
                    <position x="317" y="647"/>
 
524
                    <position x="587" y="632"/>
 
525
                </graphics>
 
526
            </arc>
 
527
            <arc id="C1Copy_P2_to_Shared_T" source="C1Copy_P2" target="Shared_T" type="inhibitor">
 
528
                <graphics>
 
529
                    <position x="377" y="1112"/>
 
530
                    <position x="647" y="1112"/>
 
531
                </graphics>
 
532
            </arc>
 
533
            <arc id="C1Copy_P6_to_C1Copy_T4" source="C1Copy_P6" target="C1Copy_T4" type="inhibitor">
 
534
                <graphics>
 
535
                    <position x="1067" y="992"/>
 
536
                </graphics>
 
537
            </arc>
 
538
            <arc id="C1CopyCopy_P0_to_Shared_T" source="C1CopyCopy_P0" target="Shared_T" type="inhibitor">
 
539
                <graphics>
 
540
                    <position x="1592" y="707"/>
 
541
                </graphics>
 
542
            </arc>
 
543
            <arc id="C1CopyCopy_P1_to_Shared_T" source="C1CopyCopy_P1" target="Shared_T" type="inhibitor">
 
544
                <graphics>
 
545
                    <position x="1262" y="797"/>
 
546
                    <position x="1472" y="647"/>
 
547
                    <position x="1742" y="632"/>
 
548
                </graphics>
 
549
            </arc>
 
550
            <arc id="C1CopyCopy_P2_to_Shared_T" source="C1CopyCopy_P2" target="Shared_T" type="inhibitor">
 
551
                <graphics>
 
552
                    <position x="1532" y="1112"/>
 
553
                    <position x="1802" y="1112"/>
 
554
                </graphics>
 
555
            </arc>
 
556
            <arc id="C1CopyCopy_P6_to_C1CopyCopy_T4" source="C1CopyCopy_P6" target="C1CopyCopy_T4" type="inhibitor">
 
557
                <graphics>
 
558
                    <position x="2222" y="992"/>
 
559
                </graphics>
 
560
            </arc>
 
561
        </page>
 
562
        <name>
 
563
            <text>ComposedModel</text>
 
564
        </name>
 
565
    </net>
 
566
</pnml>