Revised algorithm

Now we explain how revised algorithm check the inconsistency in the previous example.

L1: a]<2 [b;

L2: b]<2 [c;

L3: c]<2 [a;

Initial value:

begin(M)=0 end(M)=2;

bgein(a)=0 end(a)=2;

bgein(b)=0 end(b)=2;

begin(c)=0 end(c)=2;

L1:

bgein(b)=4 end(b)=6;

Propagation

(now L2 and L3 are marked as '0' ,so only end(b) will be propagated to M;)

end(M)=6;

L2:

begin(c)=8 end(c)=10;

propagation

(now L3 is marked with '0',so only end(c) will be propagated to M)

end(M)=10;

L3:

begin(a)=12 end(a)=14;

propagation

    S={L1,<a,M>}

    path={a};

        L1:

        begin(b)=16 end(b)=18;

        propagation

        S={L2,<b,M>}

        path={a,b}

            L2:

            begin(c)=20 end(c)=22;

            propagation

            S={L3,<c,M>}

            path={a,b,c}

                L3:

                here we find a is already in Path;

                and L3 will change begin(a)=24 end(a)=26 which

                is original propagation condition;

                So we stop here.

                In fact, if keep running it will cause a dead loop.