3 ms·

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 in

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 ago
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 ago
> 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.