// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// 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 .
%{
// Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef.
// It matters with g++ 4.6.
#include
%}
%module(package="spot", director="1") impl
%include "std_shared_ptr.i"
%include "std_vector.i"
%include "std_string.i"
%include "std_list.i"
%include "std_set.i"
%include "std_map.i"
%include "std_pair.i"
%include "stdint.i"
%include "exception.i"
%include "typemaps.i"
// git grep 'typedef.*std::shared_ptr' | grep -v const |
// sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g'
%shared_ptr(spot::dstar_aut)
%shared_ptr(spot::parsed_aut)
%shared_ptr(spot::fair_kripke)
%shared_ptr(spot::kripke)
%shared_ptr(spot::kripke_graph)
%shared_ptr(spot::kripke)
%shared_ptr(spot::ta)
%shared_ptr(spot::ta_explicit)
%shared_ptr(spot::ta_product)
%shared_ptr(spot::tgta)
%shared_ptr(spot::tgta_explicit)
%shared_ptr(spot::bdd_dict)
%shared_ptr(spot::twa)
%shared_ptr(spot::twa_graph)
%shared_ptr(spot::twa_product)
%shared_ptr(spot::twa_product_init)
%shared_ptr(spot::taa_tgba)
%shared_ptr(spot::taa_tgba_string)
%shared_ptr(spot::taa_tgba_formula)
%shared_ptr(spot::twa_run)
%shared_ptr(spot::twa_word)
%shared_ptr(spot::emptiness_check_result)
%shared_ptr(spot::emptiness_check)
%shared_ptr(spot::emptiness_check_instantiator)
%shared_ptr(spot::tgbasl)
%import "buddy.i"
%{
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
#include
using namespace spot;
%}
// Swig come with iterators that implement a decrement method. This
// is not supported in our "successor" iterators. Also we want
// iterators to return pointers so that data can be modified during
// iteration.
%fragment("ForwardIterator_T","header",fragment="SwigPyIterator_T") {
namespace swig
{
template::pointer,
typename FromOper = from_oper >
class ForwardIterator_T : public SwigPyIterator_T
{
public:
FromOper from;
typedef OutIterator out_iterator;
typedef ValueType value_type;
typedef SwigPyIterator_T base;
ForwardIterator_T(out_iterator curr, out_iterator first,
out_iterator last, PyObject *seq)
: SwigPyIterator_T(curr, seq), begin(first), end(last)
{
}
PyObject *value() const {
if (base::current == end) {
throw stop_iteration();
} else {
return from(static_cast(&*(base::current)));
}
}
SwigPyIterator *copy() const
{
return new ForwardIterator_T(*this);
}
SwigPyIterator *incr(size_t n = 1)
{
while (n--) {
if (base::current == end) {
throw stop_iteration();
} else {
++base::current;
}
}
return this;
}
protected:
out_iterator begin;
out_iterator end;
};
template
inline SwigPyIterator*
make_forward_iterator(const OutIter& current,
const OutIter& begin,
const OutIter& end, PyObject *seq = 0)
{
return new ForwardIterator_T(current, begin, end, seq);
}
// Likewise, but without returning a pointer.
template::value_type,
typename FromOper = from_oper >
class ForwardIterator_T_NP : public SwigPyIterator_T
{
public:
FromOper from;
typedef OutIterator out_iterator;
typedef ValueType value_type;
typedef SwigPyIterator_T base;
ForwardIterator_T_NP(out_iterator curr, out_iterator first,
out_iterator last, PyObject *seq)
: SwigPyIterator_T(curr, seq), begin(first), end(last)
{
}
PyObject *value() const {
if (base::current == end) {
throw stop_iteration();
} else {
return from(static_cast(*(base::current)));
}
}
SwigPyIterator *copy() const
{
return new ForwardIterator_T_NP(*this);
}
SwigPyIterator *incr(size_t n = 1)
{
while (n--) {
if (base::current == end) {
throw stop_iteration();
} else {
++base::current;
}
}
return this;
}
protected:
out_iterator begin;
out_iterator end;
};
template
inline SwigPyIterator*
make_forward_iterator_np(const OutIter& current,
const OutIter& begin,
const OutIter& end, PyObject *seq = 0)
{
return new ForwardIterator_T_NP(current, begin, end, seq);
}
}
}
%fragment("ForwardIterator_T");
// For spot::emptiness_check_instantiator::construct and any other
// function that return errors via a "char **err" argument.
%typemap(in, numinputs=0) char** OUTPUT (char* temp) {
$1 = &temp;
}
%typemap(argout) char** OUTPUT {
PyObject *obj = SWIG_FromCharPtr(*$1);
if (!$result) {
$result = obj;
//# If the function returns null_ptr (i.e. Py_None), we
//# don't want to override it with OUTPUT as in the
//# default implementation of t_output_helper.
// } else if ($result == Py_None) {
// Py_DECREF($result);
// $result = obj;
} else {
if (!PyList_Check($result)) {
PyObject *o2 = $result;
$result = PyList_New(1);
PyList_SetItem($result, 0, o2);
}
PyList_Append($result, obj);
Py_DECREF(obj);
}
};
%apply char** OUTPUT { char** err };
// This is mainly for acc_cond::is_parity()
%typemap(in, numinputs=0) bool& (bool temp) {
$1 = &temp;
};
%typemap(argout) bool& {
PyObject *obj = SWIG_From_bool(*$1);
if (!$result) {
$result = obj;
} else {
if (!PyList_Check($result)) {
PyObject *o2 = $result;
$result = PyList_New(1);
PyList_SetItem($result, 0, o2);
}
PyList_Append($result, obj);
Py_DECREF(obj);
}
};
// Allow None to be passed for formula. Some functions like
// postprocessor::run() take an optional formula that defaults to
// nullptr. So it make sense to have function that take formulas that
// default to None on the Python side.
%typemap(in) spot::formula {
void *tmp;
int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*), 0);
if (!SWIG_IsOK(res)) {
%argument_fail(res, "spot::formula", $symname, $argnum);
}
if (tmp) {
spot::formula* temp = reinterpret_cast< spot::formula * >(tmp);
$1 = *temp;
if (SWIG_IsNewObj(res)) delete temp;
}
// if tmp == nullptr, then the default value of $1 is fine.
}
%typemap(typecheck) spot::formula {
$1 = SWIG_CheckState(SWIG_ConvertPtr($input, nullptr,
$descriptor(spot::formula*), 0));
}
%typemap(out) spot::formula {
if (!$1)
$result = SWIG_Py_Void();
else
$result = SWIG_NewPointerObj(new spot::formula($1), $descriptor(spot::formula*), SWIG_POINTER_OWN);
}
%typemap(out) std::string* {
if (!$1)
$result = SWIG_Py_Void();
else
$result = SWIG_FromCharPtr($1->c_str());
}
%exception {
try {
$action
}
catch (const spot::parse_error& e)
{
std::string er("\n");
er += e.what();
SWIG_exception(SWIG_SyntaxError, er.c_str());
}
catch (const std::invalid_argument& e)
{
SWIG_exception(SWIG_ValueError, e.what());
}
catch (const std::runtime_error& e)
{
SWIG_exception(SWIG_RuntimeError, e.what());
}
}
%include
%include
%include
%include
%include
%include
%implicitconv spot::trival;
%include
%implicitconv std::vector;
%include
namespace std {
%template(liststr) list;
%template(vectorformula) vector;
%template(vectorunsigned) vector;
%template(vectorstring) vector;
%template(atomic_prop_set) set;
%template(relabeling_map) map;
}
%include
%include
%include
/* these must come before apcollect.hh */
%include
%include
%include
%implicitconv spot::acc_cond::mark_t;
%implicitconv spot::acc_cond::acc_code;
%feature("flatnested") spot::acc_cond::mark_t;
%feature("flatnested") spot::acc_cond::acc_code;
%apply bool* OUTPUT {bool& max, bool& odd};
%include
%template(pair_bool_mark) std::pair;
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%nodefaultctor spot::digraph;
%nodefaultctor spot::internal::state_out;
%nodefaultctor spot::internal::all_trans;
%nodefaultctor spot::internal::universal_dests;
%traits_swigtype(spot::internal::edge_storage >);
%fragment(SWIG_Traits_frag(spot::internal::edge_storage >));
%typemap(out, optimal="1") spot::internal::all_trans> {
$result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor,
SWIG_POINTER_OWN);
}
%typemap(out, optimal="1") spot::internal::const_universal_dests {
$result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor,
SWIG_POINTER_OWN);
}
%noexception spot::twa_graph::edges;
%noexception spot::twa_graph::univ_dests;
// Instead of %feature("shadow") we would like to use just
// %pythonprepend spot::twa_graph::out %{ self.report_univ_dest(src) %}
// However Swig 3.0.2 (from Debian stable) names the argument "*args"
// while Swig 3.0.10 uses "src", and we want to be compatible with both.
%feature("shadow") spot::twa_graph::out %{
def out(self, src: 'unsigned int'):
self.report_univ_dest(src)
return $action(self, src)
%}
%feature("shadow") spot::twa_graph::state_from_number %{
def state_from_number(self, s: 'unsigned int') -> "spot::twa_graph_state const *":
self.report_univ_dest(src)
return $action(self, src)
%}
%feature("shadow") spot::twa_graph::state_acc_sets %{
def state_acc_sets(self, s: 'unsigned int') -> "spot::acc_cond::mark_t":
self.report_univ_dest(src)
return $action(self, src)
%}
%feature("shadow") spot::twa_graph::state_is_accepting %{
def state_is_accepting(self, src) -> "bool":
if type(src) == int:
self.report_univ_dest(src)
return $action(self, src)
%}
%include
%template(twa_graph_state_out) spot::internal::state_out>;
%template(twa_graph_all_trans) spot::internal::all_trans>;
%template(twa_graph_edge_boxed_data) spot::internal::boxed_label;
%template(twa_graph_edge_storage) spot::internal::edge_storage >;
// Should come after the definition of twa_graph
%include
%include
%include
%include
%include
%include
%include
%feature("flatnested") spot::twa_run::step;
%include
%template(list_step) std::list;
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%traits_swigtype(spot::scc_info_node);
%fragment(SWIG_Traits_frag(spot::scc_info_node));
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%template(list_bdd) std::list;
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%include
%extend spot::trival {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
spot::trival __neg__()
{
return !*self;
}
spot::trival __and__(spot::trival other)
{
return *self && other;
}
spot::trival __or__(spot::trival other)
{
return *self || other;
}
}
%extend std::set {
std::string __str__()
{
std::ostringstream s;
s << "{";
bool comma = false;
for (auto& i: *self)
{
if (comma)
s << ", ";
else
comma = true;
spot::print_psl(s, i);
}
s << "}";
return s.str();
}
std::string __repr__()
{
std::ostringstream s;
s << "{";
bool comma = false;
for (auto& i: *self)
{
if (comma)
s << ", ";
else
comma = true;
spot::print_psl(s, i);
}
s << "}";
return s.str();
}
std::string _repr_latex_()
{
std::ostringstream s;
s << "$\\{";
bool comma = false;
for (auto& i: *self)
{
if (comma)
s << ", ";
else
comma = true;
spot::print_sclatex_psl(s, i);
}
s << "\\}$";
return s.str();
}
}
%exception spot::formula::__getitem__ {
try {
$action
}
catch (const std::runtime_error& e)
{
SWIG_exception(SWIG_IndexError, e.what());
}
}
%extend spot::formula {
// __cmp__ is for Python 2.0
int __cmp__(spot::formula b) { return self->id() - b.id(); }
size_t __hash__() { return self->id(); }
unsigned __len__() { return self->size(); }
formula __getitem__(unsigned pos) { return (*self)[pos]; }
std::string __repr__() { return spot::str_psl(*self); }
std::string _repr_latex_()
{
return std::string("$") + spot::str_sclatex_psl(*self) + '$';
}
std::string __str__() { return spot::str_psl(*self); }
}
%extend spot::bdd_dict {
bool operator==(const spot::bdd_dict& b) const
{
return self == &b;
}
bool operator!=(const spot::bdd_dict& b) const
{
return self != &b;
}
}
%extend spot::twa {
void set_name(std::string name)
{
self->set_named_prop("automaton-name", new std::string(name));
}
std::string* get_name()
{
return self->get_named_prop("automaton-name");
}
void set_state_names(std::vector names)
{
self->set_named_prop("state-names",
new std::vector(std::move(names)));
}
std::vector* get_state_names()
{
return self->get_named_prop>("state-names");
}
twa* highlight_state(unsigned state, unsigned color)
{
auto hs =
self->get_named_prop>("highlight-states");
if (!hs)
{
hs = new std::map;
self->set_named_prop("highlight-states", hs);
}
(*hs)[state] = color;
return self;
}
twa* highlight_edge(unsigned edge, unsigned color)
{
auto ht =
self->get_named_prop>("highlight-edges");
if (!ht)
{
ht = new std::map;
self->set_named_prop("highlight-edges", ht);
}
(*ht)[edge] = color;
return self;
}
}
%extend spot::internal::state_out> {
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
{
return swig::make_forward_iterator(self->begin(), self->begin(),
self->end(), *PYTHON_SELF);
}
}
%extend spot::internal::all_trans> {
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
{
return swig::make_forward_iterator(self->begin(), self->begin(),
self->end(), *PYTHON_SELF);
}
}
%extend spot::internal::const_universal_dests {
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
{
return swig::make_forward_iterator_np(self->begin(), self->begin(),
self->end(), *PYTHON_SELF);
}
}
%extend spot::twa_graph {
unsigned new_univ_edge(unsigned src, const std::vector& v,
bdd cond, acc_cond::mark_t acc = 0U)
{
return self->new_univ_edge(src, v.begin(), v.end(), cond, acc);
}
void set_univ_init_state(const std::vector& v)
{
self->set_univ_init_state(v.begin(), v.end());
}
void report_univ_dest(unsigned src)
{
if (self->is_univ_dest(src))
throw std::runtime_error
("universal destinations should be explored with univ_dest()");
}
}
%extend spot::scc_info {
swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
{
return swig::make_forward_iterator(self->begin(), self->begin(),
self->end(), *PYTHON_SELF);
}
}
%extend spot::acc_cond::acc_code {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::acc_cond::mark_t {
// http://comments.gmane.org/gmane.comp.programming.swig/14822
mark_t(const std::vector& f)
{
return new spot::acc_cond::mark_t(f.begin(), f.end());
}
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::acc_cond {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::twa_run {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%extend spot::twa_word {
std::string __repr__()
{
std::ostringstream os;
os << *self;
return os.str();
}
std::string __str__()
{
std::ostringstream os;
os << *self;
return os.str();
}
}
%nodefaultctor std::ostream;
namespace std {
class ostream {};
class ofstream : public ostream
{
public:
ofstream(const char *fn);
~ofstream();
};
class ostringstream : public ostream
{
public:
ostringstream();
std::string str() const;
~ostringstream();
};
}
%inline %{
bool fnode_instances_check()
{
return spot::fnode::instances_check();
}
spot::twa_graph_ptr
ensure_digraph(const spot::twa_ptr& a)
{
auto aa = std::dynamic_pointer_cast(a);
if (aa)
return aa;
return spot::make_twa_graph(a, spot::twa::prop_set::all());
}
std::ostream&
get_cout()
{
return std::cout;
}
void
nl_cout()
{
std::cout << std::endl;
}
std::ostream&
get_cerr()
{
return std::cerr;
}
void
nl_cerr()
{
std::cerr << std::endl;
}
void
print_on(std::ostream& on, const std::string& what)
{
on << what;
}
int
unblock_signal(int signum)
{
sigset_t set;
sigemptyset(&set);
sigaddset(&set, signum);
return sigprocmask(SIG_UNBLOCK, &set, 0);
}
// for alternation.hh
unsigned states_and(const spot::twa_graph_ptr& aut,
const std::vector& il)
{
return states_and(aut, il.begin(), il.end());
}
%}
%extend spot::parse_error_list {
bool
__nonzero__()
{
return !self->empty();
}
bool
__bool__()
{
return !self->empty();
}
}
%extend spot::parse_aut_error_list {
bool
__nonzero__()
{
return !self->empty();
}
bool
__bool__()
{
return !self->empty();
}
}