quint verify reports an unsound counterexample

[konnov]

When I run quint verify on river.qnt as follows:

quint verify --max-steps=50 --invariant=noSolution river.qnt

I rightfully reports a counterexample, but the contents of the counterexample is definitely is not what I expected:

$ quint verify --max-steps=50 --invariant=noSolution river.qnt
An example execution:

[State 0]
{
  boat: Set(),
  destination: Set(),
  origin: Set("cabbage", "farmer", "goat", "wolf")
}

[State 1]
{
  boat: Set("cabbage", "farmer", "goat", "wolf"),
  destination: Set(),
  origin: Set("cabbage", "wolf")
}

[State 2]
{
  boat: Set(),
  destination: Set("farmer", "goat"),
  origin: Set("cabbage", "wolf")
}
...

The boat should carry at most one item, in addition to the farmer. We should find which part of the pipeline contains a bug.

[konnov]

We should run it against the older version of Apalache, before the arena refactoring. The TLA+ file can be extracted when running the server as:

$APALACHE_HOME/bin/apalache-mc server --write-intermediate=true

[konnov]

@thpani, @Kukovec, ideas?

[thpani]

have you checked if the translation is correct?

[konnov]

It seems to be like how I expected it.

[Kukovec]

Could it be that because of

quint/examples/puzzles/river/river.qnt

Lines 52 to 53 in 7a1079e

	boat' = boat.union(toEmbark),
	origin' = origin.exclude(toEmbark),

and the fact that toEmbark is nondet, it is getting independently computed 2x?

[konnov]

-------------------------- MODULE 12_OutAnalysisPass --------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache

VARIABLE
  (*
    @type: Set(Str);
  *)
  origin

VARIABLE
  (*
    @type: Set(Str);
  *)
  boat

VARIABLE
  (*
    @type: Set(Str);
  *)
  destination

(*
  @type: (() => Bool);
*)
Init_si_0000 ==
  origin' := { "wolf", "goat", "cabbage", "farmer" }
    /\ boat' := {}
    /\ destination' := {}

(*
  @type: (() => Bool);
*)
Next_si_0000 ==
  "farmer" \in boat
    /\ boat' := {}
    /\ destination' := (destination \union boat)
    /\ origin' := origin

(*
  @type: (() => Bool);
*)
Next_si_0001 ==
  "farmer" \in boat
    /\ boat' := {}
    /\ origin' := (origin \union boat)
    /\ destination' := destination

(*
  @type: (() => Bool);
*)
Next_si_0002 ==
  "farmer" \in origin
    /\ Skolem((\E s$1 \in SUBSET origin:
      (Cardinality(s$1) <= 2 /\ "farmer" \in s$1)
        /\ (((~(\A t_2$1 \in { "goat", "cabbage" }:
                t_2$1 \in origin /\ ~(t_2$1 \in s$1))
              \/ ("farmer" \in origin /\ ~("farmer" \in s$1)))
            /\ (~(\A t_5$1 \in { "goat", "wolf" }:
                t_5$1 \in origin /\ ~(t_5$1 \in s$1))
              \/ ("farmer" \in origin /\ ~("farmer" \in s$1))))
          /\ boat' := (boat \union s$1)
          /\ origin' := { t_7$1 \in origin: ~(t_7$1 \in s$1) }
          /\ destination' := destination)))

(*
  @type: (() => Bool);
*)
Next_si_0003 ==
  "farmer" \in destination
    /\ Skolem((\E s$2 \in SUBSET destination:
      (Cardinality(s$2) <= 2 /\ "farmer" \in s$2)
        /\ (((~(\A t_9$1 \in { "goat", "cabbage" }:
                t_9$1 \in destination /\ ~(t_9$1 \in s$2))
              \/ ("farmer" \in destination /\ ~("farmer" \in s$2)))
            /\ (~(\A t_c$1 \in { "goat", "wolf" }:
                t_c$1 \in destination /\ ~(t_c$1 \in s$2))
              \/ ("farmer" \in destination /\ ~("farmer" \in s$2))))
          /\ boat' := (boat \union s$2)
          /\ destination' := { t_e$1 \in destination: ~(t_e$1 \in s$2) }
          /\ origin' := origin)))

(*
  @type: Bool;
*)
VCInv_si_0 == ~(origin = {}) \/ ~(boat = {})

(*
  @type: Bool;
*)
VCNotInv_si_0 == origin = {} /\ boat = {}

================================================================================

[thpani]

TLA+ looks good, I would also guess arenas:
boat in state #1 is wrong, but it somehow seems to have been right going into state #2.

[Kukovec]

Does running the TLA produce the same witness purely in Apalache?

[thpani]

Trace above is from the translated TLA+:

--------------------------- MODULE River ---------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache

VARIABLE
  (*
    @type: Set(Str);
  *)
  origin

VARIABLE
  (*
    @type: Set(Str);
  *)
  boat

VARIABLE
  (*
    @type: Set(Str);
  *)
  destination

(*
  @type: ((Set(Str)) => Bool);
*)
isSafe(location) ==
  ({ "goat", "cabbage" } \subseteq location => "farmer" \in location)
    /\ ({ "goat", "wolf" } \subseteq location => "farmer" \in location)

(*
  @type: (() => Bool);
*)
init ==
  origin' := { "wolf", "goat", "cabbage", "farmer" }
    /\ boat' := {}
    /\ destination' := {}

(*
  @type: (() => Bool);
*)
embarkOrigin ==
  "farmer" \in origin
    /\ (\E toEmbark \in {
      s \in SUBSET origin:
        Cardinality(s) <= 2 /\ "farmer" \in s
    }:
      isSafe((origin \ toEmbark))
        /\ boat' := (boat \union toEmbark)
        /\ origin' := (origin \ toEmbark)
        /\ destination' := destination)

(*
  @type: (() => Bool);
*)
disembarkDestination ==
  "farmer" \in boat
    /\ boat' := {}
    /\ destination' := (destination \union boat)
    /\ origin' := origin

(*
  @type: (() => Bool);
*)
embarkDestination ==
  "farmer" \in destination
    /\ (\E toEmbark \in {
      s \in SUBSET destination:
        Cardinality(s) <= 2 /\ "farmer" \in s
    }:
      isSafe((destination \ toEmbark))
        /\ boat' := (boat \union toEmbark)
        /\ destination' := (destination \ toEmbark)
        /\ origin' := origin)

(*
  @type: (() => Bool);
*)
disembarkOrigin ==
  "farmer" \in boat
    /\ boat' := {}
    /\ origin' := (origin \union boat)
    /\ destination' := destination

(*
  @type: (() => Bool);
*)
safety == isSafe(origin) /\ isSafe(boat) /\ isSafe(destination)

(*
  @type: (() => Bool);
*)
noSolution == origin /= {} \/ boat /= {}

(*
  @type: (() => Bool);
*)
consistency ==
  origin \intersect destination = {}
    /\ origin \intersect boat = {}
    /\ boat \intersect destination = {}

(*
  @type: (() => Bool);
*)
step ==
  embarkOrigin
    \/ disembarkDestination
    \/ embarkDestination
    \/ disembarkOrigin

================================================================================

[Kukovec]

interestingly, when I pass --inv=noSolution Apalache finds a conterexample which violates consistency, but with
--inv=consistency it finds no conterexample for the same length...

[konnov]

Yeah, I tried the same. So it is probably model reconstruction.

[konnov]

Can you try noSolution /\ consistency?

[Kukovec]

I did that too, same CE as just noSolution

[konnov]

Just an update, it is not a bug in the transpiler but a bug in the recent refactoring.

[konnov]

Since this has been fixed on the Apalache side, shall we check that this has been fixed in Quint and close the issue?

[thpani]

Since this has been fixed on the Apalache side, shall we check that this has been fixed in Quint and close the issue?

Since this is transpilation-related, lemme take this over.

Yes, we're good on quint verify - I will open a PR to bring the river example back.