From fe2fc88fc6577d2eec09bc5dd1f842d910299d8c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 10 May 2015 16:30:12 +0200 Subject: [PATCH] bin: add a --check option for automata outputs This currently only allows extra check for stutter invariance. * src/bin/common_aoutput.cc: Add check option, and test stutter invariance. * src/twaalgos/stutter.cc, src/twaalgos/stutter.hh (check_stutter_invariance): New function. * src/tests/stutter-tgba.test: Test it. --- src/bin/common_aoutput.cc | 42 +++++++++++++++++++++++++++++++++++++ src/tests/stutter-tgba.test | 7 +++++++ src/twaalgos/stutter.cc | 34 ++++++++++++++++++++++++++++++ src/twaalgos/stutter.hh | 9 ++++++++ 4 files changed, 92 insertions(+) diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 7ae9172cc..f29a127be 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -19,6 +19,7 @@ #include "common_sys.hh" #include "error.h" +#include "argmatch.h" #include "common_aoutput.hh" #include "common_post.hh" @@ -31,6 +32,7 @@ #include "twaalgos/lbtt.hh" #include "twaalgos/hoa.hh" #include "twaalgos/neverclaim.hh" +#include "twaalgos/stutter.hh" automaton_format_t automaton_format = Dot; static const char* opt_dot = nullptr; @@ -39,12 +41,35 @@ static const char* hoa_opt = nullptr; const char* opt_name = nullptr; static const char* opt_output = nullptr; static const char* stats = ""; +enum check_type + { + check_stutter = (1 << 0), + check_all = -1U, + }; +static char const *const check_args[] = + { + "stutter-invariant", "stuttering-invariant", + "stutter-insensitive", "stuttering-insensitive", + "stutter-sensitive", "stuttering-sensitive", + "all", + 0 + }; +static check_type const check_types[] = + { + check_stutter, check_stutter, + check_stutter, check_stutter, + check_stutter, check_stutter, + check_all + }; +ARGMATCH_VERIFY(check_args, check_types); +unsigned opt_check = 0U; enum { OPT_DOT = 1, OPT_LBTT, OPT_NAME, OPT_STATS, + OPT_CHECK, }; static const argp_option options[] = @@ -88,6 +113,10 @@ static const argp_option options[] = "(ignored with --lbtt or --spin)", 0 }, { "stats", OPT_STATS, "FORMAT", 0, "output statistics about the automaton", 0 }, + { "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL, + "test for the additional property PROP and output the result " + "in the HOA format (implies -H). PROP may be any prefix of " + "'all' (default), or 'stutter-invariant'.", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -190,6 +219,13 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) case 'o': opt_output = arg; break; + case OPT_CHECK: + automaton_format = Hoa; + if (arg) + opt_check |= XARGMATCH("--check", arg, check_args, check_types); + else + opt_check |= check_all; + break; case OPT_DOT: automaton_format = Dot; opt_dot = arg; @@ -244,6 +280,12 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, double time, const spot::const_hoa_aut_ptr& haut) { + if (opt_check) + { + if (opt_check & check_stutter) + check_stutter_invariance(aut, f); + } + // Name the output automaton. if (opt_name) { diff --git a/src/tests/stutter-tgba.test b/src/tests/stutter-tgba.test index f91caa53a..dd3f69d03 100755 --- a/src/tests/stutter-tgba.test +++ b/src/tests/stutter-tgba.test @@ -70,4 +70,11 @@ State: 2 --END-- EOF +run 0 $ltl2tgba -H 'F(a & X(!a & b))' > input +grep stutter-invariant input && exit 1 +run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2 +grep stutter-invariant input.2 +run 0 $autfilt --check=stutter input > input.2 +grep stutter-invariant input.2 + diff output expected diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index a9cec6ed8..098108538 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -29,6 +29,8 @@ #include "ltlvisit/remove_x.hh" #include "twaalgos/product.hh" #include "twaalgos/ltl2tgba_fm.hh" +#include "twaalgos/isdet.hh" +#include "twaalgos/dtgbacomp.hh" #include "twa/twaproduct.hh" #include "twa/bddprint.hh" #include @@ -637,4 +639,36 @@ namespace spot SPOT_UNREACHABLE(); } } + + bool + check_stutter_invariance(const twa_graph_ptr& aut, const ltl::formula* f) + { + bool is_stut = aut->is_stutter_invariant(); + if (is_stut) + return is_stut; + + twa_graph_ptr neg = nullptr; + if (f) + { + auto* nf = ltl::unop::instance(ltl::unop::Not, f->clone()); + neg = translator(aut->get_dict()).run(nf); + nf->destroy(); + } + else + { + // If the automaton is deterministic, we + // know how to complement it. + aut->prop_deterministic(is_deterministic(aut)); + if (!aut->is_deterministic()) + return false; + + neg = dtgba_complement(aut); + } + + is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), + std::move(neg), get_all_ap(aut)); + if (is_stut) + aut->prop_stutter_invariant(is_stut); + return is_stut; + } } diff --git a/src/twaalgos/stutter.hh b/src/twaalgos/stutter.hh index 6c20dff84..487f176a6 100644 --- a/src/twaalgos/stutter.hh +++ b/src/twaalgos/stutter.hh @@ -57,4 +57,13 @@ namespace spot is_stutter_invariant(twa_graph_ptr&& aut_f, twa_graph_ptr&& aut_nf, bdd aps, int algo = 0); + + /// \brief Check whether \a aut is stutter-invariant + /// + /// This procedure only works if \a aut is deterministic, or if the + /// equivalent formula \a f is given. The stutter-invariant property + /// of the automaton is updated and also returned. + SPOT_API bool + check_stutter_invariance(const twa_graph_ptr& aut, + const ltl::formula* f = nullptr); }