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, --buchi, --Buchi
	      automaton	with BA1/4chi acceptance

       -B, --sba, --ba
	      state-based BA1/4chi Automaton (same as -S -b)

       --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, --gba
	      automaton	with Generalized BA1/4chi acceptance (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|i(ID)|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, (i) or (i(GRAPHID))
	      add IDs, (k) use state labels 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 transi-
	      tion-based acceptance, (u) hide true states, (v)	vertical  lay-
	      out,  (y)	 split universal edges by color, (+INT)	add INT	to all
	      set numbers, (<INT) display at most INT states, (#) show	inter-
	      nal 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)  2022   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.10.4	 February 2022			 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.1-RELEASE+and+Ports>

home | help