From 50bdc24514de41e06f5cdb8110d6671f8c8f55a4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 5 Feb 2014 18:10:48 +0100 Subject: [PATCH] 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/bin/randltl.cc | 14 +++--- src/ltltest/Makefile.am | 10 ++-- src/ltltest/rand.test | 99 +++++++++++++++++++++++++++++++++++++++ src/ltlvisit/apcollect.cc | 10 +++- src/ltlvisit/apcollect.hh | 9 +++- src/ltlvisit/randomltl.cc | 32 +++++++++++-- 6 files changed, 154 insertions(+), 20 deletions(-) create mode 100755 src/ltltest/rand.test diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 243bc7a1f..b3730f31d 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -283,7 +283,8 @@ main(int argc, char** argv) break; case OutputSERE: rf = rs = new spot::ltl::random_sere(&aprops); - tok_pS = rf->parse_options(opt_pS); + tok_pS = rs->parse_options(opt_pS); + tok_pB = rs->rb.parse_options(opt_pB); if (opt_pL) error(2, 0, "option --ltl-priorities unsupported for SERE output"); break; @@ -335,6 +336,7 @@ main(int argc, char** argv) default: error(2, 0, "internal error: unknown type of output"); } + destroy_atomic_prop_set(aprops); exit(0); } @@ -409,10 +411,6 @@ main(int argc, char** argv) (*i)->destroy(); } // Cleanup the atomic_prop set. - { - spot::ltl::atomic_prop_set::const_iterator i = aprops.begin(); - while (i != aprops.end()) - (*(i++))->destroy(); - } + destroy_atomic_prop_set(aprops); return 0; } diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 887530240..f241a6443 100644 --- a/src/ltltest/Makefile.am +++ b/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 \ diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test new file mode 100755 index 000000000..b7750582c --- /dev/null +++ b/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 . + +. ./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 < stdout + +cat >expected < out && + exit 1 +sort out > out2 +cat >expected <destroy(); + } + + atomic_prop_set* atomic_prop_collect(const formula* f, atomic_prop_set* s) { diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 480480b0e..382f203ea 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -40,6 +40,11 @@ namespace spot typedef std::set atomic_prop_set; + /// \brief Destroy all the atomic propositions in an + /// atomic_prop_set. + SPOT_API void + destroy_atomic_prop_set(atomic_prop_set& as); + /// \brief Return the set of atomic propositions occurring in a formula. /// /// \param f the formula to inspect diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 99c268cf6..029e77692 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -191,9 +191,7 @@ namespace spot else assert(!"unexpected max_n"); } - assert(total_1_ != 0.0); - assert(total_2_ != 0.0); - assert(total_2_and_more_ != 0.0); + assert(total_2_and_more_ >= total_2_); } const formula* @@ -204,6 +202,30 @@ namespace spot double r = drand(); op_proba* p; + // Approximate impossible cases. + if (n == 1 && total_1_ == 0.0) + { + if (total_2_ != 0.0) + n = 2; + else + n = 3; + } + else if (n == 2 && total_2_ == 0.0) + { + if (total_1_ != 0.0) + n = 1; + else + n = 3; + } + else if (n > 2 && total_2_and_more_ == 0.0) + { + if (total_1_ != 0.0) + n = 1; + else + assert(total_2_ == 0.0); + } + + if (n == 1) { r *= total_1_;