bin: overhaul default input selection
If no input have been specified, and the standard input is not a tty all tools now default to reading it. If standard input is a tty, all tools display an error message. Additionally, - is now a shorthand for -F- in all tools. * NEWS: Summarize this. * bin/common_finput.cc, bin/common_finput.hh (check_no_formulas, check_no_automaton): New functions that implement the above istty() logic. * bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlgrind.cc: Use these function, and recognize '-' if it was not the case. * tests/core/acc_word.test, tests/core/ltldo.test, tests/core/minusx.test, tests/core/readsave.test, tests/core/unambig.test: Adjust some tests to exercise this. * doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/oaut.org: Adjust the documentation and simplify some examples.
This commit is contained in:
Alexandre Duret-Lutz
parent
abff7eba8e
commit
dd6875d5fe
22 changed files with 119 additions and 54 deletions
|
|
@ -739,7 +739,7 @@ of the form =cycle{b}=, and display the associated formula (which was
|
|||
stored as the name of the automaton by =ltl2tgba=).
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- |
|
||||
randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba |
|
||||
autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \
|
||||
--reject-word='cycle{b}' --stats=%M -n 10
|
||||
#+END_SRC
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ formulas, and show the resulting number of states (=%s=) and edges
|
|||
(=%e=) of the automaton constructed for each formula.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
genltl --and-gf=1..5 --u-left=1..5 | ltl2tgba -F- --stats '%f,%s,%e'
|
||||
genltl --and-gf=1..5 --u-left=1..5 | ltl2tgba --stats '%f,%s,%e'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
|
|
|
|||
|
|
@ -421,9 +421,9 @@ For instance here is a complex command that will
|
|||
1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]],
|
||||
2. use [[file:ltlfilt.org][=ltlfilt=]] to rewrite the W and M operators away (=--remove-wm=),
|
||||
simplify the formulas (=-r=), remove duplicates (=u=) as well as
|
||||
formulas that have a size less then 3 (=--size-min=3=),
|
||||
3. use =head= to keep only 10 of such formula
|
||||
4. loop to process each of these formula:
|
||||
formulas that have a size less then 3 (=--size-min=3=), and
|
||||
keep only the 10 first formulas (=-n 10=)
|
||||
3. loop to process each of these formula:
|
||||
- print it
|
||||
- then convert the formula into =ltl2dstar='s input format, process
|
||||
it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA
|
||||
|
|
@ -438,8 +438,7 @@ deterministic, and =%p= whether the automaton is complete.
|
|||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
randltl -n -1 --tree-size=10..14 a b c |
|
||||
ltlfilt --remove-wm -r -u --size-min=3 |
|
||||
head -n 10 |
|
||||
ltlfilt --remove-wm -r -u --size-min=3 -n 10 |
|
||||
while read f; do
|
||||
echo "$f"
|
||||
ltlfilt -l -f "$f" |
|
||||
|
|
|
|||
|
|
@ -835,7 +835,7 @@ For instance we can study the size of the automata generated for the
|
|||
right-nested =U= formulas as follows:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
genltl --u-right=1..8 | ltl2tgba -F - --stats '%s states and %e edges for "%f"'
|
||||
genltl --u-right=1..8 | ltl2tgba --stats '%s states and %e edges for "%f"'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: 2 states and 2 edges for "p1"
|
||||
|
|
@ -847,7 +847,11 @@ genltl --u-right=1..8 | ltl2tgba -F - --stats '%s states and %e edges for "%f"'
|
|||
: 7 states and 28 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U p7)))))"
|
||||
: 8 states and 36 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U (p7 U p8))))))"
|
||||
|
||||
Here =-F -= means that formulas should be read from the standard input.
|
||||
Note that because no formula have been passed as argument to
|
||||
=ltl2tgba=, it defaulted to reading them from standard input. Such a
|
||||
behaviour can be requested explicitly with =-F -= if needed (e.g., to
|
||||
read from standard input in addition to processing other formula
|
||||
supplied with =-f=).
|
||||
|
||||
When computing the size of an automaton, we distinguish /transitions/
|
||||
and /edges/. An edge between two states is labeled by a Boolean
|
||||
|
|
|
|||
|
|
@ -44,8 +44,9 @@ The core of =ltlcross= is a loop that does the following steps:
|
|||
|
||||
* Formula selection
|
||||
|
||||
Formulas to translate should be specified using the [[file:ioltl.org][common input options]].
|
||||
Standard input is read if no =-f= or =-F= option is given.
|
||||
Formulas to translate should be specified using the [[file:ioltl.org][common input
|
||||
options]]. Standard input is read if it is not connected to a terminal,
|
||||
and no =-f= or =-F= options are given.
|
||||
|
||||
* Configuring translators
|
||||
|
||||
|
|
|
|||
|
|
@ -15,8 +15,9 @@ formulas.) It can be used to perform a number of tasks. Essentially:
|
|||
Because it read and write formulas, =ltlfilt= accepts
|
||||
all the [[file:ioltl.org][common input and output options]].
|
||||
|
||||
Additionally, if no =-f= or =-F= option is specified, =ltlfilt=
|
||||
will read formulas from the standard input.
|
||||
Additionally, if no =-f= or =-F= option is specified, and =ltlfilt=
|
||||
will read formulas from the standard input if it is not connected to a
|
||||
terminal.
|
||||
|
||||
For instance the following will convert two LTL formulas expressed
|
||||
using infix notation (with different names supported for the same
|
||||
|
|
|
|||
|
|
@ -1015,18 +1015,18 @@ using =autfilt -n5=.
|
|||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
randltl -n -1 a b |
|
||||
ltl2tgba -F- |
|
||||
ltl2tgba |
|
||||
autfilt --states=3 --stats='!(%M)' |
|
||||
ltl2tgba -F- |
|
||||
ltl2tgba |
|
||||
autfilt --states=3 --stats=%M -n5
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: G(F!a & XF(a | G!b))
|
||||
: GFb | G(!b & FG!b)
|
||||
: !a & F((a | b) & (!a | !b))
|
||||
: !a | (b R a)
|
||||
: !b & X(!b U a)
|
||||
: G(b | F(b & Fa))
|
||||
: (!a | b | (!b & (b W Ga))) & (a | (!b & (b | (!b M F!a))))
|
||||
: (!a | (!a R b)) & (a | (a U !b))
|
||||
: !a & F((!a | FG!a) & (a | GFa))
|
||||
: X(!b W a)
|
||||
|
||||
Note that the above result can also be obtained without using
|
||||
=autfilt= and automata names. We can use the fact that =ltl2tgba
|
||||
|
|
@ -1045,13 +1045,15 @@ head -n5 | cut -d, -f2 # return the five first formulas
|
|||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: G(F!a & XF(a | G!b))
|
||||
: GFb | G(!b & FG!b)
|
||||
: !a & F((!a | !b) & (a | b))
|
||||
: !a | (b R a)
|
||||
: !b & X(!b U a)
|
||||
|
||||
: G(b | F(b & Fa))
|
||||
: (!a | b | (!b & (b W Ga))) & (a | (!b & (b | (!b M F!a))))
|
||||
: (!a | (!a R b)) & (a | (a U !b))
|
||||
: !a & F((!a | FG!a) & (a | GFa))
|
||||
: X(!b W a)
|
||||
|
||||
Note that the =-F-= argument in the first call to =ltl2tgba= is
|
||||
superfluous as the tool default to reading from its standard input.
|
||||
But we put it there for symmetry with the second call.
|
||||
|
||||
# LocalWords: num toc html syntaxes ltl tgba sed utf UTF lbtt SCCs
|
||||
# LocalWords: GraphViz's hoaf HOA LBTT's neverclaim ba SPOT's Gb cn
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue