From ea5f52ddbb06103a41ab2cf55e961340dab6dc58 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Jan 2016 15:54:11 +0100 Subject: [PATCH] randaut: rename -d as -e This is so that we can have -d as an alias for --dot everywhere. * bin/randaut.cc: Rename -d as -e. * NEWS: Mention the change. * doc/org/autfilt.org, doc/org/oaut.org, doc/org/randaut.org, tests/core/parseaut.test, tests/core/readsave.test: Adjust. --- NEWS | 3 ++ bin/randaut.cc | 10 ++--- doc/org/autfilt.org | 22 +++++----- doc/org/oaut.org | 2 +- doc/org/randaut.org | 68 ++++++++++++++++------------- tests/core/parseaut.test | 6 +-- tests/core/readsave.test | 92 +++++++++++++++++++--------------------- 7 files changed, 106 insertions(+), 97 deletions(-) diff --git a/NEWS b/NEWS index 3a6a94b77..c4e2d019f 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,9 @@ New in spot 1.99.6a (not yet released) Command-line tools: + * randaut's short option for --density used to be -d. It has been renamed + to -e so that -d means --dot in all tools. + * autfilt has a new option: --is-inherently-weak. Library: diff --git a/bin/randaut.cc b/bin/randaut.cc index f0ce89313..95e060e5a 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -46,7 +46,7 @@ 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 Q, the degree\n\ +If the edge 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\ @@ -63,7 +63,7 @@ states, 1 to 3 acceptance sets, and three atomic propositions:\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 edges, and 3 to 4 atomic propositions:\n\ - % randaut -n3 -D -H -Q8 -d.8 -S -A 'Rabin 2..3' 3..4\n\ + % randaut -n3 -D -H -Q8 -e.8 -S -A 'Rabin 2..3' 3..4\n\ "; enum { @@ -86,7 +86,7 @@ static const argp_option options[] = { "colored", OPT_COLORED, nullptr, 0, "build an automaton in which each edge (or state if combined with " "-S) belong to a single acceptance set", 0 }, - { "density", 'd', "FLOAT", 0, "density of the edges (0.2)", 0 }, + { "density", 'e', "FLOAT", 0, "density of the edges (0.2)", 0 }, { "deterministic", 'D', nullptr, 0, "build a complete, deterministic automaton ", 0 }, { "unique", 'u', nullptr, 0, @@ -206,7 +206,7 @@ parse_opt(int key, char* arg, struct argp_state* as) ba_options(); ba_wanted = true; break; - case 'd': + case 'e': opt_density = to_float(arg); if (opt_density < 0.0 || opt_density > 1.0) error(2, 0, "density should be between 0.0 and 1.0"); diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 0d599524b..13dff0990 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -102,22 +102,22 @@ statistics. #+BEGIN_SRC sh :results verbatim :exports both -randaut --hoa -n 10 -A0..2 -Q10..20 -d0.05 2 | +randaut --hoa -n 10 -A0..2 -Q10..20 -e0.05 2 | autfilt --stats='%s states, %e edges, %a acc-sets, %c SCCs, det=%d' #+END_SRC #+RESULTS: #+begin_example -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 +16 states, 30 edges, 1 acc-sets, 3 SCCs, det=0 +20 states, 42 edges, 2 acc-sets, 1 SCCs, det=0 +15 states, 27 edges, 2 acc-sets, 1 SCCs, det=0 +10 states, 17 edges, 1 acc-sets, 1 SCCs, det=1 +13 states, 25 edges, 1 acc-sets, 1 SCCs, det=0 +11 states, 18 edges, 0 acc-sets, 1 SCCs, det=0 +19 states, 41 edges, 2 acc-sets, 1 SCCs, det=0 +11 states, 18 edges, 0 acc-sets, 1 SCCs, det=0 +12 states, 21 edges, 1 acc-sets, 5 SCCs, det=0 +18 states, 37 edges, 1 acc-sets, 5 SCCs, det=0 #+end_example The following =%= sequences are available: diff --git a/doc/org/oaut.org b/doc/org/oaut.org index dff34b408..99eebcec5 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -875,7 +875,7 @@ 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 -d0.2 -Q100 -n1000 a --stats %e > size.csv +randaut -e0.2 -Q100 -n1000 a --stats %e > size.csv R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))" #+END_SRC diff --git a/doc/org/randaut.org b/doc/org/randaut.org index 9b21e547b..9d3d186b0 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -73,35 +73,36 @@ 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 +The number of edges can be controlled using the =-e= (or =--density=) option. The argument should be a number between 0 and 1. -In an automaton with $Q$ states and density $d$, the degree of each +In an automaton with $Q$ states and density $e$, the degree of each state will follow a normal distribution with mean $1+(Q-1)d$ and -variance $(Q-1)d(1-d)$. +variance $(Q-1)e(1-e)$. -In particular =-d0= will cause all states to have 1 successors, and -=-d1= will cause all states to be interconnected. +In particular =-e0= will cause all states to have 1 successors, and +=-e1= will cause all states to be interconnected. #+NAME: randaut2 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -d0 2 +randaut -Q3 -e0 2 #+END_SRC #+RESULTS: randaut2 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + 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=] - 1 [label="1"] + 1 [label=<1>] 1 -> 1 [label=] - 2 [label="2"] + 2 [label=<2>] 2 -> 1 [label=] } #+end_example @@ -114,28 +115,29 @@ $txt #+NAME: randaut3 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -d1 2 +randaut -Q3 -e1 2 #+END_SRC #+RESULTS: randaut3 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + 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 -> 0 [label=] 0 -> 1 [label=] - 1 [label="1"] + 1 [label=<1>] 1 -> 1 [label=] 1 -> 2 [label=] 1 -> 0 [label=] - 2 [label="2"] + 2 [label=<2>] 2 -> 1 [label=] 2 -> 0 [label=] 2 -> 2 [label=] @@ -209,27 +211,30 @@ ans =-s= (or =--spin=) implies =-B=. #+NAME: randaut4 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -d0.5 -A3 -a0.5 2 +randaut -Q3 -e0.5 -A3 -a0.5 2 #+END_SRC #+RESULTS: randaut4 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 1 [label=] 0 -> 0 [label=❷>] 1 [label="1"] - 1 -> 2 [label=❶❷>] + 1 -> 1 [label=⓿❶>] + 1 -> 2 [label=❶>] 2 [label="2"] - 2 -> 2 [label=⓿>] - 2 -> 1 [label=⓿❶>] + 2 -> 1 [label=⓿>] + 2 -> 0 [label=⓿>] + 2 -> 2 [label=⓿>] } #+end_example @@ -242,26 +247,30 @@ $txt #+NAME: randaut5 #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q3 -d0.4 -B -a0.7 2 +randaut -Q3 -e0.4 -B -a0.7 2 #+END_SRC #+RESULTS: randaut5 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label="0"] + 0 -> 1 [label=] 0 -> 2 [label=] - 1 [label="1"] - 1 -> 2 [label=] + 1 [label="1", peripheries=2] + 1 -> 1 [label=] + 1 -> 0 [label=] 2 [label="2", peripheries=2] + 2 -> 0 [label=] + 2 -> 2 [label=] 2 -> 1 [label=] - 2 -> 0 [label=] } #+end_example @@ -273,7 +282,7 @@ $txt #+NAME: randaut5b #+BEGIN_SRC sh :results verbatim :exports code -randaut -Q6 -d0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a +randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a #+END_SRC #+RESULTS: randaut5b @@ -402,17 +411,18 @@ therefore deterministic and complete. #+NAME: randaut6 #+BEGIN_SRC sh :results verbatim :exports code -randaut -D -Q3 -d0.6 -A2 -a0.5 2 +randaut -D -Q3 -e0.6 -A2 -a0.5 2 #+END_SRC #+RESULTS: randaut6 #+begin_example digraph G { rankdir=LR + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -437,7 +447,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 =-Q= allows the situation where a state +the combination of =-e= 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/tests/core/parseaut.test b/tests/core/parseaut.test index 54d21dd95..48a3ed959 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -1218,7 +1218,7 @@ grep "identifier.*v1" output.err # This was generated by -# randaut -n 10 -Hl 3 -d 0.055 --seed=3 | fmt +# randaut -n 10 -Hl 3 -e 0.055 --seed=3 | fmt cat > input <input <<\EOF HOA: v1 States: 3 @@ -48,10 +44,10 @@ State: 2 --END-- EOF -run 0 $autfilt --hoa input > stdout +run 0 autfilt --hoa input > stdout diff stdout input -test `$autfilt -c --is-weak input` = 0 +test `autfilt -c --is-weak input` = 0 # Transition merging cat >input <<\EOF @@ -97,23 +93,23 @@ cat stdout run 0 autfilt -F stdout --isomorph expected # Likewise, with a randomly generated TGBA. -run 0 randaut -Q 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input +run 0 randaut -Q 20 a b -e 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 +run 0 autfilt --hoa --merge-transitions input > stdout run 0 autfilt -F input --isomorph stdout # But this second output should be the same as the first -run 0 $autfilt --hoa stdout > stdout2 +run 0 autfilt --hoa stdout > stdout2 diff stdout stdout2 # Find formula that can be translated into a 3-state automaton, and # exercise both %M and %m. The nonexistant file should never be # open, because the input stream is infinite and autfilt should # stop after 10 automata. -$randltl -n -1 a b | - $ltl2tgba -H -F - | - $autfilt -F- -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \ +randltl -n -1 a b | + ltl2tgba -H -F - | + autfilt -F- -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \ --name='%M, %S states' --stats='<%m>, %e, %a' -n 10 > output cat >expected <, 5, 1 @@ -270,16 +266,16 @@ State: 9 --END-- EOF -$autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output +autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output diff output expected -cat < tmp.hoa +cat < tmp.hoa a U b false !b && Xb && GFa EOF -$autfilt output +autfilt output cat >expected <output +autfilt -H input | + SPOT_DOTDEFAULT=vcsn SPOT_DOTEXTRA='/* hello world */' autfilt >output cat >expected <output +ltl2tgba --dot=a 'GFa & GFb' >output cat output cat >expected <output +ltl2tgba --dot=ban 'GFa & GFb' >output cat output cat >expected <output +SPOT_DOTDEFAULT=bra ltl2tgba --dot='e.f(Lato)' 'GFa & GFb' >output cat output zero='⓿' @@ -510,7 +506,7 @@ digraph G { } EOF -$autfilt --dot=bao in >out +autfilt --dot=bao in >out diff out expected cat >expected2 <' >out +autfilt --dot=bao1 in | grep -v '>' >out diff out expected2 # Let's pretend that this is some used supplied input, as discussed in @@ -571,7 +567,7 @@ EOF # status here, because the actual error messages are tested in # parseaut.test) and produce a valid output with the number of states # fixed, and the missing state definitions. -$autfilt -H input >output1 && exit 1 +autfilt -H input >output1 && exit 1 cat >expect1 < output1b +autfilt -H output1 > output1b diff output1 output1b # Here is the scenario where the undefined states are actually states # we wanted to remove. So we tell autfilt to fix the automaton using # --remove-dead-states -$autfilt -H --remove-dead input >output2 && exit 1 +autfilt -H --remove-dead input >output2 && exit 1 cat >expect2 <output2b +autfilt -Hk expect2 >output2b cat >expect2b <output3 -$autfilt -H --remove-dead input >>output3 +autfilt -H --remove-unreach input >output3 +autfilt -H --remove-dead input >>output3 cat >expect3 <stderr && exit 1 +autfilt -Hz input 2>stderr && exit 1 grep 'print_hoa.*z' stderr cat >input4 <output4 -$autfilt -H --small input4 >output4b -$autfilt -H --high input4 >output4c +autfilt -H --small --high input4 >output4 +autfilt -H --small input4 >output4b +autfilt -H --high input4 >output4c cat output4 cat >expect4<output5 -test `$autfilt --is-weak -c output4` = 1 -test `$autfilt --is-terminal -c output4` = 0 +autfilt -Hv --small input4 >output5 +test `autfilt --is-weak -c output4` = 1 +test `autfilt --is-terminal -c output4` = 0 sed 's/\[0\]/[t]/g' expect4 > output4d -test `$autfilt --is-terminal -c output4d` = 1 +test `autfilt --is-terminal -c output4d` = 1 cat >expect5<output6 +run 0 autfilt -Hk input6 >output6 cat >expect6 <output7 +test `autfilt -c --is-inherently-weak input7` = 1 +test `autfilt -c --is-weak input7` = 0 +autfilt --check input7 -H >output7 cat >expected7 <