quint icon indicating copy to clipboard operation
quint copied to clipboard

Test failures for tests in instanced modules do not give the right command to rerun

Open p-offtermatt opened this issue 1 year ago • 0 comments

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.*
}

p-offtermatt avatar Sep 28 '23 06:09 p-offtermatt