gen: pass the bdd_dict to aut_pattern()
* spot/gen/automata.hh (aut_pattern): Add the dict argument. * spot/gen/automata.cc, python/spot/gen.i: Adjust. * tests/python/gen.py: Make sure two automata built without specifying any dictionary share the same one.
This commit is contained in:
parent
11ca2803c9
commit
649793df75
4 changed files with 24 additions and 5 deletions
|
|
@ -30,6 +30,7 @@
|
||||||
%include "std_shared_ptr.i"
|
%include "std_shared_ptr.i"
|
||||||
|
|
||||||
%shared_ptr(spot::twa_graph)
|
%shared_ptr(spot::twa_graph)
|
||||||
|
%shared_ptr(spot::bdd_dict)
|
||||||
|
|
||||||
%{
|
%{
|
||||||
#include <spot/gen/automata.hh>
|
#include <spot/gen/automata.hh>
|
||||||
|
|
@ -40,6 +41,7 @@ using namespace spot;
|
||||||
%import(module="spot.impl") <spot/misc/common.hh>
|
%import(module="spot.impl") <spot/misc/common.hh>
|
||||||
%import(module="spot.impl") <spot/tl/formula.hh>
|
%import(module="spot.impl") <spot/tl/formula.hh>
|
||||||
%import(module="spot.impl") <spot/twa/fwd.hh>
|
%import(module="spot.impl") <spot/twa/fwd.hh>
|
||||||
|
%import(module="spot.impl") <spot/twa/bdddict.hh>
|
||||||
|
|
||||||
%exception {
|
%exception {
|
||||||
try {
|
try {
|
||||||
|
|
@ -86,6 +88,14 @@ def ltl_patterns(*args):
|
||||||
for n in range(min, max + 1):
|
for n in range(min, max + 1):
|
||||||
yield ltl_pattern(pat, n)
|
yield ltl_pattern(pat, n)
|
||||||
|
|
||||||
|
|
||||||
|
# Override aut_pattern now(), because %feature("shadow") does not
|
||||||
|
# seem to work correctly. See https://github.com/swig/swig/issues/980
|
||||||
|
def aut_pattern(pattern: 'spot::gen::aut_pattern_id', n: 'int',
|
||||||
|
dict: 'spot::bdd_dict_ptr' = None) -> "spot::twa_graph_ptr":
|
||||||
|
return _gen.aut_pattern(pattern, n, dict or spot._bdd_dict)
|
||||||
|
|
||||||
|
|
||||||
def aut_patterns(*args):
|
def aut_patterns(*args):
|
||||||
"""
|
"""
|
||||||
Generate automata patterns.
|
Generate automata patterns.
|
||||||
|
|
|
||||||
|
|
@ -28,7 +28,7 @@ namespace spot
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
static twa_graph_ptr
|
static twa_graph_ptr
|
||||||
ks_cobuchi(unsigned n)
|
ks_cobuchi(unsigned n, bdd_dict_ptr dict)
|
||||||
{
|
{
|
||||||
if (n == 0)
|
if (n == 0)
|
||||||
throw std::runtime_error("ks_cobuchi expects a positive argument");
|
throw std::runtime_error("ks_cobuchi expects a positive argument");
|
||||||
|
|
@ -45,7 +45,6 @@ namespace spot
|
||||||
// the automaton has 2n+1 states, numbered from 0 to 2n
|
// the automaton has 2n+1 states, numbered from 0 to 2n
|
||||||
// 0 is the initial state and the only non-deterministic state
|
// 0 is the initial state and the only non-deterministic state
|
||||||
|
|
||||||
auto dict = make_bdd_dict();
|
|
||||||
auto aut = make_twa_graph(dict);
|
auto aut = make_twa_graph(dict);
|
||||||
|
|
||||||
// register aps
|
// register aps
|
||||||
|
|
@ -91,7 +90,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n)
|
twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
|
||||||
{
|
{
|
||||||
if (n < 0)
|
if (n < 0)
|
||||||
{
|
{
|
||||||
|
|
@ -105,7 +104,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
// Keep this alphabetically-ordered!
|
// Keep this alphabetically-ordered!
|
||||||
case AUT_KS_COBUCHI:
|
case AUT_KS_COBUCHI:
|
||||||
return ks_cobuchi(n);
|
return ks_cobuchi(n, dict);
|
||||||
case AUT_END:
|
case AUT_END:
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -21,6 +21,7 @@
|
||||||
|
|
||||||
#include <spot/misc/common.hh>
|
#include <spot/misc/common.hh>
|
||||||
#include <spot/twa/fwd.hh>
|
#include <spot/twa/fwd.hh>
|
||||||
|
#include <spot/twa/bdddict.hh>
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
@ -55,7 +56,13 @@ namespace spot
|
||||||
/// The pattern is specified using one value from the aut_pattern_id
|
/// The pattern is specified using one value from the aut_pattern_id
|
||||||
/// enum. See the man page of the `genaut` binary for a
|
/// enum. See the man page of the `genaut` binary for a
|
||||||
/// description of those patterns, and bibliographic references.
|
/// description of those patterns, and bibliographic references.
|
||||||
SPOT_API twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n);
|
///
|
||||||
|
/// In case you want to combine this automaton with other
|
||||||
|
/// automata, pass the bdd_dict to use to make sure that all share
|
||||||
|
/// the same.
|
||||||
|
SPOT_API twa_graph_ptr
|
||||||
|
aut_pattern(aut_pattern_id pattern, int n,
|
||||||
|
spot::bdd_dict_ptr dict = make_bdd_dict());
|
||||||
|
|
||||||
/// \brief convert an aut_pattern_it value into a name
|
/// \brief convert an aut_pattern_it value into a name
|
||||||
///
|
///
|
||||||
|
|
|
||||||
|
|
@ -31,6 +31,9 @@ assert k2.num_states() == 5
|
||||||
# the type returned by spot.gen.ks_cobuchi() is the correct one.
|
# the type returned by spot.gen.ks_cobuchi() is the correct one.
|
||||||
assert 'to_str' in dir(k2)
|
assert 'to_str' in dir(k2)
|
||||||
|
|
||||||
|
k3 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 3)
|
||||||
|
assert k2.get_dict() == k3.get_dict()
|
||||||
|
|
||||||
try:
|
try:
|
||||||
gen.aut_pattern(gen.AUT_KS_COBUCHI, 0)
|
gen.aut_pattern(gen.AUT_KS_COBUCHI, 0)
|
||||||
except RuntimeError as e:
|
except RuntimeError as e:
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue