6 ms·

Sequence diagrames (that seems not much different swimlane diagrams) are great, so much so that I created a tool that generates them from appropriately built TL

by _flux 2y ago

Sequence diagrames (that seems not much different swimlane diagrams) are great, so much so that I created a tool that generates them from appropriately built TLA+ specs representing message exchange scenarios: https://github.com/eras/tlsd https://github.com/eras/tlsd However, while they are good for representing scenarios, they are not that good for specifying functionality. You can easily represent the one golden path in the system, but if you need to start representing errors or diverging paths, you probably end up needing multiple diagrams, and if you need multiple diagrams, then how do you know if you have enough diagrams to fully specify the functionality? > The protocol is complicated enough for me to think that the diagrams are the source of truth of the protocol. In other words, I'd venture to say that if an implementation of the Double Rachet algorithm ever does something that doesn't match the diagrams, it is more likely it is the code that is wrong than vice-versa. I would believe the latter statement, but I wouldn't say the first statement is that said in other words, so I don't believe this is the correct conclusion. My conclusion would be that diagrams are great way to visualize the truth of the protocol, but they are not a good way to be the source of truth: they should be generated from a more versatile (and formal) source truth.

billfruit 2y ago
Statechart diagrams are even better than sequence diagrams, because they can encode quite a lot of behaviour visually.
- manbash 2y ago
  State diagram and sequence diagram complement each other, rather than competing.
- _flux 2y ago
  State diagrams are basically visual code, aren't they? And indeed they good for specifying, being the source of truth, but like code, they (afaik) don't really work for representing interactions with multiple actors (other than by sending/receiving messages), and they don't have a time component. But you could generate sequence diagrams from them, or at least verify them. Xstate does have some functionality for interacting with the specified state machine, but I haven't played with it a lot. The idea of generating—or at least verifying—Xstate state machines with TLA+ has come across my mind, though.
  - billfruit 2y ago
    Statecharts are highly useful to represent behaviour. Sequence diagrams do not capture it as much. Timed behaviour, like timeouts can be represented in statecharts by having transitions on time based conditions. For example an event puts the system in a 'waiting' state, and in the waiting state there is a 30 second transition to a 'fail' state unless some other event happens which pulls the system out of the 'waiting' state. Also it provides a good indication of what behaviour is valid and what not valid and what are don't cares. External interactions of a system can be model as the state changes of a system. They also have 'memory', special elements that remember which substate the system was in before it jumped out of the state last time. I recommend David Harel's very interesting paper on modelling behaviour with state charts.

by _flux 2y ago

billfruit 2y ago

Statechart diagrams are even better than sequence diagrams, because they can encode quite a lot of behaviour visually.

manbash 2y ago
State diagram and sequence diagram complement each other, rather than competing.
_flux 2y ago
State diagrams are basically visual code, aren't they? And indeed they good for specifying, being the source of truth, but like code, they (afaik) don't really work for representing interactions with multiple actors (other than by sending/receiving messages), and they don't have a time component. But you could generate sequence diagrams from them, or at least verify them. Xstate does have some functionality for interacting with the specified state machine, but I haven't played with it a lot. The idea of generating—or at least verifying—Xstate state machines with TLA+ has come across my mind, though.
- billfruit 2y ago
  Statecharts are highly useful to represent behaviour. Sequence diagrams do not capture it as much. Timed behaviour, like timeouts can be represented in statecharts by having transitions on time based conditions. For example an event puts the system in a 'waiting' state, and in the waiting state there is a 30 second transition to a 'fail' state unless some other event happens which pulls the system out of the 'waiting' state. Also it provides a good indication of what behaviour is valid and what not valid and what are don't cares. External interactions of a system can be model as the state changes of a system. They also have 'memory', special elements that remember which substate the system was in before it jumped out of the state last time. I recommend David Harel's very interesting paper on modelling behaviour with state charts.