Forward Rechability

Passed

Waiting

Final

Init

n,Z

INITIAL Passed := Ø;

Waiting := {(n0,Z0)}

REPEAT

- pick (n,Z) in Waiting

- if for some Z’ Z

(n,Z’) in Passed then STOP

- else (explore) add

{ (m,U) : (n,Z) => (m,U) }

to Waiting;

Add (n,Z) to Passed

UNTIL Waiting = Ø

or

Final is in Waiting

n,Z’

m,U

Init -> Final ?

Previous slide

Next slide

Back to first slide

View graphic version