sktrdie on TLA+: design, model, document, and verify concurrent systems

Comment on TLA+: design, model, document, and verify concurrent systems parent

Interesting I see. I thought BP was built on top of Live Sequence Charts - a visual formalism for describing specs that can also be executed.

Thanks for the info. I'll have to dive a bit more into TLA+. Even though I still don't see how the request/wait/block is implemented in TLA+... I mean you still need an even selection mechanism for it or not?

hwayne 7y

In the TicTacToe spec, we have

    Next2 ==
      /\ turn' = turn + 1            \* A
      /\ current' = Opponent         \* B
      /\ ∃i,j∈1..N:                  \* C
           /\board[i,j] = Empty      \* C.1
           /\ board'[i,j] = current  \* C.2

For `Next2` to be true, the square [i, j] has to be empty AND in the following state, that same square must have whichever mark was `current` in it. Since `current` switches between the two each step of the behavior, this forces each player to wait until their turn comes around.

pron 7y

I thought BP was built on top of Live Sequence Charts

Yes, but LSC are also based on temporal logic, as were Harel's Statecharts (perhaps the first synchronous programming language).

I mean you still need an even selection mechanism for it or not?

Not sure what you mean by "even." TLA+ is nondeterministic, and the formulas can serve as rules to restrict that nondeterminism (where simple logical conjunction is used to compose the rules). Also, nothing is really "implemented" in TLA+, as it's not a programming language. It's a formal specification language that describes the behavior of discrete systems.

Comments