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

autfilt: add option --simplify_acceptance

Browse source 
* NEWS: Mention this.
* bin/autfilt.cc: Add option --simplify-acceptance.
This commit is contained in:
Thomas Medioni 2017-05-04 14:49:22 +02:00
parent a12d676bdc
commit 570c433122
2 changed files with 16 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -18,6 +18,9 @@ New in spot 2.3.4.dev (not yet released)
formulas into labels that are min-terms. (See spot::split_edges() formulas into labels that are min-terms. (See spot::split_edges()
below.) below.)
- autfilt learned --simplify-acceptance to simplify some acceptance
conditions. (See spot::simplify_acceptance() below.)
Library: Library:
- A new library, libspotgen, gathers all functions used to generate - A new library, libspotgen, gathers all functions used to generate

14
bin/autfilt.cc
View file

@ -137,6 +137,7 @@ enum {
OPT_SCCS, OPT_SCCS,
OPT_SEED, OPT_SEED,
OPT_SEP_SETS, OPT_SEP_SETS,
OPT_SIMPL_ACC,
OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_SIMPLIFY_EXCLUSIVE_AP,
OPT_SPLIT_EDGES, OPT_SPLIT_EDGES,
OPT_STATES, OPT_STATES,
@ -325,6 +326,9 @@ static const argp_option options[] =
{ "remove-dead-states", OPT_REM_DEAD, nullptr, 0, { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
"remove states that are unreachable, or that cannot belong to an " "remove states that are unreachable, or that cannot belong to an "
"infinite path", 0 }, "infinite path", 0 },
{ "simplify-acceptance", OPT_SIMPL_ACC, nullptr, 0,
"simplify the acceptance condition by merging identical acceptance sets "
"and by simplifying some terms containing complementary sets", 0 },
{ "split-edges", OPT_SPLIT_EDGES, nullptr, 0, { "split-edges", OPT_SPLIT_EDGES, nullptr, 0,
"split edges into transitions labeled by conjunctions of all atomic " "split edges into transitions labeled by conjunctions of all atomic "
"propositions, so they can be read as letters", 0 }, "propositions, so they can be read as letters", 0 },
@ -497,6 +501,7 @@ static bool opt_dualize = false;
static spot::acc_cond::mark_t opt_mask_acc = 0U; static spot::acc_cond::mark_t opt_mask_acc = 0U;
static std::vector<bool> opt_keep_states = {}; static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0; static unsigned int opt_keep_states_initial = 0;
static bool opt_simpl_acc = false;
static bool opt_simplify_exclusive_ap = false; static bool opt_simplify_exclusive_ap = false;
static bool opt_rem_dead = false; static bool opt_rem_dead = false;
static bool opt_rem_unreach = false; static bool opt_rem_unreach = false;
@ -867,6 +872,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_SEP_SETS: case OPT_SEP_SETS:
opt_sep_sets = true; opt_sep_sets = true;
break; break;
case OPT_SIMPL_ACC:
opt_simpl_acc = true;
break;
case OPT_SIMPLIFY_EXCLUSIVE_AP: case OPT_SIMPLIFY_EXCLUSIVE_AP:
opt_simplify_exclusive_ap = true; opt_simplify_exclusive_ap = true;
opt_merge = true; opt_merge = true;
@ -1074,8 +1082,12 @@ namespace
spot::strip_acceptance_here(aut); spot::strip_acceptance_here(aut);
if (opt_merge) if (opt_merge)
aut->merge_edges(); aut->merge_edges();
if (opt_clean_acc)
if (opt_simpl_acc)
simplify_acceptance_here(aut);
else if (opt_clean_acc)
cleanup_acceptance_here(aut); cleanup_acceptance_here(aut);
if (opt_sep_sets) if (opt_sep_sets)
separate_sets_here(aut); separate_sets_here(aut);
if (opt_complement_acc) if (opt_complement_acc)