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

FreeBSD Manual Pages


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

       autfilt - filter, convert, and transform	omega-automata

       autfilt [OPTION...] [FILENAME[/COL]...]

       Convert,	transform, and filter omega-automata.

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

	      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 (with state-based acceptance)

       --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 is	allowed	(default)

       -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

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

       -c, --count
	      print only a count of matched automata

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

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

       -n, --max-count=NUM
	      output at	most NUM automata

	      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

   Filtering options:
       --acc-sccs=RANGE, --accepting-sccs=RANGE
	      keep automata whose number of non-trivial	accepting SCCs	is  in

	      keep automata whose number of acceptance sets is in RANGE

	      keep automata that accept	WORD

	      match automata with given	acceptance condition

	      match  automata  with a number of	(declared) atomic propositions
	      in RANGE

	      keep automata that are isomorphic	to the automaton in FILENAME

	      keep automata whose number of edges is in	RANGE

	      keep automata that are equivalent	(language-wise)	to the automa-
	      ton in FILENAME

	      keep automata that use existential branching (i.e., make non-de-
	      terministic choices)

	      keep alternating automata	that use universal branching

       --included-in=FILENAME keep automata whose languages  are  included  in
	      of the automaton from FILENAME

	      keep  automata whose number of accepting inherently-weak SCCs is
	      in RANGE.	 An accepting SCC is inherently	weak if	 it  does  not
	      have a rejecting cycle.

	      keep  automata  whose  languages	have an	non-empty intersection
	      with the automaton from FILENAME

	      keep only	automata using universal branching

	      keep colored automata (i.e., exactly  one	 acceptance  mark  per
	      transition or state)

	      keep complete automata

	      keep deterministic automata

	      keep automata with an empty language

	      keep only	inherently weak	automata

	      keep semi-deterministic automata

       --is-stutter-invariant keep automata representing stutter-invariant

	      keep only	terminal automata

	      keep only	unambiguous automata

	      keep only	very-weak automata

	      keep only	weak automata

	      keep  automata  whose  number  of	 nondeterministic states is in

       -N, --nth=RANGE
	      assuming input automata are numbered from	1, keep	only those  in

       --rej-sccs=RANGE, --rejecting-sccs=RANGE
	      keep  automata  whose number of non-trivial rejecting SCCs is in

	      keep automata that reject	WORD

	      keep automata whose number of SCCs is in RANGE

	      keep automata whose number of states is in RANGE

	      keep automata whose number of  accepting	terminal  SCCs	is  in
	      RANGE.  Terminal SCCs are	weak and complete.

       --triv-sccs=RANGE, --trivial-sccs=RANGE
	      keep automata whose number of trivial SCCs is in RANGE

	      match  automata  with  a	number	of declared, but unused	atomic
	      propositions in RANGE

	      match automata with a number  of	used  atomic  propositions  in

       -u, --unique
	      do  not  output the same automaton twice (same in	the sense that
	      they are isomorphic)

       -v, --invert-match
	      select non-matching automata

	      keep automata whose number of accepting weak SCCs	is  in	RANGE.
	      In  a  weak  SCC,	 all transitions belong	to the same acceptance

       RANGE may have one of the following forms: 'INT', 'INT..INT',  '..INT',
       or 'INT..'

       WORD  is	 lasso-shaped  and  written as 'BF;BF;...;BF;cycle{BF;...;BF}'
       where BF	are arbitrary Boolean  formulas.   The	'cycle{...}'  part  is
       mandatory, but the prefix can be	omitted.

	      remove unused acceptance sets from the automaton

	      put the acceptance condition in Conjunctive Normal Form

	      complement each automaton	(different strategies are used)

	      complement the acceptance	condition (without touching the	autom-

       --decompose-scc=t|w|s|N|aN, --decompose-strength=t|w|s|N|aN
	      extract the (t) terminal,	(w) weak, or (s) strong	part of	an au-
	      tomaton  or (N) the subautomaton leading to the Nth SCC, or (aN)
	      to the Nth accepting SCC (option can be combined with commas  to
	      extract multiple parts)

	      allow less stuttering

	      put the acceptance condition in Disjunctive Normal Form

	      dualize each automaton

	      if  any  of those	APs occur in the automaton, restrict all edges
	      to ensure	two of them may	not be true at	the  same  time.   Use
	      this  option multiple times to declare independent groups	of ex-
	      clusive propositions.

       --generalized-rabin[=unique-inf|share-inf],	    --gra[=unique-inf|
	      rewrite  the  acceptance condition as generalized	Rabin; the de-
	      fault "unique-inf" option	uses the generalized Rabin  definition
	      from  the	 HOA  format; the "share-inf" option allows clauses to
	      share Inf	sets, therefore	reducing the number of sets

       --generalized-streett[=unique-fin|share-fin],	    --gsa[=unique-fin|
	      rewrite  the  acceptance	condition  as generalized Streett; the
	      "share-fin" option allows	clauses	to share Fin  sets,  therefore
	      reducing the number of sets; the default "unique-fin" does not

	      allow more stuttering (two possible algorithms)

	      only  keep  specified  states.   The first state will be the new
	      initial state.  Implies --remove-unreachable-states.

	      remove all transitions in	specified acceptance sets

	      merge transitions	with same destination and acceptance

	      Degeneralize automata according to sets NUM1,NUM2,... If no sets
	      are  given,  partial  degeneralization is	performed for all con-
	      junctions	of Inf and disjunctions	of Fin.

       --product=FILENAME, --product-and=FILENAME
	      build the	product	with the automaton in  FILENAME	 to  intersect

	      build  the  product  with	 the automaton in FILENAME to sum lan-

	      randomize	states and transitions (specify	's' or 't' to  random-
	      ize only states or transitions)

	      remove atomic propositions either	by existential quantification,
	      or by assigning them 0 or	1

	      remove states that are unreachable, or that cannot belong	to  an
	      infinite path

	      rewrite the automaton without using Fin acceptance

	      remove states that are unreachable from the initial state

	      remove declared atomic propositions that are not used

	      minimize the automaton using a SAT solver	(only works for	deter-
	      ministic automata). Supported options are	acc=STRING,  states=N,
	      max-states=N,    sat-incr=N,    sat-incr-steps=N,	  sat-langmap,
	      sat-naive, colored, preproc=N. Spot uses by default its  PicoSAT
	      distribution  but	an external SATsolver can be set thanks	to the
	      SPOT_SATSOLVER environment variable(see spot-x).

	      if both Inf(x) and Fin(x)	appear in  the	acceptance  condition,
	      replace Fin(x) by	a new Fin(y) and adjust	the automaton

	      simplify	the  acceptance	 condition by merging identical	accep-
	      tance sets and by	simplifying some terms	containing  complemen-
	      tary sets

	      if  --exclusive-ap  is used, assume those	AP groups are actually
	      exclusive	in the system to simplify the expression of transition
	      labels (implies --merge-transitions)

	      split  edges  into  transitions  labeled	by conjunctions	of all
	      atomic propositions, so they can be read as letters

	      convert to an automaton with Streett-like	acceptance. Works only
	      with acceptance condition	in DNF

	      remove the acceptance condition and all acceptance sets

       --sum=FILENAME, --sum-or=FILENAME
	      build the	sum with the automaton in FILENAME to sum languages

	      build  the  sum with the automaton in FILENAME to	intersect lan-

   Decorations (for -d and -H1.1 output):
	      highlight	one accepting run using	color NUM

	      highlight	states that recognize identical	languages

	      highlight	nondeterministic states	and edges with color NUM

	      highlight	nondeterministic edges with color NUM

	      highlight	nondeterministic states	with color NUM

	      highlight	one run	matching WORD using color NUM

   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)

	      prefer small automata

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

       --low  minimal optimizations (fast)

	      moderate optimizations

       If  any	option among --small, --deterministic, or --any	is given, then
       the simplification level	defaults to --high unless specified otherwise.
       If  any option among --low, --medium, or	--high is given, then the sim-
       plification goal	defaults to --small unless  specified  otherwise.   If
       none  of	 those	options	 are  specified, then autfilt acts as is --any
       --low were given: these actually	disable	the simplification routines.

   Miscellaneous options:
	      seed for the random number generator (0)

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

       --help print this help

	      print program version

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

   Exit	status:
       0      if some automata were output

       1      if no automata were output (no match)

       2      if any error has been reported

	      By  default,  SAT-based  minimization  executes a	binary search,
	      checking N/2 etc.	 The upper bound being	N  (the	 size  of  the
	      starting	automaton),  the  lower	 bound is always 1 except when
	      sat-langmap option is used.

	      DOUBLEQUOTEDSTRING is an acceptance formula in the  HOA  syntax,
	      or  a  parametrized acceptance name (the different acc-name: op-
	      tions from HOA).

	      force all	transitions (or	all states if -S is used) to belong to
	      exactly one acceptance condition.

	      M	 is an upper-bound on the maximum number of states of the con-
	      structed automaton.

	      use an incremental approach  for	SAT-based  minimization	 algo-
	      rithm.  M	 can be	either 1 or 2. They correspond respectively to
	      -x sat-minimize=2	and -x sat-minimize=3  options.	 They  restart
	      the  encoding  only  after (N-1)-sat-incr-steps states have been
	      won.  Each iterations of both starts by encoding the research of
	      an  N-1 automaton, N being the size of the starting automaton. 1
	      uses Picosat assumptions.	 It additionally assumes that the last
	      sat-incr-steps  states are unnecessary. On failure, it relax the
	      assumptions to do	a binary search	 between  N-1  and  (N-1)-sat-
	      incr-steps. sat-incr-steps defaults to 6.	2, as for it, after an
	      N-1 state	automaton has been found, uses incremental solving for
	      the next sat-incr-steps iterations by forbidding the usage of an
	      additional state without reencoding the problem  again.  A  full
	      encoding	 occurs	  after	  sat-incr-steps   iterations	unless
	      sat-incr-steps=-1	(see SPOT_XCNF environment variable  described
	      in spot-x). It defaults to 2.

	      set  the	value of sat-incr-steps	to M. This is used by sat-incr

	      use the naive algorithm to find a	smaller	automaton.  It	starts
	      from  N  (N  being  the size of the starting automaton) and then
	      checks N-1, N-2, etc. until the last successful check.

	      Find the lower bound of default sat-minimize procedure (1). This
	      relies  on the fact that the size	of the minimal automaton is at
	      least equal to the total number of  different  languages	recog-
	      nized by the automaton's states.

	      M	 is  a	fixed  number  of states to use	in the result (all the
	      states needs not be accessible in	 the  result.  Therefore,  the
	      output might be smaller nonetheless). The	SAT-based procedure is
	      just used	once to	synthesize one automaton, and no further mini-
	      mization is attempted.

       The  following papers are related to some of the	transformations	imple-
       mented in autfilt.

       o      Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis
	      Poitrenaud:   Strength-based   decomposition   of	 the  property
	      BA1/4chi automaton for faster  model  checking.  Proceedings  of
	      TACAS'13.	LNCS 7795.

	      The --strength-decompose option implements the definitions given
	      in the above paper.

       o      FrantiA!ek Blahoudek, Alexandre Duret-Lutz, VojtAech Rujbr,  and
	      Jan  StrejAek:  On  refinement of	BA1/4chi automata for explicit
	      model checking.  Proceedings of SPIN'15.	LNCS 9232.

	      That paper gives the motivation for options  --exclusive-ap  and

       o      Thibaud  Michaud and Alexandre Duret-Lutz: Practical stutter-in-
	      variance	checks	for  I-regular	languages.    Proceedings   of
	      SPIN'15.	LNCS 9232.

	      Describes	 the  algorithms used by the --destut and --instut op-
	      tions.  These options correpond respectively to cl() and sl() in
	      the paper.

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

	      Describes	the --sat-minimize option.

       Report bugs to <>.

       Copyright  (C)  2020   Laboratoire  de Recherche	et DA(C)veloppement de
       l'Epita.	   License   GPLv3+:   GNU   GPL   version    3	   or	 later
       This  is	 free  software:  you  are free	to change and redistribute it.
       There is	NO WARRANTY, to	the extent permitted by	law.

       spot-x(7) dstar2tgba(1)

autfilt	(spot) 2.9.5		 November 2020			    AUTFILT(1)


Want to link to this manual page? Use this URL:

home | help