Operation of the script is straightforward: prepare an input file that describes the truth table for paths through a prime, and run tracecase with that file as its standard input.
Because in most truth tables the number of cases is larger than the number of variables, we'll rotate the truth table so that each column is one case, and each row is one condition. This allows us to annotate each row of the truth table with a description of the corresponding condition.
Here is an input file representing the prime described in Section 2.3, “Application example”:
TFF a==0 XFT b > 0
Input to the script, then, consists of a set of lines, one per condition. Each line starts with a set of truth values, each of which is either T, F, or X (case-insensitive), optionally followed by at least one whitespace character and the description of the condition.
The first three columns of the above sample input files represent the three cases, corresponding to the three different paths through the code.
If the script detects no errors, it produces no output. It will detect two types of errors:
Cases that are not covered in the truth table.
Cases that are covered by more than set of inputs.
Here is a sample run demonstrating uncovered cases. In this example, four combinations of inputs do not correspond to the cases listed.
$ tracecase tff C1 xft C2 tft C3 FFT: uncovered FTF: uncovered TFF: uncovered TTF: uncovered
The first error messages tells us that there are no columns in the table that match the case (C1′ ∧ C2′ ∧ C3). The second line says there is no match for (C1′ ∧ C2 ∧ C3′), and so forth.
Here is an example of multiply-covered cases.
$ tracecase xtft ttff TT: covers 2 cases: XT TT
In the above example, the case where C1 and C2 are both true
matches both “
XT” and “
TT”, reading down the first two columns.