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

ltlfilt: support --ap=RANGE instead of --ap=N

Browse source 
Fixes #131.

* bin/ltlfilt.cc: Implement the option.
* tests/core/ltlfilt.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-15 14:14:18 +01:00
parent 1b12df46fe
commit 52bf1da3c2
3 changed files with 41 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -48,6 +48,8 @@ New in spot 1.99.7a (not yet released)
--bsize=RANGE. The old names are still supported for backward --bsize=RANGE. The old names are still supported for backward
compatibility, but they are not documented anymore. compatibility, but they are not documented anymore.
* ltlfilt's option --ap=N can now take a RANGE as parameter.
Library: Library:
* Building products with different dictionaries now raise an * Building products with different dictionaries now raise an

19
bin/ltlfilt.cc
View file

@ -194,8 +194,8 @@ static const argp_option options[] =
{ "stutter-insensitive", OPT_STUTTER_INSENSITIVE, nullptr, 0, { "stutter-insensitive", OPT_STUTTER_INSENSITIVE, nullptr, 0,
"match stutter-insensitive LTL formulas", 0 }, "match stutter-insensitive LTL formulas", 0 },
{ "stutter-invariant", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "stutter-invariant", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "ap", OPT_AP_N, "N", 0, { "ap", OPT_AP_N, "RANGE", 0,
"match formulas which use exactly N atomic propositions", 0 }, "match formulas with a number of atomic propositions in RANGE", 0 },
{ "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0}, { "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0},
{ "unique", 'u', nullptr, 0, { "unique", 'u', nullptr, 0,
"drop formulas that have already been output (not affected by -v)", 0 }, "drop formulas that have already been output (not affected by -v)", 0 },
@ -264,8 +264,7 @@ static relabeling_mode relabeling = NoRelabeling;
static spot::relabeling_style style = spot::Abc; static spot::relabeling_style style = spot::Abc;
static bool remove_x = false; static bool remove_x = false;
static bool stutter_insensitive = false; static bool stutter_insensitive = false;
static bool ap = false; static range ap_n = { -1, -1 };
static unsigned ap_n = 0;
static int opt_max_count = -1; static int opt_max_count = -1;
static long int match_count = 0; static long int match_count = 0;
@ -433,8 +432,7 @@ parse_opt(int key, char* arg, struct argp_state*)
unabbreviate += spot::default_unabbrev_string; unabbreviate += spot::default_unabbrev_string;
break; break;
case OPT_AP_N: case OPT_AP_N:
ap = true; ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
ap_n = to_int(arg);
break; break;
case OPT_SYNTACTIC_SAFETY: case OPT_SYNTACTIC_SAFETY:
syntactic_safety = true; syntactic_safety = true;
@ -578,7 +576,14 @@ namespace
matched &= !syntactic_recurrence || f.is_syntactic_recurrence(); matched &= !syntactic_recurrence || f.is_syntactic_recurrence();
matched &= !syntactic_persistence || f.is_syntactic_persistence(); matched &= !syntactic_persistence || f.is_syntactic_persistence();
matched &= !syntactic_si || f.is_syntactic_stutter_invariant(); matched &= !syntactic_si || f.is_syntactic_stutter_invariant();
matched &= !ap || atomic_prop_collect(f)->size() == ap_n; if (matched && (ap_n.min > 0 || ap_n.max >= 0))
{
auto s = atomic_prop_collect(f);
int n = s->size();
delete s;
matched &= (ap_n.min <= 0) || (n >= ap_n.min);
matched &= (ap_n.max < 0) || (n <= ap_n.max);
}
if (matched && (size.min > 0 || size.max >= 0)) if (matched && (size.min > 0 || size.max >= 0))
{ {

28
tests/core/ltlfilt.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et # Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -140,6 +140,32 @@ checkopt -v --ltl <<EOF
!{a:b[*]:c} !{a:b[*]:c}
EOF EOF
checkopt -v --ap=3 <<EOF
GFa | FGb
F(GFa | Gb)
F(b W GFa)
GFa | Gb
b W GFa
a U Fb
G(a & Xb)
Xa
F(a & !Xa & Xb)
EOF
checkopt --ap=2..3 <<EOF
GFa | FGb
F(GFa | Gb)
F(b W GFa)
GFa | Gb
b W GFa
!({a;b[*];c}!)
!{a:b[*]:c}
a U Fb
G(a & Xb)
F(a & !Xa & Xb)
a & (b | c)
EOF
checkopt -v --stutter-invariant <<EOF checkopt -v --stutter-invariant <<EOF
!({a;b[*];c}!) !({a;b[*];c}!)
G(a & Xb) G(a & Xb)