python: add prints for atomic_prop_set
Fixes #159. * python/spot/ltsmin.i: Here. * python/spot/impl.i: Disable duplicate instantiation. * tests/python/ltsmin.ipynb: Test it.
This commit is contained in:
parent
e429e2f056
commit
901f287032
3 changed files with 143 additions and 13 deletions
|
|
@ -495,6 +495,60 @@ namespace std {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
%extend std::set<spot::formula> {
|
||||||
|
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__ {
|
%exception spot::formula::__getitem__ {
|
||||||
try {
|
try {
|
||||||
$action
|
$action
|
||||||
|
|
|
||||||
|
|
@ -57,10 +57,6 @@ using namespace spot;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
namespace std {
|
|
||||||
%template(atomic_prop_set) set<spot::formula>;
|
|
||||||
}
|
|
||||||
|
|
||||||
%rename(model) spot::ltsmin_model;
|
%rename(model) spot::ltsmin_model;
|
||||||
%rename(kripke_raw) spot::ltsmin_model::kripke;
|
%rename(kripke_raw) spot::ltsmin_model::kripke;
|
||||||
%include <spot/ltsmin/ltsmin.hh>
|
%include <spot/ltsmin/ltsmin.hh>
|
||||||
|
|
|
||||||
|
|
@ -18,7 +18,7 @@
|
||||||
"version": "3.5.1"
|
"version": "3.5.1"
|
||||||
},
|
},
|
||||||
"name": "",
|
"name": "",
|
||||||
"signature": "sha256:d1444ee3c1e56aaa453ac171d129f0ba4486e1e194debc51965d45429a844334"
|
"signature": "sha256:c71f218a80ffc2fb08377daa20d703d7c421278e48d625c4f9fca8ff8f59d80a"
|
||||||
},
|
},
|
||||||
"nbformat": 3,
|
"nbformat": 3,
|
||||||
"nbformat_minor": 0,
|
"nbformat_minor": 0,
|
||||||
|
|
@ -447,7 +447,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f7b280d08a0> >"
|
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f1de22e1870> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -726,7 +726,7 @@
|
||||||
"</svg>"
|
"</svg>"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<IPython.core.display.SVG at 0x7f7b280dd630>"
|
"<IPython.core.display.SVG at 0x7f1de228ae80>"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -1082,7 +1082,7 @@
|
||||||
"</svg>"
|
"</svg>"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<IPython.core.display.SVG at 0x7f7b110b9c50>"
|
"<IPython.core.display.SVG at 0x7f1de228ab38>"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -1152,7 +1152,7 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7b2fcf8090> >"
|
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1dd5f6a630> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
|
|
@ -1314,12 +1314,92 @@
|
||||||
"</svg>\n"
|
"</svg>\n"
|
||||||
],
|
],
|
||||||
"text": [
|
"text": [
|
||||||
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f7b280d08d0> >"
|
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f1de22e17e0> >"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 13
|
"prompt_number": 13
|
||||||
},
|
},
|
||||||
|
{
|
||||||
|
"cell_type": "markdown",
|
||||||
|
"metadata": {},
|
||||||
|
"source": [
|
||||||
|
"If we want to create a `model_check` function that takes a model and formula, we need to get the list of atomic propositions used in the formula using `atomic_prop_collect()`. This returns an `atomic_prop_set`:"
|
||||||
|
]
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"cell_type": "code",
|
||||||
|
"collapsed": false,
|
||||||
|
"input": [
|
||||||
|
"a = spot.atomic_prop_collect(spot.formula('\"a < 2\" W \"b == 1\"'))\n",
|
||||||
|
"dir(a)"
|
||||||
|
],
|
||||||
|
"language": "python",
|
||||||
|
"metadata": {},
|
||||||
|
"outputs": [
|
||||||
|
{
|
||||||
|
"metadata": {},
|
||||||
|
"output_type": "pyout",
|
||||||
|
"prompt_number": 17,
|
||||||
|
"text": [
|
||||||
|
"['__bool__',\n",
|
||||||
|
" '__class__',\n",
|
||||||
|
" '__contains__',\n",
|
||||||
|
" '__delattr__',\n",
|
||||||
|
" '__dict__',\n",
|
||||||
|
" '__dir__',\n",
|
||||||
|
" '__doc__',\n",
|
||||||
|
" '__eq__',\n",
|
||||||
|
" '__format__',\n",
|
||||||
|
" '__ge__',\n",
|
||||||
|
" '__getattribute__',\n",
|
||||||
|
" '__getitem__',\n",
|
||||||
|
" '__gt__',\n",
|
||||||
|
" '__hash__',\n",
|
||||||
|
" '__init__',\n",
|
||||||
|
" '__iter__',\n",
|
||||||
|
" '__le__',\n",
|
||||||
|
" '__len__',\n",
|
||||||
|
" '__lt__',\n",
|
||||||
|
" '__module__',\n",
|
||||||
|
" '__ne__',\n",
|
||||||
|
" '__new__',\n",
|
||||||
|
" '__nonzero__',\n",
|
||||||
|
" '__reduce__',\n",
|
||||||
|
" '__reduce_ex__',\n",
|
||||||
|
" '__repr__',\n",
|
||||||
|
" '__setattr__',\n",
|
||||||
|
" '__sizeof__',\n",
|
||||||
|
" '__str__',\n",
|
||||||
|
" '__subclasshook__',\n",
|
||||||
|
" '__swig_destroy__',\n",
|
||||||
|
" '__weakref__',\n",
|
||||||
|
" 'add',\n",
|
||||||
|
" 'append',\n",
|
||||||
|
" 'begin',\n",
|
||||||
|
" 'clear',\n",
|
||||||
|
" 'count',\n",
|
||||||
|
" 'discard',\n",
|
||||||
|
" 'empty',\n",
|
||||||
|
" 'end',\n",
|
||||||
|
" 'equal_range',\n",
|
||||||
|
" 'erase',\n",
|
||||||
|
" 'find',\n",
|
||||||
|
" 'insert',\n",
|
||||||
|
" 'iterator',\n",
|
||||||
|
" 'lower_bound',\n",
|
||||||
|
" 'rbegin',\n",
|
||||||
|
" 'rend',\n",
|
||||||
|
" 'size',\n",
|
||||||
|
" 'swap',\n",
|
||||||
|
" 'this',\n",
|
||||||
|
" 'thisown',\n",
|
||||||
|
" 'upper_bound']"
|
||||||
|
]
|
||||||
|
}
|
||||||
|
],
|
||||||
|
"prompt_number": 17
|
||||||
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "code",
|
"cell_type": "code",
|
||||||
"collapsed": false,
|
"collapsed": false,
|
||||||
|
|
@ -1333,7 +1413,7 @@
|
||||||
"language": "python",
|
"language": "python",
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"outputs": [],
|
"outputs": [],
|
||||||
"prompt_number": 14
|
"prompt_number": 15
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"cell_type": "code",
|
"cell_type": "code",
|
||||||
|
|
@ -1347,13 +1427,13 @@
|
||||||
{
|
{
|
||||||
"metadata": {},
|
"metadata": {},
|
||||||
"output_type": "pyout",
|
"output_type": "pyout",
|
||||||
"prompt_number": 15,
|
"prompt_number": 16,
|
||||||
"text": [
|
"text": [
|
||||||
"False"
|
"False"
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"prompt_number": 15
|
"prompt_number": 16
|
||||||
}
|
}
|
||||||
],
|
],
|
||||||
"metadata": {}
|
"metadata": {}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue