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

Add ltl2aa binary to tests/core

Browse source
This commit is contained in:
Antoine Martin 2022-08-31 10:59:39 +02:00
parent ffd60219b5
commit 7b376a212c
3 changed files with 25 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tests/Makefile.am
View file

@ -76,6 +76,7 @@ check_PROGRAMS = \
core/intvcomp \ core/intvcomp \
core/intvcmp2 \ core/intvcmp2 \
core/kripkecat \ core/kripkecat \
core/ltl2aa \
core/ltl2dot \ core/ltl2dot \
core/ltl2text \ core/ltl2text \
core/ltlrel \ core/ltlrel \
@ -125,6 +126,7 @@ core_cube_SOURCES = core/cube.cc
core_equals_SOURCES = core/equalsf.cc core_equals_SOURCES = core/equalsf.cc
core_kind_SOURCES = core/kind.cc core_kind_SOURCES = core/kind.cc
core_length_SOURCES = core/length.cc core_length_SOURCES = core/length.cc
core_ltl2aa_SOURCES = core/ltl2aa.cc
core_ltl2dot_SOURCES = core/readltl.cc core_ltl2dot_SOURCES = core/readltl.cc
core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
core_ltl2text_SOURCES = core/readltl.cc core_ltl2text_SOURCES = core/readltl.cc

1
tests/core/.gitignore vendored
View file

@ -33,6 +33,7 @@ kripkecat
length length
.libs .libs
ikwiad ikwiad
ltl2aa
ltl2dot ltl2dot
ltl2text ltl2text
ltlmagic 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;
}