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

* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files.

Browse source 
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS)
(libtgbaalgos_la_SOURCES): Add them.
* src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public.
* src/tgbatest/randtgba.cc: New file.
* src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it.
* src/tgbatest/readsave.test: Check a random graph.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-12 17:24:46 +00:00
parent e54ddd46ed
commit 5bcb6091fd
8 changed files with 427 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,5 +1,13 @@
2004-11-12 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS)
(libtgbaalgos_la_SOURCES): Add them.
* src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public.
* src/tgbatest/randtgba.cc: New file.
* src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it.
* src/tgbatest/readsave.test: Check a random graph.
* misc/random.cc, misc/random.hh: New files.
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.

5
src/tgba/tgbaexplicit.hh
View file

@ -73,6 +73,10 @@ namespace spot
void complement_all_acceptance_conditions();
void merge_transitions();
/// Return the tgba_explicit::state for \a name, creating the state if
/// it does not exist.
state* add_state(const std::string& name);
// tgba interface
virtual ~tgba_explicit();
virtual spot::state* get_init_state() const;
@ -90,7 +94,6 @@ namespace spot
virtual bdd compute_support_conditions(const spot::state* state) const;
virtual bdd compute_support_variables(const spot::state* state) const;
state* add_state(const std::string& name);
bdd get_acceptance_condition(const ltl::formula* f);
typedef Sgi::hash_map<const std::string, tgba_explicit::state*,

2
src/tgbaalgos/Makefile.am
View file

@ -38,6 +38,7 @@ tgbaalgos_HEADERS = \
neverclaim.hh \
powerset.hh \
projrun.hh \
randomgraph.hh \
reachiter.hh \
replayrun.hh \
rundotdec.hh \
@ -58,6 +59,7 @@ libtgbaalgos_la_SOURCES = \
neverclaim.cc \
powerset.cc \
projrun.cc \
randomgraph.cc \
reachiter.cc \
replayrun.cc \
rundotdec.cc \

155
src/tgbaalgos/randomgraph.cc Normal file
View file

@ -0,0 +1,155 @@
// Copyright (C) 2004 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 "randomgraph.hh"
#include "tgba/tgbaexplicit.hh"
#include "misc/random.hh"
#include "ltlast/atomic_prop.hh"
#include "ltlvisit/destroy.hh"
#include <sstream>
#include <list>
#include <set>
namespace spot
{
namespace
{
std::string
st(int n)
{
std::stringstream s;
s << n;
return "S" + s.str();
}
std::string
acc(int n)
{
std::stringstream s;
s << n;
return "a" + s.str();
}
void
random_labels(tgba_explicit* aut,
const std::string& src, const std::string& dest,
const std::list<int>& props, float t,
const std::list<bdd>& accs, float a)
{
bdd p = bddtrue;
for (std::list<int>::const_iterator i = props.begin();
i != props.end(); ++i)
p &= (drand() < t ? bdd_ithvar : bdd_nithvar)(*i);
bdd ac = bddfalse;
for (std::list<bdd>::const_iterator i = accs.begin();
i != accs.end(); ++i)
if (drand() < a)
ac |= *i;
tgba_explicit::transition* u = aut->create_transition(src, dest);
aut->add_conditions(u, p);
aut->add_acceptance_conditions(u, ac);
}
}
tgba*
random_graph(int n, float d,
const ltl::atomic_prop_set* ap, bdd_dict* dict,
int n_acc, float a, float t,
ltl::environment* env)
{
tgba_explicit* res = new tgba_explicit(dict);
std::list<int> props;
for (ltl::atomic_prop_set::const_iterator i = ap->begin();
i != ap->end(); ++i)
props.push_back(dict->register_proposition(*i, res));
std::list<bdd> accs;
bdd allneg = bddtrue;
for (int i = 0; i < n_acc; ++i)
{
ltl::formula* f = env->require(acc(i));
int v = dict->register_acceptance_variable(f, res);
ltl::destroy(f);
allneg &= bdd_nithvar(v);
bdd b = bdd_ithvar(v);
accs.push_back(b);
}
for (std::list<bdd>::iterator i = accs.begin(); i != accs.end(); ++i)
*i &= bdd_exist(allneg, *i);
typedef std::set<std::string> node_set;
node_set nodes_to_process;
node_set unreachable_nodes;
nodes_to_process.insert(st(0));
for (int i = 1; i < n; ++i)
unreachable_nodes.insert(st(i));
while (!nodes_to_process.empty())
{
std::string src = *nodes_to_process.begin();
nodes_to_process.erase(nodes_to_process.begin());
if (!unreachable_nodes.empty())
{
// Pick a random unreachable node.
int index = mrand(unreachable_nodes.size());
node_set::const_iterator i;
for (i = unreachable_nodes.begin(); index; ++i, --index)
assert(i != unreachable_nodes.end());
// Link it from src.
random_labels(res, src, *i, props, t, accs, a);
nodes_to_process.insert(*i);
unreachable_nodes.erase(i);
}
// Randomly link node to another node (including itself).
for (int i = 0; i < n; ++i)
{
if (drand() >= d)
continue;
std::string dest = st(i);
random_labels(res, src, dest, props, t, accs, a);
node_set::iterator j = unreachable_nodes.find(dest);
if (j != unreachable_nodes.end())
{
nodes_to_process.insert(dest);
unreachable_nodes.erase(j);
}
}
// Avoid dead ends.
if (res->add_state(src)->empty())
random_labels(res, src, src, props, t, accs, a);
}
return res;
}
}

76
src/tgbaalgos/randomgraph.hh Normal file
View file

@ -0,0 +1,76 @@
// Copyright (C) 2004 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_TGBAALGOS_RANDOMGRAPH_HH
# define SPOT_TGBAALGOS_RANDOMGRAPH_HH
#include "ltlvisit/apcollect.hh"
#include "ltlenv/defaultenv.hh"
namespace spot
{
class bdd_dict;
class tgba;
/// \brief Construct a tgba randomly.
///
/// \param n The number of states wanted in the automata. All states
/// will be connected, and there will be no dead state.
/// \param d The density of the automata. This is the probability
/// (between 0.0 and 1.0), to add a transition between two
/// states. All states have at least one outgoing transition,
/// so \a d is considered only when adding the remaining transition.
/// A density of 1 means all states will be connected to each other.
/// \param ap The list of atomic property that should label the transition.
/// \param dict The bdd_dict to used for this automata.
/// \param n_acc The number of acceptance sets to use.
/// \param a The probability (between 0.0 and 1.0) that a transition belongs
/// to an acceptance set.
/// \param t The probability (between 0.0 and 1.0) that an atomic proposition
/// is true.
/// \param env The environment in which to declare the acceptance conditions.
///
/// This algorithms is adapted from the one in Fig 6.2 page 48 of
/// \verbatim
/// @TechReport{ tauriainen.00.a66,
/// author = {Heikki Tauriainen},
/// title = {Automated Testing of {B\"u}chi Automata Translators for
/// {L}inear {T}emporal {L}ogic},
/// address = {Espoo, Finland},
/// institution = {Helsinki University of Technology, Laboratory for
/// Theoretical Computer Science},
/// number = {A66},
/// year = {2000},
/// url = {http://citeseer.nj.nec.com/tauriainen00automated.html},
/// type = {Research Report},
/// note = {Reprint of Master's thesis}
/// }
/// \endverbatim
/// The only difference is that labels are on transitions, and that
/// acceptance conditions are handled. Otherwise the logic is the same.
tgba*
random_graph(int n, float d,
const ltl::atomic_prop_set* ap, bdd_dict* dict,
int n_acc = 0, float a = 0.1, float t = 0.5,
ltl::environment* env = &ltl::default_environment::instance());
}
#endif // SPOT_TGBAALGOS_RANDOMGRAPH_HH

7
src/tgbatest/Makefile.am
View file

@ -23,9 +23,9 @@ AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = ../libspot.la
# This is the most used test program, and it's also useful
# to run manually outside the test suite. Always build it.
noinst_PROGRAMS = ltl2tgba
# These are the most used test programs, and they are also useful
# to run manually outside the test suite. Always build them.
noinst_PROGRAMS = ltl2tgba randtgba
check_SCRIPTS = defs
# Keep this sorted alphabetically.
@ -54,6 +54,7 @@ ltl2tgba_SOURCES = ltl2tgba.cc
ltlprod_SOURCES = ltlprod.cc
mixprod_SOURCES = mixprod.cc
powerset_SOURCES = powerset.cc
randtgba_SOURCES = randtgba.cc
readsave_SOURCES = readsave.cc
reductgba_SOURCES = reductgba.cc
reduccmp_SOURCES = reductgba.cc

163
src/tgbatest/randtgba.cc Normal file
View file

@ -0,0 +1,163 @@
// Copyright (C) 2004 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 <cstdlib>
#include <iostream>
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/destroy.hh"
#include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/save.hh"
#include "ltlenv/defaultenv.hh"
#include "ltlast/atomic_prop.hh"
#include "tgbaalgos/dotty.hh"
#include "misc/random.hh"
void
syntax(char* prog)
{
std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
<< std::endl
<< "Options:" << std::endl
<< " -a N F number of accepence conditions a propability that"
<< " one is true [0 0.0]" << std::endl
<< " -d F density of the graph [0.2]" << std::endl
<< " -g output in dot format" << std::endl
<< " -n N number of nodes of the graph [20]" << std::endl
<< " -s N seed for the random number generator" << std::endl
<< " -t F probability of the atomic propositions to be true"
<< " [0.5]"
<< std::endl
<< "Where:" << std::endl
<< " F are floats between 0.0 and 1.0 inclusive" << std::endl
<< " N are positive integers" << std::endl
<< " PROPS are the atomic properties to use on transitions"
<< std::endl;
exit(2);
}
int
to_int(const char* s)
{
char* endptr;
int res = strtol(s, &endptr, 10);
if (*endptr)
{
std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
exit(1);
}
return res;
}
float
to_float(const char* s)
{
char* endptr;
float res = strtof(s, &endptr);
if (*endptr)
{
std::cerr << "Failed to parse `" << s << "' as a float." << std::endl;
exit(1);
}
return res;
}
int
main(int argc, char** argv)
{
int opt_n_acc = 0;
float opt_a = 0.0;
float opt_d = 0.2;
int opt_n = 20;
float opt_t = 0.5;
bool opt_dot = false;
int argn = 0;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
if (argc <= 1)
syntax(argv[0]);
while (++argn < argc)
{
if (!strcmp(argv[argn], "-a"))
{
if (argc < argn + 3)
syntax(argv[0]);
opt_n_acc = to_int(argv[++argn]);
opt_a = to_float(argv[++argn]);
}
else if (!strcmp(argv[argn], "-d"))
{
if (argc < argn + 1)
syntax(argv[0]);
opt_d = to_float(argv[++argn]);
}
else if (!strcmp(argv[argn], "-g"))
{
opt_dot = true;
}
else if (!strcmp(argv[argn], "-n"))
{
if (argc < argn + 1)
syntax(argv[0]);
opt_n = to_int(argv[++argn]);
}
else if (!strcmp(argv[argn], "-s"))
{
if (argc < argn + 1)
syntax(argv[0]);
spot::srand(to_int(argv[++argn]));
}
else if (!strcmp(argv[argn], "-t"))
{
if (argc < argn + 1)
syntax(argv[0]);
opt_t = to_float(argv[++argn]);
}
else
{
ap->insert(static_cast<spot::ltl::atomic_prop*>
(env.require(argv[argn])));
}
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba* a = spot::random_graph(opt_n, opt_d, ap, dict,
opt_n_acc, opt_a, opt_t, &env);
if (opt_dot)
dotty_reachable(std::cout, a);
else
tgba_save_reachable(std::cout, a);
for (spot::ltl::atomic_prop_set::iterator i = ap->begin();
i != ap->end(); ++i)
spot::ltl::destroy(*i);
delete a;
delete dict;
delete ap;
return 0;
}

16
src/tgbatest/readsave.test
View file

@ -56,4 +56,18 @@ sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout
diff input stdout
rm input stdout expected
rm -f input stdout expected
# Likewise, with a randomly generated TGBA.
run 0 ./randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' input > tmp_ &&
mv tmp_ input
cat input
run 0 ./readsave input > stdout
sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout > tmp_ &&
mv tmp_ stdout
diff input stdout
rm -f input stdout