Tricking elm-test into solving a river-crossing puzzle

It’s a mini-blogpost in an Ellie. Written in a “literate programming” style - my comments-to-code ratio has never been so high, I imagine

https://ellie-app.com/nHNx6brVja1/0

7 Likes

Got it on the second try, you saved my saturday night

Great post, I have never thought about using test for this purpose! I tried another approach enumerating all possible game states only, and generating all valid paths instead of fuzz testing, but it was harder to develop and too easy to make a mistake because there are 15 states, and obviously in a real case like a webapp this would not be possible in complex cases. But very funny puzzle!

https://ellie-app.com/8RkX2Krgsa1/0

2 Likes

In many quick test implementations this trick is built in.

A lot of them have a `forAll` function which corresponds to elm test’s `fuzz` function and corresponds to a `∀` in logic.

They also have an `exists` function (which doesn’t exist in elm (pun not intended)) and corresponds to an `∃` in logic. It’s implementation follows logic:

`∃x.f(x) = !∀x.!f(x)`

Which is essentially what OP’s post does.

1 Like

Well, we are not alone:

It seems more common for those that use testing by enumeration (vs random generation), right?

I didn’t immediately follow your post, so let me go at it from a different angle, try to “braindump” what I think is happening in the Ellie and hopefully arrive at the same conclusion

``````there doesn't exist a list of Msgs x such that update(x, allLeft) == allRight
!∃x: update(x, allLeft) == allRight
``````

which can be said as

``````for all lists of Msgs x: update(x, allLeft) /= allRight
∀x: update(x, allLeft) /= allRight
``````

If we extract the `update(x, allLeft) == allRight` into predicate `p(x)`, then:

``````!∃x: p(x)
∀x: !p(x)
``````

which are the same. (Cool!)
Alright, so that agrees with your post. I had trouble reading the logic statement, but now I think I can translate it into English for myself:

exists x such that f(x) MEANS THAT not for all x is it true that not f(x)

Exactly.