From 3bf3d2c8a165352731a4f1baa79bd94c82c5fb2e Mon Sep 17 00:00:00 2001 From: Thibaud Michaud Date: Thu, 6 Nov 2014 16:02:57 +0100 Subject: [PATCH] Adding python functions to mirror the functionalities found in src/bin * wrap/python/spot.i: Rename to... * wrap/python/spot_impl.i: ...this, and import spot_impl from spot.py so that it is not needed to recompile everything when modifying python code. * wrap/python/spot.py: Adding python functions to mirror the functionalities found in src/bin. * src/bin/common_r.cc: Move simplification level... * src/ltlvisit/simplify.hh: ... here as a constructor of ltl_simplifier_options, to make it available in wrap/python. * src/bin/ltlfilt.cc: Set simplification level using the new ltl_simplifier_options constructor. * src/bin/randltl.cc: Move most of the code... * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: ... here, as a class named randltlgenerator. * wrap/python/tests/bddnqueen.py, wrap/python/tests/minato.py: Avoid calling bdd_init twice by moving 'import spot' after bdd initialization. * wrap/python/Makefile.am: Rename spot to spot_impl * wrap/python/tests/Makefile.am: Add ipnbdoctest.py. * wrap/python/.gitignore: Rename spot.py to spot_impl.py * src/ltlvisit/tostring.cc: \ttrue and \ffalse should be \top and \bot. * wrap/python/tests/ipnbdoctest.py: Run code cells of a python notebook and compare the output to the actual content of the notebook. * wrap/python/tests/randltl.ipynb: Document and test randltl. * wrap/python/tests/run.in: Call ipnbdoctest.py to run ipython notebooks. --- src/bin/common_r.cc | 25 +- src/bin/ltlfilt.cc | 2 +- src/bin/randltl.cc | 241 +++-------- src/ltlvisit/randomltl.cc | 225 +++++++++- src/ltlvisit/randomltl.hh | 73 +++- src/ltlvisit/simplify.hh | 21 + src/ltlvisit/tostring.cc | 4 +- wrap/python/.gitignore | 2 +- wrap/python/Makefile.am | 24 +- wrap/python/spot.py | 227 ++++++++++ wrap/python/{spot.i => spot_impl.i} | 57 ++- wrap/python/tests/Makefile.am | 6 +- wrap/python/tests/bddnqueen.py | 6 +- wrap/python/tests/ipnbdoctest.py | 220 ++++++++++ wrap/python/tests/minato.py | 7 +- wrap/python/tests/randltl.ipynb | 632 ++++++++++++++++++++++++++++ wrap/python/tests/run.in | 13 +- 17 files changed, 1528 insertions(+), 257 deletions(-) create mode 100644 wrap/python/spot.py rename wrap/python/{spot.i => spot_impl.i} (92%) create mode 100755 wrap/python/tests/ipnbdoctest.py create mode 100644 wrap/python/tests/randltl.ipynb diff --git a/src/bin/common_r.cc b/src/bin/common_r.cc index fea33d061..599aaace6 100644 --- a/src/bin/common_r.cc +++ b/src/bin/common_r.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -38,26 +38,3 @@ parse_r(const char* arg) } error(2, 0, "invalid simplification level '%s'", arg); } - -spot::ltl::ltl_simplifier_options -simplifier_options() -{ - spot::ltl::ltl_simplifier_options options(false, false, false); - switch (simplification_level) - { - case 3: - options.containment_checks = true; - options.containment_checks_stronger = true; - // fall through - case 2: - options.synt_impl = true; - // fall through - case 1: - options.reduce_basics = true; - options.event_univ = true; - // fall through - default: - break; - } - return options; -} diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index da4606612..7d0b039f1 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -638,7 +638,7 @@ main(int argc, char** argv) if (boolean_to_isop && simplification_level == 0) simplification_level = 1; - spot::ltl::ltl_simplifier_options opt = simplifier_options(); + spot::ltl::ltl_simplifier_options opt(simplification_level); opt.boolean_to_isop = boolean_to_isop; spot::ltl::ltl_simplifier simpl(opt); try diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index ea45978da..a6bdd8013 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -42,6 +42,7 @@ #include "ltlenv/defaultenv.hh" #include "misc/random.hh" #include "misc/hash.hh" +#include "misc/optionmap.hh" const char argp_program_doc[] ="\ Generate random temporal logic formulas.\n\n\ @@ -135,9 +136,8 @@ const struct argp_child children[] = { 0, 0, 0, 0 } }; -static enum { OutputBool, OutputLTL, OutputSERE, OutputPSL } - output = OutputLTL; spot::ltl::atomic_prop_set aprops; +static int output = OUTPUTLTL; static char* opt_pL = 0; static char* opt_pS = 0; static char* opt_pB = 0; @@ -149,39 +149,6 @@ static bool opt_unique = true; static bool opt_wf = false; static bool ap_count_given = false; -void -remove_some_props(spot::ltl::atomic_prop_set& s) -{ - // How many propositions to remove from s? - // (We keep at least one.) - size_t n = spot::mrand(s.size()); - - while (n--) - { - auto i = s.begin(); - std::advance(i, spot::mrand(s.size())); - s.erase(i); - } -} - -// GF(p_1) & GF(p_2) & ... & GF(p_n) -const spot::ltl::formula* -GF_n(spot::ltl::atomic_prop_set& ap) -{ - const spot::ltl::formula* res = 0; - for (auto v: ap) - { - const spot::ltl::formula* f = - spot::ltl::unop::instance(spot::ltl::unop::F, v->clone()); - f = spot::ltl::unop::instance(spot::ltl::unop::G, f); - if (res) - res = spot::ltl::multop::instance(spot::ltl::multop::And, f, res); - else - res = f; - } - return res; -} - static int parse_opt(int key, char* arg, struct argp_state* as) { @@ -189,22 +156,22 @@ parse_opt(int key, char* arg, struct argp_state* as) switch (key) { case 'B': - output = OutputBool; + output = OUTPUTBOOL; break; case 'L': - output = OutputLTL; + output = OUTPUTLTL; break; case 'n': opt_formulas = to_int(arg); break; case 'P': - output = OutputPSL; + output = OUTPUTPSL; break; case OPT_R: parse_r(arg); break; case 'S': - output = OutputSERE; + output = OUTPUTSERE; break; case OPT_BOOLEAN_PRIORITIES: opt_pB = arg; @@ -271,90 +238,6 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) exit(err); - spot::ltl::random_formula* rf = 0; - spot::ltl::random_psl* rp = 0; - spot::ltl::random_sere* rs = 0; - const char* tok_pL = 0; - const char* tok_pS = 0; - const char* tok_pB = 0; - - switch (output) - { - case OutputLTL: - rf = new spot::ltl::random_ltl(&aprops); - tok_pL = rf->parse_options(opt_pL); - if (opt_pS) - error(2, 0, "option --sere-priorities unsupported for LTL output"); - if (opt_pB) - error(2, 0, "option --boolean-priorities unsupported for LTL output"); - break; - case OutputBool: - rf = new spot::ltl::random_boolean(&aprops); - tok_pB = rf->parse_options(opt_pB); - if (opt_pL) - error(2, 0, "option --ltl-priorities unsupported for Boolean output"); - if (opt_pS) - error(2, 0, "option --sere-priorities unsupported for Boolean output"); - break; - case OutputSERE: - rf = rs = new spot::ltl::random_sere(&aprops); - tok_pS = rs->parse_options(opt_pS); - tok_pB = rs->rb.parse_options(opt_pB); - if (opt_pL) - error(2, 0, "option --ltl-priorities unsupported for SERE output"); - break; - case OutputPSL: - rf = rp = new spot::ltl::random_psl(&aprops); - rs = &rp->rs; - tok_pL = rp->parse_options(opt_pL); - tok_pS = rs->parse_options(opt_pS); - tok_pB = rs->rb.parse_options(opt_pB); - break; - } - - if (tok_pL) - error(2, 0, "failed to parse LTL priorities near '%s'", tok_pL); - if (tok_pS) - error(2, 0, "failed to parse SERE priorities near '%s'", tok_pS); - if (tok_pB) - error(2, 0, "failed to parse Boolean priorities near '%s'", tok_pB); - - if (opt_dump_priorities) - { - switch (output) - { - case OutputLTL: - std::cout - << "Use --ltl-priorities to set the following LTL priorities:\n"; - rf->dump_priorities(std::cout); - break; - case OutputBool: - std::cout - << ("Use --boolean-priorities to set the following Boolean " - "formula priorities:\n"); - rf->dump_priorities(std::cout); - break; - case OutputPSL: - std::cout - << "Use --ltl-priorities to set the following LTL priorities:\n"; - rp->dump_priorities(std::cout); - // Fall through. - case OutputSERE: - std::cout - << "Use --sere-priorities to set the following SERE priorities:\n"; - rs->dump_priorities(std::cout); - std::cout - << ("Use --boolean-priorities to set the following Boolean " - "formula priorities:\n"); - rs->rb.dump_priorities(std::cout); - break; - default: - error(2, 0, "internal error: unknown type of output"); - } - destroy_atomic_prop_set(aprops); - exit(0); - } - // running 'randltl 0' is one way to generate formulas using no // atomic propositions so do not complain in that case. if (aprops.empty() && !ap_count_given) @@ -363,69 +246,71 @@ main(int argc, char** argv) spot::srand(opt_seed); - typedef - std::unordered_set> fset_t; - fset_t unique_set; + spot::option_map opts; + opts.set("output", output); + opts.set("tree_size_min", opt_tree_size.min); + opts.set("tree_size_max", opt_tree_size.max); + opts.set("opt_wf", opt_wf); + opts.set("opt_seed", opt_seed); + opts.set("simplification_level", simplification_level); + spot::ltl::randltlgenerator rg(aprops, opts, opt_pL, opt_pS, opt_pB); - spot::ltl::ltl_simplifier simpl(simplifier_options()); + if (opt_dump_priorities) + { + switch (output) + { + case OUTPUTLTL: + std::cout + << "Use --ltl-priorities to set the following LTL priorities:\n"; + rg.dump_ltl_priorities(std::cout); + break; + case OUTPUTBOOL: + std::cout + << ("Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"); + rg.dump_bool_priorities(std::cout); + break; + case OUTPUTPSL: + std::cout + << "Use --ltl-priorities to set the following LTL priorities:\n"; + rg.dump_psl_priorities(std::cout); + // Fall through. + case OUTPUTSERE: + std::cout + << "Use --sere-priorities to set the following SERE priorities:\n"; + rg.dump_sere_priorities(std::cout); + std::cout + << ("Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"); + rg.dump_sere_bool_priorities(std::cout); + break; + default: + error(2, 0, "internal error: unknown type of output"); + } + opts.~option_map(); + destroy_atomic_prop_set(aprops); + exit(0); + } while (opt_formulas < 0 || opt_formulas--) { -#define MAX_TRIALS 100000 - unsigned trials = MAX_TRIALS; - bool ignore; - const spot::ltl::formula* f = 0; - do - { - ignore = false; - int size = opt_tree_size.min; - if (size != opt_tree_size.max) - size = spot::rrand(size, opt_tree_size.max); - f = rf->generate(size); - - if (opt_wf) - { - spot::ltl::atomic_prop_set s = aprops; - remove_some_props(s); - f = spot::ltl::multop::instance(spot::ltl::multop::And, - f, GF_n(s)); - } - - if (simplification_level) - { - const spot::ltl::formula* tmp = simpl.simplify(f); - f->destroy(); - f = tmp; - } - if (opt_unique) - { - if (unique_set.insert(f).second) - { - f->clone(); - } - else - { - ignore = true; - f->destroy(); - } - } - } - while (ignore && --trials); - if (trials == 0) - error(2, 0, "failed to generate a new unique formula after %d trials", - MAX_TRIALS); static int count = 0; - output_formula_checked(f, 0, ++count); - f->destroy(); + spot::ltl::randltlgenerator rg2(aprops, opts); + const spot::ltl::formula* f = rg.next(); + if (!f) + { + opts.~option_map(); + error(2, 0, "failed to generate a new unique formula after %d "\ + "trials", MAX_TRIALS); + } + else + { + output_formula_checked(f, 0, ++count); + f->destroy(); + } }; - delete rf; - // Cleanup the unicity table. - for (auto i: unique_set) - i->destroy(); - // Cleanup the atomic_prop set. destroy_atomic_prop_set(aprops); return 0; } diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 8d14dc618..d58119ca6 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -27,6 +27,9 @@ #include "misc/random.hh" #include #include +#include "misc/optionmap.hh" +#include "ltlenv/defaultenv.hh" +#include namespace spot { @@ -266,6 +269,8 @@ namespace spot const char* random_formula::parse_options(char* options) { + if (!options) + return nullptr; char* key = strtok(options, "=\t, :;"); while (key) { @@ -399,5 +404,221 @@ namespace spot update_sums(); } - } // ltl -} // spot + void + randltlgenerator::construct(atomic_prop_set aprops, option_map& opts, + char* opt_pL, + char* opt_pS, + char* opt_pB) + + { + aprops_ = aprops; + output_ = opts.get("output", OUTPUTLTL); + opt_seed_ = opts.get("seed", 0); + opt_tree_size_min_ = opts.get("tree_size_min", 15); + opt_tree_size_max_ = opts.get("tree_size_max", 15); + opt_unique_ = opts.get("unique", true); + opt_wf_ = opts.get("wf", false); + opt_simpl_level_ = opts.get("simplification_level", 3); + + const char* tok_pL = 0; + const char* tok_pS = 0; + const char* tok_pB = 0; + + switch (output_) + { + case OUTPUTLTL: + rf_ = new random_ltl(&aprops_); + if (opt_pS) + throw std::invalid_argument("Cannot set sere priorities with "\ + "LTL output"); + if (opt_pB) + throw std::invalid_argument("Cannot set boolean priorities with "\ + "LTL output"); + tok_pL = rf_->parse_options(opt_pL); + break; + case OUTPUTBOOL: + rf_ = new random_boolean(&aprops_); + tok_pB = rf_->parse_options(opt_pB); + if (opt_pL) + throw std::invalid_argument("Cannot set ltl priorities with "\ + "Boolean output"); + if (opt_pS) + throw std::invalid_argument("Cannot set sere priorities "\ + "with Boolean output"); + break; + case OUTPUTSERE: + rf_ = rs_ = new random_sere(&aprops_); + tok_pS = rs_->parse_options(opt_pS); + tok_pB = rs_->rb.parse_options(opt_pB); + if (opt_pL) + throw std::invalid_argument("Cannot set ltl priorities "\ + "with SERE output"); + break; + case OUTPUTPSL: + rf_ = rp_ = new random_psl(&aprops_); + rs_ = &rp_->rs; + tok_pL = rp_->parse_options(opt_pL); + tok_pS = rs_->parse_options(opt_pS); + tok_pB = rs_->rb.parse_options(opt_pB); + break; + } + + if (tok_pL) + throw("failed to parse LTL priorities near '" + std::string(tok_pL)); + if (tok_pS) + throw("failed to parse SERE priorities near " + std::string(tok_pS)); + if (tok_pB) + throw("failed to parse Boolean priorities near " + + std::string(tok_pB)); + + spot::srand(opt_seed_); + ltl_simplifier_options simpl_opts(opt_simpl_level_); + ltl_simplifier simpl_(simpl_opts); + } + + randltlgenerator::randltlgenerator(int aprops_n, option_map& opts, + char* opt_pL, + char* opt_pS, + char* opt_pB) + { + atomic_prop_set aprops_; + default_environment& e = + default_environment::instance(); + for (int i = 0; i < aprops_n; ++i) + { + std::ostringstream p; + p << 'p' << i; + aprops_.insert(static_cast + (e.require(p.str()))); + } + construct(aprops_, opts, opt_pL, opt_pS, opt_pB); + } + + randltlgenerator::randltlgenerator(atomic_prop_set aprops, + option_map& opts, + char* opt_pL, + char* opt_pS, + char* opt_pB) + + { + construct(aprops, opts, opt_pL, opt_pS, opt_pB); + } + + + randltlgenerator::~randltlgenerator() + { + delete rf_; + // Cleanup the unicity table. + for (auto i: unique_set_) + i->destroy(); + } + const formula* randltlgenerator::next() + { + unsigned trials = MAX_TRIALS; + bool ignore; + const formula* f = nullptr; + do + { + ignore = false; + int size = opt_tree_size_min_; + if (size != opt_tree_size_max_) + size = spot::rrand(size, opt_tree_size_max_); + f = rf_->generate(size); + + if (opt_wf_) + { + atomic_prop_set s = aprops_; + remove_some_props(s); + f = multop::instance(multop::And, + f, GF_n()); + } + + if (opt_simpl_level_) + { + const spot::ltl::formula* tmp = simpl_.simplify(f); + f->destroy(); + f = tmp; + } + + if (opt_unique_) + { + if (unique_set_.insert(f).second) + { + f->clone(); + } + else + { + ignore = true; + f->destroy(); + } + } + } while (ignore && --trials); + if (trials <= 0) + return nullptr; + return f; + } + + void + randltlgenerator::remove_some_props(atomic_prop_set& s) + { + // How many propositions to remove from s? + // (We keep at least one.) + size_t n = spot::mrand(aprops_.size()); + + while (n--) + { + auto i = s.begin(); + std::advance(i, spot::mrand(s.size())); + s.erase(i); + } + } + + // GF(p_1) & GF(p_2) & ... & GF(p_n) + const formula* + randltlgenerator::GF_n() + { + const formula* res = 0; + for (auto v: aprops_) + { + const formula* f = + unop::instance(unop::F, v->clone()); + f = unop::instance(unop::G, f); + if (res) + res = multop::instance(multop::And, f, res); + else + res = f; + } + return res; + } + + void + randltlgenerator::dump_ltl_priorities(std::ostream& os) + { + rf_->dump_priorities(os); + } + + void + randltlgenerator::dump_bool_priorities(std::ostream& os) + { + rf_->dump_priorities(os); + } + + void + randltlgenerator::dump_psl_priorities(std::ostream& os) + { + rp_->dump_priorities(os); + } + + void + randltlgenerator::dump_sere_priorities(std::ostream& os) + { + rs_->dump_priorities(os); + } + + void + randltlgenerator::dump_sere_bool_priorities(std::ostream& os) + { + rs_->rb.dump_priorities(os); + } + } +} diff --git a/src/ltlvisit/randomltl.hh b/src/ltlvisit/randomltl.hh index 77457866a..d14f3243b 100644 --- a/src/ltlvisit/randomltl.hh +++ b/src/ltlvisit/randomltl.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -26,6 +26,17 @@ #include "apcollect.hh" #include +#include +#include "misc/optionmap.hh" +#include "misc/hash.hh" +#include "simplify.hh" + +#define OUTPUTBOOL 1 +#define OUTPUTLTL 2 +#define OUTPUTSERE 3 +#define OUTPUTPSL 4 +#define MAX_TRIALS 100000 + namespace spot { namespace ltl @@ -292,10 +303,64 @@ namespace spot random_sere rs; }; + class SPOT_API randltlgenerator + { + typedef + std::unordered_set> fset_t; + + public: + randltlgenerator(int aprops_n, option_map& opts, + char* opt_pL = nullptr, + char* opt_pS = nullptr, + char* opt_pB = nullptr); - } -} + randltlgenerator(atomic_prop_set aprops, option_map& opts, + char* opt_pL = nullptr, + char* opt_pS = nullptr, + char* opt_pB = nullptr); + + void construct(atomic_prop_set aprops, option_map& opts, + char* opt_pL, char* opt_pS, + char* opt_pB); + + ~randltlgenerator(); + + const spot::ltl::formula* next(); + + void dump_ltl_priorities(std::ostream& os); + + void dump_bool_priorities(std::ostream& os); + void dump_psl_priorities(std::ostream& os); + void dump_sere_priorities(std::ostream& os); + + void dump_sere_bool_priorities(std::ostream& os); + + void remove_some_props(atomic_prop_set& s); + + const formula* GF_n(); + + private: + fset_t unique_set_; + atomic_prop_set aprops_; + + int opt_seed_; + int opt_tree_size_min_; + int opt_tree_size_max_; + bool opt_unique_; + bool opt_wf_; + int opt_simpl_level_; + ltl_simplifier simpl_; + + int output_; + + random_formula* rf_ = 0; + random_psl* rp_ = 0; + random_sere* rs_ = 0; + }; + } +} #endif // SPOT_LTLVIST_RANDOMLTL_HH diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index e7e9e46bf..5a6bcfe6c 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -53,6 +53,27 @@ namespace spot { } + ltl_simplifier_options(int level) : + ltl_simplifier_options(false, false, false) + { + switch (level) + { + case 3: + containment_checks = true; + containment_checks_stronger = true; + // fall through + case 2: + synt_impl = true; + // fall through + case 1: + reduce_basics = true; + event_univ = true; + // fall through + default: + break; + } + } + bool reduce_basics; bool synt_impl; bool event_univ; diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index bea663b7a..759e53492 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -273,8 +273,8 @@ namespace spot }; const char* sclatex_kw[] = { - "\\ffalse", - "\\ttrue", + "\\bot", + "\\top", "\\varepsilon", " \\oplus ", " \\rightarrow ", diff --git a/wrap/python/.gitignore b/wrap/python/.gitignore index 06748a6ea..891c9779a 100644 --- a/wrap/python/.gitignore +++ b/wrap/python/.gitignore @@ -3,7 +3,7 @@ Makefile Makefile.in *.la -spot.py* +spot_impl.py* buddy.py* *.lo *.loT diff --git a/wrap/python/Makefile.am b/wrap/python/Makefile.am index 572a1c142..68a84a48a 100644 --- a/wrap/python/Makefile.am +++ b/wrap/python/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et Development de +## Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et Development de ## l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -25,25 +25,25 @@ SUBDIRS = . ajax tests AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src -I$(top_builddir)/src \ $(BUDDY_CPPFLAGS) -DSWIG_TYPE_TABLE=spot -EXTRA_DIST = spot.i buddy.i -python_PYTHON = $(srcdir)/spot.py $(srcdir)/buddy.py -pyexec_LTLIBRARIES = _spot.la _buddy.la +EXTRA_DIST = spot_impl.i buddy.i +python_PYTHON = $(srcdir)/spot_impl.py $(srcdir)/buddy.py spot.py +pyexec_LTLIBRARIES = _spot_impl.la _buddy.la MAINTAINERCLEANFILES = \ - $(srcdir)/spot_wrap.cxx $(srcdir)/spot.py \ + $(srcdir)/spot_impl_wrap.cxx $(srcdir)/spot_impl.py \ $(srcdir)/buddy_wrap.cxx $(srcdir)/buddy.py ## spot -_spot_la_SOURCES = $(srcdir)/spot_wrap.cxx $(srcdir)/spot_wrap.h -_spot_la_LDFLAGS = -avoid-version -module -_spot_la_LIBADD = $(top_builddir)/src/libspot.la +_spot_impl_la_SOURCES = $(srcdir)/spot_impl_wrap.cxx $(srcdir)/spot_impl_wrap.h +_spot_impl_la_LDFLAGS = -avoid-version -module +_spot_impl_la_LIBADD = $(top_builddir)/src/libspot.la -$(srcdir)/spot_wrap.cxx: $(srcdir)/spot.i - $(SWIG) -c++ -python -I$(srcdir) -I$(top_srcdir)/src $(srcdir)/spot.i +$(srcdir)/spot_impl_wrap.cxx: $(srcdir)/spot_impl.i + $(SWIG) -c++ -python -I$(srcdir) -I$(top_srcdir)/src $(srcdir)/spot_impl.i -$(srcdir)/spot.py: $(srcdir)/spot.i - $(MAKE) $(AM_MAKEFLAGS) spot_wrap.cxx +$(srcdir)/spot_impl.py: $(srcdir)/spot_impl.i + $(MAKE) $(AM_MAKEFLAGS) spot_impl_wrap.cxx ## buddy diff --git a/wrap/python/spot.py b/wrap/python/spot.py new file mode 100644 index 000000000..92e411383 --- /dev/null +++ b/wrap/python/spot.py @@ -0,0 +1,227 @@ +# -*- coding: utf-8 -*- +# Copyright (C) 2014 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +from spot_impl import * +import subprocess +import sys + +_bdd_dict = make_bdd_dict() + +def render_automaton_as_svg(a): + dotsrc = ostringstream() + dotty_reachable(dotsrc, a) + dotty = subprocess.Popen(['dot', '-Tsvg'], + stdin=subprocess.PIPE, + stdout=subprocess.PIPE) + dotty.stdin.write(dotsrc.str().encode('utf-8')) + res = dotty.communicate() + return res[0].decode('utf-8') + +tgba._repr_svg_ = render_automaton_as_svg + +def formula_str_ctor(self, str): + self.this = parse_formula(str) + +formula.__init__ = formula_str_ctor + +def tgba_str_ctor(self, str): + self.this = ltl_to_tgba_fm(parse_formula(str), _bdd_dict) + +tgba.__init__ = tgba_str_ctor + +# Wrapper around a formula iterator to which we add some methods of formula +# (using _addfilter and _addmap), so that we can write things like +# formulas.simplify().is_X_free(). +class formulaiterator: + def __init__(self, formulas): + self._formulas = formulas + + def __iter__(self): + return self + + def __next__(self): + return next(self._formulas) + +# fun shoud be a predicate and should be a method of formula. +# _addfilter adds this predicate as a filter whith the same name in +# formulaiterator. +def _addfilter(fun): + def filtf(self, *args, **kwargs): + it = filter(lambda f: getattr(f, fun)(*args, **kwargs), self) + return formulaiterator(it) + def nfiltf(self, *args, **kwargs): + it = filter(lambda f: not getattr(f, fun)(*args, **kwargs), self) + return formulaiterator(it) + setattr(formulaiterator, fun, filtf) + if fun[:3] == 'is_': + notfun = fun[:3] + 'not_' + fun[3:] + elif fun[:4] == 'has_': + notfun = fun[:4] + 'no_' + fun[4:] + else: + notfun = 'not_' + fun + setattr(formulaiterator, fun, filtf) + setattr(formulaiterator, notfun, nfiltf) + +# fun should be a function taking a formula as its first parameter and returning +# a formula. +# _addmap adds this function as a method of formula and formulaiterator. +def _addmap(fun): + def mapf(self, *args, **kwargs): + return formulaiterator(map(lambda f: getattr(f, fun)(*args, **kwargs), +self)) + setattr(formula, fun, lambda self, *args, **kwargs: globals()[fun](self, + *args, **kwargs)) + setattr(formulaiterator, fun, mapf) + +def randltl(ap, n = -1, **kwargs): + """Generate random formulas. + + Returns a random formula iterator. + + ap: the number of atomic propositions used to generate random formulas. + + n: number of formulas to generate, or unbounded if n < 0. + + **kwargs: + seed: seed for the random number generator (0). + output: can be 'ltl', 'psl', 'bool' or 'sere' ('ltl'). + allow_dups: allow duplicate formulas (False). + tree_size: tree size of the formulas generated, before mandatory + simplifications (15) + boolean_priorities: set priorities for Boolean formulas. + ltl_priorities: set priorities for LTL formulas. + sere_priorities: set priorities for SERE formulas. + dump_priorities: show current priorities, do not generate any formula. + simplify: + 0 No rewriting + 1 basic rewritings and eventual/universal rules + 2 additional syntactic implication rules + 3 (default) better implications using containment + """ + opts = option_map() + output_map = { + "ltl" : OUTPUTLTL, + "psl" : OUTPUTPSL, + "bool" : OUTPUTBOOL, + "sere" : OUTPUTSERE + } + + if isinstance(ap, list): + aprops = atomic_prop_set() + e = default_environment.instance() + for elt in ap: + aprops.insert(is_atomic_prop(e.require(elt))) + ap = aprops + ltl_priorities = kwargs.get("ltl_priorities", None) + sere_priorities = kwargs.get("sere_priorities", None) + boolean_priorities = kwargs.get("boolean_priorities", None) + output = output_map[kwargs.get("output", "ltl")] + opts.set("output", output) + opts.set("seed", kwargs.get("seed", 0)) + tree_size = kwargs.get("tree_size", 15) + if isinstance(tree_size, tuple): + tree_size_min, tree_size_max = tree_size + else: + tree_size_min = tree_size_max = tree_size + opts.set("tree_size_min", tree_size_min) + opts.set("tree_size_max", tree_size_max) + opts.set("unique", not kwargs.get("allow_dups", False)) + opts.set("wf", kwargs.get("weak_fairness", False)) + simpl_level = kwargs.get("simplify", 0) + if simpl_level > 3 or simpl_level < 0: + sys.stderr.write('invalid simplification level: ' + simpl_level) + return + opts.set("simplification_level", simpl_level) + + rg = randltlgenerator(ap, opts, ltl_priorities, sere_priorities, + boolean_priorities) + + dump_priorities = kwargs.get("dump_priorities", False) + if dump_priorities: + dumpstream = ostringstream() + if output == OUTPUTLTL: + print('Use argument ltl_priorities=STRING to set the following ' \ + 'LTL priorities:\n') + rg.dump_ltl_priorities(dumpstream) + print(dumpstream.str()) + elif output == OUTPUTBOOL: + print('Use argument boolean_priorities=STRING to set the ' \ + 'following Boolean formula priorities:\n') + rg.dump_bool_priorities(dumpstream) + print(dumpstream.str()) + elif output == OUTPUTPSL or output == OUTPUTSERE: + if output != OUTPUTSERE: + print('Use argument ltl_priorities=STRING to set the following ' \ + 'LTL priorities:\n') + rg.dump_psl_priorities(dumpstream) + print(dumpstream.str()) + print('Use argument sere_priorities=STRING to set the following ' \ + 'SERE priorities:\n') + rg.dump_sere_priorities(dumpstream) + print(dumpstream.str()) + print('Use argument boolean_priorities=STRING to set the ' \ + 'following Boolean formula priorities:\n') + rg.dump_sere_bool_priorities(dumpstream) + print(dumpstream.str()) + else: + sys.stderr.write("internal error: unknown type of output") + return + + def _randltlgenerator(rg): + i = 0 + while i != n: + f = rg.next() + if f is None: + sys.stderr.write("Warning: could not generate a new unique formula " \ + "after " + str(MAX_TRIALS) + " trials.\n") + yield None + else: + yield f + i += 1 + return formulaiterator(_randltlgenerator(rg)) + +def simplify(f, **kwargs): + level = kwargs.get('level', None) + if level is not None: + return ltl_simplifier(ltl_simplifier_options(level)).simplify(f) + + basics = kwargs.get('basics', True) + synt_impl = kwargs.get('synt_impl', True) + event_univ = kwargs.get('event_univ', True) + containment_checks = kwargs.get('containment_checks', False) + containment_checks_stronger = kwargs.get('containment_checks_stronger', False) + nenoform_stop_on_boolean = kwargs.get('nenoform_stop_on_boolean', False) + reduce_size_strictly = kwargs.get('reduce_size_strictly', False) + boolean_to_isop = kwargs.get('boolean_to_isop', False) + favor_event_univ = kwargs.get('favor_event_univ', False) + + simp_opts = ltl_simplifier_options(basics, synt_impl, event_univ, + containment_checks, containment_checks_stronger, nenoform_stop_on_boolean, + reduce_size_strictly, boolean_to_isop, favor_event_univ) + + return ltl_simplifier(simp_opts).simplify(f) + +for fun in dir(formula): + if callable(getattr(formula, fun)) and fun[:3] == 'is_' \ +or fun[:4] == 'has_': + _addfilter(fun) + +for fun in ['remove_x', 'get_literal', 'relabel', 'relabel_bse', +'simplify', 'unabbreviate_ltl']: + _addmap(fun) diff --git a/wrap/python/spot.i b/wrap/python/spot_impl.i similarity index 92% rename from wrap/python/spot.i rename to wrap/python/spot_impl.i index d61c5d3f0..5a9908d4d 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot_impl.i @@ -26,11 +26,12 @@ #include %} -%module(directors="1") spot +%module(directors="1") spot_impl %include "std_shared_ptr.i" %include "std_string.i" %include "std_list.i" +%include "std_set.i" %include "exception.i" // git grep 'typedef.*std::shared_ptr' | grep -v const | @@ -93,6 +94,7 @@ namespace std { #include "tgba/bdddict.hh" +#include "ltlvisit/apcollect.hh" #include "ltlvisit/dotty.hh" #include "ltlvisit/dump.hh" #include "ltlvisit/lunabbrev.hh" @@ -100,8 +102,11 @@ namespace std { #include "ltlvisit/simplify.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" -#include "ltlvisit/apcollect.hh" #include "ltlvisit/lbt.hh" +#include "ltlvisit/randomltl.hh" +#include "ltlvisit/length.hh" +#include "ltlvisit/remove_x.hh" +#include "ltlvisit/relabel.hh" #include "tgba/bddprint.hh" #include "tgba/fwd.hh" @@ -129,6 +134,7 @@ namespace std { #include "tgbaalgos/simulation.hh" #include "tgbaalgos/postproc.hh" #include "tgbaalgos/stutter.hh" +#include "tgbaalgos/translate.hh" #include "hoaparse/public.hh" @@ -168,10 +174,10 @@ using namespace spot; PyList_Append($result,obj); Py_DECREF(obj); } + }; %apply char** OUTPUT { char** err }; - %exception { try { $action @@ -182,6 +188,12 @@ using namespace spot; er += e.what(); SWIG_exception(SWIG_SyntaxError, er.c_str()); } + catch (const std::invalid_argument& e) + { + std::string er("\n"); + er += e.what(); + SWIG_exception(SWIG_ValueError, er.c_str()); + } } // False and True cannot be redefined in Python3, even in a class. @@ -210,6 +222,7 @@ using namespace spot; %include "tgba/bdddict.hh" +%include "ltlvisit/apcollect.hh" %include "ltlvisit/dotty.hh" %include "ltlvisit/dump.hh" %include "ltlvisit/lunabbrev.hh" @@ -218,6 +231,10 @@ using namespace spot; %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" %include "ltlvisit/lbt.hh" +%include "ltlvisit/randomltl.hh" +%include "ltlvisit/length.hh" +%include "ltlvisit/remove_x.hh" +%include "ltlvisit/relabel.hh" // Help SWIG with namespace lookups. #define ltl spot::ltl @@ -238,7 +255,6 @@ namespace spot { } // Should come after the definition of tgba_digraph -%include "ltlvisit/apcollect.hh" %include "tgbaalgos/degen.hh" %include "tgbaalgos/dotty.hh" @@ -259,6 +275,7 @@ namespace spot { %include "tgbaalgos/simulation.hh" %include "tgbaalgos/postproc.hh" %include "tgbaalgos/stutter.hh" +%include "tgbaalgos/translate.hh" %include "hoaparse/public.hh" @@ -272,9 +289,23 @@ namespace spot { %include "taalgos/minimize.hh" - #undef ltl + +namespace std { + %template(atomic_prop_set) set; +} + +%{ + namespace swig { + template <> struct traits { + typedef pointer_category category; + static const char* type_name() { return"atomic_prop const *"; } + }; + } +%} + %extend spot::ltl::formula { // When comparing formula, make sure Python compare our @@ -323,22 +354,6 @@ namespace std { }; } -%pythoncode %{ -import subprocess - -def render_automaton_as_svg(a): - dotsrc = ostringstream() - dotty_reachable(dotsrc, a) - dotty = subprocess.Popen(['dot', '-Tsvg'], - stdin=subprocess.PIPE, - stdout=subprocess.PIPE) - dotty.stdin.write(dotsrc.str().encode('utf-8')) - res = dotty.communicate() - return res[0].decode('utf-8') - -tgba._repr_svg_ = render_automaton_as_svg -%} - %inline %{ spot::ltl::parse_error_list empty_parse_error_list() diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index fe7a52251..1f28a8b45 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2010, 2012, 2013 Labortatoire de Recherche et Développement de +## Copyright (C) 2010, 2012, 2013, 2014 Labortatoire de Recherche et Développement de ## l'EPITA. ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -21,7 +21,8 @@ EXTRA_DIST = \ $(TESTS) \ - ltl2tgba.py + ltl2tgba.py \ + ipnbdoctest.py LOG_COMPILER = ./run LOG_DRIVER = $(TEST_LOG_DRIVER) @@ -39,4 +40,5 @@ TESTS = \ minato.py \ optionmap.py \ parsetgba.py \ + randltl.ipynb \ setxor.py diff --git a/wrap/python/tests/bddnqueen.py b/wrap/python/tests/bddnqueen.py index 22807e978..c336bf2ce 100755 --- a/wrap/python/tests/bddnqueen.py +++ b/wrap/python/tests/bddnqueen.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +# Copyright (C) 2010, 2011, 2012, 2014 Laboratoire de Recherche et # Développement de l'EPITA. # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -25,7 +25,6 @@ import sys from buddy import * -from spot import nl_cout # Build the requirements for all other fields than (i,j) assuming # that (i,j) has a queen. @@ -96,6 +95,9 @@ sys.stdout.write("There are %d solutions, one is:\n" % bdd_satcount(queen)) solution = bdd_satone(queen) bdd_printset(solution) + +from spot import nl_cout + nl_cout() # Cleanup all BDD variables before calling bdd_done(), otherwise diff --git a/wrap/python/tests/ipnbdoctest.py b/wrap/python/tests/ipnbdoctest.py new file mode 100755 index 000000000..bfe3e897a --- /dev/null +++ b/wrap/python/tests/ipnbdoctest.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python +""" +simple example script for running and testing notebooks. + +Usage: `ipnbdoctest.py foo.ipynb [bar.ipynb [...]]` + +Each cell is submitted to the kernel, and the outputs are compared with those stored in the notebook. +""" + +from __future__ import print_function + +import os,sys,time +import base64 +import re +from difflib import unified_diff as diff + +from collections import defaultdict +try: + from queue import Empty +except ImportError: + print('Python 3.x is needed to run this script.') + sys.exit(77) + +try: + from IPython.kernel import KernelManager +except ImportError: + from IPython.zmq.blockingkernelmanager import BlockingKernelManager as KernelManager + +from IPython.nbformat.current import reads, NotebookNode + + +def compare_png(a64, b64): + """compare two b64 PNGs (incomplete)""" + try: + import Image + except ImportError: + pass + adata = base64.decodestring(a64) + bdata = base64.decodestring(b64) + return True + +def sanitize(s): + """sanitize a string for comparison. + + fix universal newlines, strip trailing newlines, and normalize likely random values (memory addresses and UUIDs) + """ + if not isinstance(s, str): + return s + # normalize newline: + s = s.replace('\r\n', '\n') + + # ignore trailing newlines (but not space) + s = s.rstrip('\n') + + # normalize hex addresses: + s = re.sub(r'0x[a-f0-9]+', '0xFFFFFFFF', s) + + # normalize UUIDs: + s = re.sub(r'[a-f0-9]{8}(\-[a-f0-9]{4}){3}\-[a-f0-9]{12}', 'U-U-I-D', s) + + return s + + +def consolidate_outputs(outputs): + """consolidate outputs into a summary dict (incomplete)""" + data = defaultdict(list) + data['stdout'] = '' + data['stderr'] = '' + + for out in outputs: + if out.type == 'stream': + data[out.stream] += out.text + elif out.type == 'pyerr': + data['pyerr'] = dict(ename=out.ename, evalue=out.evalue) + else: + for key in ('png', 'svg', 'latex', 'html', 'javascript', 'text', 'jpeg',): + if key in out: + data[key].append(out[key]) + return data + + +def compare_outputs(test, ref, skip_compare=('png', 'traceback', 'latex', 'prompt_number')): + for key in ref: + if key not in test: + print("missing key: %s != %s" % (test.keys(), ref.keys())) + return False + elif key not in skip_compare and sanitize(test[key]) != sanitize(ref[key]): + print("mismatch %s:" % key) + exp = ref[key] + eff = test[key] + if exp[:-1] != '\n': + exp += '\n' + if eff[:-1] != '\n': + eff += '\n' + print(''.join(diff(exp.splitlines(1), eff.splitlines(1), + fromfile='expected', tofile='effective'))) + return False + return True + + +def run_cell(shell, iopub, cell): + # print cell.input + shell.execute(cell.input) + # wait for finish, maximum 20s + shell.get_msg(timeout=20) + outs = [] + + while True: + try: + msg = iopub.get_msg(timeout=0.2) + except Empty: + break + msg_type = msg['msg_type'] + if msg_type in ('status', 'pyin'): + continue + elif msg_type == 'clear_output': + outs = [] + continue + + content = msg['content'] + # print msg_type, content + out = NotebookNode(output_type=msg_type) + + if msg_type == 'stream': + out.stream = content['name'] + out.text = content['data'] + elif msg_type in ('display_data', 'pyout'): + out['metadata'] = content['metadata'] + for mime, data in content['data'].items(): + attr = mime.split('/')[-1].lower() + # this gets most right, but fix svg+html, plain + attr = attr.replace('+xml', '').replace('plain', 'text') + setattr(out, attr, data) + if msg_type == 'pyout': + out.prompt_number = content['execution_count'] + elif msg_type == 'pyerr': + out.ename = content['ename'] + out.evalue = content['evalue'] + out.traceback = content['traceback'] + else: + print("unhandled iopub msg:", msg_type) + + outs.append(out) + return outs + + +def test_notebook(nb): + km = KernelManager() + km.start_kernel(extra_arguments=['--pylab=inline'], stderr=open(os.devnull, 'w')) + try: + kc = km.client() + kc.start_channels() + iopub = kc.iopub_channel + except AttributeError: + # IPython 0.13 + kc = km + kc.start_channels() + iopub = kc.sub_channel + shell = kc.shell_channel + + # run %pylab inline, because some notebooks assume this + # even though they shouldn't + shell.execute("pass") + shell.get_msg() + while True: + try: + iopub.get_msg(timeout=1) + except Empty: + break + + successes = 0 + failures = 0 + errors = 0 + for ws in nb.worksheets: + for i, cell in enumerate(ws.cells): + if cell.cell_type != 'code': + continue + try: + outs = run_cell(shell, iopub, cell) + except Exception as e: + print("failed to run cell:", repr(e)) + print(cell.input) + errors += 1 + continue + + failed = False + if len(outs) != len(cell.outputs): + print("output length mismatch (expected {}, got {})".format( + len(cell.outputs), len(outs))) + failed = True + for out, ref in zip(outs, cell.outputs): + if not compare_outputs(out, ref): + failed = True + print("cell %d: " % i, end="") + if failed: + print("FAIL") + failures += 1 + else: + print("OK") + successes += 1 + + print() + print("tested notebook %s" % nb.metadata.name) + print(" %3i cells successfully replicated" % successes) + if failures: + print(" %3i cells mismatched output" % failures) + if errors: + print(" %3i cells failed to complete" % errors) + kc.stop_channels() + km.shutdown_kernel() + del km + if failures | errors: + sys.exit(1) + +if __name__ == '__main__': + for ipynb in sys.argv[1:]: + print("testing %s" % ipynb) + with open(ipynb) as f: + nb = reads(f.read(), 'json') + test_notebook(nb) diff --git a/wrap/python/tests/minato.py b/wrap/python/tests/minato.py index 989bcce4f..ead000fcc 100755 --- a/wrap/python/tests/minato.py +++ b/wrap/python/tests/minato.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et +# Développement de l'Epita # Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -20,7 +20,6 @@ # You should have received a copy of the GNU General Public License # along with this program. If not, see . -import spot import buddy import sys @@ -33,6 +32,8 @@ c = buddy.bdd_ithvar(2) w = -a & -b | -c & b | a & -b +import spot + isop = spot.minato_isop(w) i = isop.next() diff --git a/wrap/python/tests/randltl.ipynb b/wrap/python/tests/randltl.ipynb new file mode 100644 index 000000000..4c36a574b --- /dev/null +++ b/wrap/python/tests/randltl.ipynb @@ -0,0 +1,632 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:b16de2c9883c0fecb450f9d7f4885937abcfc1d1fef584d47109fcee13a68c9a" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "heading", + "level": 1, + "metadata": {}, + "source": [ + "Documentation for spot's randltl python binding" + ] + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "import spot" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "heading", + "level": 2, + "metadata": {}, + "source": [ + "Basic usage" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Generate random formulas from specified atomic propositions:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(['a', 'b', 'c'])\n", + "for i in range(3):\n", + " print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "0 R b\n", + "F(XG(F!b M Fb) W (b R a))\n" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Generate random formulas using 3 atomic propositions:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3)\n", + "for i in range(3):\n", + " print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "0 R p1\n", + "F(XG(F!p1 M Fp1) W (p1 R p0))\n" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "By default, there is no limit to the number of formulas generated.
\n", + "To specify a number of formulas:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, 4)\n", + "for formula in f:\n", + " print(formula)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "0 R p1\n", + "F(XG(F!p1 M Fp1) W (p1 R p0))\n", + "F(p0 R !p2)\n" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "heading", + "level": 2, + "metadata": {}, + "source": [ + "Keyword arguments" + ] + }, + { + "cell_type": "heading", + "level": 2, + "metadata": {}, + "source": [ + "seed" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Seed for the pseudo random number generator (default: 0)." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, seed=11)\n", + "print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "G(p1 U Gp0)\n" + ] + } + ], + "prompt_number": 12 + }, + { + "cell_type": "heading", + "level": 3, + "metadata": {}, + "source": [ + "output" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Type of formulas to output: 'ltl', 'psl', 'bool' or 'sere' (default: 'ltl')." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, output='psl', seed=332)\n", + "print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "{{p0 && p2}[*]}<>-> (Fp2 & Fp0)\n" + ] + } + ], + "prompt_number": 26 + }, + { + "cell_type": "heading", + "level": 3, + "metadata": {}, + "source": [ + "allow_dups" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Allow duplicate formulas (default: False)." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(1, allow_dups=True)\n", + "print(next(f))\n", + "print(next(f))\n", + "print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "0\n", + "Fp0\n" + ] + } + ], + "prompt_number": 27 + }, + { + "cell_type": "heading", + "level": 3, + "metadata": {}, + "source": [ + "tree_size" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Tree size of the formulas generated, before mandatory simplifications (default: 15)." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, tree_size=30, seed=11)\n", + "print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "G(((p0 U !Xp2) M Gp2) U Gp0)\n" + ] + } + ], + "prompt_number": 29 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "A range can be specified as a tuple:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, tree_size=(1, 40))\n", + "print(next(f))\n", + "print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "X!(Gp2 M p1) R (!p1 M Xp2)\n", + "F(G(F(Gp0 R (1 U Fp1)) M (p1 -> Gp0)) M F((p0 | Fp0) W Gp1))\n" + ] + } + ], + "prompt_number": 30 + }, + { + "cell_type": "heading", + "level": 3, + "metadata": {}, + "source": [ + "boolean_priorities, ltl_priorities, sere_priorities, dump_priorities" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, output='bool', boolean_priorities='and=10,or=0')\n", + "for i in range(5):\n", + " print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "!p1 & (p1 <-> p2)\n", + "p1\n", + "p0 & ((p1 & p2) <-> !(!p0 & p1 & p2))\n", + "1\n" + ] + } + ], + "prompt_number": 31 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To see which operators are available along with their default priorities:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.randltl(3, output='psl', dump_priorities=True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "Use argument ltl_priorities=STRING to set the following LTL priorities:\n", + "\n", + "ap\t3\n", + "false\t1\n", + "true\t1\n", + "not\t1\n", + "F\t1\n", + "G\t1\n", + "X\t1\n", + "Closure\t1\n", + "equiv\t1\n", + "implies\t1\n", + "xor\t1\n", + "R\t1\n", + "U\t1\n", + "W\t1\n", + "M\t1\n", + "and\t1\n", + "or\t1\n", + "EConcat\t1\n", + "UConcat\t1\n", + "\n", + "Use argument sere_priorities=STRING to set the following SERE priorities:\n", + "\n", + "ap\t3\n", + "false\t1\n", + "true\t1\n", + "not\t1\n", + "F\t1\n", + "G\t1\n", + "X\t1\n", + "Closure\t1\n", + "equiv\t1\n", + "implies\t1\n", + "xor\t1\n", + "R\t1\n", + "U\t1\n", + "W\t1\n", + "M\t1\n", + "and\t1\n", + "or\t1\n", + "EConcat\t1\n", + "UConcat\t1\n", + "eword\t1\n", + "boolform\t1\n", + "star\t1\n", + "star_b\t1\n", + "fstar\t1\n", + "fstar_b\t1\n", + "and\t1\n", + "andNLM\t1\n", + "or\t1\n", + "concat\t1\n", + "fusion\t1\n", + "\n", + "Use argument boolean_priorities=STRING to set the following Boolean formula priorities:\n", + "\n", + "ap\t3\n", + "false\t1\n", + "true\t1\n", + "not\t1\n", + "F\t1\n", + "G\t1\n", + "X\t1\n", + "Closure\t1\n", + "equiv\t1\n", + "implies\t1\n", + "xor\t1\n", + "R\t1\n", + "U\t1\n", + "W\t1\n", + "M\t1\n", + "and\t1\n", + "or\t1\n", + "EConcat\t1\n", + "UConcat\t1\n", + "eword\t1\n", + "boolform\t1\n", + "star\t1\n", + "star_b\t1\n", + "fstar\t1\n", + "fstar_b\t1\n", + "and\t1\n", + "andNLM\t1\n", + "or\t1\n", + "concat\t1\n", + "fusion\t1\n", + "ap\t3\n", + "false\t1\n", + "true\t1\n", + "not\t1\n", + "equiv\t1\n", + "implies\t1\n", + "xor\t1\n", + "and\t1\n", + "or\t1\n", + "\n" + ] + } + ], + "prompt_number": 32 + }, + { + "cell_type": "heading", + "level": 3, + "metadata": {}, + "source": [ + "simplify" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "0 No rewriting
\n", + "1 basic rewritings and eventual/universal rules
\n", + "2 additional syntactic implication rules
\n", + "3 better implications using containment
\n", + "default: 3" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, simplify=0, seed=5)\n", + "print(next(f))\n", + "f = spot.randltl(3, simplify=3, seed=5)\n", + "print(next(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "G!(!p2 & (Xp1 | F(p0 R Xp1)))\n", + "G(p2 | (X!p1 & G(!p0 U X!p1)))\n" + ] + } + ], + "prompt_number": 36 + }, + { + "cell_type": "heading", + "level": 2, + "metadata": {}, + "source": [ + "Filters and maps" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "most boolean functions found in the class formula can be used to filter the random formula generator like this:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, 20).is_syntactic_stutter_invariant()\n", + "for formula in f:\n", + " print(formula)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "0 R p1\n", + "F(p0 R !p2)\n", + "G(p0 | Fp1) W (FGp1 R !p1)\n", + "(p1 R G!p2) | G(p1 U !p0)\n", + "(p1 W p0) U p1\n", + "F!G(!Gp2 W p2)\n", + "G!p2 & (!((p1 & Fp2) M p2) U p2)\n" + ] + } + ], + "prompt_number": 40 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "likewise, functions from formula to formula can be applied to map the iterator:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(2, 6).remove_x()\n", + "for formula in f:\n", + " print(formula)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "!(F!p1 M 1)\n", + "(Fp1 | Gp0) M 1\n", + "F!(!p1 <-> FGp1)\n", + "Gp1 U (p1 U GFp1)\n", + "(!p1 U p1) U ((p0 & (p0 U (!p0 & (!p0 -> Fp1))) & ((p1 U !p0) | (!p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p0 -> Fp1))) & ((!p1 U p0) | (p1 U p0))) | (p1 & (p1 U (!p1 & (!p0 -> Fp1))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p0 -> Fp1))) & ((!p0 U p1) | (p0 U p1))) | ((!p0 -> Fp1) & (Gp0 | G!p0) & (Gp1 | G!p1)))\n" + ] + } + ], + "prompt_number": 42 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "You may have noticed that the return type of randltl is 'formulaiterator'.
\n", + "Since the boolean functions and the 'mapping' functions return an iterator of the same type, this means these operations can be chained like this:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.randltl(3, 20).is_syntactic_stutter_invariant().relabel(spot.Abc).simplify()\n", + "for formula in f:\n", + " print(formula)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0\n", + "Ga\n", + "F(a R !b)\n", + "G(a | Fb) | (FGb R !b)\n", + "G!b | G(a U !c)\n", + "b U a\n", + "0\n", + "0\n" + ] + } + ], + "prompt_number": 44 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [] + } + ], + "metadata": {} + } + ] +} \ No newline at end of file diff --git a/wrap/python/tests/run.in b/wrap/python/tests/run.in index 87bfecb42..a6d07c956 100644 --- a/wrap/python/tests/run.in +++ b/wrap/python/tests/run.in @@ -1,9 +1,9 @@ #!/bin/sh - -# Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement de -# l'EPITA (LRDE). +# -*- coding: utf-8 -*- +# Copyright (C) 2010, 2011, 2014, 2015 Laboratoire de Recherche et +# Developpement de l'EPITA (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 -# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université # Pierre et Marie Curie. # # This file is part of Spot, a model checking library. @@ -36,11 +36,14 @@ test -z "$1" && PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@ case $1 in + *.ipynb) + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ + exec @PYTHON@ @srcdir@/ipnbdoctest.py "$@";; *.py) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@ "$@";; *.test) exec sh -x "$@";; - ipython*) + *python*) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec "$@";; *) echo "Unknown extension" >&2 -- GitLab