↻
TEMPORAL
← All solvers
◐
Evaluate
¬
∧
∨
⊃
≡
X
G
F
U
R
(
)
¬ X G F bind tightest, then ∧, then ∨, then U and R, then ⊃ — so
p | r U q & s
is
(p∨r) U (q∧s)
Path
+ state
− state
Loop to
Ask
find a path…
is it valid?
Undo
Restart
The path
Click a letter to flip it, a state to look at it. The last state loops back, so the path is infinite and
G
and
F
have something to quantify over.