-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAccessControl.bcm
87 lines (87 loc) · 22.3 KB
/
AccessControl.bcm
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
<?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">
<org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/TestRBAC/Context.bcc" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.seesContext#+"/>
<org.eventb.core.scInternalContext name="Context">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" org.eventb.core.predicate="finite(USERS)" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2" org.eventb.core.predicate="finite(GROUPS)" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.axiom#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3" org.eventb.core.predicate="IdPath∈ℕ → GROUPS" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.axiom#," org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="GROUPS" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.carrierSet#(" org.eventb.core.type="ℙ(GROUPS)"/>
<org.eventb.core.scCarrierSet name="USERS" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(USERS)"/>
<org.eventb.core.scConstant name="IdPath" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.constant#+" org.eventb.core.type="ℙ(ℤ×GROUPS)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="Contexu" org.eventb.core.label="inv2" org.eventb.core.predicate="UserToGroupMapping∈USERS ↔ GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contexv" org.eventb.core.label="inv4" org.eventb.core.predicate="GroupToGroupMapping∈GROUPS ↔ GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contexw" org.eventb.core.label="inv5" org.eventb.core.predicate="UserIndirectMembership∈USERS ↔ GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#3" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contexx" org.eventb.core.label="inv6" org.eventb.core.predicate="UserToGroupMapping⊆UserIndirectMembership" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#4" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contexy" org.eventb.core.label="inv7" org.eventb.core.predicate="GroupIndirectMembership∈GROUPS ↔ GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#6" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contexz" org.eventb.core.label="inv8" org.eventb.core.predicate="GroupToGroupMapping⊆GroupIndirectMembership" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#7" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contex{" org.eventb.core.label="inv9" org.eventb.core.predicate="∀rel⦂GROUPS×GROUPS·rel∈GroupIndirectMembership⇒(∃path⦂ℙ(ℤ×GROUPS)·path∈ℕ → GROUPS∧path(0)=(prj1 ⦂ ℙ(GROUPS×GROUPS×GROUPS))(rel)∧(∃k⦂ℤ·k∈ℕ∧path(k)=(prj2 ⦂ ℙ(GROUPS×GROUPS×GROUPS))(rel)∧(∀n⦂ℤ·n∈ℕ∧n<k⇒path(n) ↦ path(n+1)∈GroupToGroupMapping)))" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#9" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="Contex|" org.eventb.core.label="inv10" org.eventb.core.predicate="∀rel⦂USERS×GROUPS·rel∈UserIndirectMembership⇒(∃path⦂ℙ(ℤ×GROUPS)·path∈ℕ → GROUPS∧path(0)∈UserToGroupMapping[{(prj1 ⦂ ℙ(USERS×GROUPS×USERS))(rel)}]∧(∃k⦂ℤ·k∈ℕ∧path(k)=(prj2 ⦂ ℙ(USERS×GROUPS×GROUPS))(rel)∧(∀n⦂ℤ·n∈ℕ∧n<k⇒path(n) ↦ path(n+1)∈GroupToGroupMapping)))" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.invariant#C" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="UserIndirectMembership" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.variable#2" org.eventb.core.type="ℙ(USERS×GROUPS)"/>
<org.eventb.core.scVariable name="GroupIndirectMembership" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.variable#5" org.eventb.core.type="ℙ(GROUPS×GROUPS)"/>
<org.eventb.core.scVariable name="GroupToGroupMapping" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.variable#\/" org.eventb.core.type="ℙ(GROUPS×GROUPS)"/>
<org.eventb.core.scVariable name="UserToGroupMapping" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.variable#," org.eventb.core.type="ℙ(USERS×GROUPS)"/>
<org.eventb.core.scEvent name="GroupIndirectMembershiq" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#'">
<org.eventb.core.scAction name="'" org.eventb.core.assignment="UserToGroupMapping ≔ ∅ ⦂ ℙ(USERS×GROUPS)" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#'|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="GroupToGroupMapping ≔ ∅ ⦂ ℙ(GROUPS×GROUPS)" org.eventb.core.label="act3" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#'|org.eventb.core.action#)"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="UserIndirectMembership ≔ ∅ ⦂ ℙ(USERS×GROUPS)" org.eventb.core.label="act4" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#'|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="GroupIndirectMembership ≔ ∅ ⦂ ℙ(GROUPS×GROUPS)" org.eventb.core.label="act5" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#'|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="GroupIndirectMembershir" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="AddUserToGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="User∈USERS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="Group∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="Group" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(|org.eventb.core.parameter#(" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="User" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(|org.eventb.core.parameter#'" org.eventb.core.type="USERS"/>
<org.eventb.core.scAction name="Grouq" org.eventb.core.assignment="UserToGroupMapping ≔ UserToGroupMapping∪{User ↦ Group}" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(|org.eventb.core.action#+"/>
<org.eventb.core.scAction name="Grour" org.eventb.core.assignment="UserIndirectMembership ≔ UserIndirectMembership∪{User ↦ Group}" org.eventb.core.label="act2" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#(|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="GroupIndirectMembershis" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="AddGroupToGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="ContainingGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="MemberGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="ContainingGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1|org.eventb.core.parameter#'" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="MemberGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1|org.eventb.core.parameter#(" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scAction name="ContainingGrouq" org.eventb.core.assignment="GroupToGroupMapping ≔ GroupToGroupMapping∪{MemberGroup ↦ ContainingGroup}" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1|org.eventb.core.action#+"/>
<org.eventb.core.scAction name="ContainingGrour" org.eventb.core.assignment="GroupIndirectMembership ≔ GroupIndirectMembership∪{MemberGroup ↦ ContainingGroup}" org.eventb.core.label="act2" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#1|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="GroupIndirectMembershit" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ValidateIndirectGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="memberGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="containingGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="intermediateGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="memberGroup ↦ intermediateGroup∈GroupIndirectMembership" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="intermediateGroup ↦ containingGroup∈GroupToGroupMapping" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="memberGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.parameter#'" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="containingGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.parameter#(" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="intermediateGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.parameter#-" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scAction name="intermediateGrouq" org.eventb.core.assignment="GroupIndirectMembership ≔ GroupIndirectMembership∪{memberGroup ↦ containingGroup}" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#8|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="GroupIndirectMembershiu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RemoveGroupFromGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="ContainingGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="MemberGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="MemberGroup ↦ ContainingGroup∈GroupToGroupMapping" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="ContainingGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.parameter#'" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="MemberGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.parameter#(" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scAction name="ContainingGrouq" org.eventb.core.assignment="GroupToGroupMapping ≔ GroupToGroupMapping ∖ {MemberGroup ↦ ContainingGroup}" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.action#,"/>
<org.eventb.core.scAction name="ContainingGrour" org.eventb.core.assignment="GroupIndirectMembership ≔ GroupToGroupMapping ∖ {MemberGroup ↦ ContainingGroup}" org.eventb.core.label="act2" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.action#-"/>
<org.eventb.core.scAction name="ContainingGrous" org.eventb.core.assignment="UserIndirectMembership ≔ UserToGroupMapping" org.eventb.core.label="act3" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#@|org.eventb.core.action#."/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="GroupIndirectMembershiv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RemoveUserFromGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="User∈USERS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="Group∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="User ↦ Group∈UserToGroupMapping" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="Group" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.parameter#(" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="User" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.parameter#'" org.eventb.core.type="USERS"/>
<org.eventb.core.scAction name="Grouq" org.eventb.core.assignment="UserToGroupMapping ≔ UserToGroupMapping ∖ {User ↦ Group}" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.action#,"/>
<org.eventb.core.scAction name="Grour" org.eventb.core.assignment="UserIndirectMembership ≔ ({User} ⩤ UserIndirectMembership)∪(UserToGroupMapping ∖ {User ↦ Group})" org.eventb.core.label="act2" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#A|org.eventb.core.action#-"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="GroupIndirectMembershiw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ValidateIndirectUser" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="User∈USERS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="DirectGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="IndirectGroup∈GROUPS" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="User ↦ DirectGroup∈UserToGroupMapping" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="DirectGroup ↦ IndirectGroup∈GroupIndirectMembership" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="IndirectGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.parameter#)" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scParameter name="User" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.parameter#'" org.eventb.core.type="USERS"/>
<org.eventb.core.scParameter name="DirectGroup" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.parameter#(" org.eventb.core.type="GROUPS"/>
<org.eventb.core.scAction name="IndirectGrouq" org.eventb.core.assignment="UserIndirectMembership ≔ UserIndirectMembership∪{User ↦ IndirectGroup}" org.eventb.core.label="act1" org.eventb.core.source="/TestRBAC/AccessControl.bum|org.eventb.core.machineFile#AccessControl|org.eventb.core.event#B|org.eventb.core.action#\/"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>