informalsystems/modelator

Command `simulate`

ivan-gavran opened this issue · 0 comments

ivan-gavran commented

Incorporate the Apalache's simulate command to modelator (and, by extension, atomkraft).
Parameters:

  • max-trace: the number of traces to generate
  • trace-length: length of the trace to simulate

We will not enable is running the simulate mode for finding traces corresponding to particular tests (which is an option that exists in Apalache).