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 the following way: you must supply an initialization file, using the -i ifile option. spdet will execute any operator declaration it encounters.