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

autfilt: add a --strip-acceptance option

Browse source 
* src/bin/autfilt.cc: New option.
* src/tgbatest/sbacc.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-03 23:02:37 +01:00
parent acb67c1bf6
commit ee0b8e4ea8
2 changed files with 29 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/bin/autfilt.cc
View file

@ -48,6 +48,7 @@
#include "tgbaalgos/canonicalize.hh" #include "tgbaalgos/canonicalize.hh"
#include "tgbaalgos/mask.hh" #include "tgbaalgos/mask.hh"
#include "tgbaalgos/sbacc.hh" #include "tgbaalgos/sbacc.hh"
#include "tgbaalgos/stripacc.hh"
static const char argp_program_doc[] ="\ static const char argp_program_doc[] ="\
@ -76,6 +77,7 @@ Exit status:\n\
#define OPT_INTERSECT 16 #define OPT_INTERSECT 16
#define OPT_MASK_ACC 17 #define OPT_MASK_ACC 17
#define OPT_SBACC 18 #define OPT_SBACC 18
#define OPT_STRIPACC 19
static const argp_option options[] = static const argp_option options[] =
{ {
@ -110,6 +112,8 @@ static const argp_option options[] =
{ "state-based-acceptance", OPT_SBACC, 0, 0, { "state-based-acceptance", OPT_SBACC, 0, 0,
"define the acceptance using states", 0 }, "define the acceptance using states", 0 },
{ "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
{ "strip-acceptance", OPT_STRIPACC, 0, 0,
"remove the acceptance conditions and all acceptance sets", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Filtering options:", 6 }, { 0, 0, 0, 0, "Filtering options:", 6 },
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
@ -178,6 +182,7 @@ static bool opt_destut = false;
static char opt_instut = 0; static char opt_instut = 0;
static bool opt_is_empty = false; static bool opt_is_empty = false;
static bool opt_sbacc = false; static bool opt_sbacc = false;
static bool opt_stripacc = false;
static std::unique_ptr<unique_aut_t> opt_uniq = nullptr; static std::unique_ptr<unique_aut_t> opt_uniq = nullptr;
static spot::acc_cond::mark_t opt_mask_acc = 0U; static spot::acc_cond::mark_t opt_mask_acc = 0U;
@ -314,6 +319,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_STATES: case OPT_STATES:
opt_states = parse_range(arg, 0, std::numeric_limits<int>::max()); opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
break; break;
case OPT_STRIPACC:
opt_stripacc = true;
break;
case OPT_TGBA: case OPT_TGBA:
if (automaton_format == Spin) if (automaton_format == Spin)
error(2, 0, "--spin and --tgba are incompatible"); error(2, 0, "--spin and --tgba are incompatible");
@ -366,6 +374,8 @@ namespace
// Preprocessing. // Preprocessing.
if (opt_stripacc)
spot::strip_acceptance_here(aut);
if (opt_merge) if (opt_merge)
aut->merge_transitions(); aut->merge_transitions();

20
src/tgbatest/sbacc.test
View file

@ -102,7 +102,25 @@ diff out.hoa expected
$autfilt --sba -H expected > out.hoa $autfilt --sba -H expected > out.hoa
diff out.hoa expected diff out.hoa expected
$autfilt --strip-acc -H expected > out.hoa
cat >expected <<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0] 1
State: 1
[0] 2
State: 2
[0] 0
--END--
EOF
diff out.hoa expected
../../bin/randltl --weak-fairness -n 20 2 | ../../bin/randltl --weak-fairness -n 20 2 |
../../bin/ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O" ../../bin/ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O"