Commit 2329056d authored by Matthew Fernandez's avatar Matthew Fernandez
Browse files

fix: perform quantifier loop comparison as signed

This was leading to the misc/pending-queue.m model terminating early with a
surprisingly small number of states. Some more explanation from the Github
issue:

  The misc/pending-queue.m model produces many fewer states (81) than it used to
  (147487952), which is unexpected. Bisecting indicates 79579fd5 is the first bad
  commit.
  ...
  The problem here is that commit 79579fd5 inadvertently caused the comparison in
  the loop emitted for a quantifier to become unsigned. A quantifier emits code
  that previously looked something like:

    const value_t step = VALUE_C(1);
    const value_t lb = VALUE_C(-1);
    const value_t ub = VALUE_C(3);
    for (value_t _ru1_i = lb; _ru_i <= ub; _ru_i += step) {
    ...

  After that commit, the emitted code looks like:

    const raw_value_t step = (raw_value_t)1;
    const raw_value_t lb = (raw_value_t)VALUE_C(-1);
    const raw_value_t ub = (raw_value_t)VALUE_C(3);
    for (raw_value_t _ru1_i = 1; _ru_i <= ub - lb + 1; _ru_i += step) {
    ...

  Now everything generally works out fine except in cases like the above when
  the range spans positive and negative values. Notice that the first iteration
  of the loop in the second case already has a false condition. The problem here
  is that the comparison was previously comparing value_ts and now it's
  comparing raw_value_ts. In a typical model this goes from comparing int8_t
  values to uint8_t values.

Github: closes #142 "pending-queue.m terminates exploration too early"
parent f3c1b183
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment