CLEM Home Page

Link of two Partial Orders

In our setting, only input variables of a system are connected to output variables of the other and conversely. Our approach allows an efficient link of two already sorted equation systems, to perform separated compilation, for instance. We don't need to launch the sorting algorithm from its initial step. Assume we want to link two sorted equation systems A and B with a common variable x. This latter is either an input variable of A and an output one of B or the opposite.Let us illustrate this linking algorithm on a small example. We consider two equations systems and their respective sort as it is shown in the following table:

A
a = x + y
b = x + ¬ y
c = a + t
d = a + c
e = a + t

a	b	c	d	e	x	y	t
(1; 1)	(1; 3)	(2; 2)	(3; 3)	(2; 3)	(0; 0)	(0; 0)	(0; 2)

B
y = m
z = a
v = w

a	m	v	w	y	z
(0; 0)	(0; 0)	(1; 1)	(0; 0)	(1; 1)	(1; 1)

A and B equation systems and their respective variables CanDate and MustDate computed according to our sorting algorithm

Let us denote C^A(a) (resp C^B(a)) the CanDate of a in A (resp B). Similarly, we will denote M^A(a) (resp M^B(a)) the MustDate of a in A (resp in B). To link equation system A with equation system B, we only consider their common variables (y and a).

We consider a. We compute &Delta^C(a) = |C^A(a) - C^B(a)|, thus since C^B(a) = 0 and C^A(a) =1 ,we shift by &Delta^C(a) the CanDate of a and the variable in its can dependency in B. In B we have the dependency a->z, thus we shift the CanDate of a and z. We have a similar situation for the must date of a thus we perform the same shift.

We consider y. We compute &Delta^C(y) and since C^A(y) = 0 and C^B(y) =1, we shift in equation A the CanDate of y and all the variables in its can dependency. In A, we have the following can dependencies: d -> c ->a -> y; e -> a -> y; b -> y; Thus a, b. c. d, e are can dependencies of y in A and we shift their CanDate by &Delta^C(y). But, doing that we change the Candate of a which is a common variable already considered. Thus, we must also increase the CanDate of the variables in the can dependency of a in B in order to maintain the coherency previously set. The result of the link algorithm for A and B is detailed in the following box:

Linking A with B

a	b	c	d	e	x	y	z
(1,1)	(1,3)	(2,2)	(3,3)	(2,3)	(0,0)	(0,0)	(0,2)
		&Delta^C(a)	+	&Delta^M(a)	&darr
(1,1)	(1,3)	(2,2)	(3,3)	(2,3)	(0,0)	(0,0)	(0,2)
		&Delta^C(y)	+	&Delta^M(y)	&darr
(2,2)	(2,4)	(3,3)	(4,4)	(3,4)	(0,0)	(1,1)	(0,2)
&rarr	&rarr	&rarr	&rarr	&rarr	&rarr	&rarr	&rarr
(2,2)	(2,4)	(3,3)	(4,4)	(3,4)	(0,0)	(1,1)	(0,2)

a	m	v	w	y	z
(0,0)	(0,0)	(1,1)	(0,0)	(1,1)	(1,1)
		&Delta^C(a)	+	&Delta^M(a)	&darr
(1,1)	(0,0)	(1,1)	(0,0)	(1,1)	(2,2)
		&Delta^C(y)	+	&Delta^M(y)	&darr
(1,1)	(0,0)	(1,1)	(0,0)	(1,1)	(2,2)
+1					+1
(2,2)	0,0)	(1,1)	(0,0)	(1,1)	(3,3)

a	b	c	d	e	m	v	w	x	y	z	t
(2,2)	(2,4)	(3,3)	(4,4)	(3,4)	(0,0)	(1,1)	(0,0)	(0,0)	(1,1)	(3,3)	(0,2)

Sorting1

Sorting2

Sorting3

0:	m x v t
1:	y = m
	v = w
2:	b = x + ¬y
	a = x + y
3:	c = a + t
	z = a
	e = a + t
4:	d = a + c

0:	m x v t
1:	y = m
	v = w
2:	a = x + y
3:	b = x + ¬y
	c = a + t
	z = a
4:	e = a + t
	d = a + c

0:	m x v t
1:	y = m
	v = w
2:	a = x + y
3:	c = a + t
	z = a
4:	b = x + ¬y
	e = a + t
	d = a + c

Different valid sorting hold for A linked with B according to CanDate and MustDate computation. We get 5 equation levels. In each level, equations are independent and can be evaluated whatever the order is. A variable can be evaluated in each level between its CanDate and its MustDate. For instance, the equation that defines b can be evaluated either at level 2, or 3 or 4.