Commit d90e38eb authored by Maximilien Colange's avatar Maximilien Colange
Browse files

Add a new library to generate formulas and automata.

This library, called libspotgen, gathers functions to generate classes
of automata found in the literature.
Related to #254.

* NEWS, README: Mention the modification.
* Makefile.am, debian/control, debian/libspotgen0.install: Build the new
  library in a separate package.
* spot/gen/automata.hh, spot/gen/automata.cc: Add a family of co-Büchi
  automata.
* configure.ac, spot/Makefile.am, spot/gen/Makefile.am: Build the new
  library.
parent b428ed31
......@@ -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 \
......
......@@ -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.
......
......@@ -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.
......
# -*- 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
......
......@@ -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
......
usr/lib/*-*/libspotgen.so.*
......@@ -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
......
## -*- 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 <http://www.gnu.org/licenses/>.
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)
// -*- 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 <http://www.gnu.org/licenses/>.
#include <spot/gen/automata.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/tl/parse.hh>
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;
}
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/twa/twagraph.hh>
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);
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment