"Such that" is failing

[jaimerson]

So I have the following code:

for_all {s, t, j} in such_that({s_, t_, j_} in {int, int, int} when(s_ < j_ and j_ < t_)) do
    #...
end

Because I need j to be a value between s and t. Seems correct. However, here's the output I'm getting:

I don't think this is the expected behaviour. (apologies in advance if this is my mistake and/or this is not the place to submit this kind of report)

[luc-tielen]

Most likely related to how the such_that macro is implemented in ExCheck since tuples can be represented differently in AST depending on if the number of elements equals to 2:

iex(1)> quote do: {1} {:{}, [], [1]} iex(2)> quote do: {1,2} {1, 2} iex(3)> quote do: {1,2, 3} {:{}, [], [1, 2, 3]}

Might look into this later if I have some time...

EDIT: actually I was completely wrong, problem could be in triq with the guard.. The following fails:

property "such that with 1 element" do for_all x in suchthat({x} in {int} when x_ < 0) do x < 0 end end

while the following succeeds:

property "such that with 1 element" do for_all x in suchthat({x} in {int} when x_ > 0) do x > 0 end end

The :suchthat_failed is triggered when suchthat can't generate a correct scenario after 100 (default) attempts.. maybe we need to open an issue on triq repo instead?

[parroty]

@jaimerson thanks for the report. @Primordus thanks for the analysis.

The :suchthat_failed is triggered when suchthat can't generate a correct scenario after 100 (default) attempts.. maybe we need to open an issue on triq repo instead?

I could simulate the same behavior, but haven't been able to identify the cause enough yet. Do you have any further insight regarding which part is causing failure? (It's using triq's internal functionality, and would like to isolate the issue if opening a issue).

As you indicated, it seems erlang:exit(suchthat_failed) is called in triq after failing to generate a correct scenario, but I'm not confident about its condition.

The following seems generating negative values, but your example (replacing 1 with 0) results in suchthat_failed. The other example x > 0 (which does not contain 0) seems working as you indicated.

property "such that with less than 1" do
  for_all {x} in such_that({x_} in {int} when x_ < 1) do
    IO.puts "x = #{x}"
    x < 1
  end
end

outputs

x = 0
.x = 0
.x = 0
.x = -3
.x = -3
.x = 0
.x = -5
.x = -5
.x = -2
.x = -2
...

and

property "such that with larger than 0" do
  for_all {x} in such_that({x_} in {int} when x_ > 0) do
    IO.puts "x = #{x}"
    x > 0
  end
end

outputs

x = 1
.x = 2
.x = 3
.x = 3
.x = 3
.x = 1
...

[luc-tielen]

Just played around some more, the following (even simpler case) also fails:

property "such that with 1 element" do for_all x in suchthat(x in int when x_ < 0) do IO.puts "x = #{x}" x < 1 end end

Maybe something wrong with the int generator / such that / combination of the 2? Following variations I checked fail: x < 0 x < -1 ... x > 1 x > 2 ... In short, x < N with N <= 0 or x > N with N >= 1..

Might be a good idea to write these same tests in Erlang and check if they fail there as well so we can pinpoint where it goes wrong or add some debug statements in triq. I suspect the int shrinking algorithm might be going in the wrong direction somehow and runs out after 100 tries? Can't look further into this today, maybe investigate some more during the week.

[devstopfix]

I have tested this with triq 1.2.0 and 1.3.0 and now it seems to work.

The original:

  property :stj_such_that_constraints do
    for_all {s, t, j} in such_that({s_, t_, j_} in {int(), int(), int()} when s_ < j_ and j_ < t_) do
      assert j > s, inspect([s, j, t])
      assert j < t, inspect([s, j, t])
    end
  end

An alternate formulation without using constraints:

  defp gen_sjt,
    do:
      [int(), pos_integer(), pos_integer()]
      |> bind(fn [s, dj, dt] -> {s, s + dj, s + dj + dt} end)

  property :sjt_bind do
    for_all {s, j, t} in gen_sjt() do
      assert j > s, inspect([s, j, t])
      assert j < t, inspect([s, j, t])
    end
  end

[devstopfix]

Testing from iex -S mix:

import :triq_dom

:triq_dom.suchthat([{int(), int(), int()}], fn [{a,b,c}] -> (a < b) and (b < c) end) |> sample
[
  [{6, 10, 12}],
  [{0, 3, 8}],
  [{-26, -15, -6}],
  [{-12, -11, 17}],
  [{-13, -7, 6}],
  [{-8, 0, 6}],
  [{-21, -15, 9}],
  [{7, 11, 13}],
  [{-13, 0, 13}],
  [{1, 9, 13}],
  [{-12, 9, 11}]
]