diff --git a/NEWS b/NEWS index 5bc920c00..cfef10722 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,16 @@ New in spot 1.99.7a (not yet released) * Building products with different dictionaries now raise an exception instead of using an assertion that could be disabled. + * 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. + + Python: + + * The ltsmin interface has been binded in Python. See + https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example. + Documentation: * There is a new page giving informal illustrations (and extra diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index 13b18117c..9dfb22e78 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -47,20 +47,36 @@ using namespace spot; %import(module="spot.impl") %import(module="spot.impl") +%exception { + try { + $action + } + catch (const std::runtime_error& e) + { + SWIG_exception(SWIG_RuntimeError, e.what()); + } +} + namespace std { %template(atomic_prop_set) set; } +%rename(model) spot::ltsmin_model; +%rename(kripke_raw) spot::ltsmin_model::kripke; %include %pythoncode %{ import spot -def load(filename, ap_set, dict=spot._bdd_dict, - dead=spot.formula_ap('dead'), - compress=2, debug=False): +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 load_ltsmin(filename, dict, s, dead, compress, debug) + return self.kripke_raw(s, dict, dead, compress) +model.kripke = _kripke %} diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 89d681f5d..4922e8947 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -53,21 +53,33 @@ namespace spot typedef void (*TransitionCB)(void *ctx, transition_info_t *transition_info, int *dst); + } - struct spins_interface + struct spins_interface + { + lt_dlhandle handle; // handle to the dynamic library + void (*get_initial_state)(void *to); + int (*have_property)(); + int (*get_successors)(void* m, int *in, TransitionCB, void *arg); + int (*get_state_size)(); + const char* (*get_state_variable_name)(int var); + int (*get_state_variable_type)(int var); + int (*get_type_count)(); + const char* (*get_type_name)(int type); + int (*get_type_value_count)(int type); + const char* (*get_type_value_name)(int type, int value); + + ~spins_interface() { - lt_dlhandle handle; // handle to the dynamic library - void (*get_initial_state)(void *to); - int (*have_property)(); - int (*get_successors)(void* m, int *in, TransitionCB, void *arg); - int (*get_state_size)(); - const char* (*get_state_variable_name)(int var); - int (*get_state_variable_type)(int var); - int (*get_type_count)(); - const char* (*get_type_name)(int type); - int (*get_type_value_count)(int type); - const char* (*get_type_value_name)(int type, int value); - }; + if (handle) + lt_dlclose(handle); + lt_dlexit(); + } + }; + + namespace + { + typedef std::shared_ptr spins_interface_ptr; //////////////////////////////////////////////////////////////////////// // STATE @@ -322,14 +334,15 @@ namespace spot }; - int + void convert_aps(const atomic_prop_set* aps, - const spins_interface* d, + spins_interface_ptr d, bdd_dict_ptr dict, formula dead, prop_set& out) { int errors = 0; + std::ostringstream err; int state_size = d->get_state_size(); typedef std::map val_map_t; @@ -367,8 +380,7 @@ namespace spot ++s; if (!*s) { - std::cerr << "Proposition `" << str - << "' cannot be parsed." << std::endl; + err << "Proposition `" << str << "' cannot be parsed.\n"; ++errors; continue; } @@ -393,8 +405,7 @@ namespace spot if (name == name_p) { - std::cerr << "Proposition `" << str - << "' cannot be parsed." << std::endl; + err << "Proposition `" << str << "' cannot be parsed.\n"; free(name); ++errors; continue; @@ -415,9 +426,9 @@ namespace spot if (ni == val_map.end()) { - std::cerr << "No variable `" << name - << "' found in model (for proposition `" - << str << "')." << std::endl; + err << "No variable `" << name + << "' found in model (for proposition `" + << str << "').\n"; free(name); ++errors; continue; @@ -429,14 +440,12 @@ namespace spot 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 << '\n'; + err << "No state `" << lastdot << "' known for variable `" + << name << "'.\n"; + err << "Possible states are:"; + for (auto& ej: enum_map[type_num]) + err << ' ' << ej.first; + err << '\n'; free(name); ++errors; @@ -446,16 +455,16 @@ namespace spot // At this point, *s should be 0. if (*s) { - std::cerr << "Trailing garbage `" << s - << "' at end of proposition `" - << str << "'." << std::endl; + err << "Trailing garbage `" << s + << "' at end of proposition `" + << str << "'.\n"; free(name); ++errors; continue; } // Record that X.Y must be equal to Z. - int v = dict->register_proposition(*ap, d); + int v = dict->register_proposition(*ap, d.get()); one_prop p = { ni->second.num, OP_EQ, ei->second, v }; out.push_back(p); free(name); @@ -515,9 +524,9 @@ namespace spot break; default: report_error: - std::cerr << "Unexpected `" << s - << "' while parsing atomic proposition `" << str - << "'." << std::endl; + err << "Unexpected `" << s + << "' while parsing atomic proposition `" << str + << "'.\n"; ++errors; free(name); continue; @@ -534,8 +543,7 @@ namespace spot val = strtol(s, &s_end, 10); if (s == s_end) { - std::cerr << "Failed to parse `" << s - << "' as an integer." << std::endl; + err << "Failed to parse `" << s << "' as an integer.\n"; ++errors; free(name); continue; @@ -555,14 +563,13 @@ namespace spot enum_map_t::const_iterator ei = enum_map[type_num].find(st); if (ei == enum_map[type_num].end()) { - std::cerr << "No state `" << st - << "' known for variable `" - << name << "'." << std::endl; - std::cerr << "Possible states are:"; + err << "No state `" << st << "' known for variable `" + << name << "'.\n"; + err << "Possible states are:"; for (ei = enum_map[type_num].begin(); ei != enum_map[type_num].end(); ++ei) - std::cerr << ' ' << ei->first; - std::cerr << '\n'; + err << ' ' << ei->first; + err << '\n'; free(name); ++errors; @@ -578,11 +585,11 @@ namespace spot ++s; if (*s) { - std::cerr << "Unexpected `" << s - << "' while parsing atomic proposition `" << str - << "'." << std::endl; - ++errors; - continue; + err << "Unexpected `" << s + << "' while parsing atomic proposition `" << str + << "'.\n"; + ++errors; + continue; } @@ -591,7 +598,8 @@ namespace spot out.push_back(p); } - return errors; + if (errors) + throw std::runtime_error(err.str()); } //////////////////////////////////////////////////////////////////////// @@ -601,7 +609,7 @@ namespace spot { public: - spins_kripke(const spins_interface* d, const bdd_dict_ptr& dict, + spins_kripke(spins_interface_ptr d, const bdd_dict_ptr& dict, const spot::prop_set* ps, formula dead, int compress) : kripke(dict), @@ -679,13 +687,9 @@ namespace spot delete[] uncompressed_; delete[] compressed_; } - lt_dlclose(d_->handle); + dict_->unregister_all_my_variables(d_.get()); - dict_->unregister_all_my_variables(d_); - - delete d_; delete ps_; - lt_dlexit(); if (state_condition_last_state_) state_condition_last_state_->destroy(); @@ -918,7 +922,7 @@ namespace spot } private: - const spins_interface* d_; + spins_interface_ptr d_; int state_size_; bdd_dict_ptr dict_; const char** vname_; @@ -950,8 +954,8 @@ namespace spot // Call spins to compile "foo.prom" as "foo.prom.spins" if the latter // does not exist already or is older. - static bool - compile_model(std::string& filename, std::string& ext, bool verbose) + static void + compile_model(std::string& filename, std::string& ext) { std::string command; std::string compiled_ext; @@ -968,22 +972,14 @@ namespace spot } else { - if (verbose) - std::cerr << "Unknown extension `" << ext - << ("'. Use `.prom', `.pm', `.pml', `.dve', `.dve2C' or" - "`.prom.spins'.") << std::endl; - return false; + throw std::runtime_error(std::string("Unknown extension '") + + ext + "'. Use '.prom', '.pm', '.pml', " + "'.dve', '.dve2C', or '.prom.spins'."); } struct stat s; if (stat(filename.c_str(), &s) != 0) - { - if (verbose) - { - std::cerr << "Cannot open " << filename << std::endl; - return true; - } - } + throw std::runtime_error(std::string("Cannot open ") + filename); std::string old = filename; filename += compiled_ext; @@ -998,26 +994,19 @@ namespace spot if (stat(filename.c_str(), &d) == 0) if (s.st_mtime < d.st_mtime) // The .spins or .dve2C is up-to-date, no need to recompile it. - return false; + return; int res = system(command.c_str()); if (res) - { - if (verbose) - std::cerr << "Execution of `" << command.c_str() - << "' returned exit code " << WEXITSTATUS(res) - << ".\n"; - return true; - } - return false; + throw std::runtime_error(std::string("Execution of '") + + command.c_str() + "' returned exit code " + + std::to_string(WEXITSTATUS(res))); } } - kripke_ptr - load_ltsmin(const std::string& file_arg, const bdd_dict_ptr& dict, - const atomic_prop_set* to_observe, - const formula dead, int compress, bool verbose) + ltsmin_model + ltsmin_model::load(const std::string& file_arg) { std::string file; if (file_arg.find_first_of("/\\") != std::string::npos) @@ -1027,33 +1016,20 @@ namespace spot std::string ext = file.substr(file.find_last_of(".")); if (ext != ".spins" && ext != ".dve2C") - { - if (compile_model(file, ext, verbose)) - { - if (verbose) - std::cerr << "Failed to compile `" << file_arg - << "'." << std::endl; - return nullptr; - } - } + compile_model(file, ext); if (lt_dlinit()) - { - if (verbose) - std::cerr << "Failed to initialize libltdl." << std::endl; - return nullptr; - } + throw std::runtime_error("Failed to initialize libltldl."); lt_dlhandle h = lt_dlopen(file.c_str()); if (!h) { - if (verbose) - std::cerr << "Failed to load `" << file << "'." << std::endl; lt_dlexit(); - return nullptr; + throw std::runtime_error(std::string("Failed to load '") + + file + "'."); } - spins_interface* d = new spins_interface; + auto d = std::make_shared(); d->handle = h; // SpinS interface. @@ -1112,36 +1088,38 @@ namespace spot && d->get_type_name && d->get_type_value_count && d->get_type_value_name)) - { - if (verbose) - std::cerr << "Failed to resolve some symbol while loading `" - << file << "'\n"; - delete d; - lt_dlexit(); - return nullptr; - } + throw std::runtime_error(std::string("Failed resolve some symbol" + "while loading '") + file + "'."); if (d->have_property && d->have_property()) - { - if (verbose) - std::cerr << "Model with an embedded property are not supported." - << std::endl; - delete d; - lt_dlexit(); - return nullptr; - } + throw std::runtime_error("Models with embedded properties " + "are not supported."); + return { d }; + } + + + kripke_ptr + ltsmin_model::kripke(const atomic_prop_set* to_observe, + bdd_dict_ptr dict, + const formula dead, int compress) const + { spot::prop_set* ps = new spot::prop_set; - int errors = convert_aps(to_observe, d, dict, dead, *ps); - if (errors) + try + { + convert_aps(to_observe, iface, dict, dead, *ps); + } + catch (std::runtime_error) { delete ps; - dict->unregister_all_my_variables(d); - delete d; - lt_dlexit(); - return nullptr; + dict->unregister_all_my_variables(iface.get()); + throw; } - return std::make_shared(d, dict, ps, dead, compress); + return std::make_shared(iface, dict, ps, dead, compress); + } + + ltsmin_model::~ltsmin_model() + { } } diff --git a/spot/ltsmin/ltsmin.hh b/spot/ltsmin/ltsmin.hh index d216ad7b6..c45f8a133 100644 --- a/spot/ltsmin/ltsmin.hh +++ b/spot/ltsmin/ltsmin.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -24,40 +24,56 @@ namespace spot { + struct spins_interface; - // \brief Load an ltsmin model, either from divine or promela. - // - // The filename given can be either a *.pm/*.pml/*.prom promela - // source or a *.spins dynamic library compiled with "spins file". - // If a promela source is supplied, this function will call spins to - // update the *.spins library only if it is not newer. - // - // Similarly the divine models can be specified as *.dve source or - // *.dve or *.dve2C libraries. - // - // The dead parameter is used to control the behavior of the model - // on dead states (i.e. the final states of finite sequences). - // If DEAD is "false", it means we are not - // interested in finite sequences of the system, and dead state - // will have no successor. If DEAD is - // "true", we want to check finite sequences as well as infinite - // sequences, but do not need to distinguish them. In that case - // dead state will have a loop labeled by true. If DEAD is any - // other string, this is the name a property that should be true - // when looping on a dead state, and false otherwise. - // - // This function returns 0 on error. - // - // \a file the name of the *.prom source file or the dynamic library - // \a to_observe the list of atomic propositions that should be observed - // in the model - // \a dict the BDD dictionary to use - // \a dead an atomic proposition or constant to use for looping on - // dead states - // \a verbose whether to output verbose messages - SPOT_API kripke_ptr - load_ltsmin(const std::string& file, const bdd_dict_ptr& dict, - const atomic_prop_set* to_observe, - formula dead = formula::tt(), - int compress = 0, bool verbose = true); + class SPOT_API ltsmin_model final + { + public: + ~ltsmin_model(); + + // \brief Load an ltsmin model, either from divine or promela. + // + // The filename given can be either a *.pm/*.pml/*.prom promela + // source or a *.spins dynamic library compiled with "spins file". + // If a promela source is supplied, this function will call spins to + // update the *.spins library only if it is not newer. + // + // Similarly the divine models can be specified as *.dve source or + // *.dve or *.dve2C libraries. + // + static ltsmin_model load(const std::string& file); + + // \brief Generate a Kripke structure on-the-fly + // + // The dead parameter is used to control the behavior of the model + // on dead states (i.e. the final states of finite sequences). + // If DEAD is "false", it means we are not + // interested in finite sequences of the system, and dead state + // will have no successor. If DEAD is + // "true", we want to check finite sequences as well as infinite + // sequences, but do not need to distinguish them. In that case + // dead state will have a loop labeled by true. If DEAD is any + // other string, this is the name a property that should be true + // when looping on a dead state, and false otherwise. + // + // This function returns 0 on error. + // + // \a to_observe the list of atomic propositions that should be observed + // in the model + // \a dict the BDD dictionary to use + // \a dead an atomic proposition or constant to use for looping on + // dead states + // \a compress whether to compress the states. Use 0 to disable, 1 + // to enable compression, 2 to enable a faster compression that only + // work if all variables are smaller than 2^28. + kripke_ptr kripke(const atomic_prop_set* to_observe, + bdd_dict_ptr dict, + formula dead = formula::tt(), + int compress = 0) const; + private: + ltsmin_model(std::shared_ptr iface) : iface(iface) + { + } + std::shared_ptr iface; + }; } diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index d73634da9..ed81b09e7 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE) +// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de +// Recherche et Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -216,8 +216,15 @@ checked_main(int argc, char **argv) if (output != DotFormula) { tm.start("loading ltsmin model"); - model = spot::load_ltsmin(argv[1], dict, &ap, deadf, - compress_states, true); + try + { + model = spot::ltsmin_model::load(argv[1]).kripke(&ap, dict, deadf, + compress_states); + } + catch (std::runtime_error& e) + { + std::cerr << e.what() << '\n'; + } tm.stop("loading ltsmin model"); if (!model) diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb index 5346b61d9..a39f9c40e 100644 --- a/tests/python/ltsmin.ipynb +++ b/tests/python/ltsmin.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:d5994cc04991eaf218539c16319f17128cf42be5d813785fd977ee3d991a5c00" + "signature": "sha256:eba4457368b676284d4696dd7afe5596d865c6f9f6f44b5fd5dc7c6585757c89" }, "nbformat": 3, "nbformat_minor": 0, @@ -59,7 +59,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "m = spot.ltsmin.load(srcdir + '/../ltsmin/finite.dve', ['P.a<1', 'P.b>2'])\n", + "m = spot.ltsmin.load(srcdir + '/../ltsmin/finite.dve')\n", "m" ], "language": "python", @@ -69,6 +69,27 @@ "metadata": {}, "output_type": "pyout", "prompt_number": 3, + "text": [ + " >" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "k = m.kripke([\"P.a<1\", \"P.b>2\"])\n", + "k" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7f40740974e0> >" + " *' at 0x7f6990bd4600> >" ] } ], - "prompt_number": 3 + "prompt_number": 4 }, { "cell_type": "code", @@ -328,7 +349,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 4, + "prompt_number": 5, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7f40740977e0> >" + " *' at 0x7f6990bd4c90> >" ] } ], - "prompt_number": 4 + "prompt_number": 5 }, { "cell_type": "code", "collapsed": false, "input": [ - "spot.otf_product(m, a)" + "spot.otf_product(k, a)" ], "language": "python", "metadata": {}, @@ -398,7 +419,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 5, + "prompt_number": 6, "svg": [ "\n", "\n" ], "text": [ - " *' at 0x7f4074097720> >" + " *' at 0x7f6990bd49c0> >" ] } ], - "prompt_number": 5 - }, - { - "cell_type": "code", - "collapsed": false, - "input": [], - "language": "python", - "metadata": {}, - "outputs": [], - "prompt_number": 5 + "prompt_number": 6 } ], "metadata": {}