[BUG] Benchmark results are producing strange results on encoding tests

[shonfeder]

Report from @rodrigo7491:

With the Error (see the detailed results report in the md file), it was with 012encoding+SetSndRcv . First run (before PR #1121) is here and and the second run is here.
With the odd runtime it was with 013encoding+SetSndRcv_NoFullDrop . First run is here and second one is here.

[rodrigo7491]

I should have made an issue directly, instead of messaging you @shonfeder , sorry about that. It seems that some links did not carry over, they are listed below:

• 012encoding+SetSndRcv (With some instances producing counter-examples)
  • Add reports from v0.17.6-SNAPSHOT apalache-tests#87
  • Add reports from v0.17.6-SNAPSHOT apalache-tests#91
• 013encoding+SetSndRcv_NoFullDrop (With an odd runtime)
  • Add reports from v0.17.6-SNAPSHOT apalache-tests#86
  • Add reports from v0.17.6-SNAPSHOT apalache-tests#92

[shonfeder]

No worries! I had asked you to message me the info. :)

Thank you for the additional context and info! 🙏

[shonfeder]

@rodrigo7491 Here's one counterexample for the SetSndRcv experiment: https://github.com/informalsystems/apalache-tests/pull/97/files#diff-ab54fb3cf295df97c5583bf0324e2077bc59642f826db557efdcdc1a1c943fb0

You'll find counter examples for the other failing runs in that PR. All the ones I've looked at have this same shape:

(* Transition 0 to State1 *)
State1 ==
  Values = { 0, 1, 2, 3, 4 }
    /\ medium = {0}
    /\ receiver = {}
    /\ sender = { 1, 2, 3, 4 }

(* Transition 1 to State2 *)
State2 ==
  Values = { 0, 1, 2, 3, 4 }
    /\ medium = {0}
    /\ receiver = {}
    /\ sender = {}

(* Transition 1 to State3 *)
State3 == Values = { 0, 1, 2, 3, 4 }/\ medium = {}/\ receiver = {}/\ sender = {}

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == sender = {} /\ medium = {} /\ receiver = {}

i.e., at some point, the sender just drops all of it's values from one state to the next.

Note that I am able to reproduce this outcome on my system. E.g., with

apalache-mc check --profiling=true --run-dir=./out --init=Init --next=Next --inv=Inv --smt-encoding=arrays --length=6 --cinit=CInit6 SetSndRcv.tla

Producing

---------------------------- MODULE counterexample ----------------------------

EXTENDS SetSndRcv

(* Constant initialization state *)
ConstInit == Values = { 0, 1, 2, 3, 4, 5, 6 }

(* Initial state *)
State0 ==
  Values = { 0, 1, 2, 3, 4, 5, 6 }
    /\ medium = {}
    /\ receiver = {}
    /\ sender = { 0, 1, 2, 3, 4, 5, 6 }

(* Transition 0 to State1 *)
State1 ==
  Values = { 0, 1, 2, 3, 4, 5, 6 }
    /\ medium = {3}
    /\ receiver = {}
    /\ sender = { 0, 1, 2, 4, 5, 6 }

(* Transition 1 to State2 *)
State2 ==
  Values = { 0, 1, 2, 3, 4, 5, 6 }
    /\ medium = {3}
    /\ receiver = {}
    /\ sender = {3}

(* Transition 0 to State3 *)
State3 ==
  Values = { 0, 1, 2, 3, 4, 5, 6 }
    /\ medium = {3}
    /\ receiver = {}
    /\ sender = {}

(* Transition 1 to State4 *)
State4 ==
  Values = { 0, 1, 2, 3, 4, 5, 6 }
    /\ medium = {}
    /\ receiver = {}
    /\ sender = {}

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == sender = {} /\ medium = {} /\ receiver = {}

================================================================================
(* Created by Apalache on Thu Dec 02 15:27:43 EST 2021 *)
(* https://github.com/informalsystems/apalache *)

[shonfeder]

I'm also reproducing the same kind of timing results on the NoFullDrop variant when running locally. E.g., running with

apalache-mc check --profiling=true --run-dir=./out --init=Init --next=Next --inv=Inv --smt-encoding=arrays --length=14 --cinit=CInit14 SetSndRcv_NoFullDrop.tla

using the arrays encoding, I get

Total time: 35.116 sec                                            I@15:35:16.583
EXITCODE: OK

Whereas using the oopsla19 encoding:

apalache-mc check --profiling=true --run-dir=./out --init=Init --next=Next --inv=Inv --smt-encoding=oopsla19 --length=14 --cinit=CInit14 SetSndRcv_NoFullDrop.tla
Total time: 4.7 sec                                               I@15:35:35.070
EXITCODE: OK

Let's sync up tomorrow to see if we can figure out what's going on!

[shonfeder]

Oh, that was running with the last release. If I switch the current release, I get times that are even closer in line with the CI results on SetSndRcv_NoFullDrop.tla:

For arrays:

It took me 0 days  0 hours  3 min  9 sec                          I@15:47:55.028
Total time: 189.392 sec                                           I@15:47:55.028

and for oopsla:

It took me 0 days  0 hours  0 min  4 sec                          I@15:57:45.744
Total time: 4.33 sec                                              I@15:57:45.744

[rodrigo7491]

Thanks for the changes @shonfeder. I am now able to reproduce the error with SetSndRcv.tla. It turns out I simply forgot to add --inv=Inv to the call, novice mistake. The good news is that I figured out the cause of the problem. I will work on the fix first and then will have a look at SetSndRcv_NoFullDrop.tla.

[shonfeder]

Wonderful! The benchmarks are doing their job, and we have improved our debugging abilities! 🗡️

I'll add a flag to the CI that will let us tell the CI job when we want it to commit the counter examples etc.

[shonfeder]

We agreed a flag's not necessary for now, we can just make a quick code change when debugging is needed.