search

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
780 stars 31 forks source link

How to run tests in deep modules? #1184

Closed p-offtermatt closed 3 days ago

p-offtermatt commented 11 months ago

My spec is this: https://github.com/cosmos/interchain-security/blob/e09968d94a4e5a84bf144e5f0737e1f529494772/tests/difference/core/quint_model/ccv.qnt#L212

When I run quint test ccv.qnt --main CCVDefaultStateMachine I would expect the tests in the CCV module to be run. They are not; I guess because they themselves are not imported in CCVDefaultStateMachine, because CCV is not exported by CCVStatemachineLogic.

Adding export CCV.* to CCVStatemachineLogic (e.g. after import CCV.* does not work), when running quint test I get this:

Error: Internal error while flattening [QNT404] Name 'PROVIDER_CHAIN' not found,[QNT404] Name 'PROVIDER_CHAIN' not found
    at resolveNamesOrThrow (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:90:15)
    at flattenModules (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:61:35)
    at runTests (/Users/offtermatt/projects/quint/quint/dist/src/cliCommands.js:248:104)
    at EitherConstructor.asyncChain (/Users/offtermatt/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /Users/offtermatt/projects/quint/quint/dist/src/cli.js:33:39

If I add export CCV without .*, I get this error:

Error: Internal error while flattening [QNT404] Name 'UnbondingPeriodPositiveTest' not found,[QNT404] Name 'VscTimeoutPositiveTest' not found,[QNT404] Name 'CcvTimeoutPositiveTest' not found,[QNT404] Name 'CcvTimeoutLargerThanUnbondingPeriodTest' not found,[QNT404] Name 'ProviderIsNotAConsumerTest' not found,[QNT404] Name 'CcvTimeoutKeysTest' not found,[QNT404] Name 'UnbondingPeriodKeysTest' not found
    at resolveNamesOrThrow (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:90:15)
    at flattenModules (/Users/offtermatt/projects/quint/quint/dist/src/flattening/fullFlattener.js:73:24)
    at runTests (/Users/offtermatt/projects/quint/quint/dist/src/cliCommands.js:248:104)
    at EitherConstructor.asyncChain (/Users/offtermatt/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /Users/offtermatt/projects/quint/quint/dist/src/cli.js:33:39

Is there a way to do what I am trying to do, i.e. run the tests in CCV, but with the instantiation I have done through CCVStatemachineLogic from CCVDefaultStateMachine? I am not sure if any of the behaviour here is a bug. At least from a users perspective, the error messages seem weird, but I can't quite tell.

bugarela commented 11 months ago

I guess because they themselves are not imported in CCVDefaultStateMachine, because CCV is not exported by CCVStatemachineLogic.

Yes, that's right, you need the export exactly as you said.

The export should work, but it's breaking flattening for some reason. That's not even related to the tests - if I comment out all of the tests, it still crashes.

Seems like an export bug to me.

p-offtermatt commented 11 months ago

Thanks for looking into it. I worked around this for now by splitting my modules differently, so it's not blocking me.