1
Fork 0
mirror of https://github.com/Jaxan/hybrid-ads.git synced 2025-04-27 15:07:45 +02:00

Adds an extra program option: the random seed (optional)

This commit is contained in:
Joshua Moerman 2015-07-28 16:37:10 +02:00
parent d44610e4d6
commit e3b512fe6d
9 changed files with 57 additions and 26 deletions

View file

@ -15,7 +15,7 @@ splitting_tree::splitting_tree(size_t N, size_t d) : states(N), depth(d) {
iota(begin(states), end(states), 0); iota(begin(states), end(states), 0);
} }
result create_splitting_tree(const mealy & g, options opt) { result create_splitting_tree(const mealy & g, options opt, uint_fast32_t random_seed) {
const auto N = g.graph_size; const auto N = g.graph_size;
const auto P = g.input_size; const auto P = g.input_size;
const auto Q = g.output_size; const auto Q = g.output_size;
@ -34,8 +34,7 @@ result create_splitting_tree(const mealy & g, options opt) {
// List of inputs, will be shuffled in case of randomizations // List of inputs, will be shuffled in case of randomizations
vector<input> all_inputs(P); vector<input> all_inputs(P);
iota(begin(all_inputs), end(all_inputs), 0); iota(begin(all_inputs), end(all_inputs), 0);
random_device rd; mt19937 generator(random_seed);
mt19937 generator(rd());
size_t current_order = 0; size_t current_order = 0;
bool split_in_current_order = false; bool split_in_current_order = false;

View file

@ -111,4 +111,4 @@ struct result {
/// \brief Creates a splitting tree by partition refinement. /// \brief Creates a splitting tree by partition refinement.
/// \returns a splitting tree and other calculated structures. /// \returns a splitting tree and other calculated structures.
result create_splitting_tree(mealy const & m, options opt); result create_splitting_tree(mealy const & m, options opt, uint_fast32_t random_seed);

View file

@ -34,11 +34,10 @@ void test(const mealy & specification, const transfer_sequences & prefixes,
void randomized_test(const mealy & specification, const transfer_sequences & prefixes, void randomized_test(const mealy & specification, const transfer_sequences & prefixes,
const separating_family & separating_family, size_t min_k, size_t rnd_length, const separating_family & separating_family, size_t min_k, size_t rnd_length,
const writer & output) { const writer & output, uint_fast32_t random_seed) {
clog << "*** K >= " << min_k << endl; clog << "*** K >= " << min_k << endl;
std::random_device rd; std::mt19937 generator(random_seed);
std::mt19937 generator(rd());
// https://en.wikipedia.org/wiki/Geometric_distribution we have the random variable Y here // https://en.wikipedia.org/wiki/Geometric_distribution we have the random variable Y here
uniform_int_distribution<> unfair_coin(0, rnd_length); uniform_int_distribution<> unfair_coin(0, rnd_length);

View file

@ -19,7 +19,7 @@ void test(mealy const & specification, transfer_sequences const & prefixes,
/// \brief Performs random non-exhaustive tests for more states (harmonized, e.g. HSI / DS) /// \brief Performs random non-exhaustive tests for more states (harmonized, e.g. HSI / DS)
void randomized_test(mealy const & specification, transfer_sequences const & prefixes, void randomized_test(mealy const & specification, transfer_sequences const & prefixes,
separating_family const & separating_family, size_t min_k, separating_family const & separating_family, size_t min_k,
size_t rnd_length, writer const & output); size_t rnd_length, writer const & output, uint_fast32_t random_seed);
/// \brief returns a writer which simply writes everything to cout (via inputs) /// \brief returns a writer which simply writes everything to cout (via inputs)
writer default_writer(const std::vector<std::string> & inputs); writer default_writer(const std::vector<std::string> & inputs);

View file

@ -38,9 +38,8 @@ transfer_sequences create_transfer_sequences(const mealy& machine, state s){
return words; return words;
} }
transfer_sequences create_randomized_transfer_sequences(const mealy & machine, state s){ transfer_sequences create_randomized_transfer_sequences(const mealy & machine, state s, uint_fast32_t random_seed){
random_device rd; mt19937 generator(random_seed);
mt19937 generator(rd());
vector<bool> visited(machine.graph_size, false); vector<bool> visited(machine.graph_size, false);
vector<word> words(machine.graph_size); vector<word> words(machine.graph_size);

View file

@ -7,4 +7,4 @@ struct mealy;
using transfer_sequences = std::vector<word>; using transfer_sequences = std::vector<word>;
transfer_sequences create_transfer_sequences(mealy const & machine, state s); transfer_sequences create_transfer_sequences(mealy const & machine, state s);
transfer_sequences create_randomized_transfer_sequences(mealy const & machine, state s); transfer_sequences create_randomized_transfer_sequences(mealy const & machine, state s, uint_fast32_t random_seed);

View file

@ -18,8 +18,8 @@ using namespace std;
using time_logger = silent_timer; using time_logger = silent_timer;
int main(int argc, char *argv[]) try { int main(int argc, char *argv[]) try {
if(argc != 5) { if(argc != 5 && argc != 6) {
cerr << "usage: main <filename> <max k> <rnd length> <all|fixed|random>" << endl; cerr << "usage: main <filename> <max k> <rnd length> <all|fixed|random> [<seed>]" << endl;
return 1; return 1;
} }
const string filename = argv[1]; const string filename = argv[1];
@ -32,6 +32,9 @@ int main(int argc, char *argv[]) try {
const bool streaming = mode == "all" || mode == "fixed"; const bool streaming = mode == "all" || mode == "fixed";
const bool random_part = mode == "all" || mode == "random"; const bool random_part = mode == "all" || mode == "random";
const bool seed_provided = argc == 6;
const uint_fast32_t seed = seed_provided ? stoul(argv[5]) : 0;
const bool use_distinguishing_sequence = true; const bool use_distinguishing_sequence = true;
const bool randomize_prefixes = true; const bool randomize_prefixes = true;
const bool randomize_hopcroft = true; const bool randomize_hopcroft = true;
@ -57,10 +60,23 @@ int main(int argc, char *argv[]) try {
const auto & machine = reachable_submachine(move(machine_and_translation.first), 0); const auto & machine = reachable_submachine(move(machine_and_translation.first), 0);
const auto & translation = machine_and_translation.second; const auto & translation = machine_and_translation.second;
// every thread gets its own seed
const auto random_seeds = [&] {
vector<uint_fast32_t> seeds(4);
if (seed_provided) {
seed_seq s{seed};
s.generate(seeds.begin(), seeds.end());
} else {
random_device rd;
generate(seeds.begin(), seeds.end(), ref(rd));
}
return seeds;
}();
auto all_pair_separating_sequences = [&]{ auto all_pair_separating_sequences = [&]{
const auto splitting_tree_hopcroft = [&]{ const auto splitting_tree_hopcroft = [&]{
time_logger t("creating hopcroft splitting tree"); time_logger t("creating hopcroft splitting tree");
return create_splitting_tree(machine, randomize_hopcroft ? randomized_hopcroft_style : hopcroft_style); return create_splitting_tree(machine, randomize_hopcroft ? randomized_hopcroft_style : hopcroft_style, random_seeds[0]);
}(); }();
return splitting_tree_hopcroft.root; return splitting_tree_hopcroft.root;
@ -70,7 +86,7 @@ int main(int argc, char *argv[]) try {
const auto tree = [&]{ const auto tree = [&]{
time_logger t("Lee & Yannakakis I"); time_logger t("Lee & Yannakakis I");
if(use_distinguishing_sequence) if(use_distinguishing_sequence)
return create_splitting_tree(machine, randomize_lee_yannakakis ? randomized_lee_yannakakis_style : lee_yannakakis_style); return create_splitting_tree(machine, randomize_lee_yannakakis ? randomized_lee_yannakakis_style : lee_yannakakis_style, random_seeds[1]);
else else
return result(machine.graph_size); return result(machine.graph_size);
}(); }();
@ -86,7 +102,7 @@ int main(int argc, char *argv[]) try {
auto transfer_sequences = [&]{ auto transfer_sequences = [&]{
time_logger t("determining transfer sequences"); time_logger t("determining transfer sequences");
if(randomize_prefixes){ if(randomize_prefixes){
return create_randomized_transfer_sequences(machine, 0); return create_randomized_transfer_sequences(machine, 0, random_seeds[2]);
} else { } else {
return create_transfer_sequences(machine, 0); return create_transfer_sequences(machine, 0);
} }
@ -107,7 +123,7 @@ int main(int argc, char *argv[]) try {
if(random_part){ if(random_part){
time_logger t("outputting all random tests"); time_logger t("outputting all random tests");
const auto k_max_ = streaming ? k_max + 1 : 0; const auto k_max_ = streaming ? k_max + 1 : 0;
randomized_test(machine, transfer_sequences, separating_family, k_max_, rnd_length, default_writer(inputs)); randomized_test(machine, transfer_sequences, separating_family, k_max_, rnd_length, default_writer(inputs), random_seeds[3]);
} }
} catch (exception const & e) { } catch (exception const & e) {

View file

@ -6,8 +6,9 @@
#include <trie.hpp> #include <trie.hpp>
#include <future> #include <future>
#include <string>
#include <iostream> #include <iostream>
#include <random>
#include <string>
using namespace std; using namespace std;
@ -23,14 +24,16 @@ static Method parse_method(string const & s) {
} }
int main(int argc, char * argv[]) { int main(int argc, char * argv[]) {
if (argc != 4) { if (argc != 4 && argc != 5) {
cerr << "usage: methods <file> <mode> <k_max>\n"; cerr << "usage: methods <file> <mode> <k_max> [<seed>]\n";
return 1; return 1;
} }
const string filename = argv[1]; const string filename = argv[1];
const Method method = parse_method(argv[2]); const Method method = parse_method(argv[2]);
const size_t k_max = std::stoul(argv[3]); const size_t k_max = std::stoul(argv[3]);
const bool seed_provided = argc == 5;
const uint_fast32_t seed = seed_provided ? stoul(argv[5]) : 0;
const auto machine = [&] { const auto machine = [&] {
if (filename.find(".txt") != string::npos) { if (filename.find(".txt") != string::npos) {
@ -43,21 +46,33 @@ int main(int argc, char * argv[]) {
return read_mealy_from_dot(filename).first; return read_mealy_from_dot(filename).first;
}(); }();
const auto random_seeds = [&] {
vector<uint_fast32_t> seeds(3);
if (seed_provided) {
seed_seq s{seed};
s.generate(seeds.begin(), seeds.end());
} else {
random_device rd;
generate(seeds.begin(), seeds.end(), ref(rd));
}
return seeds;
}();
auto sequence_fut = async([&] { auto sequence_fut = async([&] {
if (method == hsi_method) { if (method == hsi_method) {
return create_adaptive_distinguishing_sequence(result(machine.graph_size)); return create_adaptive_distinguishing_sequence(result(machine.graph_size));
} }
const auto tree = create_splitting_tree(machine, randomized_lee_yannakakis_style); const auto tree = create_splitting_tree(machine, randomized_lee_yannakakis_style, random_seeds[0]);
return create_adaptive_distinguishing_sequence(tree); return create_adaptive_distinguishing_sequence(tree);
}); });
auto pairs_fut = async([&] { auto pairs_fut = async([&] {
const auto tree = create_splitting_tree(machine, randomized_min_hopcroft_style); const auto tree = create_splitting_tree(machine, randomized_min_hopcroft_style, random_seeds[1]);
return tree.root; return tree.root;
}); });
auto prefixes_fut = async([&] { auto prefixes_fut = async([&] {
return create_transfer_sequences(machine, 0); return create_randomized_transfer_sequences(machine, 0, random_seeds[2]);
}); });
auto middles_fut = async([&] { auto middles_fut = async([&] {

View file

@ -3,8 +3,9 @@
#include <splitting_tree.hpp> #include <splitting_tree.hpp>
#include <write_tree_to_dot.hpp> #include <write_tree_to_dot.hpp>
#include <string>
#include <iostream> #include <iostream>
#include <random>
#include <string>
using namespace std; using namespace std;
@ -20,7 +21,9 @@ int main(int argc, char * argv[]) {
const auto & translation = machine_and_translation.second; const auto & translation = machine_and_translation.second;
const auto options = randomized ? randomized_lee_yannakakis_style : lee_yannakakis_style; const auto options = randomized ? randomized_lee_yannakakis_style : lee_yannakakis_style;
const auto tree = create_splitting_tree(machine, options);
random_device rd;
const auto tree = create_splitting_tree(machine, options, rd());
const auto sequence = create_adaptive_distinguishing_sequence(tree); const auto sequence = create_adaptive_distinguishing_sequence(tree);
write_splitting_tree_to_dot(tree.root, filename + ".tree"); write_splitting_tree_to_dot(tree.root, filename + ".tree");