5 ms·
I got lost at Next diagram: next P : ●ー○ー○ P : ○ー●ー○ Is the P in the 2nd row meant to represent “P after evaluating next(P)”?
by dejj 5y ago
I got lost at Next diagram:
next P : ●ー○ー○
P : ○ー●ー○
Is the P in the 2nd row meant to represent “P after evaluating next(P)”?
- sriram_malhar 5y agoEach 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.
- dejj 5y agoDoes the “next P” of row 1 refer to: a) the 2nd dot in the 1st row? b) the entire 2nd row?
- mmerlin 5y ago(a)
- dejj 5y agoShouldn’t it then be: next P : ●ー●ー○ ?
- deleted 5y ago[deleted]
- sriram_malhar 5y agoNo. 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.
- dejj 5y agoI 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.
- mmerlin 5y agoYes it is the "next state" of P after applying the function