9.7.5 Options

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 nondet declarations, were checked with the -r option, then 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.