diff --git a/NEWS b/NEWS index 4e0e249cf..1843b7915 100644 --- a/NEWS +++ b/NEWS @@ -117,7 +117,10 @@ New in spot 1.99b (not yet released) the same %-escape sequences that are available for --stats or --format. - - All tools that output automata have a --check option that + - all tools that output formulas have a -0 option to separate + formulas with \0. This helps in conjunction with xargs -0. + + - all tools that output automata have a --check option that request extra checks to be performed on the output to fill in properties values for the HOA format. This options implies -H for HOA output. For instance diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 920dccc9b..3c3ed2504 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -39,6 +39,7 @@ enum { output_format_t output_format = spot_output; bool full_parenth = false; bool escape_csv = false; +char output_terminator = '\n'; static const argp_option options[] = { @@ -58,6 +59,9 @@ static const argp_option options[] = "send output to a file named FORMAT instead of standard output. The" " first formula sent to a file truncates it unless FORMAT starts" " with '>>'.", 0 }, + { "zero-terminated-output", '0', 0, 0, + "separate output formulas with \\0 instead of \\n " + "(for use with xargs -0)", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -212,6 +216,9 @@ parse_opt_output(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { + case '0': + output_terminator = 0; + break; case '8': output_format = utf8_output; break; @@ -304,7 +311,7 @@ output_formula_checked(const spot::ltl::formula* f, out = &p.first->second->ostream(); } output_formula(*out, f, filename, linenum, prefix, suffix); - *out << '\n'; + *out << output_terminator; // Make sure we abort if we can't write to std::cout anymore // (like disk full or broken pipe with SIGPIPE ignored). check_cout(); diff --git a/src/tests/ltlfilt.test b/src/tests/ltlfilt.test index 0b35e75e2..0ded87f7c 100755 --- a/src/tests/ltlfilt.test +++ b/src/tests/ltlfilt.test @@ -25,10 +25,12 @@ set -e +ltlfilt=../../bin/ltlfilt + checkopt() { cat >exp - run 0 ../../bin/ltlfilt "$@" formulas > out + run 0 $ltlfilt "$@" formulas > out diff exp out } @@ -168,7 +170,7 @@ p0 & GFp1 & FGp1 p0 | Gp1 | FG(p2 | Xp3) EOF -run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out +run 0 $ltlfilt -u --nnf --relabel-bool=pnn in >out diff exp out cat >exp <p1 && <>[]p1 p0 || []p1 || <>[](p2 || Xp3) EOF -run 0 ../../bin/ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out +run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out diff exp out cat >exp <exp <out +run 0 $ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out +diff exp out + +run 0 $ltlfilt -0 in > out +perl -i -pe 's/\0/@\n/g' out +cat >exp < stderr && exit 1 +$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1 test $? = 2 grep 'non-LTL' stderr SPOT_STUTTER_CHECK=555 \ -../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1 +$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1 test $? = 2 grep 'invalid' stderr SPOT_STUTTER_CHECK=5 \ -../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' +$ltlfilt --stutter-invariant -f '!{a:b*:c}' # This one was incorrectly diagnosed as stutter invariant because of a # bug in the bitvectors. -../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1 +$ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1 -../../bin/ltlfilt -c -o 'foo' -f a 2>stderr && exit 1 +$ltlfilt -c -o 'foo' -f a 2>stderr && exit 1 grep 'ltlfilt: options --output and --count are incompatible' stderr true