search

informalsystems / quint

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

The ITF trace produced by quint verify is not formatted correctly #1448

Closed ivan-gavran closed 2 months ago

ivan-gavran commented 5 months ago

When running quint verify ..., the resulting ITF trace does not adhere to the ITF trace format: instead of being a JSON object ({...}), it is an array containing a single JSON object ([{...}]). An example is given in out.itf.json.

This does not happen when running Apalache directly on a TLA+ file.

romac commented 2 months ago

@bugarela Was this fixed in https://github.com/informalsystems/quint/pull/1365?

bugarela commented 2 months ago

@bugarela Was this fixed in #1365?

No, that only touched the simulator (quint run) output and I almost made the same mistake as here, but noticed and fixed.

This one should be a simple fix tho, I'll mark it as good-first-issue and perhaps @MahtabNorouzi can work on it next month