quint
quint copied to clipboard
Test failures for tests in instanced modules do not give the right command to rerun
Take this spec:
module Core {
const x: int
run CoreTest = 1 == 2
}
module Extra {
import Core(x = 5).*
}
When running quint test --main Extra spec.qnt
, the test failure reads this:
Extra
1) Extra::Core::CoreTest failed after 1 test(s)
1 failed
1) Extra::Core::CoreTest:
/Users/offtermatt/projects/interchain-security/tests/difference/core/quint_model/test.qnt:5:5 - error: Extra::Core::CoreTest returns false
5: run CoreTest = 1 == 2
Use --seed=0x7c211ef2544ad --match=Extra::Core::CoreTest to repeat.
Use --verbosity=3 to show executions.
Further debug with: quint --verbosity=3 test.qnt
/Users/offtermatt/projects/interchain-security/tests/difference/core/quint_model/test.qnt:5:5 - error: Extra::Core::CoreTest returns false
5: run CoreTest = 1 == 2
In particular, notice this:
Use --seed=0x7c211ef2544ad --match=Extra::Core::CoreTest to repeat.
Rerunning with this does not actually work:
% quint test --main Extra test.qnt --seed=0x7c211ef2544ad --match=Extra::Core::CoreTest
Extra
It seems to be a problem with the module prefacing here. It works if I run
quint test --main Extra test.qnt --seed=0x7c211ef2544ad --match=CoreTest
This problem does not appear when the spec does not have tests in instantiated modules, i.e. here everything is ok:
module Core {
const x: int
run CoreTest = 1 == 2
}
module Extra {
import Core.*
}