...
 
Commits (124)
......@@ -197,12 +197,15 @@ spot/ Sources for libspot.
kripke/ Kripke Structure interface.
tl/ Temporal Logic formulas and algorithms.
misc/ Miscellaneous support files.
mc/ All algorithms useful for model checking
parseaut/ Parser for automata in multiple formats.
parsetl/ Parser for LTL/PSL formulas.
priv/ Private algorithms, used internally but not exported.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
twa/ TωA objects and cousins (Transition-based ω-Automata).
twacube/ TωA objects based on cube (not-bdd).
twacube_algos/ TωAcube algorithms
twaalgos/ Algorithms on TωA.
gtec/ Couvreur's Emptiness-Check.
gen/ Sources for libspotgen.
......@@ -238,6 +241,7 @@ lib/ Gnulib's portability modules.
utf8/ Nemanja Trifunovic's utf-8 routines.
elisp/ Related emacs modes, used for building the documentation.
picosat/ A distribution of PicoSAT 965 (a satsolver library).
spot/bricks/ A collection of useful C++ code provided by DiVinE 3.3.2
Build-system stuff
------------------
......
......@@ -142,6 +142,7 @@ fi
AX_CHECK_BUDDY
AC_CHECK_HEADERS([sys/times.h valgrind/memcheck.h])
AX_CHECK_DIVINE
AC_CHECK_FUNCS([times kill alarm sigaction])
LT_CONFIG_LTDL_DIR([ltdl])
......@@ -234,6 +235,7 @@ AC_CONFIG_FILES([
spot/ltsmin/Makefile
spot/Makefile
spot/misc/Makefile
spot/mc/Makefile
spot/parseaut/Makefile
spot/parsetl/Makefile
spot/priv/Makefile
......@@ -242,8 +244,10 @@ AC_CONFIG_FILES([
spot/tl/Makefile
spot/twaalgos/gtec/Makefile
spot/twaalgos/Makefile
spot/twacube_algos/Makefile
spot/twa/Makefile
spot/gen/Makefile
spot/twacube/Makefile
python/Makefile
tests/core/defs
tests/ltsmin/defs:tests/core/defs.in
......
......@@ -49,6 +49,33 @@ License: BSD-2-Clause
OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
MODIFICATIONS.
Files: spot/bricks/*
Copyright: 2010-2014 Petr Ročkai, Jiří Weiser, Vladimír Štill
License: BSD-2-Clause
Permission is hereby granted, without written agreement and without
license or royalty fees, to use, reproduce, prepare derivative
works, distribute, and display this software and its documentation
for any purpose, provided that (1) the above copyright notice and
the following two paragraphs appear in all copies of the source code
and (2) redistributions, including without limitation binaries,
reproduce these notices in the supporting documentation. Substantial
modifications to this software may be copyrighted by their authors
and need not follow the licensing terms described here, provided
that the new terms are clearly indicated in all files where they apply.
.
IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
.
JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
MODIFICATIONS.
Files: utf8/*
Copyright: 2006 Nemanja Trifunovic
License: BSL-1.0
......
usr/include/spot
usr/include/spot/bricks
usr/lib/*-*/libspot.so
usr/lib/*-*/libspot.a
usr/lib/*-*/pkgconfig/libspot.pc
......
......@@ -27,19 +27,19 @@ LTOPLUG := $(shell gcc -v 2>&1 | \
# ARFLAGS is for Automake
# AR_FLAGS is for Libtool
LTOSETUP = \
LDFLAGS='-fuse-linker-plugin' \
NM='nm --plugin $(LTOPLUG)' \
ARFLAGS='cru --plugin $(LTOPLUG)' \
AR_FLAGS='cru --plugin $(LTOPLUG)' \
RANLIB='ranlib --plugin $(LTOPLUG)' \
LTOSETUP = \
LDFLAGS='-fuse-linker-plugin' \
NM='nm --plugin $(LTOPLUG)' \
ARFLAGS='cru --plugin $(LTOPLUG)' \
AR_FLAGS='cru --plugin $(LTOPLUG)' \
RANLIB='ranlib --plugin $(LTOPLUG)'
VALGRIND=false
PRO1SETUP = \
CFLAGS='-flto -fprofile-generate' \
PRO1SETUP = \
CFLAGS='-flto -fprofile-generate' \
CXXFLAGS='-flto -fprofile-generate'
PRO2SETUP = \
CFLAGS='-flto -fprofile-use' \
CXXFLAGS='-flto -fprofile-use'
PRO2SETUP = \
CFLAGS='-flto -fprofile-use -fprofile-correction' \
CXXFLAGS='-flto -fprofile-use -fprofile-correction'
PYDEFAULT=$(shell py3versions --default)
PYOTHERS=$(filter-out $(PYDEFAULT), $(shell py3versions --supported))
......
......@@ -22,11 +22,16 @@
AUTOMAKE_OPTIONS = subdir-objects
nobase_include_HEADERS= bricks/brick-assert bricks/brick-bitlevel \
bricks/brick-hash bricks/brick-hashset bricks/brick-shmem \
bricks/brick-types
# 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 \
parseaut parsetl . ltsmin gen
SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \
twacube_algos mc parseaut parsetl . ltsmin gen
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
......@@ -42,6 +47,9 @@ libspot_la_LIBADD = \
tl/libtl.la \
twaalgos/libtwaalgos.la \
twa/libtwa.la \
twacube_algos/libtwacube_algos.la \
twacube/libtwacube.la \
mc/libmc.la \
../lib/libgnu.la \
../picosat/libpico.la
......
// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-
/*
* Various assert macros based on C++ exceptions and their support code.
*/
/*
* (c) 2006-2016 Petr Ročkai <code@fixp.eu>
*
* Permission to use, copy, modify, and distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*/
#include <exception>
#include <string>
#include <sstream>
#ifndef TEST
#define TEST(n) void n()
#define TEST_FAILING(n) void n()
#endif
#ifndef NDEBUG
#define BRICK_SHARP_FIRST(x, ...) #x
#define ASSERT(...) ::brick::_assert::assert_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( BRICK_SHARP_FIRST( __VA_ARGS__, ignored ) ) ), __VA_ARGS__ )
#define ASSERT_PRED(p, x) ::brick::_assert::assert_pred_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( #p "( " #x " )" ) ), x, p( x ) )
#define ASSERT_EQ(x, y) ::brick::_assert::assert_eq_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( #x " == " #y ) ), x, y )
#define ASSERT_LT(x, y) ::brick::_assert::assert_lt_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( #x " < " #y ) ), x, y )
#define ASSERT_LEQ(x, y) ::brick::_assert::assert_leq_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( #x " <= " #y ) ), x, y )
#define ASSERT_NEQ(x, y) ::brick::_assert::assert_neq_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( #x " != " #y ) ), x, y )
#define ASSERT_EQ_IDX(i, x, y) ::brick::_assert::assert_eq_fn( \
BRICK_LOCWRAP( BRICK_LOCATION_I( #x " == " #y, i ) ), x, y )
#else
#define ASSERT(...) static_cast< decltype(__VA_ARGS__, void(0)) >(0)
#define ASSERT_PRED(p, x) static_cast< decltype(p, x, void(0)) >(0)
#define ASSERT_EQ(x, y) static_cast< decltype(x, y, void(0)) >(0)
#define ASSERT_LEQ(x, y) static_cast< decltype(x, y, void(0)) >(0)
#define ASSERT_LT(x, y) static_cast< decltype(x, y, void(0)) >(0)
#define ASSERT_NEQ(x, y) static_cast< decltype(x, y, void(0)) >(0)
#define ASSERT_EQ_IDX(i, x, y) static_cast< decltype(i, x, y, void(0)) >(0)
#endif
/* you must #include <brick-string> to use ASSERT_UNREACHABLE_F */
#define UNREACHABLE_F(...) ::brick::_assert::assert_die_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( brick::string::fmtf(__VA_ARGS__) ) ) )
#define UNREACHABLE(...) ::brick::_assert::assert_die_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( ::brick::_assert::fmt( __VA_ARGS__ ) ) ) )
#define UNREACHABLE_() ::brick::_assert::assert_die_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( "an unreachable location" ) ) )
#define NOT_IMPLEMENTED() ::brick::_assert::assert_die_fn( \
BRICK_LOCWRAP( BRICK_LOCATION( "a missing implementation" ) ) )
#ifdef _MSC_VER
#define UNUSED
#define noexcept
#else
#define UNUSED __attribute__((unused))
#endif
#ifndef BRICK_ASSERT_H
#define BRICK_ASSERT_H
namespace brick {
namespace _assert {
/* discard any number of parameters, taken as const references */
template< typename... X >
void unused( const X&... ) { }
struct Location {
int line, iteration;
std::string file, stmt;
Location( const char *f, int l, std::string st, int iter = -1 )
: line( l ), iteration( iter ), file( f ), stmt( st )
{
int slashes = 0;
for ( int i = 0; i < int( file.size() ); ++i )
if ( file[i] == '/' )
++ slashes;
while ( slashes >= 3 )
{
file = std::string( file, file.find( "/" ) + 1, std::string::npos );
-- slashes;
}
if ( f != file )
file = ".../" + file;
}
};
#define BRICK_LOCATION(stmt) ::brick::_assert::Location( __FILE__, __LINE__, stmt )
#define BRICK_LOCATION_I(stmt, i) ::brick::_assert::Location( __FILE__, __LINE__, stmt, i )
// lazy location construction in C++11
#if __cplusplus >= 201103L
#define BRICK_LOCWRAP(x) [&]{ return (x); }
#define BRICK_LOCUNWRAP(x) (x)()
#else
#define BRICK_LOCWRAP(x) (x)
#define BRICK_LOCUNWRAP(x) (x)
#endif
struct AssertFailed : std::exception
{
std::string str;
template< typename X >
friend inline AssertFailed &operator<<( AssertFailed &f, X x )
{
std::stringstream str;
str << x;
f.str += str.str();
return f;
}
AssertFailed( Location l, const char *expected = "expected" )
{
(*this) << l.file << ": " << l.line;
if ( l.iteration != -1 )
(*this) << " (iteration " << l.iteration << ")";
(*this) << ":\n " << expected << " " << l.stmt;
}
const char *what() const noexcept override { return str.c_str(); }
};
static inline void format( AssertFailed & ) {}
template< typename X, typename... Y >
void format( AssertFailed &f, X x, Y... y )
{
f << x;
format( f, y... );
}
template< typename Location, typename X, typename... Y >
void assert_fn( Location l, X x, Y... y )
{
if ( x )
return;
AssertFailed f( BRICK_LOCUNWRAP( l ) );
format( f, y... );
throw f;
}
template< typename Location >
inline void assert_die_fn( Location l ) __attribute__((noreturn));
template< typename Location >
inline void assert_die_fn( Location l )
{
throw AssertFailed( BRICK_LOCUNWRAP( l ), "encountered" );
}
#define ASSERT_FN(name, op, inv) \
template< typename Location > \
void assert_ ## name ## _fn( Location l, int64_t x, int64_t y ) \
{ \
if ( !( x op y ) ) { \
AssertFailed f( BRICK_LOCUNWRAP( l ) ); \
f << "\n but got " \
<< x << " " #inv " " << y << "\n"; \
throw f; \
} \
} \
\
template< typename Location, typename X, typename Y > \
auto assert_ ## name ## _fn( Location l, X x, Y y ) \
-> typename std::enable_if< \
!std::is_integral< X >::value || \
!std::is_integral< Y >::value >::type \
{ \
if ( !( x op y ) ) { \
AssertFailed f( BRICK_LOCUNWRAP( l ) ); \
f << "\n but got " \
<< x << " " #inv " " << y << "\n"; \
throw f; \
} \
}
ASSERT_FN(eq, ==, !=)
ASSERT_FN(leq, <=, >)
ASSERT_FN(lt, <, >=)
template< typename Location, typename X >
void assert_pred_fn( Location l, X x, bool p )
{
if ( !p ) {
AssertFailed f( BRICK_LOCUNWRAP( l ) );
f << "\n but got x = " << x << "\n";
throw f;
}
}
template< typename Location, typename X, typename Y >
void assert_neq_fn( Location l, X x, Y y )
{
if ( x != y )
return;
AssertFailed f( BRICK_LOCUNWRAP( l ) );
f << "\n but got "
<< x << " == " << y << "\n";
throw f;
}
inline std::string fmt( const char *str ) { return str; }
inline std::string fmt( std::string str ) { return str; }
// another overload of fmt is exported by brick-string and it allows more complex formating
}
}
#endif
// vim: syntax=cpp tabstop=4 shiftwidth=4 expandtab
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2013, 2014, 2016 Laboratoire de Recherche
// Copyright (C) 2009, 2010, 2013, 2014, 2016, 2017 Laboratoire de Recherche
// et Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
......@@ -20,9 +20,81 @@
#pragma once
#include <spot/kripke/fairkripke.hh>
#include <spot/twacube/cube.hh>
#include <memory>
namespace spot
{
/// \brief This class is a template representation of a Kripke
/// structure. It is composed of two template parameters: State
/// represents a state of the Kripke structure, SuccIterator is
/// an iterator over the (possible) successors of a state.
///
/// Do not delete by hand any states and/or iterator that
/// are provided by this template class. Specialisations
/// will handle it.
template<typename State, typename SuccIterator>
class SPOT_API kripkecube:
public std::enable_shared_from_this<kripkecube<State, SuccIterator>>
{
public:
/// \brief Returns the initial State of the System. The \a tid parameter
/// is used internally for sharing this structure among threads.
State initial(unsigned tid);
/// \brief Provides a string representation of the parameter state
std::string to_string(const State, unsigned tid) const;
/// \brief Returns an iterator over the successors of the parameter state.
SuccIterator* succ(const State, unsigned tid);
/// \brief Allocation and deallocation of iterator is costly. This
/// method allows to reuse old iterators.
void recycle(SuccIterator*, unsigned tid);
/// \brief This method allow to deallocate a given state.
const std::vector<std::string> get_ap();
};
/// \brief This method allows to ensure (at compile time) if
/// a given parameter is of type kripkecube. It also check
/// if the iterator has the good interface.
template <typename State, typename SuccIter>
bool is_a_kripkecube(kripkecube<State, SuccIter>&)
{
// Hardly waiting C++17 concepts...
State (kripkecube<State, SuccIter>::*test_initial)(unsigned) =
&kripkecube<State, SuccIter>::initial;
std::string (kripkecube<State, SuccIter>::*test_to_string)
(const State, unsigned) const = &kripkecube<State, SuccIter>::to_string;
void (kripkecube<State, SuccIter>::*test_recycle)(SuccIter*, unsigned) =
&kripkecube<State, SuccIter>::recycle;
const std::vector<std::string>
(kripkecube<State, SuccIter>::*test_get_ap)() =
&kripkecube<State, SuccIter>::get_ap;
void (SuccIter::*test_next)() = &SuccIter::next;
State (SuccIter::*test_state)() const= &SuccIter::state;
bool (SuccIter::*test_done)() const= &SuccIter::done;
cube (SuccIter::*test_condition)() const = &SuccIter::condition;
void (SuccIter::*test_fireall)() = &SuccIter::fireall;
bool (SuccIter::*test_naturally_expanded)() const =
&SuccIter::naturally_expanded;
// suppress warnings about unused variables
(void) test_initial;
(void) test_to_string;
(void) test_recycle;
(void) test_get_ap;
(void) test_next;
(void) test_state;
(void) test_done;
(void) test_condition;
(void) test_fireall;
(void) test_naturally_expanded;
// Always return true since otherwise a compile-time error will be raised.
return true;
}
/// \ingroup kripke
/// \brief Iterator code for Kripke structure
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.