Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
DSTAR2TGBA(1)			 User Commands			 DSTAR2TGBA(1)

NAME
       dstar2tgba - convert automata into BA1/4chi automata

SYNOPSIS
       dstar2tgba [OPTION...] [FILENAME[/COL]...]

DESCRIPTION
       Convert	automata  with	any  acceptance	 condition  into  variants  of
       BA1/4chi	automata.

       This reads automata into	any supported format  (HOA,  LBTT,  ltl2dstar,
       never claim) and	outputs	a Transition-based Generalized BA1/4chi	Autom-
       ata in GraphViz's format	by default.  Each supplied  file  may  contain
       multiple	automata.

   Input:
       -F, --file=FILENAME
	      process the automaton in FILENAME

       --trust-hoa=BOOL
	      If  false,  properties  listed  in HOA files are ignored,	unless
	      they can be easily verified.  If true  (the  default)  any  sup-
	      ported property is trusted.

   Output automaton type:
       -B, --ba
	      BA1/4chi Automaton (implies -S)

       --cobuchi, --coBuchi
	      automaton	with co-BA1/4chi acceptance (will recognize a superset
	      of the input language if not co-BA1/4chi realizable)

       -C, --complete
	      output a complete	automaton

       -G, --generic
	      any acceptance condition is allowed

       -M, --monitor
	      Monitor (accepts all finite prefixes of the given	property)

       -p, --colored-parity[=any|min|max|odd|even|min odd|min even|max odd|max

       even]  colored automaton	with parity acceptance

       -P, --parity[=any|min|max|odd|even|min odd|min even|max odd|max even]
	      automaton	with parity acceptance

       -S, --state-based-acceptance, --sbacc
	      define the acceptance using states

       --tgba Transition-based Generalized BA1/4chi Automaton (default)

   Output format:
       -8, --utf8
	      enable UTF-8  characters	in  output  (ignored  with  --lbtt  or
	      --spin)

       --check[=PROP]
	      test  for	 the additional	property PROP and output the result in
	      the HOA format (implies -H).  PROP may be	some prefix  of	 'all'
	      (default),  'unambiguous',  'stutter-invariant', 'stutter-sensi-
	      tive-example', 'semi-determinism', or 'strength'.

       -d,  --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|
       +INT|_INT|#]
	      GraphViz's  format.   Add	letters	for (1)	force numbered states,
	      (a) show acceptance condition  (default),	 (A)  hide  acceptance
	      condition,  (b)  acceptance  sets	as bullets, (B)	bullets	except
	      for BA1/4chi/co-BA1/4chi automata, (c) force circular nodes, (C)
	      color  nodes  with COLOR,	(d) show origins when known, (e) force
	      elliptic nodes, (E) force	rEctangular nodes, (f(FONT)) use FONT,
	      (g)  hide	 edge labels, (h) horizontal layout, (k) use state la-
	      bels when	possible, (K) use  transition  labels  (default),  (n)
	      show  name,  (N) hide name, (o) ordered transitions, (r) rainbow
	      colors  for  acceptance  sets,  (R)  color  acceptance  sets  by
	      Inf/Fin,	(s)  with SCCs,	(t) force transition-based acceptance,
	      (u) hide true states, (v)	vertical layout, (y)  split  universal
	      edges  by	 color,	(+INT) add INT to all set numbers, (<INT) dis-
	      play at most INT states, (#) show	internal edge numbers

       -H, --hoaf[=1.1|i|k|l|m|s|t|v]
	      Output the automaton in HOA format (default).   Add  letters  to
	      select  (1.1) version 1.1	of the format, (i) use implicit	labels
	      for complete deterministic automata, (s) prefer state-based  ac-
	      ceptance when possible [default],	(t) force transition-based ac-
	      ceptance,	(m) mix	state and transition-based acceptance, (k) use
	      state  labels when possible, (l) single-line output, (v) verbose
	      properties

       --lbtt[=t]
	      LBTT's format (add =t to force transition-based acceptance  even
	      on BA1/4chi automata)

       --name=FORMAT
	      set the name of the output automaton

       -o, --output=FORMAT
	      send  output  to a file named FORMAT instead of standard output.
	      The first	automaton sent to a file truncates  it	unless	FORMAT
	      starts with '>>'.

       -q, --quiet
	      suppress all normal output

       -s, --spin[=6|c]
	      Spin  neverclaim	(implies  --ba).   Add	letters	 to select (6)
	      Spin's 6.2.4 style, (c) comments on states

       --stats=FORMAT, --format=FORMAT
	      output statistics	about the automaton

       Any FORMAT string may use the following interpreted sequences (capitals
       for input, minuscules for output):

       %%     a	single %

       %<     the  part	 of  the  line before the automaton if it comes	from a
	      column extracted from a CSV file

       %>     the part of the line after the automaton if it comes from	a col-
	      umn extracted from a CSV file

       %A, %a number of	acceptance sets

       %C, %c, %[LETTERS]C, %[LETTERS]c
	      number  of SCCs; you may filter the SCCs to count	using the fol-
	      lowing LETTERS, possibly concatenated: (a)  accepting,  (r)  re-
	      jecting, (c) complete, (v) trivial, (t) terminal,	(w) weak, (iw)
	      inherently weak. Use uppercase letters to	negate them.

       %D, %d 1	if the automaton is deterministic, 0 otherwise

       %E, %e number of	reachable edges

       %F     name of the input	file

       %G, %g, %[LETTERS]G, %[LETTERS]g
	      acceptance condition (in HOA syntax); add	brackets to  print  an
	      acceptance  name instead and LETTERS to tweak the	format:	(0) no
	      parameters, (a) accentuated, (b) abbreviated, (d)	style used  in
	      dot   output,   (g)  no  generalized  parameter,	(l)  recognize
	      Street-like and Rabin-like, (m) no main parameter, (p) no	parity
	      parameter, (o) name unknown acceptance as	'other', (s) shorthand
	      for 'lo0'.

       %H, %h the automaton in HOA format on a single  line  (use  %[opt]H  or
	      %[opt]h to specify additional options as in --hoa=opt)

       %L     location in the input file

       %M, %m name of the automaton

       %N, %n number of	nondeterministic states

       %P, %p 1	if the automaton is complete, 0	otherwise

       %r     wall-clock time elapsed in seconds (excluding parsing)

       %R, %[LETTERS]R
	      CPU  time	 (excluding  parsing),	in seconds; Add	LETTERS	to re-
	      strict to(u) user	time, (s) system time, (p) parent process,  or
	      (c) children processes.

       %S, %s number of	reachable states

       %T, %t number of	reachable transitions

       %U, %u, %[LETTER]U, %[LETTER]u
	      1	if the automaton contains some universal

       branching (or a number of [s]tates or [e]dges with
	      universal	branching)

       %W, %w one word accepted	by the automaton

       %X, %x, %[LETTERS]X, %[LETTERS]x
	      number  of  atomic  propositions declared	in the automaton;  add
	      LETTERS to list atomic propositions with (n) no quoting, (s) oc-
	      casional	double-quotes  with  C-style escape, (d) double-quotes
	      with C-style escape, (c) double-quotes  with  CSV-style  escape,
	      (p)  between  parentheses,  any extra non-alphanumeric character
	      will be used to separate propositions

   Simplification goal:
       -a, --any
	      no preference, do	not bother making it small or deterministic

       -D, --deterministic
	      prefer deterministic automata (combine with --generic to be sure
	      to obtain	a deterministic	automaton)

       --small
	      prefer small automata (default)

   Simplification level:
       --high all available optimizations (slow, default)

       --low  minimal optimizations (fast)

       --medium
	      moderate optimizations

   Miscellaneous options:
       -x, --extra-options=OPTS
	      fine-tuning options (see spot-x (7))

       --help print this help

       --version
	      print program version

       Mandatory  or  optional arguments to long options are also mandatory or
       optional	for any	corresponding short options.

