Commit 51a75a31 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 585e29e7
...@@ -6,13 +6,17 @@ New in spot 1.99.4a (not yet released) ...@@ -6,13 +6,17 @@ New in spot 1.99.4a (not yet released)
It currently works only for deterministic automata. It currently works only for deterministic automata.
* By default, autfilt does not simplify automata (this has not * 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 one of --small, --deterministic, or --any is given, the
optimization level automatically defaults to --high (unless optimization level automatically defaults to --high (unless
specified otherwise). For symmetry, if one of --low, --medium, or 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). (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 FILENAME[/COL] is now the same as
ltlgrind -F FILENAME[/COL] for consistency with ltlfilt. ltlgrind -F FILENAME[/COL] for consistency with ltlfilt.
...@@ -39,6 +43,11 @@ New in spot 1.99.4a (not yet released) ...@@ -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 * 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. 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. * ltl_simplifier renamed to tl_simplifier.
Python: Python:
...@@ -53,9 +62,14 @@ New in spot 1.99.4a (not yet released) ...@@ -53,9 +62,14 @@ New in spot 1.99.4a (not yet released)
* spot.postprocess(aut, *options), or aut.postprocess(*options) * spot.postprocess(aut, *options), or aut.postprocess(*options)
simplify the use of the spot.postprocessor object. (Just like we simplify the use of the spot.postprocessor object. (Just like we
have spot.translate() on top of spot.translator().) have spot.translate() on top of spot.translator().)
* spot.automata() and spot.automaton() now have an optional * spot.automata() and spot.automaton() now have additional
timeout argument to restrict the runtime of commands that optional arguments:
produce automata. - 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: Bugs fixed:
......
...@@ -36,6 +36,8 @@ libcommon_a_SOURCES = \ ...@@ -36,6 +36,8 @@ libcommon_a_SOURCES = \
common_file.hh \ common_file.hh \
common_finput.cc \ common_finput.cc \
common_finput.hh \ common_finput.hh \
common_hoaread.cc \
common_hoaread.hh \
common_output.cc \ common_output.cc \
common_output.hh \ common_output.hh \
common_post.cc \ common_post.cc \
......
...@@ -35,6 +35,7 @@ ...@@ -35,6 +35,7 @@
#include "common_range.hh" #include "common_range.hh"
#include "common_post.hh" #include "common_post.hh"
#include "common_conv.hh" #include "common_conv.hh"
#include "common_hoaread.hh"
#include "twaalgos/product.hh" #include "twaalgos/product.hh"
#include "twaalgos/isdet.hh" #include "twaalgos/isdet.hh"
...@@ -58,7 +59,7 @@ ...@@ -58,7 +59,7 @@
#include "twaalgos/complement.hh" #include "twaalgos/complement.hh"
static const char argp_program_doc[] ="\ static const char argp_program_doc[] ="\
Convert, transform, and filter Büchi automata.\v\ Convert, transform, and filter omega-automata.\v\
Exit status:\n\ Exit status:\n\
0 if some automata were output\n\ 0 if some automata were output\n\
1 if no automata were output (no match)\n\ 1 if no automata were output (no match)\n\
...@@ -229,6 +230,7 @@ static const argp_option options[] = ...@@ -229,6 +230,7 @@ static const argp_option options[] =
static const struct argp_child children[] = static const struct argp_child children[] =
{ {
{ &hoaread_argp, 0, nullptr, 0 },
{ &aoutput_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 },
{ &aoutput_io_format_argp, 0, nullptr, 4 }, { &aoutput_io_format_argp, 0, nullptr, 4 },
{ &post_argp_disabled, 0, nullptr, 20 }, { &post_argp_disabled, 0, nullptr, 20 },
...@@ -675,7 +677,7 @@ namespace ...@@ -675,7 +677,7 @@ namespace
process_file(const char* filename) process_file(const char* filename)
{ {
spot::parse_aut_error_list pel; 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; int err = 0;
......
...@@ -20,7 +20,6 @@ ...@@ -20,7 +20,6 @@
#include "common_conv.hh" #include "common_conv.hh"
#include <cstdlib> #include <cstdlib>
#include "error.h" #include "error.h"
#include "parseaut/public.hh"
int int
to_int(const char* s) to_int(const char* s)
...@@ -70,17 +69,6 @@ to_probability(const char* s) ...@@ -70,17 +69,6 @@ to_probability(const char* s)
return res; 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<long> std::vector<long>
to_longs(const char* arg) to_longs(const char* arg)
{ {
......
...@@ -30,6 +30,3 @@ float to_probability(const char* s); ...@@ -30,6 +30,3 @@ float to_probability(const char* s);
// Parse the comma or space seperate string of numbers. // Parse the comma or space seperate string of numbers.
std::vector<long> to_longs(const char* s); std::vector<long> to_longs(const char* s);
spot::twa_graph_ptr
read_automaton(const char* filename, spot::bdd_dict_ptr& dict);
// -*- 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 <http://www.gnu.org/licenses/>.
#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 };
// -*- 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 <http://www.gnu.org/licenses/>.
#pragma once
#include "common_sys.hh"
#include <argp.h>
#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);
...@@ -32,6 +32,7 @@ ...@@ -32,6 +32,7 @@
#include "common_aoutput.hh" #include "common_aoutput.hh"
#include "common_post.hh" #include "common_post.hh"
#include "common_file.hh" #include "common_file.hh"
#include "common_hoaread.hh"
#include "twaalgos/dot.hh" #include "twaalgos/dot.hh"
#include "twaalgos/lbtt.hh" #include "twaalgos/lbtt.hh"
...@@ -79,6 +80,7 @@ static const argp_option options[] = ...@@ -79,6 +80,7 @@ static const argp_option options[] =
static const struct argp_child children[] = static const struct argp_child children[] =
{ {
{ &hoaread_argp, 0, nullptr, 0 },
{ &aoutput_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 },
{ &aoutput_io_format_argp, 0, nullptr, 4 }, { &aoutput_io_format_argp, 0, nullptr, 4 },
{ &post_argp, 0, nullptr, 20 }, { &post_argp, 0, nullptr, 20 },
...@@ -170,7 +172,7 @@ namespace ...@@ -170,7 +172,7 @@ namespace
process_file(const char* filename) process_file(const char* filename)
{ {
spot::parse_aut_error_list pel; 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; int err = 0;
......
...@@ -38,6 +38,7 @@ ...@@ -38,6 +38,7 @@
#include "common_trans.hh" #include "common_trans.hh"
#include "common_file.hh" #include "common_file.hh"
#include "common_finput.hh" #include "common_finput.hh"
#include "common_hoaread.hh"
#include "parseaut/public.hh" #include "parseaut/public.hh"
#include "tl/print.hh" #include "tl/print.hh"
#include "tl/apcollect.hh" #include "tl/apcollect.hh"
...@@ -160,6 +161,7 @@ const struct argp_child children[] = ...@@ -160,6 +161,7 @@ const struct argp_child children[] =
{ {
{ &finput_argp, 0, nullptr, 1 }, { &finput_argp, 0, nullptr, 1 },
{ &trans_argp, 0, nullptr, 0 }, { &trans_argp, 0, nullptr, 0 },
{ &hoaread_argp, 0, "Parsing of automata:", 4 },
{ &misc_argp, 0, nullptr, -2 }, { &misc_argp, 0, nullptr, -2 },
{ nullptr, 0, nullptr, 0 } { nullptr, 0, nullptr, 0 }
}; };
...@@ -548,7 +550,9 @@ namespace ...@@ -548,7 +550,9 @@ namespace
spot::parse_aut_error_list pel; spot::parse_aut_error_list pel;
std::string filename = output.val()->name(); 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()) if (!pel.empty())
{ {
status_str = "parse error"; status_str = "parse error";
......
...@@ -34,6 +34,7 @@ ...@@ -34,6 +34,7 @@
#include "common_aoutput.hh" #include "common_aoutput.hh"
#include "common_post.hh" #include "common_post.hh"
#include "common_trans.hh" #include "common_trans.hh"
#include "common_hoaread.hh"
#include "tl/relabel.hh" #include "tl/relabel.hh"
#include "misc/bareword.hh" #include "misc/bareword.hh"
...@@ -93,6 +94,7 @@ build_percent_list() ...@@ -93,6 +94,7 @@ build_percent_list()
const struct argp_child children[] = const struct argp_child children[] =
{ {
{ &hoaread_argp, 0, "Parsing of automata:", 3 },
{ &finput_argp, 0, nullptr, 1 }, { &finput_argp, 0, nullptr, 1 },
{ &trans_argp, 0, nullptr, 3 }, { &trans_argp, 0, nullptr, 3 },
{ &aoutput_argp, 0, nullptr, 4 }, { &aoutput_argp, 0, nullptr, 4 },
...@@ -169,7 +171,9 @@ namespace ...@@ -169,7 +171,9 @@ namespace
spot::parse_aut_error_list pel; spot::parse_aut_error_list pel;
std::string filename = output.val()->name(); 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()) if (!pel.empty())
{ {
problem = true; problem = true;
......
...@@ -78,6 +78,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); ...@@ -78,6 +78,7 @@ extern "C" int strverscmp(const char *s1, const char *s2);
spot::location used_loc; spot::location used_loc;
}; };
spot::parsed_aut_ptr h; spot::parsed_aut_ptr h;
spot::automaton_parser_options opts;
std::string format_version; std::string format_version;
spot::location format_version_loc; spot::location format_version_loc;
spot::environment* env; spot::environment* env;
...@@ -423,6 +424,16 @@ header: format-version header-items ...@@ -423,6 +424,16 @@ header: format-version header-items
res.complete = true; 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 version: IDENTIFIER
...@@ -1927,6 +1938,7 @@ namespace spot ...@@ -1927,6 +1938,7 @@ namespace spot
{ {
restart: restart:
result_ r; result_ r;
r.opts = opts_;
r.h = std::make_shared<spot::parsed_aut>(); r.h = std::make_shared<spot::parsed_aut>();
r.h->aut = make_twa_graph(dict); r.h->aut = make_twa_graph(dict);
r.env = &env; r.env = &env;
......
...@@ -64,6 +64,7 @@ namespace spot ...@@ -64,6 +64,7 @@ namespace spot
{ {
bool ignore_abort = false; ///< Skip aborted automata bool ignore_abort = false; ///< Skip aborted automata
bool debug = false; ///< Run the parser in debug mode? bool debug = false; ///< Run the parser in debug mode?
bool trust_hoa = true; ///< Trust properties in HOA files
}; };
class SPOT_API automaton_stream_parser class SPOT_API automaton_stream_parser
...@@ -100,7 +101,7 @@ namespace spot ...@@ -100,7 +101,7 @@ namespace spot
/// \param dict The BDD dictionary where to use. /// \param dict The BDD dictionary where to use.
/// \param env The environment of atomic proposition into which parsing /// \param env The environment of atomic proposition into which parsing
/// should take place. /// 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 /// \return A pointer to the tgba built from \a filename, or
/// 0 if the file could not be opened. /// 0 if the file could not be opened.
/// ///
......
...@@ -63,7 +63,7 @@ AP: 2 "a" "b" ...@@ -63,7 +63,7 @@ AP: 2 "a" "b"
acc-name: generalized-co-Buchi 2 acc-name: generalized-co-Buchi 2
Acceptance: 2 Fin(0)|Fin(1) Acceptance: 2 Fin(0)|Fin(1)
properties: trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic stutter-invariant
--BODY-- --BODY--
State: 0 State: 0
[0&1] 0 {0 1} [0&1] 0 {0 1}
...@@ -78,7 +78,7 @@ AP: 1 "a" ...@@ -78,7 +78,7 @@ AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic properties: deterministic inherently-weak
--BODY-- --BODY--
State: 0 State: 0
[0] 2 [0] 2
......
...@@ -76,7 +76,7 @@ AP: 1 "_foo_" ...@@ -76,7 +76,7 @@ AP: 1 "_foo_"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic stutter-invariant
--BODY-- --BODY--
State: 0 State: 0
[0] 0 {0} [0] 0 {0}
...@@ -97,6 +97,27 @@ AP: 1 "_foo_" ...@@ -97,6 +97,27 @@ AP: 1 "_foo_"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete 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 <<EOF
HOA: v1
name: "GFp0"
States: 1
Start: 0
AP: 1 "_foo_"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
......
...@@ -1658,11 +1658,15 @@ EOF ...@@ -1658,11 +1658,15 @@ EOF
# Implicit labels # Implicit labels
../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' > out.hoa ../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' >out.hoa
../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' | ../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' >out-i.hoa
sed 's/ stutter-invariant//;/properties:$/d' > out-i.hoa ../../bin/autfilt -C -Hi out.hoa --name=%M >out-i2.hoa
../../bin/autfilt -C -Hi out.hoa --name=%M > out-i2.hoa diff -u out-i.hoa out-i2.hoa
diff out-i.hoa out-i2.hoa sed 's/ stutter-invariant//;/properties:$/d' <out-i.hoa >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 <<EOF cat >expected <<EOF
HOA: v1 HOA: v1
...@@ -1673,6 +1677,7 @@ AP: 4 "c" "d" "a" "b" ...@@ -1673,6 +1677,7 @@ AP: 4 "c" "d" "a" "b"
acc-name: generalized-Buchi 2 acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1) Acceptance: 2 Inf(0)&Inf(1)
properties: implicit-labels trans-acc complete deterministic properties: implicit-labels trans-acc complete deterministic
properties: stutter-invariant
--BODY-- --BODY--
State: 0 State: 0
0 0
...@@ -1738,6 +1743,7 @@ AP: 4 "c" "d" "a" "b" ...@@ -1738,6 +1743,7 @@ AP: 4 "c" "d" "a" "b"
acc-name: generalized-Buchi 2 acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1) Acceptance: 2 Inf(0)&Inf(1)
properties: implicit-labels state-acc complete deterministic properties: implicit-labels state-acc complete deterministic
properties: stutter-invariant
--BODY-- --BODY--
State: 0 State: 0
1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2
......