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

Merge emptinesscheckexplicit into ltl2tgba.

Browse source 
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove
emptinesscheckexplicit.
(emptinesscheckexplicit_SOURCES): Remove.
(TESTS): Replace emptinesscheckexplicit.test by emptchke.test.
* src/tgbatest/emptinesscheckexplicit.cc,
src/tgbatest/emptinesscheckexplicit.test: Delete.
* src/tgbatest/empchke.test: New file.
* src/tgbatest/ltl2tgba.cc: Add support for -X.
This commit is contained in:
Alexandre Duret-Lutz 2003-10-23 11:58:11 +00:00
parent 65f84e2c61
commit d46c63a21b
5 changed files with 45 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,5 +1,15 @@
2003-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
Merge emptinesscheckexplicit into ltl2tgba.
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove
emptinesscheckexplicit.
(emptinesscheckexplicit_SOURCES): Remove.
(TESTS): Replace emptinesscheckexplicit.test by emptchke.test.
* src/tgbatest/emptinesscheckexplicit.cc,
src/tgbatest/emptinesscheckexplicit.test: Delete.
* src/tgbatest/empchke.test: New file.
* src/tgbatest/ltl2tgba.cc: Add support for -X.
Merge emptiness-checks tests into ltl2tgba.
* src/tgbatest/Makefile (check_PRORGRAMS): Remove
emptinesscheck and ltlmagic.

4
src/tgbatest/Makefile.am
View file

@ -6,7 +6,6 @@ check_SCRIPTS = defs
check_PROGRAMS = \
bddprod \
explicit \
emptinesscheckexplicit \
explprod \
ltl2tgba \
ltlprod \
@ -18,7 +17,6 @@ check_PROGRAMS = \
# Keep this sorted alphabetically.
bddprod_SOURCES = ltlprod.cc
bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
emptinesscheckexplicit_SOURCES = emptinesscheckexplicit.cc
explicit_SOURCES = explicit.cc
explprod_SOURCES = explprod.cc
ltl2tgba_SOURCES = ltl2tgba.cc
@ -43,7 +41,7 @@ TESTS = \
tripprod.test \
mixprod.test \
emptchk.test \
emptinesscheckexplicit.test \
emptchke.test \
spotlbtt.test
EXTRA_DIST = $(TESTS)

3
src/tgbatest/emptinesscheckexplicit.test → src/tgbatest/emptchke.test
View file

@ -11,4 +11,5 @@ s1, "s2", a!b, c d;
"state 3", s1,,;
EOF
./emptinesscheckexplicit input > stdout
./ltl2tgba -e -X input
./ltl2tgba -m -X input

46
src/tgbatest/emptinesscheckexplicit.cc
View file

@ -1,46 +0,0 @@
#include <iostream>
#include "tgbaparse/public.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/emptinesscheck.hh"
void
syntax(char* prog)
{
std::cerr << prog << " [-d] filename" << std::endl;
exit(2);
}
int
main(int argc, char** argv)
{
int exit_code = 0;
if (argc < 2)
syntax(argv[0]);
bool debug = false;
int filename_index = 1;
if (!strcmp(argv[1], "-d"))
{
debug = true;
if (argc < 3)
syntax(argv[0]);
filename_index = 2;
}
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
pel, dict, env, debug);
spot::emptiness_check empty_check;
if (spot::format_tgba_parse_errors(std::cerr, pel))
return 2;
bool emptiness = empty_check.tgba_emptiness_check(a);
empty_check.counter_example(a);
delete a;
return 0;
}

43
src/tgbatest/ltl2tgba.cc
View file

@ -13,12 +13,14 @@
#include "tgba/tgbatba.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/emptinesscheck.hh"
#include "tgbaparse/public.hh"
void
syntax(char* prog)
{
std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl
<< " "<< prog << " -F [OPTIONS...] file" << std::endl
<< " "<< prog << " -X [OPTIONS...] file" << std::endl
<< std::endl
<< "Options:" << std::endl
<< " -a display the accepting_conditions BDD, not the "
@ -45,6 +47,8 @@ syntax(char* prog)
<< " -R same as -r, but as a set" << std::endl
<< " -t display reachable states in LBTT's format" << std::endl
<< " -v display the BDD variables used by the automaton"
<< std::endl
<< " -X do compute an automaton, read it from a file"
<< std::endl;
exit(2);
}
@ -63,6 +67,7 @@ main(int argc, char** argv)
enum { None, Couvreur, MagicSearch } echeck = None;
bool magic_many = false;
bool expect_counter_example = false;
bool from_file = false;
for (;;)
{
@ -145,6 +150,10 @@ main(int argc, char** argv)
{
output = 5;
}
else if (!strcmp(argv[formula_index], "-X"))
{
from_file = true;
}
else
{
break;
@ -174,24 +183,36 @@ main(int argc, char** argv)
}
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(input, pel, env, debug_opt);
exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
spot::bdd_dict* dict = new spot::bdd_dict();
if (f)
spot::ltl::formula* f = 0;
if (!from_file)
{
spot::ltl::parse_error_list pel;
f = spot::ltl::parse(input, pel, env, debug_opt);
exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
}
if (f || from_file)
{
spot::tgba_bdd_concrete* concrete = 0;
spot::tgba* to_free = 0;
spot::tgba* a = 0;
if (fm_opt)
to_free = a = spot::ltl_to_tgba_fm(f, dict);
if (from_file)
{
spot::tgba_parse_error_list pel;
to_free = a = spot::tgba_parse(input, pel, dict, env, debug_opt);
if (spot::format_tgba_parse_errors(std::cerr, pel))
return 2;
}
else
to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
spot::ltl::destroy(f);
{
if (fm_opt)
to_free = a = spot::ltl_to_tgba_fm(f, dict);
else
to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
spot::ltl::destroy(f);
}
spot::tgba_tba_proxy* degeneralized = 0;
if (degeneralize_opt)