diff --git a/ChangeLog b/ChangeLog index 83cabbf4e..1b7ed98c0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2011-03-05 Alexandre Duret-Lutz + + Teach the DVE2 interface about atomic propositions such as "a <= + 10" or "b != 3". This only work for integer variables presently. + + * iface/dve2/dve2.hh (load_dve2): Take an atomic_prop_set + argument to indicate the AP to observe. + * iface/dve2/dve2.cc (convert_aps): New function. Parse the + atomic propositions in format them in a prop_set structure that + will allow fast generation of the state condition. + (load_dve2): Call convert_aps, and pass the resulting prop_set + structure to the kripke object. + (dve2_kripke::dve2_kripke): Store the prop_set structure. + (dve2_kripke::~dve2_kripke): Release the prop_set, and unregister + the bdd_variable associated to it. + (compute_state_condition): New method that uses the prop_set. + (succ_iter, state_condition): Call compute_state_condition(). + * iface/dve2/dve2check.cc: Adjust the call to load_dve2 to + pass it atomic propositions read from the command line. + 2011-03-05 Alexandre Duret-Lutz Display states variables in the state label. diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 773488424..fe7062bf2 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -192,6 +192,174 @@ namespace spot callback_context::transitions_t::const_iterator it_; }; + //////////////////////////////////////////////////////////////////////// + // PREDICATE EVALUATION + + typedef enum { OP_EQ, OP_NE, OP_LT, OP_GT, OP_LE, OP_GE } relop; + + struct one_prop + { + int var_num; + relop op; + int val; + int bddvar; // if "var_num op val" is true, output bddvar, + // else its negation + }; + typedef std::vector prop_set; + + int + convert_aps(const ltl::atomic_prop_set* aps, + const dve2_interface* d, + bdd_dict* dict, + prop_set& out) + { + int errors = 0; + + int state_size = d->get_state_variable_count(); + std::map val_n; + for (int i = 0; i < state_size; ++i) + val_n[d->get_state_variable_name(i)] = i; + + for (ltl::atomic_prop_set::const_iterator ap = aps->begin(); + ap != aps->end(); ++ap) + { + std::string str = (*ap)->name(); + const char* s = str.c_str(); + + // Skip any leading blank. + while (*s && (*s == ' ' || *s == '\t')) + ++s; + if (!*s) + { + std::cerr << "Proposition `" << str + << "' cannot be parsed." << std::endl; + ++errors; + continue; + } + + + char* name = (char*) malloc(str.size() + 1); + char* name_p = name; + while (*s && (*s != '=') && *s != '<' && *s != '!' && *s != '>') + { + if (*s == ' ' || *s == '\t') + ++s; + else + *name_p++ = *s++; + } + *name_p = 0; + + if (name == name_p) + { + std::cerr << "Proposition `" << str + << "' cannot be parsed." << std::endl; + free(name); + ++errors; + continue; + } + + // Lookup the name + std::map::const_iterator ni = val_n.find(name); + if (ni == val_n.end()) + { + std::cerr << "No variable `" << name + << "' found in model (for proposition `" + << str << "')." << std::endl; + free(name); + ++errors; + continue; + } + free(name); + + if (!*s) // No operator? Assume "!= 0". + { + int v = dict->register_proposition(*ap, d); + one_prop p = { ni->second, OP_NE, 0, v }; + out.push_back(p); + continue; + } + + relop op; + + switch (*s) + { + case '!': + if (s[1] != '=') + goto report_error; + op = OP_NE; + s += 2; + break; + case '=': + if (s[1] != '=') + goto report_error; + op = OP_EQ; + s += 2; + break; + case '<': + if (s[1] == '=') + { + op = OP_LE; + s += 2; + } + else + { + op = OP_LT; + ++s; + } + break; + case '>': + if (s[1] == '=') + { + op = OP_LE; + s += 2; + } + else + { + op = OP_LT; + ++s; + } + break; + default: + report_error: + std::cerr << "Unexpected `" << s + << "' while parsing atomic proposition `" << str + << "'." << std::endl; + ++errors; + continue; + } + + while (*s && (*s == ' ' || *s == '\t')) + ++s; + + char* s_end; + int val = strtol(s, &s_end, 10); + if (s == s_end) + { + std::cerr << "Failed to parse `" << s + << "' as an integer." << std::endl; + ++errors; + continue; + } + s = s_end; + while (*s && (*s == ' ' || *s == '\t')) + ++s; + if (*s) + { + std::cerr << "Unexpected character `" << s + << "' while parsing atomic proposition `" << str + << "'." << std::endl; + ++errors; + continue; + } + + int v = dict->register_proposition(*ap, d); + one_prop p = { ni->second, op, val, v }; + out.push_back(p); + } + + return errors; + } + //////////////////////////////////////////////////////////////////////// // KRIPKE @@ -199,8 +367,8 @@ namespace spot { public: - dve2_kripke(const dve2_interface* d, bdd_dict* dict) - : d_(d), dict_(dict) + dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps) + : d_(d), dict_(dict), ps_(ps) { state_size_ = d_->get_state_variable_count(); @@ -212,7 +380,13 @@ namespace spot ~dve2_kripke() { delete[] vname_; + lt_dlclose(d_->handle); + + dict_->unregister_all_my_variables(d_); + delete d_; + delete ps_; + lt_dlexit(); } virtual @@ -224,6 +398,36 @@ namespace spot return res; } + bdd + compute_state_condition(const dve2_state* s) const + { + bdd res = bddtrue; + for (prop_set::const_iterator i = ps_->begin(); + i != ps_->end(); ++i) + { + int l = s->vars[(*i).var_num]; + int r = (*i).val; + + + bool cond = false; + switch ((*i).op) + { + case OP_EQ: cond = (l == r); break; + case OP_NE: cond = (l != r); break; + case OP_LT: cond = (l < r); break; + case OP_GT: cond = (l > r); break; + case OP_LE: cond = (l <= r); break; + case OP_GE: cond = (l >= r); break; + } + + if (cond) + res &= bdd_ithvar((*i).bddvar); + else + res &= bdd_nithvar((*i).bddvar); + } + return res; + } + virtual dve2_succ_iterator* succ_iter(const state* local_state, @@ -238,15 +442,16 @@ namespace spot (void) t; assert((unsigned)t == cc->transitions.size()); - return new dve2_succ_iterator(cc, bddtrue); + return new dve2_succ_iterator(cc, compute_state_condition(s)); } virtual bdd - state_condition(const state* s) const + state_condition(const state* st) const { - (void) s; - return bddfalse; + const dve2_state* s = dynamic_cast(st); + assert(s); + return compute_state_condition(s); } virtual @@ -283,6 +488,7 @@ namespace spot int state_size_; bdd_dict* dict_; const char** vname_; + const prop_set* ps_; }; } @@ -291,7 +497,8 @@ namespace spot //////////////////////////////////////////////////////////////////////////// // LOADER - kripke* load_dve2(const std::string& file_arg, bdd_dict* dict, bool verbose) + kripke* load_dve2(const std::string& file_arg, bdd_dict* dict, + ltl::atomic_prop_set* to_observe, bool verbose) { std::string file; if (file_arg.find_first_of("/\\") != std::string::npos) @@ -371,6 +578,17 @@ namespace spot return 0; } - return new dve2_kripke(d, dict); + prop_set* ps = new prop_set; + int errors = convert_aps(to_observe, d, dict, *ps); + if (errors) + { + delete ps; + dict->unregister_all_my_variables(d); + delete d; + lt_dlexit(); + return 0; + } + + return new dve2_kripke(d, dict, ps); } } diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh index 8e6de9ae3..2975d6d18 100644 --- a/iface/dve2/dve2.hh +++ b/iface/dve2/dve2.hh @@ -22,10 +22,15 @@ # define SPOT_IFACE_DVE2_DVE2_HH #include "kripke/kripke.hh" +#include "ltlvisit/apcollect.hh" + + namespace spot { - kripke* load_dve2(const std::string& file, bdd_dict* dict, + kripke* load_dve2(const std::string& file, + bdd_dict* dict, + ltl::atomic_prop_set* to_observe, bool verbose = true); } diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index 38498dd48..9f6bb330f 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -20,12 +20,16 @@ #include "dve2.hh" #include "tgbaalgos/dotty.hh" -#include "ltlenv/declenv.hh" +#include "ltlenv/defaultenv.hh" +#include "ltlast/allnodes.hh" int main(int argc, char **argv) { - spot::ltl::declarative_environment env; + spot::ltl::default_environment& env = + spot::ltl::default_environment::instance(); + + spot::ltl::atomic_prop_set ap; if (argc <= 1) { @@ -35,12 +39,18 @@ main(int argc, char **argv) while (argc > 2) { - env.declare(argv[argc - 1]); + ap.insert(static_cast + (env.require(argv[argc - 1]))); --argc; } spot::bdd_dict* dict = new spot::bdd_dict(); - spot::kripke* a = spot::load_dve2(argv[1], dict, true); + spot::kripke* a = spot::load_dve2(argv[1], dict, &ap, true); + + for (spot::ltl::atomic_prop_set::const_iterator it = ap.begin(); + it != ap.end(); ++it) + (*it)->destroy(); + ap.clear(); if (!a) { @@ -51,5 +61,17 @@ main(int argc, char **argv) spot::dotty_reachable(std::cout, a); delete a; + + spot::ltl::atomic_prop::dump_instances(std::cerr); + spot::ltl::unop::dump_instances(std::cerr); + spot::ltl::binop::dump_instances(std::cerr); + spot::ltl::multop::dump_instances(std::cerr); + spot::ltl::automatop::dump_instances(std::cerr); + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::automatop::instance_count() == 0); + delete dict; }