Add ltl2aa binary to tests/core

This commit is contained in:
Antoine Martin 2022-08-31 10:59:39 +02:00
parent bdf9762498
commit b1589b293a
3 changed files with 25 additions and 0 deletions

View file

@ -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

View file

@ -33,6 +33,7 @@ kripkecat
length
.libs
ikwiad
ltl2aa
ltl2dot
ltl2text
ltlmagic

22
tests/core/ltl2aa.cc Normal file
View file

@ -0,0 +1,22 @@
#include "config.h"
#include <fstream>
#include <spot/tl/formula.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/translate_aa.hh>
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;
}