Commit 715805fa authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 97665a58
...@@ -152,7 +152,7 @@ $txt ...@@ -152,7 +152,7 @@ $txt
* Acceptance condition * 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, - =-A ACCEPTANCE= (or =--acceptance=ACCEPTANCE=) controls both the acceptance condition,
and the number of associated acceptance sets. The =ACCEPTANCE= argument is documented and the number of associated acceptance sets. The =ACCEPTANCE= argument is documented
...@@ -191,12 +191,17 @@ randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p' ...@@ -191,12 +191,17 @@ randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p'
- =-a= (or =--acc-probability=) controls the probability that any - =-a= (or =--acc-probability=) controls the probability that any
transition belong to a given acceptance set. transition belong to a given acceptance set.
- =-S= (or =--state-acc=) requests that the automaton use state-based - =-S= (or =--state-based-acceptance=) requests that the automaton
acceptance. In this case, =-a= is the probability that a /state/ use state-based acceptance. In this case, =-a= is the probability
belong to the acceptance set. (Because Spot only deals with that a /state/ belong to the acceptance set. (Because Spot only
transition-based acceptance internally, this options force all deals with transition-based acceptance internally, this options
transitions leaving a state to belong to the same acceptance sets. force all transitions leaving a state to belong to the same
But if the output format allows state-acceptance, it will be used.) 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=, In addition, =-B= (or =--ba=) is a shorthand for =-A1 -S=,
ans =-s= (or =--spin=) implies =-B=. ans =-s= (or =--spin=) implies =-B=.
...@@ -268,14 +273,14 @@ $txt ...@@ -268,14 +273,14 @@ $txt
#+NAME: randaut5b #+NAME: randaut5b
#+BEGIN_SRC sh :results verbatim :exports code #+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 #+END_SRC
#+RESULTS: randaut5b #+RESULTS: randaut5b
#+begin_example #+begin_example
digraph G { digraph G {
rankdir=LR rankdir=LR
label=<(Fin(<font color="#5DA5DA">⓿</font>) | Inf(<font color="#F17CB0">❶</font>)) &amp; (Fin(<font color="#FAA43A">❷</font>) | Inf(<font color="#B276B2">❸</font>))> label=<(Fin(<font color="#5DA5DA"></font>) | Inf(<font color="#F17CB0"></font>)) &amp; (Fin(<font color="#FAA43A"></font>) | Inf(<font color="#B276B2"></font>))>
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
fontname="Lato" fontname="Lato"
...@@ -290,21 +295,20 @@ digraph G { ...@@ -290,21 +295,20 @@ digraph G {
0 -> 3 [label=<!p0 &amp; !p1>] 0 -> 3 [label=<!p0 &amp; !p1>]
1 [label=<1>] 1 [label=<1>]
1 -> 5 [label=<!p0 &amp; p1>] 1 -> 5 [label=<!p0 &amp; p1>]
2 [label=<2<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>] 2 [label=<2<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
2 -> 0 [label=<!p0 &amp; p1>] 2 -> 1 [label=<!p0 &amp; p1>]
2 -> 4 [label=<!p0 &amp; !p1>] 2 -> 2 [label=<!p0 &amp; !p1>]
2 -> 4 [label=<p0 &amp; p1>]
3 [label=<3>] 3 [label=<3>]
3 -> 1 [label=<!p0 &amp; !p1>] 3 -> 2 [label=<!p0 &amp; !p1>]
3 -> 2 [label=<p0 &amp; !p1>] 3 -> 3 [label=<!p0 &amp; p1>]
3 -> 5 [label=<!p0 &amp; !p1>] 4 [label=<4>]
3 -> 4 [label=<p0 &amp; !p1>] 4 -> 0 [label=<!p0 &amp; !p1>]
4 [label=<4<br/><font color="#B276B2">❸</font>>] 4 -> 5 [label=<!p0 &amp; p1>]
4 -> 2 [label=<p0 &amp; !p1>] 5 [label=<5<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
4 -> 5 [label=<!p0 &amp; !p1>]
4 -> 3 [label=<!p0 &amp; p1>]
5 [label=<5<br/><font color="#F17CB0">❶</font>>]
5 -> 3 [label=<!p0 &amp; p1>]
5 -> 1 [label=<p0 &amp; p1>] 5 -> 1 [label=<p0 &amp; p1>]
5 -> 2 [label=<!p0 &amp; !p1>]
5 -> 3 [label=<p0 &amp; p1>]
} }
#+end_example #+end_example
...@@ -314,6 +318,73 @@ $txt ...@@ -314,6 +318,73 @@ $txt
#+RESULTS: #+RESULTS:
[[file:randaut5b.png]] [[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=<Inf(<font color="#5DA5DA">⓿</font>) | (Fin(<font color="#F17CB0">❶</font>) &amp; (Inf(<font color="#FAA43A">❷</font>) | Fin(<font color="#B276B2">❸</font>)))>
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<br/><font color="#F17CB0">❶</font>>]
0 -> 2 [label=<!p0 &amp; !p1>]
0 -> 8 [label=<!p0 &amp; !p1>]
0 -> 0 [label=<p0 &amp; !p1>]
0 -> 6 [label=<!p0 &amp; p1>]
1 [label=<1<br/><font color="#B276B2">❸</font>>]
1 -> 5 [label=<!p0 &amp; !p1>]
1 -> 9 [label=<!p0 &amp; p1>]
2 [label=<2<br/><font color="#FAA43A">❷</font>>]
2 -> 4 [label=<p0 &amp; p1>]
2 -> 5 [label=<!p0 &amp; !p1>]
3 [label=<3<br/><font color="#5DA5DA">⓿</font>>]
3 -> 6 [label=<p0 &amp; !p1>]
3 -> 1 [label=<!p0 &amp; p1>]
4 [label=<4<br/><font color="#5DA5DA">⓿</font>>]
4 -> 6 [label=<!p0 &amp; !p1>]
4 -> 1 [label=<p0 &amp; p1>]
5 [label=<5<br/><font color="#5DA5DA">⓿</font>>]
5 -> 0 [label=<!p0 &amp; !p1>]
5 -> 8 [label=<p0 &amp; !p1>]
5 -> 7 [label=<!p0 &amp; !p1>]
6 [label=<6<br/><font color="#5DA5DA">⓿</font>>]
6 -> 2 [label=<!p0 &amp; !p1>]
6 -> 3 [label=<!p0 &amp; !p1>]
7 [label=<7<br/><font color="#FAA43A">❷</font>>]
7 -> 3 [label=<!p0 &amp; p1>]
7 -> 1 [label=<!p0 &amp; p1>]
8 [label=<8<br/><font color="#5DA5DA">⓿</font>>]
8 -> 3 [label=<!p0 &amp; p1>]
8 -> 4 [label=<p0 &amp; !p1>]
8 -> 2 [label=<p0 &amp; !p1>]
8 -> 0 [label=<!p0 &amp; p1>]
9 [label=<9<br/><font color="#F17CB0">❶</font>>]
9 -> 0 [label=<p0 &amp; p1>]
9 -> 6 [label=<p0 &amp; !p1>]
}
#+end_example
#+BEGIN_SRC dot :file randaut5c.png :cmdline -Tpng :var txt=randaut5c :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut5c.png]]
* Determinism * Determinism
......
...@@ -69,6 +69,7 @@ a high density of transitions, and 3 to 4 atomic propositions:\n\ ...@@ -69,6 +69,7 @@ a high density of transitions, and 3 to 4 atomic propositions:\n\
enum { enum {
OPT_SEED = 1, OPT_SEED = 1,
OPT_COLORED,
}; };
static const argp_option options[] = static const argp_option options[] =
...@@ -83,6 +84,9 @@ static const argp_option options[] = ...@@ -83,6 +84,9 @@ static const argp_option options[] =
"use a negative value for unbounded generation", 0 }, "use a negative value for unbounded generation", 0 },
{ "ba", 'B', 0, 0, { "ba", 'B', 0, 0,
"build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 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 }, { "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 },
{ "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ", { "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ",
0 }, 0 },
...@@ -138,10 +142,11 @@ static const char* opt_seed_str = "0"; ...@@ -138,10 +142,11 @@ static const char* opt_seed_str = "0";
static int opt_automata = 1; static int opt_automata = 1;
static range opt_states = { 10, 10 }; static range opt_states = { 10, 10 };
static float opt_density = 0.2; 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 float opt_acc_prob = 0.2;
static bool opt_deterministic = false; static bool opt_deterministic = false;
static bool opt_state_acc = false; static bool opt_state_acc = false;
static bool opt_colored = false;
static bool ba_wanted = false; static bool ba_wanted = false;
static bool generic_wanted = false; static bool generic_wanted = false;
static bool gba_wanted = false; static bool gba_wanted = false;
...@@ -224,6 +229,9 @@ parse_opt(int key, char* arg, struct argp_state* as) ...@@ -224,6 +229,9 @@ parse_opt(int key, char* arg, struct argp_state* as)
opt_uniq = opt_uniq =
std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>()); std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
break; break;
case OPT_COLORED:
opt_colored = true;
break;
case OPT_SEED: case OPT_SEED:
opt_seed = to_int(arg); opt_seed = to_int(arg);
opt_seed_str = arg; opt_seed_str = arg;
...@@ -290,6 +298,16 @@ main(int argc, char** argv) ...@@ -290,6 +298,16 @@ main(int argc, char** argv)
if (automaton_format == Spin) if (automaton_format == Spin)
ba_options(); 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 try
{ {
spot::srand(opt_seed); spot::srand(opt_seed);
...@@ -328,12 +346,16 @@ main(int argc, char** argv) ...@@ -328,12 +346,16 @@ main(int argc, char** argv)
{ {
code = spot::parse_acc_code(opt_acceptance); code = spot::parse_acc_code(opt_acceptance);
accs = code.used_sets().max_set(); 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 = auto aut =
spot::random_graph(size, opt_density, &aprops, d, spot::random_graph(size, opt_density, &aprops, d,
accs, opt_acc_prob, 0.5, accs, opt_acc_prob, 0.5,
opt_deterministic, opt_state_acc); opt_deterministic, opt_state_acc,
opt_colored);
if (opt_acceptance) if (opt_acceptance)
aut->set_acceptance(accs, code); aut->set_acceptance(accs, code);
......
...@@ -133,3 +133,15 @@ AP: 2 "p0" "p1" ...@@ -133,3 +133,15 @@ AP: 2 "p0" "p1"
AP: 3 "p0" "p1" "p2" AP: 3 "p0" "p1" "p2"
EOF EOF
diff output expected 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
:
...@@ -36,7 +36,7 @@ namespace spot ...@@ -36,7 +36,7 @@ namespace spot
namespace namespace
{ {
unsigned static unsigned
random_deterministic_labels_rec(std::vector<bdd>& labels, int *props, random_deterministic_labels_rec(std::vector<bdd>& labels, int *props,
int props_n, bdd current, unsigned n) int props_n, bdd current, unsigned n)
{ {
...@@ -69,7 +69,7 @@ namespace spot ...@@ -69,7 +69,7 @@ namespace spot
} }
} }
std::vector<bdd> static std::vector<bdd>
random_deterministic_labels(int *props, int props_n, unsigned n) random_deterministic_labels(int *props, int props_n, unsigned n)
{ {
std::vector<bdd> bddvec; std::vector<bdd> bddvec;
...@@ -77,16 +77,23 @@ namespace spot ...@@ -77,16 +77,23 @@ namespace spot
return bddvec; return bddvec;
} }
acc_cond::mark_t static acc_cond::mark_t
random_acc_cond(twa_graph_ptr aut, unsigned n_accs, float a) random_acc(unsigned n_accs, float a)
{ {
acc_cond::mark_t m = 0U; acc_cond::mark_t m = 0U;
for (unsigned i = 0U; i < n_accs; ++i) for (unsigned i = 0U; i < n_accs; ++i)
if (drand() < a) if (drand() < a)
m |= aut->acc().mark(i); m.set(i);
return m; return m;
} }
static acc_cond::mark_t
random_acc1(unsigned n_accs)
{
auto u = static_cast<unsigned>(mrand(static_cast<int>(n_accs)));
return acc_cond::mark_t({u});
}
bdd bdd
random_labels(int* props, int props_n, float t) random_labels(int* props, int props_n, float t)
{ {
...@@ -118,7 +125,7 @@ namespace spot ...@@ -118,7 +125,7 @@ namespace spot
random_graph(int n, float d, random_graph(int n, float d,
const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict,
unsigned n_accs, float a, float t, unsigned n_accs, float a, float t,
bool deterministic, bool state_acc) bool deterministic, bool state_acc, bool colored)
{ {
assert(n > 0); assert(n > 0);
auto res = make_twa_graph(dict); auto res = make_twa_graph(dict);
...@@ -188,12 +195,12 @@ namespace spot ...@@ -188,12 +195,12 @@ namespace spot
unsigned dst; unsigned dst;
acc_cond::mark_t m = 0U; acc_cond::mark_t m = 0U;
if (state_acc) 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) for (auto& l: labels)
{ {
if (!state_acc) 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 // No connection to unreachable successors so far. This
// is our last chance, so force it now. // is our last chance, so force it now.
......
...@@ -51,6 +51,8 @@ namespace spot ...@@ -51,6 +51,8 @@ namespace spot
/// is true. /// is true.
/// \param deterministic build a complete and deterministic automaton /// \param deterministic build a complete and deterministic automaton
/// \param state_acc build an automaton with state-based acceptance /// \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 /// This algorithms is adapted from the one in Fig 6.2 page 48 of
/** \verbatim /** \verbatim
...@@ -81,7 +83,8 @@ namespace spot ...@@ -81,7 +83,8 @@ namespace spot
random_graph(int n, float d, random_graph(int n, float d,
const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict,
unsigned n_accs = 0, float a = 0.1, float t = 0.5, 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. /// Build a random acceptance where each acceptance sets is used once.
SPOT_API acc_cond::acc_code random_acceptance(unsigned n_accs); SPOT_API acc_cond::acc_code random_acceptance(unsigned n_accs);
......
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