Bug in tutorial example

[jokasimr]

In the tutorial, Model 2: reachability matrix seems to have a bug.

The example from the tutorial, with maximization added to illustrate issue:

$ graph.essence
given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
find reach : matrix indexed by [vertices, vertices] of bool
$ Adding maximization to illustrate that the constraint allows reach to be true for non-connected vertices 
maximizing sum u,v : vertices . toInt(reach[u, v])
such that
  forAll u,v : vertices . reach[u,v] =
    ((u = v) \/ ({u,v} in G) \/
    (exists w : vertices . ({u,w} in G) /\ reach[w,v])) $ this can be true without u, v being connected
find connected : bool
such that
  connected = (forAll u,v : vertices . reach[u,v])

With parameter file:

$ graph.param
letting n be 4
letting G be {{1, 2}, {3, 4}}

Running conjure solve -ac graph.essence graph.param produces the solution:

$ **Expected the reach matrix to not be full**.
language Essence 1.3

letting connected be true
letting reach be
        [[true, true, true, true; int(1..4)], [true, true, true, true; int(1..4)], [true, true, true, true; int(1..4)],
         [true, true, true, true; int(1..4)];
             int(1..4)]
$ Visualisation for reach
$ T T T T
$ T T T T
$ T T T T
$ T T T T

The issue seems to be that in the line (exists w : vertices . ({u,w} in G) /\ reach[w,v]) can be satisfied by setting reach[u, v] = true /\ reach[w, v] = true even if v is not actually reachable from either vertex.

Hope this is not some misunderstanding on my part. If so please disregard this issue.

Thank you for a great tool and amazing documentation!

[ozgurakgun]

Thanks for the report, tagging @ott2 since he wrote that example.

[ott2]

Thanks, this is definitely a bug.

Model 2 is implicitly assuming a particular variable ordering, and is essentially the same incomplete specification as Model 4. To make it correct we need to add a minimising statement, in the same way that Model 5 fixes Model 4.

[ozgurakgun]

Just wondering if you could have a go at fixing this one @ott2? I am thinking it'll be easier for you to fix it since you wrote the example.

[olexandr-konovalov]

@ozgurakgun is this fixed in https://github.com/conjure-cp/conjure/releases/tag/v2.4.0 ?

[ozgurakgun]

I don't think so. This is a bug in the docs, just to be clear.