diff --git a/NEWS b/NEWS index 207e8aedf..b856aac5c 100644 --- a/NEWS +++ b/NEWS @@ -43,6 +43,10 @@ New in spot 1.99a (not yet released) used in a stream. The parser currently ignore all optional 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 requires GCC >= 4.6 or Clang >= 3.1. These minimum versions are old enough that it should not be an issue to most people. diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 8a466b7b6..d62ff063f 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -39,11 +39,13 @@ #include "tgba/bddprint.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" +#include "misc/random.hh" #include "hoaparse/public.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\ "; @@ -53,6 +55,8 @@ Convert, transform, and filter Büchi automata.\n\ #define OPT_LBTT 3 #define OPT_SPOT 4 #define OPT_STATS 5 +#define OPT_RANDOMIZE 6 +#define OPT_SEED 7 static const argp_option options[] = { @@ -111,24 +115,44 @@ static const argp_option options[] = { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "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 }, { "extra-options", 'x', "OPTS", 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 } }; -const struct argp_child children[] = +static const struct argp_child children[] = { { &post_argp_disabled, 0, 0, 20 }, { &misc_argp, 0, 0, -1 }, { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; -bool utf8 = false; -const char* stats = ""; -const char* hoa_opt = 0; -spot::option_map extra_options; +static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } + format = Dot; +static const char* stats = ""; +static const char* hoa_opt = 0; +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 parse_opt(int key, char* arg, struct argp_state*) @@ -180,6 +204,31 @@ parse_opt(int key, char* arg, struct argp_state*) format = Lbtt; } 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: format = Spot; break; @@ -301,6 +350,9 @@ namespace auto aut = post.run(haut->aut, nullptr); const double conversion_time = sw.stop(); + if (randomize_st || randomize_tr) + spot::randomize(aut, randomize_st, randomize_tr); + switch (format) { case Dot: @@ -385,6 +437,8 @@ main(int argc, char** argv) if (jobs.empty()) jobs.emplace_back("-", true); + spot::srand(opt_seed); + spot::postprocessor post(&extra_options); post.set_pref(pref | comp); post.set_type(type); diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 248308d52..9f946c8ff 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -725,6 +725,21 @@ namespace spot //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& 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&& newst, unsigned used_states) { assert(newst.size() == states_.size()); diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 89818cc20..803f271a2 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -57,6 +57,7 @@ tgbaalgos_HEADERS = \ product.hh \ projrun.hh \ randomgraph.hh \ + randomize.hh \ reachiter.hh \ reducerun.hh \ replayrun.hh \ @@ -108,6 +109,7 @@ libtgbaalgos_la_SOURCES = \ product.cc \ projrun.cc \ randomgraph.cc \ + randomize.cc \ reachiter.cc \ reducerun.cc \ replayrun.cc \ diff --git a/src/tgbaalgos/randomize.cc b/src/tgbaalgos/randomize.cc new file mode 100644 index 000000000..285b7aedb --- /dev/null +++ b/src/tgbaalgos/randomize.cc @@ -0,0 +1,55 @@ +// -*- 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 . + +#include +#include +#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 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_(); + } +} diff --git a/src/tgbaalgos/randomize.hh b/src/tgbaalgos/randomize.hh new file mode 100644 index 000000000..76e32297a --- /dev/null +++ b/src/tgbaalgos/randomize.hh @@ -0,0 +1,37 @@ +// -*- 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 . + +#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 diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index c0cb52797..ffb54416b 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -104,6 +104,7 @@ TESTS = \ degenid.test \ degenlskip.test \ kv.test \ + randomize.test \ lbttparse.test \ scc.test \ sccsimpl.test \ diff --git a/src/tgbatest/randomize.test b/src/tgbatest/randomize.test new file mode 100755 index 000000000..7f922afb7 --- /dev/null +++ b/src/tgbatest/randomize.test @@ -0,0 +1,82 @@ +#!/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 + +ltl2tgba=../../bin/ltl2tgba +autfilt=../../bin/autfilt + +$ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out + +cat >expected < 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