quint

quint copied to clipboard

quint test run produces itf traces without the last state

module myTest {
  var x: int
  action init = x' = 0
  run myTest = init.then(x' = 1).then(x' = 2).then(x' = 3)
}

and then

$ quint test --output {}.itf.json myTest.qnt
$ jq -c .states < myTest.itf.json
[{"#meta":{"index":0},"x":{"#bigint":"0"}},{"#meta":{"index":1},"x":{"#bigint":"1"}},{"#meta":{"index":2},"x":{"#bigint":"2"}}]

Reported by @rnbguy

It is reproducible on HEAD.

@konnov noted this is probably a regression from #1133

is this resolved? I see that my example still produces wrong output on latest main.

Whoops! I closed the wrong issue. Thanks for checking :)