List all the success and failure paths

[jayaprabhakar k]

Hi,

When a model checker is run with the tla+ toolbox, it lists the number of states explored, and if anything failed and shows one such failure.

I am curious if there's a way to list all the generated state transitions along with their statuses?

I understand, the design still has bugs if it fails for one case, but it would be nice to know which all cases it succeeded.

Is there a way to get this, either in the toolbox or in the command line?

Thanks,

JP