From 3991a51a1747563250f8bb80f1e15f9077029365 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Jun 2003 12:45:11 +0000 Subject: [PATCH] * src/ltlvisit/clone.cc (clone): New const version. * src/ltlvisit/clone.hh (clone): Likewise. * src/ltlvisit/destroy.cc (destroy): New const version. * src/ltlvisit/destroy.hh (destroy): Likewise. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::create_state, tgba_bdd_concrete_factory::create_atomic_prop, tgba_bdd_concrete_factory::promise): Clone new formulae. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict, tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods that clone and destroy formulae. * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba. (ltl2tgba_SOURCES): New variable. (TESTS): Add ltl2tgba.test. --- ChangeLog | 16 ++++++++ src/ltlvisit/clone.cc | 5 +++ src/ltlvisit/clone.hh | 2 + src/ltlvisit/destroy.cc | 8 +++- src/ltlvisit/destroy.hh | 2 + src/tgba/tgbabddconcretefactory.cc | 10 ++++- src/tgba/tgbabdddict.cc | 45 +++++++++++++++++++++++ src/tgba/tgbabdddict.hh | 5 +++ src/tgbatest/.cvsignore | 1 + src/tgbatest/Makefile.am | 8 ++-- src/tgbatest/ltl2tgba.cc | 59 ++++++++++++++++++++++++++++++ src/tgbatest/ltl2tgba.test | 15 ++++++++ 12 files changed, 170 insertions(+), 6 deletions(-) create mode 100644 src/tgbatest/ltl2tgba.cc create mode 100755 src/tgbatest/ltl2tgba.test diff --git a/ChangeLog b/ChangeLog index 592bf6de8..867db1019 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,21 @@ 2003-06-06 Alexandre Duret-Lutz + * src/ltlvisit/clone.cc (clone): New const version. + * src/ltlvisit/clone.hh (clone): Likewise. + * src/ltlvisit/destroy.cc (destroy): New const version. + * src/ltlvisit/destroy.hh (destroy): Likewise. + * src/tgba/tgbabddconcretefactory.cc + (tgba_bdd_concrete_factory::create_state, + tgba_bdd_concrete_factory::create_atomic_prop, + tgba_bdd_concrete_factory::promise): Clone new formulae. + * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict, + tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods + that clone and destroy formulae. + * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files. + * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba. + (ltl2tgba_SOURCES): New variable. + (TESTS): Add ltl2tgba.test. + * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include . diff --git a/src/ltlvisit/clone.cc b/src/ltlvisit/clone.cc index f9a976f87..8b3a04507 100644 --- a/src/ltlvisit/clone.cc +++ b/src/ltlvisit/clone.cc @@ -70,5 +70,10 @@ namespace spot return v.result(); } + formula* + clone(const formula* f) + { + return clone(const_cast(f)); + } } } diff --git a/src/ltlvisit/clone.hh b/src/ltlvisit/clone.hh index 6a4dcf97b..fc29d2125 100644 --- a/src/ltlvisit/clone.hh +++ b/src/ltlvisit/clone.hh @@ -36,6 +36,8 @@ namespace spot /// \brief Clone a formula. formula* clone(formula* f); + /// \brief Clone a formula. + formula* clone(const formula* f); } } diff --git a/src/ltlvisit/destroy.cc b/src/ltlvisit/destroy.cc index 5ab24ef6e..b5f0f253e 100644 --- a/src/ltlvisit/destroy.cc +++ b/src/ltlvisit/destroy.cc @@ -16,10 +16,16 @@ namespace spot }; void - destroy(formula *f) + destroy(formula* f) { destroy_visitor v; f->accept(v); } + + void + destroy(const formula* f) + { + destroy(const_cast(f)); + } } } diff --git a/src/ltlvisit/destroy.hh b/src/ltlvisit/destroy.hh index 375c4f57d..ed236bf13 100644 --- a/src/ltlvisit/destroy.hh +++ b/src/ltlvisit/destroy.hh @@ -9,6 +9,8 @@ namespace spot { /// \brief Destroys a formula void destroy(formula *f); + /// \brief Destroys a formula + void destroy(const formula *f); } } diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index a60ce8056..92791d806 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -1,6 +1,7 @@ +#include "ltlvisit/clone.hh" #include "tgbabddconcretefactory.hh" -namespace spot +namespace spot { tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory() { @@ -14,8 +15,9 @@ namespace spot if (sii != dict_.now_map.end()) return sii->second; - int num = create_pair(); + f = clone(f); + int num = create_pair(); dict_.now_map[f] = num; dict_.now_formula_map[num] = f; @@ -37,6 +39,8 @@ namespace spot if (sii != dict_.var_map.end()) return sii->second; + f = clone(f); + int num = create_node(); dict_.var_map[f] = num; dict_.var_formula_map[num] = f; @@ -55,6 +59,8 @@ namespace spot if (sii != dict_.prom_map.end()) return sii->second; + f = clone(f); + int num = create_node(); dict_.prom_map[f] = num; dict_.prom_formula_map[num] = f; diff --git a/src/tgba/tgbabdddict.cc b/src/tgba/tgbabdddict.cc index 32213b799..5c67d83e3 100644 --- a/src/tgba/tgbabdddict.cc +++ b/src/tgba/tgbabdddict.cc @@ -1,5 +1,7 @@ #include "tgbabdddict.hh" #include "ltlvisit/tostring.hh" +#include "ltlvisit/clone.hh" +#include "ltlvisit/destroy.hh" namespace spot { @@ -55,4 +57,47 @@ namespace spot return true; } + tgba_bdd_dict::tgba_bdd_dict() + { + } + + tgba_bdd_dict::tgba_bdd_dict(const tgba_bdd_dict& other) + : now_map(other.now_map), + now_formula_map(other.now_formula_map), + var_map(other.var_map), + var_formula_map(other.var_formula_map), + prom_map(other.prom_map), + prom_formula_map(other.prom_formula_map) + { + fv_map::iterator i; + for (i = now_map.begin(); i != now_map.end(); ++i) + ltl::clone(i->first); + for (i = var_map.begin(); i != var_map.end(); ++i) + ltl::clone(i->first); + for (i = prom_map.begin(); i != prom_map.end(); ++i) + ltl::clone(i->first); + } + + tgba_bdd_dict& + tgba_bdd_dict::operator=(const tgba_bdd_dict& other) + { + if (this != &other) + { + this->~tgba_bdd_dict(); + new (this) tgba_bdd_dict(other); + } + return *this; + } + + tgba_bdd_dict::~tgba_bdd_dict() + { + fv_map::iterator i; + for (i = now_map.begin(); i != now_map.end(); ++i) + ltl::destroy(i->first); + for (i = var_map.begin(); i != var_map.end(); ++i) + ltl::destroy(i->first); + for (i = prom_map.begin(); i != prom_map.end(); ++i) + ltl::destroy(i->first); + } + } diff --git a/src/tgba/tgbabdddict.hh b/src/tgba/tgbabdddict.hh index 9b4d6e199..39778207f 100644 --- a/src/tgba/tgbabdddict.hh +++ b/src/tgba/tgbabdddict.hh @@ -29,6 +29,11 @@ namespace spot /// Whether this dictionary contains \a other. bool contains(const tgba_bdd_dict& other) const; + + tgba_bdd_dict(); + tgba_bdd_dict(const tgba_bdd_dict& other); + tgba_bdd_dict& operator=(const tgba_bdd_dict& other); + ~tgba_bdd_dict(); }; } diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index 87d1ecadc..668c496f5 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -6,3 +6,4 @@ explicit .libs tgbaread readsave +ltl2tgba diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 40214e25c..e57b913d5 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -6,17 +6,19 @@ check_SCRIPTS = defs check_PROGRAMS = \ explicit \ readsave \ - tgbaread - + tgbaread \ + ltl2tgba explicit_SOURCES = explicit.cc +ltl2tgba_SOURCES = ltl2tgba.cc readsave_SOURCES = readsave.cc tgbaread_SOURCES = tgbaread.cc TESTS = \ explicit.test \ tgbaread.test \ - readsave.test + readsave.test \ + ltl2tgba.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc new file mode 100644 index 000000000..470648b5e --- /dev/null +++ b/src/tgbatest/ltl2tgba.cc @@ -0,0 +1,59 @@ +#include +#include +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgba/ltl2tgba.hh" +#include "tgbaalgos/dotty.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " [-d] formula" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc < 2) + syntax(argv[0]); + + bool debug = false; + int formula_index = 1; + + if (!strcmp(argv[1], "-d")) + { + debug = true; + if (argc < 3) + syntax(argv[0]); + formula_index = 2; + } + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::parse_error_list pel; + spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], + pel, env, debug); + + exit_code = + spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); + + if (f) + { + spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f); + spot::ltl::destroy(f); + spot::dotty_reachable(std::cout, a); + } + else + { + exit_code = 1; + } + + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + return exit_code; +} diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test new file mode 100755 index 000000000..107e51d64 --- /dev/null +++ b/src/tgbatest/ltl2tgba.test @@ -0,0 +1,15 @@ +#!/bin/sh + +. ./defs + +set -e + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +./ltl2tgba a +./ltl2tgba 'a U b' +./ltl2tgba 'X a' +./ltl2tgba 'a & b & c' +./ltl2tgba 'a | b | (c U (d & (g U (h ^ i))))' +./ltl2tgba 'Xa & (b U !a) & (b U !a)'