Raw LTL Specification Parser - VerifiableRobotics/LTLMoP GitHub Wiki

The Raw LTL Specification Parser lets one write a specification in plain LTL. This can be useful either for practicing LTL, or for testing out specifications that might be hard to write under the constraints of a higher-level grammar.

• Either bare proposition names may be used, or they may be optionally prepended by e. and s. to distinguish environment and system propositions, respectively.
• Temporal operators are represented as follows: [] (always), <> (eventually), next(something)
• The specification is split into \phi_e and \phi_s based on a single line of dashes in between the two parts (e.g. ---) (TODO: assume no env assumptions if "---" separator line is absent.)
• Macros such as STAY_THERE will be substituted with the correct LTL. See [Specification Macros](Specification Macros).
• The specification must be written in the GR(1) fragment of LTL. (TODO: enforce this in a friendly way)