From 51a75a316d2308dd5b82de73e386e124a26b5629 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Oct 2015 23:56:13 +0200 Subject: [PATCH] parseaut: Add a trust_hoa option. Fixes #114. * src/parseaut/public.hh: Add support for a trust_hoa option. * src/parseaut/parseaut.yy: If trust_hoa is set, recognize the "inherently-weak" and "stutter-invariant" properties. * src/bin/common_conv.cc, src/bin/common_conv.hh (read_automaton): Move... * src/bin/common_hoaread.cc, src/bin/common_hoaread.hh: ... in this new file, that also handle the --trust-hoa option. * src/bin/Makefile.am: Add them. * src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc: Use them. * src/tests/parseaut.test, src/tests/ltldo.test: Adjust, and test --trust-hoa=no. * src/tests/complement.test, src/tests/prodor.test, src/tests/sbacc.test: Adjust. * wrap/python/spot.py (automata): Add option trust_hoa. * NEWS: Update. --- NEWS | 24 ++++++++--- src/bin/Makefile.am | 2 + src/bin/autfilt.cc | 6 ++- src/bin/common_conv.cc | 12 ------ src/bin/common_conv.hh | 3 -- src/bin/common_hoaread.cc | 90 +++++++++++++++++++++++++++++++++++++++ src/bin/common_hoaread.hh | 34 +++++++++++++++ src/bin/dstar2tgba.cc | 4 +- src/bin/ltlcross.cc | 6 ++- src/bin/ltldo.cc | 6 ++- src/parseaut/parseaut.yy | 12 ++++++ src/parseaut/public.hh | 3 +- src/tests/complement.test | 4 +- src/tests/ltldo.test | 23 +++++++++- src/tests/parseaut.test | 16 ++++--- src/tests/prodor.test | 3 +- src/tests/sbacc.test | 2 +- wrap/python/spot.py | 9 +++- 18 files changed, 221 insertions(+), 38 deletions(-) create mode 100644 src/bin/common_hoaread.cc create mode 100644 src/bin/common_hoaread.hh diff --git a/NEWS b/NEWS index 9e9749541..844734f21 100644 --- a/NEWS +++ b/NEWS @@ -6,13 +6,17 @@ New in spot 1.99.4a (not yet released) It currently works only for deterministic automata. * By default, autfilt does not simplify automata (this has not - changed), as if the --low --any options where used. But now, if + changed), as if the --low --any options were used. But now, if one of --small, --deterministic, or --any is given, the optimization level automatically defaults to --high (unless specified otherwise). For symmetry, if one of --low, --medium, or - --high is given, thn the translation intent defaults to --small + --high is given, then the translation intent defaults to --small (unless specified otherwise). + * autfilt, dstar2tgba, ltlcross, and ltldo now trust the (supported) + automaton properties declared in any HOA file they read. This can + be disabled with option --trust-hoa=no. + * ltlgrind FILENAME[/COL] is now the same as ltlgrind -F FILENAME[/COL] for consistency with ltlfilt. @@ -39,6 +43,11 @@ New in spot 1.99.4a (not yet released) * The HOA parser will diagnose any version that is not v1, unless it looks like a subversion of v1 and no parse error was detected. + * The way to pass option to the automaton parser has been changed to + make it easier to introduct new options. One such new option is + "trust_hoa": when true (the default) supported properties declared + in HOA files are trusted even if they cannot be easily be verified. + * ltl_simplifier renamed to tl_simplifier. Python: @@ -53,9 +62,14 @@ New in spot 1.99.4a (not yet released) * spot.postprocess(aut, *options), or aut.postprocess(*options) simplify the use of the spot.postprocessor object. (Just like we have spot.translate() on top of spot.translator().) - * spot.automata() and spot.automaton() now have an optional - timeout argument to restrict the runtime of commands that - produce automata. + * spot.automata() and spot.automaton() now have additional + optional arguments: + - timeout: to restrict the runtime of commands that + produce automata + - trust_hoa: can be set to False to ignore HOA properties + that cannot be easily verified + - ignore_abort: can be set to False if you do not want to + skip automata ended with --ABORT--. Bugs fixed: diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 97ad1f8ee..0dc735be7 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -36,6 +36,8 @@ libcommon_a_SOURCES = \ common_file.hh \ common_finput.cc \ common_finput.hh \ + common_hoaread.cc \ + common_hoaread.hh \ common_output.cc \ common_output.hh \ common_post.cc \ diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index c890e2721..5bf4d6cd9 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -35,6 +35,7 @@ #include "common_range.hh" #include "common_post.hh" #include "common_conv.hh" +#include "common_hoaread.hh" #include "twaalgos/product.hh" #include "twaalgos/isdet.hh" @@ -58,7 +59,7 @@ #include "twaalgos/complement.hh" static const char argp_program_doc[] ="\ -Convert, transform, and filter Büchi automata.\v\ +Convert, transform, and filter omega-automata.\v\ Exit status:\n\ 0 if some automata were output\n\ 1 if no automata were output (no match)\n\ @@ -229,6 +230,7 @@ static const argp_option options[] = static const struct argp_child children[] = { + { &hoaread_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, { &aoutput_io_format_argp, 0, nullptr, 4 }, { &post_argp_disabled, 0, nullptr, 20 }, @@ -675,7 +677,7 @@ namespace process_file(const char* filename) { spot::parse_aut_error_list pel; - auto hp = spot::automaton_stream_parser(filename); + auto hp = spot::automaton_stream_parser(filename, opt_parse); int err = 0; diff --git a/src/bin/common_conv.cc b/src/bin/common_conv.cc index 8d9b3729e..4320e6b9a 100644 --- a/src/bin/common_conv.cc +++ b/src/bin/common_conv.cc @@ -20,7 +20,6 @@ #include "common_conv.hh" #include #include "error.h" -#include "parseaut/public.hh" int to_int(const char* s) @@ -70,17 +69,6 @@ to_probability(const char* s) return res; } -spot::twa_graph_ptr -read_automaton(const char* filename, spot::bdd_dict_ptr& dict) -{ - spot::parse_aut_error_list pel; - auto p = spot::parse_aut(filename, pel, dict); - if (spot::format_parse_aut_errors(std::cerr, filename, pel) - || !p || p->aborted) - error(2, 0, "failed to read automaton from %s", filename); - return std::move(p->aut); -} - std::vector to_longs(const char* arg) { diff --git a/src/bin/common_conv.hh b/src/bin/common_conv.hh index daf1e6139..43d7b4622 100644 --- a/src/bin/common_conv.hh +++ b/src/bin/common_conv.hh @@ -30,6 +30,3 @@ float to_probability(const char* s); // Parse the comma or space seperate string of numbers. std::vector to_longs(const char* s); - -spot::twa_graph_ptr -read_automaton(const char* filename, spot::bdd_dict_ptr& dict); diff --git a/src/bin/common_hoaread.cc b/src/bin/common_hoaread.cc new file mode 100644 index 000000000..37254cc54 --- /dev/null +++ b/src/bin/common_hoaread.cc @@ -0,0 +1,90 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 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 . + +#include "common_hoaread.hh" +#include "argmatch.h" +#include "error.h" + +enum + { + OPT_TRUST_HOA = 1, + }; + +static const argp_option options[] = +{ + { "trust-hoa", OPT_TRUST_HOA, "BOOL", 0, + "If False, properties listed in HOA files are ignored, " + "unless they can be easily verified. If True (the default) " + "any supported property is trusted.", 1 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } +}; + +spot::automaton_parser_options opt_parse; + +spot::twa_graph_ptr +read_automaton(const char* filename, spot::bdd_dict_ptr& dict) +{ + spot::parse_aut_error_list pel; + auto p = spot::parse_aut(filename, pel, dict, + spot::default_environment::instance(), + opt_parse); + if (spot::format_parse_aut_errors(std::cerr, filename, pel) + || !p || p->aborted) + error(2, 0, "failed to read automaton from %s", filename); + return std::move(p->aut); +} + +static bool parse_bool(const char* opt, const char* arg) +{ + enum bool_type { bool_false, bool_true }; + static char const *const bool_args[] = + { + "false", "no", "0", + "true", "yes", "1", + nullptr + }; + static bool_type const bool_types[] = + { + bool_false, bool_false, bool_false, + bool_true, bool_true, bool_true, + }; + ARGMATCH_VERIFY(bool_args, bool_types); + bool_type bt = XARGMATCH(opt, arg, bool_args, bool_types); + return bt == bool_true; +} + +static int +parse_opt_hoaread(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case OPT_TRUST_HOA: + opt_parse.trust_hoa = parse_bool("--trust-hoa", arg); + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + + +const struct argp hoaread_argp = { options, parse_opt_hoaread, + nullptr, nullptr, nullptr, + nullptr, nullptr }; diff --git a/src/bin/common_hoaread.hh b/src/bin/common_hoaread.hh new file mode 100644 index 000000000..9a3654a9f --- /dev/null +++ b/src/bin/common_hoaread.hh @@ -0,0 +1,34 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 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 . + +#pragma once + +#include "common_sys.hh" + +#include + +#include "parseaut/public.hh" + + +extern const struct argp hoaread_argp; + +extern spot::automaton_parser_options opt_parse; + +spot::twa_graph_ptr +read_automaton(const char* filename, spot::bdd_dict_ptr& dict); diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index df15a07c2..658350b02 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -32,6 +32,7 @@ #include "common_aoutput.hh" #include "common_post.hh" #include "common_file.hh" +#include "common_hoaread.hh" #include "twaalgos/dot.hh" #include "twaalgos/lbtt.hh" @@ -79,6 +80,7 @@ static const argp_option options[] = static const struct argp_child children[] = { + { &hoaread_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, { &aoutput_io_format_argp, 0, nullptr, 4 }, { &post_argp, 0, nullptr, 20 }, @@ -170,7 +172,7 @@ namespace process_file(const char* filename) { spot::parse_aut_error_list pel; - auto hp = spot::automaton_stream_parser(filename); + auto hp = spot::automaton_stream_parser(filename, opt_parse); int err = 0; diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 8904b5d0d..71f80e4a1 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -38,6 +38,7 @@ #include "common_trans.hh" #include "common_file.hh" #include "common_finput.hh" +#include "common_hoaread.hh" #include "parseaut/public.hh" #include "tl/print.hh" #include "tl/apcollect.hh" @@ -160,6 +161,7 @@ const struct argp_child children[] = { { &finput_argp, 0, nullptr, 1 }, { &trans_argp, 0, nullptr, 0 }, + { &hoaread_argp, 0, "Parsing of automata:", 4 }, { &misc_argp, 0, nullptr, -2 }, { nullptr, 0, nullptr, 0 } }; @@ -548,7 +550,9 @@ namespace spot::parse_aut_error_list pel; std::string filename = output.val()->name(); - auto aut = spot::parse_aut(filename, pel, dict); + auto aut = spot::parse_aut(filename, pel, dict, + spot::default_environment::instance(), + opt_parse); if (!pel.empty()) { status_str = "parse error"; diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index bf1b7838e..905b9b8c9 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -34,6 +34,7 @@ #include "common_aoutput.hh" #include "common_post.hh" #include "common_trans.hh" +#include "common_hoaread.hh" #include "tl/relabel.hh" #include "misc/bareword.hh" @@ -93,6 +94,7 @@ build_percent_list() const struct argp_child children[] = { + { &hoaread_argp, 0, "Parsing of automata:", 3 }, { &finput_argp, 0, nullptr, 1 }, { &trans_argp, 0, nullptr, 3 }, { &aoutput_argp, 0, nullptr, 4 }, @@ -169,7 +171,9 @@ namespace spot::parse_aut_error_list pel; std::string filename = output.val()->name(); - auto aut = spot::parse_aut(filename, pel, dict); + auto aut = spot::parse_aut(filename, pel, dict, + spot::default_environment::instance(), + opt_parse); if (!pel.empty()) { problem = true; diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 6f1f6c013..190fb8dad 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -78,6 +78,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); spot::location used_loc; }; spot::parsed_aut_ptr h; + spot::automaton_parser_options opts; std::string format_version; spot::location format_version_loc; spot::environment* env; @@ -423,6 +424,16 @@ header: format-version header-items res.complete = true; } } + if (res.opts.trust_hoa) + { + auto e = res.props.end(); + bool si = res.props.find("stutter-invariant") != e; + res.h->aut->prop_stutter_invariant(si); + bool ss = res.props.find("stutter-sensitive") != e; + res.h->aut->prop_stutter_sensitive(ss); + bool iw = res.props.find("inherently-weak") != e; + res.h->aut->prop_inherently_weak(iw); + } } version: IDENTIFIER @@ -1927,6 +1938,7 @@ namespace spot { restart: result_ r; + r.opts = opts_; r.h = std::make_shared(); r.h->aut = make_twa_graph(dict); r.env = &env; diff --git a/src/parseaut/public.hh b/src/parseaut/public.hh index 61b5c1641..64514fe21 100644 --- a/src/parseaut/public.hh +++ b/src/parseaut/public.hh @@ -64,6 +64,7 @@ namespace spot { bool ignore_abort = false; ///< Skip aborted automata bool debug = false; ///< Run the parser in debug mode? + bool trust_hoa = true; ///< Trust properties in HOA files }; class SPOT_API automaton_stream_parser @@ -100,7 +101,7 @@ namespace spot /// \param dict The BDD dictionary where to use. /// \param env The environment of atomic proposition into which parsing /// should take place. - /// \param debug When true, causes the parser to trace its execution. + /// \param opts Additional options to pass to the parser. /// \return A pointer to the tgba built from \a filename, or /// 0 if the file could not be opened. /// diff --git a/src/tests/complement.test b/src/tests/complement.test index 91e4579e0..c5adc3f21 100755 --- a/src/tests/complement.test +++ b/src/tests/complement.test @@ -63,7 +63,7 @@ AP: 2 "a" "b" acc-name: generalized-co-Buchi 2 Acceptance: 2 Fin(0)|Fin(1) properties: trans-labels explicit-labels trans-acc complete -properties: deterministic +properties: deterministic stutter-invariant --BODY-- State: 0 [0&1] 0 {0 1} @@ -78,7 +78,7 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic +properties: deterministic inherently-weak --BODY-- State: 0 [0] 2 diff --git a/src/tests/ltldo.test b/src/tests/ltldo.test index e261dbaaf..f48f5c718 100755 --- a/src/tests/ltldo.test +++ b/src/tests/ltldo.test @@ -76,7 +76,7 @@ AP: 1 "_foo_" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete -properties: deterministic +properties: deterministic stutter-invariant --BODY-- State: 0 [0] 0 {0} @@ -97,6 +97,27 @@ AP: 1 "_foo_" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 +[0] 0 {0} +[!0] 0 +--END-- +EOF +diff output expected + +# Not trusting properties +run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H --trust-hoa=no >output +cat output +cat >expected < out.hoa -../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' | - sed 's/ stutter-invariant//;/properties:$/d' > out-i.hoa -../../bin/autfilt -C -Hi out.hoa --name=%M > out-i2.hoa -diff out-i.hoa out-i2.hoa +../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' >out.hoa +../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' >out-i.hoa +../../bin/autfilt -C -Hi out.hoa --name=%M >out-i2.hoa +diff -u out-i.hoa out-i2.hoa +sed 's/ stutter-invariant//;/properties:$/d' out-i3.hoa +../../bin/autfilt --trust-hoa=no -C -Hi out.hoa --name=%M >out-i2.hoa +diff -u out-i3.hoa out-i2.hoa + + cat >expected <