When run from the command line, the determinacy checker has a few options to control its workings.
-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
declarations, were checked with the
-r option, the output would
* 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.
-d option causes the tool to print out the needed
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.
-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
qpc(1): you must supply an
initialization file, using the