-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathBPMNOS_SYNTAX.maude
More file actions
executable file
·1979 lines (1640 loc) · 96.2 KB
/
BPMNOS_SYNTAX.maude
File metadata and controls
executable file
·1979 lines (1640 loc) · 96.2 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
fmod BPMNOS-SYNTAX is
protecting QID .
protecting BOOL .
protecting INT .
protecting NAT .
protecting STRING .
protecting FLOAT .
protecting CONVERSION .
sorts Model Collaboration Pool OrgName Process ActProcElement ProcElement ProcElements .
sorts InternalAction SndAction RcvAction Action .
sorts SndCollab RcvCollab ActCollaboration CollaborationAction .
sorts EdgeSet Edges Edge EdgeName EdgeToken .
sorts Task TaskName .
sorts MsgSet Msgs Msg MsgName MsgToken .
sorts Status .
sorts InterRcv InterRcvSet .
sorts TokenUpdate Kill .
subsorts String < OrgName EdgeName TaskName MsgName .
subsorts Nat < EdgeToken MsgToken .
subsorts Edge < Edges < EdgeSet .
subsorts Msg < Msgs < MsgSet .
subsorts ProcElement < ProcElements < ActProcElement < Process .
subsorts Pool < Collaboration < ActCollaboration < Model .
subsorts InterRcv < InterRcvSet .
subsorts TokenUpdate Kill < InternalAction < Action .
subsorts SndAction RcvAction < Action .
subsorts SndCollab RcvCollab < CollaborationAction .
***Constants
ops disabled enabled running msgSent msgReceived completed : -> Status .
op emptyPool : -> Collaboration [ctor] .
op emptyProcess : -> Process [ctor] .
op emptyMsgSet : -> Msgs [ctor] .
op emptyEdgeSet : -> Edges [ctor] .
op emptyAction : -> Action [ctor] .
op emptyProcElements : -> ProcElements [ctor] .
op noAction : -> CollaborationAction [ctor] .
***Linking symbols
op {_}_ : CollaborationAction Collaboration -> ActCollaboration [prec 43].
op {_}_ : Action ProcElements -> ActProcElement [frozen prec 41 ] .
op _|_ : Collaboration Collaboration -> Collaboration [ assoc comm frozen prec 42 id: emptyPool ] .
op _|_ : ActProcElement ProcElements -> ActProcElement [ assoc comm frozen prec 40 ] .
op _|_ : ProcElements ProcElements -> ProcElements [ assoc comm frozen prec 40 ] .
op _._ : EdgeName EdgeToken -> Edge [ prec 35 frozen ] .
op _._ : TaskName Status -> Task [ prec 35 frozen ] .
op _.msg_ : MsgName MsgToken -> Msg [ prec 35 frozen ] .
op _and_ : Edges Edges -> Edges [ assoc comm prec 38 frozen id: emptyEdgeSet ] .
op _andmsg_ : Msgs Msgs -> Msgs [ assoc comm prec 38 frozen ] .
op _^_ : InterRcv InterRcv -> InterRcv [ assoc comm prec 33 frozen ] .
***Aggregation Elements
op collaboration(_) : ActCollaboration -> Model [format ( nir! d ntm rn d )] .
op pool(_,_,in:_,out:_) : OrgName Process Msgs Msgs -> Pool [ frozen format ( ntg! d d d nt gnt d d d d d d d ) ] .
op proc(_) : ActProcElement -> Process [ frozen format ( ttb! d nttty bnttt d )] .
op edges(_) : Edges -> EdgeSet [ frozen ] .
op eventRcvSplit(_) : InterRcv -> InterRcvSet [ frozen ] .
op eventInterRcv(_,_,_) : Status Edge Msg -> InterRcv [ frozen format( d d d d d d d d d ) ] .
***Tasks
op task(_,_,_,_) : Status Edge Edge TaskName -> ProcElement [ frozen format( cntttt d d d d d d d d d d ) ] .
op taskSnd(_,_,_,_,_) : Status Edge Edge Msg TaskName -> ProcElement [ frozen format( cntttt d d d d d d d d d d d d )] .
op taskRcv(_,_,_,_,_) : Status Edge Edge Msg TaskName -> ProcElement [ frozen format( cntttt d d d d d d d d d d d d )] .
***Interrupt
op taskBNI(_,_,_,_,_,_) : Status Edge Edge Msg TaskName Edge -> ProcElement [ frozen format( cntttt d d d d d d d d d d d d d d ) ] .
op taskBI(_,_,_,_,_,_) : Status Edge Edge Msg TaskName Edge -> ProcElement [ frozen format( cntttt d d d d d d d d d d d d d d ) ] .
***Events
op start(_,_) : Status Edge -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op interSnd(_,_,_,_) : Status Edge Edge Msg -> ProcElement [ frozen format( cntttt d d d d d d d d d d ) ] .
op interRcv(_,_,_,_) : Status Edge Edge Msg -> ProcElement [ frozen format( cntttt d d d d d d d d d d ) ] .
op startRcv(_,_,_) : Status Edge Msg -> ProcElement [ frozen format( cntttt d d d d d d d d ) ] .
op endSnd(_,_,_) : Status Edge Msg -> ProcElement [ frozen format( cntttt d d d d d d d d ) ] .
op terminate(_,_) : Status Edge -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op end (_,_) : Status Edge -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
***Gateways
op andJoin (_,_) : EdgeSet Edge -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op andSplit(_,_) : Edge EdgeSet -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op xorJoin(_,_) : EdgeSet Edge -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op xorSplit(_,_) : Edge EdgeSet -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op orSplit (_,_) : Edge EdgeSet -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
op eventSplit(_,_) : Edge InterRcvSet -> ProcElement [ frozen format( cntttt d d d d d d ) ] .
***ProcElement interleavingAction
---markingUpdate to propagate the tokens along a prcess
op markingUpdate(_,_) : ProcElements InternalAction -> ProcElement .
---tokenUpd to increase or decrease the value of an EdgeToken based on an InternalAction
op tokenUpd(_,_) : Edge InternalAction -> Edge .
op tokenUpd(_,_) : InterRcv InternalAction -> InterRcv .
---tokenUpd to increase or decrease the value of EdgeTokens present in a Edges based on an InternalAction
op tokenUpdEdges(_,_) : Edges InternalAction -> Edges .
***Action definition
---CollaborationAction
op collab(_,_) : OrgName Action -> CollaborationAction .
op exchange(_,_,_) : OrgName OrgName MsgName -> CollaborationAction .
---Actions
op snd(_) : MsgName -> SndAction .
op rcv(_) : MsgName -> RcvAction .
---InternalAction
op running(_) : TaskName -> InternalAction .
op completed(_) : TaskName -> InternalAction .
op tUpd(_,_) : Edges Edges -> TokenUpdate .
op kill : -> Kill .
op endReached : -> InternalAction .
***Additional Functions
---determine the nature of an Action (if it is interleaving, internal or a sndAction)
op isInterleaving(_) : Action -> Bool .
op isInternal(_) : Action -> Bool .
op isSndAction(_) : Action -> Bool .
---determine the nature of a CollaborationAction (if it is interleaving, internal or a sndAction)
op isSndCollab(_) : CollaborationAction -> Bool .
---set InterRcvSet status
op setStatusEnabled(_) : InterRcv -> InterRcv .
op setStatusDisabled(_) : InterRcv -> InterRcv .
---Decrease a token (EdgeToken and MsgToken)
op decreaseToken(_) : EdgeToken -> EdgeToken .
op decreaseMsgToken(_) : MsgToken -> MsgToken .
---Increase a token (EdgeToken and MsgToken)
op increaseToken(_) : EdgeToken -> EdgeToken .
op increaseMsgToken(_) : MsgToken -> MsgToken .
---Increase EdgeTokens of the first Edges if its Edges are also in the second Edges
op increaseTokenEdgeSet(_,_) : Edges Edges -> Edges .
---Decrease EdgeTokens of the first Edges if its Edges are also in the second Edges and if the EdgeTokens are > 0
op decreaseTokenEdgeSet(_,_) : Edges Edges -> Edges .
---incAllEdges increases all the edge tokens values of an Edges
op incAllEdges(_) : Edges -> Edges .
---decAllEdges decreases all the edge tokens values of an Edges
op decAllEdges(_) : Edges -> Edges .
---incMsgs increases the MsgToken value of one single Msg, if this Msg is present in an Msgs (by cheching MsgName)
op incMsgs(_,_) : Msgs MsgName -> Msgs .
---decMsgs decreases the MsgToken value of one single Msg, if this Msg is present in an Msgs (by cheching MsgName)
op decMsgs(_,_) : Msgs MsgName -> Msgs .
---resetAllProcTokens, resets all the EdgeToken and TaskToken in the process; the int becomes 0 while the Status becomes disabled
op resetAllProcTokens(_) : ProcElement -> ProcElement .
---resetEdges, resets all the Edge Tokens of an Edges
op resetEdges(_) : Edges -> Edges .
---resetInterRcv, resets all the interRcvevent in an eventSplit
op resetInterRcv(_) : InterRcv -> InterRcv .
------checkAllEdges increases all the edge tokens values of an Edges
--- op checkAllEdges(_) : Edges -> Bool .
------fixAllEdges to set to 1 edges with token = 10 and set to zero the resetAllProcTokens
--- op fixAllEdges(_) : Edges -> Edges .
---Verification functions
---inEdges to check if an Edge is inside and Edges (searching only for the EdgeName)
op _inEdges_ : EdgeName Edges -> Bool [prec 39] .
---inMsgs to check if an Edge is inside and Edges (searching only for the EdgeName)
op _inMsgs_ : MsgName Msgs -> Bool [prec 39] .
---intersect to extract the intersection between two edges (resulting in the edges present in both the set of edges)
op _intersect_ : Edges Edges -> Edges .
---inSet to check if an Edge that is in an Edges is also cntained in another Edges
op _inSet_ : Edges Edges -> Bool [prec 40] .
---allTokenSet? check if all the tokens of edges inside an Edges are set (>0)
op allTokenSet?(_) : Edges -> Bool .
---noTokenSet? check if no tokens of edges inside an Edges are set (>0)
op noTokenSet?(_) : Edges -> Bool .
---noInterRcvSet check if no InterRcv has a token (set to >0)
op noInterRcvSet(_) : InterRcv -> Bool .
---noTokenPresent check if no tokens is in a composition of BPMN elements which is a ProcElements here
op noTokenPresent(_) : ProcElements -> Bool .
---howManyTokenPresent check if there is only one token in a composition of BPMN elements which is a ProcElements here
op noMultipleTokenPresent(_) : ProcElements -> Bool .
---noTokenPresent check if no tokens is in a composition of BPMN elements which is a ProcElements here
op rlyNoTokenPresent(_) : ProcElements -> Bool .
---noTokenPresentExceptEndAndEndEdge check if no tokens is in a composition of BPMN elements which is a ProcElements here
op noTokenPresentExceptEndAndEndEdge(_) : ProcElements -> Bool .
---noTokenPresent check if no tokens and no message is in a composition of BPMN elements which is a ProcElements here
op noMessagePending(_) : Msgs -> Int .
op noMultipleMessagePending(_) : Msgs -> Bool .
op noMultipleTokenPresentAround(_) : ProcElements -> Int .
---howManyTokenPresent check if there is only one token in a composition of BPMN elements which is a ProcElements here
op noMultipleTokenEnd(_) : ProcElements -> Bool .
---To count numer of tokens present in the Model
op countTokens(_) : ProcElements -> Float .
op countTokens(_) : Edges -> Float .
op countTokens(_) : InterRcv -> Float .
---Check if in Edges one Sequence Flow has token >1
op multipleTokenPresentEdges(_) : Edges -> Bool .
--- Check if a SQF has a token traversedSQF(ProcElements1,EdgeName)
op checkTraversedSQF(_,_) : ProcElements EdgeName -> Bool .
---op intToFloat(_) : Int -> Float .
---var int1 : Int .
---var float1 : Float .
---eq intToFloat( int1 ) = float( int1 ) .
*** Variables definition
---OrgName
vars OrgName1 OrgName2 : OrgName .
---ProcElement
vars ProcElem1 ProcElem2 : ProcElement .
---Edges
vars Edges0 Edges1 Edges2 : Edges .
---Status
vars Status1 : Status .
---TaskName
var TName : TaskName .
---InputEdgeName and OutputEdgeName
var EName IEName OEName BNIEName IENameA : EdgeName .
---InputEdgeToken and OutputEdgeToken
var EToken IEToken OEToken BNIEToken IETokenA : EdgeToken .
---InterRcv
var interRcv : InterRcv .
---Var for Messages
vars Msgs1 : Msgs .
vars MsgName1 MsgName2 : MsgName .
vars MsgToken1 MsgToken2 : MsgToken .
vars inputMsgSet outputMsgSet : Msgs .
---Action
var Action1 : Action .
---CollaborationAction
var CollAction1 : CollaborationAction .
var Coll1 : Collaboration .
var ProcElements1 : ProcElements .
---isInterleaving
ceq isInterleaving(Action1) = false if Action1 :: TokenUpdate or Action1 :: Kill .
eq isInterleaving(Action1) = true [otherwise] .
---isInternal
ceq isInternal(Action1) = true if Action1 :: InternalAction .
eq isInternal(Action1) = false [otherwise] .
---isSndAction
ceq isSndAction(Action1) = true if Action1 :: SndAction .
eq isSndAction(Action1) = false [otherwise] .
---isSndCollab
ceq isSndCollab(CollAction1) = true if CollAction1 :: SndCollab .
eq isSndCollab(CollAction1) = false [otherwise] .
---increaseTokenEdgeSet( Edges , Edges)
ceq increaseTokenEdgeSet(IEName . IEToken and Edges1 , Edges2) =
IEName . increaseToken(IEToken) and increaseTokenEdgeSet(Edges1 , Edges2) if IEName inEdges Edges2 == true .
eq increaseTokenEdgeSet(IEName . IEToken and Edges1 , Edges2) =
IEName . IEToken and increaseTokenEdgeSet(Edges1 , Edges2) [otherwise] .
---increaseTokenEdgeSet( Edge , Edges)
eq increaseTokenEdgeSet(emptyEdgeSet , Edges2) =
emptyEdgeSet .
ceq increaseTokenEdgeSet(IEName . IEToken , Edges2) =
IEName . increaseToken(IEToken) if IEName inEdges Edges2 == true .
eq increaseTokenEdgeSet(IEName . IEToken , Edges2) =
IEName . IEToken [owise] .
---decreaseTokenEdgeSet( Edges , Edges)
ceq decreaseTokenEdgeSet(IEName . IEToken and Edges1 , Edges2) =
IEName . decreaseToken(IEToken) and decreaseTokenEdgeSet(Edges1 , Edges2) if IEToken > 0 /\ IEName inEdges Edges2 .
eq decreaseTokenEdgeSet(IEName . IEToken and Edges1 , Edges2) =
IEName . IEToken and decreaseTokenEdgeSet(Edges1 , Edges2) [otherwise] .
---decreaseTokenEdgeSet( Edge , Edges)
eq decreaseTokenEdgeSet(emptyEdgeSet , Edges2) =
emptyEdgeSet .
ceq decreaseTokenEdgeSet(IEName . IEToken , Edges2) =
IEName . decreaseToken(IEToken) if IEToken > 0 /\ IEName inEdges Edges2 .
eq decreaseTokenEdgeSet(IEName . IEToken , Edges2) =
IEName . IEToken [otherwise] .
---Edges intersect Edges
eq emptyEdgeSet intersect Edges2 =
emptyEdgeSet .
eq Edges1 intersect emptyEdgeSet =
emptyEdgeSet .
ceq IEName . IEToken and Edges1 intersect Edges2 =
IEName . IEToken and ( Edges1 intersect Edges2 ) if IEName inEdges Edges2 .
eq IEName . IEToken and Edges1 intersect Edges2 =
Edges1 intersect Edges2 [otherwise] .
---Edge intersect Edges
ceq IEName . IEToken intersect Edges2 = IEName . IEToken if IEName inEdges Edges2 .
eq IEName . IEToken intersect Edges2 = emptyEdgeSet [otherwise] .
ceq tokenUpdEdges( Edges0, tUpd(Edges1 , Edges2)) =
increaseTokenEdgeSet( Edges0 , Edges0 intersect Edges2) if Edges0 intersect Edges2 =/= emptyEdgeSet .
ceq tokenUpdEdges( Edges0, tUpd(Edges1 , Edges2)) =
decreaseTokenEdgeSet( Edges0 , Edges0 intersect Edges1) if Edges0 intersect Edges1 =/= emptyEdgeSet .
eq tokenUpdEdges( Edges0, tUpd(Edges1 , Edges2)) = Edges0 [owise] .
---tokenUpd(InterRcvSet , tUpd(Edges, Edges))
ceq tokenUpd( interRcv ^ eventInterRcv( Status1 , EName . EToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= tokenUpd( interRcv , tUpd( Edges1 , Edges2 )) ^ eventInterRcv( Status1 , EName . decreaseToken(EToken) , MsgName1 .msg MsgToken1 ) if EName inEdges Edges1 .
eq tokenUpd( interRcv ^ eventInterRcv( Status1 , EName . EToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= tokenUpd( interRcv , tUpd( Edges1 , Edges2 )) ^ eventInterRcv( Status1 , EName . EToken , MsgName1 .msg MsgToken1 ) [otherwise] .
ceq tokenUpd( eventInterRcv( Status1 , EName . EToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= eventInterRcv( Status1 , EName . decreaseToken(EToken) , MsgName1 .msg MsgToken1 ) if EName inEdges Edges1 .
eq tokenUpd( eventInterRcv( Status1 , EName . EToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= eventInterRcv( Status1 , EName . EToken , MsgName1 .msg MsgToken1 ) [otherwise] .
---tokenUpd(Edge , tUpd(Edges, Edges))
ceq tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) =
OEName . increaseToken(OEToken) if OEName inEdges Edges2 .
ceq tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) =
OEName . decreaseToken(OEToken) if OEName inEdges Edges1 .
ceq tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) =
OEName . OEToken if (OEName inEdges Edges2 =/= true) /\ (OEName inEdges Edges1 =/= true) .
eq markingUpdate(emptyProcElements , tUpd( Edges1 , Edges2 ))
= emptyProcElements .
***Singolo ProcElement
---markingUpdate defined for start
eq markingUpdate( start( Status1 , OEName . OEToken ) , tUpd( Edges1 , Edges2 ))
= start( Status1 , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 ))) .
---markingUpdate defined for task
eq markingUpdate( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) , tUpd( Edges1 , Edges2 ) )
= task( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , TName ) .
---markingUpdate defined for end
eq markingUpdate( end( Status1 , OEName . OEToken ) , tUpd( Edges1 , Edges2 ))
= end( Status1 , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 ))) .
---markingUpdate defined for xorSplit
eq markingUpdate ( xorSplit( IEName . IEToken , edges( Edges0 ) ) , tUpd( Edges1 , Edges2 ) )
= xorSplit( tokenUpd(IEName . IEToken , tUpd( Edges1 , Edges2 )) , edges( tokenUpdEdges( Edges0 , tUpd( Edges1 , Edges2 )))) .
---markingUpdate defined for andSplit
eq markingUpdate ( andSplit( IEName . IEToken ,edges( Edges0 ) ) , tUpd( Edges1 , Edges2 ) )
= andSplit( tokenUpd(IEName . IEToken , tUpd( Edges1 , Edges2 )) , edges( tokenUpdEdges( Edges0 , tUpd( Edges1 , Edges2 )))) .
---markingUpdate defined for orSplit
eq markingUpdate ( orSplit( IEName . IEToken , edges( Edges0 ) ) , tUpd( Edges1 , Edges2 ) )
= orSplit( tokenUpd(IEName . IEToken , tUpd( Edges1 , Edges2 )) , edges(tokenUpdEdges( Edges0 , tUpd( Edges1 , Edges2 )))) .
---markingUpdate defined for xorJoin
eq markingUpdate( xorJoin( edges( Edges0 ) , IEName . IEToken ) , tUpd( Edges1 , Edges2 ) )
= xorJoin( edges(tokenUpdEdges( Edges0 , tUpd( Edges1 , Edges2 ))) , tokenUpd(IEName . IEToken , tUpd( Edges1 , Edges2 ) )) .
---markingUpdate defined for andJoin
eq markingUpdate( andJoin( edges( Edges0 ) , IEName . IEToken ) , tUpd( Edges1 , Edges2 ) )
= andJoin( edges(tokenUpdEdges( Edges0 , tUpd( Edges1 , Edges2 ))) , tokenUpd(IEName . IEToken , tUpd( Edges1 , Edges2 ) ) ) .
---markingUpdate defined for eventSplit
eq markingUpdate ( eventSplit( IEName . IEToken , eventRcvSplit( interRcv ) ) , tUpd( Edges1 , Edges2 ) )
= eventSplit( tokenUpd(IEName . IEToken , tUpd( Edges1 , Edges2 )) , eventRcvSplit(tokenUpd( interRcv , tUpd( Edges1 , Edges2 ) ) ) ) .
---markingUpdate defined for startRcv
eq markingUpdate( startRcv(Status1 , OEName . OEToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ))
= startRcv(Status1 , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )), MsgName1 .msg MsgToken1 ) .
---markingUpdate defined for taskSnd
eq markingUpdate( taskSnd( Status1 , IEName . IEToken, OEName . OEToken , MsgName1 .msg MsgToken1 , TName ) , tUpd( Edges1 , Edges2 ) )
= taskSnd( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 , TName ) .
---markingUpdate defined for taskRcv
eq markingUpdate( taskRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName ) , tUpd( Edges1 , Edges2 ) )
= taskRcv( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 , TName ) .
---markingUpdate defined for interSnd
eq markingUpdate( interSnd( Status1, IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= interSnd( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 ) .
---markingUpdate defined for interRcv
eq markingUpdate( interRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= interRcv( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 ) .
---markingUpdate defined for endSnd
eq markingUpdate( endSnd( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) , tUpd( Edges1 , Edges2 ) )
= endSnd( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 ) .
---markingUpdate defined for terminate
eq markingUpdate( terminate( Status1 , OEName . OEToken ) , tUpd( Edges1 , Edges2 ) )
= terminate( Status1 , tokenUpd(OEName . OEToken , tUpd( Edges1 , Edges2 ))) .
***Exception
eq markingUpdate( taskBNI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) , tUpd( Edges1 , Edges2 ) )
= taskBNI( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) .
eq markingUpdate( taskBI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) , tUpd( Edges1 , Edges2 ) )
= taskBI( Status1 , tokenUpd( IEName . IEToken , tUpd( Edges1 , Edges2 )) , tokenUpd( OEName . OEToken , tUpd( Edges1 , Edges2 )) , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) .
eq markingUpdate( ProcElem1 | ProcElements1 , tUpd( Edges1 , Edges2 ) )
= markingUpdate( ProcElem1, tUpd( Edges1 , Edges2 ) ) | markingUpdate(ProcElements1 , tUpd( Edges1 , Edges2 ) ) .
--- EdgeName inEdges emptyEdgeSet
eq EName inEdges emptyEdgeSet = false .
--- EdgeName inEdges Edge
ceq EName inEdges IEName . IEToken
= false if EName =/= IEName .
ceq EName inEdges IEName . IEToken
= true if EName == IEName .
ceq EName inEdges IEName . IEToken and Edges0
= true if IEName == EName .
eq EName inEdges IEName . IEToken and Edges0
= false [otherwise] .
--- MsgName inMsgs emptyMsgSet
eq MsgName1 inMsgs emptyMsgSet = false .
--- MsgName inMsgs
ceq MsgName1 inMsgs MsgName2 .msg MsgToken2
= false if MsgName1 =/= MsgName2 .
ceq MsgName1 inMsgs MsgName2 .msg MsgToken2
= true if MsgName1 == MsgName2 .
ceq MsgName1 inMsgs MsgName2 .msg MsgToken2 andmsg Msgs1
= true if MsgName2 == MsgName1 .
eq MsgName1 inMsgs MsgName2 .msg MsgToken2 andmsg Msgs1
= false [otherwise] .
---incMsgs(Msg , MsgName)
ceq incMsgs( MsgName1 .msg MsgToken1 , MsgName2 )
= MsgName1 .msg increaseToken( MsgToken1 ) if MsgName1 = MsgName2 .
eq incMsgs( MsgName1 .msg MsgToken1 , MsgName2 )
= MsgName1 .msg MsgToken1 [otherwise] .
ceq incMsgs( MsgName1 .msg MsgToken1 andmsg Msgs1 , MsgName2 )
= MsgName1 .msg increaseToken( MsgToken1 ) andmsg Msgs1 if MsgName1 = MsgName2 .
eq incMsgs( MsgName1 .msg MsgToken1 andmsg Msgs1 , MsgName2 )
= MsgName1 .msg MsgToken1 andmsg incMsgs( Msgs1 , MsgName2 ) [otherwise] .
---decMsgs(Msg , MsgName)
ceq decMsgs( MsgName1 .msg MsgToken1 , MsgName2 )
= MsgName1 .msg decreaseToken( MsgToken1 ) if MsgName1 = MsgName2 .
eq decMsgs( MsgName1 .msg MsgToken1 , MsgName2 )
= MsgName1 .msg MsgToken1 [otherwise] .
ceq decMsgs( MsgName1 .msg MsgToken1 andmsg Msgs1 , MsgName2 )
= MsgName1 .msg decreaseToken( MsgToken1 ) andmsg Msgs1 if MsgName1 = MsgName2 .
eq decMsgs( MsgName1 .msg MsgToken1 andmsg Msgs1 , MsgName2 )
= MsgName1 .msg MsgToken1 andmsg decMsgs( Msgs1 , MsgName2 ) [otherwise] .
---increase an EdgeToken by 1
---limitator of 9 tokens
---ceq increaseToken( EToken ) = EToken + 1 if EToken < 10 .
---eq increaseToken( EToken ) = EToken [otherwise] .
---without limitator
eq increaseToken( EToken ) = EToken + 1 .
---decrease an EdgeToken by 1
eq decreaseToken( EToken ) = EToken - 1 .
---incAllEdges( Edges , Edge )
eq incAllEdges( emptyEdgeSet ) = emptyEdgeSet .
eq incAllEdges( Edges0 and IEName . IEToken )
= IEName . increaseToken( IEToken ) and incAllEdges( Edges0 ) .
eq incAllEdges( IEName . IEToken )
= IEName . increaseToken( IEToken ) .
------checkAllEdges if any has 10 tokens return true
---eq checkAllEdges( emptyEdgeSet ) = false .
---eq checkAllEdges( IEName . 9 ) = true .
---eq checkAllEdges( Edges0 and IEName . 9 ) = true .
---eq checkAllEdges( Edges0 ) = false [otherwise] .
------fixAllEdges if any has 10 tokens return true
---eq fixAllEdges( emptyEdgeSet ) = emptyEdgeSet .
------ceq fixAllEdges( Edges0 and IEName . IEToken )
------= IEName . 0 and fixAllEdges( Edges0 ) if IEToken > 0 /\ IEToken < 10 .
------ ceq fixAllEdges( Edges0 and IEName . IEToken )
------= IEName . 0 and fixAllEdges( Edges0 ) if IEToken > 0 /\ IEToken < 10 .
---ceq fixAllEdges( Edges0 and IEName . IEToken )
---= IEName . 1 and fixAllEdges( Edges0 ) if IEToken = 9 .
---eq fixAllEdges( Edges0 and IEName . IEToken )
---= IEName . IEToken and fixAllEdges( Edges0 ) [otherwise] .
------eq fixAllEdges( Edges0 and IEName . 10 ) = IEName . 1 and fixAllEdges( Edges0 ) .
------eq fixAllEdges( Edges0 and IEName . IEToken ) = Edges0 and IEName . IEToken [otherwise] .
------ceq fixAllEdges( IEName . IEToken )
------= IEName . 0 if IEToken > 0 /\ IEToken < 10 .
---ceq fixAllEdges( IEName . IEToken )= IEName . 1 if IEToken = 9 .
---eq fixAllEdges( IEName . IEToken )= IEName . IEToken [otherwise] .
---allTokenSet?( Edge )
ceq allTokenSet?( IEName . IEToken )
= false if IEToken == 0 .
eq allTokenSet?( IEName . IEToken )
= true [otherwise] .
---allTokenSet?(Edge and Edges)
ceq allTokenSet?( IEName . IEToken and Edges0 )
= false if IEToken == 0 .
eq allTokenSet?( IEName . IEToken and Edges0 )
= true [otherwise] .
---noTokenSet?( Edge )
ceq noTokenSet?( IEName . IEToken )
= false if IEToken > 0 .
eq noTokenSet?( IEName . IEToken )
= true [otherwise] .
---noTokenSet?(Edge and Edges)
ceq noTokenSet?( IEName . IEToken and Edges0 )
= false if IEToken > 0 .
eq noTokenSet?( IEName . IEToken and Edges0 )
= true [otherwise] .
---noTokenPresent defined for start
eq noTokenPresent( start( disabled , OEName . 0 ) )
= true .
---noTokenPresent defined for start
eq noTokenPresent( start( Status1 , OEName . OEToken ) )
= false [otherwise] .
---noTokenPresent defined for task
eq noTokenPresent( task( disabled , IEName . 0 , OEName . 0 , TName ) )
= true .
---noTokenPresent defined for task
eq noTokenPresent( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= false [otherwise] .
---noTokenPresent defined for end
eq noTokenPresent( end( Status1 , OEName . 0 ))
= true .
---noTokenPresent defined for end
eq noTokenPresent( end( Status1 , OEName . OEToken ) )
= false [otherwise] .
---noTokenPresent defined for xorSplit
ceq noTokenPresent ( xorSplit( IEName . 0 , edges( Edges0 ) ) )
= true if noTokenSet?(Edges0) = true .
---noTokenPresent defined for xorSplit
eq noTokenPresent ( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= false [otherwise] .
---noTokenPresent defined for andSplit
ceq noTokenPresent ( andSplit( IEName . 0 ,edges( Edges0 ) ) )
= true if noTokenSet?(Edges0) = true .
---noTokenPresent defined for andSplit
eq noTokenPresent ( andSplit( IEName . IEToken ,edges( Edges0 ) ) )
= false [otherwise] .
---noTokenPresent defined for orSplit
ceq noTokenPresent ( orSplit( IEName . 0 , edges( Edges0 ) ) )
= true if noTokenSet?(Edges0) = true .
---noTokenPresent defined for orSplit
eq noTokenPresent ( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= false [otherwise] .
---noTokenPresent defined for xorJoin
ceq noTokenPresent( xorJoin( edges( Edges0 ) , IEName . 0 ) )
= true if noTokenSet?(Edges0) = true .
---noTokenPresent defined for xorJoin
eq noTokenPresent( xorJoin( edges( Edges0 ) , IEName . IEToken ) )
= false [otherwise] .
---noTokenPresent defined for andJoin
ceq noTokenPresent( andJoin( edges( Edges0 ) , IEName . 0 ) )
= true if noTokenSet?(Edges0) = true .
---noTokenPresent defined for andJoin
eq noTokenPresent( andJoin( edges( Edges0 ) , IEName . IEToken ) )
= false [otherwise] .
---noTokenPresent defined for eventSplit
eq noTokenPresent ( eventSplit( IEName . 0 , eventRcvSplit( interRcv ) ) )
= true .
---noTokenPresent defined for eventSplit
eq noTokenPresent ( eventSplit( IEName . IEToken , eventRcvSplit( interRcv ) ) )
= false [otherwise] .
---noTokenPresent defined for startRcv
eq noTokenPresent( startRcv(disabled , OEName . 0 , MsgName1 .msg MsgToken1 ) )
= true .
---noTokenPresent defined for startRcv
eq noTokenPresent( startRcv(Status1 , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= false [otherwise] .
---noTokenPresent defined for taskSnd
eq noTokenPresent( taskSnd( disabled , IEName . 0, OEName . 0 , MsgName1 .msg MsgToken1 , TName ))
= true .
---noTokenPresent defined for taskSnd
eq noTokenPresent( taskSnd( Status1 , IEName . IEToken, OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= false [otherwise] .
---noTokenPresent defined for taskRcv
eq noTokenPresent( taskRcv( disabled , IEName . 0 , OEName . 0 , MsgName1 .msg MsgToken1 , TName ))
= true .
---noTokenPresent defined for taskRcv
eq noTokenPresent( taskRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= false [otherwise] .
---noTokenPresent defined for interSnd
eq noTokenPresent( interSnd( disabled, IEName . 0 , OEName . 0 , MsgName1 .msg MsgToken1 ) )
= true .
---noTokenPresent defined for interSnd
eq noTokenPresent( interSnd( Status1, IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= false [otherwise] .
---noTokenPresent defined for interRcv
eq noTokenPresent( interRcv( disabled , IEName . 0 , OEName . 0 , MsgName1 .msg MsgToken1 ) )
= true .
---noTokenPresent defined for interRcv
eq noTokenPresent( interRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= false [otherwise] .
---noTokenPresent defined for endSnd
eq noTokenPresent( endSnd( disabled , IEName . 0 , MsgName1 .msg MsgToken1 ) )
= true .
---noTokenPresent defined for endSnd
eq noTokenPresent( endSnd( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= false [otherwise] .
---noTokenPresent defined for terminate
eq noTokenPresent( terminate( disabled , OEName . 0 ) )
= true .
---noTokenPresent defined for terminate
eq noTokenPresent( terminate( Status1 , OEName . OEToken ) )
= false [otherwise] .
***noTokenPresent Exception
eq noTokenPresent( taskBNI( disabled , IEName . 0 , OEName . 0 , MsgName1 .msg MsgToken1 , TName , BNIEName . 0 ) )
= true .
***noTokenPresent Exception
eq noTokenPresent( taskBNI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) )
= false [otherwise] .
eq noTokenPresent( taskBI( disabled , IEName . 0 , OEName . 0 , MsgName1 .msg MsgToken1 , TName , BNIEName . 0 ) )
= true .
eq noTokenPresent( taskBI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) )
= false [otherwise] .
eq noTokenPresent( emptyProcElements )
= true .
ceq noTokenPresent( ProcElem1 | ProcElements1 )
= false if noTokenPresent( ProcElem1 ) = false .
eq noTokenPresent( ProcElem1 | ProcElements1 )
= true [otherwise] .
---noMultipleTokenPresent notSafe detection
---noMultipleTokenPresent defined for start
ceq noMultipleTokenPresent( start( Status1 , OEName . OEToken ) )
= false if OEToken > 1 .
---noMultipleTokenPresent defined for start
eq noMultipleTokenPresent( start( Status1 , OEName . OEToken ) )
= true [otherwise] .
---noMultipleTokenPresent defined for task
ceq noMultipleTokenPresent( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= false if IEToken > 1 or OEToken > 1 .
---noMultipleTokenPresent defined for task
eq noMultipleTokenPresent( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= true [otherwise] .
---noMultipleTokenPresent defined for end
ceq noMultipleTokenPresent( end( Status1 , OEName . OEToken ))
= false if OEToken > 1 .
---noMultipleTokenPresent defined for end
eq noMultipleTokenPresent( end( Status1 , OEName . OEToken ) )
= true [otherwise] .
---noMultipleTokenPresent defined for xorSplit
ceq noMultipleTokenPresent( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= false if IEToken > 1 .
---MANCA QUESTA PARTE --> ANDREBBE CAMBIATA...FORSE...FORSE NON SERVE\/ noTokenSet?(Edges0) = true .
ceq noMultipleTokenPresent ( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= false if multipleTokenPresentEdges( Edges0 ) = true .
---noMultipleTokenPresent defined for xorSplit
eq noMultipleTokenPresent( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= true [otherwise] .
---noMultipleTokenPresent defined for andSplit
ceq noMultipleTokenPresent( andSplit( IEName . IEToken ,edges( Edges0 ) ) )
= false if IEToken > 1 .
---noMultipleTokenPresent defined for andSplit
ceq noMultipleTokenPresent( andSplit( IEName . IEToken , edges( Edges0 ) ) )
= false if multipleTokenPresentEdges( Edges0 ) = true .
---noMultipleTokenPresent defined for andSplit
eq noMultipleTokenPresent( andSplit( IEName . IEToken ,edges( Edges0 ) ) )
= true [otherwise] .
---noMultipleTokenPresent defined for orSplit
ceq noMultipleTokenPresent( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= false if IEToken > 1 .
---NON SERVE multipleTokenPresentEdges, BASTA FARE COME SOTO
---noMultipleTokenPresent defined for andSplit
--- ceq noMultipleTokenPresent ( orSplit( IEName . IEToken , edges( OEName . OEToken and Edges0 ) ) )
--- = false if OEToken > 1 .
---noMultipleTokenPresent defined for andSplit
ceq noMultipleTokenPresent( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= false if multipleTokenPresentEdges( Edges0 ) = true .
---noMultipleTokenPresent defined for orSplit
eq noMultipleTokenPresent ( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= true [otherwise] .
---noMultipleTokenPresent defined for xorJoin
ceq noMultipleTokenPresent( xorJoin( edges( Edges0 ) , OEName . OEToken ) )
= false if OEToken > 1 .
ceq noMultipleTokenPresent ( xorJoin( edges( Edges0 ) , OEName . OEToken ) )
= false if multipleTokenPresentEdges( Edges0 ) = true .
---noMultipleTokenPresent defined for xorJoin
eq noMultipleTokenPresent( xorJoin( edges( Edges0 ) , OEName . OEToken ) )
= true [otherwise] .
---noMultipleTokenPresent defined for andJoin
ceq noMultipleTokenPresent( andJoin( edges( Edges0 ) , OEName . OEToken ) )
= false if OEToken > 1 .
ceq noMultipleTokenPresent( andJoin( edges( Edges0 ) , OEName . OEToken ) )
= false if multipleTokenPresentEdges( Edges0 ) = true .
---noMultipleTokenPresent defined for andJoin
eq noMultipleTokenPresent( andJoin( edges( Edges0 ) , OEName . OEToken ) )
= true [otherwise] .
---noMultipleTokenPresent defined for eventSplit
ceq noMultipleTokenPresent( eventSplit( IEName . IEToken , eventRcvSplit( interRcv ) ) )
= false if IEToken > 1 .
---noMultipleTokenPresent defined for eventSplit
eq noMultipleTokenPresent( eventSplit( IEName . IEToken , eventRcvSplit( interRcv ) ) )
= true [otherwise] .
---noMultipleTokenPresent defined for startRcv
ceq noMultipleTokenPresent( startRcv(Status1 , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= false if OEToken > 1 .
---noMultipleTokenPresent defined for startRcv
eq noMultipleTokenPresent( startRcv(Status1 , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= true [otherwise] .
---noMultipleTokenPresent defined for taskSnd
ceq noMultipleTokenPresent( taskSnd( Status1 , IEName . IEToken, OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= false if IEToken > 1 or OEToken > 1 .
---noMultipleTokenPresent defined for taskSnd
eq noMultipleTokenPresent( taskSnd( Status1 , IEName . IEToken, OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= true [otherwise] .
---noMultipleTokenPresent defined for taskRcv
ceq noMultipleTokenPresent( taskRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= false if IEToken > 1 or OEToken > 1 .
---noMultipleTokenPresent defined for taskRcv
eq noMultipleTokenPresent( taskRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= true [otherwise] .
---noMultipleTokenPresent defined for interSnd
ceq noMultipleTokenPresent( interSnd( Status1, IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= false if IEToken > 1 or OEToken > 1 .
---noMultipleTokenPresent defined for interSnd
eq noMultipleTokenPresent( interSnd( Status1, IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= true [otherwise] .
---noMultipleTokenPresent defined for interRcv
ceq noMultipleTokenPresent( interRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= false if IEToken > 1 or OEToken > 1 .
---noMultipleTokenPresent defined for interRcv
eq noMultipleTokenPresent( interRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= true [otherwise] .
---noMultipleTokenPresent defined for endSnd
ceq noMultipleTokenPresent( endSnd( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= false if IEToken > 1 .
---noMultipleTokenPresent defined for endSnd
eq noMultipleTokenPresent( endSnd( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= true [otherwise] .
---noMultipleTokenPresent defined for terminate
ceq noMultipleTokenPresent( terminate( Status1 , OEName . OEToken ) )
= false if OEToken > 1 .
---noMultipleTokenPresent defined for terminate
eq noMultipleTokenPresent( terminate( Status1 , OEName . OEToken ) )
= true [otherwise] .
***noMultipleTokenPresent Exception
ceq noMultipleTokenPresent( taskBNI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . 0 ) )
= false if IEToken > 1 or OEToken > 1 .
***noMultipleTokenPresent Exception
eq noMultipleTokenPresent( taskBNI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) )
= true [otherwise] .
ceq noMultipleTokenPresent( taskBI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . 0 ) )
= false if IEToken > 1 or OEToken > 1 .
eq noMultipleTokenPresent( taskBI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) )
= true [otherwise] .
eq noMultipleTokenPresent( emptyProcElements )
= true .
---INVERTI
ceq noMultipleTokenPresent( ProcElem1 | ProcElements1 )
= false if noMultipleTokenPresent( ProcElem1 ) = false .
eq noMultipleTokenPresent( ProcElem1 | ProcElements1 )
= true [otherwise] .
---noMessagePending pending in a Msgs of a pool
---pool(_,_,in:_,out:_)
--- MsgName inMsgs emptyMsgSet
eq noMessagePending ( MsgName2 .msg MsgToken2 andmsg Msgs1 ) =
noMessagePending( MsgName2 .msg MsgToken2 ) + noMessagePending( Msgs1 ) .
eq noMessagePending( emptyMsgSet ) = 0 .
eq noMessagePending( MsgName2 .msg MsgToken2 )
= MsgToken2 .
eq noMultipleMessagePending ( MsgName2 .msg MsgToken2 andmsg Msgs1 ) =
noMultipleMessagePending( MsgName2 .msg MsgToken2 ) and noMultipleMessagePending( Msgs1 ) .
eq noMultipleMessagePending( emptyMsgSet ) = true .
ceq noMultipleMessagePending( MsgName2 .msg MsgToken2 )
= false if MsgToken2 > 1 .
eq noMultipleMessagePending( MsgName2 .msg MsgToken2 )
= true [otherwise] .
eq MsgName1 inMsgs emptyMsgSet = false .
--- MsgName inMsgs
ceq MsgName1 inMsgs MsgName2 .msg MsgToken2
= false if MsgName1 =/= MsgName2 .
ceq MsgName1 inMsgs MsgName2 .msg MsgToken2
= true if MsgName1 == MsgName2 .
ceq MsgName1 inMsgs MsgName2 .msg MsgToken2 andmsg Msgs1
= true if MsgName2 == MsgName1 .
eq MsgName1 inMsgs MsgName2 .msg MsgToken2 andmsg Msgs1
= false [otherwise] .
***noMultipleTokenPresentAround
---noMultipleTokenPresentAround notSafe detection
---noMultipleTokenPresentAround defined for start
ceq noMultipleTokenPresentAround( start( Status1 , OEName . OEToken ) )
= 0 if OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for start
eq noMultipleTokenPresentAround( start( Status1 , OEName . OEToken ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for task
ceq noMultipleTokenPresentAround( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for task
eq noMultipleTokenPresentAround( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for end
ceq noMultipleTokenPresentAround( end( Status1 , OEName . OEToken ))
= 0 if OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for end
eq noMultipleTokenPresentAround( end( Status1 , OEName . OEToken ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for xorSplit
ceq noMultipleTokenPresentAround ( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= 0 if IEToken = 0 .
---MANCA QUESTA PARTE --> ANDREBBE CAMBIATA...FORSE...FORSE NON SERVE\/ noTokenSet?(Edges0) = true .
---noMultipleTokenPresentAround defined for xorSplit
eq noMultipleTokenPresentAround ( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for andSplit
ceq noMultipleTokenPresentAround ( andSplit( IEName . IEToken ,edges( Edges0 ) ) )
= 0 if IEToken = 0 .
---noMultipleTokenPresentAround defined for andSplit
eq noMultipleTokenPresentAround ( andSplit( IEName . IEToken ,edges( Edges0 ) ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for orSplit
ceq noMultipleTokenPresentAround ( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= 0 if IEToken = 0 .
---noMultipleTokenPresentAround defined for orSplit
eq noMultipleTokenPresentAround ( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for xorJoin
ceq noMultipleTokenPresentAround( xorJoin( edges( Edges0 ) , OEName . OEToken ) )
= 0 if OEToken = 0 .
---noMultipleTokenPresentAround defined for xorJoin
eq noMultipleTokenPresentAround( xorJoin( edges( Edges0 ) , OEName . OEToken ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for andJoin
ceq noMultipleTokenPresentAround( andJoin( edges( Edges0 ) , OEName . OEToken ) )
= 0 if OEToken = 0 .
---noMultipleTokenPresentAround defined for andJoin
eq noMultipleTokenPresentAround( andJoin( edges( Edges0 ) , OEName . OEToken ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for eventSplit
ceq noMultipleTokenPresentAround ( eventSplit( IEName . IEToken , eventRcvSplit( interRcv ) ) )
= 0 if IEToken = 0 .
---noMultipleTokenPresentAround defined for eventSplit
eq noMultipleTokenPresentAround ( eventSplit( IEName . IEToken , eventRcvSplit( interRcv ) ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for startRcv
ceq noMultipleTokenPresentAround( startRcv(Status1 , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= 0 if OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for startRcv
eq noMultipleTokenPresentAround( startRcv(Status1 , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for taskSnd
ceq noMultipleTokenPresentAround( taskSnd( Status1 , IEName . IEToken, OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for taskSnd
eq noMultipleTokenPresentAround( taskSnd( Status1 , IEName . IEToken, OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for taskRcv
ceq noMultipleTokenPresentAround( taskRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for taskRcv
eq noMultipleTokenPresentAround( taskRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName ))
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for interSnd
ceq noMultipleTokenPresentAround( interSnd( Status1, IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for interSnd
eq noMultipleTokenPresentAround( interSnd( Status1, IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for interRcv
ceq noMultipleTokenPresentAround( interRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for interRcv
eq noMultipleTokenPresentAround( interRcv( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for endSnd
ceq noMultipleTokenPresentAround( endSnd( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= 0 if IEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for endSnd
eq noMultipleTokenPresentAround( endSnd( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= 1 [otherwise] .
---noMultipleTokenPresentAround defined for terminate
ceq noMultipleTokenPresentAround( terminate( Status1 , OEName . OEToken ) )
= 0 if OEToken = 0 /\ Status1 = disabled .
---noMultipleTokenPresentAround defined for terminate
eq noMultipleTokenPresentAround( terminate( Status1 , OEName . OEToken ) )
= 1 [otherwise] .
***noMultipleTokenPresentAround Exception
ceq noMultipleTokenPresentAround( taskBNI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . 0 ) )
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
***noMultipleTokenPresentAround Exception
eq noMultipleTokenPresentAround( taskBNI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) )
= 1 [otherwise] .
ceq noMultipleTokenPresentAround( taskBI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . 0 ) )
= 0 if IEToken = 0 /\ OEToken = 0 /\ Status1 = disabled .
eq noMultipleTokenPresentAround( taskBI( Status1 , IEName . IEToken , OEName . OEToken , MsgName1 .msg MsgToken1 , TName , BNIEName . BNIEToken ) )
= 1 [otherwise] .
eq noMultipleTokenPresentAround( emptyProcElements )
= 0 .
eq noMultipleTokenPresentAround( ProcElem1 | ProcElements1 )
= 0 + noMultipleTokenPresentAround( ProcElem1 ) + noMultipleTokenPresentAround(ProcElements1 ) .
--- eq noMultipleTokenPresentAround( ProcElem1 | ProcElements1 )
--- = false [otherwise] .
***countTokens
eq countTokens( Edges0 and IEName . IEToken ) = countTokens( Edges0 ) + float( IEToken ) .
eq countTokens( IEName . IEToken ) = float( IEToken ) .
eq countTokens( emptyEdgeSet ) = 0.0 .
---noInterRcvSet( Edge )
ceq countTokens( eventInterRcv( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= float( IEToken ) + 1.0 if Status1 =/= disabled .
eq countTokens( eventInterRcv( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) )
= float( IEToken ) [otherwise] .
---countTokens(Edge and Edges)
eq countTokens( eventInterRcv( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 ) ^ interRcv )
= countTokens(eventInterRcv( Status1 , IEName . IEToken , MsgName1 .msg MsgToken1 )) + countTokens( interRcv ) .
---countTokens to count number of token present in the model in a certain moment
***countTokens
---countTokens defined for start
ceq countTokens( start( Status1 , OEName . OEToken ) )
= float( OEToken ) + 1.0 if Status1 =/= disabled .
---countTokens defined for start
eq countTokens( start( Status1 , OEName . OEToken ) )
= float( OEToken ) [otherwise] .
---countTokens defined for task
ceq countTokens( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= float( OEToken ) + 1.0 if Status1 =/= disabled .
---countTokens defined for task
eq countTokens( task( Status1 , IEName . IEToken , OEName . OEToken , TName ) )
= float( OEToken ) [otherwise] .
---countTokens defined for end
ceq countTokens( end( Status1 , OEName . OEToken ))
= float( OEToken ) + 1.0 if Status1 =/= disabled .
---countTokens defined for end
eq countTokens( end( Status1 , OEName . OEToken ) )
= float( OEToken ) [otherwise] .
---countTokens defined for xorSplit
eq countTokens ( xorSplit( IEName . IEToken , edges( Edges0 ) ) )
= countTokens( Edges0 ) .
---countTokens defined for andSplit
eq countTokens ( andSplit( IEName . IEToken ,edges( Edges0 ) ) )
= countTokens( Edges0 ) .
---countTokens defined for orSplit
eq countTokens ( orSplit( IEName . IEToken , edges( Edges0 ) ) )
= countTokens( Edges0 ) .
---countTokens defined for xorJoin
eq countTokens( xorJoin( edges( Edges0 ) , OEName . OEToken ) )
= countTokens( Edges0 ) + float( OEToken ) .