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

Equip the LTL parser with printers for formulas and other token.

Browse source 
* src/ltlparse/ltlparse.yy: Add new printers.  Suggested by Akim
Demaille.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-10 10:11:11 +02:00
parent 509edabab4
commit ebe2362bc9
2 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
THANKS
View file

@ -1,6 +1,7 @@
We are grateful to these people for their comments, help, or We are grateful to these people for their comments, help, or
suggestions. suggestions.
Akim Demaille
Christian Dax Christian Dax
Étienne Renault Étienne Renault
Felix Klaedtke Felix Klaedtke

5
src/ltlparse/ltlparse.yy
View file

@ -35,6 +35,7 @@
#include <string> #include <string>
#include "public.hh" #include "public.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh"
struct minmax_t { unsigned min, max; }; struct minmax_t { unsigned min, max; };
} }
@ -144,6 +145,10 @@ using namespace spot::ltl;
%destructor { $$->destroy(); } <ltl> %destructor { $$->destroy(); } <ltl>
%printer { debug_stream() << *$$; } <str> %printer { debug_stream() << *$$; } <str>
%printer { spot::ltl::to_string($$, debug_stream()); } <ltl>
%printer { spot::ltl::to_string($$, debug_stream(), false, true); } sere bracedsere
%printer { debug_stream() << $$; } <num>
%printer { debug_stream() << $$.min << ".." << $$.max; } <minmax>
%% %%
result: START_LTL subformula END_OF_INPUT result: START_LTL subformula END_OF_INPUT