Evaluate formula over path.

Represent formula as string.

Rewrite formula to use only atomic connectives/modal operators.