Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Error when running quint test --verbosity=x where x in {3,4,5} #1387

Open
p-offtermatt opened this issue Mar 1, 2024 · 0 comments
Open

Error when running quint test --verbosity=x where x in {3,4,5} #1387

p-offtermatt opened this issue Mar 1, 2024 · 0 comments
Labels
bug Something isn't working

Comments

@p-offtermatt
Copy link
Member

p-offtermatt commented Mar 1, 2024

My spec is here:
https://github.com/cosmos/interchain-security/blob/c69977414782ed604f53cf555e342bb177163123/tests/mbt/model/ccv_model.qnt#L523

When I run

quint test ccv_model.qnt --verbosity=3

I get this error:

TypeError: Cannot read properties of undefined (reading 'subframes')
    at TraceRecorderImpl.onNextState (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/trace.js:147:32)
    at CompilerVisitor.chainAllOrThen (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1116:35)
    at lazyCompute (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1129:40)
    at Object.eval (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1541:20)
    at CompilerVisitor.chainAllOrThen (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1091:29)
    at lazyCompute (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1129:40)
    at Object.eval (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1541:20)
    at CompilerVisitor.chainAllOrThen (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1091:29)
    at lazyCompute (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1129:40)
    at Object.eval (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1541:20)

The same happens for verbosity 4 and 5. Everything works fine for lower verbosities.

It doesn't seem to be a general problem with verbosity in tests - I tried --verbosity=3 with this very simple module, and there everything works fine, so I assume it's something specific to my spec.

module a {
    var a: int

    action init: bool = a' = 1

    action foo: bool = a' = 2

    run FooTest = init.then(foo).then(all{a == 1, foo})
}
$ quint test test.qnt --verbosity=3

  a
    1) FooTest failed after 1 test(s)

  1 failed

  1) FooTest:
      /Users/offtermatt/projects/interchain-security/tests/mbt/model/test.qnt:8:5 - error: [QNT511] Test FooTest returned false
      8:     run FooTest = init.then(foo).then(all{a == 1, foo})

[Frame 0]
init => true

[Frame 1]
foo => true

[Frame 2]
_ => none

    Use --seed=0x327e8c85f463b --match=FooTest to repeat.

/Users/offtermatt/projects/interchain-security/tests/mbt/model/test.qnt:8:5 - error: [QNT511] Test FooTest returned false
8:     run FooTest = init.then(foo).then(all{a == 1, foo})
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Tests failed
@p-offtermatt p-offtermatt added the bug Something isn't working label Mar 1, 2024
@p-offtermatt p-offtermatt changed the title Error when running quint test --verbosity=3 Error when running quint test --verbosity=x where x in {3,4,5} Mar 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant