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

* src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files.

Browse source 
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS,
libltlvisit_la_SOURCES): Distribute them.
* src/ltltest/randltl.cc: New file.
* src/ltltest/Makefile.am (LDADD): Link with ../libspot.la directly.
(noinst_PROGRAMS, randltl_SOURCES): New.
(EXTRA_DIST, CLEANFILES): The list of random formulae is now generated.
* src/ltltest/formulae.txt: Delete.
* src/ltltest/reduc.test: Use randltl to generate formulae.
* src/ltlvisit/length.cc (length_visitor): Fix computation
of the length of multops.
* src/ltlvisit/length.hh (length): Document the length of multops.
This commit is contained in:
Alexandre Duret-Lutz 2005-01-05 16:20:21 +00:00
parent 7216701631
commit e366b081a8
10 changed files with 573 additions and 2214 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ltlvisit/Makefile.am
View file

@ -1,4 +1,4 @@
## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
## 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.
##
@ -35,6 +35,7 @@ ltlvisit_HEADERS = \
lunabbrev.hh \
nenoform.hh \
postfix.hh \
randomltl.hh \
reduce.hh \
simpfg.hh \
syntimpl.hh \
@ -53,6 +54,7 @@ libltlvisit_la_SOURCES = \
lunabbrev.cc \
nenoform.cc \
postfix.cc \
randomltl.cc \
reduce.cc \
simpfg.cc \
syntimpl.cc \

3
src/ltlvisit/length.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// 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.
//
@ -77,6 +77,7 @@ namespace spot
visit(const multop* mo)
{
unsigned mos = mo->size();
++result_;
for (unsigned i = 0; i < mos; ++i)
result_ += length(mo->nth(i));
}

7
src/ltlvisit/length.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// 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.
//
@ -33,7 +33,10 @@ namespace spot
///
/// The length of a formula is the number of atomic properties,
/// constants, and operators (logical and temporal) occurring in
/// the formula.
/// the formula. spot::ltl::multops count only for 1, even if
/// they have more than two operands (e.g. <code>a | b | c</code>
/// has length 4, because <code>|</code> is represented once
/// internally).
int length(const formula* f);
}
}

247
src/ltlvisit/randomltl.cc Normal file
View file

@ -0,0 +1,247 @@
// Copyright (C) 2005 Laboratoire d'Informatique de 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.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cassert>
#include <algorithm>
#include "randomltl.hh"
#include "ltlast/allnodes.hh"
#include "misc/random.hh"
#include <iostream>
namespace spot
{
namespace ltl
{
namespace
{
formula*
ap_builder(const random_ltl* rl, int n)
{
assert(n == 1);
(void) n;
atomic_prop_set::const_iterator i = rl->ap()->begin();
std::advance(i, mrand(rl->ap()->size()));
return (*i)->ref();
}
formula*
true_builder(const random_ltl*, int n)
{
assert(n == 1);
(void) n;
return constant::true_instance();
}
formula*
false_builder(const random_ltl*, int n)
{
assert(n == 1);
(void) n;
return constant::false_instance();
}
template <unop::type Op>
formula*
unop_builder(const random_ltl* rl, int n)
{
assert(n >= 2);
return unop::instance(Op, rl->generate(n - 1));
}
template <binop::type Op>
formula*
binop_builder(const random_ltl* rl, int n)
{
assert(n >= 3);
--n;
int l = rrand(1, n - 1);
return binop::instance(Op, rl->generate(l), rl->generate(n - l));
}
template <multop::type Op>
formula*
multop_builder(const random_ltl* rl, int n)
{
assert(n >= 3);
--n;
int l = rrand(1, n - 1);
return multop::instance(Op, rl->generate(l), rl->generate(n - l));
}
} // anonymous
void
random_ltl::op_proba::setup(const char* name, int min_n, builder build)
{
this->name = name;
this->min_n = min_n;
this->proba = 1.0;
this->build = build;
}
namespace
{
const int proba_size = 14;
}
random_ltl::random_ltl(const atomic_prop_set* ap)
{
ap_ = ap;
proba_ = new op_proba[proba_size];
proba_[0].setup("ap", 1, ap_builder);
proba_[1].setup("false", 1, false_builder);
proba_[2].setup("true", 1, true_builder);
proba_2_ = proba_ + 3;
proba_[3].setup("not", 2, unop_builder<unop::Not>);
proba_[4].setup("F", 2, unop_builder<unop::F>);
proba_[5].setup("G", 2, unop_builder<unop::G>);
proba_[6].setup("X", 2, unop_builder<unop::X>);
proba_[7].setup("equiv", 3, binop_builder<binop::Equiv>);
proba_[8].setup("implies", 3, binop_builder<binop::Implies>);
proba_[9].setup("xor", 3, binop_builder<binop::Xor>);
proba_[10].setup("R", 3, binop_builder<binop::R>);
proba_[11].setup("U", 3, binop_builder<binop::U>);
proba_[12].setup("and", 3, multop_builder<multop::And>);
proba_[13].setup("or", 3, multop_builder<multop::Or>);
proba_[0].proba = ap_->size();
update_sums();
}
random_ltl::~random_ltl()
{
delete[] proba_;
}
void
random_ltl::update_sums()
{
total_1_ = 0.0;
total_2_ = 0.0;
total_2_and_more_ = 0.0;
for (int i = 0; i < proba_size; ++i)
{
if (proba_[i].min_n == 1)
total_1_ += proba_[i].proba;
else if (proba_[i].min_n == 2)
total_2_ += proba_[i].proba;
else if (proba_[i].min_n > 2)
total_2_and_more_ += proba_[i].proba;
else
assert(!"un expected max_n");
}
total_2_and_more_ += total_2_;
assert(total_1_ != 0.0);
assert(total_2_ != 0.0);
assert(total_2_and_more_ != 0.0);
}
formula*
random_ltl::generate(int n) const
{
assert(n > 0);
if (n == 1)
{
double r = drand() * total_1_;
op_proba* p = proba_;
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
assert(p->min_n == 1);
return p->build(this, n);
}
else if (n == 2)
{
double r = drand() * total_2_;
op_proba* p = proba_2_;
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
assert(p->min_n == 2);
return p->build(this, n);
}
else
{
double r = drand() * total_2_and_more_;
op_proba* p = proba_2_;
double s = p->proba;
while (s < r)
{
++p;
s += p->proba;
}
assert(p->min_n >= 2);
return p->build(this, n);
}
}
const char*
random_ltl::parse_options(char* options)
{
char* key = strtok(options, "=\t, :;");
while (key)
{
char* value = strtok(0, "=\t, :;");
if (value == 0)
return key;
char* endptr;
double res = strtod(value, &endptr);
if (*endptr)
return value;
int i;
for (i = 0; i < proba_size; ++i)
{
if (('a' <= *proba_[i].name && *proba_[i].name <= 'z'
&& !strcasecmp(proba_[i].name, key))
|| !strcmp(proba_[i].name, key))
{
proba_[i].proba = res;
break;
}
}
if (i == proba_size)
return key;
key = strtok(0, "=\t, :;");
}
update_sums();
return 0;
}
std::ostream&
random_ltl::dump_priorities(std::ostream& os) const
{
for (int i = 0; i < proba_size; ++i)
os << proba_[i].name << "\t" << proba_[i].proba << std::endl;
return os;
}
} // ltl
} // spot

136
src/ltlvisit/randomltl.hh Normal file
View file

@ -0,0 +1,136 @@
// Copyright (C) 2005 Laboratoire d'Informatique de 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.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_LTLVISIT_RANDOMLTL_HH
# define SPOT_LTLVISIT_RANDOMLTL_HH
#include "apcollect.hh"
#include <iosfwd>
namespace spot
{
namespace ltl
{
/// \brief Generate random LTL formulae.
/// \ingroup ltl_io
///
/// This class recursively construct LTL formulae of a given size.
/// The formulae will use the use atomic propositions from the
/// set of proposition passed to the constructor, in addition to the
/// constant and all LTL operators supported by Spot.
///
/// By default each operator has equal chance to be selected.
/// Also, each atomic proposition has as much chance as each
/// constant (i.e., true and false) to be picked. This can be
/// tuned using parse_options().
class random_ltl
{
public:
/// Create a random LTL generator using atomic propositions from \a ap.
random_ltl(const atomic_prop_set* ap);
~random_ltl();
/// \brief Generate a formula of size \a n.
///
/// It is possible to obtain formulae that are smaller than \a
/// n, because some simple simplifications are performed by the
/// AST. (For instance the formula <code>a | a</code> is
/// automatically reduced to <code>a</code> by spot::ltl::multop.)
///
/// Furthermore, for the purpose of this generator,
/// <code>a | b | c</code> has length 5, while it has length
/// <code>4</code> for spot::ltl::length().
formula* generate(int n) const;
/// \brief Print the priorities of each operator, constants,
/// and atomic propositions.
std::ostream& dump_priorities(std::ostream& os) const;
/// \brief Update the priorities used to generate LTL formulae.
///
/// The initial priorities are as follows.
///
/// \verbatim
/// ap n
/// false 1
/// true 1
/// not 1
/// F 1
/// G 1
/// X 1
/// equiv 1
/// implies 1
/// xor 1
/// R 1
/// U 1
/// and 1
/// or 1
/// \endverbatim
///
/// Where \c n is the number of atomic propositions in the
/// set passed to the constructor.
///
/// This means that each operator has equal chance to be
/// selected. Also, each atomic proposition has as much chance
/// as each constant (i.e., true and false) to be picked. This
/// can be
///
/// These priorities can be altered using this function.
/// \a options should be comma-separated list of KEY=VALUE
/// assignments, using keys from the above list.
/// For instance <code>"xor=0, F=3"</code> will prevent \c xor
/// from being used, and will raise the relative probability of
/// occurrences of the \c F operator.
const char* parse_options(char* options);
/// Return the set of atomic proposition used to build formulae.
const atomic_prop_set*
ap() const
{
return ap_;
}
protected:
void update_sums();
private:
struct op_proba
{
const char* name;
int min_n;
double proba;
typedef formula* (*builder)(const random_ltl* rl, int n);
builder build;
void setup(const char* name, int min_n, builder build);
};
op_proba* proba_;
double total_1_;
op_proba* proba_2_;
double total_2_;
double total_2_and_more_;
const atomic_prop_set* ap_;
};
}
}
#endif // SPOT_LTLVIST_RANDOMLTL_HH