Record machine variables #943

Motivation

This is a feature request to show the state of machine variables in the .trace.json files. This could be displayed in the "Peasy Visualizer". The TLA Toolbox, for a comparative example, displays the error trace with the state at each step. I believe it can be configured to only show variables that change between states to keep the noise down, but that's more of a detail of the visualizer.

The use-case for this is to reduce the need for dumping a bunch of state variables into formatted strings to speed up prototyping. I see a common pattern in P code like:

assert currentBalance == resp.balance,
       format ("Withdraw failed BUT the account balance changed! client thinks: {0}, bank balance: {1}",
               currentBalance, resp.balance);

If the state variables are immediately viewable in all cases, most asserts can be simplified:

assert currentBalance == resp.balance, "Withdraw failed BUT the account balance changed!";

Proposal

For example, from the Client/Server tutorial, one of the events provides the following trace:

{
    "type": "MonitorProcessEvent",
    "details": {
      "log": "BankBalanceIsAlwaysCorrect is processing event \u0027eWithDrawResp with payload (\u003Cstatus:1, accountId:0, balance:
14, rId:1, \u003E)\u0027 in state \u0027WaitForWithDrawReqAndResp\u0027.",
      "event": "eWithDrawResp",
      "state": "WaitForWithDrawReqAndResp",
      "payload": {
        "status": 1,
        "accountId": 0,
        "balance": 14,
        "rId": 1
      },
      "sender": "BankServer(2)",
      "monitor": "BankBalanceIsAlwaysCorrect",
      "clock": {
        "BankBalanceIsAlwaysCorrect": 7,
        "TestWithSingleClient(1)": 3,
        "Client(3)": 6,
        "BankServer(2)": 3
      }
    }
  }

I'd suggest adding a "machines" key with something like the following. There are a few things to iron out, like:

1. How to represent maps, since JSON expects string-keys, not any type. Probably a list of entries.
2. Managing cycles. I've shown a proposal below which is just string "references". It may be best to decorate values with their types in this case. Like { "value": "Database(2)", "type": "reference" }.

{
  ...
  "machines": {
    "BankServer(2)": {
      "database": "Database(2)",
    },
    "Database(2)": {
       "server": "BankServer(2)",
       "balance": {
         "1": 10
       }
     }
  }
}