[HN Gopher] TLA+ Graph Explorer
       ___________________________________________________________________
        
       TLA+ Graph Explorer
        
       Author : hwayne
       Score  : 48 points
       Date   : 2021-04-07 18:54 UTC (4 hours ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | ahelwer wrote:
       | This is great, and replicates a feature I really like about
       | PRISM: the ability to step through your model's transitions to
       | see that they do what you think they do (and are enabled when you
       | think they are). I notice in the screenshots the next states are
       | labeled Child 1-N, wonder whether there will be an update to map
       | those children to the names of the actions taken in the spec
       | (although that feature would probably require interpreting the
       | spec itself instead of just the dotfile).
       | 
       | We also finally have a TLA+ state visualizer! One of the really
       | neat ideas included with Runway (RIP, F in the chat, etc.). You
       | write the visualizations in D3 I guess?
        
       | rgovostes wrote:
       | https://en.wikipedia.org/wiki/TLA%2B
        
         | ASalazarMX wrote:
         | Your comment is very helpful, but it would have been perfect if
         | it included the first paragraph.
         | 
         | > TLA+ is a formal specification language developed by Leslie
         | Lamport. It is used to design, model, document, and verify
         | programs, especially concurrent systems and distributed
         | systems. TLA+ has been described as exhaustively-testable
         | pseudocode, and its use likened to drawing blueprints for
         | software systems; TLA is an acronym for Temporal Logic of
         | Actions.
        
         | DannyB2 wrote:
         | Thank You for that!
         | 
         | I was puzzling over, trying to find a meaning for TLA.
         | 
         | In the 1980s I learned that TLA meant "Three Letter Acronyms".
         | That made it easier to complain about the use of TLAs that were
         | not explained. A TLA becomes a form of jargon that those not
         | "on the inside" don't get.
        
       ___________________________________________________________________
       (page generated 2021-04-07 23:01 UTC)