diff --git a/ChangeLog b/ChangeLog index e48051558..0371f5293 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2009-06-02 Alexandre Duret-Lutz + + Introduce some experimental kripke classes to simplify writing + interfaces. + + * src/kripke/Makefile.am, src/kripke/fairkripke.cc, + src/kripke/fairkripke.hh, src/kripke/kripke.cc, + src/kripke/kripke.hh: New files. + * src/Makefile.am: Recurse into kripke and link libkripke.la. + * configure.ac: Output src/kripke/Makefile. + 2009-06-02 Alexandre Duret-Lutz * src/tgbatest/scc.test: New file. diff --git a/configure.ac b/configure.ac index db8fe2478..f1f9bada8 100644 --- a/configure.ac +++ b/configure.ac @@ -1,4 +1,4 @@ -# Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire +# Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis # Coopératifs (SRC), Université Pierre et Marie Curie. # @@ -79,36 +79,37 @@ AC_CONFIG_FILES([ bench/ltl2tgba/defs doc/Doxyfile doc/Makefile - iface/Makefile - iface/gspn/Makefile iface/gspn/defs + iface/gspn/Makefile + iface/Makefile iface/nips/Makefile - iface/nips/nips_vm/Makefile - iface/nips/nipstest/Makefile iface/nips/nipstest/defs - src/Makefile + iface/nips/nipstest/Makefile + iface/nips/nips_vm/Makefile src/eltlparse/Makefile - src/eltltest/Makefile src/eltltest/defs - src/evtgba/Makefile + src/eltltest/Makefile src/evtgbaalgos/Makefile + src/evtgba/Makefile src/evtgbaparse/Makefile - src/evtgbatest/Makefile src/evtgbatest/defs + src/evtgbatest/Makefile + src/kripke/Makefile src/ltlast/Makefile src/ltlenv/Makefile src/ltlparse/Makefile - src/ltltest/Makefile src/ltltest/defs + src/ltltest/Makefile src/ltlvisit/Makefile + src/Makefile src/misc/Makefile src/sanity/Makefile - src/tgba/Makefile - src/tgbaalgos/Makefile src/tgbaalgos/gtec/Makefile + src/tgbaalgos/Makefile + src/tgba/Makefile src/tgbaparse/Makefile - src/tgbatest/Makefile src/tgbatest/defs + src/tgbatest/Makefile wrap/Makefile wrap/python/Makefile wrap/python/cgi/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 4dda23ced..d33944fe1 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -25,7 +25,8 @@ AUTOMAKE_OPTIONS = subdir-objects # Keep tests at the end. SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse \ tgba tgbaalgos tgbaparse \ - evtgba evtgbaalgos evtgbaparse . \ + evtgba evtgbaalgos evtgbaparse \ + kripke . \ ltltest eltltest tgbatest evtgbatest sanity lib_LTLIBRARIES = libspot.la @@ -43,7 +44,8 @@ libspot_la_LIBADD = \ tgbaparse/libtgbaparse.la \ evtgba/libevtgba.la \ evtgbaalgos/libevtgbaalgos.la \ - evtgbaparse/libevtgbaparse.la + evtgbaparse/libevtgbaparse.la \ + kripke/libkripke.la # Dummy C++ source to cause C++ linking. nodist_EXTRA_libspot_la_SOURCES = _.cc diff --git a/src/kripke/Makefile.am b/src/kripke/Makefile.am new file mode 100644 index 000000000..79169cfed --- /dev/null +++ b/src/kripke/Makefile.am @@ -0,0 +1,32 @@ +## Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +## +## 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. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +kripkedir = $(pkgincludedir)/kripke + +kripke_HEADERS = \ + fairkripke.hh \ + kripke.hh + +noinst_LTLIBRARIES = libkripke.la +libkripke_la_SOURCES = \ + fairkripke.cc \ + kripke.cc diff --git a/src/kripke/fairkripke.cc b/src/kripke/fairkripke.cc new file mode 100644 index 000000000..9b28daff5 --- /dev/null +++ b/src/kripke/fairkripke.cc @@ -0,0 +1,59 @@ +// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// +// 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 "fairkripke.hh" + +namespace spot +{ + + fair_kripke_succ_iterator::fair_kripke_succ_iterator(const fair_kripke* aut, + const state* st) + : cond(aut->conditions_of_state(st)), + acc_cond(aut->acceptance_conditions_of_state(st)) + { + } + + fair_kripke_succ_iterator::~fair_kripke_succ_iterator() + { + } + + bdd + fair_kripke_succ_iterator::current_conditions() const + { + return cond; + } + + bdd + fair_kripke_succ_iterator::current_acceptance_conditions() const + { + return acc_cond; + } + + bdd + fair_kripke::compute_support_conditions(const state* s) const + { + return conditions_of_state(s); + } + + bdd + fair_kripke::compute_support_variables(const state* s) const + { + return bdd_support(conditions_of_state(s)); + } +} diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh new file mode 100644 index 000000000..9ac67903d --- /dev/null +++ b/src/kripke/fairkripke.hh @@ -0,0 +1,62 @@ +// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// +// 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_KRIPKE_FAIRKRIPKE_HH +# define SPOT_KRIPKE_FAIRKRIPKE_HH + +#include "tgba/tgba.hh" +#include "tgba/succiter.hh" + +namespace spot +{ + class fair_kripke; + + class fair_kripke_succ_iterator : public tgba_succ_iterator + { + public: + fair_kripke_succ_iterator(const fair_kripke* aut, const state* st); + virtual ~fair_kripke_succ_iterator(); + + virtual bdd current_conditions() const; + virtual bdd current_acceptance_conditions() const; + protected: + bdd cond; + bdd acc_cond; + }; + + class fair_kripke : public tgba + { + public: + virtual bdd conditions_of_state(const state* s) const = 0; + virtual bdd acceptance_conditions_of_state(const state* s) const = 0; + virtual fair_kripke_succ_iterator* kripke_succ_iter(const state* s) = 0; + + virtual fair_kripke_succ_iterator* + succ_iter(const state* local_state, + const state* global_state = 0, + const tgba* global_automaton = 0); + protected: + virtual bdd compute_support_conditions(const state* s) const; + virtual bdd compute_support_variables(const state* s) const; + }; + +} + + +#endif // SPOT_KRIPKE_FAIRKRIPKE_HH diff --git a/src/kripke/kripke.cc b/src/kripke/kripke.cc new file mode 100644 index 000000000..bdb4f0eaf --- /dev/null +++ b/src/kripke/kripke.cc @@ -0,0 +1,42 @@ +// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// +// 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 "kripke.hh" + +namespace spot +{ + + bdd kripke::acceptance_conditions_of_state(const state*) const + { + // There is no acceptance conditions. + return bddfalse; + } + + bdd kripke::all_acceptance_conditions() const + { + // There is no acceptance conditions. + return bddfalse; + } + + bdd kripke::neg_acceptance_conditions() const + { + return bddtrue; + } + +} diff --git a/src/kripke/kripke.hh b/src/kripke/kripke.hh new file mode 100644 index 000000000..e74df560e --- /dev/null +++ b/src/kripke/kripke.hh @@ -0,0 +1,41 @@ +// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita +// +// 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_KRIPKE_KRIPKE_HH +# define SPOT_KRIPKE_KRIPKE_HH + +#include "fairkripke.hh" + +namespace spot +{ + + typedef fair_kripke_succ_iterator kripke_succ_iterator; + + class kripke: public fair_kripke + { + public: + virtual ~kripke(); + + virtual bdd acceptance_conditions_of_state(const state* s) const; + virtual bdd neg_acceptance_conditions() const; + virtual bdd all_acceptance_conditions() const; + }; +} + +#endif // SPOT_KRIPKE_KRIPKE_HH