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.

ChangeLog

+2009-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	* src/tgbatest/scc.test: New file.

configure.ac

-# 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), dpartement Systmes Rpartis
 # Coopratifs (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

src/Makefile.am

-## Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## dpartement Systmes Rpartis Coopratifs (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

src/kripke/Makefile.am

+## 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

src/kripke/fairkripke.cc

+// 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));
+  }
+}

src/kripke/fairkripke.hh

+// 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

src/kripke/kripke.cc

+// 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;
+  }
+
+}

src/kripke/kripke.hh

+// 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