randltl: fix generation without unary operators

* spot/tl/randomltl.hh (has_unary_ops): New method.
* spot/tl/randomltl.cc: Avoid creating subformulas of even size
when we do not have unary operators.
* tests/core/randpsl.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2024-08-21 21:36:54 +02:00
parent bdc63db9f0
commit 97832af321
4 changed files with 61 additions and 6 deletions

View file

@ -36,3 +36,21 @@ test `wc -l < formulas` = 50
randltl --psl --sere-priorities=first_match=10 -n 100 2 | grep first_match
# the random generator had trouble generating formulas of the proper size when
# unary operators were disabled
P=true=0,false=0,not=0
randltl --tree-size=19 -B --boolean-prio=$P 1000 -n10 --stats=%a >out
cat >expected <<EOF
10
10
10
10
10
10
10
10
10
10
EOF
diff expected out