diff --git a/tests/Makefile.am b/tests/Makefile.am index 6f7abf994..9bf0cef73 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -76,6 +76,7 @@ check_PROGRAMS = \ core/intvcomp \ core/intvcmp2 \ core/kripkecat \ + core/ltl2aa \ core/ltl2dot \ core/ltl2text \ core/ltlrel \ @@ -125,6 +126,7 @@ core_cube_SOURCES = core/cube.cc core_equals_SOURCES = core/equalsf.cc core_kind_SOURCES = core/kind.cc core_length_SOURCES = core/length.cc +core_ltl2aa_SOURCES = core/ltl2aa.cc core_ltl2dot_SOURCES = core/readltl.cc core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY core_ltl2text_SOURCES = core/readltl.cc diff --git a/tests/core/.gitignore b/tests/core/.gitignore index d4ebfae45..fdee02715 100644 --- a/tests/core/.gitignore +++ b/tests/core/.gitignore @@ -33,6 +33,7 @@ kripkecat length .libs ikwiad +ltl2aa ltl2dot ltl2text ltlmagic diff --git a/tests/core/ltl2aa.cc b/tests/core/ltl2aa.cc new file mode 100644 index 000000000..82b4b9c7e --- /dev/null +++ b/tests/core/ltl2aa.cc @@ -0,0 +1,22 @@ +#include "config.h" + +#include + +#include +#include +#include +#include + +int main(int argc, char * argv[]) +{ + if (argc < 3) + return 1; + + spot::formula f = spot::parse_formula(argv[1]); + spot::bdd_dict_ptr d = spot::make_bdd_dict(); + auto aut = ltl_to_aa(f, d, true); + + std::ofstream out(argv[2]); + spot::print_hoa(out, aut); + return 0; +}