Pre-translation rewriting is highly effective for random formulas, but ineffective for structured formulas [2,5]. To measure performance on scalable, non-random formulas we tested the tools on formulas that describe -bit binary counters with increasing values of . These formulas are irreducible by pre-translation rewriting, uniquely satisfiable, and represent a predictably-sized state space. Correctness is easily determined by checking for precisely the unique counterexample for each counter formula. We tested four constructions of binary counter formulas, varying two factors: number of variables and nesting of 's.
We can represent a binary counter using two variables: a counter variable and a marker variable to designate the beginning of each new counter value. Alternatively, we can use 3 variables, adding a variable to encode carry bits, which eliminates the need for -connectives in the formula. We can nest 's to provide more succinct formulas or express the formulas using a conjunction of unnested -sub-formulas.
Let be an atomic proposition. Then a computation over is a word in . By dividing into blocks of length , we can view as a sequence of -bit values, denoting the sequence of values assumed by an -bit counter starting at , and incrementing successively by . To simplify the formulas, we represent each block as having the most significant bit on the right and the least significant bit on the left. For example, for the blocks cycle through the values , , , and . For technical convenience, we use an atomic proposition to mark the blocks. That is, we intend to hold at point precisely when .
For to represent an -bit counter, the following properties need to hold:
For , these properties are captured by the conjunction of the following formulas:
Scalable counter formulas of this form are automatically generated by LTLcounter.pl. Usage: LTLcounter.pl number_of_bits
Note that this encoding creates formulas of length . A more compact encoding results in formulas of length . For example, we can replace formula (2) above with:
Scalable counter formulas of this form, with nested -operators, are automatically generated by LTLcounterLinear.pl. Usage: LTLcounterLinear.pl number_of_bits
We can eliminate the use of -connectives in the formula by adding an atomic proposition representing the carry bit. The required properties of an -bit counter with carry are as follows:
A 4-bit Binary Counter | ||||||||||
m | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 |
b | 0000 | 0001 | 0010 | 0011 | 0100 | 0101 | 0110 | 0111 | 1000 | 1001 |
c | 0000 | 0001 | 0000 | 0011 | 0000 | 0001 | 0000 | 0111 | 0000 | 0001 |
m | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 | 0001 | ... | ||
b | 1010 | 1011 | 1100 | 1101 | 1110 | 1111 | 0000 | ... | ||
c | 0000 | 0011 | 0000 | 0001 | 0000 | 1111 | 0000 | ... |
To describe the behavior of the counter, we describe six properties and AND them together. For example, here is the program output for a 4-bit counter:
For , these properties are captured by the conjunction of the following formulas.
Scalable counter formulas of this form, using a carry bit and no -operators, are automatically generated by LTLcounterCarry.pl. Usage: LTLcounterCarry.pl number_of_bits
Scalable counter formulas using a carry bit and nested -operators are automatically generated by LTLcounterCarryLinear.pl. Usage: LTLcounterCarryLinear.pl number_of_bits