herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
215 stars 54 forks source link

[asl] Fix the non-determinstic ASL primitive `somebool` #900

Closed maranget closed 1 month ago

maranget commented 1 month ago

Before, the evaluation of the somebool primitive by "ASLSem" was yielding no candidate, because of some unsolved equations. Now, we have two candidates, as expected.

As an example the following litmus test now yields two candidates:

ASL non-deterministic

{ }

// Non deterministically returns 1 or 2
func g() => integer
begin
  let b = SomeBoolean();
  if b then
    return 1;
  end
  return 2;
end

func main() => integer
begin
  let z = g();
  return 0;
end

locations [0:main.0.z;]
maranget commented 1 month ago

Merged, as being a (small) bug fix.