alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlparse: rename the main functions

Browse source 
parse         -> parse_infix_psl
parse_lbt     -> parse_prefix_ltl
parse_sere    -> parse_infix_sere
parse_boolean -> parse_infix_boolean

Fixes #87.

* src/ltlparse/ltlparse.yy, src/ltlparse/public.hh:
Do the above changes.
* doc/mainpage.dox, doc/org/tut01.org, iface/ltsmin/modelcheck.cc,
src/bin/common_finput.cc, src/hoaparse/hoaparse.yy,
src/kripkeparse/kripkeparse.yy, src/tests/checkpsl.cc,
src/tests/checkta.cc, src/tests/complementation.cc,
src/tests/consterm.cc, src/tests/emptchk.cc, src/tests/equalsf.cc,
src/tests/kind.cc, src/tests/length.cc, src/tests/ltl2tgba.cc,
src/tests/ltlprod.cc, src/tests/ltlrel.cc, src/tests/randtgba.cc,
src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
src/tests/tostring.cc, wrap/python/ajax/spot.in,
wrap/python/tests/alarm.py, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-06-03 09:03:50 +02:00
parent aedce8101c
commit 98790f5345
29 changed files with 118 additions and 113 deletions
Download patch file Download diff file Expand all files Collapse all files

8
doc/mainpage.dox
View file

@ -20,13 +20,13 @@
/// \section pointers Handy starting points
///
/// \li spot::ltl::formula Base class for an LTL or PSL formula.
/// \li spot::ltl::parse Parsing a text string into a
/// \li spot::ltl::parse_infix_psl Parsing a text string into a
/// spot::ltl::formula.
/// \li spot::tgba Base class for Transition-based
/// Generalized Büchi Automaton.
/// \li spot::twa Base class for Transition-based
/// ω-Automata.
/// \li spot::translator Convert a spot::ltl::formula into a
/// spot::tgba.
/// \li spot::kripke Base class for Kripke structures.
/// \li spot::tgba_product On-the-fly product of two spot::tgba.
/// \li spot::twa_product On-the-fly product of two spot::twa.
/// \li spot::emptiness_check Base class for all emptiness-check algorithms
/// (see also module \ref emptiness_check)

21
doc/org/tut01.org
View file

@ -102,7 +102,7 @@ parser. Additionally, this give you control over how to print errors.
{
std::string input = "[]<>p0 || <>[]p1";
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f = spot::ltl::parse(input, pel);
const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
if (spot::ltl::format_parse_errors(std::cerr, input, pel))
{
if (f)
@ -119,10 +119,13 @@ parser. Additionally, this give you control over how to print errors.
: | G F p0 F G p1
: ([](<>(p0))) || (<>([](p1)))
So =parse()= process the =input=, and stores any diagnostic in =pel=,
which is a list of pairs associating each error to a location. You could
iterate over that list to print it by yourself as you wish, or you can
call =format_parse_errors()= to do that for you.
So =parse_infix_psl()= processes =input=, and stores any diagnostic in
=pel=, which is a list of pairs associating each error to a location.
You could iterate over that list to print it by yourself as you wish,
or you can call =format_parse_errors()= to do that for you. Note that
as its name implies, this parser can read more than LTL formulas (the
fragment of PSL we support is basically LTL extended with regular
expressions).
If =pel= is empty, =format_parse_errors()= will do nothing and return
false.
@ -147,7 +150,7 @@ with the "fixed" formula if you wish. Here is an example:
{
std::string input = "(a U b))";
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f = spot::ltl::parse(input, pel);
const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel);
// Use std::cout instead of std::cerr because we can only
// show the output of std::cout in this documentation.
(void) spot::ltl::format_parse_errors(std::cout, input, pel);
@ -186,8 +189,8 @@ currently this is done manually by calling =f->clone()= and
** Calling the prefix parser explicitly
The only difference here is the call to =parse_lbt()= instead of
=parse()=.
The only difference here is the call to =parse_prefix_ltl()= instead of
=parse_infix_psl()=.
#+BEGIN_SRC C++ :results verbatim :exports both
#include <string>
@ -199,7 +202,7 @@ The only difference here is the call to =parse_lbt()= instead of
{
std::string input = "& & G p0 p1 p2";
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f = spot::ltl::parse_lbt(input, pel);
const spot::ltl::formula* f = spot::ltl::parse_prefix_ltl(input, pel);
if (spot::ltl::format_parse_errors(std::cerr, input, pel))
{
if (f)