Database Reference
In-Depth Information
=
p
0
=⊥
0
,
p
1
=
3
(p
2
,p
3
,p
4
)
,(p
2
=
E
a
1
.p
5
),
B
3
)
.
(p
3
=
a
2
.p
6
),(p
4
=
a
3
.p
7
),(p
5
=
B
1
),(p
6
=
B
2
),(p
7
=
Let us consider the non-flattened (direct) transition system on the left, and the
flattened system (obtained from the algorithm '
DBprog
') on the right in the diagram
bellow. Notice that the branching in the (direct) diagram on the left is expressed
by the non-flattened equation
(p
1
=
3
(a
1
.p
2
,a
2
.p
3
,a
3
.p
4
))
while in the flattened
system on the right by the equation
(p
1
=
3
(ass(s
2
).p
2
, ass(s
3
).p
3
, ass(s
4
).p
4
))
which is substituted by the
flattened
equation
(p
1
=
3
(p
2
,p
3
,p
4
))
∈
E
.
Let us show that this replacement (i.e., flattening) is valid: we denote the solution of
the set of equations
E
for a variable
p
i
by
s
E
(p
i
)
and its value (i.e., denotation) by
T
(
s
E
(p
i
))
. For generality, we will demonstrate it for any branching node
p
i
with
n
≥
2 outgoing branches (in our case
i
=
1
,n
=
3):
T
s
E
(p
i
)
=
T
s
E
n
ass(p
i
+
1
).p
i
+
1
,...,ass(p
i
+
n
).p
i
+
n
n
ass(p
i
+
1
)
⊗
T
s
E
(p
i
+
n
)
,...,ass(p
i
+
n
)
⊗
T
s
E
(p
i
+
n
)
=+
n
ass(p
i
+
1
)
⊗
T
s
E
(a
1
.p
i
+
n
+
1
)
,...,ass(p
i
+
n
)
⊗
T
s
E
(a
n
.p
i
+
2
n
)
=+
n
ass(p
i
+
1
)
a
1
⊗
T
s
E
(p
i
+
n
+
1
)
,...,ass(p
i
+
n
)
a
n
⊗
T
s
E
(p
i
+
2
n
)
=+
⊗
⊗
(from
ass(p
i
+
k
)
1
,...,n
because
Ta
k
is the information flux from the instance-database
ass(p
i
+
k
)
⊗
a
k
=
T ass(p
i
+
k
)
∩
Ta
k
=
Ta
k
,k
=
=
ass(p
i
)
for all
k
=
1
,...,n
, and hence
Ta
k
⊆
T ass(p
i
+
k
)
. Here, in our example
ass(p
i
+
k
)
=
ass(p
i
)
=
A
)
n
a
1
⊗
T
s
E
(p
i
+
n
+
1
)
,...,a
n
⊗
T
s
E
(p
i
+
2
n
)
=+
n
T
a
1
.
s
E
(p
i
+
n
+
1
)
,...,
T
a
n
.
s
E
(p
i
+
2
n
)
=+
n
T
s
E
(a
1
.p
i
+
n
+
1
)
,...,
T
s
E
(a
n
.p
i
+
2
n
)
=+
