Classes
struct	spot::parsed_formula
	The result of a formula parser. More...

class	spot::random_formula
	Base class for random formula generators. More...

class	spot::random_ltl
	Generate random LTL formulae. More...

class	spot::random_boolean
	Generate random Boolean formulae. More...

class	spot::random_sere
	Generate random SERE. More...

class	spot::random_psl
	Generate random PSL formulae. More...

Typedefs
typedef std::pair< location, std::string >	spot::one_parse_error
	A parse diagnostic with its location. More...

typedef std::list< one_parse_error >	spot::parse_error_list
	A list of parser diagnostics, as filled by parse. More...

Functions
std::ostream &	spot::print_dot_psl (std::ostream &os, formula f)
	Write a formula tree using dot's syntax. More...

parsed_formula	spot::parse_infix_psl (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
	Build a formula from an LTL string. More...

parsed_formula	spot::parse_infix_boolean (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
	Build a Boolean formula from a string. More...

parsed_formula	spot::parse_prefix_ltl (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false)
	Build a formula from an LTL string in LBT's format. More...

formula	spot::parse_formula (const std::string &ltl_string, environment &env=default_environment::instance())
	A simple wrapper to parse_infix_psl() and parse_prefix_ltl(). More...

parsed_formula	spot::parse_infix_sere (const std::string &sere_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
	Build a formula from a string representing a SERE. More...

void	spot::fix_utf8_locations (const std::string &input_string, parse_error_list &error_list)
	Fix location of diagnostics assuming the input is utf8. More...

std::ostream &	spot::print_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as a string which is parsable. More...

std::string	spot::str_psl (formula f, bool full_parent=false)
	Convert a PSL formula into a string which is parsable. More...

std::ostream &	spot::print_utf8_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as an utf-8 string which is parsable. More...

std::string	spot::str_utf8_psl (formula f, bool full_parent=false)
	Convert a PSL formula into a utf-8 string which is parsable. More...

std::ostream &	spot::print_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a string which is parsable. More...

std::string	spot::str_sere (formula f, bool full_parent=false)
	Convert a SERE formula into a string which is parsable. More...

std::ostream &	spot::print_utf8_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a utf-8 string which is parsable. More...

std::string	spot::str_utf8_sere (formula f, bool full_parent=false)
	Convert a SERE formula into a string which is parsable. More...

std::ostream &	spot::print_spin_ltl (std::ostream &os, formula f, bool full_parent=false)
	Output an LTL formula as a string parsable by Spin. More...

std::string	spot::str_spin_ltl (formula f, bool full_parent=false)
	Convert an LTL formula into a string parsable by Spin. More...

std::ostream &	spot::print_wring_ltl (std::ostream &os, formula f)
	Output an LTL formula as a string parsable by Wring. More...

std::string	spot::str_wring_ltl (formula f)
	Convert a formula into a string parsable by Wring. More...

std::ostream &	spot::print_latex_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as a LaTeX string. More...

std::string	spot::str_latex_psl (formula f, bool full_parent=false)
	Output a formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulae). More...

std::ostream &	spot::print_latex_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a LaTeX string. More...

std::string	spot::str_latex_sere (formula f, bool full_parent=false)
	Output a SERE formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulae). More...

std::ostream &	spot::print_sclatex_psl (std::ostream &os, formula f, bool full_parent=false)
	Output a PSL formula as a self-contained LaTeX string. More...

std::string	spot::str_sclatex_psl (formula f, bool full_parent=false)
	Output a PSL formula as a self-contained LaTeX string. More...

std::ostream &	spot::print_sclatex_sere (std::ostream &os, formula f, bool full_parent=false)
	Output a SERE formula as a self-contained LaTeX string. More...

std::string	spot::str_sclatex_sere (formula f, bool full_parent=false)
	Output a SERE formula as a self-contained LaTeX string. More...

std::ostream &	spot::print_lbt_ltl (std::ostream &os, formula f)
	Output an LTL formula as a string in LBT's format. More...

std::string	spot::str_lbt_ltl (formula f)
	Output an LTL formula as a string in LBT's format. More...

Detailed Description

Typedef Documentation

◆ one_parse_error

typedef std::pair<location, std::string> spot::one_parse_error

#include <spot/tl/parse.hh>

A parse diagnostic with its location.

◆ parse_error_list

typedef std::list<one_parse_error> spot::parse_error_list

#include <spot/tl/parse.hh>

A list of parser diagnostics, as filled by parse.

Function Documentation

◆ fix_utf8_locations()

void spot::fix_utf8_locations	(	const std::string &	input_string,
		parse_error_list &	error_list
	)

#include <spot/tl/parse.hh>

Fix location of diagnostics assuming the input is utf8.

The different parser functions return a parse_error_list that contain locations specified at the byte level. Although these parser recognize some utf8 characters they only work byte by byte and will report positions by counting byte.

This function fixes the positions returned by the parser to look correct when the string is interpreted as a utf8-encoded string.

It is invalid to call this function on a string that is not valid utf8.

You should NOT call this function before calling spot::parsed_formula::format_errors() because it is already called inside if needed. You may need this function only if you want to write your own error reporting code.

Parameters

input_string	The string that were parsed.
error_list	The error list filled by spot::parse or spot::parse_sere while parsing input_string.

◆ parse_formula()

formula spot::parse_formula	(	const std::string &	ltl_string,
		environment &	env = `default_environment::instance()`
	)

#include <spot/tl/parse.hh>

A simple wrapper to parse_infix_psl() and parse_prefix_ltl().

This is mostly meant for interactive use. It first tries parse_infix_psl(); if this fails it tries parse_prefix_ltl(); and if both fails it returns the errors of the first call to parse_infix_psl() as a parse_error exception.

◆ parse_infix_boolean()

parsed_formula spot::parse_infix_boolean	(	const std::string &	ltl_string,
		environment &	env = `default_environment::instance()`,
		bool	debug = `false`,
		bool	lenient = `false`
	)

#include <spot/tl/parse.hh>

Build a Boolean formula from a string.

Parameters

ltl_string	The string to parse.
env	The environment into which parsing should take place.
debug	When true, causes the parser to trace its execution.
lenient	When true, parenthesized blocks that cannot be parsed as subformulas will be considered as atomic propositions.

Returns: A parsed_formula

Note that the parser usually tries to recover from errors. The field parsed_formula::f in the returned object can be a non-zero value even if it encountered error during the parsing of ltl_string. If you want to make sure ltl_string was parsed succesfully, check parsed_formula::errors for emptiness.

Warning: This function is not reentrant.

◆ parse_infix_psl()

parsed_formula spot::parse_infix_psl	(	const std::string &	ltl_string,
		environment &	env = `default_environment::instance()`,
		bool	debug = `false`,
		bool	lenient = `false`
	)

#include <spot/tl/parse.hh>

Build a formula from an LTL string.

Parameters

ltl_string	The string to parse.
env	The environment into which parsing should take place.
debug	When true, causes the parser to trace its execution.
lenient	When true, parenthesized blocks that cannot be parsed as subformulas will be considered as atomic propositions.

Returns: A formula built from ltl_string, or formula(nullptr) if the input was unparsable.

Note that the parser usually tries to recover from errors. The field parsed_formula::f in the returned object can be a non-zero value even if it encountered error during the parsing of ltl_string. If you want to make sure ltl_string was parsed succesfully, check parsed_formula::errors for emptiness.

Warning: This function is not reentrant.

◆ parse_infix_sere()

parsed_formula spot::parse_infix_sere	(	const std::string &	sere_string,
		environment &	env = `default_environment::instance()`,
		bool	debug = `false`,
		bool	lenient = `false`
	)

#include <spot/tl/parse.hh>

Build a formula from a string representing a SERE.

Parameters

sere_string	The string to parse.
env	The environment into which parsing should take place.
debug	When true, causes the parser to trace its execution.
lenient	When true, parenthesized blocks that cannot be parsed as subformulas will be considered as atomic propositions.

Returns: A formula built from sere_string, or formula(0) if the input was unparsable.

Note that the parser usually tries to recover from errors. The field parsed_formula::f in the returned object can be a non-zero value even if it encountered error during the parsing of ltl_string. If you want to make sure ltl_string was parsed succesfully, check parsed_formula::errors for emptiness.

Warning: This function is not reentrant.

◆ parse_prefix_ltl()

parsed_formula spot::parse_prefix_ltl	(	const std::string &	ltl_string,
		environment &	env = `default_environment::instance()`,
		bool	debug = `false`
	)

#include <spot/tl/parse.hh>

Build a formula from an LTL string in LBT's format.

Parameters

ltl_string	The string to parse.
env	The environment into which parsing should take place.
debug	When true, causes the parser to trace its execution.

Returns: A formula built from ltl_string, or formula(nullptr) if the input was unparsable.

Note that the parser usually tries to recover from errors. The field parsed_formula::f in the returned object can be a non-zero value even if it encountered error during the parsing of ltl_string. If you want to make sure ltl_string was parsed succesfully, check parsed_formula::errors for emptiness.

The LBT syntax, also used by the lbtt and scheck tools, is extended to support W, and M operators (as done in lbtt), and double-quoted atomic propositions that do not start with 'p'.

Warning: This function is not reentrant.

◆ print_dot_psl()

std::ostream& spot::print_dot_psl	(	std::ostream &	os,
		formula	f
	)

#include <spot/tl/dot.hh>

Write a formula tree using dot's syntax.

Parameters

os	The stream where it should be output.
f	The formula to translate.

dot is part of the GraphViz package http://www.graphviz.org/

◆ print_latex_psl()

std::ostream& spot::print_latex_psl	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a PSL formula as a LaTeX string.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_latex_sere()

std::ostream& spot::print_latex_sere	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a SERE formula as a LaTeX string.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_lbt_ltl()

std::ostream& spot::print_lbt_ltl	(	std::ostream &	os,
		formula	f
	)

#include <spot/tl/print.hh>

Output an LTL formula as a string in LBT's format.

The formula must be an LTL formula (ELTL and PSL operators are not supported). The M and W operator will be output as-is, because this is accepted by LBTT, however if you plan to use the output with other tools, you should probably rewrite these two operators using unabbreviate_wm().

Parameters

f	The formula to translate.
os	The stream where it should be output.

◆ print_psl()

std::ostream& spot::print_psl	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a PSL formula as a string which is parsable.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_sclatex_psl()

std::ostream& spot::print_sclatex_psl	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a PSL formula as a self-contained LaTeX string.

The result cannot be parsed back.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_sclatex_sere()

std::ostream& spot::print_sclatex_sere	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a SERE formula as a self-contained LaTeX string.

The result cannot be parsed back.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_sere()

std::ostream& spot::print_sere	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a SERE formula as a string which is parsable.

Parameters

f	The formula to translate.
os	The stream where it should be output.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_spin_ltl()

std::ostream& spot::print_spin_ltl	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output an LTL formula as a string parsable by Spin.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_utf8_psl()

std::ostream& spot::print_utf8_psl	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a PSL formula as an utf-8 string which is parsable.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_utf8_sere()

std::ostream& spot::print_utf8_sere	(	std::ostream &	os,
		formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a SERE formula as a utf-8 string which is parsable.

Parameters

os	The stream where it should be output.
f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ print_wring_ltl()

std::ostream& spot::print_wring_ltl	(	std::ostream &	os,
		formula	f
	)

#include <spot/tl/print.hh>

Output an LTL formula as a string parsable by Wring.

Parameters

os	The stream where it should be output.
f	The formula to translate.

◆ str_latex_psl()

std::string spot::str_latex_psl	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulae).

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_latex_sere()

std::string spot::str_latex_sere	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a SERE formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulae).

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_lbt_ltl()

std::string spot::str_lbt_ltl ( formula f )

#include <spot/tl/print.hh>

Output an LTL formula as a string in LBT's format.

The formula must be an LTL formula (ELTL and PSL operators are not supported). The M and W operator will be output as-is, because this is accepted by LBTT, however if you plan to use the output with other tools, you should probably rewrite these two operators using unabbreviate_wm().

Parameters

f	The formula to translate.

◆ str_psl()

std::string spot::str_psl	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Convert a PSL formula into a string which is parsable.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_sclatex_psl()

std::string spot::str_sclatex_psl	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a PSL formula as a self-contained LaTeX string.

The result cannot be parsed bacl.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_sclatex_sere()

std::string spot::str_sclatex_sere	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Output a SERE formula as a self-contained LaTeX string.

The result cannot be parsed bacl.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_sere()

std::string spot::str_sere	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Convert a SERE formula into a string which is parsable.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_spin_ltl()

std::string spot::str_spin_ltl	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Convert an LTL formula into a string parsable by Spin.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_utf8_psl()

std::string spot::str_utf8_psl	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Convert a PSL formula into a utf-8 string which is parsable.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_utf8_sere()

std::string spot::str_utf8_sere	(	formula	f,
		bool	full_parent = `false`
	)

#include <spot/tl/print.hh>

Convert a SERE formula into a string which is parsable.

Parameters

f	The formula to translate.
full_parent	Whether or not the string should by fully parenthesized.

◆ str_wring_ltl()

std::string spot::str_wring_ltl ( formula f )

#include <spot/tl/print.hh>

Convert a formula into a string parsable by Wring.

Parameters

f	The formula to translate.

Classes

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ one_parse_error

◆ parse_error_list

Function Documentation

◆ fix_utf8_locations()

◆ parse_formula()

◆ parse_infix_boolean()

◆ parse_infix_psl()

◆ parse_infix_sere()

◆ parse_prefix_ltl()

◆ print_dot_psl()

◆ print_latex_psl()

◆ print_latex_sere()

◆ print_lbt_ltl()

◆ print_psl()

◆ print_sclatex_psl()

◆ print_sclatex_sere()

◆ print_sere()

◆ print_spin_ltl()

◆ print_utf8_psl()

◆ print_utf8_sere()

◆ print_wring_ltl()

◆ str_latex_psl()

◆ str_latex_sere()

◆ str_lbt_ltl()

◆ str_psl()

◆ str_sclatex_psl()

◆ str_sclatex_sere()

◆ str_sere()

◆ str_spin_ltl()

◆ str_utf8_psl()

◆ str_utf8_sere()

◆ str_wring_ltl()