HISTORY
       dstar2tgba was introduced in Spot 1.2 as	a command that reads  automata
       in  ltl2dstar's	format,	 and converts them into	TGBA.  At this time it
       was the only command-line tool being able to read automata.

       In Spot 1.99.1 the autfilt command was introduced, but could only  read
       automata	 in  the  HOA format, or in lbtt's format, or as never claims.
       So dstar2tgba was still the only	way to process automata	in ltl2dstar's
       format.

       In  Spot	 1.99.4	 the  parser for ltl2dstar's format was	finally	merged
       with the	parser used by autfilt for reading the other format.  This im-
       plies  not  only	that autfilt can now read ltl2dstar's format, but also
       that dstar2tgba can read	the other formats as well.

       Nowadays, the command

	   % dstar2tgba	some files

       can be used as a	shorthand for

	   % autfilt --tgba --high --small some	files

       The name	dstar2tgba is kept for backward	compatibility and  because  it
       is  used	in at least one	published paper, but naming this tool aut2tgba
       would make more sense.

BIBLIOGRAPHY
       1.     The					       ltl2dstarmanual
	      <http://www.ltl2dstar.de/docs/ltl2dstar.html>.

	      Documents	the output format of ltl2dstar.

       2.     Chistof  LA<paragraph>ding:  Mehods  for	the  Transformation of
	      I-Automata: Complexity and Connection  to	 Second	 Order	Logic.
	      Diploma Thesis.  University of Kiel. 1998.

	      Describes	 various  tranformations  from non-deterministic Rabin
	      and Streett automata to BA1/4chi automata.   Slightly  optimized
	      variants of these	transformations	are used by dstar2tgba for the
	      general cases.

       3.     Sriram C.	Krishnan, Anuj Puri, and Robert	K. Brayton:  Determin-
	      istic  I-automata	 vis-a-vis  Deterministic  BA1/4chi  Automata.
	      ISAAC'94.

	      Explains how to preserve the determinism of  Rabin  and  Streett
	      automata	when  the  property can	be repreted by a Deterministic
	      automaton.  dstar2tgba implements	this for the Rabin case	 only.
	      In other words, translating a deterministic Rabin	automaton with
	      dstar2tgba will produce a	deterministic TGBA or BA if such a au-
	      tomaton exists.

       4.     Souheib  Baarir  and Alexandre Duret-Lutz: Mechanizing the mini-
	      mization of deterministic	generalized BA1/4chi  automata.	  Pro-
	      ceedings of FORTE'14.  LNCS 8461.

	      Explains	the SAT-based minimization techniques that can be used
	      (on  request  only)  by  dstar2tgba  to  minimize	 deterministic
	      BA1/4chi automata.

       5.     Souheib  Baarir and Alexandre Duret-Lutz:	SAT-based minimization
	      of deterministic	I-automata.   Proceedings  of  LPAR'15	(a.k.a
	      LPAR-20).	 LNCS 9450.

	      Extends the previous paper by allowing arbitrary acceptance con-
	      ditions.

REPORTING BUGS
       Report bugs to <spot@lrde.epita.fr>.

COPYRIGHT
       Copyright (C) 2021  Laboratoire de  Recherche  et  DA(C)veloppement  de
       l'Epita.	    License    GPLv3+:	  GNU	GPL   version	3   or	 later
       <http://gnu.org/licenses/gpl.html>.
       This is free software: you are free  to	change	and  redistribute  it.
       There is	NO WARRANTY, to	the extent permitted by	law.

SEE ALSO
       spot-x(7), autfilt(1)

dstar2tgba (spot) 2.9.7		   May 2021			 DSTAR2TGBA(1)

NAME | SYNOPSIS | DESCRIPTION | HISTORY | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=dstar2tgba&sektion=1&manpath=FreeBSD+13.0-RELEASE+and+Ports>

home | help