Commit c0e98912 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

randomize: new function

* src/tgbaalgos/randomize.cc, src/tgbaalgos/randomize.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/graph/graph.hh (rename_states_): New method.
* src/bin/autfilt.cc: Add options --randomize and --seed.
* src/tgbatest/randomize.test: Test them.
* src/tgbatest/Makefile.am: Add randomize.test.
* NEWS: Mention randomize().
parent 0db0eca1
...@@ -43,6 +43,10 @@ New in spot 1.99a (not yet released) ...@@ -43,6 +43,10 @@ New in spot 1.99a (not yet released)
used in a stream. The parser currently ignore all optional used in a stream. The parser currently ignore all optional
headers (starting with a lowercase letter). headers (starting with a lowercase letter).
- randomize() is a new algorithm that reorder the states
and transition of an automaton at random. It can be
used from the command-line using "autfilt --randomize".
- Spot is now compiling in C++11 mode. The set of features we use - Spot is now compiling in C++11 mode. The set of features we use
requires GCC >= 4.6 or Clang >= 3.1. These minimum versions requires GCC >= 4.6 or Clang >= 3.1. These minimum versions
are old enough that it should not be an issue to most people. are old enough that it should not be an issue to most people.
......
...@@ -39,11 +39,13 @@ ...@@ -39,11 +39,13 @@
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "misc/optionmap.hh" #include "misc/optionmap.hh"
#include "misc/timer.hh" #include "misc/timer.hh"
#include "misc/random.hh"
#include "hoaparse/public.hh" #include "hoaparse/public.hh"
#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/randomize.hh"
const char argp_program_doc[] ="\ static const char argp_program_doc[] ="\
Convert, transform, and filter Büchi automata.\n\ Convert, transform, and filter Büchi automata.\n\
"; ";
...@@ -53,6 +55,8 @@ Convert, transform, and filter Büchi automata.\n\ ...@@ -53,6 +55,8 @@ Convert, transform, and filter Büchi automata.\n\
#define OPT_LBTT 3 #define OPT_LBTT 3
#define OPT_SPOT 4 #define OPT_SPOT 4
#define OPT_STATS 5 #define OPT_STATS 5
#define OPT_RANDOMIZE 6
#define OPT_SEED 7
static const argp_option options[] = static const argp_option options[] =
{ {
...@@ -111,24 +115,44 @@ static const argp_option options[] = ...@@ -111,24 +115,44 @@ static const argp_option options[] =
{ "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 }, "a single %", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Transformation:", -1 },
{ "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
"randomize states and transitions (specify 's' or 't' to"
"randomize only states or transitions)", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ "extra-options", 'x', "OPTS", 0, { "extra-options", 'x', "OPTS", 0,
"fine-tuning options (see spot-x (7))", 0 }, "fine-tuning options (see spot-x (7))", 0 },
{ "seed", OPT_SEED, "INT", 0,
"seed for the random number generator (0)", 0 },
{ 0, 0, 0, 0, 0, 0 } { 0, 0, 0, 0, 0, 0 }
}; };
const struct argp_child children[] = static const struct argp_child children[] =
{ {
{ &post_argp_disabled, 0, 0, 20 }, { &post_argp_disabled, 0, 0, 20 },
{ &misc_argp, 0, 0, -1 }, { &misc_argp, 0, 0, -1 },
{ 0, 0, 0, 0 } { 0, 0, 0, 0 }
}; };
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa }
bool utf8 = false; format = Dot;
const char* stats = ""; static const char* stats = "";
const char* hoa_opt = 0; static const char* hoa_opt = 0;
spot::option_map extra_options; static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
static int
to_int(const char* s)
{
char* endptr;
int res = strtol(s, &endptr, 10);
if (*endptr)
error(2, 0, "failed to parse '%s' as an integer.", s);
return res;
}
static int static int
parse_opt(int key, char* arg, struct argp_state*) parse_opt(int key, char* arg, struct argp_state*)
...@@ -180,6 +204,31 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -180,6 +204,31 @@ parse_opt(int key, char* arg, struct argp_state*)
format = Lbtt; format = Lbtt;
} }
break; break;
case OPT_RANDOMIZE:
if (arg)
{
for (auto p = arg; *p; ++p)
switch (*p)
{
case 's':
randomize_st = true;
break;
case 't':
randomize_tr = true;
break;
default:
error(2, 0, "unknown argument for --randomize: '%c'", *p);
}
}
else
{
randomize_tr = true;
randomize_st = true;
}
break;
case OPT_SEED:
opt_seed = to_int(arg);
break;
case OPT_SPOT: case OPT_SPOT:
format = Spot; format = Spot;
break; break;
...@@ -301,6 +350,9 @@ namespace ...@@ -301,6 +350,9 @@ namespace
auto aut = post.run(haut->aut, nullptr); auto aut = post.run(haut->aut, nullptr);
const double conversion_time = sw.stop(); const double conversion_time = sw.stop();
if (randomize_st || randomize_tr)
spot::randomize(aut, randomize_st, randomize_tr);
switch (format) switch (format)
{ {
case Dot: case Dot:
...@@ -385,6 +437,8 @@ main(int argc, char** argv) ...@@ -385,6 +437,8 @@ main(int argc, char** argv)
if (jobs.empty()) if (jobs.empty())
jobs.emplace_back("-", true); jobs.emplace_back("-", true);
spot::srand(opt_seed);
spot::postprocessor post(&extra_options); spot::postprocessor post(&extra_options);
post.set_pref(pref | comp); post.set_pref(pref | comp);
post.set_type(type); post.set_type(type);
......
...@@ -725,6 +725,21 @@ namespace spot ...@@ -725,6 +725,21 @@ namespace spot
//dump_storage(std::cerr); //dump_storage(std::cerr);
} }
// Rename all the states in the transition vector. The
// transitions_ vector is left in a state that is incorrect and
// should eventually be fixed by a call to chain_transitions_()
// before any iteration on the successor of a state is performed.
void rename_states_(const std::vector<unsigned>& newst)
{
assert(newst.size() == states_.size());
unsigned tend = transitions_.size();
for (unsigned t = 1; t < tend; t++)
{
transitions_[t].dst = newst[transitions_[t].dst];
transitions_[t].src = newst[transitions_[t].src];
}
}
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states) void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
{ {
assert(newst.size() == states_.size()); assert(newst.size() == states_.size());
......
...@@ -57,6 +57,7 @@ tgbaalgos_HEADERS = \ ...@@ -57,6 +57,7 @@ tgbaalgos_HEADERS = \
product.hh \ product.hh \
projrun.hh \ projrun.hh \
randomgraph.hh \ randomgraph.hh \
randomize.hh \
reachiter.hh \ reachiter.hh \
reducerun.hh \ reducerun.hh \
replayrun.hh \ replayrun.hh \
...@@ -108,6 +109,7 @@ libtgbaalgos_la_SOURCES = \ ...@@ -108,6 +109,7 @@ libtgbaalgos_la_SOURCES = \
product.cc \ product.cc \
projrun.cc \ projrun.cc \
randomgraph.cc \ randomgraph.cc \
randomize.cc \
reachiter.cc \ reachiter.cc \
reducerun.cc \ reducerun.cc \
replayrun.cc \ replayrun.cc \
......
// -*- 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/>.
#include <algorithm>
#include <numeric>
#include "randomize.hh"
#include "misc/random.hh"
namespace spot
{
SPOT_API void
randomize(tgba_digraph_ptr& aut, bool randomize_states,
bool randomize_transitions)
{
if (!randomize_states && !randomize_transitions)
return;
auto& g = aut->get_graph();
if (randomize_states)
{
unsigned n = g.num_states();
std::vector<unsigned> nums(n);
std::iota(nums.begin(), nums.end(), 0);
std::random_shuffle(nums.begin(), nums.end(), spot::mrand);
g.rename_states_(nums);
aut->set_init_state(nums[aut->get_init_state_number()]);
}
if (randomize_transitions)
{
auto begin = g.transitions().begin() + 1;
auto end = g.transitions().end();
std::random_shuffle(begin, end, spot::mrand);
}
typedef tgba_digraph::graph_t::trans_storage_t tr_t;
g.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
{ return lhs.src < rhs.src; });
g.chain_transitions_();
}
}
// -*- 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/>.
#ifndef SPOT_TGBAALGOS_RANDOMIZE_HH
# define SPOT_TGBAALGOS_RANDOMIZE_HH
#include "tgba/tgbagraph.hh"
namespace spot
{
/// \brief Randomize a TGBA
///
/// Make a random permutation of the state, and of the transitions
/// leaving this state.
SPOT_API void
randomize(tgba_digraph_ptr& aut,
bool randomize_states = true,
bool randomize_transitions = true);
}
#endif // SPOT_TGBAALGOS_RANDOMGRAPH_HH
...@@ -104,6 +104,7 @@ TESTS = \ ...@@ -104,6 +104,7 @@ TESTS = \
degenid.test \ degenid.test \
degenlskip.test \ degenlskip.test \
kv.test \ kv.test \
randomize.test \
lbttparse.test \ lbttparse.test \
scc.test \ scc.test \
sccsimpl.test \ sccsimpl.test \
......
#!/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
ltl2tgba=../../bin/ltl2tgba
autfilt=../../bin/autfilt
$ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out
cat >expected <<EOF
HOA: v1
name: "Ga | Gb | Gc | Gd"
States: 5
Start: 0
AP: 4 "a" "b" "c" "d"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0] 1
[1] 2
[2] 3
[3] 4
State: 1
[0] 1
State: 2
[1] 2
State: 3
[2] 3
State: 4
[3] 4
--END--
EOF
diff out expected
# The seed and formula where chosen so that these four outputs are
# different.
run 0 $autfilt --seed=1 --dot out > 1.dot
run 0 $autfilt --seed=1 --dot --randomize=t out > 2.dot
run 0 $autfilt --seed=1 --dot --randomize=s out > 3.dot
run 0 $autfilt --seed=1 --dot --randomize=st out > 4.dot
cmp 1.dot 2.dot && exit 1
cmp 1.dot 3.dot && exit 1
cmp 2.dot 3.dot && exit 1
cmp 2.dot 4.dot && exit 1
cmp 3.dot 4.dot && exit 1
# A second run should produce the same output
$autfilt --seed=1 --dot out > 1b.dot
$autfilt --seed=1 --dot --randomize=t out > 2b.dot
$autfilt --seed=1 --dot --randomize=s out > 3b.dot
$autfilt --seed=1 --dot --randomize=st out > 4b.dot
diff 1.dot 1b.dot
diff 2.dot 2b.dot
diff 3.dot 3b.dot
diff 4.dot 4b.dot
$autfilt --randomize=foo out 2>stderr && exit 1
grep "unknown argument for --randomize: 'f'" stderr
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment