feat: Add support for multiple invariants in CLI commands

[jesicaMao]

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

This PR implements the feature requested in issue #1573 to support checking multiple invariants and reporting which specific ones were violated.
Changes include:
Added support for the --invariants CLI option to accept a list of invariants
Combined multiple invariants with logical AND for evaluation
Implemented detailed reporting of which specific invariants were violated
Updated documentation with examples showing how to use the feature
Added support for both simulator and verification modes

Fixes #1573

[jesicaMao]

@bugarela Could you kindly check #1662 . Please let me know if I need to change anything.

[bugarela]

Hi, some preliminary comments. I'm getting some compilation issues, also reported by the CI. Was this working for you?

[bugarela]

This change is not necessary, as guessMainModule already returns prev.args.main if provided.

Suggested change

	const guessedMainModule = guessMainModule(prev)
	const mainName = prev.args.main || guessedMainModule
	const mainName = guessMainModule(prev)

[bugarela]

Suggested change

	const guessedMainModule = guessMainModule(prev)
	const mainName = prev.args.main || guessedMainModule
	const mainName = guessMainModule(prev)

[jesicaMao]

@bugarela I have made the changes. Could you kindly check and let me know if everything is alright?

[bugarela]

Hi, sorry for the delay. Seems like there are still compilation issues. Are you able to successfully run npm run compile locally?

[jesicaMao]

Hi @bugarela. I did run npm run compile locally after making the changes. Let me check again and I will let you know as soon as I can. Thank You.

[jesicaMao]

@bugarela please check if everything is alright now.

[bugarela]

Hi @jesicaMao! Awesome, it seems to work now 🎉 thanks for seeing this through.
The failing tests are a simple thing: you are adding one more "artificial" definition, and the test checks the definition count, so we just need to update the expectation.

I can take this on from here and get it merged today/tomorrow if that's ok for you. Again, thank you!!

[bugarela]

Ok, I'm testing things locally and turns out this is never loading the final state of the trace to evaluate the invariant there. It is evaluating the invariant on a completely new state (new evaluator), so it doesn't really work for invariants that reference the state (which are all real invariants in practice):

$ quint run ../examples/language-features/counters.qnt --invariants "n >= 0" "n < 10"
An example execution:

[State 0] { n: 1 }

[State 1] { n: 2 }

[State 2] { n: 3 }

[State 3] { n: 6 }

[State 4] { n: 12 }

[violation] Found an issue (9ms).
Violated invariants:
Use --verbosity=3 to show executions.
Use --seed=0x116c719f7aa6a5 to reproduce.
error: Invariant violated

(this was supposed to print "n < 10")

I have a pretty good idea how to fix this, but it is not something very trivial. I'll find sometime between this and next week to try it. I think the changes you made to the UI are super helpful already and a great head start, but this evaluation part is tricky.

[jesicaMao]

@bugarela Thanks a lot for your valuable feedback. I am overwhelmed to know my changes were useful. Please let me if I need to change anything else.

[bugarela]

I fixed it and slightly changed the formatting:

It also works on quint verify :D