Commit 0ac35a15 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

randaut: rename -S as -Q for consistency

This way -S means --state-based-acc like with other tools
producing automata.   This fixes #82.

* src/bin/randaut.cc: Rename -S as -Q, rename --state-acc as
--state-based-acc (with --sbacc as a synonym), and declare -S as the
short version of --state-based-acc.
* doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org,
src/tests/isomorph.test, src/tests/randaut.test,
src/tests/randtgba.test, src/tests/readsave.test, src/tests/uniq.test,
wrap/python/tests/randaut.ipynb: Adjust all calls to randaut.
parent a6ef2456
......@@ -99,22 +99,22 @@ statistics.
#+BEGIN_SRC sh :results verbatim :exports both
randaut --hoa -n 10 -A0..2 -S10..20 -d0.05 2 |
randaut --hoa -n 10 -A0..2 -Q10..20 -d0.05 2 |
autfilt --stats='%s states, %e edges, %a acc-sets, %c SCCs, det=%d'
#+END_SRC
#+RESULTS:
#+begin_example
16 states, 27 edges, 1 acc-sets, 2 SCCs, det=0
12 states, 20 edges, 1 acc-sets, 2 SCCs, det=0
11 states, 15 edges, 0 acc-sets, 4 SCCs, det=1
16 states, 29 edges, 0 acc-sets, 2 SCCs, det=0
15 states, 30 edges, 2 acc-sets, 1 SCCs, det=0
11 states, 17 edges, 1 acc-sets, 2 SCCs, det=0
11 states, 16 edges, 1 acc-sets, 1 SCCs, det=1
17 states, 28 edges, 1 acc-sets, 1 SCCs, det=0
19 states, 36 edges, 0 acc-sets, 3 SCCs, det=0
11 states, 16 edges, 2 acc-sets, 6 SCCs, det=0
16 states, 28 edges, 1 acc-sets, 1 SCCs, det=0
19 states, 37 edges, 0 acc-sets, 1 SCCs, det=0
16 states, 24 edges, 1 acc-sets, 1 SCCs, det=0
12 states, 16 edges, 0 acc-sets, 5 SCCs, det=0
12 states, 17 edges, 2 acc-sets, 3 SCCs, det=0
15 states, 21 edges, 2 acc-sets, 5 SCCs, det=0
10 states, 12 edges, 0 acc-sets, 4 SCCs, det=1
10 states, 14 edges, 1 acc-sets, 1 SCCs, det=0
19 states, 27 edges, 1 acc-sets, 1 SCCs, det=0
11 states, 12 edges, 1 acc-sets, 9 SCCs, det=1
#+end_example
The following =%= sequences are available:
......
......@@ -871,23 +871,23 @@ density 0.2, and just count the number of edges in each automaton. Then
use =R= to summarize the distribution of these values:
#+BEGIN_SRC sh :results verbatim :exports both
randaut -d 0.2 -S 10 -n 1000 a --stats %e > size.csv
randaut -d0.2 -Q10 -n1000 a --stats %e > size.csv
R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))"
#+END_SRC
#+RESULTS:
: edges
: Min. :17.00
: 1st Qu.:25.00
: Median :28.00
: Mean :27.96
: 3rd Qu.:30.00
: Max. :42.00
: Min. :14.00
: 1st Qu.:22.00
: Median :25.00
: Mean :24.72
: 3rd Qu.:27.00
: Max. :36.00
For $S=10$ states and density $D=0.2$ the expected degree of each
state $1+(S-1)D = 1+9\times 0.2 = 2.8$ so the expected number of edges
should be 10 times that.
For $Q=10$ states and density $D=0.2$ the expected degree of each
state is $1+(Q-1)D = 1+9\times 0.2 = 2.8$, so the expected number of
edges should be 10 times that.
* Naming automata
......@@ -1006,7 +1006,7 @@ automaton is deterministic. We can generate 20 random automata, and
output them in two files depending on their determinism:
#+BEGIN_SRC sh :results verbatim :exports both
randaut -n 20 -S2 -d1 1 -H -o out-det%d.hoa
randaut -n 20 -Q2 -d1 1 -H -o out-det%d.hoa
autfilt -c out-det0.hoa # Count of non-deterministic automata
autfilt -c out-det1.hoa # Count of deterministic automata
#+END_SRC
......@@ -1024,7 +1024,7 @@ deterministic automata, it may look like we produced more
than 20 automata:
#+BEGIN_SRC sh :results verbatim :exports both
randaut -D -n 20 -S2 -d1 1 -H -o out-det%d.hoa
randaut -D -n 20 -Q2 -d1 1 -H -o out-det%d.hoa
autfilt -c out-det0.hoa # Count of non-deterministic automata
autfilt -c out-det1.hoa # Count of deterministic automata
#+END_SRC
......@@ -1039,6 +1039,6 @@ previous execution, while =out-det1.hoa= has been overwritten.
In the case where you want to append to a file instead of overwriting
it, prefix the output filename with =>>= as in
: randaut -D -n 20 -S2 1 -H -o '>>out-det%d.hoa'
: randaut -D -n 20 -Q2 1 -H -o '>>out-det%d.hoa'
(You need the quotes so that the shell does not interpret '>>'.)
......@@ -69,22 +69,22 @@ instead of giving a list of atomic propositions.
* States and density
The numbers of states can be controlled using the =-S= option. This
option will accept a range as argument, so for instance =-S3..6= will
The numbers of states can be controlled using the =-Q= option. This
option will accept a range as argument, so for instance =-Q3..6= will
generate an automaton with 3 to 6 states.
The number of edges can be controlled using the =-d= (or
=--density=) option. The argument should be a number between 0 and 1.
In an automaton with $S$ states and density $d$, the degree of each
state will follow a normal distribution with mean $1+(S-1)d$ and
variance $(S-1)d(1-d)$.
In an automaton with $Q$ states and density $d$, the degree of each
state will follow a normal distribution with mean $1+(Q-1)d$ and
variance $(Q-1)d(1-d)$.
In particular =-d0= will cause all states to have 1 successors, and
=-d1= will cause all states to be interconnected.
#+NAME: randaut2
#+BEGIN_SRC sh :results verbatim :exports code
randaut -S3 -d0 2
randaut -Q3 -d0 2
#+END_SRC
#+RESULTS: randaut2
......@@ -114,7 +114,7 @@ $txt
#+NAME: randaut3
#+BEGIN_SRC sh :results verbatim :exports code
randaut -S3 -d1 2
randaut -Q3 -d1 2
#+END_SRC
#+RESULTS: randaut3
......@@ -191,20 +191,20 @@ randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p'
- =-a= (or =--acc-probability=) controls the probability that any
transition belong to a given acceptance set.
- =--state-acc= requests that the automaton use state-based
- =-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.)
In addition, =-B= (or =--ba=) is a shorthand for =-A1 --state-acc=,
In addition, =-B= (or =--ba=) is a shorthand for =-A1 -S=,
ans =-s= (or =--spin=) implies =-B=.
#+NAME: randaut4
#+BEGIN_SRC sh :results verbatim :exports code
randaut -S3 -d0.5 -A3 -a0.5 2
randaut -Q3 -d0.5 -A3 -a0.5 2
#+END_SRC
#+RESULTS: randaut4
......@@ -237,7 +237,7 @@ $txt
#+NAME: randaut5
#+BEGIN_SRC sh :results verbatim :exports code
randaut -S3 -d0.4 -B -a0.7 2
randaut -Q3 -d0.4 -B -a0.7 2
#+END_SRC
#+RESULTS: randaut5
......@@ -268,7 +268,7 @@ $txt
#+NAME: randaut5b
#+BEGIN_SRC sh :results verbatim :exports code
randaut -S6 -d0.4 --state-acc -a.2 -A 'Streett 1..3' 2 --dot=.a
randaut -Q6 -d0.4 --state-acc -a.2 -A 'Streett 1..3' 2 --dot=.a
#+END_SRC
#+RESULTS: randaut5b
......@@ -284,27 +284,27 @@ digraph G {
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 [label=<0>]
0 -> 2 [label=<!p0 &amp; !p1>]
0 -> 1 [label=<!p0 &amp; !p1<br/><font color="#FAA43A">❷</font>>]
0 -> 5 [label=<!p0 &amp; !p1>]
1 [label="1"]
1 -> 0 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
1 -> 3 [label=<!p0 &amp; !p1>]
2 [label="2"]
2 -> 5 [label=<!p0 &amp; !p1<br/><font color="#F17CB0">❶</font>>]
2 -> 3 [label=<p0 &amp; !p1<br/><font color="#5DA5DA">⓿</font>>]
2 -> 2 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font>>]
0 -> 1 [label=<!p0 &amp; !p1>]
0 -> 3 [label=<!p0 &amp; !p1>]
1 [label=<1>]
1 -> 5 [label=<!p0 &amp; p1>]
2 [label=<2<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
2 -> 0 [label=<!p0 &amp; p1>]
2 -> 4 [label=<!p0 &amp; !p1>]
3 [label="3"]
3 -> 2 [label=<p0 &amp; p1<br/><font color="#F17CB0">❶</font>>]
4 [label="4"]
4 -> 3 [label=<!p0 &amp; !p1>]
4 -> 5 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
5 [label="5"]
5 -> 0 [label=<p0 &amp; p1>]
5 -> 3 [label=<p0 &amp; p1>]
5 -> 2 [label=<!p0 &amp; p1<br/><font color="#B276B2">❸</font>>]
3 [label=<3>]
3 -> 1 [label=<!p0 &amp; !p1>]
3 -> 2 [label=<p0 &amp; !p1>]
3 -> 5 [label=<!p0 &amp; !p1>]
3 -> 4 [label=<p0 &amp; !p1>]
4 [label=<4<br/><font color="#B276B2">❸</font>>]
4 -> 2 [label=<p0 &amp; !p1>]
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>]
}
#+end_example
......@@ -331,7 +331,7 @@ therefore deterministic and complete.
#+NAME: randaut6
#+BEGIN_SRC sh :results verbatim :exports code
randaut -D -S3 -d0.6 -A2 -a0.5 2
randaut -D -Q3 -d0.6 -A2 -a0.5 2
#+END_SRC
#+RESULTS: randaut6
......@@ -366,7 +366,7 @@ $txt
Note that in a deterministic automaton with $a$ atomic propositions,
it is not possible to have states with more than $2^a$ successors. If
the combination of =-d= and =-S= allows the situation where a state
the combination of =-d= and =-Q= allows the situation where a state
can have more than $2^a$ successors, the degree will be clipped to
$2^a$. When working with random deterministic automata over $a$
atomic propositions, we suggest you always request more than $2^a$
......
......@@ -47,29 +47,28 @@ const char argp_program_doc[] = "\
Generate random connected automata.\n\n\
The automata are built over the atomic propositions named by PROPS...\n\
or, if N is a nonnegative number, using N arbitrary names.\n\
If the density is set to D, and the number of states to S, the degree\n\
of each state follows a normal distribution with mean 1+(S-1)D and\n\
variance (S-1)D(1-D). In particular, for D=0 all states have a single\n\
If the density is set to D, and the number of states to Q, the degree\n\
of each state follows a normal distribution with mean 1+(Q-1)D and\n\
variance (Q-1)D(1-D). In particular, for D=0 all states have a single\n\
successor, while for D=1 all states are interconnected.\v\
Examples:\n\
\n\
This builds a random neverclaim with 4 states and labeled using the two\n\
atomic propositions \"a\" and \"b\":\n\
% randaut --spin -S4 a b\n\
% randaut --spin -Q4 a b\n\
\n\
This builds three random, complete, and deterministic TGBA with 5 to 10\n\
states, 1 to 3 acceptance sets, and three atomic propositions:\n\
% randaut -n3 -D -H -S5..10 -A1..3 3\n\
% randaut -n3 -D -H -Q5..10 -A1..3 3\n\
\n\
Build 3 random, complete, and deterministic Rabin automata\n\
with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \n\
a high density of transitions, and 3 to 4 atomic propositions:\n\
% randaut -n3 -D -H -S8 -d.8 --state-based -A 'Rabin 2..3' 3..4\n\
% randaut -n3 -D -H -Q8 -d.8 -S -A 'Rabin 2..3' 3..4\n\
";
enum {
OPT_SEED = 1,
OPT_STATE_ACC,
};
static const argp_option options[] =
......@@ -92,8 +91,9 @@ static const argp_option options[] =
"are isomorphic)", 0 },
{ "seed", OPT_SEED, "INT", 0,
"seed for the random number generator (0)", 0 },
{ "states", 'S', "RANGE", 0, "number of states to output (10)", 0 },
{ "state-acc", OPT_STATE_ACC, 0, 0, "use state-based acceptance", 0 },
{ "states", 'Q', "RANGE", 0, "number of states to output (10)", 0 },
{ "state-based-acceptance", 'S', 0, 0, "used state-based acceptance", 0 },
{ "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
RANGE_DOC,
{ 0, 0, 0, 0, "ACCEPTANCE may be either a RANGE (in which case "
"generalized Büchi is assumed), or an arbitrary acceptance formula "
......@@ -212,11 +212,14 @@ parse_opt(int key, char* arg, struct argp_state* as)
case 'n':
opt_automata = to_int(arg);
break;
case 'S':
case 'Q':
opt_states = parse_range(arg);
if (opt_states.min > opt_states.max)
std::swap(opt_states.min, opt_states.max);
break;
case 'S':
opt_state_acc = true;
break;
case 'u':
opt_uniq =
std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
......@@ -225,9 +228,6 @@ parse_opt(int key, char* arg, struct argp_state* as)
opt_seed = to_int(arg);
opt_seed_str = arg;
break;
case OPT_STATE_ACC:
opt_state_acc = true;
break;
case ARGP_KEY_ARG:
// If this is the unique non-option argument, it can
// be a number of atomic propositions to build.
......
......@@ -23,11 +23,11 @@
set -e
for i in 0 1 2; do
../../bin/randaut a b --seed=$i -S10 --hoa >iso$i
../../bin/randaut a b --seed=$i -Q10 --hoa >iso$i
../../bin/autfilt iso$i --randomize --hoa >aut$i
done
for i in 3 4 5; do
../../bin/randaut a b --seed=$i -S10 -D --hoa >iso$i
../../bin/randaut a b --seed=$i -Q10 -D --hoa >iso$i
../../bin/autfilt iso$i --randomize --hoa >aut$i
done
......
......@@ -25,13 +25,13 @@ set -e
randaut=../../bin/randaut
autfilt=../../bin/autfilt
$randaut --spin -S4 a b | ../ltl2tgba -H -XN - >out
$randaut --spin -Q4 a b | ../ltl2tgba -H -XN - >out
grep 'States: 4' out
grep 'AP: 2' out
grep 'state-acc' out
grep 'Acceptance: 1' out
$randaut -n 3 --hoa -S5..9 -A1..3 3 >out
$randaut -n 3 --hoa -Q5..9 -A1..3 3 >out
test `grep -c 'States: [5-9]$' out` = 3
test `grep -c 'Acceptance: [1-3] ' out` = 3
test `grep -c 'AP: 3 ' out` = 3
......@@ -72,8 +72,8 @@ diff out2 expected
$randaut -n 5 --dot=@ a 2>stderr && exit 1
grep 'randaut: unknown option.*@' stderr
$randaut -n -1 -S2 2 -H | $autfilt -H --is-deterministic -n 3 -o out.hoa
$randaut -n -1 -S2 2 -H | $autfilt -H -v --is-deterministic -n 4 -o '>>out.hoa'
$randaut -n -1 -Q2 2 -H | $autfilt -H --is-deterministic -n 3 -o out.hoa
$randaut -n -1 -Q2 2 -H | $autfilt -H -v --is-deterministic -n 4 -o '>>out.hoa'
$autfilt -H out.hoa -o 'out-det%d.hoa'
$autfilt -H out.hoa -o '>>out-det%d.hoa'
test 8 = `$autfilt -c out-det0.hoa`
......@@ -83,10 +83,10 @@ $autfilt -H out.hoa -o foo -c 2>stderr && exit 1
grep 'autfilt: options --output and --count are incompatible' stderr
(
$randaut -n 2 -S5 -A4 -H 2
$randaut -A 'random 4' -n 2 -S5 -H 2
$randaut -A 'parity rand rand 2..4' -n3 -S5 -H 2
$randaut -A 'generalized-Rabin 3 1..2 2..3 0' -n3 -S5 -H 2
$randaut -n 2 -Q5 -A4 -H 2
$randaut -A 'random 4' -n 2 -Q5 -H 2
$randaut -A 'parity rand rand 2..4' -n3 -Q5 -H 2
$randaut -A 'generalized-Rabin 3 1..2 2..3 0' -n3 -Q5 -H 2
) | grep -E '(acc-name:|Acceptance:)' > output
cat output
......
......@@ -23,9 +23,9 @@
set -e
for n in 10 20 30 40 50 60 70 80 90 100 200 500 1000; do
# Make sure graph generated by randaut have successors for each
# Make sure graphs generated by randaut have successors for each
# of their $n nodes.
../../bin/randaut -S$n 3 -Hl |
../../bin/randaut -Q$n 3 -Hl |
sed 's/.*--BODY--//;s/State:/\n&/g;s/--END--//' > out
grep -q 'State: [0-9][0-9]* .*$' out
grep -q 'State: [0-9]* *$' out && exit 1
......
......@@ -95,7 +95,7 @@ cat stdout
run 0 ../../bin/autfilt -F stdout --isomorph expected
# Likewise, with a randomly generated TGBA.
run 0 ../../bin/randaut -S 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input
run 0 ../../bin/randaut -Q 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input
# the first read-write can renumber the states
run 0 $autfilt --hoa --merge-transitions input > stdout
......
......@@ -21,8 +21,8 @@
. ./defs
set -e
../../bin/randaut a b -S5 --hoa > aut1
../../bin/randaut a b c -S10 --hoa > aut2
../../bin/randaut a b -Q5 --hoa > aut1
../../bin/randaut a b c -Q10 --hoa > aut2
../../bin/autfilt --randomize aut1 --hoa > rand11
../../bin/autfilt --randomize --seed=1 aut1 --hoa > rand12
../../bin/autfilt --randomize --seed=2 aut1 --hoa > rand13
......@@ -36,7 +36,7 @@ cat aut1 aut2 rand11 rand12 rand13 rand21 rand22 rand23 > all
diff aut out
run 0 ../../bin/randaut -Hl -u -n 4 -S1 a b | sort |
run 0 ../../bin/randaut -Hl -u -n 4 -Q1 a b | sort |
../../bin/autfilt -H | grep '&' > out
cat >expected <<EOF
[!0&!1] 0
......@@ -48,7 +48,7 @@ diff out expected
# This should fail: the random automaton generator can only generate 4
# different one-state automaton with two atomic propositions.
../../bin/randaut -Hl -u -n 5 -S1 a b >out 2>stderr && exit 1
../../bin/randaut -Hl -u -n 5 -Q1 a b >out 2>stderr && exit 1
test $? = 2
grep 'failed to generate a new unique automaton' stderr
test 4 = `wc -l < out`
......@@ -42,7 +42,7 @@
"collapsed": false,
"input": [
"txt = \"<TABLE><TR><TH>before</TH><TH>after</TH>\"\n",
"for a in spot.automata('randaut -A \"random 4\" -H -S5 -n10 2|'):\n",
"for a in spot.automata('randaut -A \"random 4\" -H -Q5 -n10 2|'):\n",
" txt += \"<TR><TD>{0}</TD><TD>{1}</TD></TR>\".format(a.show('.a').data, spot.cleanup_acceptance(a).show('.a').data)\n",
"txt += (\"</TABLE>\")\n",
"HTML(txt)"
......@@ -2006,4 +2006,4 @@
"metadata": {}
}
]
}
\ No newline at end of file
}
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