From 7010a02cd92ba72e3b6be4ef3225cafa949076d1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 27 Oct 2004 11:18:13 +0000 Subject: [PATCH] * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: New files. * src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS, libevtgbaalgos_la_SOURCES): Add them. * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test: New files. * src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them. (ltl2evtgba_SOURCES): New variable. --- ChangeLog | 9 ++ src/evtgbaalgos/Makefile.am | 6 +- src/evtgbaalgos/tgba2evtgba.cc | 150 +++++++++++++++++++++++++++++++++ src/evtgbaalgos/tgba2evtgba.hh | 37 ++++++++ src/evtgbatest/Makefile.am | 5 +- src/evtgbatest/ltl2evtgba.cc | 135 +++++++++++++++++++++++++++++ src/evtgbatest/ltl2evtgba.test | 49 +++++++++++ 7 files changed, 388 insertions(+), 3 deletions(-) create mode 100644 src/evtgbaalgos/tgba2evtgba.cc create mode 100644 src/evtgbaalgos/tgba2evtgba.hh create mode 100644 src/evtgbatest/ltl2evtgba.cc create mode 100755 src/evtgbatest/ltl2evtgba.test diff --git a/ChangeLog b/ChangeLog index 54f64dcb4..b0d3d6125 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,14 @@ 2004-10-27 Alexandre Duret-Lutz + * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: + New files. + * src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS, + libevtgbaalgos_la_SOURCES): Add them. + * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test: + New files. + * src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them. + (ltl2evtgba_SOURCES): New variable. + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert that the true state has only one link when unobs is used. diff --git a/src/evtgbaalgos/Makefile.am b/src/evtgbaalgos/Makefile.am index a9c799141..5b23df795 100644 --- a/src/evtgbaalgos/Makefile.am +++ b/src/evtgbaalgos/Makefile.am @@ -27,10 +27,12 @@ evtgbaalgosdir = $(pkgincludedir)/evtgbaalgos evtgbaalgos_HEADERS = \ dotty.hh \ reachiter.hh \ - save.hh + save.hh \ + tgba2evtgba.hh noinst_LTLIBRARIES = libevtgbaalgos.la libevtgbaalgos_la_SOURCES = \ dotty.cc \ reachiter.cc \ - save.cc + save.cc \ + tgba2evtgba.cc diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc new file mode 100644 index 000000000..65789a99c --- /dev/null +++ b/src/evtgbaalgos/tgba2evtgba.cc @@ -0,0 +1,150 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "tgba2evtgba.hh" +#include "tgba/tgba.hh" +#include "evtgba/explicit.hh" +#include "tgbaalgos/reachiter.hh" +#include "ltlvisit/tostring.hh" +#include "ltlvisit/destroy.hh" + +namespace spot +{ + namespace + { + class tgba_to_evtgba_iter: + public tgba_reachable_iterator_depth_first + { + public: + tgba_to_evtgba_iter(const tgba* a) + : tgba_reachable_iterator_depth_first(a) + { + res = new evtgba_explicit; + } + + ~tgba_to_evtgba_iter() + { + } + + virtual void + start() + { + const rsymbol_set ss = + acc_to_symbol_set(automata_->all_acceptance_conditions()); + for (rsymbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i) + res->declare_acceptance_condition(*i); + } + + virtual void + process_state(const state* s, int n, tgba_succ_iterator*) + { + std::string str = this->automata_->format_state(s); + name_[n] = str; + if (n == 1) + res->set_init_state(str); + } + + virtual void + process_link(int in, int out, const tgba_succ_iterator* si) + { + // We might need to format out before process_state is called. + name_map_::const_iterator i = name_.find(out); + if (i == name_.end()) + { + const state* s = si->current_state(); + process_state(s, out, 0); + delete s; + } + + rsymbol_set ss = acc_to_symbol_set(si->current_acceptance_conditions()); + + bdd all = si->current_condition(); + while (all != bddfalse) + { + bdd one = bdd_satone(all); + all -= one; + while (one != bddfalse) + { + bdd low = bdd_low(one); + if (low == bddfalse) + { + const ltl::formula* v = + automata_->get_dict()->var_formula_map[bdd_var(one)]; + res->add_transition(name_[in], + to_string(v), + ss, + name_[out]); + break; + } + else + { + one = low; + } + } + assert(one != bddfalse); + } + } + + evtgba_explicit* res; + protected: + typedef std::map name_map_; + name_map_ name_; + + rsymbol_set + acc_to_symbol_set(bdd acc) const + { + rsymbol_set ss; + while (acc != bddfalse) + { + bdd one = bdd_satone(acc); + acc -= one; + while (one != bddfalse) + { + bdd low = bdd_low(one); + if (low == bddfalse) + { + const ltl::formula* v = + automata_->get_dict()->acc_formula_map[bdd_var(one)]; + ss.insert(rsymbol(to_string(v))); + break; + } + else + { + one = low; + } + } + assert(one != bddfalse); + } + return ss; + } + + }; + + } // anonymous + + evtgba_explicit* + tgba_to_evtgba(const tgba* a) + { + tgba_to_evtgba_iter i(a); + i.run(); + return i.res; + } +} // spot diff --git a/src/evtgbaalgos/tgba2evtgba.hh b/src/evtgbaalgos/tgba2evtgba.hh new file mode 100644 index 000000000..a58117046 --- /dev/null +++ b/src/evtgbaalgos/tgba2evtgba.hh @@ -0,0 +1,37 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH +# define SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH + +namespace spot +{ + class tgba; + class evtgba_explicit; + + /// \brief Convert a tgba into an evtgba. + /// + /// (This cannot be done on-the-fly because the alphabet of a tgba + /// as unknown beforehand.) + evtgba_explicit* tgba_to_evtgba(const tgba* a); +} + +#endif // SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH diff --git a/src/evtgbatest/Makefile.am b/src/evtgbatest/Makefile.am index 7e57db64d..aecb57847 100644 --- a/src/evtgbatest/Makefile.am +++ b/src/evtgbatest/Makefile.am @@ -26,11 +26,13 @@ LDADD = ../libspot.la check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ + ltl2evtgba \ explicit \ product \ readsave # Keep this sorted alphabetically. +ltl2evtgba_SOURCES = ltl2evtgba.cc explicit_SOURCES = explicit.cc product_SOURCES = product.cc readsave_SOURCES = readsave.cc @@ -40,7 +42,8 @@ readsave_SOURCES = readsave.cc TESTS = \ explicit.test \ readsave.test \ - product.test + product.test \ + ltl2evtgba.test EXTRA_DIST = $(TESTS) CLEANFILES = input1 input2 input3 stdout expected diff --git a/src/evtgbatest/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc new file mode 100644 index 000000000..4510c88c1 --- /dev/null +++ b/src/evtgbatest/ltl2evtgba.cc @@ -0,0 +1,135 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "evtgbaparse/public.hh" +#include "evtgbaalgos/save.hh" +#include "evtgbaalgos/dotty.hh" +#include "evtgbaalgos/tgba2evtgba.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " [-d] [-D] formula" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc < 2) + syntax(argv[0]); + + bool debug_opt = false; + bool dotty_opt = false; + + bool post_branching = false; + bool fair_loop_approx = false; + + int formula_index = 1; + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::ltl::atomic_prop_set* unobservables = new spot::ltl::atomic_prop_set; + + while (argv[formula_index][0] == '-' && formula_index < argc) + { + if (!strcmp(argv[formula_index], "-d")) + { + debug_opt = true; + } + else if (!strcmp(argv[formula_index], "-D")) + { + dotty_opt = true; + } + else if (!strcmp(argv[formula_index], "-L")) + { + fair_loop_approx = true; + } + else if (!strcmp(argv[formula_index], "-p")) + { + post_branching = true; + } + else if (!strncmp(argv[formula_index], "-U", 2)) + { + // Parse -U's argument. + const char* tok = strtok(argv[formula_index] + 2, ", \t;"); + while (tok) + { + unobservables->insert + (static_cast(env.require(tok))); + tok = strtok(0, ", \t;"); + } + } + else + { + syntax(argv[0]); + } + ++formula_index; + } + + if (formula_index == argc) + syntax(argv[0]); + + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::ltl::formula* f = 0; + + { + spot::ltl::parse_error_list pel; + f = spot::ltl::parse(argv[formula_index], pel, env, debug_opt); + exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], + pel); + } + + if (f) + { + spot::tgba* a = spot::ltl_to_tgba_fm(f, dict, false, true, + post_branching, + fair_loop_approx, unobservables); + + spot::ltl::destroy(f); + spot::evtgba* e = spot::tgba_to_evtgba(a); + + if (dotty_opt) + spot::dotty_reachable(std::cout, e); + else + spot::evtgba_save_reachable(std::cout, e); + + delete e; + delete a; + } + + for (spot::ltl::atomic_prop_set::iterator i = unobservables->begin(); + i != unobservables->end(); ++i) + spot::ltl::destroy(*i); + delete unobservables; + + delete dict; + + return exit_code; +} diff --git a/src/evtgbatest/ltl2evtgba.test b/src/evtgbatest/ltl2evtgba.test new file mode 100755 index 000000000..847745b7a --- /dev/null +++ b/src/evtgbatest/ltl2evtgba.test @@ -0,0 +1,49 @@ +#!/bin/sh +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +check () +{ + run 0 ./ltl2evtgba "$1" + run 0 ./ltl2evtgba -Uun1,un2,un3 "$1" +} + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +check a +check 'a U b' +check 'X a' +check 'a & b & c' +check 'a | b | (c U (d & (g U (h ^ i))))' +check 'Xa & (b U !a) & (b U !a)' +check 'Fa & Xb & GFc & Gd' +check 'Fa & Xa & GFc & Gc' +check 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +check 'a R (b R c)' +check '(a U b) U (c U d)' + +check '((Xp2)U(X(1)))*(p1 R(p2 R p0))'