Database Reference
In-Depth Information
“insertion” processing described in Sect.
7.2.2
for the list
Y
=
S
(A,α
∗
)
, or during
S
OP
“deletion” processing described in Sect.
7.2.1
for the list
Y
=
(A,α
∗
)
given by
Definition
54
.
Output.
A database-mapping process-program
P
composed of a set of flattened
guarded equations with the set of process variables
p
k
∈
X
and an assignment
ass
:
X
→
S
where
S
⊆
Ob
DB
is the set of states.
0
,(
A
∅
,α
∗
)),(p
1
,A,(
,α
∗
))
1. Set
X
={
p
0
,p
1
}
,
S
Gr
={
(p
0
,
⊥
A
}
,thesetof
equations
E
={
(p
0
=
nil)
}
, the pointer to the variables
i
=
1.
2. Let
n
=|
Y
|
.If
n
=
0 then insert the equation
(p
i
=
A)
in
E
and goto 4.
If
n
≥
2 then set
N
=
j
=
0,
L
to be the empty list, and goto 3.
a,(
B
,α
1
)
∈
Y
.
Control loop
. If there exists an equation
(p
k
=
a.p
m
)
∈
E
with
(p
k
,A)
∈
π
1
,
2
S
Gr
and
(p
m
,B)
∈
π
1
,
2
S
Gr
such that
B
=
α
1
(
B
)
then insert
(p
i
=
A)
into
E
(i.e., interrupt a loop and close this path) and goto 4.
Otherwise, insert new process variable
p
i
+
1
in
X
,
(p
i
+
1
,α
1
(
Let
,α
1
))
B
),(
B
in
S
Gr
and the equation
(p
i
=
a.p
i
+
1
)
in
E
.Goto4.
3.
N
=
N
+
1. If
N
≤
n
goto 3.1.
Let
j
=|
L
|
be the set of elements in the list
L
.If
j
=
0(
L
is empty) then
j
L)
.Goto4.
3.1.
Control loop
. If there exists an equation
(p
k
=
insert
(p
i
=
A)
into
E
; Otherwise insert
(p
i
=
a.p
m
)
∈
E
with
α
1
(
(p
k
,A)
∈
π
1
,
2
S
Gr
and
(p
m
,B)
∈
π
1
,
2
S
Gr
such that
B
=
B
)
then (i.e.,
interrupt a loop and close this path) and goto 3.
Otherwise,
j
1. Insert
p
i
+
j
into
L
,
p
i
+
j
,p
i
+
j
+
n
in
X
,
(p
i
+
j
=
a.p
i
+
j
+
n
)
into
E
, and
(p
i
+
j
,A,(
=
j
+
,α
1
)),(p
i
+
j
+
n
,α
1
(
,α
1
))
into
B
B
),(
B
S
Gr
.
Goto 3.
4. If this process is interrupted by the administrator with an execution of the op-
eration '
nil
', then set
X
0
,(
A
∅
,α
∗
))
={
p
0
}
,
S
Gr
={
(p
0
,
⊥
}
, the set of equa-
and goto 6.
5. Continue the
forward
insertion (or
backward
deletion) chaining (a propaga-
tion) for the variable
p
m
, with the minimal index
m
such that it is not on the
left side of any equation in
E
. If there is no such variable, goto 6.
Set
(p
m
,A,(
tions
E
={
(p
0
=
nil)
}
,α
∗
))
α
∗
(
A
∈
S
Gr
, with
A
=
A
=
=
)
and
Y
S
(A,α
∗
)
(or
Y
S
OP
(A,α
∗
)
during the deletion processing) given by Definition
54
.
If
1 then set the index
i
to the value of this index of the
last
created
program-variable and goto 2. Otherwise insert the equation
(p
m
=
A)
into
E
and goto 5.
6. Stop. This process of generation of the new equations in this program
P
ends.
Return
the program
P
with equations in
E
and the assignment
ass
|
Y
|≥
:
X
→
S
(its graph is obtained by the projection on the first two columns in
S
Gr
).
Note that the
Control loop
is an additional filtering w.r.t. the filtering provided
by Definition
54
for computation of the sets
Y
=
S
(A,α
∗
)
(or
Y
=
S
OP
(A,α
∗
)
during
the deletion processing) which controls that the target database of a transition is
modified: by this control loop, we additionally control that such a transition is not a
repetition of an equal previously executed transition, in order to interrupt the infinite
