3.3.4 Recursion

Continuation.

Now finally we come to the THEN-part in scan_state/2. It consists in calling scan_states/2 (plural!) on the Ds produced by the preceding setof/3-call. The scan_states/2-predicate recursively calls scan_state/2 (singular!) on every state on Ds:

scan_states(A,[S|Ss]):-
  scan_state(A,S),              % scan state from state list
  scan_states(A,Ss).            % go to next state from state list

scan_states(_,[]).              % state list already emptied?

In our example, this means that the transition trans(a1,2,3,a) is copied to trans(a2,2,3,a). Then the next level of the recursion is entered by calling scan_states/2 again, this time on Ds=[3]. Now there are two transitions. This means that Ds will have two members: [2,4]. State 2 has already been processed, and state 4 for has no outgoing transitions. This indicates that a1 has been fully traversed and the next call to scan_states/2 should end the recursion.

How is this done? For state 2, the one that has already been processed, the first clause of scan_state/2 will succeed, because the database contains the entry state(cp(a1,b1),2) that was asserted when state 2 was processed for the first time. This means that no further recursive level will be entered. For state 4, recursion will end simply because setof/3 in scan_state/2 won't find any transitions and so Ds will be empty.

Finally notice that state 4 is the final state of a1. For this reason, the call to check check_final/2 in the second clause of scan_state/2 will not just trivially succeed. Rather it will really do something before it succeeds. Let's have a look at the code:

check_final(A,S):-
  final(A,S),!.                 % final states receive special treatment

check_final(_,_).               % non-final states: no processing necessary - just return true

The first clause contains a call to final/2. This predicate is again implemented differently for cp, intersection and union. Here's the clause for cp:

final(cp(A1,A2),S):-
  final(A1,S),
  assert(final(A2,S)).

If S is a final state in the original A1, an according final state is asserted for the copy A2. In our example, the entry final(b1,2) will be asserted. For all non-final states, the above clause of final/2 will fail and the second clause of check_final/2 will succeed without any further actions.

Summing up, after running scan(cp(a1,b1)), the following will have happened:

• Due to the call to start/2 in scan/1, the database will contain the entry:

  start(b1,1)

• The calls to trans/2 in the second clause of scan_state/2 will have added:

  trans(b1,1,2,h).
trans(b1,2,3,a).
trans(b1,3,4,!).
trans(b1,3,2,h).

• The call to final/2 in check_final/2 will have added:

  final(b1,4).

That's a full copy of a1. Additionally, the database will contain the entries:

state(cp(a1,b1),1).
state(cp(a1,b1),2).
state(cp(a1,b1),3).
state(cp(a1,b1),4).

These were asserted in scan_state/2 as control information and can be retracted.