3.3.3 scan_state/2

Continuation.

Now control returns to the top-level call of scan/1, the database contains a new entry start(a2,1) and S is instantiated to 1. Next thing in scan/1 is a call to scan_state/2. This predicate is the most important part of our system. Here's the code:

scan_state(A,S):-
  state(A,S),!.                 % state already scanned?

The predicate consists of two clauses. The second one is the one that succeeds in our example, so let's look at it first. After unifying the two arguments A and S respectively with the the instruction cp(a1,b1) and the state name 1 in the head, the call to assert/1 in the first line of the body adds an entry state(cp(a1,b1),1) to the database. This marks state 1 as processed in copying cp(a1,b1). Next, it is checked if S is a final state. This is done using check_final/2. We will look at the code later. Suffice it to say for now that check_final/2 will not do anything and just succeed trivially in our example because state 1 isn't a final state.

The final lines of scan_state/2-predicate make use of a special Prolog construction similar to ``if-then-else''-constructions in imperative languages like Basic. This construction has the form (IF -> THEN;
ELSE).

So in the scan_state/2-predicate, the IF part contains a call to setof/3. Basically, this call gives us all states D which are the destination of a transition originating from state S over any symbol X in the automaton resulting from the operation that's just being performed. The result is a list bound to the variable Ds (``destinations''). Just as in a1 itself, we can only reach state 2 from 1 in the copy that we are making. So Ds=[2].

If setof/3 does not find any destinations, it fails, the ``if-then-else''-construction activates the ELSE-part. This part contains only the atom true, letting scan_state/2 succeed. But if setof/3 finds any destination-states, the list containing them is further processed.

Before we discuss how this is done, let's have a closer look at what happens ``within'' the setof/3-call in our example. Using the instantiations we've collected, the call looks as follows:

setof(D,X^trans(cp(a1,b1),1,X,D),Ds)

This means that trans(cp(a1,b1),1,X,D) is called and re-done until no further solutions are available. Like start/2, /trans/4 is implemented differently for all kinds of operations that can be specified. Here is the clause for cp:

trans(cp(A1,A2),S,D,X):-
  trans(A1,S,D,X),
  assert(trans(A2,S,D,X)).

If the original automaton A1 has a transition from S over X to D, then an according transition is asserted for its copy A2. The solution for D is the destination state of the transition found in the original automaton. In our example, a copy of the transition trans(a1,1,2,h) is asserted as trans(b1,1,2,h). And because trans(a1,1,2,h) is the only transition out of state 1 in a1, setof/3 has already finished its job and Ds is instantiated to [2] (as we've already said above).