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 be
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
declarations, were checked with the -r option, the output
* 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
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
The -D option is like -d, except that it prints out
nondet declarations that should appear, whether they
are already in the file or not. This is useful if you prefer to replace
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.