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

autfilt: support --stats=%L to display the automaton location

Browse source 
* src/bin/autfilt.cc: Add support for %L.
* src/tgbatest/hoaparse.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-11 15:45:14 +01:00
parent ac225c0ee9
commit 9c672ac49b
2 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/bin/autfilt.cc
View file

@ -102,6 +102,8 @@ static const argp_option options[] =
" minuscules for output):", 4 }, " minuscules for output):", 4 },
{ "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"name of the input file", 0 }, "name of the input file", 0 },
{ "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"location in the input file", 0 },
{ "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"number of states", 0 }, "number of states", 0 },
{ "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
@ -324,6 +326,7 @@ namespace
declare('E', &haut_edges_); declare('E', &haut_edges_);
declare('F', &filename_); declare('F', &filename_);
declare('f', &filename_); // Override the formula printer. declare('f', &filename_); // Override the formula printer.
declare('L', &haut_loc_);
declare('S', &haut_states_); declare('S', &haut_states_);
declare('T', &haut_trans_); declare('T', &haut_trans_);
} }
@ -338,6 +341,7 @@ namespace
const char* filename, double run_time) const char* filename, double run_time)
{ {
filename_ = filename; filename_ = filename;
haut_loc_ = haut->loc;
if (has('T')) if (has('T'))
{ {
@ -373,6 +377,7 @@ namespace
spot::printable_value<unsigned> haut_trans_; spot::printable_value<unsigned> haut_trans_;
spot::printable_value<unsigned> haut_acc_; spot::printable_value<unsigned> haut_acc_;
spot::printable_value<unsigned> haut_scc_; spot::printable_value<unsigned> haut_scc_;
spot::printable_value<spot::location> haut_loc_;
}; };

10
src/tgbatest/hoaparse.test
View file

@ -26,7 +26,7 @@ set -e
expecterr() expecterr()
{ {
cat >$1.exp cat >$1.exp
../../bin/autfilt --hoa $1 2>$1.err >$1.out && exit 1 ../../bin/autfilt --hoa "$@" 2>$1.err >$1.out && exit 1
test $? = 2 test $? = 2
cat $1.err cat $1.err
diff $1.err $1.exp diff $1.err $1.exp
@ -35,7 +35,7 @@ expecterr()
expectok() expectok()
{ {
cat >$1.exp cat >$1.exp
../../bin/autfilt --hoa $1 >$1.out ../../bin/autfilt --hoa "$@" >$1.out
test $? = 0 test $? = 0
cat $1.out cat $1.out
diff $1.out $1.exp diff $1.out $1.exp
@ -383,6 +383,7 @@ cat >input <<EOF
[!@a & @bc] 0 {1} [!@a & @bc] 0 {1}
[@a & @bc] 0 {0 1} [@a & @bc] 0 {0 1}
--END-- --END--
/* Some comment */
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
@ -425,6 +426,11 @@ State: 1
--END-- --END--
EOF EOF
expectok input --stats='%F:%L' <<EOF
input:1.5-16.11
input:18.1-26.7
EOF
cat >input <<EOF cat >input <<EOF
HOA: v1 HOA: v1
--ABORT-- --ABORT--