Specifying State Machines with Temporal Logic 71 points by todsacerdoti 15 days ago | hide | past | favorite | 11 comments

 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 accurateThat 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/
 I got lost at Next diagram:`````` next P : ●ー○ー○ P : ○ー●ー○ `````` Is the P in the 2nd row meant to represent “P after evaluating next(P)”?
 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.
 Does the “next P” of row 1 refer to: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:`````` 1 2 3 P ● ● ○ (next P) ● ○ ○ `````` All formulae share the same timeline in terms of state numbering.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.
 Yes it is the "next state" of P after applying the function

Search: