diff --git a/python/spot/impl.i b/python/spot/impl.i index a279d5d96..2a1db01ff 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -495,6 +495,60 @@ namespace std { } } +%extend std::set { + 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__ { try { $action diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index 03e490de2..1483df950 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -57,10 +57,6 @@ using namespace spot; } } -namespace std { - %template(atomic_prop_set) set; -} - %rename(model) spot::ltsmin_model; %rename(kripke_raw) spot::ltsmin_model::kripke; %include diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb index 069a0c5e1..c8e84e95c 100644 --- a/tests/python/ltsmin.ipynb +++ b/tests/python/ltsmin.ipynb @@ -18,7 +18,7 @@ "version": "3.5.1" }, "name": "", - "signature": "sha256:d1444ee3c1e56aaa453ac171d129f0ba4486e1e194debc51965d45429a844334" + "signature": "sha256:c71f218a80ffc2fb08377daa20d703d7c421278e48d625c4f9fca8ff8f59d80a" }, "nbformat": 3, "nbformat_minor": 0, @@ -447,7 +447,7 @@ "\n" ], "text": [ - " *' at 0x7f7b280d08a0> >" + " *' at 0x7f1de22e1870> >" ] } ], @@ -726,7 +726,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1082,7 +1082,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1152,7 +1152,7 @@ "\n" ], "text": [ - " *' at 0x7f7b2fcf8090> >" + " *' at 0x7f1dd5f6a630> >" ] } ], @@ -1314,12 +1314,92 @@ "\n" ], "text": [ - " *' at 0x7f7b280d08d0> >" + " *' at 0x7f1de22e17e0> >" ] } ], "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", "collapsed": false, @@ -1333,7 +1413,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 14 + "prompt_number": 15 }, { "cell_type": "code", @@ -1347,13 +1427,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 15, + "prompt_number": 16, "text": [ "False" ] } ], - "prompt_number": 15 + "prompt_number": 16 } ], "metadata": {}