Specifying State Machines with Temporal Logic(wickstrom.tech)
wickstrom.tech
Specifying State Machines with Temporal Logic
https://wickstrom.tech/programming/2021/05/03/specifying-state-machines-with-temporal-logic.html
12 comments
Each circle represents a state. A filled circle represents the formula to be true in that state.
Here P is true in state 2, then false subsequently. So in state 1, the formula "next P" is true. "next P" is false in state 2, because P is false in state 3.
Here P is true in state 2, then false subsequently. So in state 1, the formula "next P" is true. "next P" is false in state 2, because P is false in state 3.
Does the “next P” of row 1 refer to:
a) the 2nd dot in the 1st row?
b) the entire 2nd row?
a) the 2nd dot in the 1st row?
b) the entire 2nd row?
(a)
Shouldn’t it then be:
next P : ●ー●ー○
?No. It should be:
In non-temporal logic, all operators operate on the values at a single time. So, when we say "P and Q", or "not P", these implicitly all apply to some state i.
Temporal logic adds "next", which links a state i to the state i+1. (next P) in state i refers to the value of P in state (i+1). (always P) refers to states (i ... inf).
In this example, the value of (next P) in state 2 must be false, because it refers to P's value in state 3.
1 2 3
P ● ● ○
(next P) ● ○ ○
In non-temporal logic, all operators operate on the values at a single time. So, when we say "P and Q", or "not P", these implicitly all apply to some state i.
Temporal logic adds "next", which links a state i to the state i+1. (next P) in state i refers to the value of P in state (i+1). (always P) refers to states (i ... inf).
In this example, the value of (next P) in state 2 must be false, because it refers to P's value in state 3.
I can comprehend your interpretation of ‘next’; it is algebraic: For all states ‘i’: ‘next P’ is true for state ‘i’, if P is true for state ‘i+1’.
The article seems to have a side-effect based interpretation rather than an algebraic one. It seems that ‘next P’ updates the state state of ‘P’. Hence the different diagram.
The article seems to have a side-effect based interpretation rather than an algebraic one. It seems that ‘next P’ updates the state state of ‘P’. Hence the different diagram.
[deleted]
Yes it is the "next state" of P after applying the function
I would assume some limiting factors here are:
- the speed of end to end tests - the flakiness of end to end tests - the coupling to the user interface - the fact that specifications for practical applications can be very complex, with know way of knowing the spec is accurate
That being said, I think this approaches the platonic ideal of how to test applications. We may get better at synthesizing programs from specifications - the hardware field does it with FPGAs.
I have been really into TLA+ since diving into it, it seems to provide such an elegant model of computation. From what I’ve read, TLA+ was created to address limitations of LTL for large, practical applications. So that will also be interesting to see how it plays out.
Kudos for trying though, I’m interested in seeing what comes out of this path.
- the speed of end to end tests - the flakiness of end to end tests - the coupling to the user interface - the fact that specifications for practical applications can be very complex, with know way of knowing the spec is accurate
That being said, I think this approaches the platonic ideal of how to test applications. We may get better at synthesizing programs from specifications - the hardware field does it with FPGAs.
I have been really into TLA+ since diving into it, it seems to provide such an elegant model of computation. From what I’ve read, TLA+ was created to address limitations of LTL for large, practical applications. So that will also be interesting to see how it plays out.
Kudos for trying though, I’m interested in seeing what comes out of this path.
When learning about it, I'd thought LTL would be useful for declaratively specifying GUI behaviour. Does anyone know of other work in this, more particular, case?
The author of the post, Oskar Wickstrom, is building such a tool (he mentions it in passing) : https://quickstrom.io/
Is the P in the 2nd row meant to represent “P after evaluating next(P)”?