2.10.1 The Byrd Box Model And Ports

Standard Prolog debugging tools are built around the so-called "Byrd Box Model" or "4 Port Model" which models each predicate in a Prolog program as a state machine ("box") that transitions through states ("ports") as a program is evaluated. The developer can ask the engine to pause for program inspection when it reaches specific ports or predicates.

As we go through this overview, remember that a "port" is just another word for a "state" in the state machine that each predicate transitions through during evaluation. The state machine is called a "box" because it is drawn like this:

                *--------------------------------------*
         Call   |                                      |   Exit
     ---------> +  descendant(X,Y) :- offspring(X,Y).  + --------->
                |                                      |
                |  descendant(X,Z) :-                  |
     <--------- +     offspring(X,Y), descendant(Y,Z). + <---------
         Fail   |                                      |   Redo
                *--------------------------------------*

The standard ports are: call, redo, exit and fail. SWI-Prolog extends this with two more: unify and exception. Each trace happens at a particular phase of predicate resolution. Recall that when resolving or "proving" a predicate, the Prolog engine:

1. Collects all rules that might match by having a head with the same name and number of arguments
   • call is traced, once, if any rules might match.
   • redo is also traced when the engine backtracks to find the next matching rule.

2. Finds the next matching rule whose head can be unified with the predicate
   • unify is traced with the results of unification if one is found.
   • fail is traced if no rule heads can be unified.

3. Applies variable assignments from unification to clauses in the rule body and continues at #1 with the updated clauses
4. After all of the body clauses of the matched rule have either succeeded, failed, or thrown an exception:
   • exit is traced if all of them succeeded (meaning this rule is true).
   • fail is traced if any of them failed (meaning this rule is false).
   • exception is traced if any of them threw an exception.

   This means there can be a lot of traces between the initial call and the end of tracing for a particular predicate.