walkthrough

DUAL MAS Walkthrough Testcase for Program Verification

Test graph G*

Cut Table for MAS ordering: a b j k i c p l o h m d n e g f

Cut Number	Cut Vertex Pair	Cut Graph		Forward Cut Coloring	Reverse Cut Coloring	Dual Coloring	Connectivity Upper Bound	ConnectivityBound Gap
Cut Number	Cut Vertex Pair	Size	Incidence	Forward Cut Coloring	Reverse Cut Coloring	Dual Coloring	Connectivity Upper Bound	ConnectivityBound Gap
1	a / b	4	1/4	1	4	4	4	0
2	b / j	6	2/4	2	3	4	4	0
3	j / k	6	3/3	3	2	4	4	0
4	k / i	8	4/5	3	3	5	5	0
5	i / c	7	3/5	2	2	4	4	0
6	c / p	7	3/5	2	2	4	4	0
7	p / l	8	4/4	3	3	5	5	0
8	l / o	8	4/5	3	2	4	6	2
9	o / h	10	5/6	3	2	4	5	1
10	h / m	9	4/5	2	1	3	5	2
11	m / d	11	4/5	3	2	4	4	0
12	d / n	9	4/4	3	1	4	4	0
13	n / e	8	4/3	3	1	4	4	0
14	e / g	6	4/2	3	1	4	4	0
15	g / f	4	4/1	4	1	4	4	0

Forward Search
Step I:

Vertex a is visited
Vertices b, i, j, k are reached for the first time.

The dashed line represents the cut: cut size = 4. (i.e. # of edges in cut is four)

Vertices represented in orange (visited) and yellow (reached but not visited by this step) are used to compute the cut incidence: 1 / 4. (i.e. 1/4 means one visited vertex and 4 unvisited vertices are incident to edges of the cut.)

Step II:

The next vertex to be visited is b (note: we had the choice between b, i, j, k.)

Vertex c is visited for the first time
Vertices k and i are reached for the second time. (note: a second edge color [purple] different color is used for these edges.)

The dashed line represents the cut: cut size = 6.
Vertices represented in orange and yellow are used to compute the cut incidence: 2/ 4

Step III:

The next vertex to be visited is j (note: we had the choice between j, k.. These two vertices have been reached two times.)

Vertex i is visited for the second time
Vertex k is reached for the third time. (note: a third edge color [green] is used to for this edges.)

The dashed line represents the cut: cut size = 6.

Vertices represented in orange and yellow are used to compute the cut incidence: 3/ 4

Step IV:

The next vertex to be visited is k.This is the only choice since it is at the highest level. It has been reached 3 times.

Vertex c is reached for the second time.
Vertex o, l, p are reached for the first time.
Vertex i is reached for the third time.

The dashed line represents the cut: cut size = 8.

Vertices represented in orange and yellow are used to compute the cut incidence: 4/ 5.

Step V:

The next vertex to be visited is i.

Vertex p is reached for the second time.
Vertex h, is reached for the first time.

Step VI:

The next vertex to be visited is c.

Step VII:

The next vertex to be visited is p.

Step VIII:

The next vertex to be visited is l.

Step IX:

The next vertex to be visited is o.

Step X:

The next vertex to be visited is h.

Step XI:

The next vertex to be visited is m.

Step XII:

The next vertex to be visited is d.

Step XIII

The next vertex to be visited is n.

Step XIV:

The next vertex to be visited is e.

Step XV:

The next vertex to be visited is g.

Step XVI:

The next vertex to be visited is f.

Forward search statistics:

Total edges colored	40
# colored 1 (orange)	15 (spanning tree)
# colored 2 (purple)	14 (one tree)
# colored 3 (green)	10 (three tree)
# colored 4 (blue)	1

Reverse Search

The search order to be respected is: f, g, e, n, d, m, h, o, l, p, c, i, k, j, b, a,
Step I:

Vertex f is visited
Vertices e, m, n, g are reached for the first time.

Step II:

Vertex g is visited
Vertices h, o are reached for the first time.
Vertex n is reached for the second time.

Step III:

According to our ordering the next vertex to be visited is e. Nevertheless vertex n is at level 2. Thus vertex n will have to be "downgraded" to the same level as e by "deleting" edge (g,n) from the reverse coloring process. This is represented by the purple dashed line.

Vertex e is visited
Vertices d, l are reached for the first time.
Vertex m is reached for the second time.

Step IV:

The next vertex to be visited is: n which is at level 1. Vertex m being at level 2 must be downgraded.

Vertices m, o and h are reached for the second time.

Step V:

The next vertex to be visited is d that is at level 1. Vertices m, o and h being at level 2 must be downgraded.

Vertex c is reached for the first time.
Vertices o and m are reached for the second time.

Step VI:

Vertex m is visited
Vertex l is reached for the second time.
Vertex o is reached for the third time.

Step VII:

The next vertex to be visited is h and h is at level 1. Vertices l and o being at levels 2 and 3 must be downgraded to level 1

Vertices i and p are reached for the first time.
Vertex o is reached for the second time.

Step VIII:

Vertex to be visited next is o.
Vertex k is reached for the first time.
Vertices l and p are reached for the second time.

Step IX:

Vertex to be visited next is l and l is at level 2.
Vertices c and k are visited for the second time.
Vertex p is visited for the third time.

Step X:

Vertex to be visited next is p and p is at level 3.
Vertex i is reached for the second time.
Vertex k is reached for the third time.

Step XI:

The next vertex to be visited is c that is at level 2. K which is at level 3 will have to be downgraded to level 2.

Vertex b is reached for the first time.
Vertex k is reached for the third time.

Step XII:

The next vertex to be visited is i and i is at level 2. Vertex k which is at level 3 will have to be downgraded to level 2.

Vertices a and i are reached for the first time.
Vertex k is reached for the third time.

Step XIII:

Vertex to be visited next is k and k is at level 3.
Vertices a, b, j are reached for the second time.

Step XIV:

Vertex j is visited.
Vertices a and b are reached for the third time.

Step XV:

Vertex b is visited.
Vertex a is reached for the fourth time.

Step XVI:

Vertex a is visited at level 4

Reverse search statistics:

Total edges colored	30
# colored 1 (orange)	15 (spanning tree)
# colored 2 (purple)	10 (one tree)
# colored 3 (green)	4 (three tree)
# colored 4 (blue)	1