diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 964c50c00..78c92faea 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -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: diff --git a/doc/org/oaut.org b/doc/org/oaut.org index c39c34620..2faf91e09 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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 '>>'.) diff --git a/doc/org/randaut.org b/doc/org/randaut.org index e02ba5897..c5966be61 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -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=] - 0 -> 1 [label=❷>] - 0 -> 5 [label=] - 1 [label="1"] - 1 -> 0 [label=⓿❷>] - 1 -> 3 [label=] - 2 [label="2"] - 2 -> 5 [label=❶>] - 2 -> 3 [label=⓿>] - 2 -> 2 [label=⓿>] + 0 -> 1 [label=] + 0 -> 3 [label=] + 1 [label=<1>] + 1 -> 5 [label=] + 2 [label=<2
⓿❷>] + 2 -> 0 [label=] 2 -> 4 [label=] - 3 [label="3"] - 3 -> 2 [label=❶>] - 4 [label="4"] - 4 -> 3 [label=] - 4 -> 5 [label=⓿❶>] - 5 [label="5"] - 5 -> 0 [label=] - 5 -> 3 [label=] - 5 -> 2 [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=] + 5 -> 1 [label=] } #+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$ diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 6be931569..88479dce4 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -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(new std::set>()); @@ -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. diff --git a/src/tests/isomorph.test b/src/tests/isomorph.test index e463c872c..98d80367e 100755 --- a/src/tests/isomorph.test +++ b/src/tests/isomorph.test @@ -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 diff --git a/src/tests/randaut.test b/src/tests/randaut.test index 095a49e64..633fea7bb 100755 --- a/src/tests/randaut.test +++ b/src/tests/randaut.test @@ -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 diff --git a/src/tests/randtgba.test b/src/tests/randtgba.test index debece47b..2f0e3187b 100755 --- a/src/tests/randtgba.test +++ b/src/tests/randtgba.test @@ -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 diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 831cf77bd..02474ba35 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -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 diff --git a/src/tests/uniq.test b/src/tests/uniq.test index 685a938a9..596873386 100755 --- a/src/tests/uniq.test +++ b/src/tests/uniq.test @@ -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 <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` diff --git a/wrap/python/tests/randaut.ipynb b/wrap/python/tests/randaut.ipynb index 5a1d19bcb..ab39f177a 100644 --- a/wrap/python/tests/randaut.ipynb +++ b/wrap/python/tests/randaut.ipynb @@ -42,7 +42,7 @@ "collapsed": false, "input": [ "txt = \"\"\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 += \"\".format(a.show('.a').data, spot.cleanup_acceptance(a).show('.a').data)\n", "txt += (\"
beforeafter
{0}{1}
\")\n", "HTML(txt)" @@ -2006,4 +2006,4 @@ "metadata": {} } ] -} \ No newline at end of file +}