Yes, that is true.
One can also use web technology and/or SVG graphics.
An online example is available here
(ABZ’14 case study)
(ABZ’16 case study; see also https://www3.hhu.de/stups/prob/index.php/ABZ16).
These visualisations use Event-B models, but could just as well have used TLA+ models.
Unfortunately, we have no real Toolbox integration (yet).
There may be a tutorial about using ProB for TLA+ at the next TLA+ workshop.
Description: Message signed with OpenPGP using GPGMail