Evaluate formula over path.
Represent formula as string.
Rewrite formula to use only atomic connectives/modal operators.