autfilt: add options --is-deterministic --is-complete and -v
* src/bin/autfilt.cc: Here. * src/tgbatest/hoaparse.test: More tests.
This commit is contained in:
Alexandre Duret-Lutz
parent
9c672ac49b
commit
9cee6e6fa1
2 changed files with 111 additions and 5 deletions
|
|
@ -37,6 +37,7 @@
|
|||
#include "tgbaalgos/product.hh"
|
||||
#include "tgbaalgos/save.hh"
|
||||
#include "tgbaalgos/stats.hh"
|
||||
#include "tgbaalgos/isdet.hh"
|
||||
#include "tgba/bddprint.hh"
|
||||
#include "misc/optionmap.hh"
|
||||
#include "misc/timer.hh"
|
||||
|
|
@ -65,6 +66,8 @@ Exit status:\n\
|
|||
#define OPT_PRODUCT 8
|
||||
#define OPT_MERGE 9
|
||||
#define OPT_ARE_ISOMORPHIC 10
|
||||
#define OPT_IS_COMPLETE 11
|
||||
#define OPT_IS_DETERMINISTIC 12
|
||||
|
||||
static const argp_option options[] =
|
||||
{
|
||||
|
|
@ -131,13 +134,18 @@ static const argp_option options[] =
|
|||
{ "product", OPT_PRODUCT, "FILENAME", 0,
|
||||
"build the product with FILENAME", 0 },
|
||||
{ "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
|
||||
"randomize states and transitions (specify 's' or 't' to"
|
||||
"randomize states and transitions (specify 's' or 't' to "
|
||||
"randomize only states or transitions)", 0 },
|
||||
/**************************************************/
|
||||
{ 0, 0, 0, 0, "Filters:", 6 },
|
||||
{ "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
|
||||
"keep automata that are isomorphic the automaton in FILENAME", 0 },
|
||||
"keep automata that are isomorphic to the automaton in FILENAME", 0 },
|
||||
{ "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 },
|
||||
{ "is-complete", OPT_IS_COMPLETE, 0, 0,
|
||||
"the automaton is complete", 0 },
|
||||
{ "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0,
|
||||
"the automaton is deterministic", 0 },
|
||||
{ "invert-match", 'v', 0, 0, "select non-matching automata", 0},
|
||||
/**************************************************/
|
||||
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
|
||||
{ "extra-options", 'x', "OPTS", 0,
|
||||
|
|
@ -167,6 +175,9 @@ static auto dict = spot::make_bdd_dict();
|
|||
static spot::tgba_digraph_ptr opt_product = nullptr;
|
||||
static bool opt_merge = false;
|
||||
static spot::tgba_digraph_ptr opt_are_isomorphic = nullptr;
|
||||
static bool opt_is_complete = false;
|
||||
static bool opt_is_deterministic = false;
|
||||
static bool opt_invert = false;
|
||||
|
||||
static int
|
||||
to_int(const char* s)
|
||||
|
|
@ -208,6 +219,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
if (type != spot::postprocessor::Monitor)
|
||||
type = spot::postprocessor::BA;
|
||||
break;
|
||||
case 'v':
|
||||
opt_invert = true;
|
||||
break;
|
||||
case 'x':
|
||||
{
|
||||
const char* opt = extra_options.parse_options(arg);
|
||||
|
|
@ -228,6 +242,12 @@ parse_opt(int key, char* arg, struct argp_state*)
|
|||
opt_are_isomorphic = std::move(p->aut);
|
||||
break;
|
||||
}
|
||||
case OPT_IS_COMPLETE:
|
||||
opt_is_complete = true;
|
||||
break;
|
||||
case OPT_IS_DETERMINISTIC:
|
||||
opt_is_deterministic = true;
|
||||
break;
|
||||
case OPT_LBTT:
|
||||
if (arg)
|
||||
{
|
||||
|
|
@ -416,14 +436,19 @@ namespace
|
|||
|
||||
bool matched = true;
|
||||
|
||||
if (opt_is_complete)
|
||||
matched &= is_complete(aut);
|
||||
if (opt_is_deterministic)
|
||||
matched &= is_deterministic(aut);
|
||||
if (opt_are_isomorphic)
|
||||
matched &= !are_isomorphic(aut, opt_are_isomorphic).empty();
|
||||
|
||||
one_match |= matched;
|
||||
|
||||
if (!matched)
|
||||
// Drop or keep matched automata depending on the --invert option
|
||||
if (matched == opt_invert)
|
||||
return 0;
|
||||
|
||||
one_match = true;
|
||||
|
||||
// Postprocessing.
|
||||
|
||||
if (opt_product)
|
||||
|
|
|
|||
|
|
@ -903,3 +903,84 @@ EOF
|
|||
run 0 ../ltl2tgba -d -XH input 2> output.err
|
||||
grep -- "--BODY--" output.err
|
||||
grep "identifier.*v1" output.err
|
||||
|
||||
|
||||
|
||||
# This was generated by
|
||||
# randaut -n 10 -Hl 3 -d 0.055 --seed=3 | fmt
|
||||
cat > input <<EOF
|
||||
HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance:
|
||||
0 t properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY-- State: 0 [0&!1&2] 0 [0&1&2] 1 State: 1 [0&1&2] 2 State: 2
|
||||
[!0&1&!2] 3 State: 3 [!0&1&!2] 4 State: 4 [!0&1&2] 1 [0&!1&!2] 5 State:
|
||||
5 [!0&1&2] 6 State: 6 [!0&1&2] 7 State: 7 [0&1&2] 8 State: 8 [!0&!1&2]
|
||||
9 State: 9 [0&1&2] 2 [!0&!1&!2] 6 [!0&1&!2] 1 --END-- HOA: v1 States: 10
|
||||
Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance: 0 t properties:
|
||||
trans-labels explicit-labels state-acc deterministic --BODY-- State: 0
|
||||
[!0&1&2] 1 State: 1 [0&!1&!2] 2 State: 2 [!0&1&!2] 3 State: 3 [0&!1&2]
|
||||
4 [!0&!1&!2] 5 [!0&1&!2] 6 State: 4 [!0&!1&!2] 7 [0&!1&2] 0 State: 5
|
||||
[0&1&!2] 8 State: 6 [!0&1&!2] 7 State: 7 [!0&1&!2] 9 State: 8 [!0&1&2]
|
||||
2 State: 9 [0&1&2] 6 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0"
|
||||
"p1" "p2" acc-name: all Acceptance: 0 t properties: trans-labels
|
||||
explicit-labels state-acc deterministic --BODY-- State: 0 [0&1&!2]
|
||||
1 State: 1 [0&1&!2] 2 [0&!1&!2] 3 State: 2 [!0&1&!2] 1 [!0&!1&!2] 4
|
||||
State: 3 [0&1&!2] 5 State: 4 [!0&1&2] 3 [!0&!1&2] 6 State: 5 [0&1&!2]
|
||||
7 State: 6 [!0&!1&!2] 8 State: 7 [!0&!1&!2] 5 State: 8 [!0&!1&!2] 9
|
||||
[0&1&!2] 6 State: 9 [!0&1&2] 8 [0&!1&2] 4 [!0&!1&!2] 7 --END-- HOA:
|
||||
v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance:
|
||||
0 t properties: trans-labels explicit-labels state-acc --BODY-- State:
|
||||
0 [0&1&2] 1 State: 1 [0&1&2] 2 State: 2 [0&!1&!2] 3 [0&!1&2] 4 [0&!1&2]
|
||||
0 State: 3 [!0&1&2] 1 [0&!1&2] 2 [!0&!1&2] 5 State: 4 [0&1&!2] 6 State: 5
|
||||
[!0&1&!2] 7 State: 6 [0&!1&!2] 2 State: 7 [!0&!1&2] 8 State: 8 [0&!1&!2]
|
||||
9 State: 9 [!0&1&!2] 7 [!0&1&!2] 6 --END-- HOA: v1 States: 10 Start: 0 AP:
|
||||
3 "p0" "p1" "p2" acc-name: all Acceptance: 0 t properties: trans-labels
|
||||
explicit-labels state-acc --BODY-- State: 0 [!0&!1&2] 1 State: 1 [!0&!1&2]
|
||||
2 State: 2 [0&1&!2] 3 State: 3 [!0&1&!2] 4 State: 4 [!0&1&2] 5 State:
|
||||
5 [0&!1&!2] 6 State: 6 [!0&!1&!2] 5 [!0&!1&!2] 7 State: 7 [!0&!1&!2] 7
|
||||
[!0&!1&2] 6 [0&!1&2] 8 State: 8 [0&1&2] 8 [0&1&!2] 9 State: 9 [0&!1&2]
|
||||
2 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name:
|
||||
all Acceptance: 0 t properties: trans-labels explicit-labels state-acc
|
||||
deterministic --BODY-- State: 0 [!0&!1&2] 1 State: 1 [0&!1&!2] 2 State: 2
|
||||
[!0&!1&2] 3 State: 3 [!0&!1&!2] 4 State: 4 [!0&1&!2] 5 State: 5 [!0&1&2]
|
||||
6 State: 6 [0&1&!2] 1 [!0&!1&!2] 3 [!0&1&2] 7 State: 7 [0&1&2] 8 State:
|
||||
8 [0&!1&!2] 7 [0&1&!2] 9 State: 9 [0&1&2] 0 --END-- HOA: v1 States: 10
|
||||
Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance: 0 t properties:
|
||||
trans-labels explicit-labels state-acc deterministic --BODY-- State: 0
|
||||
[0&1&!2] 1 State: 1 [!0&1&2] 2 State: 2 [0&1&2] 3 State: 3 [0&1&!2] 4
|
||||
State: 4 [!0&!1&2] 5 State: 5 [!0&!1&!2] 6 State: 6 [!0&1&!2] 7 State: 7
|
||||
[!0&!1&!2] 3 [!0&1&2] 8 State: 8 [0&!1&2] 9 State: 9 [!0&!1&!2] 9 [0&!1&2]
|
||||
3 [!0&1&!2] 2 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2"
|
||||
acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels
|
||||
state-acc --BODY-- State: 0 [0&!1&!2] 1 State: 1 [!0&!1&2] 2 [0&!1&2] 3
|
||||
State: 2 [0&!1&2] 4 State: 3 [0&!1&!2] 5 [0&!1&!2] 6 State: 4 [0&!1&!2] 7
|
||||
[0&!1&2] 3 State: 5 [!0&!1&!2] 8 State: 6 [!0&!1&2] 4 [0&!1&2] 6 State: 7
|
||||
[0&!1&2] 4 [!0&!1&!2] 1 State: 8 [!0&1&2] 6 [0&1&2] 9 State: 9 [0&1&!2]
|
||||
3 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name:
|
||||
all Acceptance: 0 t properties: trans-labels explicit-labels state-acc
|
||||
--BODY-- State: 0 [!0&1&2] 1 State: 1 [!0&!1&!2] 2 [!0&!1&2] 3 [!0&1&2]
|
||||
4 [!0&1&2] 5 State: 2 [0&1&!2] 2 [0&!1&2] 6 State: 3 [0&1&2] 3 [0&!1&2] 7
|
||||
[!0&1&2] 2 State: 4 [!0&!1&!2] 8 State: 5 [0&!1&!2] 2 [!0&!1&2] 6 State:
|
||||
6 [!0&!1&2] 2 [!0&1&!2] 7 State: 7 [0&1&2] 9 State: 8 [!0&1&2] 7 State:
|
||||
9 [!0&1&2] 2 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2"
|
||||
acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels
|
||||
state-acc deterministic --BODY-- State: 0 [!0&!1&!2] 1 State: 1 [0&1&!2] 2
|
||||
[!0&!1&!2] 3 [0&!1&2] 4 State: 2 [0&1&!2] 5 State: 3 [!0&!1&!2] 6 State:
|
||||
4 [!0&!1&!2] 7 State: 5 [!0&1&2] 2 State: 6 [!0&!1&2] 8 State: 7 [0&1&2]
|
||||
9 State: 8 [0&!1&!2] 7 State: 9 [!0&1&!2] 1 [0&1&!2] 7 --END--
|
||||
EOF
|
||||
|
||||
expectok input --is-deter --stats='%F:%L: %c' <<EOF
|
||||
input:1.1-6.53: 2
|
||||
input:6.55-12.28: 2
|
||||
input:12.30-18.62: 5
|
||||
input:30.11-35.51: 1
|
||||
input:35.53-41.21: 3
|
||||
input:53.22-58.62: 3
|
||||
EOF
|
||||
|
||||
expectok input -v --is-deter --stats='%F:%L: %n' <<EOF
|
||||
input:18.64-24.42: 2
|
||||
input:24.44-30.9: 1
|
||||
input:41.23-47.9: 1
|
||||
input:47.11-53.20: 1
|
||||
EOF
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue