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

autfilt: add a --quiet option

Browse source 
* src/bin/autfilt.cc: Add option.
* src/tgbatest/det.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-11 15:15:23 +01:00
parent 541ce543c7
commit 1e84bb1ee7
2 changed files with 58 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/bin/autfilt.cc
View file

@ -89,6 +89,7 @@ static const argp_option options[] =
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
"LBTT's format (add =t to force transition-based acceptance even" "LBTT's format (add =t to force transition-based acceptance even"
" on Büchi automata)", 0 }, " on Büchi automata)", 0 },
{ "quiet", 'q', 0, 0, "suppress all normal output", 0 },
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
{ "utf8", '8', 0, 0, "enable UTF-8 characters in output " { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
@ -151,7 +152,7 @@ static const struct argp_child children[] =
{ 0, 0, 0, 0 } { 0, 0, 0, 0 }
}; };
static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa, Quiet }
format = Dot; format = Dot;
static bool one_match = false; static bool one_match = false;
static const char* stats = ""; static const char* stats = "";
@ -197,6 +198,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case 'M': case 'M':
type = spot::postprocessor::Monitor; type = spot::postprocessor::Monitor;
break; break;
case 'q':
format = Quiet;
break;
case 's': case 's':
format = Spin; format = Spin;
if (type != spot::postprocessor::Monitor) if (type != spot::postprocessor::Monitor)
@ -443,6 +447,9 @@ namespace
case Hoa: case Hoa:
spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
break; break;
case Quiet:
// Do not output anything.
break;
case Spot: case Spot:
spot::tgba_save_reachable(std::cout, aut); spot::tgba_save_reachable(std::cout, aut);
break; break;

78
src/tgbatest/det.test
View file

@ -59,39 +59,61 @@ EOF
$ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out $ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out
diff formulas out diff formulas out
cat >in.tgba <<'EOF' cat >in.hoa <<'EOF'
acc = "1"; HOA: v1
"1", "2", "a", "1"; States: 3
"1", "1", "!a",; Start: 0
"2", "3", "a", "1"; AP: 1 "a"
"2", "1", "!a",; acc-name: Buchi
"3", "3", "a",; Acceptance: 1 Inf(0)
"3", "1", "!a",; properties: trans-labels explicit-labels trans-acc complete deterministic
--BODY--
State: 0
[!0] 0
[0] 1 {0}
State: 1
[!0] 0
[0] 2 {0}
State: 2
[!0] 0
[0] 2
--END--
EOF EOF
# FIXME: we should improve this output # FIXME: we should improve this output
cat >ex.tgba <<'EOF' cat >ex.hoa <<'EOF'
acc = "0"; HOA: v1
"0", "0", "!a",; States: 5
"0", "1", "a",; Start: 0
"0", "3", "!a",; AP: 1 "a"
"1", "0", "!a",; acc-name: Buchi
"1", "2", "a",; Acceptance: 1 Inf(0)
"1", "3", "!a",; properties: trans-labels explicit-labels state-acc
"3", "3", "!a", "0"; --BODY--
"2", "0", "!a",; State: 0
"2", "2", "a",; [!0] 0
"2", "3", "!a",; [0] 1
"2", "5", "a",; [!0] 2
"5", "3", "!a", "0"; State: 1
"5", "5", "a", "0"; [!0] 0
[0] 3
[!0] 2
State: 2 {0}
[!0] 2
State: 3
[!0] 0
[0] 3
[!0] 2
[0] 4
State: 4 {0}
[!0] 2
[0] 4
--END--
EOF EOF
run 0 ../ltl2tgba -H -DC -XH in.hoa > out.hoa
run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba run 1 ../../bin/autfilt -q --are-isomorph in.hoa out.hoa
# FIXME: use are-isomorphic once it is available run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa
diff out.tgba ex.tgba
run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba
cat >ex.tgba <<EOF cat >ex.tgba <<EOF