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

bin: fix handling for --output & --format with LTL outputs

Browse source 
* bin/common_output.cc: Set the output stream for LTL formats.
* tests/core/serial.test: Add a test case about this issue that also
improve the covering of the previous patch about saving file
descriptors.
This commit is contained in:
Alexandre Duret-Lutz 2023-07-26 21:33:36 +02:00
parent 7f1a33cc61
commit 0923f8efe2
3 changed files with 18 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
tests/core/serial.test
View file

@ -78,3 +78,16 @@ test 2000 = `ls -l randaut-*.hoa | wc -l`
# likewise for LTL formulas
randltl 2 -n 2000 -o randltl-%l.ltl
test 2000 = `ls -l randltl-*.ltl | wc -l`
# Test the code path that works that has to reopen files
randltl -n100 --tree-size 1 26 --allow-dups -o '%f'.ltl --format=pass1
randltl -n100 --tree-size 1 26 --allow-dups -o '>>%f'.ltl --format=pass2
(uniq -c p1.ltl; uniq -c p20.ltl) | sed 's/^ *\([0-9][0-9]*\) */\1 /g' >out
cat >expected <<EOF
4 pass1
4 pass2
5 pass1
5 pass2
EOF
diff out expected