alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

acc_code: parse from the constructor

Browse source 
* spot/twa/acc.hh, spot/twa/acc.cc (parse_acc_code): Rename as...
(acc_cond::acc_code): ... this, making it a lot easier to build
acceptance conditions from strings.
* NEWS: Mention the change.
* spot/twaalgos/dtwasat.cc, spot/bin/randaut.cc, spot/tests/acc.cc:
Adjust.
* wrap/python/tests/acc_cond.ipynb, wrap/python/tests/accparse.ipynb,
wrap/python/tests/accparse2.py: Simplify, but not completely to exercise
all variants.
* wrap/python/spot_impl.i: Make acc_code's constructor implicit.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-18 17:47:16 +01:00
parent d0b29051b2
commit df1ef302e8
10 changed files with 189 additions and 133 deletions
Download patch file Download diff file Expand all files Collapse all files

1
wrap/python/spot_impl.i
View file

@ -353,6 +353,7 @@ namespace std {
%include <spot/twa/bddprint.hh>
%include <spot/twa/fwd.hh>
%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};

177
wrap/python/tests/acc_cond.ipynb
View file

@ -18,7 +18,7 @@
"version": "3.4.3+"
},
"name": "",
"signature": "sha256:c447381803e03318b0d23c721f53fa232f91ec81af26a7c09c817463eee5d417"
"signature": "sha256:9abaa081794db5d5479c8c9c179c8518aa52b60abdb4b7a106045646e277d43a"
},
"nbformat": 3,
"nbformat_minor": 0,
@ -473,14 +473,14 @@
"\n",
"`acc_code` encodes the formula of the acceptance condition using a kind of bytecode that basically corresponds to an encoding in [reverse Polish notation](http://en.wikipedia.org/wiki/Reverse_Polish_notation) in which conjunctions of `Inf(n)` terms, and disjunctions of `Fin(n)` terms are grouped. In particular, the frequently-used genaralized-B\u00fcchi acceptance conditions (like `Inf(0)&Inf(1)&Inf(2)`) are always encoded as a single term (like `Inf({0,1,2})`).\n",
"\n",
"The simplest way to construct an `acc_code` is via the `parse_acc_code()` function."
"The simplest way to construct an `acc_code` by passing a string that represent the formula to build."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.parse_acc_code('(Inf(0)&Fin(1))|Inf(2)')"
"spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')"
],
"language": "python",
"metadata": {},
@ -507,7 +507,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"spot.parse_acc_code('Rabin 2')"
"spot.acc_code('Rabin 2')"
],
"language": "python",
"metadata": {},
@ -534,8 +534,8 @@
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_acc_code('Streett 2..4'))\n",
"print(spot.parse_acc_code('Streett 2..4'))"
"print(spot.acc_code('Streett 2..4'))\n",
"print(spot.acc_code('Streett 2..4'))"
],
"language": "python",
"metadata": {},
@ -562,7 +562,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"spot.parse_acc_code('random 3..5')"
"spot.acc_code('random 3..5')"
],
"language": "python",
"metadata": {},
@ -589,7 +589,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.parse_acc_code('parity min odd 5')\n",
"a = spot.acc_code('parity min odd 5')\n",
"a"
],
"language": "python",
@ -660,8 +660,8 @@
"cell_type": "code",
"collapsed": false,
"input": [
"x = spot.parse_acc_code('Rabin 2')\n",
"y = spot.parse_acc_code('Rabin 2') << 4\n",
"x = spot.acc_code('Rabin 2')\n",
"y = spot.acc_code('Rabin 2') << 4\n",
"print(x)\n",
"print(y)"
],
@ -732,7 +732,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"Instead of using `parse_acc_code()`, it is also possible to build a formula from atoms like `Inf({...})`, `Fin({...})`, `t`, or `f`.\n",
"Instead of using `acc_code('string')`, it is also possible to build an acceptance formula from atoms like `Inf({...})`, `Fin({...})`, `t`, or `f`.\n",
"\n",
"Remember that in our encoding for the formula, terms like `Inf(1)&Inf(2)` and `Fin(3)|Fin(4)|Fin(5)` are actually stored as `Inf({1,2})` and `Fin({3,4,5})`, where `{1,2}` and `{3,4,5}` are instance of `mark_t`. These terms can be generated with the\n",
"functions `spot.acc_code.inf(mark)` and `spot.acc_code.fin(mark)`.\n",
@ -851,7 +851,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.parse_acc_code('Fin(0) & Inf(1) | Inf(2)')\n",
"acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n",
"print(\"acc =\", acc)\n",
"for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):\n",
" print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))"
@ -888,7 +888,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.parse_acc_code('Fin(0) & Inf(2)')\n",
"acc = spot.acc_code('Fin(0) & Inf(2)')\n",
"print(acc)\n",
"print(acc.used_sets())\n",
"print(acc.used_sets().max_set())"
@ -926,7 +926,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(4, spot.parse_acc_code('Rabin 2'))\n",
"acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
"acc"
],
"language": "python",
@ -943,6 +943,34 @@
],
"prompt_number": 34
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For convenience, you can pass the string directly:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(4, 'Rabin 2')\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 35,
"text": [
"(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))"
]
}
],
"prompt_number": 35
},
{
"cell_type": "code",
"collapsed": false,
@ -955,13 +983,13 @@
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 35,
"prompt_number": 36,
"text": [
"4"
]
}
],
"prompt_number": 35
"prompt_number": 36
},
{
"cell_type": "code",
@ -975,13 +1003,13 @@
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 36,
"prompt_number": 37,
"text": [
"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))"
]
}
],
"prompt_number": 36
"prompt_number": 37
},
{
"cell_type": "markdown",
@ -1003,13 +1031,13 @@
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 37,
"prompt_number": 38,
"text": [
"(4, t)"
]
}
],
"prompt_number": 37
"prompt_number": 38
},
{
"cell_type": "code",
@ -1020,51 +1048,23 @@
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 38,
"text": [
"(6, t)"
]
}
],
"prompt_number": 38
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc.set_acceptance(spot.parse_acc_code('Streett 2'))\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 39,
"text": [
"(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
"(6, t)"
]
}
],
"prompt_number": 39
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Calling the constructor of `acc_cond` by passing just an instance of `acc_code` will automatically set the number of acceptance sets to the minimum needed by the formula:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(spot.parse_acc_code('Streett 2'))\n",
"acc.set_acceptance('Streett 2')\n",
"acc"
],
"language": "python",
@ -1075,7 +1075,7 @@
"output_type": "pyout",
"prompt_number": 40,
"text": [
"(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
"(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
]
}
],
@ -1085,15 +1085,14 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"The above is in fact just syntactic sugar for:"
"Calling the constructor of `acc_cond` by passing just an instance of `acc_code` (or a string that will be passed to the `acc_code` constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"code = spot.parse_acc_code('Streett 2')\n",
"acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
"acc = spot.acc_cond('Streett 2')\n",
"acc"
],
"language": "python",
@ -1110,6 +1109,35 @@
],
"prompt_number": 41
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The above is in fact just syntactic sugar for:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"code = spot.acc_code('Streett 2')\n",
"acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
"acc"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 42,
"text": [
"(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
]
}
],
"prompt_number": 42
},
{
"cell_type": "markdown",
"metadata": {},
@ -1131,13 +1159,13 @@
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 42,
"prompt_number": 43,
"text": [
"(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))"
]
}
],
"prompt_number": 42
"prompt_number": 43
},
{
"cell_type": "markdown",
@ -1170,7 +1198,7 @@
]
}
],
"prompt_number": 43
"prompt_number": 44
},
{
"cell_type": "markdown",
@ -1185,7 +1213,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(spot.parse_acc_code('Rabin 2'))\n",
"acc = spot.acc_cond('Rabin 2')\n",
"print(acc)\n",
"print(acc.is_rabin())\n",
"print(acc.is_streett())"
@ -1203,7 +1231,7 @@
]
}
],
"prompt_number": 44
"prompt_number": 45
},
{
"cell_type": "markdown",
@ -1216,7 +1244,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(spot.parse_acc_code('parity min odd 4'))\n",
"acc = spot.acc_cond('parity min odd 4')\n",
"print(acc)\n",
"print(acc.is_parity())\n",
"acc.set_generalized_buchi()\n",
@ -1237,7 +1265,7 @@
]
}
],
"prompt_number": 45
"prompt_number": 46
},
{
"cell_type": "markdown",
@ -1266,7 +1294,7 @@
]
}
],
"prompt_number": 46
"prompt_number": 47
},
{
"cell_type": "markdown",
@ -1287,13 +1315,13 @@
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 47,
"prompt_number": 48,
"text": [
"{0,1,2,3}"
]
}
],
"prompt_number": 47
"prompt_number": 48
},
{
"cell_type": "markdown",
@ -1324,7 +1352,7 @@
]
}
],
"prompt_number": 48
"prompt_number": 49
},
{
"cell_type": "markdown",
@ -1354,13 +1382,13 @@
]
}
],
"prompt_number": 49
"prompt_number": 50
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(0)\n",
"acc = spot.acc_cond(0) # use 0 acceptance sets, and the default formula (t)\n",
"print(acc)\n",
"print(acc.unsat_mark())"
],
@ -1376,13 +1404,13 @@
]
}
],
"prompt_number": 50
"prompt_number": 51
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"acc = spot.acc_cond(spot.parse_acc_code('Streett 2'))\n",
"acc = spot.acc_cond('Streett 2')\n",
"print(acc)\n",
"print(acc.unsat_mark())"
],
@ -1398,7 +1426,16 @@
]
}
],
"prompt_number": 51
"prompt_number": 52
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 52
}
],
"metadata": {}

