tgba: simplify usage of named properties
* src/tgba/tgba.hh, src/tgba/tgba.cc (set_named_prop): Add a template version. (get_named_prop): Hide the old version, and supply a template version that casts. * src/bin/ltlcross.cc, src/hoaparse/hoaparse.yy, src/tgbaalgos/hoa.cc, src/tgbaalgos/product.cc: Adjust usage.
This commit is contained in:
parent
5a1e38d90f
commit
61edf7f41d
6 changed files with 23 additions and 12 deletions
|
|
@ -1244,8 +1244,7 @@ namespace
|
||||||
state_set& s)
|
state_set& s)
|
||||||
{
|
{
|
||||||
auto aut = m->get_aut();
|
auto aut = m->get_aut();
|
||||||
auto ps = static_cast<const spot::product_states*>
|
auto ps = aut->get_named_prop<const spot::product_states>("product-states");
|
||||||
(aut->get_named_prop("product-states"));
|
|
||||||
unsigned c = m->scc_count();
|
unsigned c = m->scc_count();
|
||||||
for (unsigned n = 0; n < c; ++n)
|
for (unsigned n = 0; n < c; ++n)
|
||||||
if (m->is_accepting_scc(n) || m->is_trivial(n))
|
if (m->is_accepting_scc(n) || m->is_trivial(n))
|
||||||
|
|
|
||||||
|
|
@ -359,9 +359,7 @@ header-item: "States:" INT
|
||||||
}
|
}
|
||||||
| "name:" STRING
|
| "name:" STRING
|
||||||
{
|
{
|
||||||
res.h->aut->set_named_prop("automaton-name", $2, [](void* name) {
|
res.h->aut->set_named_prop("automaton-name", $2);
|
||||||
delete static_cast<std::string*>(name);
|
|
||||||
});
|
|
||||||
}
|
}
|
||||||
| "properties:" properties
|
| "properties:" properties
|
||||||
| HEADERNAME header-spec
|
| HEADERNAME header-spec
|
||||||
|
|
|
||||||
|
|
@ -98,7 +98,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void*
|
void*
|
||||||
tgba::get_named_prop(std::string s) const
|
tgba::get_named_prop_(std::string s) const
|
||||||
{
|
{
|
||||||
auto i = named_prop_.find(s);
|
auto i = named_prop_.find(s);
|
||||||
if (i == named_prop_.end())
|
if (i == named_prop_.end())
|
||||||
|
|
|
||||||
|
|
@ -665,12 +665,28 @@ namespace spot
|
||||||
std::pair<void*,
|
std::pair<void*,
|
||||||
std::function<void(void*)>>> named_prop_;
|
std::function<void(void*)>>> named_prop_;
|
||||||
#endif
|
#endif
|
||||||
|
void* get_named_prop_(std::string s) const;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
|
|
||||||
#ifndef SWIG
|
#ifndef SWIG
|
||||||
void set_named_prop(std::string s,
|
void set_named_prop(std::string s,
|
||||||
void* val, std::function<void(void*)> destructor);
|
void* val, std::function<void(void*)> destructor);
|
||||||
void* get_named_prop(std::string s) const;
|
|
||||||
|
template<typename T>
|
||||||
|
void set_named_prop(std::string s, T* val)
|
||||||
|
{
|
||||||
|
set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
|
||||||
|
}
|
||||||
|
|
||||||
|
template<typename T>
|
||||||
|
T* get_named_prop(std::string s) const
|
||||||
|
{
|
||||||
|
void* p = get_named_prop_(s);
|
||||||
|
if (!p)
|
||||||
|
return nullptr;
|
||||||
|
return static_cast<T*>(p);
|
||||||
|
}
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
bool has_single_acc_set() const
|
bool has_single_acc_set() const
|
||||||
|
|
|
||||||
|
|
@ -250,9 +250,9 @@ namespace spot
|
||||||
|
|
||||||
const char nl = newline ? '\n' : ' ';
|
const char nl = newline ? '\n' : ' ';
|
||||||
os << "HOA: v1" << nl;
|
os << "HOA: v1" << nl;
|
||||||
auto* n = aut->get_named_prop("automaton-name");
|
auto n = aut->get_named_prop<std::string>("automaton-name");
|
||||||
if (n)
|
if (n)
|
||||||
escape_str(os << "name: \"", *static_cast<std::string*>(n)) << '"' << nl;
|
escape_str(os << "name: \"", *n) << '"' << nl;
|
||||||
else if (f)
|
else if (f)
|
||||||
escape_str(os << "name: \"", to_string(f)) << '"' << nl;
|
escape_str(os << "name: \"", to_string(f)) << '"' << nl;
|
||||||
os << "States: " << num_states << nl
|
os << "States: " << num_states << nl
|
||||||
|
|
|
||||||
|
|
@ -56,9 +56,7 @@ namespace spot
|
||||||
+ right->acc().num_sets());
|
+ right->acc().num_sets());
|
||||||
|
|
||||||
auto v = new product_states;
|
auto v = new product_states;
|
||||||
res->set_named_prop("product-states", v, [](void* vv) {
|
res->set_named_prop("product-states", v);
|
||||||
delete static_cast<product_states*>(vv);
|
|
||||||
});
|
|
||||||
|
|
||||||
auto new_state =
|
auto new_state =
|
||||||
[&](unsigned left_state, unsigned right_state) -> unsigned
|
[&](unsigned left_state, unsigned right_state) -> unsigned
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue