After #2, the library logic and parser allow to build the syntax tree of a formula from a textual description.
The grammar tries to comply with A Standard Grammar for Temporal Logics on Finite Traces, but the PR does not include operators like "weak until" W and "strong release" M.

The goal of this issue is to double-check that the full syntax is supported by our parser.

This issue is to keep track of a discrepancy between NNF with empty-trace and non-empty trace semantics.

For example, let us denote ~ the logical not and ! the propositional not. Also, let a be an atom.

The NNF of a is a in both semantics.
The NNF of !a is !a in both semantics.
The NNF of ~a should be !a | end for empty-trace sem., and !a for non-empty trace sem.
The NNF of ~!a should be a | end for empty-trace sem., and a for non-empty trace sem.

This parser reads a partfile and stores the environment-agent variable partition.

Ideally, it should be implemented as a Visitor.

Is your feature request related to a problem? Please describe.
A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]

Describe the solution you'd like
A clear and concise description of what you want to happen.

Describe alternatives you've considered
A clear and concise description of any alternative solutions or features you've considered.

Additional context
Add any other context or screenshots about the feature request here.