diff --git a/NEWS b/NEWS index cfef10722..70b7a369d 100644 --- a/NEWS +++ b/NEWS @@ -8,7 +8,9 @@ New in spot 1.99.7a (not yet released) * The load_ltsmin() function has been split in two. Now you should first call ltsmin_model::load(filename) to create an ltlmin_model, and then call the ltsmin_model::kripke(...) method to create an - automaton that can be iterated on the fly. + automaton that can be iterated on the fly. The intermediate + object can be queried about the supported variables and their + types. Python: diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index 9dfb22e78..5b33b525b 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -71,12 +71,39 @@ import spot def load(filename): return model.load(filename) -def _kripke(self, ap_set, dict=spot._bdd_dict, - dead=spot.formula_ap('dead'), - compress=2): - s = spot.atomic_prop_set() - for ap in ap_set: - s.insert(spot.formula_ap(ap)) - return self.kripke_raw(s, dict, dead, compress) -model.kripke = _kripke +@spot._extend(model) +class model: + def kripke(self, ap_set, dict=spot._bdd_dict, + dead=spot.formula_ap('dead'), + compress=2): + s = spot.atomic_prop_set() + for ap in ap_set: + s.insert(spot.formula_ap(ap)) + return self.kripke_raw(s, dict, dead, compress) + + def info(self): + res = {} + ss = self.state_size() + res['state_size'] = ss + res['variables'] = [(self.state_variable_name(i), + self.state_variable_type(i)) for i in range(ss)] + tc = self.type_count() + res['types'] = [(self.type_name(i), + [self.type_value_name(i, j) + for j in range(self.type_value_count(i))]) + for i in range(tc)] + return res + + def __repr__(self): + res = "ltsmin model with the following variables:\n"; + info = self.info() + for (var, t) in info['variables']: + res += ' ' + var + ': '; + type, vals = info['types'][t] + if vals: + res += str(vals) + else: + res += type + res += '\n'; + return res %} diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 4922e8947..d12da45a5 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1122,4 +1122,41 @@ namespace spot ltsmin_model::~ltsmin_model() { } + + + int ltsmin_model::state_size() const + { + return iface->get_state_size(); + } + + const char* ltsmin_model::state_variable_name(int var) const + { + return iface->get_state_variable_name(var); + } + + int ltsmin_model::state_variable_type(int var) const + { + return iface->get_state_variable_type(var); + } + + int ltsmin_model::type_count() const + { + return iface->get_type_count(); + } + + const char* ltsmin_model::type_name(int type) const + { + return iface->get_type_name(type); + } + + int ltsmin_model::type_value_count(int type) + { + return iface->get_type_value_count(type); + } + + const char* ltsmin_model::type_value_name(int type, int val) + { + return iface->get_type_value_name(type, val); + } + } diff --git a/spot/ltsmin/ltsmin.hh b/spot/ltsmin/ltsmin.hh index c45f8a133..fc9a6df3b 100644 --- a/spot/ltsmin/ltsmin.hh +++ b/spot/ltsmin/ltsmin.hh @@ -70,6 +70,22 @@ namespace spot bdd_dict_ptr dict, formula dead = formula::tt(), int compress = 0) const; + + /// Number of variables in a state + int state_size() const; + /// Name of each variable + const char* state_variable_name(int var) const; + /// Type of each variable + int state_variable_type(int var) const; + /// Number of different types + int type_count() const; + /// Name of each type + const char* type_name(int type) const; + /// Count of enumerated values for a type + int type_value_count(int type); + /// Name of each enumerated value for a type + const char* type_value_name(int type, int val); + private: ltsmin_model(std::shared_ptr iface) : iface(iface) { diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb index a39f9c40e..ae61fb603 100644 --- a/tests/python/ltsmin.ipynb +++ b/tests/python/ltsmin.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:eba4457368b676284d4696dd7afe5596d865c6f9f6f44b5fd5dc7c6585757c89" + "signature": "sha256:f568358fc00acf6332b52560daa1a34f21cb30c73d81197ab7c5c015de11e12e" }, "nbformat": 3, "nbformat_minor": 0, @@ -70,12 +70,37 @@ "output_type": "pyout", "prompt_number": 3, "text": [ - " >" + "ltsmin model with the following variables:\n", + " P: ['x']\n", + " P.a: int\n", + " P.b: int" ] } ], "prompt_number": 3 }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "m.info()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "text": [ + "{'state_size': 3,\n", + " 'types': [('P', ['x']), ('int', [])],\n", + " 'variables': [('P', 0), ('P.a', 1), ('P.b', 1)]}" + ] + } + ], + "prompt_number": 4 + }, { "cell_type": "code", "collapsed": false, @@ -89,7 +114,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 4, + "prompt_number": 5, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7f6990bd4600> >" + " *' at 0x7f54f809d9c0> >" ] } ], - "prompt_number": 4 + "prompt_number": 5 }, { "cell_type": "code", @@ -349,7 +374,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 5, + "prompt_number": 6, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7f6990bd4c90> >" + " *' at 0x7f54f809dde0> >" ] } ], - "prompt_number": 5 + "prompt_number": 6 }, { "cell_type": "code", @@ -419,7 +444,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 6, + "prompt_number": 7, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7f6990bd49c0> >" + " *' at 0x7f54f809d7e0> >" ] } ], - "prompt_number": 6 + "prompt_number": 7 } ], "metadata": {}