From fd12c02345e6abdf473b6958ee18bb27afa13c4b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Jun 2003 14:54:30 +0000 Subject: [PATCH] * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): New constructor. * src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product): New constructor. * tgbatest/tripprod.cc, tgbatest/tripprod.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (tripprod_SOURCES): New variable. (CLEANFILES): Add input3. (TESTS): Add tripprod.test. --- ChangeLog | 13 +++++++++ src/tgba/tgbaproduct.cc | 7 +++++ src/tgba/tgbaproduct.hh | 3 +++ src/tgbatest/.cvsignore | 1 + src/tgbatest/Makefile.am | 13 +++++---- src/tgbatest/explprod.cc | 4 +-- src/tgbatest/tripprod.cc | 54 ++++++++++++++++++++++++++++++++++++++ src/tgbatest/tripprod.test | 39 +++++++++++++++++++++++++++ 8 files changed, 127 insertions(+), 7 deletions(-) create mode 100644 src/tgbatest/tripprod.cc create mode 100755 src/tgbatest/tripprod.test diff --git a/ChangeLog b/ChangeLog index ad1d99836..1506606f1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2003-06-17 Alexandre Duret-Lutz + + * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): + New constructor. + * src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product): + New constructor. + * tgbatest/tripprod.cc, tgbatest/tripprod.test: New files. + * src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod. + (tripprod_SOURCES): New variable. + (CLEANFILES): Add input3. + (TESTS): Add tripprod.test. + 2003-06-16 Alexandre Duret-Lutz * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ... @@ -46,6 +58,7 @@ * tgba/tgbaexplicit.cc (state_explicit::clone): New method. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise): Call ltl::destroy on existing formulae. + * tgbatest/explprod.cc, tgbatest/explprod.test: New files. * tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (explprod_SOURCES): New variable. (TESTS): Add explprod.test. diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 802f2f05d..b3f601418 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -9,6 +9,13 @@ namespace spot //////////////////////////////////////////////////////////// // state_bdd_product + state_bdd_product::state_bdd_product(const state_bdd_product& o) + : state_bdd(o.as_bdd()), + left_(o.left()->clone()), + right_(o.right()->clone()) + { + } + state_bdd_product::~state_bdd_product() { delete left_; diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index b712bf686..fff1d9fea 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -26,6 +26,9 @@ namespace spot { } + /// Copy constructor + state_bdd_product(const state_bdd_product& o); + virtual ~state_bdd_product(); state* diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index c0c095c1a..096d7bc17 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -12,3 +12,4 @@ bddprod explprod *.ps *.dot +tripprod diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 49929a83c..e3e9c85b9 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -10,16 +10,18 @@ check_PROGRAMS = \ ltl2tgba \ ltlprod \ bddprod \ - explprod + explprod \ + tripprod -bddprod_SOURCES = ltlprod.cc +bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT explicit_SOURCES = explicit.cc explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc -ltlprod_SOURCES = ltlprod.cc +ltlprod_SOURCES = ltlprod.cc readsave_SOURCES = readsave.cc tgbaread_SOURCES = tgbaread.cc +tripprod_SOURCES = tripprod.cc TESTS = \ explicit.test \ @@ -28,8 +30,9 @@ TESTS = \ ltl2tgba.test \ ltlprod.test \ bddprod.test \ - explprod.test + explprod.test \ + tripprod.test EXTRA_DIST = $(TESTS) -CLEANFILES = input input1 input2 stdout expected +CLEANFILES = input input1 input2 input3 stdout expected diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 48f02286c..5af25b041 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -29,9 +29,9 @@ main(int argc, char** argv) return 2; spot::tgba_parse_error_list pel2; spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); - if (spot::format_tgba_parse_errors(std::cerr, pel1)) + if (spot::format_tgba_parse_errors(std::cerr, pel2)) return 2; - + { spot::tgba_product p(*a1, *a2); spot::tgba_save_reachable(std::cout, p); diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc new file mode 100644 index 000000000..eae80c873 --- /dev/null +++ b/src/tgbatest/tripprod.cc @@ -0,0 +1,54 @@ +#include +#include +#include "tgba/ltl2tgba.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaparse/public.hh" +#include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " file1 file2 file3" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc != 4) + syntax(argv[0]); + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel1; + spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env); + if (spot::format_tgba_parse_errors(std::cerr, pel1)) + return 2; + spot::tgba_parse_error_list pel2; + spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); + if (spot::format_tgba_parse_errors(std::cerr, pel2)) + return 2; + spot::tgba_parse_error_list pel3; + spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, env); + if (spot::format_tgba_parse_errors(std::cerr, pel3)) + return 2; + + { + spot::tgba_product p(*a1, *a2); + spot::tgba_product p2(p, *a3); + spot::tgba_save_reachable(std::cout, p2); + } + + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::atomic_prop::instance_count() != 0); + delete a1; + delete a2; + delete a3; + assert(spot::ltl::atomic_prop::instance_count() == 0); + return exit_code; +} diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test new file mode 100755 index 000000000..bf53e8546 --- /dev/null +++ b/src/tgbatest/tripprod.test @@ -0,0 +1,39 @@ +#!/bin/sh + +. ./defs + +set -e + +cat >input1 <input2 <input3 <expected < stdout + +cat stdout +diff stdout expected +rm input1 input2 input3 stdout expected