informalsystems/modelator

Easy-to-understand trace representation

andrey-kuprianov opened this issue · 0 comments

As requested by @tesnimab, as a feature likely to be much needed by our users, alongside with the ITF trace representation (for automatic processing), we need to produce an easy-to-understand representation for humans.

For that we can use the (tweaked) version of the tabular differential representation that has been developed by @rnbguy. This could be implemented e.g. as follows:

When we call atomkraft model sample --examples "Ex1,Ex2" then a trace trace1 is produced for Ex1 by an Atomkraft command, it is stored in the following forms:

  • traces/<timestamp>/Ex1/trace1.itf.json (for automatic processing)
  • traces/<timestamp>/Ex1/trace1.txt (complete tabular representation, with all state components)
  • traces/<timestamp>/Ex1/trace1.diff.txt (shortened tabular representation, with only differences between consecutive states)

Other alternatives are of course possible, and should be discussed.

This feature is fine to implement in the feature freeze period, before the prototype release, because:

  • it is requested by our product owner as critical, and
  • it concerns only with output, so no unforeseen interactions with other components should happen.