||::(
    1 -> 2 ;
    1 -> 3 -> 4 -> 3 -> 2 ;

    trace a path, starting from 1
)

|:: ($A -> $B -> $C)|
    :: $A is connected to $B
    :: ($B -> $C)
|:: ($A -> $B)|
    :: $A is connected to $B
|:: ;|
    :: clean up

|:: (trace a path, starting from $A)|
    :: visit $A
    :: trace a path

|:: $A is connected to $B|
    :connections: $A $B

|:: visit $A|
    :: mark $A as visited
    :: get neighbors for $A
    :: cross off any visited neighbors

|:: trace a path? :neighbors: $A|
    :: visit $A
|:: trace a path|

|:: get neighbors for $A :no more connections:|
|:: get neighbors for $A? :connections: $A $B?|
    :: next connection :neighbors: $B
|:: get neighbors for $A?|
    :: next connection

|:: next connection :connections: $A $B|
    :checked connections: $A $B
|:: next connection|
    :: reset connections
    :no more connections:

|:: mark $A as visited :yes:|
|:: mark $A as visited :no:|
    :visited: $A
|:: mark $A as visited?|
    :: check if $A has been visited before

|:: check if $A has been visited before  :visited: $A?|
    :: reset visited :yes:
|:: check if $A has been visited before? :visited: $B|
    :checked visited: $B
|:: check if $A has been visited before|
    :: reset visited :no:

|:: cross off any visited neighbors? :yes: :neighbors: $A|
|:: cross off any visited neighbors? :no:  :neighbors: $A|
    :checked neighbors: $A
|:: cross off any visited neighbors? :neighbors: $A?|
    :: check if $A has been visited before
|:: cross off any visited neighbors|
    :: reset neighbors

|:: reset connections? :checked connections: $A $B|
    :connections: $A $B
|:: reset visited? :checked visited: $A|
    :visited: $A
|:: reset neighbors? :checked neighbors: $A|
    :neighbors: $A
|:: reset $|

|:: clean up? :neighbors: $A|
|:: clean up? :visited: $A|
|:: clean up|