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

Adding option to filter by number of atomic propositions in ltlfilt.

Browse source 
* src/bin/ltlfilt.cc: Add --ap=N option.
This commit is contained in:
Thibaud Michaud 2014-10-16 23:59:34 +02:00 • committed by Alexandre Duret-Lutz
parent b012621357
commit 24d60edc84
1 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/bin/ltlfilt.cc
View file

@ -39,6 +39,7 @@
#include "ltlvisit/relabel.hh" #include "ltlvisit/relabel.hh"
#include "ltlvisit/wmunabbrev.hh" #include "ltlvisit/wmunabbrev.hh"
#include "ltlvisit/remove_x.hh" #include "ltlvisit/remove_x.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlast/unop.hh" #include "ltlast/unop.hh"
#include "ltlast/multop.hh" #include "ltlast/multop.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
@ -81,6 +82,7 @@ Exit status:\n\
#define OPT_BOOLEAN_TO_ISOP 27 #define OPT_BOOLEAN_TO_ISOP 27
#define OPT_REMOVE_X 28 #define OPT_REMOVE_X 28
#define OPT_STUTTER_INSENSITIVE 29 #define OPT_STUTTER_INSENSITIVE 29
#define OPT_AP_N 30
static const argp_option options[] = static const argp_option options[] =
{ {
@ -152,6 +154,8 @@ static const argp_option options[] =
{ "stutter-insensitive", OPT_STUTTER_INSENSITIVE, 0, 0, { "stutter-insensitive", OPT_STUTTER_INSENSITIVE, 0, 0,
"match stutter-insensitive LTL formulas", 0 }, "match stutter-insensitive LTL formulas", 0 },
{ "stutter-invariant", 0, 0, OPTION_ALIAS, 0, 0 }, { "stutter-invariant", 0, 0, OPTION_ALIAS, 0, 0 },
{ "ap", OPT_AP_N, "N", 0,
"match formulas which use exactly N atomic propositions", 0 },
{ "invert-match", 'v', 0, 0, "select non-matching formulas", 0}, { "invert-match", 'v', 0, 0, "select non-matching formulas", 0},
{ "unique", 'u', 0, 0, { "unique", 'u', 0, 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 },
@ -219,6 +223,8 @@ static spot::ltl::relabeling_style style = spot::ltl::Abc;
static bool remove_wm = false; static bool remove_wm = false;
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 unsigned ap_n = 0;
static const spot::ltl::formula* implied_by = 0; static const spot::ltl::formula* implied_by = 0;
static const spot::ltl::formula* imply = 0; static const spot::ltl::formula* imply = 0;
@ -361,6 +367,10 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_STUTTER_INSENSITIVE: case OPT_STUTTER_INSENSITIVE:
stutter_insensitive = true; stutter_insensitive = true;
break; break;
case OPT_AP_N:
ap = true;
ap_n = to_int(arg);
break;
case OPT_SYNTACTIC_SAFETY: case OPT_SYNTACTIC_SAFETY:
syntactic_safety = true; syntactic_safety = true;
break; break;
@ -521,6 +531,7 @@ namespace
matched &= !syntactic_obligation || f->is_syntactic_obligation(); matched &= !syntactic_obligation || f->is_syntactic_obligation();
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 &= !ap || atomic_prop_collect(f)->size() == ap_n;
if (matched && (size_min > 0 || size_max >= 0)) if (matched && (size_min > 0 || size_max >= 0))
{ {