Commit db1e842a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

ltsmin: add accessors for variable names and types

* spot/ltsmin/ltsmin.hh, spot/ltsmin/ltsmin.cc: Expose more of the
ltsmin interface.
* python/spot/ltsmin.i: Add some helper functions on top of this
new interface.
* tests/python/ltsmin.ipynb: Test them.
* NEWS: Mention it.
parent 907b72fb
......@@ -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:
......
......@@ -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
%}
......@@ -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);
}
}
......@@ -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<const spins_interface> iface) : iface(iface)
{
......
{
"metadata": {
"name": "",
"signature": "sha256:eba4457368b676284d4696dd7afe5596d865c6f9f6f44b5fd5dc7c6585757c89"
"signature": "sha256:f568358fc00acf6332b52560daa1a34f21cb30c73d81197ab7c5c015de11e12e"
},
"nbformat": 3,
"nbformat_minor": 0,
......@@ -70,12 +70,37 @@
"output_type": "pyout",
"prompt_number": 3,
"text": [
"<spot.ltsmin.model; proxy of <Swig Object of type 'spot::ltsmin_model *' at 0x7f6990bd44e0> >"
"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": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
......@@ -331,11 +356,11 @@
"</svg>\n"
],
"text": [
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f6990bd4600> >"
"<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' 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": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
......@@ -401,11 +426,11 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6990bd4c90> >"
"<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' 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": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
......@@ -531,11 +556,11 @@
"</svg>\n"
],
"text": [
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f6990bd49c0> >"
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f54f809d7e0> >"
]
}
],
"prompt_number": 6
"prompt_number": 7
}
],
"metadata": {}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment