1. spot::ltl::parse() and spot::ltl::format_parse_errors()

Spot provides one function, spot::ltl::parse() that parses a string (representing an LtlFormula) and returns a spot::ltl::formula object (representing the same formula, of course). The string must follows the LtlSyntax. parse() will also return a list of errors in a separate parse_error_list object (a list of location/diagnostic pairs). Errors are not output (because parse() does not know where and how you may want error to be output).

Another function, format_parse_errors(), provides a convenient way to output errors on a stream.

These functions are declared in spot/ltlparse/public.hh as follows:

namespace spot
{
  namespace ltl
  {
    typedef std::pair<yy::Location, std::string> parse_error;
    typedef std::list<parse_error> parse_error_list;

    formula* parse(const std::string& ltl_string,
                   parse_error_list& error_list,
                   environment& env = default_environment::instance(),
                   bool debug = false);

    bool format_parse_errors(std::ostream& os,
                             const std::string& ltl_string,
                             parse_error_list& error_list);
  }
}

There are three ways parse can exit.

  1. If it returns a non-NULL formula* object and an empty error_list, this means the parse was completely successful.

  2. If it returns a non-NULL formula* object and a non-empty error_list, an error was detected during parsing, and parse() found a way to continue parsing anyway. The resulting formula is unlikely to match the supplied ltl_string, but it could be what the user intended (e.g. a missing closing parenthesis at the end).

  3. If it returns a NULL formula* the parse failed completely and error_list is non-empty.

The second case make it possible to continue processing a formula even on error. format_parse_errors() will return true iff it output any diagnostic (i.e., if error_list is non-empty).

We recommend using this two functions as follows:

spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(str, pel);

int exit_code = spot::ltl::format_parse_errors(std::cerr, str, pel);

if (f)
  {
     // do something with f
  }
else
  {
    exit_code = 1;
  }

exit(exit_code);

2. spot::ltl::formula

The following diagram shows the hierarchy of classes using the LTL abstract syntax trees.

All formulae are reference counted, except the two constants spot::ltl::constant::true_instance() and spot::ltl::constant::false_instance() defined using the PPR:SingletonPattern.

None of these objects can be constructed directly. You have to use the instance() method; it will go through a unique table to ensure that two identical abstract syntax trees will have the same address by construction. This way syntactic equality can be tested in constant time. (This also means the abstract syntax tree is in fact an acyclic graph.)

Operators and and or are represented as spot::ltl::multop, i.e., operators with multiple operands. This allows some easy simplifications during the construction of an abstract syntax tree. For instance a * b * a will be constructed as a multop with only two children (a and b), because there is not point in listing a twice.

It should be noted that although the equality of two formula* means the two LtlFormulae are equivalent, the converse is not true. The following figures show formulae a * (a + b) * (b + c) and (a * b) + (a * c): although they are logically equivalent, they have different abstract syntax trees.

(!) You can build such abstract syntax trees interactively using ltl2tgba with the option draw the formula.

3. The purpose of the environment

The purpose of the environment argument of parse() is twofold.

  1. we sometimes want the LTL parser to reject unknown atomic propositions. From the parser point of view, the environment can be seen as the seen as the set AP of known atomic propositions.
  2. two atomic properties with the same name can coexist in Spot if they do not share the same environment. This can come useful when composing modules with set of atomic propositions that should be considered disjoint although they use similar names.

The following sequence diagram shows how the environment is queried for each (potential) atomic proposition the parser reads.

parseseq

The default_environment is an environment that will accept any atomic proposition. Spots also comes with a declarative_environment where atomic propositions need to be registered first before they can be required.

HowToParseLtlFormulae (last edited 2007-03-30 09:09:15 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.