diff --git a/ChangeLog b/ChangeLog index 7fa12f7ca3320fccad5aca1eb7c9ede076b67e9c..dde572efd2024e2a270a1ed784a4753f1df1c517 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,19 @@ 2003-06-05 Alexandre Duret-Lutz + * src/tgba/bddprint.cc (dict): Make this variable static. + (want_prom): New global static variable. + (print_handle): Honor want_prom. + (print_sat_handler, bdd_print_sat, bdd_format_sat): New functions. + (bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom. + * src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions. + * src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, + src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files. + * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add + save.cc and save.hh. + * src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave. + (readsave_SOURCES): New variable. + (TESTS): Add readsave.test. + * configure.ac: Output src/tgbaparse/Makefile. * src/Makefile.am (SUBDIRS): Add tgbaparse. (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la. diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 6ae64c719010e1723c59e431d8e1b4cb2ebbdc86..b020691884fea5d2baa03f691c9ecbe90c36b381 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -5,7 +5,10 @@ namespace spot { /// Global dictionary used by print_handler() to lookup variables. - const tgba_bdd_dict* dict; + static const tgba_bdd_dict* dict; + + /// Global flag to enable Prom[x] output (instead of `x'). + static bool want_prom; /// Stream handler used by Buddy to display BDD variables. static void @@ -20,7 +23,11 @@ namespace spot isi = dict->prom_formula_map.find(var); if (isi != dict->prom_formula_map.end()) { - o << "Prom["; to_string(isi->second, o) << "]"; + if (want_prom) + o << "Prom["; + to_string(isi->second, o); + if (want_prom) + o << "]"; } else { @@ -46,10 +53,49 @@ namespace spot } + static std::ostream* where; + static void + print_sat_handler(char* varset, int size) + { + bool not_first = false; + for (int v = 0; v < size; ++v) + { + if (varset[v] < 0) + continue; + if (not_first) + *where << " "; + else + not_first = true; + if (varset[v] == 0) + *where << "!"; + print_handler(*where, v); + } + } + + std::ostream& + bdd_print_sat(std::ostream& os, const tgba_bdd_dict& d, bdd b) + { + dict = &d; + where = &os; + want_prom = false; + assert (bdd_satone(b) == b); + bdd_allsat (b, print_sat_handler); + return os; + } + + std::string + bdd_format_sat(const tgba_bdd_dict& d, bdd b) + { + std::ostringstream os; + bdd_print_sat(os, d, b); + return os.str(); + } + std::ostream& bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b) { dict = &d; + want_prom = true; bdd_strm_hook(print_handler); os << bddset << b; bdd_strm_hook(0); @@ -68,6 +114,7 @@ namespace spot bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b) { dict = &d; + want_prom = true; bdd_strm_hook(print_handler); os << bdddot << b; bdd_strm_hook(0); @@ -78,6 +125,7 @@ namespace spot bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b) { dict = &d; + want_prom = true; bdd_strm_hook(print_handler); os << bddtable << b; bdd_strm_hook(0); diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index 0469b2b34680eed9cbdb9ba3102d26dc6ae5c549..b653b1d6c930f1f7eca10f54b1ca33da58ab880c 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -9,29 +9,46 @@ namespace spot { + /// \brief Print a BDD as a list of literals. + /// + /// This assumes that \a b is a conjunction of literals. + /// \param os The output stream. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. + std::ostream& bdd_print_sat(std::ostream& os, + const tgba_bdd_dict& dict, bdd b); + + /// \brief Format a BDD as a list of literals. + /// + /// This assumes that \a b is a conjunction of literals. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. + /// \return The BDD formated as a string. + std::string bdd_format_sat(const tgba_bdd_dict& dict, bdd b); + /// \brief Print a BDD as a set. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. - /// \param b The BDD to print. + /// \param b The BDD to print. std::ostream& bdd_print_set(std::ostream& os, const tgba_bdd_dict& dict, bdd b); /// \brief Format a BDD as a set. /// \param dict The dictionary to use, to lookup variables. - /// \param b The BDD to print. + /// \param b The BDD to print. /// \return The BDD formated as a string. std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b); /// \brief Print a BDD as a diagram in dotty format. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. - /// \param b The BDD to print. + /// \param b The BDD to print. std::ostream& bdd_print_dot(std::ostream& os, const tgba_bdd_dict& dict, bdd b); /// \brief Print a BDD as a table. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. - /// \param b The BDD to print. + /// \param b The BDD to print. std::ostream& bdd_print_table(std::ostream& os, const tgba_bdd_dict& dict, bdd b); diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 1ea6cb31646ee5c899b1373f24b9137b6b65dcf0..d897a3847a67bbc90b3986cf6d04590b19cee465 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -4,4 +4,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ dotty.cc \ - dotty.hh + dotty.hh \ + save.cc \ + save.hh + diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc new file mode 100644 index 0000000000000000000000000000000000000000..9395c663aff0ce7b3e0ca3969d1847e8de1facaf --- /dev/null +++ b/src/tgbaalgos/save.cc @@ -0,0 +1,52 @@ +#include +#include "tgba/tgba.hh" +#include "save.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + typedef std::set seen_set; + + /// Process successors. + static void + save_rec(std::ostream& os, const tgba& g, state* st, seen_set& m) + { + m.insert(st); + std::string cur = g.format_state(st); + tgba_succ_iterator* si = g.succ_iter(st); + for (si->first(); !si->done(); si->next()) + { + state* s = si->current_state(); + os << "\"" << cur << "\", \"" << g.format_state(s) << "\", "; + + bdd_print_sat(os, g.get_dict(), si->current_condition()) << ", "; + bdd_print_sat(os, g.get_dict(), si->current_promise()) << ";" + << std::endl; + + // Destination already explored? + seen_set::iterator i = m.find(s); + if (i != m.end()) + { + delete s; + } + else + { + save_rec(os, g, s, m); + // Do not delete S, it is used as key in M. + } + } + delete si; + } + + std::ostream& + tgba_save_reachable(std::ostream& os, const tgba& g) + { + seen_set m; + state* state = g.get_init_state(); + save_rec(os, g, state, m); + // Finally delete all states used as keys in m: + for (seen_set::iterator i = m.begin(); i != m.end(); ++i) + delete *i; + return os; + } +} diff --git a/src/tgbaalgos/save.hh b/src/tgbaalgos/save.hh new file mode 100644 index 0000000000000000000000000000000000000000..8bba7990813b803c146862ebf3ed3f6c45303639 --- /dev/null +++ b/src/tgbaalgos/save.hh @@ -0,0 +1,13 @@ +#ifndef SPOT_TGBAALGOS_SAVE_HH +# define SPOT_TGBAALGOS_SAVE_HH + +#include "tgba/tgba.hh" +#include + +namespace spot +{ + /// \brief Save reachable states in text format. + std::ostream& tgba_save_reachable(std::ostream& os, const tgba& g); +} + +#endif // SPOT_TGBAALGOS_SAVE_HH diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index a64121d548ce115cf368a792b9bc72599ddde8d8..87d1ecadcf9b63427fe2e6c2f46be43cd5298754 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -5,3 +5,4 @@ defs explicit .libs tgbaread +readsave diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e4bb9808f22942e45d4d60ea34edd487a9bf12da..40214e25cebbd00976531080f949cde6dc24450a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -5,14 +5,18 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ explicit \ + readsave \ tgbaread + explicit_SOURCES = explicit.cc +readsave_SOURCES = readsave.cc tgbaread_SOURCES = tgbaread.cc TESTS = \ explicit.test \ - tgbaread.test + tgbaread.test \ + readsave.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc new file mode 100644 index 0000000000000000000000000000000000000000..ed094c60d19d79fbb2d05e8ea75698391d59e317 --- /dev/null +++ b/src/tgbatest/readsave.cc @@ -0,0 +1,50 @@ +#include +#include "tgbaparse/public.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/save.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::tgba_explicit* a = spot::tgba_parse(argv[filename_index], + pel, env, debug); + + exit_code = + spot::format_tgba_parse_errors(std::cerr, pel); + + if (a) + { + spot::tgba_save_reachable(std::cout, *a); + delete a; + } + else + { + exit_code = 1; + } + return exit_code; +} diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test new file mode 100755 index 0000000000000000000000000000000000000000..04ea445d7df6f33bb086a75f439a9a0cade2df1d --- /dev/null +++ b/src/tgbatest/readsave.test @@ -0,0 +1,27 @@ +#!/bin/sh + +. ./defs + +set -e + +cat >input < stdout + +cat >expected < stdout +diff input stdout + +rm input stdout expected