acc: parse standard acceptance names
* src/twa/acc.cc, src/twa/acc.hh: Add method to create standard acceptance conditions, and adjust the parse_acc_code to recognize them * wrap/python/spot_impl.i (acc_cond::acc_code): Add a printer. * wrap/python/tests/accparse.ipynb: New test file. * wrap/python/tests/Makefile.am: Add it. * src/tests/satmin2.test: Use the new syntax.
This commit is contained in:
Alexandre Duret-Lutz
parent
7880b25aae
commit
8e1c846984
6 changed files with 306 additions and 7 deletions
|
|
@ -165,11 +165,11 @@ State: 0
|
|||
--END--
|
||||
EOF
|
||||
|
||||
$autfilt --sat-minimize='acc="Inf(0)|Fin(1)",max-states=2' foo.hoa \
|
||||
$autfilt --sat-minimize='acc="Streett 1",max-states=2' foo.hoa \
|
||||
--stats=%s >out
|
||||
test "`cat out`" = 1
|
||||
|
||||
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)",max-states=4' foo.hoa \
|
||||
$autfilt --sat-minimize='acc="Rabin 1",max-states=4' foo.hoa \
|
||||
--stats=%s >out && exit 1
|
||||
test -z "`cat out`"
|
||||
|
||||
|
|
|
|||
|
|
@ -1012,8 +1012,6 @@ namespace spot
|
|||
|
||||
static unsigned parse_num(const char*& input)
|
||||
{
|
||||
skip_space(input);
|
||||
expect(input, '(');
|
||||
|
||||
errno = 0;
|
||||
char* end;
|
||||
|
|
@ -1027,6 +1025,14 @@ namespace spot
|
|||
}
|
||||
input = end;
|
||||
|
||||
return num;
|
||||
}
|
||||
|
||||
static unsigned parse_par_num(const char*& input)
|
||||
{
|
||||
skip_space(input);
|
||||
expect(input, '(');
|
||||
unsigned num = parse_num(input);
|
||||
skip_space(input);
|
||||
expect(input, ')');
|
||||
return num;
|
||||
|
|
@ -1056,12 +1062,12 @@ namespace spot
|
|||
else if (!strncmp(input, "Inf", 3))
|
||||
{
|
||||
input += 3;
|
||||
res = acc_cond::acc_code::inf({parse_num(input)});
|
||||
res = acc_cond::acc_code::inf({parse_par_num(input)});
|
||||
}
|
||||
else if (!strncmp(input, "Fin", 3))
|
||||
{
|
||||
input += 3;
|
||||
res = acc_cond::acc_code::fin({parse_num(input)});
|
||||
res = acc_cond::acc_code::fin({parse_par_num(input)});
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -1088,7 +1094,65 @@ namespace spot
|
|||
acc_cond::acc_code parse_acc_code(const char* input)
|
||||
{
|
||||
skip_space(input);
|
||||
acc_cond::acc_code c = parse_acc(input);
|
||||
acc_cond::acc_code c;
|
||||
if (!strncmp(input, "all", 3))
|
||||
{
|
||||
input += 3;
|
||||
c = acc_cond::acc_code::t();
|
||||
}
|
||||
else if (!strncmp(input, "none", 4))
|
||||
{
|
||||
input += 4;
|
||||
c = acc_cond::acc_code::f();
|
||||
}
|
||||
else if (!strncmp(input, "Buchi", 5))
|
||||
{
|
||||
input += 5;
|
||||
c = acc_cond::acc_code::buchi();
|
||||
}
|
||||
else if (!strncmp(input, "co-Buchi", 8))
|
||||
{
|
||||
input += 8;
|
||||
c = acc_cond::acc_code::cobuchi();
|
||||
}
|
||||
else if (!strncmp(input, "generalized-Buchi", 17))
|
||||
{
|
||||
input += 17;
|
||||
c = acc_cond::acc_code::generalized_buchi(parse_num(input));
|
||||
}
|
||||
else if (!strncmp(input, "generalized-co-Buchi", 20))
|
||||
{
|
||||
input += 20;
|
||||
c = acc_cond::acc_code::generalized_buchi(parse_num(input));
|
||||
}
|
||||
else if (!strncmp(input, "Rabin", 5))
|
||||
{
|
||||
input += 5;
|
||||
c = acc_cond::acc_code::rabin(parse_num(input));
|
||||
}
|
||||
else if (!strncmp(input, "Streett", 7))
|
||||
{
|
||||
input += 7;
|
||||
c = acc_cond::acc_code::streett(parse_num(input));
|
||||
}
|
||||
else if (!strncmp(input, "generalized-Rabin", 17))
|
||||
{
|
||||
input += 17;
|
||||
unsigned num = parse_num(input);
|
||||
std::vector<unsigned> v;
|
||||
v.reserve(num);
|
||||
while (num > 0)
|
||||
{
|
||||
v.push_back(parse_num(input));
|
||||
--num;
|
||||
}
|
||||
c = acc_cond::acc_code::generalized_rabin(v.begin(), v.end());
|
||||
}
|
||||
else
|
||||
{
|
||||
c = parse_acc(input);
|
||||
}
|
||||
skip_space(input);
|
||||
if (*input)
|
||||
{
|
||||
std::ostringstream s;
|
||||
|
|
|
|||
|
|
@ -451,6 +451,74 @@ namespace spot
|
|||
return inf_neg(mark_t(vals));
|
||||
}
|
||||
|
||||
static acc_code buchi()
|
||||
{
|
||||
return inf({0});
|
||||
}
|
||||
|
||||
static acc_code cobuchi()
|
||||
{
|
||||
return fin({0});
|
||||
}
|
||||
|
||||
static acc_code generalized_buchi(unsigned n)
|
||||
{
|
||||
acc_cond::mark_t m = (1U << n) - 1;
|
||||
return inf(m);
|
||||
}
|
||||
|
||||
static acc_code generalized_co_buchi(unsigned n)
|
||||
{
|
||||
acc_cond::mark_t m = (1U << n) - 1;
|
||||
return fin(m);
|
||||
}
|
||||
|
||||
// n is a number of pairs.
|
||||
static acc_code rabin(unsigned n)
|
||||
{
|
||||
acc_cond::acc_code res = f();
|
||||
while (n > 0)
|
||||
{
|
||||
acc_cond::acc_code pair = inf({2*n - 1});
|
||||
pair.append_and(fin({2*n - 2}));
|
||||
res.append_or(std::move(pair));
|
||||
--n;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
// n is a number of pairs.
|
||||
static acc_code streett(unsigned n)
|
||||
{
|
||||
acc_cond::acc_code res = t();
|
||||
while (n > 0)
|
||||
{
|
||||
acc_cond::acc_code pair = inf({2*n - 1});
|
||||
pair.append_or(fin({2*n - 2}));
|
||||
res.append_and(std::move(pair));
|
||||
--n;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
template<class iterator>
|
||||
static acc_code generalized_rabin(iterator begin, iterator end)
|
||||
{
|
||||
acc_cond::acc_code res = f();
|
||||
unsigned n = 0;
|
||||
for (iterator i = begin; i != end; ++i)
|
||||
{
|
||||
acc_cond::acc_code pair = fin({n++});
|
||||
acc_cond::mark_t m = 0U;
|
||||
for (unsigned ni = *i; ni > 0; --ni)
|
||||
m.set({n++});
|
||||
pair.append_and(inf(m));
|
||||
std::swap(pair, res);
|
||||
res.append_or(std::move(pair));
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
void append_and(acc_code&& r)
|
||||
{
|
||||
if (is_true() || r.is_false())
|
||||
|
|
|
|||
|
|
@ -344,6 +344,22 @@ spot::ltl::formula_ptr_less_than>;
|
|||
std::string __str__() { return spot::ltl::to_string(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();
|
||||
}
|
||||
}
|
||||
|
||||
%nodefaultctor std::ostream;
|
||||
namespace std {
|
||||
class ostream {};
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@ LOG_DRIVER = $(TEST_LOG_DRIVER)
|
|||
check_SCRIPTS = run
|
||||
|
||||
TESTS = \
|
||||
accparse.ipynb \
|
||||
alarm.py \
|
||||
automata.ipynb \
|
||||
automata-io.ipynb \
|
||||
|
|
|
|||
150
wrap/python/tests/accparse.ipynb
Normal file
150
wrap/python/tests/accparse.ipynb
Normal file
|
|
@ -0,0 +1,150 @@
|
|||
{
|
||||
"metadata": {
|
||||
"kernelspec": {
|
||||
"display_name": "Python 3",
|
||||
"language": "python",
|
||||
"name": "python3"
|
||||
},
|
||||
"language_info": {
|
||||
"codemirror_mode": {
|
||||
"name": "ipython",
|
||||
"version": 3
|
||||
},
|
||||
"file_extension": ".py",
|
||||
"mimetype": "text/x-python",
|
||||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.4.3+"
|
||||
},
|
||||
"name": ""
|
||||
},
|
||||
"nbformat": 3,
|
||||
"nbformat_minor": 0,
|
||||
"worksheets": [
|
||||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": true,
|
||||
"input": [
|
||||
"import spot\n",
|
||||
"spot.setup()"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"prompt_number": 1
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"c = spot.parse_acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"metadata": {},
|
||||
"output_type": "pyout",
|
||||
"prompt_number": 2,
|
||||
"text": [
|
||||
"(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 2
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"c.to_dnf()"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"metadata": {},
|
||||
"output_type": "pyout",
|
||||
"prompt_number": 3,
|
||||
"text": [
|
||||
"(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 3
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"c.to_cnf()"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"metadata": {},
|
||||
"output_type": "pyout",
|
||||
"prompt_number": 4,
|
||||
"text": [
|
||||
"(Inf(0) | Inf(2)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (Fin(1)|Fin(3))"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 4
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": false,
|
||||
"input": [
|
||||
"for acc in ['all', 't', \n",
|
||||
" 'Buchi', 'generalized-Buchi 3', 'generalized-Buchi 0',\n",
|
||||
" 'co-Buchi', 'generalized-co-Buchi 3', 'generalized-co-Buchi 0',\n",
|
||||
" 'Rabin 2', 'Rabin 0',\n",
|
||||
" 'Streett 2', 'Streett 0',\n",
|
||||
" 'generalized-Rabin 3 1 2 3', 'generalized-Rabin 0']:\n",
|
||||
" print(acc, ': ', spot.parse_acc_code(acc), sep='')"
|
||||
],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"output_type": "stream",
|
||||
"stream": "stdout",
|
||||
"text": [
|
||||
"all: t\n",
|
||||
"t: t\n",
|
||||
"Buchi: Inf(0)\n",
|
||||
"generalized-Buchi 3: Inf(0)&Inf(1)&Inf(2)\n",
|
||||
"generalized-Buchi 0: t\n",
|
||||
"co-Buchi: Fin(0)\n",
|
||||
"generalized-co-Buchi 3: Inf(0)&Inf(1)&Inf(2)\n",
|
||||
"generalized-co-Buchi 0: t\n",
|
||||
"Rabin 2: (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
|
||||
"Rabin 0: f\n",
|
||||
"Streett 2: (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n",
|
||||
"Streett 0: t\n",
|
||||
"generalized-Rabin 3 1 2 3: (Fin(0) & Inf(1)) | (Fin(2) & (Inf(3)&Inf(4))) | (Fin(5) & (Inf(6)&Inf(7)&Inf(8)))\n",
|
||||
"generalized-Rabin 0: f\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"prompt_number": 5
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"collapsed": true,
|
||||
"input": [],
|
||||
"language": "python",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"prompt_number": null
|
||||
}
|
||||
],
|
||||
"metadata": {}
|
||||
}
|
||||
]
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue