randltl: gracefully handle the absence of unary or binary operators.

* src/ltlvisit/randomltl.cc: Fix generation of formulas when unary or
binary operators are missing.
* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh
(destroy_atomic_prop_set): New function.
* src/bin/randltl.cc: Use it, and also honnor --boolean-priorities
when generating SEREs.
* src/ltltest/rand.test: New file.
* src/ltltest/Makefile.am: Add it.

src/ltltest/Makefile.am

@@ -1,8 +1,9 @@
-## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
+## Recherche et Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-## Université Pierre et Marie Curie.
+## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+## Université Pierre et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -101,6 +102,7 @@ TESTS = \
   latex.test \
   lbt.test \
   lenient.test \
+  rand.test \
   isop.test \
   syntimpl.test \
   reduc.test \

src/ltltest/rand.test

@@ -0,0 +1,99 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2014 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+set -e
+
+randltl=../../bin/randltl
+
+run 0 $randltl -S -n 20 a b c --tree-size=10 \
+    --sere-priorities=and=0,andNLM=0 \
+    --boolean-priorities=equiv=0,implies=0,xor=0,and=0,not=0 \
+    --dump-priorities > stdout
+
+cat >expected <<EOF
+Use --sere-priorities to set the following SERE priorities:
+eword	1
+boolform	1
+star	1
+star_b	1
+and	0
+andNLM	0
+or	1
+concat	1
+fusion	1
+Use --boolean-priorities to set the following Boolean formula priorities:
+ap	3
+false	1
+true	1
+not	0
+equiv	0
+implies	0
+xor	0
+and	0
+or	1
+EOF
+diff stdout expected
+
+
+run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \
+   --sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \
+   --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \
+   --dump-pr > stdout
+
+cat >expected <<EOF
+Use --sere-priorities to set the following SERE priorities:
+eword	0
+boolform	1
+star	0
+star_b	0
+and	0
+andNLM	0
+or	0
+concat	0
+fusion	0
+Use --boolean-priorities to set the following Boolean formula priorities:
+ap	3
+false	0
+true	0
+not	0
+equiv	0
+implies	0
+xor	0
+and	0
+or	0
+EOF
+diff stdout expected
+
+
+
+# Disabling all operators will prevent more formulas to be generated.
+$randltl -S -n 10000 a b c --tree-size=10..20 \
+ --sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \
+ --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out &&
+  exit 1
+sort out > out2
+cat >expected <<EOF
+a
+b
+c
+EOF
+
+diff expected out2