In other words, if the result for a state is q, and the bound p falls in the range
[q-e,q+e] where is the error bound from model checking computations, then an
error is generated rather than producing a potentially incorrect true/false result.
Explicit model checking engine only for now.
Test cases are added, and some (unrelated) existing regression tests with dubiously
close bound checks are fixed.
Dave Parker