← Back to branch summary

~tapaal-dist-ctl/verifypn/verifypnTestFramework

« back to all changes in this revision

Viewing changes to testFramework/completeModelDB/DatabaseWithMutex-PT-04/CTLCardinality.txt

  • Committer: tobiasj1991 at gmail
  • Date: 2016-04-28 10:42:22 UTC
  • Revision ID: tobiasj1991@gmail.com-20160428104222-6vcahq0z3xnzncje
Cleaning up

Show diffs side-by-side

added added

removed removed

Lines of Context:
testFramework/completeModelDB/DatabaseWithMutex-PT-04/CTLCardinality.txt
1
 
Property DatabaseWithMutex-COL-04-CTLCardinality-0
2
 
  "Automatically generated"
3
 
  is:
4
 
    E X A ((((#tokens("RecBuff_4_1", "RecBuff_1_4", "RecBuff_2_1", "RecBuff_1_3", "RecBuff_4_4", "RecBuff_1_1", "RecBuff_3_4", "RecBuff_2_3", "RecBuff_3_2", "RecBuff_4_2", "RecBuff_4_3", "RecBuff_1_2", "RecBuff_3_3", "RecBuff_2_2", "RecBuff_3_1", "RecBuff_2_4")) <= (#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")))) U (((1) <= (#tokens("Active_1_4", "Active_3_2", "Active_2_4", "Active_1_1", "Active_3_4", "Active_2_1", "Active_2_2", "Active_1_3", "Active_4_4", "Active_4_2", "Active_4_1", "Active_2_3", "Active_3_1", "Active_3_3", "Active_4_3", "Active_1_2")))))
5
 
  end.
6
 
Property DatabaseWithMutex-COL-04-CTLCardinality-1
7
 
  "Automatically generated"
8
 
  is:
9
 
    A F ! ! ! ((#tokens("RecBuff_4_1", "RecBuff_1_4", "RecBuff_2_1", "RecBuff_1_3", "RecBuff_4_4", "RecBuff_1_1", "RecBuff_3_4", "RecBuff_2_3", "RecBuff_3_2", "RecBuff_4_2", "RecBuff_4_3", "RecBuff_1_2", "RecBuff_3_3", "RecBuff_2_2", "RecBuff_3_1", "RecBuff_2_4")) <= (#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")))
10
 
  end.
11
 
Property DatabaseWithMutex-COL-04-CTLCardinality-2
12
 
  "Automatically generated"
13
 
  is:
14
 
    ((A F ! ((3) <= (#tokens("all_active_4", "all_active_3", "all_active_1", "all_active_2")))) & (((3) <= (#tokens("Mutex_1", "Mutex_4", "Mutex_3", "Mutex_2")))))
15
 
  end.
16
 
Property DatabaseWithMutex-COL-04-CTLCardinality-3
17
 
  "Automatically generated"
18
 
  is:
19
 
    ((A G ! ((((#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")) <= (#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")))) & (((3) <= (#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")))))) & (E G A X ((#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")) <= (#tokens("all_active_4", "all_active_3", "all_active_1", "all_active_2")))))
20
 
  end.
21
 
Property DatabaseWithMutex-COL-04-CTLCardinality-4
22
 
  "Automatically generated"
23
 
  is:
24
 
    E F ((E X ((#tokens("WaitMutex_4_2", "WaitMutex_4_1", "WaitMutex_3_3", "WaitMutex_1_2", "WaitMutex_2_3", "WaitMutex_2_1", "WaitMutex_1_4", "WaitMutex_4_3", "WaitMutex_3_1", "WaitMutex_2_4", "WaitMutex_1_1", "WaitMutex_3_4", "WaitMutex_2_2", "WaitMutex_4_4", "WaitMutex_3_2", "WaitMutex_1_3")) <= (#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")))) & (((3) <= (#tokens("RecBuff_4_1", "RecBuff_1_4", "RecBuff_2_1", "RecBuff_1_3", "RecBuff_4_4", "RecBuff_1_1", "RecBuff_3_4", "RecBuff_2_3", "RecBuff_3_2", "RecBuff_4_2", "RecBuff_4_3", "RecBuff_1_2", "RecBuff_3_3", "RecBuff_2_2", "RecBuff_3_1", "RecBuff_2_4")))))
25
 
  end.
26
 
Property DatabaseWithMutex-COL-04-CTLCardinality-5
27
 
  "Automatically generated"
28
 
  is:
29
 
    A G ((A X ((3) <= (#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")))) | (((((((#tokens("RecBuff_4_1", "RecBuff_1_4", "RecBuff_2_1", "RecBuff_1_3", "RecBuff_4_4", "RecBuff_1_1", "RecBuff_3_4", "RecBuff_2_3", "RecBuff_3_2", "RecBuff_4_2", "RecBuff_4_3", "RecBuff_1_2", "RecBuff_3_3", "RecBuff_2_2", "RecBuff_3_1", "RecBuff_2_4")) <= (#tokens("Active_1_4", "Active_3_2", "Active_2_4", "Active_1_1", "Active_3_4", "Active_2_1", "Active_2_2", "Active_1_3", "Active_4_4", "Active_4_2", "Active_4_1", "Active_2_3", "Active_3_1", "Active_3_3", "Active_4_3", "Active_1_2")))) | (((1) <= (#tokens("Active_1_4", "Active_3_2", "Active_2_4", "Active_1_1", "Active_3_4", "Active_2_1", "Active_2_2", "Active_1_3", "Active_4_4", "Active_4_2", "Active_4_1", "Active_2_3", "Active_3_1", "Active_3_3", "Active_4_3", "Active_1_2")))))) & (((((#tokens("RecBuff_4_1", "RecBuff_1_4", "RecBuff_2_1", "RecBuff_1_3", "RecBuff_4_4", "RecBuff_1_1", "RecBuff_3_4", "RecBuff_2_3", "RecBuff_3_2", "RecBuff_4_2", "RecBuff_4_3", "RecBuff_1_2", "RecBuff_3_3", "RecBuff_2_2", "RecBuff_3_1", "RecBuff_2_4")) <= (#tokens("Mutex_1", "Mutex_4", "Mutex_3", "Mutex_2")))) | (((3) <= (#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")))))))))
30
 
  end.
31
 
Property DatabaseWithMutex-COL-04-CTLCardinality-6
32
 
  "Automatically generated"
33
 
  is:
34
 
    A G A X ((#tokens("WaitMutex_4_2", "WaitMutex_4_1", "WaitMutex_3_3", "WaitMutex_1_2", "WaitMutex_2_3", "WaitMutex_2_1", "WaitMutex_1_4", "WaitMutex_4_3", "WaitMutex_3_1", "WaitMutex_2_4", "WaitMutex_1_1", "WaitMutex_3_4", "WaitMutex_2_2", "WaitMutex_4_4", "WaitMutex_3_2", "WaitMutex_1_3")) <= (#tokens("Mutex_1", "Mutex_4", "Mutex_3", "Mutex_2")))
35
 
  end.
36
 
Property DatabaseWithMutex-COL-04-CTLCardinality-7
37
 
  "Automatically generated"
38
 
  is:
39
 
    E G ! E F ((2) <= (#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")))
40
 
  end.
41
 
Property DatabaseWithMutex-COL-04-CTLCardinality-8
42
 
  "Automatically generated"
43
 
  is:
44
 
    E X A ((((#tokens("updating_1_3", "updating_4_2", "updating_1_1", "updating_2_1", "updating_2_4", "updating_3_1", "updating_3_2", "updating_2_2", "updating_4_1", "updating_3_4", "updating_1_2", "updating_4_3", "updating_1_4", "updating_3_3", "updating_2_3", "updating_4_4")) <= (#tokens("all_passive_1", "all_passive_4", "all_passive_2", "all_passive_3")))) U (((#tokens("all_passive_1", "all_passive_4", "all_passive_2", "all_passive_3")) <= (#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")))))
45
 
  end.
46
 
Property DatabaseWithMutex-COL-04-CTLCardinality-9
47
 
  "Automatically generated"
48
 
  is:
49
 
    E X E G ((((#tokens("WaitMutex_4_2", "WaitMutex_4_1", "WaitMutex_3_3", "WaitMutex_1_2", "WaitMutex_2_3", "WaitMutex_2_1", "WaitMutex_1_4", "WaitMutex_4_3", "WaitMutex_3_1", "WaitMutex_2_4", "WaitMutex_1_1", "WaitMutex_3_4", "WaitMutex_2_2", "WaitMutex_4_4", "WaitMutex_3_2", "WaitMutex_1_3")) <= (#tokens("Mutex_1", "Mutex_4", "Mutex_3", "Mutex_2")))) & (((#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")) <= (#tokens("updating_1_3", "updating_4_2", "updating_1_1", "updating_2_1", "updating_2_4", "updating_3_1", "updating_3_2", "updating_2_2", "updating_4_1", "updating_3_4", "updating_1_2", "updating_4_3", "updating_1_4", "updating_3_3", "updating_2_3", "updating_4_4")))))
50
 
  end.
51
 
Property DatabaseWithMutex-COL-04-CTLCardinality-10
52
 
  "Automatically generated"
53
 
  is:
54
 
    ((((E F ((#tokens("all_passive_1", "all_passive_4", "all_passive_2", "all_passive_3")) <= (#tokens("Modify_1_1", "Modify_1_3", "Modify_2_1", "Modify_3_1", "Modify_4_2", "Modify_4_1", "Modify_3_4", "Modify_3_2", "Modify_4_4", "Modify_2_2", "Modify_4_3", "Modify_1_2", "Modify_2_4", "Modify_1_4", "Modify_3_3", "Modify_2_3")))) | (A X ((1) <= (#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")))))) | (E F ((2) <= (#tokens("updating_1_3", "updating_4_2", "updating_1_1", "updating_2_1", "updating_2_4", "updating_3_1", "updating_3_2", "updating_2_2", "updating_4_1", "updating_3_4", "updating_1_2", "updating_4_3", "updating_1_4", "updating_3_3", "updating_2_3", "updating_4_4")))))
55
 
  end.
56
 
Property DatabaseWithMutex-COL-04-CTLCardinality-11
57
 
  "Automatically generated"
58
 
  is:
59
 
    A ((((#tokens("Modify_1_1", "Modify_1_3", "Modify_2_1", "Modify_3_1", "Modify_4_2", "Modify_4_1", "Modify_3_4", "Modify_3_2", "Modify_4_4", "Modify_2_2", "Modify_4_3", "Modify_1_2", "Modify_2_4", "Modify_1_4", "Modify_3_3", "Modify_2_3")) <= (#tokens("all_active_4", "all_active_3", "all_active_1", "all_active_2")))) U (! ((#tokens("MesBuffReply_3_4", "MesBuffReply_2_2", "MesBuffReply_2_4", "MesBuffReply_3_2", "MesBuffReply_4_2", "MesBuffReply_1_4", "MesBuffReply_4_3", "MesBuffReply_2_1", "MesBuffReply_3_3", "MesBuffReply_1_1", "MesBuffReply_2_3", "MesBuffReply_3_1", "MesBuffReply_1_3", "MesBuffReply_4_1", "MesBuffReply_1_2", "MesBuffReply_4_4")) <= (#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")))))
60
 
  end.
61
 
Property DatabaseWithMutex-COL-04-CTLCardinality-12
62
 
  "Automatically generated"
63
 
  is:
64
 
    E F ((((3) <= (#tokens("all_active_4", "all_active_3", "all_active_1", "all_active_2")))) & (((#tokens("all_passive_1", "all_passive_4", "all_passive_2", "all_passive_3")) <= (#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")))))
65
 
  end.
66
 
Property DatabaseWithMutex-COL-04-CTLCardinality-13
67
 
  "Automatically generated"
68
 
  is:
69
 
    A ((((#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")) <= (#tokens("all_passive_1", "all_passive_4", "all_passive_2", "all_passive_3")))) U (A G ((#tokens("WaitMutex_4_2", "WaitMutex_4_1", "WaitMutex_3_3", "WaitMutex_1_2", "WaitMutex_2_3", "WaitMutex_2_1", "WaitMutex_1_4", "WaitMutex_4_3", "WaitMutex_3_1", "WaitMutex_2_4", "WaitMutex_1_1", "WaitMutex_3_4", "WaitMutex_2_2", "WaitMutex_4_4", "WaitMutex_3_2", "WaitMutex_1_3")) <= (#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")))))
70
 
  end.
71
 
Property DatabaseWithMutex-COL-04-CTLCardinality-14
72
 
  "Automatically generated"
73
 
  is:
74
 
    ((A X E X ((#tokens("updating_1_3", "updating_4_2", "updating_1_1", "updating_2_1", "updating_2_4", "updating_3_1", "updating_3_2", "updating_2_2", "updating_4_1", "updating_3_4", "updating_1_2", "updating_4_3", "updating_1_4", "updating_3_3", "updating_2_3", "updating_4_4")) <= (#tokens("Acknowledge_1_2", "Acknowledge_4_3", "Acknowledge_2_2", "Acknowledge_3_3", "Acknowledge_3_1", "Acknowledge_1_4", "Acknowledge_4_1", "Acknowledge_1_1", "Acknowledge_4_2", "Acknowledge_2_1", "Acknowledge_2_4", "Acknowledge_3_2", "Acknowledge_3_4", "Acknowledge_2_3", "Acknowledge_4_4", "Acknowledge_1_3")))) & (! E ((((#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")) <= (#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")))) U (((#tokens("Mutex_1", "Mutex_4", "Mutex_3", "Mutex_2")) <= (#tokens("Active_1_4", "Active_3_2", "Active_2_4", "Active_1_1", "Active_3_4", "Active_2_1", "Active_2_2", "Active_1_3", "Active_4_4", "Active_4_2", "Active_4_1", "Active_2_3", "Active_3_1", "Active_3_3", "Active_4_3", "Active_1_2")))))))
75
 
  end.
76
 
Property DatabaseWithMutex-COL-04-CTLCardinality-15
77
 
  "Automatically generated"
78
 
  is:
79
 
    ((E F ! ((((#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")) <= (#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")))) & (((#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")) <= (#tokens("RecBuff_4_1", "RecBuff_1_4", "RecBuff_2_1", "RecBuff_1_3", "RecBuff_4_4", "RecBuff_1_1", "RecBuff_3_4", "RecBuff_2_3", "RecBuff_3_2", "RecBuff_4_2", "RecBuff_4_3", "RecBuff_1_2", "RecBuff_3_3", "RecBuff_2_2", "RecBuff_3_1", "RecBuff_2_4")))))) & (E ((! ((3) <= (#tokens("Active_1_4", "Active_3_2", "Active_2_4", "Active_1_1", "Active_3_4", "Active_2_1", "Active_2_2", "Active_1_3", "Active_4_4", "Active_4_2", "Active_4_1", "Active_2_3", "Active_3_1", "Active_3_3", "Active_4_3", "Active_1_2")))) U (((((#tokens("all_passive_1", "all_passive_4", "all_passive_2", "all_passive_3")) <= (#tokens("Message_2_3", "Message_4_1", "Message_3_3", "Message_3_1", "Message_4_4", "Message_1_2", "Message_2_2", "Message_3_4", "Message_3_2", "Message_2_4", "Message_4_2", "Message_1_4", "Message_4_3", "Message_1_3", "Message_2_1", "Message_1_1")))) & (((#tokens("WaitMutex_4_2", "WaitMutex_4_1", "WaitMutex_3_3", "WaitMutex_1_2", "WaitMutex_2_3", "WaitMutex_2_1", "WaitMutex_1_4", "WaitMutex_4_3", "WaitMutex_3_1", "WaitMutex_2_4", "WaitMutex_1_1", "WaitMutex_3_4", "WaitMutex_2_2", "WaitMutex_4_4", "WaitMutex_3_2", "WaitMutex_1_3")) <= (#tokens("Mutex_1", "Mutex_4", "Mutex_3", "Mutex_2")))))))))
80
 
  end.