This is cool

[lemmy]

Nice work! It seems to me that your channel modules would be nice additions to https://github.com/tlaplus/CommunityModules when one wants to model communication more explicitly.

Can you clarify to what extent the timeline visualization depends on your channel modules? Note that https://github.com/tlaplus/tlaplus/issues/267#issuecomment-481951259 has a similar direction but builds on top of ShiViz, which is a dedicated tool to visualize concurrency and happen-before relationships. With https://github.com/tlaplus/tlaplus/issues/393, the ShiViz integration shown in the screencast above will also be accessible from the command-line.

[dmilstein]

As it's implemented right now, the visualization depends very heavily on the channel modules, because they collect the history of logical steps in a hidden piece of state. And the final version of that history is parsed and turned into the visualization. It's likely that with some care, the key information could all be collected from the sequence of states, without the explicit recording of history.

ShiViz looks great -- I had seen it mentioned but not figured out what it actually was. Obviously a lot of overlap (aka it's way more powerful than what I've got ;-).

I'd be happy to contribute these to Community Modules -- can we set up a sub-directory or something, because it feels like it could be a bit unwieldy to cram them all into the top-level.

[lemmy]

The idea of the Toolbox's ShiViz integration is, that the history of logical steps is calculated with trace expressions (not as part of state exploration). This has the advantage that it doesn't "taint" the spec, is not bound to specific modules, and speeds up model checking. https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla has boilerplate to write such trace expressions with support for concurrent PlusCal algorithms (could easily be extended).

I expected to add more structure to CommunityModules when it becomes too big. However, right now TLC won't find modules in sub-directories.

[oberstet]

fwiw, I also want to appreciate your work! this is indeed cool;) It was an eye opener for me as a TLA newbie to see a very clear and flexible definition of non-deterministic event queues and loops, I mean it really boils down to

NextMessages(channels, receiver) - the set of (wrapped) message a given client could see next. 

await HasMessage(Channels, self);
with wrapped_msg \in NextMessages(Channels, self) do
  with msg = Payload(wrapped_msg) do
    \* process msg
  end with;
  Channels := MarkMessageReceived(Channels, self, wrapped_msg, receiverState)

In addition, of course the visualization stuff is also pretty nice! As a means of communication, polished and built-in. Awesome. I wasn't aware of ShiViz either - yet another nugget it seems. reusing ShiViz for visualization logged from the channel code here: absolutely. that sounds too good;)