From 7b5879d26a1f535da97fafeecb95b5d6010adae8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 5 Mar 2011 23:08:05 +0100 Subject: [PATCH] Teach the DVE2 interface about enumerated types. * iface/dve2/dve2.cc (convert_aps): Add support for enumerated types. E.g. an atomic proposition such as "P_0.CS" really means "P_0 == CS". --- ChangeLog | 8 ++++ iface/dve2/dve2.cc | 107 ++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 104 insertions(+), 11 deletions(-) diff --git a/ChangeLog b/ChangeLog index 1b7ed98c0..ee08a02e6 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-03-05 Alexandre Duret-Lutz + + Teach the DVE2 interface about enumerated types. + + * iface/dve2/dve2.cc (convert_aps): Add support for + enumerated types. E.g. an atomic proposition such + as "P_0.CS" really means "P_0 == CS". + 2011-03-05 Alexandre Duret-Lutz Teach the DVE2 interface about atomic propositions such as "a <= diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index fe7062bf2..18dbe5643 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -207,6 +207,14 @@ namespace spot }; typedef std::vector prop_set; + + struct var_info + { + int num; + int type; + }; + + int convert_aps(const ltl::atomic_prop_set* aps, const dve2_interface* d, @@ -216,9 +224,28 @@ namespace spot int errors = 0; int state_size = d->get_state_variable_count(); - std::map val_n; + typedef std::map val_map_t; + val_map_t val_map; + for (int i = 0; i < state_size; ++i) - val_n[d->get_state_variable_name(i)] = i; + { + const char* name = d->get_state_variable_name(i); + int type = d->get_state_variable_type(i); + var_info v = { i , type }; + val_map[name] = v; + } + + int type_count = d->get_state_variable_type_count(); + typedef std::map enum_map_t; + std::vector enum_map(type_count); + for (int i = 0; i < type_count; ++i) + { + int enum_count = d->get_state_variable_type_value_count(i); + for (int j = 0; j < enum_count; ++j) + enum_map[i] + .insert(std::make_pair(d->get_state_variable_type_value(i, j), + j)); + } for (ltl::atomic_prop_set::const_iterator ap = aps->begin(); ap != aps->end(); ++ap) @@ -240,12 +267,18 @@ namespace spot char* name = (char*) malloc(str.size() + 1); char* name_p = name; + char* lastdot = 0; while (*s && (*s != '=') && *s != '<' && *s != '!' && *s != '>') { + if (*s == ' ' || *s == '\t') ++s; else - *name_p++ = *s++; + { + if (*s == '.') + lastdot = name_p; + *name_p++ = *s++; + } } *name_p = 0; @@ -259,22 +292,74 @@ namespace spot } // Lookup the name - std::map::const_iterator ni = val_n.find(name); - if (ni == val_n.end()) + val_map_t::const_iterator ni = val_map.find(name); + if (ni == val_map.end()) { - std::cerr << "No variable `" << name - << "' found in model (for proposition `" - << str << "')." << std::endl; + // We may have a name such as X.Y.Z + // If it is not a known variable, it might mean + // an enumerated variable X.Y with value Z. + if (lastdot) + { + *lastdot++ = 0; + ni = val_map.find(name); + } + + if (ni == val_map.end()) + { + std::cerr << "No variable `" << name + << "' found in model (for proposition `" + << str << "')." << std::endl; + free(name); + ++errors; + continue; + } + + // We have found the enumerated variable, and lastdot is + // pointing to its expected value. + int type_num = ni->second.type; + enum_map_t::const_iterator ei = enum_map[type_num].find(lastdot); + if (ei == enum_map[type_num].end()) + { + std::cerr << "No state `" << lastdot + << "' known for variable `" + << name << "'." << std::endl; + std::cerr << "Possible states are:"; + for (ei = enum_map[type_num].begin(); + ei != enum_map[type_num].end(); ++ei) + std::cerr << " " << ei->first; + std::cerr << std::endl; + + free(name); + ++errors; + continue; + } + + // At this point, *s should be 0. + if (*s) + { + std::cerr << "Trailing garbage `" << s + << "' at end of proposition `" + << str << "'." << std::endl; + free(name); + ++errors; + continue; + } + + // Record that X.Y must be equal to Z. + int v = dict->register_proposition(*ap, d); + one_prop p = { ni->second.num, OP_EQ, ei->second, v }; + out.push_back(p); free(name); - ++errors; continue; } free(name); + int var_num = ni->second.num; + if (!*s) // No operator? Assume "!= 0". { int v = dict->register_proposition(*ap, d); - one_prop p = { ni->second, OP_NE, 0, v }; + one_prop p = { var_num, OP_NE, 0, v }; out.push_back(p); continue; } @@ -353,7 +438,7 @@ namespace spot } int v = dict->register_proposition(*ap, d); - one_prop p = { ni->second, op, val, v }; + one_prop p = { var_num, op, val, v }; out.push_back(p); }