spot  2.3.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Classes | Typedefs | Functions
Input and Output of Formulas

Classes

struct  spot::parsed_formula
 The result of a formula parser. More...
 
class  spot::random_formula
 Base class for random formula generators. More...
 
struct  spot::random_formula::op_proba
 
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

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

#include <spot/tl/parse.hh>

A parse diagnostic with its location.

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

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_stringThe string that were parsed.
error_listThe error list filled by spot::parse or spot::parse_sere while parsing input_string.
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.

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_stringThe string to parse.
envThe environment into which parsing should take place.
debugWhen true, causes the parser to trace its execution.
lenientWhen 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.
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_stringThe string to parse.
envThe environment into which parsing should take place.
debugWhen true, causes the parser to trace its execution.
lenientWhen 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.
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_stringThe string to parse.
envThe environment into which parsing should take place.
debugWhen true, causes the parser to trace its execution.
lenientWhen 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.
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_stringThe string to parse.
envThe environment into which parsing should take place.
debugWhen 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.
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
osThe stream where it should be output.
fThe formula to translate.

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

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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
osThe stream where it should be output.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
osThe stream where it should be output.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
osThe stream where it should be output.
fThe formula to translate.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
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
fThe formula to translate.
full_parentWhether or not the string should by fully parenthesized.
std::string spot::str_wring_ltl ( formula  f)

#include <spot/tl/print.hh>

Convert a formula into a string parsable by Wring.

Parameters
fThe formula to translate.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Feb 20 2017 07:08:25 for spot by doxygen 1.8.8