fix: track rule transitions in the state struct
This commit increases the size of the state struct by 8 bytes -- in checkers with counterexample traces enabled -- and uses this new member to print the transition rules in counterexample traces. The purpose of this is to side step a problem wherein trying to find the transition rule between two states actually *re-triggers* a checker error. Interestingly this case that recurses was not detected with the existing test suite because examples that trigger it simply take an exit as if they were a subordinate thread. The fact that print_transition never properly returns was uncovered when I tested the machine readable output on tests/error-statement.m. This example produced invalid XML because it never closed the "<error>" tag. This issue should now be resolved. As an aside, debugging this made me think the way CMurphi constructs counterexample traces is inherently wrong. I don't think it can correctly handle assertion and error failures (as opposed to invariants), but the problems are masked for similar reasons to the ones I describe above. I think extending CMurphi to add support for more than one error before terminating would encounter this issue.
parent
be33f5e1
Please register or sign in to comment