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

FreeBSD Manual Pages

  
 
  

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

NAME
       ltl2tgta	- translate LTL/PSL formulas into Testing Automata

SYNOPSIS
       ltl2tgta	[OPTION...] [FORMULA...]

DESCRIPTION
       Translate linear-time formulas (LTL/PSL)	into Testing Automata.

       By  default it outputs a	transition-based generalized Testing Automaton
       the  smallest  Transition-based	Generalized  BA1/4chi	Automata,   in
       GraphViz's  format.   The input formula is assumed to be	stuttering-in-
       sensitive.

   Automaton type:
       --gta  Generalized Testing Automaton

       --ta   Testing Automaton

       --tgta Transition-based Generalized Testing Automaton (default)

   Input options:
       -f, --formula=STRING
	      process the formula STRING

       -F, --file=FILENAME[/COL]
	      process each line	of FILENAME as a formula; if COL is a positive
	      integer,	assume	a CSV file and read column COL;	use a negative
	      COL to drop the first line of the	CSV file

       --lbt-input
	      read all formulas	using LBT's prefix syntax

       --lenient
	      parenthesized blocks that	cannot be parsed  as  subformulas  are
	      considered as atomic properties

   Options for TA and GTA creation:
       --multiple-init
	      do not create the	fake initial state

       --single-pass
	      create a single-pass (G)TA without artificial livelock state

       --single-pass-lv
	      add an artificial	livelock state to obtain a single-pass (G)TA

   Output options:
       -8, --utf8
	      enable UTF-8 characters in output

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

       -D, --deterministic
	      prefer deterministic automata

       --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.

BIBLIOGRAPHY
       If you would like to give a reference to	this tool in  an  article,  we
       suggest you cite	the following paper:

       o      Ala  Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon:
	      Model checking using generalized testing automata.  Transactions
	      on  Petri	 Nets  and  Other  Models  of Concurrency (ToPNoC VI),
	      7400:94-112, 2012.

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

COPYRIGHT
       Copyright (C) 2020  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)

ltl2tgta (spot)	2.9.5		 November 2020			   LTL2TGTA(1)
NAME | SYNOPSIS | DESCRIPTION | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO

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

home | help