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.
This commit is contained in:
Alexandre Duret-Lutz
parent
8c04e31a35
commit
ea5f52ddbb
7 changed files with 106 additions and 97 deletions
3
NEWS
3
NEWS
|
|
@ -2,6 +2,9 @@ New in spot 1.99.6a (not yet released)
|
||||||
|
|
||||||
Command-line tools:
|
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.
|
* autfilt has a new option: --is-inherently-weak.
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// 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\
|
Generate random connected automata.\n\n\
|
||||||
The automata are built over the atomic propositions named by PROPS...\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\
|
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\
|
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\
|
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\
|
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\
|
Build 3 random, complete, and deterministic Rabin automata\n\
|
||||||
with 2 to 3 acceptance pairs, state-based acceptance, 8 states, \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\
|
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 {
|
enum {
|
||||||
|
|
@ -86,7 +86,7 @@ static const argp_option options[] =
|
||||||
{ "colored", OPT_COLORED, nullptr, 0,
|
{ "colored", OPT_COLORED, nullptr, 0,
|
||||||
"build an automaton in which each edge (or state if combined with "
|
"build an automaton in which each edge (or state if combined with "
|
||||||
"-S) belong to a single acceptance set", 0 },
|
"-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,
|
{ "deterministic", 'D', nullptr, 0,
|
||||||
"build a complete, deterministic automaton ", 0 },
|
"build a complete, deterministic automaton ", 0 },
|
||||||
{ "unique", 'u', nullptr, 0,
|
{ "unique", 'u', nullptr, 0,
|
||||||
|
|
@ -206,7 +206,7 @@ parse_opt(int key, char* arg, struct argp_state* as)
|
||||||
ba_options();
|
ba_options();
|
||||||
ba_wanted = true;
|
ba_wanted = true;
|
||||||
break;
|
break;
|
||||||
case 'd':
|
case 'e':
|
||||||
opt_density = to_float(arg);
|
opt_density = to_float(arg);
|
||||||
if (opt_density < 0.0 || opt_density > 1.0)
|
if (opt_density < 0.0 || opt_density > 1.0)
|
||||||
error(2, 0, "density should be between 0.0 and 1.0");
|
error(2, 0, "density should be between 0.0 and 1.0");
|
||||||
|
|
|
||||||
|
|
@ -102,22 +102,22 @@ statistics.
|
||||||
|
|
||||||
|
|
||||||
#+BEGIN_SRC sh :results verbatim :exports both
|
#+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'
|
autfilt --stats='%s states, %e edges, %a acc-sets, %c SCCs, det=%d'
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS:
|
#+RESULTS:
|
||||||
#+begin_example
|
#+begin_example
|
||||||
16 states, 28 edges, 1 acc-sets, 1 SCCs, det=0
|
16 states, 30 edges, 1 acc-sets, 3 SCCs, det=0
|
||||||
19 states, 37 edges, 0 acc-sets, 1 SCCs, det=0
|
20 states, 42 edges, 2 acc-sets, 1 SCCs, det=0
|
||||||
16 states, 24 edges, 1 acc-sets, 1 SCCs, det=0
|
15 states, 27 edges, 2 acc-sets, 1 SCCs, det=0
|
||||||
12 states, 16 edges, 0 acc-sets, 5 SCCs, det=0
|
10 states, 17 edges, 1 acc-sets, 1 SCCs, det=1
|
||||||
12 states, 17 edges, 2 acc-sets, 3 SCCs, det=0
|
13 states, 25 edges, 1 acc-sets, 1 SCCs, det=0
|
||||||
15 states, 21 edges, 2 acc-sets, 5 SCCs, det=0
|
11 states, 18 edges, 0 acc-sets, 1 SCCs, det=0
|
||||||
10 states, 12 edges, 0 acc-sets, 4 SCCs, det=1
|
19 states, 41 edges, 2 acc-sets, 1 SCCs, det=0
|
||||||
10 states, 14 edges, 1 acc-sets, 1 SCCs, det=0
|
11 states, 18 edges, 0 acc-sets, 1 SCCs, det=0
|
||||||
19 states, 27 edges, 1 acc-sets, 1 SCCs, det=0
|
12 states, 21 edges, 1 acc-sets, 5 SCCs, det=0
|
||||||
11 states, 12 edges, 1 acc-sets, 9 SCCs, det=1
|
18 states, 37 edges, 1 acc-sets, 5 SCCs, det=0
|
||||||
#+end_example
|
#+end_example
|
||||||
|
|
||||||
The following =%= sequences are available:
|
The following =%= sequences are available:
|
||||||
|
|
|
||||||
|
|
@ -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:
|
use =R= to summarize the distribution of these values:
|
||||||
|
|
||||||
#+BEGIN_SRC sh :results verbatim :exports both
|
#+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'))"
|
R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))"
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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
|
option will accept a range as argument, so for instance =-Q3..6= will
|
||||||
generate an automaton with 3 to 6 states.
|
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.
|
=--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
|
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
|
In particular =-e0= will cause all states to have 1 successors, and
|
||||||
=-d1= will cause all states to be interconnected.
|
=-e1= will cause all states to be interconnected.
|
||||||
|
|
||||||
#+NAME: randaut2
|
#+NAME: randaut2
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+BEGIN_SRC sh :results verbatim :exports code
|
||||||
randaut -Q3 -d0 2
|
randaut -Q3 -e0 2
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: randaut2
|
#+RESULTS: randaut2
|
||||||
#+begin_example
|
#+begin_example
|
||||||
digraph G {
|
digraph G {
|
||||||
rankdir=LR
|
rankdir=LR
|
||||||
|
node [shape="circle"]
|
||||||
fontname="Lato"
|
fontname="Lato"
|
||||||
node [fontname="Lato"]
|
node [fontname="Lato"]
|
||||||
edge [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 [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label=<0>]
|
||||||
0 -> 2 [label=<!p0 & !p1>]
|
0 -> 2 [label=<!p0 & !p1>]
|
||||||
1 [label="1"]
|
1 [label=<1>]
|
||||||
1 -> 1 [label=<!p0 & !p1>]
|
1 -> 1 [label=<!p0 & !p1>]
|
||||||
2 [label="2"]
|
2 [label=<2>]
|
||||||
2 -> 1 [label=<!p0 & !p1>]
|
2 -> 1 [label=<!p0 & !p1>]
|
||||||
}
|
}
|
||||||
#+end_example
|
#+end_example
|
||||||
|
|
@ -114,28 +115,29 @@ $txt
|
||||||
|
|
||||||
#+NAME: randaut3
|
#+NAME: randaut3
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+BEGIN_SRC sh :results verbatim :exports code
|
||||||
randaut -Q3 -d1 2
|
randaut -Q3 -e1 2
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: randaut3
|
#+RESULTS: randaut3
|
||||||
#+begin_example
|
#+begin_example
|
||||||
digraph G {
|
digraph G {
|
||||||
rankdir=LR
|
rankdir=LR
|
||||||
|
node [shape="circle"]
|
||||||
fontname="Lato"
|
fontname="Lato"
|
||||||
node [fontname="Lato"]
|
node [fontname="Lato"]
|
||||||
edge [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 [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label=<0>]
|
||||||
0 -> 2 [label=<!p0 & !p1>]
|
0 -> 2 [label=<!p0 & !p1>]
|
||||||
0 -> 0 [label=<!p0 & !p1>]
|
0 -> 0 [label=<!p0 & !p1>]
|
||||||
0 -> 1 [label=<!p0 & !p1>]
|
0 -> 1 [label=<!p0 & !p1>]
|
||||||
1 [label="1"]
|
1 [label=<1>]
|
||||||
1 -> 1 [label=<p0 & p1>]
|
1 -> 1 [label=<p0 & p1>]
|
||||||
1 -> 2 [label=<p0 & !p1>]
|
1 -> 2 [label=<p0 & !p1>]
|
||||||
1 -> 0 [label=<p0 & !p1>]
|
1 -> 0 [label=<p0 & !p1>]
|
||||||
2 [label="2"]
|
2 [label=<2>]
|
||||||
2 -> 1 [label=<!p0 & !p1>]
|
2 -> 1 [label=<!p0 & !p1>]
|
||||||
2 -> 0 [label=<p0 & !p1>]
|
2 -> 0 [label=<p0 & !p1>]
|
||||||
2 -> 2 [label=<p0 & !p1>]
|
2 -> 2 [label=<p0 & !p1>]
|
||||||
|
|
@ -209,27 +211,30 @@ ans =-s= (or =--spin=) implies =-B=.
|
||||||
|
|
||||||
#+NAME: randaut4
|
#+NAME: randaut4
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+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
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: randaut4
|
#+RESULTS: randaut4
|
||||||
#+begin_example
|
#+begin_example
|
||||||
digraph G {
|
digraph G {
|
||||||
rankdir=LR
|
rankdir=LR
|
||||||
|
node [shape="circle"]
|
||||||
fontname="Lato"
|
fontname="Lato"
|
||||||
node [fontname="Lato"]
|
node [fontname="Lato"]
|
||||||
edge [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 [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label="0"]
|
||||||
0 -> 1 [label=<!p0 & !p1>]
|
0 -> 1 [label=<!p0 & !p1>]
|
||||||
0 -> 0 [label=<!p0 & !p1<br/><font color="#FAA43A">❷</font>>]
|
0 -> 0 [label=<!p0 & !p1<br/><font color="#FAA43A">❷</font>>]
|
||||||
1 [label="1"]
|
1 [label="1"]
|
||||||
1 -> 2 [label=<!p0 & p1<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
|
1 -> 1 [label=<!p0 & p1<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
||||||
|
1 -> 2 [label=<!p0 & p1<br/><font color="#F17CB0">❶</font>>]
|
||||||
2 [label="2"]
|
2 [label="2"]
|
||||||
2 -> 2 [label=<!p0 & !p1<br/><font color="#5DA5DA">⓿</font>>]
|
2 -> 1 [label=<!p0 & p1<br/><font color="#5DA5DA">⓿</font>>]
|
||||||
2 -> 1 [label=<p0 & !p1<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
2 -> 0 [label=<p0 & p1<br/><font color="#5DA5DA">⓿</font>>]
|
||||||
|
2 -> 2 [label=<!p0 & p1<br/><font color="#5DA5DA">⓿</font>>]
|
||||||
}
|
}
|
||||||
#+end_example
|
#+end_example
|
||||||
|
|
||||||
|
|
@ -242,26 +247,30 @@ $txt
|
||||||
|
|
||||||
#+NAME: randaut5
|
#+NAME: randaut5
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+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
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: randaut5
|
#+RESULTS: randaut5
|
||||||
#+begin_example
|
#+begin_example
|
||||||
digraph G {
|
digraph G {
|
||||||
rankdir=LR
|
rankdir=LR
|
||||||
|
node [shape="circle"]
|
||||||
fontname="Lato"
|
fontname="Lato"
|
||||||
node [fontname="Lato"]
|
node [fontname="Lato"]
|
||||||
edge [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 [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label="0"]
|
||||||
|
0 -> 1 [label=<!p0 & !p1>]
|
||||||
0 -> 2 [label=<!p0 & !p1>]
|
0 -> 2 [label=<!p0 & !p1>]
|
||||||
1 [label="1"]
|
1 [label="1", peripheries=2]
|
||||||
1 -> 2 [label=<!p0 & p1>]
|
1 -> 1 [label=<!p0 & !p1>]
|
||||||
|
1 -> 0 [label=<p0 & p1>]
|
||||||
2 [label="2", peripheries=2]
|
2 [label="2", peripheries=2]
|
||||||
|
2 -> 0 [label=<p0 & p1>]
|
||||||
|
2 -> 2 [label=<p0 & !p1>]
|
||||||
2 -> 1 [label=<!p0 & !p1>]
|
2 -> 1 [label=<!p0 & !p1>]
|
||||||
2 -> 0 [label=<p0 & !p1>]
|
|
||||||
}
|
}
|
||||||
#+end_example
|
#+end_example
|
||||||
|
|
||||||
|
|
@ -273,7 +282,7 @@ $txt
|
||||||
|
|
||||||
#+NAME: randaut5b
|
#+NAME: randaut5b
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+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
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: randaut5b
|
#+RESULTS: randaut5b
|
||||||
|
|
@ -402,17 +411,18 @@ therefore deterministic and complete.
|
||||||
|
|
||||||
#+NAME: randaut6
|
#+NAME: randaut6
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+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
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: randaut6
|
#+RESULTS: randaut6
|
||||||
#+begin_example
|
#+begin_example
|
||||||
digraph G {
|
digraph G {
|
||||||
rankdir=LR
|
rankdir=LR
|
||||||
|
node [shape="circle"]
|
||||||
fontname="Lato"
|
fontname="Lato"
|
||||||
node [fontname="Lato"]
|
node [fontname="Lato"]
|
||||||
edge [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 [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label="0"]
|
||||||
|
|
@ -437,7 +447,7 @@ $txt
|
||||||
|
|
||||||
Note that in a deterministic automaton with $a$ atomic propositions,
|
Note that in a deterministic automaton with $a$ atomic propositions,
|
||||||
it is not possible to have states with more than $2^a$ successors. If
|
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
|
can have more than $2^a$ successors, the degree will be clipped to
|
||||||
$2^a$. When working with random deterministic automata over $a$
|
$2^a$. When working with random deterministic automata over $a$
|
||||||
atomic propositions, we suggest you always request more than $2^a$
|
atomic propositions, we suggest you always request more than $2^a$
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
|
# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
|
||||||
# l'Epita (LRDE).
|
# Développement de l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
#
|
#
|
||||||
|
|
@ -1218,7 +1218,7 @@ grep "identifier.*v1" output.err
|
||||||
|
|
||||||
|
|
||||||
# This was generated by
|
# 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 <<EOF
|
cat > input <<EOF
|
||||||
HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance:
|
HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance:
|
||||||
0 t properties: trans-labels explicit-labels state-acc deterministic
|
0 t properties: trans-labels explicit-labels state-acc deterministic
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche
|
# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de
|
||||||
# et Développement de l'Epita (LRDE).
|
# Recherche et Développement de l'Epita (LRDE).
|
||||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
# et Marie Curie.
|
# et Marie Curie.
|
||||||
|
|
@ -26,10 +26,6 @@
|
||||||
|
|
||||||
set -e
|
set -e
|
||||||
|
|
||||||
autfilt=autfilt
|
|
||||||
ltl2tgba=ltl2tgba
|
|
||||||
randltl=randltl
|
|
||||||
|
|
||||||
cat >input <<\EOF
|
cat >input <<\EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 3
|
States: 3
|
||||||
|
|
@ -48,10 +44,10 @@ State: 2
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
run 0 $autfilt --hoa input > stdout
|
run 0 autfilt --hoa input > stdout
|
||||||
diff stdout input
|
diff stdout input
|
||||||
|
|
||||||
test `$autfilt -c --is-weak input` = 0
|
test `autfilt -c --is-weak input` = 0
|
||||||
|
|
||||||
# Transition merging
|
# Transition merging
|
||||||
cat >input <<\EOF
|
cat >input <<\EOF
|
||||||
|
|
@ -97,23 +93,23 @@ cat stdout
|
||||||
run 0 autfilt -F stdout --isomorph expected
|
run 0 autfilt -F stdout --isomorph expected
|
||||||
|
|
||||||
# Likewise, with a randomly generated TGBA.
|
# 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
|
# 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
|
run 0 autfilt -F input --isomorph stdout
|
||||||
|
|
||||||
# But this second output should be the same as the first
|
# 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
|
diff stdout stdout2
|
||||||
|
|
||||||
# Find formula that can be translated into a 3-state automaton, and
|
# Find formula that can be translated into a 3-state automaton, and
|
||||||
# exercise both %M and %m. The nonexistant file should never be
|
# exercise both %M and %m. The nonexistant file should never be
|
||||||
# open, because the input stream is infinite and autfilt should
|
# open, because the input stream is infinite and autfilt should
|
||||||
# stop after 10 automata.
|
# stop after 10 automata.
|
||||||
$randltl -n -1 a b |
|
randltl -n -1 a b |
|
||||||
$ltl2tgba -H -F - |
|
ltl2tgba -H -F - |
|
||||||
$autfilt -F- -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \
|
autfilt -F- -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \
|
||||||
--name='%M, %S states' --stats='<%m>, %e, %a' -n 10 > output
|
--name='%M, %S states' --stats='<%m>, %e, %a' -n 10 > output
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
<F(b | Ga), 3 states>, 5, 1
|
<F(b | Ga), 3 states>, 5, 1
|
||||||
|
|
@ -270,16 +266,16 @@ State: 9
|
||||||
--END--
|
--END--
|
||||||
EOF
|
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
|
diff output expected
|
||||||
|
|
||||||
|
|
||||||
cat <<EOF | $ltl2tgba -x degen-skip=1 -F- --ba -H > tmp.hoa
|
cat <<EOF | ltl2tgba -x degen-skip=1 -F- --ba -H > tmp.hoa
|
||||||
a U b
|
a U b
|
||||||
false
|
false
|
||||||
!b && Xb && GFa
|
!b && Xb && GFa
|
||||||
EOF
|
EOF
|
||||||
$autfilt <tmp.hoa --stats='"%M","%w"' > output
|
autfilt <tmp.hoa --stats='"%M","%w"' > output
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
"a U b","cycle{b}"
|
"a U b","cycle{b}"
|
||||||
"0",""
|
"0",""
|
||||||
|
|
@ -309,8 +305,8 @@ State: 3 "s3"
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
$autfilt -H input |
|
autfilt -H input |
|
||||||
SPOT_DOTDEFAULT=vcsn SPOT_DOTEXTRA='/* hello world */' $autfilt >output
|
SPOT_DOTDEFAULT=vcsn SPOT_DOTEXTRA='/* hello world */' autfilt >output
|
||||||
|
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
digraph G {
|
digraph G {
|
||||||
|
|
@ -341,10 +337,10 @@ EOF
|
||||||
|
|
||||||
diff output expected
|
diff output expected
|
||||||
|
|
||||||
test 1 = `$autfilt -H input --complete | $autfilt --is-complete --count`
|
test 1 = `autfilt -H input --complete | autfilt --is-complete --count`
|
||||||
|
|
||||||
|
|
||||||
$ltl2tgba --dot=a 'GFa & GFb' >output
|
ltl2tgba --dot=a 'GFa & GFb' >output
|
||||||
cat output
|
cat output
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
digraph G {
|
digraph G {
|
||||||
|
|
@ -363,7 +359,7 @@ digraph G {
|
||||||
EOF
|
EOF
|
||||||
diff output expected
|
diff output expected
|
||||||
|
|
||||||
$ltl2tgba --dot=ban 'GFa & GFb' >output
|
ltl2tgba --dot=ban 'GFa & GFb' >output
|
||||||
cat output
|
cat output
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
digraph G {
|
digraph G {
|
||||||
|
|
@ -383,7 +379,7 @@ EOF
|
||||||
diff output expected
|
diff output expected
|
||||||
|
|
||||||
|
|
||||||
SPOT_DOTDEFAULT=bra $ltl2tgba --dot='e.f(Lato)' 'GFa & GFb' >output
|
SPOT_DOTDEFAULT=bra ltl2tgba --dot='e.f(Lato)' 'GFa & GFb' >output
|
||||||
cat output
|
cat output
|
||||||
|
|
||||||
zero='<font color="#5DA5DA">⓿</font>'
|
zero='<font color="#5DA5DA">⓿</font>'
|
||||||
|
|
@ -510,7 +506,7 @@ digraph G {
|
||||||
}
|
}
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
$autfilt --dot=bao in >out
|
autfilt --dot=bao in >out
|
||||||
diff out expected
|
diff out expected
|
||||||
|
|
||||||
cat >expected2 <<EOF
|
cat >expected2 <<EOF
|
||||||
|
|
@ -535,7 +531,7 @@ EOF
|
||||||
|
|
||||||
# This should remove the state names, and automatically use circled
|
# This should remove the state names, and automatically use circled
|
||||||
# states.
|
# states.
|
||||||
$autfilt --dot=bao1 in | grep -v '>' >out
|
autfilt --dot=bao1 in | grep -v '>' >out
|
||||||
diff out expected2
|
diff out expected2
|
||||||
|
|
||||||
# Let's pretend that this is some used supplied input, as discussed in
|
# 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
|
# status here, because the actual error messages are tested in
|
||||||
# parseaut.test) and produce a valid output with the number of states
|
# parseaut.test) and produce a valid output with the number of states
|
||||||
# fixed, and the missing state definitions.
|
# fixed, and the missing state definitions.
|
||||||
$autfilt -H input >output1 && exit 1
|
autfilt -H input >output1 && exit 1
|
||||||
|
|
||||||
cat >expect1 <<EOF
|
cat >expect1 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
@ -605,13 +601,13 @@ EOF
|
||||||
|
|
||||||
diff output1 expect1
|
diff output1 expect1
|
||||||
# Make sure the output is valid.
|
# Make sure the output is valid.
|
||||||
$autfilt -H output1 > output1b
|
autfilt -H output1 > output1b
|
||||||
diff output1 output1b
|
diff output1 output1b
|
||||||
|
|
||||||
# Here is the scenario where the undefined states are actually states
|
# Here is the scenario where the undefined states are actually states
|
||||||
# we wanted to remove. So we tell autfilt to fix the automaton using
|
# we wanted to remove. So we tell autfilt to fix the automaton using
|
||||||
# --remove-dead-states
|
# --remove-dead-states
|
||||||
$autfilt -H --remove-dead input >output2 && exit 1
|
autfilt -H --remove-dead input >output2 && exit 1
|
||||||
|
|
||||||
cat >expect2 <<EOF
|
cat >expect2 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
@ -633,7 +629,7 @@ EOF
|
||||||
|
|
||||||
diff output2 expect2
|
diff output2 expect2
|
||||||
|
|
||||||
$autfilt -Hk expect2 >output2b
|
autfilt -Hk expect2 >output2b
|
||||||
|
|
||||||
cat >expect2b <<EOF
|
cat >expect2b <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
@ -679,8 +675,8 @@ State: 5
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
$autfilt -H --remove-unreach input >output3
|
autfilt -H --remove-unreach input >output3
|
||||||
$autfilt -H --remove-dead input >>output3
|
autfilt -H --remove-dead input >>output3
|
||||||
|
|
||||||
cat >expect3 <<EOF
|
cat >expect3 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
@ -720,7 +716,7 @@ EOF
|
||||||
diff output3 expect3
|
diff output3 expect3
|
||||||
|
|
||||||
|
|
||||||
$autfilt -Hz input 2>stderr && exit 1
|
autfilt -Hz input 2>stderr && exit 1
|
||||||
grep 'print_hoa.*z' stderr
|
grep 'print_hoa.*z' stderr
|
||||||
|
|
||||||
cat >input4 <<EOF
|
cat >input4 <<EOF
|
||||||
|
|
@ -736,13 +732,13 @@ State: 2 {0 1} [0] 2
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
test `$autfilt --is-weak -c input4` = 1
|
test `autfilt --is-weak -c input4` = 1
|
||||||
test `$autfilt --is-inherently-weak -c input4` = 1
|
test `autfilt --is-inherently-weak -c input4` = 1
|
||||||
test `$autfilt --is-terminal -c input4` = 0
|
test `autfilt --is-terminal -c input4` = 0
|
||||||
|
|
||||||
$autfilt -H --small --high input4 >output4
|
autfilt -H --small --high input4 >output4
|
||||||
$autfilt -H --small input4 >output4b
|
autfilt -H --small input4 >output4b
|
||||||
$autfilt -H --high input4 >output4c
|
autfilt -H --high input4 >output4c
|
||||||
cat output4
|
cat output4
|
||||||
|
|
||||||
cat >expect4<<EOF
|
cat >expect4<<EOF
|
||||||
|
|
@ -767,12 +763,12 @@ diff output4 expect4
|
||||||
diff output4b expect4
|
diff output4b expect4
|
||||||
diff output4c expect4
|
diff output4c expect4
|
||||||
|
|
||||||
$autfilt -Hv --small input4 >output5
|
autfilt -Hv --small input4 >output5
|
||||||
test `$autfilt --is-weak -c output4` = 1
|
test `autfilt --is-weak -c output4` = 1
|
||||||
test `$autfilt --is-terminal -c output4` = 0
|
test `autfilt --is-terminal -c output4` = 0
|
||||||
|
|
||||||
sed 's/\[0\]/[t]/g' expect4 > output4d
|
sed 's/\[0\]/[t]/g' expect4 > output4d
|
||||||
test `$autfilt --is-terminal -c output4d` = 1
|
test `autfilt --is-terminal -c output4d` = 1
|
||||||
|
|
||||||
|
|
||||||
cat >expect5<<EOF
|
cat >expect5<<EOF
|
||||||
|
|
@ -818,7 +814,7 @@ State: 2 {0}
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
run 0 $autfilt -Hk input6 >output6
|
run 0 autfilt -Hk input6 >output6
|
||||||
cat >expect6 <<EOF
|
cat >expect6 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 3
|
States: 3
|
||||||
|
|
@ -856,9 +852,9 @@ State: 1
|
||||||
[t] 1 {0 1}
|
[t] 1 {0 1}
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
test `$autfilt -c --is-inherently-weak input7` = 1
|
test `autfilt -c --is-inherently-weak input7` = 1
|
||||||
test `$autfilt -c --is-weak input7` = 0
|
test `autfilt -c --is-weak input7` = 0
|
||||||
$autfilt --check input7 -H >output7
|
autfilt --check input7 -H >output7
|
||||||
cat >expected7 <<EOF
|
cat >expected7 <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 3
|
States: 3
|
||||||
|
|
@ -895,5 +891,5 @@ State: 1
|
||||||
[t] 1 {0}
|
[t] 1 {0}
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
test `$autfilt -c --is-inherently-weak input8` = 0
|
test `autfilt -c --is-inherently-weak input8` = 0
|
||||||
test `$autfilt -c --is-weak input8` = 0
|
test `autfilt -c --is-weak input8` = 0
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue