Repository navigation
Expand file tree
/
Copy pathmachine0.bum
More file actions
131 lines (131 loc) · 20.5 KB
/
Copy pathmachine0.bum
File metadata and controls
131 lines (131 loc) · 20.5 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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase" org.eventb.texttools.text_lastmodified="1507283693355" org.eventb.texttools.text_representation="machine machine0 sees ctx0 variables user content chat active muted chatcontent owner invariants @inv1 user ⊆ USER @inv2 content ⊆ CONTENT @inv3 chat ∈ user ↔ user // chat sessions @inv4 active ∈ user ⇸ user // active chat session @inv5 muted ∈ user ↔ user // muted sessions @inv6 active ⊆ chat // active chat sessions @inv7 muted ⊆ chat // muted chat sessions @inv8 chatcontent ∈ content ↔ chat // chat contents @inv9 owner ∈ content → user /* chat sessions inv10 chatcontent ∈ // users' chat content */ events event INITIALISATION then @init1 user ≔ ∅ @init2 content ≔ ∅ @init3 chat ≔ ∅ @init4 active ≔ ∅ // init7 chatcontent ≔ ∅ @init5 muted ≔ ∅ @init6 chatcontent ≔ ∅ @init7 owner ≔ ∅ end event creat_chat_session // US-01 any u1 u2 where @grd1 u1 ∈ user ∧ u2 ∈ user @grd2 u1 ↦ u2 ∉ chat then @act1 chat ≔ chat ∪ {u1 ↦ u2} end event select_chat // US-02 any u1 u2 where @grd1 u1 ∈ user ∧ u2 ∈ user @grd2 u1 ↦ u2 ∈ chat then @act1 active ≔ active {u1 ↦ u2} end event chatting // US-03 any u1 u2 c where @grd1 u1 ∈ user ∧ u2 ∈ user @grd2 u1 ↦ u2 ∈ chat @grd3 u1 ↦ u2 ∉ muted @grd4 u2 ↦ u1 ∉ muted @grd5 u1 ↦ u2 ∈ active @grd6 c ∈ CONTENT ∖ content then @act1 content ≔ content ∪ {c} @act2 chat ≔ chat ∪ {u2 ↦ u1} @act3 chatcontent ≔ chatcontent ∪ {c ↦ (u1 ↦ u2)} ∪ {c ↦ (u2 ↦ u1)} @act4 owner ≔ owner ∪ {c ↦ u1} end event delete_content // US-04 any u1 u2 c where @grd1 u1 ∈ user ∧ u2 ∈ user // @grd2 u1 ↦ u2 ∈ chat // useless due to the next guard @grd3 u1 ↦ u2 ∈ active @grd4 c ∈ content @grd5 (c ↦ (u1 ↦ u2)) ∈ chatcontent then @act1 chatcontent ≔ chatcontent ∖ {c ↦ (u1 ↦ u2)} end event clear_content // US-04 any u c where @grd1 u ∈ user @grd2 c ∈ content @grd3 c ↦ u ∈ owner then @act1 chatcontent ≔ {c} ⩤ chatcontent @act2 owner ≔ owner ∖ {c ↦ u} @act3 content ≔ content ∖ {c} end event delete_chat_session // US-05 	any u1 u2 	where 		@grd1 u1 ∈ user ∧ u2 ∈ user 		@grd2 u1 ↦ u2 ∈ chat 		@grd3 u1 ↦ u2 ∈ active 	then 		@act1 chatcontent ≔ chatcontent ⩥ {u1 ↦ u2} 		@act2 active ≔ active ∖ {u1 ↦ u2} 		@act3 muted ≔ muted ∖ {u1 ↦ u2} 		@act4 chat ≔ chat ∖ {u1 ↦ u2} end event mute_chat // US-06 	any u1 u2 	where 		@grd1 u1 ∈ user ∧ u2 ∈ user 		@grd2 u1 ↦ u2 ∈ chat 		@grd3 u1 ↦ u2 ∉ muted 	then 		@act1 muted ≔ muted ∪ {u1 ↦ u2} end event unmute_chat // US-07 	any u1 u2 	where 		@grd1 u1 ∈ user ∧ u2 ∈ user 		@grd2 u1 ↦ u2 ∈ chat 		@grd3 u1 ↦ u2 ∈ muted 	then 		@act1 muted ≔ muted ∖ {u1 ↦ u2} end event broadcast // US-08 any u ul c where 	@grd1 u ∈ user ∧ ul ⊆ user ∧ c ∈ CONTENT ∖ content 	@grd2 ({u} × ul) ⊆ chat then 	@act1 content ≔ content ∪ {c} 	@act3 owner ≔ owner ∪ {c ↦ u} 	@act2 chatcontent ≔ chatcontent ∪ ({c} × ({u} × ul)) end event forward // US-09 	any u ul c where 	@grd1 u ∈ user ∧ ul ⊆ user ∧ c ∈ content 	@grd2 ({u} × ul) ⊆ chat 	@grd3 chatcontent ∩ ({c} × ({u} × user)) ≠ ∅ then 	@act1 chatcontent ≔ chatcontent ∪ ({c} × ({u} × ul)) end event unselect_chat // US-10 any u1 u2 	where 	 @grd1 u1 ∈ user ∧ u2 ∈ user 	 @grd3 u1 ↦ u2 ∈ active 	then 	 @act1 active ≔ {u1} ⩤ active end end " version="5">
<org.eventb.core.seesContext name="_bHo9kKNuEeek3qZDwmMYTw" org.eventb.core.target="ctx0"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_bHpkoKNuEeek3qZDwmMYTw" org.eventb.core.assignment="user ≔ ∅" org.eventb.core.label="init1"/>
<org.eventb.core.action name="_bHpkoaNuEeek3qZDwmMYTw" org.eventb.core.assignment="content ≔ ∅" org.eventb.core.label="init2"/>
<org.eventb.core.action name="_bHpkoqNuEeek3qZDwmMYTw" org.eventb.core.assignment="chat ≔ ∅" org.eventb.core.label="init3"/>
<org.eventb.core.action name="_bHpko6NuEeek3qZDwmMYTw" org.eventb.core.assignment="active ≔ ∅" org.eventb.core.comment="init7 chatcontent ≔ ∅" org.eventb.core.label="init4"/>
<org.eventb.core.action name="_bHpkpKNuEeek3qZDwmMYTw" org.eventb.core.assignment="muted ≔ ∅" org.eventb.core.label="init5"/>
<org.eventb.core.action name="_bHpkpaNuEeek3qZDwmMYTw" org.eventb.core.assignment="chatcontent ≔ ∅" org.eventb.core.label="init6"/>
<org.eventb.core.action name="_8B7p86k4EeeVioCwPvnN6Q" org.eventb.core.assignment="owner ≔ ∅" org.eventb.core.label="init7"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_bHqLsqNuEeek3qZDwmMYTw" org.eventb.core.identifier="user"/>
<org.eventb.core.variable name="_bHqLs6NuEeek3qZDwmMYTw" org.eventb.core.identifier="content"/>
<org.eventb.core.variable name="_bHqLtKNuEeek3qZDwmMYTw" org.eventb.core.identifier="chat"/>
<org.eventb.core.variable name="_bHqLtaNuEeek3qZDwmMYTw" org.eventb.core.identifier="active"/>
<org.eventb.core.variable name="_bHqywKNuEeek3qZDwmMYTw" org.eventb.core.identifier="muted"/>
<org.eventb.core.invariant name="_bHqyxKNuEeek3qZDwmMYTw" org.eventb.core.label="inv1" org.eventb.core.predicate="user ⊆ USER"/>
<org.eventb.core.invariant name="_bHqyxaNuEeek3qZDwmMYTw" org.eventb.core.label="inv2" org.eventb.core.predicate="content ⊆ CONTENT"/>
<org.eventb.core.invariant name="_bHqyxqNuEeek3qZDwmMYTw" org.eventb.core.comment="chat sessions" org.eventb.core.label="inv3" org.eventb.core.predicate="chat ∈ user ↔ user"/>
<org.eventb.core.invariant name="_bHrZ0KNuEeek3qZDwmMYTw" org.eventb.core.comment="active chat session" org.eventb.core.label="inv4" org.eventb.core.predicate="active ∈ user ⇸ user"/>
<org.eventb.core.invariant name="_bHrZ0aNuEeek3qZDwmMYTw" org.eventb.core.comment="muted sessions" org.eventb.core.label="inv5" org.eventb.core.predicate="muted ∈ user ↔ user"/>
<org.eventb.core.invariant name="_bHrZ0qNuEeek3qZDwmMYTw" org.eventb.core.comment="active chat sessions" org.eventb.core.label="inv6" org.eventb.core.predicate="active ⊆ chat"/>
<org.eventb.core.invariant name="_bHsA4KNuEeek3qZDwmMYTw" org.eventb.core.comment="muted chat sessions" org.eventb.core.label="inv7" org.eventb.core.predicate="muted ⊆ chat"/>
<org.eventb.core.event name="_bHsA46NuEeek3qZDwmMYTw" org.eventb.core.comment="US-01" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="creat_chat_session">
<org.eventb.core.parameter name="_8B7p8Kk4EeeVioCwPvnN6Q" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_8B7p8ak4EeeVioCwPvnN6Q" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_8B7p8qk4EeeVioCwPvnN6Q" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_JI0nsKk5EeeVioCwPvnN6Q" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2 ∉ chat"/>
<org.eventb.core.action name="_Be_aOanWEeeaxakKd9Dntw" org.eventb.core.assignment="chat ≔ chat ∪ {u1 ↦ u2}" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tLzgahGEeepuZAizUZzqw" org.eventb.core.comment="US-02" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="select_chat">
<org.eventb.core.parameter name="_hqZqoKk6EeeVioCwPvnN6Q" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_hqZqoak6EeeVioCwPvnN6Q" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_hqZqoqk6EeeVioCwPvnN6Q" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_KO_lkKk5EeeVioCwPvnN6Q" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2 ∈ chat"/>
<org.eventb.core.action name="_Be_aOqnWEeeaxakKd9Dntw" org.eventb.core.assignment="active ≔ active {u1 ↦ u2}" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tLzgqhGEeepuZAizUZzqw" org.eventb.core.comment="US-03" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="chatting">
<org.eventb.core.parameter name="_Be_aMKnWEeeaxakKd9Dntw" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_Be_aManWEeeaxakKd9Dntw" org.eventb.core.identifier="u2"/>
<org.eventb.core.parameter name="_Be_aMqnWEeeaxakKd9Dntw" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name="_Be_aM6nWEeeaxakKd9Dntw" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_Be_aNKnWEeeaxakKd9Dntw" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2 ∈ chat"/>
<org.eventb.core.guard name="_Be_aNanWEeeaxakKd9Dntw" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2 ∉ muted"/>
<org.eventb.core.guard name="_Be_aNqnWEeeaxakKd9Dntw" org.eventb.core.label="grd4" org.eventb.core.predicate="u2 ↦ u1 ∉ muted"/>
<org.eventb.core.guard name="_Be_aN6nWEeeaxakKd9Dntw" org.eventb.core.label="grd5" org.eventb.core.predicate="u1 ↦ u2 ∈ active"/>
<org.eventb.core.guard name="_Be_aOKnWEeeaxakKd9Dntw" org.eventb.core.label="grd6" org.eventb.core.predicate="c ∈ CONTENT ∖ content"/>
<org.eventb.core.action name="_rFZskKnWEeeaxakKd9Dntw" org.eventb.core.assignment="content ≔ content ∪ {c}" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_rFZskanWEeeaxakKd9Dntw" org.eventb.core.assignment="chat ≔ chat ∪ {u2 ↦ u1}" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_uK8ryKnXEeeaxakKd9Dntw" org.eventb.core.assignment="chatcontent ≔ chatcontent ∪ {c ↦ (u1 ↦ u2)} ∪ {c ↦ (u2 ↦ u1)}" org.eventb.core.label="act3"/>
<org.eventb.core.action name="_EI7pMKncEeeaxakKd9Dntw" org.eventb.core.assignment="owner ≔ owner ∪ {c ↦ u1}" org.eventb.core.label="act4"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tLzg6hGEeepuZAizUZzqw" org.eventb.core.comment="US-04" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="delete_content">
<org.eventb.core.parameter name="_uK8rwKnXEeeaxakKd9Dntw" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_uK8rwanXEeeaxakKd9Dntw" org.eventb.core.identifier="u2"/>
<org.eventb.core.parameter name="_uK8rwqnXEeeaxakKd9Dntw" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name="_uK8rw6nXEeeaxakKd9Dntw" org.eventb.core.comment="@grd2 u1 ↦ u2 ∈ chat // useless due to the next guard" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_uK8rxKnXEeeaxakKd9Dntw" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2 ∈ active"/>
<org.eventb.core.guard name="_uK8rxanXEeeaxakKd9Dntw" org.eventb.core.label="grd4" org.eventb.core.predicate="c ∈ content"/>
<org.eventb.core.guard name="_uK8rxqnXEeeaxakKd9Dntw" org.eventb.core.label="grd5" org.eventb.core.predicate="(c ↦ (u1 ↦ u2)) ∈ chatcontent"/>
<org.eventb.core.action name="_EI7pNqncEeeaxakKd9Dntw" org.eventb.core.assignment="chatcontent ≔ chatcontent ∖ {c ↦ (u1 ↦ u2)}" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMakKhGEeepuZAizUZzqw" org.eventb.core.comment="US-04" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="clear_content">
<org.eventb.core.parameter name="_EI7pMancEeeaxakKd9Dntw" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_EI7pMqncEeeaxakKd9Dntw" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name="_EI7pM6ncEeeaxakKd9Dntw" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ user"/>
<org.eventb.core.guard name="_EI7pNKncEeeaxakKd9Dntw" org.eventb.core.label="grd2" org.eventb.core.predicate="c ∈ content"/>
<org.eventb.core.guard name="_EI7pNancEeeaxakKd9Dntw" org.eventb.core.label="grd3" org.eventb.core.predicate="c ↦ u ∈ owner"/>
<org.eventb.core.action name="_EI7pN6ncEeeaxakKd9Dntw" org.eventb.core.assignment="chatcontent ≔ {c} ⩤ chatcontent" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_RTWmoKndEeeaxakKd9Dntw" org.eventb.core.assignment="owner ≔ owner ∖ {c ↦ u}" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_kTIDUKndEeeaxakKd9Dntw" org.eventb.core.assignment="content ≔ content ∖ {c}" org.eventb.core.label="act3"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMakahGEeepuZAizUZzqw" org.eventb.core.comment="US-05" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="delete_chat_session">
<org.eventb.core.parameter name="_mXzTAKnsEeeHFdEvtaui5A" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_mXzTAansEeeHFdEvtaui5A" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_mXzTAqnsEeeHFdEvtaui5A" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_mXzTA6nsEeeHFdEvtaui5A" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2 ∈ chat"/>
<org.eventb.core.guard name="_mXz6EKnsEeeHFdEvtaui5A" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2 ∈ active"/>
<org.eventb.core.action name="_mXz6EansEeeHFdEvtaui5A" org.eventb.core.assignment="chatcontent ≔ chatcontent ⩥ {u1 ↦ u2}" org.eventb.core.label="act1"/>
<org.eventb.core.action name="_Il8P8anwEeeHFdEvtaui5A" org.eventb.core.assignment="active ≔ active ∖ {u1 ↦ u2}" org.eventb.core.label="act2"/>
<org.eventb.core.action name="_jydroanwEeeHFdEvtaui5A" org.eventb.core.assignment="muted ≔ muted ∖ {u1 ↦ u2}" org.eventb.core.label="act3"/>
<org.eventb.core.action name="_jyeSsqnwEeeHFdEvtaui5A" org.eventb.core.assignment="chat ≔ chat ∖ {u1 ↦ u2}" org.eventb.core.label="act4"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMakqhGEeepuZAizUZzqw" org.eventb.core.comment="US-06" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="mute_chat">
<org.eventb.core.parameter name="_Il8P8KnwEeeHFdEvtaui5A" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_Il83AKnwEeeHFdEvtaui5A" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_Il83A6nwEeeHFdEvtaui5A" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_Il9eEqnwEeeHFdEvtaui5A" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2 ∈ chat"/>
<org.eventb.core.guard name="_jyeSsKnwEeeHFdEvtaui5A" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2 ∉ muted"/>
<org.eventb.core.action name="_6YVsUKnwEeeHFdEvtaui5A" org.eventb.core.assignment="muted ≔ muted ∪ {u1 ↦ u2}" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMak6hGEeepuZAizUZzqw" org.eventb.core.comment="US-07" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="unmute_chat">
<org.eventb.core.parameter name="_Il83AanwEeeHFdEvtaui5A" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_jydroKnwEeeHFdEvtaui5A" org.eventb.core.identifier="u2"/>
<org.eventb.core.guard name="_jyeSsanwEeeHFdEvtaui5A" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_W6uHsqnxEeeHFdEvtaui5A" org.eventb.core.label="grd2" org.eventb.core.predicate="u1 ↦ u2 ∈ chat"/>
<org.eventb.core.guard name="_W6uHs6nxEeeHFdEvtaui5A" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2 ∈ muted"/>
<org.eventb.core.action name="_W6uHtKnxEeeHFdEvtaui5A" org.eventb.core.assignment="muted ≔ muted ∖ {u1 ↦ u2}" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMalKhGEeepuZAizUZzqw" org.eventb.core.comment="US-08" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="broadcast">
<org.eventb.core.parameter name="_jydroqnwEeeHFdEvtaui5A" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_jydro6nwEeeHFdEvtaui5A" org.eventb.core.identifier="ul"/>
<org.eventb.core.parameter name="_W6uHsKnxEeeHFdEvtaui5A" org.eventb.core.identifier="c"/>
<org.eventb.core.action name="_kTTSY6nxEeeHFdEvtaui5A" org.eventb.core.assignment="content ≔ content ∪ {c}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_kTTSYanxEeeHFdEvtaui5A" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ user ∧ ul ⊆ user ∧ c ∈ CONTENT ∖ content"/>
<org.eventb.core.guard name="_kTTSYqnxEeeHFdEvtaui5A" org.eventb.core.label="grd2" org.eventb.core.predicate="({u} × ul) ⊆ chat"/>
<org.eventb.core.action name="_zGLJcKn0EeeHFdEvtaui5A" org.eventb.core.assignment="owner ≔ owner ∪ {c ↦ u}" org.eventb.core.label="act3"/>
<org.eventb.core.action name="_2v_t0KoKEeeZ7YPeurqf6Q" org.eventb.core.assignment="chatcontent ≔ chatcontent ∪ ({c} × ({u} × ul))" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMalahGEeepuZAizUZzqw" org.eventb.core.comment="US-09" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="forward">
<org.eventb.core.parameter name="_W6uHsanxEeeHFdEvtaui5A" org.eventb.core.identifier="u"/>
<org.eventb.core.parameter name="_kTSrUKnxEeeHFdEvtaui5A" org.eventb.core.identifier="ul"/>
<org.eventb.core.guard name="_OkZgg6nyEeeHFdEvtaui5A" org.eventb.core.label="grd1" org.eventb.core.predicate="u ∈ user ∧ ul ⊆ user ∧ c ∈ content"/>
<org.eventb.core.guard name="_OkZghKnyEeeHFdEvtaui5A" org.eventb.core.label="grd2" org.eventb.core.predicate="({u} × ul) ⊆ chat"/>
<org.eventb.core.parameter name="_2wAU4KoKEeeZ7YPeurqf6Q" org.eventb.core.identifier="c"/>
<org.eventb.core.action name="_2wAU4aoKEeeZ7YPeurqf6Q" org.eventb.core.assignment="chatcontent ≔ chatcontent ∪ ({c} × ({u} × ul))" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_2wA78qoKEeeZ7YPeurqf6Q" org.eventb.core.label="grd3" org.eventb.core.predicate="chatcontent ∩ ({c} × ({u} × user)) ≠ ∅"/>
</org.eventb.core.event>
<org.eventb.core.event name="_6tMalqhGEeepuZAizUZzqw" org.eventb.core.comment="US-10" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="unselect_chat">
<org.eventb.core.parameter name="_2wA78KoKEeeZ7YPeurqf6Q" org.eventb.core.identifier="u1"/>
<org.eventb.core.parameter name="_2wA78aoKEeeZ7YPeurqf6Q" org.eventb.core.identifier="u2"/>
<org.eventb.core.action name="_2wA79KoKEeeZ7YPeurqf6Q" org.eventb.core.assignment="active ≔ {u1} ⩤ active" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="_BS-u8KoMEeeZ7YPeurqf6Q" org.eventb.core.label="grd1" org.eventb.core.predicate="u1 ∈ user ∧ u2 ∈ user"/>
<org.eventb.core.guard name="_wXZDAKp4EeeZ7YPeurqf6Q" org.eventb.core.label="grd3" org.eventb.core.predicate="u1 ↦ u2 ∈ active"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_rFZskqnWEeeaxakKd9Dntw" org.eventb.core.identifier="chatcontent"/>
<org.eventb.core.invariant name="_rFZsk6nWEeeaxakKd9Dntw" org.eventb.core.comment="chat contents" org.eventb.core.label="inv8" org.eventb.core.predicate="chatcontent ∈ content ↔ chat"/>
<org.eventb.core.variable name="_EI7pOKncEeeaxakKd9Dntw" org.eventb.core.identifier="owner"/>
<org.eventb.core.invariant name="_EI7pOancEeeaxakKd9Dntw" org.eventb.core.comment="chat sessions inv10 chatcontent ∈ // users' chat content " org.eventb.core.label="inv9" org.eventb.core.predicate="owner ∈ content → user"/>
</org.eventb.core.machineFile>