From 715805fad3093fc2c7e23532f3aba4ee70b44b0e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 1 Jun 2015 21:56:39 +0200 Subject: [PATCH] randaut: add a --colored option Fixes #83. * src/bin/randaut.cc: Add option. * src/twaalgos/randomgraph.cc, src/twaalgos/randomgraph.hh: Honor it. * src/tests/randaut.test: Add tests. * doc/org/randaut.org: Document it. --- doc/org/randaut.org | 115 +++++++++++++++++++++++++++++------- src/bin/randaut.cc | 26 +++++++- src/tests/randaut.test | 12 ++++ src/twaalgos/randomgraph.cc | 23 +++++--- src/twaalgos/randomgraph.hh | 5 +- 5 files changed, 148 insertions(+), 33 deletions(-) diff --git a/doc/org/randaut.org b/doc/org/randaut.org index c5966be61..9b21e547b 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -152,7 +152,7 @@ $txt * Acceptance condition -The generation of the acceptance sets abn is controlled with the following three parameters: +The generation of the acceptance sets abn is controlled with the following four parameters: - =-A ACCEPTANCE= (or =--acceptance=ACCEPTANCE=) controls both the acceptance condition, and the number of associated acceptance sets. The =ACCEPTANCE= argument is documented @@ -191,12 +191,17 @@ randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p' - =-a= (or =--acc-probability=) controls the probability that any transition belong to a given acceptance set. - - =-S= (or =--state-acc=) requests that the automaton use state-based - acceptance. In this case, =-a= is the probability that a /state/ - belong to the acceptance set. (Because Spot only deals with - transition-based acceptance internally, this options force all - transitions leaving a state to belong to the same acceptance sets. - But if the output format allows state-acceptance, it will be used.) + - =-S= (or =--state-based-acceptance=) requests that the automaton + use state-based acceptance. In this case, =-a= is the probability + that a /state/ belong to the acceptance set. (Because Spot only + deals with transition-based acceptance internally, this options + force all transitions leaving a state to belong to the same + acceptance sets. But if the output format allows state-based + acceptance, it will be used.) + - =--colored= requests that each transition (of state if combined with =-S=) + in the generated automaton should belong to exactly one set (in that + case =-a= is ignored, and =-A= must be used to specify an acceptance + condition with at least one set). In addition, =-B= (or =--ba=) is a shorthand for =-A1 -S=, ans =-s= (or =--spin=) implies =-B=. @@ -268,14 +273,14 @@ $txt #+NAME: randaut5b #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q6 -d0.4 --state-acc -a.2 -A 'Streett 1..3' 2 --dot=.a +randaut -Q6 -d0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a #+END_SRC #+RESULTS: randaut5b #+begin_example digraph G { rankdir=LR - label=<(Fin(⓿) | Inf(❶)) & (Fin(❷) | Inf(❸))> + label=<(Fin(⓿) | Inf(❶)) & (Fin(❷) | Inf(❸))> labelloc="t" node [shape="circle"] fontname="Lato" @@ -290,21 +295,20 @@ digraph G { 0 -> 3 [label=] 1 [label=<1>] 1 -> 5 [label=] - 2 [label=<2
⓿❷>] - 2 -> 0 [label=] - 2 -> 4 [label=] + 2 [label=<2
⓿❷>] + 2 -> 1 [label=] + 2 -> 2 [label=] + 2 -> 4 [label=] 3 [label=<3>] - 3 -> 1 [label=] - 3 -> 2 [label=] - 3 -> 5 [label=] - 3 -> 4 [label=] - 4 [label=<4
❸>] - 4 -> 2 [label=] - 4 -> 5 [label=] - 4 -> 3 [label=] - 5 [label=<5
❶>] - 5 -> 3 [label=] + 3 -> 2 [label=] + 3 -> 3 [label=] + 4 [label=<4>] + 4 -> 0 [label=] + 4 -> 5 [label=] + 5 [label=<5
❶❷>] 5 -> 1 [label=] + 5 -> 2 [label=] + 5 -> 3 [label=] } #+end_example @@ -314,6 +318,73 @@ $txt #+RESULTS: [[file:randaut5b.png]] +For generating random parity automata you should use the option +=--colored= to make sure each transition (or state in the following +example) belong to exactly one acceptance set. Note that you can +specify a precise parity acceptance such as =parity min even 3=, or +give =randaut= some freedom, as in this example. + +#+NAME: randaut5c +#+BEGIN_SRC sh :results verbatim :exports code +randaut -Q10 -S --colored -A 'parity rand rand 3..4' 2 --dot=.a +#+END_SRC + +#+RESULTS: randaut5c +#+begin_example +digraph G { + rankdir=LR + label=⓿) | (Fin(❶) & (Inf(❷) | Fin(❸)))> + labelloc="t" + node [shape="circle"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] + I [label="", style=invis, width=0] + I -> 0 + 0 [label=<0
❶>] + 0 -> 2 [label=] + 0 -> 8 [label=] + 0 -> 0 [label=] + 0 -> 6 [label=] + 1 [label=<1
❸>] + 1 -> 5 [label=] + 1 -> 9 [label=] + 2 [label=<2
❷>] + 2 -> 4 [label=] + 2 -> 5 [label=] + 3 [label=<3
⓿>] + 3 -> 6 [label=] + 3 -> 1 [label=] + 4 [label=<4
⓿>] + 4 -> 6 [label=] + 4 -> 1 [label=] + 5 [label=<5
⓿>] + 5 -> 0 [label=] + 5 -> 8 [label=] + 5 -> 7 [label=] + 6 [label=<6
⓿>] + 6 -> 2 [label=] + 6 -> 3 [label=] + 7 [label=<7
❷>] + 7 -> 3 [label=] + 7 -> 1 [label=] + 8 [label=<8
⓿>] + 8 -> 3 [label=] + 8 -> 4 [label=] + 8 -> 2 [label=] + 8 -> 0 [label=] + 9 [label=<9
❶>] + 9 -> 0 [label=] + 9 -> 6 [label=] +} +#+end_example + +#+BEGIN_SRC dot :file randaut5c.png :cmdline -Tpng :var txt=randaut5c :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:randaut5c.png]] * Determinism diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 88479dce4..5174a8edb 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -69,6 +69,7 @@ a high density of transitions, and 3 to 4 atomic propositions:\n\ enum { OPT_SEED = 1, + OPT_COLORED, }; static const argp_option options[] = @@ -83,6 +84,9 @@ static const argp_option options[] = "use a negative value for unbounded generation", 0 }, { "ba", 'B', 0, 0, "build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 }, + { "colored", OPT_COLORED, 0, 0, + "build an automaton in which each transition (or state if combined with " + "-S) belong to a single acceptance set", 0 }, { "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 }, { "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ", 0 }, @@ -138,10 +142,11 @@ static const char* opt_seed_str = "0"; static int opt_automata = 1; static range opt_states = { 10, 10 }; static float opt_density = 0.2; -static range opt_acc_sets = { 0, 0 }; +static range opt_acc_sets = { -1, 0 }; static float opt_acc_prob = 0.2; static bool opt_deterministic = false; static bool opt_state_acc = false; +static bool opt_colored = false; static bool ba_wanted = false; static bool generic_wanted = false; static bool gba_wanted = false; @@ -224,6 +229,9 @@ parse_opt(int key, char* arg, struct argp_state* as) opt_uniq = std::unique_ptr(new std::set>()); break; + case OPT_COLORED: + opt_colored = true; + break; case OPT_SEED: opt_seed = to_int(arg); opt_seed_str = arg; @@ -290,6 +298,16 @@ main(int argc, char** argv) if (automaton_format == Spin) ba_options(); + if (opt_colored && opt_acc_sets.min == -1 && !generic_wanted) + error(2, 0, "--colored requires at least one acceptance set; " + "use --acceptance"); + if (opt_colored && opt_acc_sets.min == 0) + error(2, 0, "--colored requires at least one acceptance set; " + "fix the range of --acceptance"); + + if (opt_acc_sets.min == -1) + opt_acc_sets.min = 0; + try { spot::srand(opt_seed); @@ -328,12 +346,16 @@ main(int argc, char** argv) { code = spot::parse_acc_code(opt_acceptance); accs = code.used_sets().max_set(); + if (opt_colored && accs == 0) + error(2, 0, "--colored requires at least one acceptance set; " + "fix the range of --acceptance"); } auto aut = spot::random_graph(size, opt_density, &aprops, d, accs, opt_acc_prob, 0.5, - opt_deterministic, opt_state_acc); + opt_deterministic, opt_state_acc, + opt_colored); if (opt_acceptance) aut->set_acceptance(accs, code); diff --git a/src/tests/randaut.test b/src/tests/randaut.test index 4d32f4480..343fa04ca 100755 --- a/src/tests/randaut.test +++ b/src/tests/randaut.test @@ -133,3 +133,15 @@ AP: 2 "p0" "p1" AP: 3 "p0" "p1" "p2" EOF diff output expected + +$randaut -A3 --colored 2 -H | grep 'properties:.*colored' +$randaut -S -A'parity min even 3' --colored 2 -H | grep 'properties:.*colored' + +$randaut --colored 2 2>stderr && exit 1 +grep 'randaut: --colored requires' stderr +$randaut -A0..2 --colored 2 2>stderr && exit 1 +grep 'randaut: --colored requires' stderr +$randaut -S -A'parity min even 0..3' -q -n10 --colored 2 2>stderr && exit 1 +grep 'randaut: --colored requires' stderr + +: diff --git a/src/twaalgos/randomgraph.cc b/src/twaalgos/randomgraph.cc index 1979242ff..aef74af41 100644 --- a/src/twaalgos/randomgraph.cc +++ b/src/twaalgos/randomgraph.cc @@ -36,7 +36,7 @@ namespace spot namespace { - unsigned + static unsigned random_deterministic_labels_rec(std::vector& labels, int *props, int props_n, bdd current, unsigned n) { @@ -69,7 +69,7 @@ namespace spot } } - std::vector + static std::vector random_deterministic_labels(int *props, int props_n, unsigned n) { std::vector bddvec; @@ -77,16 +77,23 @@ namespace spot return bddvec; } - acc_cond::mark_t - random_acc_cond(twa_graph_ptr aut, unsigned n_accs, float a) + static acc_cond::mark_t + random_acc(unsigned n_accs, float a) { acc_cond::mark_t m = 0U; for (unsigned i = 0U; i < n_accs; ++i) if (drand() < a) - m |= aut->acc().mark(i); + m.set(i); return m; } + static acc_cond::mark_t + random_acc1(unsigned n_accs) + { + auto u = static_cast(mrand(static_cast(n_accs))); + return acc_cond::mark_t({u}); + } + bdd random_labels(int* props, int props_n, float t) { @@ -118,7 +125,7 @@ namespace spot random_graph(int n, float d, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, unsigned n_accs, float a, float t, - bool deterministic, bool state_acc) + bool deterministic, bool state_acc, bool colored) { assert(n > 0); auto res = make_twa_graph(dict); @@ -188,12 +195,12 @@ namespace spot unsigned dst; acc_cond::mark_t m = 0U; if (state_acc) - m = random_acc_cond(res, n_accs, a); + m = colored ? random_acc1(n_accs) : random_acc(n_accs, a); for (auto& l: labels) { if (!state_acc) - m = random_acc_cond(res, n_accs, a); + m = colored ? random_acc1(n_accs) : random_acc(n_accs, a); // No connection to unreachable successors so far. This // is our last chance, so force it now. diff --git a/src/twaalgos/randomgraph.hh b/src/twaalgos/randomgraph.hh index 8b2768f8b..1b89f7787 100644 --- a/src/twaalgos/randomgraph.hh +++ b/src/twaalgos/randomgraph.hh @@ -51,6 +51,8 @@ namespace spot /// is true. /// \param deterministic build a complete and deterministic automaton /// \param state_acc build an automaton with state-based acceptance + /// \param colored build an automaton in which each transition (or state) + /// belongs to a single acceptance set. /// /// This algorithms is adapted from the one in Fig 6.2 page 48 of /** \verbatim @@ -81,7 +83,8 @@ namespace spot random_graph(int n, float d, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, unsigned n_accs = 0, float a = 0.1, float t = 0.5, - bool deterministic = false, bool state_acc = false); + bool deterministic = false, bool state_acc = false, + bool colored = false); /// Build a random acceptance where each acceptance sets is used once. SPOT_API acc_cond::acc_code random_acceptance(unsigned n_accs);