-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathmachine0.bcm
More file actions
135 lines (135 loc) · 35.6 KB
/
machine0.bcm
File metadata and controls
135 lines (135 loc) · 35.6 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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase">
<org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/whatsapp-lab1_test/ctx0.bcc" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.seesContext#_bHo9kKNuEeek3qZDwmMYTw"/>
<org.eventb.core.scInternalContext name="ctx0">
<org.eventb.core.scCarrierSet name="CONTENT" org.eventb.core.source="/whatsapp-lab1_test/ctx0.buc|org.eventb.core.contextFile#ctx0|org.eventb.core.carrierSet#_eMLFkaNuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(CONTENT)"/>
<org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/whatsapp-lab1_test/ctx0.buc|org.eventb.core.contextFile#ctx0|org.eventb.core.carrierSet#_eMLFkKNuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="ctx1" org.eventb.core.label="inv1" org.eventb.core.predicate="user⊆USER" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHqyxKNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx2" org.eventb.core.label="inv2" org.eventb.core.predicate="content⊆CONTENT" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHqyxaNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx3" org.eventb.core.label="inv3" org.eventb.core.predicate="chat∈user ↔ user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHqyxqNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx4" org.eventb.core.label="inv4" org.eventb.core.predicate="active∈user ⇸ user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHrZ0KNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx5" org.eventb.core.label="inv5" org.eventb.core.predicate="muted∈user ↔ user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHrZ0aNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx6" org.eventb.core.label="inv6" org.eventb.core.predicate="active⊆chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHrZ0qNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx7" org.eventb.core.label="inv7" org.eventb.core.predicate="muted⊆chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_bHsA4KNuEeek3qZDwmMYTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx8" org.eventb.core.label="inv8" org.eventb.core.predicate="chatcontent∈content ↔ chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_rFZsk6nWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="ctx9" org.eventb.core.label="inv9" org.eventb.core.predicate="owner∈content → user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.invariant#_EI7pOancEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="active" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_bHqLtaNuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(USER×USER)"/>
<org.eventb.core.scVariable name="chat" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_bHqLtKNuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(USER×USER)"/>
<org.eventb.core.scVariable name="chatcontent" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_rFZskqnWEeeaxakKd9Dntw" org.eventb.core.type="ℙ(CONTENT×(USER×USER))"/>
<org.eventb.core.scVariable name="content" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_bHqLs6NuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(CONTENT)"/>
<org.eventb.core.scVariable name="muted" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_bHqywKNuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(USER×USER)"/>
<org.eventb.core.scVariable name="owner" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_EI7pOKncEeeaxakKd9Dntw" org.eventb.core.type="ℙ(CONTENT×USER)"/>
<org.eventb.core.scVariable name="user" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.variable#_bHqLsqNuEeek3qZDwmMYTw" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scEvent name="chatcontenu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'">
<org.eventb.core.scAction name="'" org.eventb.core.assignment="user ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="init1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_bHpkoKNuEeek3qZDwmMYTw"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="content ≔ ∅ ⦂ ℙ(CONTENT)" org.eventb.core.label="init2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_bHpkoaNuEeek3qZDwmMYTw"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="chat ≔ ∅ ⦂ ℙ(USER×USER)" org.eventb.core.label="init3" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_bHpkoqNuEeek3qZDwmMYTw"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="active ≔ ∅ ⦂ ℙ(USER×USER)" org.eventb.core.label="init4" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_bHpko6NuEeek3qZDwmMYTw"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="muted ≔ ∅ ⦂ ℙ(USER×USER)" org.eventb.core.label="init5" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_bHpkpKNuEeek3qZDwmMYTw"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="chatcontent ≔ ∅ ⦂ ℙ(CONTENT×(USER×USER))" org.eventb.core.label="init6" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_bHpkpaNuEeek3qZDwmMYTw"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="owner ≔ ∅ ⦂ ℙ(CONTENT×USER)" org.eventb.core.label="init7" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#'|org.eventb.core.action#_8B7p86k4EeeVioCwPvnN6Q"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatcontenv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="creat_chat_session" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_bHsA46NuEeek3qZDwmMYTw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_bHsA46NuEeek3qZDwmMYTw|org.eventb.core.guard#_8B7p8qk4EeeVioCwPvnN6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2∉chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_bHsA46NuEeek3qZDwmMYTw|org.eventb.core.guard#_JI0nsKk5EeeVioCwPvnN6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_bHsA46NuEeek3qZDwmMYTw|org.eventb.core.parameter#_8B7p8Kk4EeeVioCwPvnN6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_bHsA46NuEeek3qZDwmMYTw|org.eventb.core.parameter#_8B7p8ak4EeeVioCwPvnN6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="chat ≔ chat∪{u1 ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_bHsA46NuEeek3qZDwmMYTw|org.eventb.core.action#_Be_aOanWEeeaxakKd9Dntw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatcontenw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="select_chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgahGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgahGEeepuZAizUZzqw|org.eventb.core.guard#_hqZqoqk6EeeVioCwPvnN6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2∈chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgahGEeepuZAizUZzqw|org.eventb.core.guard#_KO_lkKk5EeeVioCwPvnN6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgahGEeepuZAizUZzqw|org.eventb.core.parameter#_hqZqoKk6EeeVioCwPvnN6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgahGEeepuZAizUZzqw|org.eventb.core.parameter#_hqZqoak6EeeVioCwPvnN6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="active ≔ active{u1 ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgahGEeepuZAizUZzqw|org.eventb.core.action#_Be_aOqnWEeeaxakKd9Dntw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatcontenx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="chatting" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.guard#_Be_aM6nWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2∈chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.guard#_Be_aNKnWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2∉muted" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.guard#_Be_aNanWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u2 ↦ u1∉muted" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.guard#_Be_aNqnWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u1 ↦ u2∈active" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.guard#_Be_aN6nWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="c∈CONTENT ∖ content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.guard#_Be_aOKnWEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.parameter#_Be_aMqnWEeeaxakKd9Dntw" org.eventb.core.type="CONTENT"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.parameter#_Be_aMKnWEeeaxakKd9Dntw" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.parameter#_Be_aManWEeeaxakKd9Dntw" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="content ≔ content∪{c}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.action#_rFZskKnWEeeaxakKd9Dntw"/>
<org.eventb.core.scAction name="u4" org.eventb.core.assignment="chat ≔ chat∪{u2 ↦ u1}" org.eventb.core.label="act2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.action#_rFZskanWEeeaxakKd9Dntw"/>
<org.eventb.core.scAction name="u5" org.eventb.core.assignment="chatcontent ≔ chatcontent∪{c ↦ (u1 ↦ u2)}∪{c ↦ (u2 ↦ u1)}" org.eventb.core.label="act3" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.action#_uK8ryKnXEeeaxakKd9Dntw"/>
<org.eventb.core.scAction name="u6" org.eventb.core.assignment="owner ≔ owner∪{c ↦ u1}" org.eventb.core.label="act4" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzgqhGEeepuZAizUZzqw|org.eventb.core.action#_EI7pMKncEeeaxakKd9Dntw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconteny" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="delete_content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.guard#_uK8rw6nXEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2∈active" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.guard#_uK8rxKnXEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd4" org.eventb.core.predicate="c∈content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.guard#_uK8rxanXEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd5" org.eventb.core.predicate="c ↦ (u1 ↦ u2)∈chatcontent" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.guard#_uK8rxqnXEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.parameter#_uK8rwqnXEeeaxakKd9Dntw" org.eventb.core.type="CONTENT"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.parameter#_uK8rwKnXEeeaxakKd9Dntw" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.parameter#_uK8rwanXEeeaxakKd9Dntw" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="chatcontent ≔ chatcontent ∖ {c ↦ (u1 ↦ u2)}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tLzg6hGEeepuZAizUZzqw|org.eventb.core.action#_EI7pNqncEeeaxakKd9Dntw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatcontenz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="clear_content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.guard#_EI7pM6ncEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="c∈content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.guard#_EI7pNKncEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="c ↦ u∈owner" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.guard#_EI7pNancEeeaxakKd9Dntw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.parameter#_EI7pMqncEeeaxakKd9Dntw" org.eventb.core.type="CONTENT"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.parameter#_EI7pMancEeeaxakKd9Dntw" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="chatcontent ≔ {c} ⩤ chatcontent" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.action#_EI7pN6ncEeeaxakKd9Dntw"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="owner ≔ owner ∖ {c ↦ u}" org.eventb.core.label="act2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.action#_RTWmoKndEeeaxakKd9Dntw"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="content ≔ content ∖ {c}" org.eventb.core.label="act3" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakKhGEeepuZAizUZzqw|org.eventb.core.action#_kTIDUKndEeeaxakKd9Dntw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconten{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="delete_chat_session" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.guard#_mXzTAqnsEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2∈chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.guard#_mXzTA6nsEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2∈active" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.guard#_mXz6EKnsEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.parameter#_mXzTAKnsEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.parameter#_mXzTAansEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="chatcontent ≔ chatcontent ⩥ {u1 ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.action#_mXz6EansEeeHFdEvtaui5A"/>
<org.eventb.core.scAction name="u4" org.eventb.core.assignment="active ≔ active ∖ {u1 ↦ u2}" org.eventb.core.label="act2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.action#_Il8P8anwEeeHFdEvtaui5A"/>
<org.eventb.core.scAction name="u5" org.eventb.core.assignment="muted ≔ muted ∖ {u1 ↦ u2}" org.eventb.core.label="act3" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.action#_jydroanwEeeHFdEvtaui5A"/>
<org.eventb.core.scAction name="u6" org.eventb.core.assignment="chat ≔ chat ∖ {u1 ↦ u2}" org.eventb.core.label="act4" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakahGEeepuZAizUZzqw|org.eventb.core.action#_jyeSsqnwEeeHFdEvtaui5A"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconten|" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="mute_chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw|org.eventb.core.guard#_Il83A6nwEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2∈chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw|org.eventb.core.guard#_Il9eEqnwEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2∉muted" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw|org.eventb.core.guard#_jyeSsKnwEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw|org.eventb.core.parameter#_Il8P8KnwEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw|org.eventb.core.parameter#_Il83AKnwEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="muted ≔ muted∪{u1 ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMakqhGEeepuZAizUZzqw|org.eventb.core.action#_6YVsUKnwEeeHFdEvtaui5A"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconten}" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="unmute_chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw|org.eventb.core.guard#_jyeSsanwEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2∈chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw|org.eventb.core.guard#_W6uHsqnxEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2∈muted" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw|org.eventb.core.guard#_W6uHs6nxEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw|org.eventb.core.parameter#_Il83AanwEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw|org.eventb.core.parameter#_jydroKnwEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="muted ≔ muted ∖ {u1 ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMak6hGEeepuZAizUZzqw|org.eventb.core.action#_W6uHtKnxEeeHFdEvtaui5A"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconten~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="broadcast" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈user∧ul⊆user∧c∈CONTENT ∖ content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.guard#_kTTSYanxEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="{u} × ul⊆chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.guard#_kTTSYqnxEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.parameter#_W6uHsKnxEeeHFdEvtaui5A" org.eventb.core.type="CONTENT"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.parameter#_jydroqnwEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="ul" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.parameter#_jydro6nwEeeHFdEvtaui5A" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scAction name="um" org.eventb.core.assignment="content ≔ content∪{c}" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.action#_kTTSY6nxEeeHFdEvtaui5A"/>
<org.eventb.core.scAction name="un" org.eventb.core.assignment="owner ≔ owner∪{c ↦ u}" org.eventb.core.label="act3" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.action#_zGLJcKn0EeeHFdEvtaui5A"/>
<org.eventb.core.scAction name="uo" org.eventb.core.assignment="chatcontent ≔ chatcontent∪({c} × ({u} × ul))" org.eventb.core.label="act2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalKhGEeepuZAizUZzqw|org.eventb.core.action#_2v_t0KoKEeeZ7YPeurqf6Q"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconteo'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="forward" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈user∧ul⊆user∧c∈content" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.guard#_OkZgg6nyEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="{u} × ul⊆chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.guard#_OkZghKnyEeeHFdEvtaui5A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="chatcontent∩({c} × ({u} × user))≠(∅ ⦂ ℙ(CONTENT×(USER×USER)))" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.guard#_2wA78qoKEeeZ7YPeurqf6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.parameter#_2wAU4KoKEeeZ7YPeurqf6Q" org.eventb.core.type="CONTENT"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.parameter#_W6uHsanxEeeHFdEvtaui5A" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="ul" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.parameter#_kTSrUKnxEeeHFdEvtaui5A" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scAction name="um" org.eventb.core.assignment="chatcontent ≔ chatcontent∪({c} × ({u} × ul))" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalahGEeepuZAizUZzqw|org.eventb.core.action#_2wAU4aoKEeeZ7YPeurqf6Q"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="chatconteo(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="unselect_chat" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalqhGEeepuZAizUZzqw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈user∧u2∈user" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalqhGEeepuZAizUZzqw|org.eventb.core.guard#_BS-u8KoMEeeZ7YPeurqf6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2∈active" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalqhGEeepuZAizUZzqw|org.eventb.core.guard#_wXZDAKp4EeeZ7YPeurqf6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalqhGEeepuZAizUZzqw|org.eventb.core.parameter#_2wA78KoKEeeZ7YPeurqf6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalqhGEeepuZAizUZzqw|org.eventb.core.parameter#_2wA78aoKEeeZ7YPeurqf6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="active ≔ {u1} ⩤ active" org.eventb.core.label="act1" org.eventb.core.source="/whatsapp-lab1_test/machine0.bum|org.eventb.core.machineFile#machine0|org.eventb.core.event#_6tMalqhGEeepuZAizUZzqw|org.eventb.core.action#_2wA79KoKEeeZ7YPeurqf6Q"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>