Commit 11ca2803 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

gen: hide ks_cobuchi(), introduce aut_pattern()

* spot/gen/automata.hh, spot/gen/automata.cc: Hide ks_cobuchi() behind
introduce aut_pattern(), as we have already done for the formulas.
* bin/genaut.cc: Simplify using this interface.
* python/spot/gen.i: Introduce aut_patterns().
* tests/python/gen.ipynb, tests/python/gen.py: Adjust.
parent ca7f72bb
......@@ -43,28 +43,14 @@
using namespace spot;
const char argp_program_doc[] ="\
Generate omega automata from predefined patterns.";
enum {
FIRST_CLASS = 256,
OPT_KS_COBUCHI = FIRST_CLASS,
LAST_CLASS,
};
const char* const class_name[LAST_CLASS - FIRST_CLASS] =
{
"ks-cobuchi",
};
#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
const char argp_program_doc[] ="Generate ω-automata from predefined patterns.";
static const argp_option options[] =
{
/**************************************************/
// Keep this alphabetically sorted (expect for aliases).
{ nullptr, 0, nullptr, 0, "Pattern selection:", 1},
{ "ks-cobuchi", OPT_KS_COBUCHI, "RANGE", 0,
{ "ks-cobuchi", gen::AUT_KS_COBUCHI, "RANGE", 0,
"A co-Büchi automaton with 2N+1 states for which any equivalent "
"deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0},
RANGE_DOC,
......@@ -75,7 +61,7 @@ static const argp_option options[] =
struct job
{
int pattern;
gen::aut_pattern_id pattern;
struct range range;
};
......@@ -94,7 +80,7 @@ static void
enqueue_job(int pattern, const char* range_str)
{
job j;
j.pattern = pattern;
j.pattern = static_cast<gen::aut_pattern_id>(pattern);
j.range = parse_range(range_str);
jobs.push_back(j);
}
......@@ -102,35 +88,23 @@ enqueue_job(int pattern, const char* range_str)
static int
parse_opt(int key, char* arg, struct argp_state*)
{
// This switch is alphabetically-ordered.
switch (key)
if (key >= gen::AUT_BEGIN && key < gen::AUT_END)
{
case OPT_KS_COBUCHI:
enqueue_job(key, arg);
break;
default:
return ARGP_ERR_UNKNOWN;
return 0;
}
return 0;
return ARGP_ERR_UNKNOWN;
}
static void
output_pattern(int pattern, int n)
output_pattern(gen::aut_pattern_id pattern, int n)
{
twa_graph_ptr aut = nullptr;
switch (pattern)
{
// Keep this alphabetically-ordered!
case OPT_KS_COBUCHI:
aut = spot::gen::ks_cobuchi(n);
break;
default:
error(100, 0, "internal error: pattern not implemented");
}
process_timer timer;
timer.start();
twa_graph_ptr aut = spot::gen::aut_pattern(pattern, n);
timer.stop();
automaton_printer printer;
printer.print(aut, timer, nullptr, class_name[pattern - FIRST_CLASS], n);
printer.print(aut, timer, nullptr, aut_pattern_name(pattern), n);
}
static void
......
......@@ -85,4 +85,32 @@ def ltl_patterns(*args):
raise RuntimeError("invalid pattern specification")
for n in range(min, max + 1):
yield ltl_pattern(pat, n)
def aut_patterns(*args):
"""
Generate automata patterns.
The arguments should be have one of these three forms:
- (id, n)
- (id, min, max)
- id
In the first case, the pattern id=n is generated. In the second
case, all pattern id=n for min<=n<=max are generated. The
third case is a shorthand for (id, 1, 10).
"""
for spec in args:
if type(spec) is int:
pat = spec
min = 1
max = 10
else:
ls = len(spec)
if ls == 2:
pat, min, max = spec[0], spec[1], spec[1]
elif ls == 3:
pat, min, max = spec
else:
raise RuntimeError("invalid pattern specification")
for n in range(min, max + 1):
yield aut_pattern(pat, n)
%}
......@@ -17,75 +17,114 @@
// 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/twa/twagraph.hh>
#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)
namespace
{
if (n == 0)
throw std::runtime_error("ks_cobuchi() expects a positive argument");
// 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
static twa_graph_ptr
ks_cobuchi(unsigned n)
{
if (n == 0)
throw std::runtime_error("ks_cobuchi expects a positive argument");
// 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
bdd a = bdd_ithvar(aut->register_ap("a"));
bdd b = bdd_ithvar(aut->register_ap("b"));
// the automaton has 2n+1 states, numbered from 0 to 2n
// 0 is the initial state and the only non-deterministic state
// name the four letters
bdd i = a & b;
bdd s = a & (!b);
bdd p = (!a) & b;
bdd h = (!a) & (!b);
auto dict = make_bdd_dict();
auto aut = make_twa_graph(dict);
// actually build the automaton
aut->new_states(2*n+1);
aut->set_init_state(0);
aut->set_acceptance(1, acc_cond::acc_code::cobuchi());
// register aps
aut->register_ap("a");
aut->register_ap("b");
// 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);
// 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);
aut->merge_edges();
aut->prop_state_acc(true);
return 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());
twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n)
{
if (n < 0)
{
std::ostringstream err;
err << "pattern argument for " << aut_pattern_name(pattern)
<< " should be positive";
throw std::runtime_error(err.str());
}
// 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);
switch (pattern)
{
// Keep this alphabetically-ordered!
case AUT_KS_COBUCHI:
return ks_cobuchi(n);
case AUT_END:
break;
}
throw std::runtime_error("unsupported pattern");
}
aut->merge_edges();
aut->prop_state_acc(true);
return aut;
const char* aut_pattern_name(aut_pattern_id pattern)
{
static const char* const class_name[] =
{
"ks-cobuchi",
};
// Make sure we do not forget to update the above table every
// time a new pattern is added.
static_assert(sizeof(class_name)/sizeof(*class_name)
== AUT_END - AUT_BEGIN, "size mismatch");
if (pattern < AUT_BEGIN || pattern >= AUT_END)
throw std::runtime_error("unsupported pattern");
return class_name[pattern - AUT_BEGIN];
}
}
}
......@@ -19,31 +19,48 @@
#pragma once
#include <spot/twa/twagraph.hh>
#include <spot/misc/common.hh>
#include <spot/twa/fwd.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:
enum aut_pattern_id {
AUT_BEGIN = 256,
/// \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}
/// }
///
/// Only defined for n>0
AUT_KS_COBUCHI = AUT_BEGIN,
AUT_END
};
/// \brief generate an automaton from a known pattern
///
/// @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}
/// }
/// The pattern is specified using one value from the aut_pattern_id
/// enum. See the man page of the `genaut` binary for a
/// description of those patterns, and bibliographic references.
SPOT_API twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n);
/// \brief convert an aut_pattern_it value into a name
///
/// \pre n>0
SPOT_API twa_graph_ptr
ks_cobuchi(unsigned n);
/// The returned name is suitable to be used as an option
/// key for the genaut binary.
SPOT_API const char* aut_pattern_name(aut_pattern_id pattern);
}
}
......@@ -45,7 +45,7 @@
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 13
"prompt_number": 1
},
{
"cell_type": "markdown",
......@@ -71,13 +71,13 @@
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 14,
"prompt_number": 2,
"text": [
"GFp1 & GFp2 & GFp3"
]
}
],
"prompt_number": 14
"prompt_number": 2
},
{
"cell_type": "code",
......@@ -94,13 +94,13 @@
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 15,
"prompt_number": 3,
"text": [
"F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)"
]
}
],
"prompt_number": 15
"prompt_number": 3
},
{
"cell_type": "markdown",
......@@ -289,7 +289,7 @@
]
}
],
"prompt_number": 20
"prompt_number": 4
},
{
"cell_type": "markdown",
......@@ -304,7 +304,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"sg.ks_cobuchi(3).show('.a')"
"sg.aut_pattern(sg.AUT_KS_COBUCHI, 3).show('.a')"
],
"language": "python",
"metadata": {},
......@@ -312,7 +312,7 @@
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 23,
"prompt_number": 5,
"svg": [
"<svg height=\"295pt\" viewBox=\"0.00 0.00 734.00 295.41\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.906173 0.906173) rotate(0) translate(4 322)\">\n",
......@@ -491,7 +491,43 @@
]
}
],
"prompt_number": 23
"prompt_number": 5
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Multiple automata can be generated using the `aut_patterns()` function, which works similarly to `ltl_patterns()`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"for aut in sg.aut_patterns(sg.AUT_KS_COBUCHI):\n",
" print(aut.num_states())"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"3\n",
"5\n",
"7\n",
"9\n",
"11\n",
"13\n",
"15\n",
"17\n",
"19\n",
"21\n"
]
}
],
"prompt_number": 6
},
{
"cell_type": "code",
......
......@@ -24,7 +24,7 @@
import spot.gen as gen
from sys import exit
k2 = gen.ks_cobuchi(2)
k2 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 2)
assert k2.prop_state_acc()
assert k2.num_states() == 5
# to_str is defined in the spot package, so this makes sure
......@@ -32,7 +32,7 @@ assert k2.num_states() == 5
assert 'to_str' in dir(k2)
try:
gen.ks_cobuchi(0)
gen.aut_pattern(gen.AUT_KS_COBUCHI, 0)
except RuntimeError as e:
assert 'positive argument' in str(e)
else:
......
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