[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Analysis: Runway, a new formal specification system

Hi Ron,
On 5 Jul 2016, at 10:12, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

I believe TLA+ can also be visualized via automatic translation to ProB, which I think has a visualizer, but I haven't tried that.

Yes, that is true.
One can also use web technology and/or SVG graphics.
An online example is available here
 (ABZ’14 case study)
or here
(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.

Best regards,

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail