When run from the command line, the determinacy checker has a few options to control its workings.
The -r option specifies that the checker should recursively check
files in such a way that it finds nondeterminacy caused by calls to
other nondeterminate predicates, whether they are declared so or
not. Also, predicates that appear to determinate will be treated as
such, whether declared nondet or not. This option is quite useful
when first running the checker on a file, as it will find all
predicates that should be either made determinate or declared nondet
at once. Without this option, each time a nondet declaration is
added, the checker may find previously unnoticed nondeterminacy.
For example, if the original example above, without any nondet
declarations, were checked with the -r option, the output would
be:
* Non-determinate: user:parent/2 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: user:parent/2 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: user:is_parent/1 (clause 1)
* Calls nondet predicate user:parent/2.
The -d option causes the tool to print out the needed nondet
declarations. These can be readily pasted into the source files.
Note that it only prints the nondet declarations that are not already
present in the files. However, these declarations should not be
pasted into your code without each one first being checked to see if
the reported nondeterminacy is intended.
The -D option is like -d, except that it prints out all
nondet declarations that should appear, whether they are already in
the file or not. This is useful if you prefer to replace all old
nondet declarations with new ones.
Your code will probably rely on operator declarations and possibly term
expansion. The determinacy checker handles this in much the same way as
fcompile/1: you must supply an initialization file, using the
-i ifile option. Contrary to fcompile/1,
spdet will execute any operator declaration it encounters.