diff --git a/Makefile.am b/Makefile.am index 5b39e86b2..a39f9a90b 100644 --- a/Makefile.am +++ b/Makefile.am @@ -49,6 +49,7 @@ DEBIAN = \ debian/libbddx-dev.install \ debian/libspot0.install \ debian/libspotltsmin0.install \ + debian/libspotgen0.install \ debian/libspot-dev.install \ debian/python3-spot.examples \ debian/python3-spot.install \ diff --git a/NEWS b/NEWS index d44b85f80..9c9c56fd1 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,10 @@ New in spot 2.3.3.dev (not yet released) Library: + - Add a new library libspotgen. It is intended to be place to gather + functions that generate classes of formulas and automata from the + literature. This separation should ease future development. + - spot::sum() and spot::sum_and() implements the union and the intersection of two automatons, respectively. diff --git a/README b/README index 1249a4c4d..77b59c777 100644 --- a/README +++ b/README @@ -186,6 +186,7 @@ spot/ Sources for libspot. twa/ TωA objects and cousins (Transition-based ω-Automata). twaalgos/ Algorithms on TωA. gtec/ Couvreur's Emptiness-Check. + gen/ Sources for libspotgen. bin/ Command-line tools built on top of libspot. man/ Man pages for the above tools. tests/ Test suite. diff --git a/configure.ac b/configure.ac index 3e5a3bfe3..bc4957266 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, +# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016-2017, # 2017 Laboratoire de Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis @@ -279,6 +279,7 @@ AC_CONFIG_FILES([ spot/twaalgos/gtec/Makefile spot/twaalgos/Makefile spot/twa/Makefile + spot/gen/Makefile python/ajax/Makefile python/Makefile tests/core/defs diff --git a/debian/control b/debian/control index 4e85589a0..e5ef049d4 100644 --- a/debian/control +++ b/debian/control @@ -11,7 +11,7 @@ Architecture: any Section: science Recommends: graphviz Suggests: libspot-dev, spot-doc, python3-spot -Depends: libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~), ${shlibs:Depends}, ${misc:Depends} +Depends: ${shlibs:Depends}, ${misc:Depends}, libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~), libspotgen0 (>= ${source:Version}), libspotgen0 (<< ${source:Version}.1~) Description: model checking and omega-automata manipulation library Tools to manipulate omega-automata as well as linear-time temporal logic (LTL & PSL). @@ -54,11 +54,19 @@ Description: headers for the BuDDy library Package: libspotltsmin0 Architecture: any Section: science -Recommends: graphviz Suggests: libspot-dev Depends: ${shlibs:Depends}, ${misc:Depends}, libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~) Description: interface between Spot and LTSmin models - Library load LTSmin models as Spot automata. + Library for loading LTSmin models as Spot automata. + +Package: libspotgen0 +Architecture: any +Section: science +Suggests: libspot-dev +Depends: ${shlibs:Depends}, ${misc:Depends}, libspot0 (>= ${source:Version}), libspot0 (<< ${source:Version}.1~) +Description: functions for generating formulas and automata in Spot + Library for generating families of formulas and automata + taken from the literature. Package: spot-doc Section: doc diff --git a/debian/libspotgen0.install b/debian/libspotgen0.install new file mode 100644 index 000000000..554a8651d --- /dev/null +++ b/debian/libspotgen0.install @@ -0,0 +1 @@ +usr/lib/*-*/libspotgen.so.* diff --git a/spot/Makefile.am b/spot/Makefile.am index 871523d72..3cd16c054 100644 --- a/spot/Makefile.am +++ b/spot/Makefile.am @@ -25,7 +25,7 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. Keep tests at the # end, after building '.' (since the current directory contains # libspot.la needed by the tests) -SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke \ +SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke gen \ parseaut parsetl . ltsmin lib_LTLIBRARIES = libspot.la diff --git a/spot/gen/Makefile.am b/spot/gen/Makefile.am new file mode 100644 index 000000000..6eabeb2c9 --- /dev/null +++ b/spot/gen/Makefile.am @@ -0,0 +1,30 @@ +## -*- coding: utf-8 -*- +## Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +## (LRDE). +## +## 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 3 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 this program. If not, see . + +AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +spotgendir = $(pkgincludedir)/gen +spotgen_HEADERS = automata.hh + +lib_LTLIBRARIES = libspotgen.la +libspotgen_la_SOURCES = \ + automata.cc +#libspotgen_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined $(SYMBOLIC_LDFLAGS) + diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc new file mode 100644 index 000000000..ed2fdde9e --- /dev/null +++ b/spot/gen/automata.cc @@ -0,0 +1,89 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Developpement de +// l'EPITA (LRDE). +// +// 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 3 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 this program. If not, see . + +#include +#include +#include + +namespace spot +{ + namespace gen + { + + twa_graph_ptr + ks_cobuchi(unsigned n) + { + // the alphabet has four letters: + // i, s (for sigma), p (for pi), h (for hash) + // we encode this four letters alphabet thanks to two AP a and b + // the exact encoding is not important + // each letter is a permutation of the set {1..2n} + // s = (1 2 .. 2n) the rotation + // p = (1 2) the swap of the first two elements + // i is the identity + // d is the identity on {2..2n} but is undefined on 1 + + // the automaton has 2n+1 states, numbered from 0 to 2n + // 0 is the initial state and the only non-deterministic state + + auto dict = make_bdd_dict(); + auto aut = make_twa_graph(dict); + + // register aps + aut->register_ap("a"); + aut->register_ap("b"); + + // retrieve the four letters, and name them + bdd i = formula_to_bdd(parse_formula("a&&b"), dict, aut); + bdd s = formula_to_bdd(parse_formula("a&&!b"), dict, aut); + bdd p = formula_to_bdd(parse_formula("!a&&b"), dict, aut); + bdd h = formula_to_bdd(parse_formula("!a&&!b"), dict, aut); + + // actually build the automaton + aut->new_states(2*n+1); + aut->set_init_state(0); + aut->set_acceptance(1, acc_cond::acc_code::cobuchi()); + + // from 0, we can non-deterministically jump to any state (except 0) with + // any letter. + for (unsigned q = 1; q <= 2*n; ++q) + aut->new_edge(0, q, bddtrue, {0}); + // i is the identity + for (unsigned q = 1; q <= 2*n; ++q) + aut->new_edge(q, q, i); + // p swaps 1 and 2, and leaves all other states invariant + aut->new_edge(1, 2, p); + aut->new_edge(2, 1, p); + for (unsigned q = 3; q <= 2*n; ++q) + aut->new_edge(q, q, p); + // s does to next state (mod 2*n, 0 excluded) + aut->new_edge(2*n, 1, s); + for (unsigned q = 1; q < 2*n; ++q) + aut->new_edge(q, q+1, s); + // h is the same as i, except on 1 where it goes back to the initial state + aut->new_edge(1, 0, h); + for (unsigned q = 2; q <= 2*n; ++q) + aut->new_edge(q, q, h); + + aut->merge_edges(); + return aut; + } + } +} + diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh new file mode 100644 index 000000000..8570e61fd --- /dev/null +++ b/spot/gen/automata.hh @@ -0,0 +1,48 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Developpement de +// l'EPITA (LRDE). +// +// 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 3 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 this program. If not, see . + +#pragma once + +#include + +namespace spot +{ + namespace gen + { + /// \brief A family of co-Büchi automata. + /// + /// ks_cobuchi(n) is a co-Büchi automaton of size 2n+1 that is + /// good-for-games and that has no equivalent deterministic co-Büchi + /// automaton with less than 2^n / (2n+1) states. + /// For details and other classes, see: + /// + /// @InProceedings{kuperberg2015determinisation, + /// author={Kuperberg, Denis and Skrzypczak, Micha{\l}}, + /// title={On Determinisation of Good-for-Games Automata}, + /// booktitle={International Colloquium on Automata, Languages, and + /// Programming}, + /// pages={299--310}, + /// year={2015}, + /// organization={Springer} + /// } + SPOT_API twa_graph_ptr + ks_cobuchi(unsigned n); + } +} +