alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

fix ltlfilt --accept-word and --reject-word

Browse source 
* NEWS: Mention the issue.
* bin/ltlfilt.cc: Fix test.
* tests/core/acc_word.test: Test this.
This commit is contained in:
Alexandre Duret-Lutz 2018-10-15 21:17:18 +02:00
parent 34f9fb5d68
commit 31bcb57648
3 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -10,6 +10,9 @@ New in spot 2.6.2.dev (not yet released)
- ltl2tgba --low now disables the "gf-guarantee" feature, as - ltl2tgba --low now disables the "gf-guarantee" feature, as
documented. documented.
- ltlfilt's --accept-word and --reject-word options were ignored
unless used together.
New in spot 2.6.2 (2018-09-28) New in spot 2.6.2 (2018-09-28)
Build: Build:

9
bin/ltlfilt.cc
View file

@ -83,6 +83,7 @@ enum {
OPT_IGNORE_ERRORS, OPT_IGNORE_ERRORS,
OPT_IMPLIED_BY, OPT_IMPLIED_BY,
OPT_IMPLY, OPT_IMPLY,
OPT_LIVENESS,
OPT_LTL, OPT_LTL,
OPT_NEGATE, OPT_NEGATE,
OPT_NNF, OPT_NNF,
@ -183,6 +184,8 @@ static const argp_option options[] =
{ "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, nullptr, 0, { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, nullptr, 0,
"match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 }, "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 },
{ "nox", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "nox", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "liveness", OPT_LIVENESS, nullptr, 0,
"match liveness properties", 0 },
{ "safety", OPT_SAFETY, nullptr, 0, { "safety", OPT_SAFETY, nullptr, 0,
"match safety formulas (even pathological)", 0 }, "match safety formulas (even pathological)", 0 },
{ "guarantee", OPT_GUARANTEE, nullptr, 0, { "guarantee", OPT_GUARANTEE, nullptr, 0,
@ -281,6 +284,7 @@ static bool negate = false;
static bool boolean_to_isop = false; static bool boolean_to_isop = false;
static bool unique = false; static bool unique = false;
static bool psl = false; static bool psl = false;
static bool liveness = false;
static bool ltl = false; static bool ltl = false;
static bool invert = false; static bool invert = false;
static bool boolean = false; static bool boolean = false;
@ -432,6 +436,9 @@ parse_opt(int key, char* arg, struct argp_state*)
opt->imply = spot::formula::And({opt->imply, i}); opt->imply = spot::formula::And({opt->imply, i});
break; break;
} }
case OPT_LIVENESS:
liveness = true;
break;
case OPT_LTL: case OPT_LTL:
ltl = true; ltl = true;
break; break;
@ -697,7 +704,7 @@ namespace
{ {
spot::twa_graph_ptr aut = nullptr; spot::twa_graph_ptr aut = nullptr;
if (!opt->acc_words.empty() && !opt->rej_words.empty()) if (!opt->acc_words.empty() || !opt->rej_words.empty())
{ {
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);

6
tests/core/acc_word.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement # Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -137,3 +137,7 @@ done
ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1 ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1
test $? -eq 2 test $? -eq 2
grep 'highlight-word.*Fin' stderr grep 'highlight-word.*Fin' stderr
ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1
ltlfilt -f 'GF!a' --accept-word 'cycle{!a}'