16
wrap/python/tests/accparse.ipynb
View file

@ -17,7 +17,8 @@
"pygments_lexer": "ipython3",
"version": "3.4.3+"
},
"name": ""
"name": "",
"signature": "sha256:1ee7951bed30652ae110a14b210541829221552eb944ff01f25236179673dd5b"
},
"nbformat": 3,
"nbformat_minor": 0,
@ -40,7 +41,7 @@
"cell_type": "code",
"collapsed": false,
"input": [
"c = spot.parse_acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c"
"c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c"
],
"language": "python",
"metadata": {},
@ -112,7 +113,7 @@
" 'parity min even 1', 'parity max odd 1', 'parity max even 1', 'parity min odd 1',\n",
" 'parity min even 0', 'parity max odd 0', 'parity max even 0', 'parity min odd 0',\n",
" ]:\n",
" print(acc, ': ', spot.parse_acc_code(acc), sep='')"
" print(acc, ': ', spot.acc_code(acc), sep='')"
],
"language": "python",
"metadata": {},
@ -159,6 +160,15 @@
}
],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 5
}
],
"metadata": {}

49
wrap/python/tests/accparse2.py
View file

@ -20,79 +20,74 @@
import spot
a = spot.acc_cond(5)
a.set_acceptance(spot.parse_acc_code('parity min odd 5'))
a.set_acceptance(spot.acc_code('parity min odd 5'))
assert(a.is_parity() == [True, False, True])
a.set_acceptance(spot.parse_acc_code('parity max even 5'))
a.set_acceptance('parity max even 5')
assert(a.is_parity() == [True, True, False])
a.set_acceptance(spot.parse_acc_code('generalized-Buchi 5'))
a.set_acceptance('generalized-Buchi 5')
assert(a.is_parity()[0] == False)
assert(a.is_parity(True)[0] == False)
a.set_acceptance(spot.parse_acc_code(
'Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))'))
a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')
assert(a.is_parity()[0] == False)
assert(a.is_parity(True) == [True, True, False])
a = spot.acc_cond(0)
a.set_acceptance(spot.parse_acc_code('all'))
a.set_acceptance('all')
assert(a.is_rabin() == -1)
assert(a.is_streett() == 0)
assert(a.is_parity() == [True, True, True])
a.set_acceptance(spot.parse_acc_code('none'))
a.set_acceptance('none')
assert(a.is_rabin() == 0)
assert(a.is_streett() == -1)
assert(a.is_parity() == [True, True, False])
a = spot.acc_cond(2)
a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))'))
a = spot.acc_cond('(Fin(0)&Inf(1))')
assert(a.is_rabin() == 1)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('Inf(1)&Fin(0)'))
a.set_acceptance('Inf(1)&Fin(0)')
assert(a.is_rabin() == 1)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))'))
a.set_acceptance('(Fin(0)|Inf(1))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == 1)
a.set_acceptance(spot.parse_acc_code('Inf(1)|Fin(0)'))
a.set_acceptance('Inf(1)|Fin(0)')
assert(a.is_rabin() == -1)
assert(a.is_streett() == 1)
a = spot.acc_cond(4)
a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))'))
a = spot.acc_cond('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))')
assert(a.is_rabin() == 2)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))'))
a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))'))
assert(a.is_rabin() == 2)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))'))
a.set_acceptance(spot.acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))'))
assert(a.is_rabin() == -1)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))'))
a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))'))
assert(a.is_rabin() == -1)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))'))
a.set_acceptance(spot.acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))'))
assert(a.is_rabin() == -1)
assert(a.is_streett() == -1)
r = spot.parse_acc_code('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))')
a.set_acceptance(r)
a.set_acceptance('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))')
assert(a.is_rabin() == 2)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))'))
a.set_acceptance('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == 2)
a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))'))
a.set_acceptance('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == 2)
a.set_acceptance(spot.parse_acc_code('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))'))
a.set_acceptance('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))'))
a.set_acceptance('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == -1)
a.set_acceptance(spot.parse_acc_code('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))'))
a.set_acceptance('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == -1)
r = spot.parse_acc_code('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))')
a.set_acceptance(r)
a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))')
assert(a.is_rabin() == -1)
assert(a.is_streett() == 2)