Skip to content

Raw LTL Specification Parser

Jump to bottom
Cameron Finucane edited this page Jul 2, 2013 · 2 revisions

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)
Clone this wiki locally