From 372d490712bc5c4804a6ee7addba3c33546002f1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 30 Jul 2003 12:44:50 +0000 Subject: [PATCH] * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES) (ltlgspn_srg_SOURCES): New variables. (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg. * iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install gspn.hh. --- ChangeLog | 8 +++++ iface/gspn/Makefile.am | 24 +++++++++++--- iface/gspn/dcswaveltl.test | 9 +++++ iface/gspn/ltlgspn.cc | 68 ++++++++++++++++++++++++++++++++++++++ src/tgba/tgbatba.cc | 2 +- src/tgbaalgos/magic.hh | 2 +- 6 files changed, 106 insertions(+), 7 deletions(-) create mode 100755 iface/gspn/dcswaveltl.test create mode 100644 iface/gspn/ltlgspn.cc diff --git a/ChangeLog b/ChangeLog index 114dc438d..2d2a7697d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2003-07-30 Alexandre Duret-Lutz + * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. + (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES) + (ltlgspn_srg_SOURCES): New variables. + (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg. + + * iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install + gspn.hh. + * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::project_state): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index 633eb9d01..3ae655b7a 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -1,14 +1,21 @@ AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) $(LIBGSPN_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) +gspndir = $(pkgincludedir)/gspn + +gspn_HEADERS = \ + gspn.hh + lib_LTLIBRARIES = libspotgspn.la libspotgspn_la_LIBADD = $(top_builddir)/src/libspot.la libspotgspn_la_SOURCES = \ - gspn.hh \ - gspn.cc \ - gspnlib.h + gspn.cc -check_PROGRAMS = dottygspn-rg dottygspn-srg +check_PROGRAMS = \ + dottygspn-rg \ + dottygspn-srg \ + ltlgspn-rg \ + ltlgspn-srg dottygspn_rg_SOURCES = dottygspn.cc dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) @@ -16,6 +23,12 @@ dottygspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) dottygspn_srg_SOURCES = dottygspn.cc dottygspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) +ltlgspn_rg_SOURCES = ltlgspn.cc +ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) + +ltlgspn_srg_SOURCES = ltlgspn.cc +ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) + EXTRA_DIST = \ examples/DCSwave/DCSWave.def \ examples/DCSwave/DCSWave.net \ @@ -27,7 +40,8 @@ EXTRA_DIST = \ TESTS = \ simple.test \ - dcswave.test + dcswave.test \ + dcswaveltl.test # Each test case depends on defs. check_SCRIPTS = defs diff --git a/iface/gspn/dcswaveltl.test b/iface/gspn/dcswaveltl.test new file mode 100755 index 000000000..e1287a7b2 --- /dev/null +++ b/iface/gspn/dcswaveltl.test @@ -0,0 +1,9 @@ +#! /bin/sh + +. ./defs || exit 1 + +set -e + +cp -R $srcdir/examples/DCSwave . + +../ltlgspn-srg DCSwave/DCSWave '!G(ATTiIDLj => F(!SCj U SCi))' ATTiIDLj SCi SCj > output diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc new file mode 100644 index 000000000..71a2640b0 --- /dev/null +++ b/iface/gspn/ltlgspn.cc @@ -0,0 +1,68 @@ +#include "gspn.hh" +#include "ltlparse/public.hh" +#include "ltlvisit/destroy.hh" +#include "tgba/tgbatba.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/ltl2tgba.hh" +#include "tgbaalgos/magic.hh" + +int +main(int argc, char **argv) + try + { + spot::gspn_environment env; + + if (argc <= 3) + { + std::cerr << "usage: " << argv[0] + << " model formula props..." << std::endl; + exit(1); + } + + while (argc > 3) + { + env.declare(argv[argc - 1]); + --argc; + } + + spot::ltl::parse_error_list pel; + spot::ltl::formula* f = spot::ltl::parse(argv[2], pel, env); + + if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel)) + exit(1); + + spot::gspn_interface gspn(2, argv); + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::tgba* a_f = spot::ltl_to_tgba(f, dict); + spot::ltl::destroy(f); + + spot::tgba* model = new spot::tgba_gspn(dict, env); + spot::tgba_product* prod = new spot::tgba_product(model, a_f); + spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod); + + { + spot::magic_search ms(d); + + if (ms.check()) + { + ms.print_result (std::cout, model); + exit(1); + } + else + { + std::cout << "not found"; + } + } + + delete d; + delete prod; + delete model; + delete a_f; + delete dict; + } + catch (spot::gspn_exeption e) + { + std::cerr << e << std::endl; + throw; + } diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index d3b04289f..92df1ffdd 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -219,7 +219,7 @@ namespace spot + bdd_format_set(get_dict(), s->accepting_cond()) + ")"; } - state* + state* tgba_tba_proxy::project_state(const state* s, const tgba* t) const { const state_tba_proxy* s2 = dynamic_cast(s); diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 482929889..da2388adc 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -50,7 +50,7 @@ namespace spot /// /// Restrict printed states to \a the state space of restrict if /// supplied. - std::ostream& print_result(std::ostream& os, + std::ostream& print_result(std::ostream& os, const tgba* restrict = 0) const; private: