- 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.
next P : ●ー○ー○
P : ○ー●ー○
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.
a) the 2nd dot in the 1st row?
b) the entire 2nd row?
next P : ●ー●ー○
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.
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.