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

[Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>]

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

  http://wyvern.cs.uni-duesseldorf.de/bms/landing.html

 (ABZ’14 case study)

or here

 http://wyvern.cs.uni-duesseldorf.de/bms/hdmachine.html

(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,

Michael

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