Variables of the flag --mbt included into the ITF trace

[ivan-gavran]

Adds variables mbt::actionTaken and mbt::nondetPicks to ITF's "vars" field.
Also, renames existing action_taken into mbt::actionTaken and nondet_picks into mbt::nondetPicks.
Fixes issue #1558

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[ivan-gavran]

Hi @bugarela : some automated checks are failing here, and this seems to be associated with unexpected Lf token. I am not even sure if it has to do with my changes in this PR. On the other hand, I see that those tests pass in other PRs (e.g., #1561 ), so I am confused.
Any idea about what I could do to fix the problem?

[bugarela]

Hi @ivan-gavran. They are lot related to whitespaces, that's just additional information on the test reporting. The problem is the order of the fields in the JSON or in the Quint-printed trace - the comparison is not smart, it is just comparing the expected vs actual output as text. By renaming the fields, as you did, they get outputted in a different order, so you need to update the test expectations in io-cli-tests.md to have this new order of fields.

For example, on this failing test:

not ok 22 run finds violation with metadata: output mismatch
  ---
  expected stdout: |
    An example execution:

    [State 0] { mbt::actionTaken: "init",␠n:␠1, mbt::nondetPicks: {  } }

    [State 1] { mbt::actionTaken: "OnPositive",␠n:␠2, mbt::nondetPicks: {  } }

    [State 2] { mbt::actionTaken: "OnPositive",␠n:␠3, mbt::nondetPicks: {  } }

    [State 3] { mbt::actionTaken: "OnDivByThree",␠n:␠6, mbt::nondetPicks: {  } }

    [State 4] { mbt::actionTaken: "OnDivByThree",␠n:␠12, mbt::nondetPicks: {  } }

    [violation] Found an issue (duration).
    Use --verbosity=3 to show executions.
    Use --seed=0x308623f2a48e7 to reproduce.
    error: Invariant violated

  actual stdout: |
    An example execution:

    [State 0] { mbt::actionTaken: "init", mbt::nondetPicks: {  },␠n:␠1 }

    [State 1] { mbt::actionTaken: "OnPositive", mbt::nondetPicks: {  },␠n:␠2 }

    [State 2] { mbt::actionTaken: "OnPositive", mbt::nondetPicks: {  },␠n:␠3 }

    [State 3] { mbt::actionTaken: "OnDivByThree", mbt::nondetPicks: {  },␠n:␠6 }

    [State 4] { mbt::actionTaken: "OnDivByThree", mbt::nondetPicks: {  },␠n:␠12 }

    [violation] Found an issue (duration).
    Use --verbosity=3 to show executions.
    Use --seed=0x308623f2a48e7 to reproduce.
    error: Invariant violated

The order of variables is: mbt::actionTaken, mbt::nondetPicks, n. But the test expectation has: mbt::actionTaken, n, mbt::nondetPicks

[ivan-gavran]

Thanks @bugarela, fixed that. However, there again seems to be a problem with apalache-tests.md::!test out can convert ApalacheCompliation.qnt to TLA+, and the diff between the expected and actual output is

12c12
<       @type: (() => A(UNIT) | B(Int));
---
>       @type: (() => A({␠tag:␠Str␠}) | B(Int));
14c14
<     A == Variant("A", "U_OF_UNIT")
---
>     A == Variant("A", [tag␠|->␠"UNIT"])
17c17
<       @type: ((Int) => A(UNIT) | B(Int));
---
>       @type: ((Int) => A({␠tag:␠Str␠}) | B(Int));

Now I really cannot see how my changes might have an effect on the generated TLA+. Any idea what could be the reason for this failing test?

[bugarela]

Hi @ivan-gavran, thanks. This time, it's not your fault, just unfortunate timing - sorry about that. I have a fix coming in #1565

This is an issue of our CI - it uses the latest version of Apalache instead of the one Quint sets, and there was a small breaking change regarding the UNIT type in the release that was cut a few days ago. Once I merge this one, we can update your PR with main and it should be fine.

[bugarela]

There you go

[bugarela]

LGTM! Thanks for taking care of this

[ivan-gavran]

Thanks for your help! Very proud to contribute to quint (even if it is a super small PR :) )