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

--out-itf should not supress output #1571

Open
bugarela opened this issue Dec 23, 2024 · 0 comments
Open

--out-itf should not supress output #1571

bugarela opened this issue Dec 23, 2024 · 0 comments
Labels
good first issue A simple issue to start with simulator Quint simulator UX impacts or improves user experience

Comments

@bugarela
Copy link
Collaborator

We already have a --verbosity flag for that.

I personally almost always miss the output when running with --out-itf. My reasoning is: I would like to use the ITF trace for some machine task (i.e. rendering some graphic thing about the trace or using it in a MBT test), and for that, I'd like to know what happened in the trace to know if my machine task corresponds to my expectations. What I find myself doing is inspecting the ITF trace to see what happened in that particular execution, but I'd much rather inspect it in the Quint-formatted trace I'm used to reading.

If most people prefer --out-itf to produce no terminal output, we can make it so it changes the default verbosity to 0, and then we just have to set a higher verbosity to see the output.

@bugarela bugarela added simulator Quint simulator UX impacts or improves user experience good first issue A simple issue to start with labels Dec 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
good first issue A simple issue to start with simulator Quint simulator UX impacts or improves user experience
Projects
None yet
Development

No branches or pull requests

1 participant