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

FreeBSD Manual Pages

  
 
  

home | help
SPOT-X(7)			 User Commands			     SPOT-X(7)

NAME
       spot-x -	Common fine-tuning options and environment variables.

SYNOPSIS
       --extra-options STRING
       -x STRING

DESCRIPTION
       Common fine-tuning options for binaries built with Spot.

       The  argument  of  -x  or  --extra-options is a comma-separated list of
       KEY=INT assignments that	are passed  to	the  post-processing  routines
       (they  may  be passed to	other algorithms in the	future). These options
       are mostly used for benchmarking	and debugging purpose.	KEYR  (without
       any  value)  is	a  shorthand  for KEY=1, while !KEY is a shorthand for
       KEY=0.

   Temporal logic simplification options:
       tls-impl
	      Control usage of implication-based rewriting. (0)	 disables  it,
	      (1) enables rules	based on syntactic implications, (2) addition-
	      ally allows automata-based implication checks, (3) enables  more
	      rules  based  on automata-based implication checks.  The default
	      value depends on the --low, --medium, or --high settings.

   Translation options:
       comp-susp
	      Set to 1 to enable compositional suspension, as described	in our
	      SPIN'13 paper (see Bibliography below).  Set to 2, to build only
	      the skeleton TGBA	without	composing it.  Set to 0	(the  default)
	      to disable.

       early-susp
	      When set to 1, start compositional suspension on the transitions
	      that enter accepting SCCs, and not only on the  transitions  in-
	      side  accepting  SCCs.   This  option defaults to	0, and is only
	      used when	comp-susp=1.

       ltl-split
	      Set to 0 to disable the translation of automata  as  product  or
	      sum of subformulas.

       skel-simul
	      Default  to  1.	Set to 0 to disable simulation on the skeleton
	      automaton	 during	 compositional	suspension.  Only  used	  when
	      comp-susp=1.

       skel-wdba
	      Set  to 0	to disable WDBA	minimization on	the skeleton automaton
	      during compositional suspension. Set to 1	 always	 WDBA-minimize
	      the  skeleton .  Set to 2	to keep	the WDBA only if it is smaller
	      than the original	skeleton.   This  option  is  only  used  when
	      comp-susp=1  and	default	to 1 or	2 depending on whether --small
	      or --deterministic is specified.

   Postprocessing options:
       ba-simul
	      Set to 0 to  disable  simulation-based  reductions  on  automata
	      where  state-based acceptance must be preserved (e.g., after de-
	      generalization has been performed).   The	name suggests this ap-
	      plies  only  to BA1/4chi automata	for historical reasons;	it re-
	      ally applies to any state-based acceptance nowadays. Set to 1 to
	      use  only	direct simulation.  Set	to 2 to	use only reverse simu-
	      lation.  Set to 3	to iterate both	 direct	 and  reverse  simula-
	      tions.  The default is 3 in --high mode, and 0 otherwise.

       degen-lcache
	      If  non-zero  (the  default is 1), whenever the degeneralization
	      algorithm	enters an SCC on a state that has already been associ-
	      ated to a	level elsewhere, it should reuse that level. Different
	      values can be used to select which level to reuse: 1 always uses
	      the  first  level	created, 2 uses	the minimum level seen so far,
	      and 3 uses the maximum level seen	so far.	 The  "lcache"	stands
	      for "level cache".

       degen-lowinit
	      Whenever	the  degeneralization  algorihm	 enters	 a new SCC (or
	      starts from the initial state), it starts	on some	level  L  that
	      is  compatible  with all outgoing	transitions.  If degen-lowinit
	      is zero (the default) and	the corresponding state	(in the	gener-
	      alized  automaton)  has  an accepting self-loop, then level L is
	      replaced by the accepting	level, as it might favor  finding  ac-
	      cepting  cycles  earlier.	  If  degen-lowinit  is	non-zero, then
	      level L is always	used without looking for the  presence	of  an
	      accepting	self-loop.

       degen-lskip
	      If  non-zero  (the default), the degeneralization	algorithm will
	      skip as much levels as possible for each	transition.   This  is
	      enabled by default as it very often reduce the number of result-
	      ing states.  A consequence of skipping levels is that the	degen-
	      eralized	automaton  tends to have smaller cycles	around the ac-
	      cepting states.  Disabling skipping will produce	automata  with
	      large cycles, and	often with more	states.

       degen-order
	      If  non-zero, the	degeneralization algorithm will	compute	an in-
	      dependent	degeneralization order	for  each  SCC	it  processes.
	      This is currently	disabled by default.

       degen-remscc
	      If  non-zero (the	default), make sure the	output of the degenal-
	      ization has as many SCCs as the input, by	 removing  superfluous
	      ones.

       degen-reset
	      If  non-zero  (the default), the degeneralization	algorithm will
	      reset its	level any time it exits	an SCC.

       det-max-edges
	      When defined to a	positive integer N, determinizations  will  be
	      aborted  whenever	 the number of generated edges would exceed N.
	      In this case a non-deterministic automaton will be returned.

       det-max-states
	      When defined to a	positive integer N, determinizations  will  be
	      aborted  whenever	the number of generated	states would exceed N.
	      In this case a non-deterministic automaton will be returned.

       det-scc
	      Set to 0 to disable scc-based optimizations in the  determiniza-
	      tion algorithm.

       det-simul
	      Set to 0 to disable simulation-based optimizations in the	deter-
	      minization algorithm.

       det-stutter
	      Set to 0 to disable optimizations	based on  the  stutter-invari-
	      ance in the determinization algorithm.

       gen-reduce-parity
	      When  the	postprocessor routines are configured to output	autom-
	      ata with any kind	of acceptance condition, but  they  happen  to
	      process  an  automaton with parity acceptance, they call a func-
	      tion to minimize the number of colors needed.  This option  con-
	      trols what happen	when this reduction does not reduce the	number
	      of colors: when set (the default)	the output of the reduction is
	      returned,	 this  means  the  colors  in  the  automaton may have
	      changed slightly,	and in particular, there is no transition with
	      more  than  one color; when unset, the original automaton	is re-
	      turned.

       gf-guarantee
	      Set to 0	to  disable  alternate	constructions  for  GF(guaran-
	      tee)->[D]BA  and	FG(safety)->DCA.  Those	constructions are from
	      an LICS'18 paper by J.  Esparza, J. KAentAnskA1/2, and S.	 Sick-
	      ert.   This  is enabled by default for medium and	high optimiza-
	      tion levels.  Unless we are building deterministic automata, the
	      resulting	 automata are compared to the automata built using the
	      more traditional pipeline, and only kept if they are better.

       relabel-bool
	      If set to	a positive integer N, a	formula	with N atomic proposi-
	      tions  or	 more  will have its Boolean subformulas abstracted as
	      atomic propositions during the translation  to  automaton.  This
	      relabeling can speeds the	translation if a few Boolean subformu-
	      las use a	large number of	atomic propositions.  By default  N=4.
	      Setting this value to 0 will disable the rewriting.

       sat-acc
	      When  this  is  set to some positive integer, the	SAT-based will
	      attempt to construct a TGBA with the given number	of  acceptance
	      sets.  states.  It may however return an automaton with less ac-
	      ceptance sets if some of these are useless.  Setting sat-acc au-
	      tomatically sets sat-minimize to 1 if not	set differently.

       sat-incr-steps
	      Set  the	value  of sat-incr-steps. This variable	is used	by two
	      SAT-based	minimization algorithms: (2) and (3).  They  are  both
	      described	below.

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

       sat-minimize
	      Set it to	enable SAT-based minimization of  deterministic	 TGBA.
	      Depending	on its value (from 1 to	4) it changes the algorithm to
	      perform. The default value is (1)	and it proves to be  the  most
	      effective	 method. SAT-based minimization	uses PicoSAT (distrib-
	      uted with	Spot), but another installed  SAT-solver  can  be  set
	      thanks  to  the  SPOT_SATSOLVER  environment  variable. Enabling
	      SAT-based	minimization will also enable tba-det.

       sat-states
	      When this	is set to some positive	integer, the  SAT-based	 mini-
	      mization	will attempt to	construct a TGBA with the given	number
	      of states.  It may however return	an automaton with less	states
	      if some of these are unreachable or useless.  Setting sat-states
	      automatically enables sat-minimize, but  no  iteration  is  per-
	      formed.	If  no	equivalent automaton could be constructed with
	      the given	number of states, the original automaton is returned.

       scc-filter
	      Set to 1 (the default) to	enable SCC-pruning and acceptance sim-
	      plification  at  the  beginning  of post-processing. Transitions
	      that are outside of accepting SCC	 are  removed  from  accepting
	      sets, except those that enter into an accepting SCC. Set to 2 to
	      remove even these	entering transition from the  accepting	 sets.
	      Set  to  0 to disable this SCC-pruning and acceptance simpifica-
	      tion pass.

       simul  Set to 0 to disable simulation-based reductions.	Set  to	 1  to
	      use only direct simulation. Set to 2 to use only reverse simula-
	      tion. Set	to 3 to	iterate	both direct and	 reverse  simulations.
	      The  default  is	3,  except  when option	--low is specified, in
	      which case the default is	1.

       state-based
	      Set to 1 to instruct the SAT-minimization	procedure to produce a
	      TGBA  where all outgoing transition of a state have the same ac-
	      ceptance sets.  By default this is only enabled when  option  -B
	      is used.

       tba-det
	      Set  to  1  to attempt a powerset	determinization	if the TGBA is
	      not already deterministic.  Doing	so will	degeneralize  the  au-
	      tomaton.	 This  is  disabled by default,	unless sat-minimize is
	      set.

       wdba-minimize
	      Set to 0 to disable WDBA-minimization, to	1 to always try	it, or
	      2	 to  attempt  it  only on syntactic obligations	or on automata
	      that are weak and	deterministic.	The default  is	 1  in	--high
	      mode,  else  2  in  --medium or --deterministic modes, else 0 in
	      --low mode.

SAT-MINIMIZE VALUES
       1      Used by default, 1 performs 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.

       2      Use PicoSAT assumptions. Each iteration encodes the search of an
	      (N-1) state equivalent automaton,	and additionally assumes  that
	      the  last	sat-incr-steps states are unnecessary. On failure, re-
	      lax the assumptions to  do  a  binary  search  between  N-1  and
	      N-1-sat-incr-steps.  sat-incr-steps defaults to 6.

       3      After  an	 (N-1) state automaton has been	found, use 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 will occur	 after	sat-incr-steps	itera-
	      tions  unless sat-incr-steps=-1 (see SPOT_XCNF environment vari-
	      able). sat-incr-steps defaults to	2.

       4      This naive method	tries to reduce	the size of the	automaton  one
	      state  at	 a  time.  Note	that it	restarts all the encoding each
	      time.

ENVIRONMENT VARIABLES
       SPOT_BDD_TRACE
	      If this variable is set  to  any	value,	statistics  about  BDD
	      garbage  collection  and resizing	will be	output on standard er-
	      ror.

       SPOT_DEFAULT_FORMAT
	      Set to a value of	dot or hoa to override the default format used
	      to  output automata.  Up to Spot 1.9.6 the default output	format
	      for automata used	to be dot.  Starting with Spot 1.9.7, the  de-
	      fault  output  format  switched  to hoa as it is more convenient
	      when chaining tools in a pipe.  Set this variable	to dot to  get
	      the  old	behavior.   Additional	options	 may  be passed	to the
	      printer by suffixing the output format with = and	 the  options.
	      For instance running
		  % SPOT_DEFAULT_FORMAT=dot=bar	autfilt	...
	      is the same as running
		  % autfilt --dot=bar ...
	      but  the use of the environment variable makes more sense	if you
	      set it up	once for many commands.

       SPOT_DEBUG_PARSER
	      If this variable is set to any value, the	 automaton  parser  of
	      Spot  is	executed  in debug mode, showing how the input is pro-
	      cessed.

       SPOT_DOTDEFAULT
	      Whenever the --dot option	is used	 without  argument  (even  im-
	      plicitely	 via  SPOT_DEFAULT_FORMAT), the	contents of this vari-
	      able is used as default argument.	 If you	have some default set-
	      tings  in	SPOT_DOTDEFAULT	and want to append to options xyz tem-
	      porarily for one call, use --dot=.xyz: the dot character will be
	      replaced	by  the	 contents  of  the SPOT_DOTDEFAULT environment
	      variable.

       SPOT_DOTEXTRA
	      The contents of this variable is added to	any dot	output,	 imme-
	      diately before the first state is	output.	 This makes it easy to
	      override global attributes of the	graph.

       SPOT_HOA_TOLERANT
	      If this variable is set, a few sanity checks  performed  by  the
	      HOA  parser  are	skipped.  The tests in questions correspond to
	      issues in	third-party tools that	output	incorrect  HOA	(e.g.,
	      declaring	the automaton with property "univ-branch" when no uni-
	      versal branching is actually used)

       SPOT_O_CHECK
	      Specifies	the default algorithm  that  should  be	 used  by  the
	      is_obligation()  function.   The value should be one of the fol-
	      lowing:

		     1	    Make sure that the formula and  its	 negation  are
			    realizable by non-deterministic co-BA1/4chi	autom-
			    ata.

		     2	    Make sure that the formula and  its	 negation  are
			    realizable by deterministic	BA1/4chi automata.

		     3	    Make sure that the formula is realizable by	a weak
			    and	deterministic BA1/4chi automata.

       SPOT_OOM_ABORT
	      If this variable is set, Out-Of-Memory errors will  abort()  the
	      program  (potentially  generating	a coredump) instead of raising
	      an exception.  This is useful to debug a program and to obtain a
	      stack trace pointing to the function doing the allocation.  When
	      this variable is unset (the default), std::bad_alloc are	thrown
	      on memory	allocation failures, and the stack is usually unwinded
	      up to top-level, losing the original context of the error.  Note
	      that  at least ltlcross has some custom handling of std::bad_al-
	      loc to recover from products that	are  too  large	 (by  ignoring
	      them), and setting this variable will interfer with that.

       SPOT_PR_CHECK
	      Select the default algorithm that	must be	used to	check the per-
	      sistence or recurrence property of a formula f.  The  values  it
	      can  take	 are between 1 and 3. All  methods work	either on f or
	      !f thanks	to the duality of persistence and recurrence  classes.
	      See  this	 page  <https://spot.lrde.epita.fr/hierarchy.html> for
	      more details. If it is set to:

		     1	    It will try	to check if f (or !f)  is  co-BA1/4chi
			    realizable	in  order  to tell if f	belongs	to the
			    persistence	(or the	recurrence) class.

		     2	    It checks if f (or !f) is det-BA1/4chi  realizable
			    via	a reduction to deterministic-Rabin in order to
			    tell if f belongs to the recurrence	(or  the  per-
			    sistance) class.

		     3	    It	checks if f (or	!f) is det-BA1/4chi realizable
			    via	a reduction to deterministic-parity  in	 order
			    to	tell  if  f  belongs to	the recurrence (or the
			    persistance) class.

       SPOT_SATLOG
	      If set to	a filename, the	SAT-based minimization	routines  will
	      append  statistics about each iteration to the named file.  Each
	      line lists the following comma-separated values: input number of
	      states,  target  number of states, number	of reachable states in
	      the output, number of edges in the output, number	of transitions
	      in the output, number of variables in the	SAT problem, number of
	      clauses in the SAT problem, user time for	encoding the SAT prob-
	      lem,  system  time  for  encoding	the SAT	problem, user time for
	      solving the SAT problem, system time for solving the  SAT	 prob-
	      lem, automaton produced at this step in HOA format.

       SPOT_SATSOLVER
	      If  set,	this  variable should indicate how to call an external
	      SAT-solver - by default, Spot uses PicoSAT, which	is distributed
	      with.  This  is used by the sat-minimize option described	above.
	      The format to follow is the following:  "<sat_solver>  [options]
	      %I >%O".	The escape sequences %I	and %O respectively denote the
	      names of the input and output files.  These temporary files  are
	      created in the directory specified by SPOT_TMPDIR	or TMPDIR (see
	      below). The SAT-solver should follow the convention of  the  SAT
	      Competition for its input	and output format.

       SPOT_STREETT_CONV_MIN
	      The  number of Streett pairs above which conversion from Streett
	      acceptance to generalized-BA1/4chi  acceptance  should  be  made
	      with  a  dedicated  algorithm.  By default this is 3, i.e., if a
	      Streett automaton	with 3 acceptance pairs	or more	has to be con-
	      verted  into  generalized-BA1/4chi,  the	dedicated algorithm is
	      used.  This algorithm is close to	the classical conversion  from
	      Streett  to  BA1/4chi, but with several tweaks.  When this algo-
	      rithm is not used, the standard "Fin-removal" approach  is  used
	      instead:	first  the acceptance condition	is converted into dis-
	      junctive normal form (DNF), then Fin acceptance is removed  like
	      for   Rabin  automata,  yielding	a  disjuction  of  generalized
	      BA1/4chi acceptance, and the result is  finally  converted  into
	      conjunctive  normal  form	(CNF) to obtain	a generalized BA1/4chi
	      acceptance.  Both	algorithms have	a worst-case size that is  ex-
	      ponential	 in  the  number of Streett pairs, but in practice the
	      dedicated	algorithm works	better for most	Streett	automata  with
	      3	 or  more pairs	(and many 2-pair Streett automata as well, but
	      the difference here is less clear).  Setting this	variable to  0
	      will  disable the	dedicated algorithm.  Setting it to 1 will en-
	      able it for all Streett automata,	however	we  do	not  recommand
	      setting it to less than 2, because the "Fin-removal" approach is
	      better for single-pair Streett automata.

       SPOT_STUTTER_CHECK
	      Select the default check used to decide stutter invariance.  The
	      variable	should	hold a value between 1 and 8, corresponding to
	      the following tests described in our Spin'15 paper (see the BIB-
	      LIOGRAPHY	section).  The default is 8.

		     1	    sl(a) x sl(!a)

		     2	    sl(cl(a)) x	!a

		     3	    cl(sl(a)) x	!a

		     4	    sl2(a) x sl2(!a)

		     5	    sl2(cl(a)) x !a

		     6	    cl(sl2(a)) x !a

		     7	    sl(a) x sl(!a), performed on-the-fly

		     8	    cl(a) x cl(!a)
       This  variable is used by the --check=stutter-invariance	and --stutter-
       invariant options, but it is ignored by --check=stutter-sensitive-exam-
       ple.

       SPOT_TMPDIR, TMPDIR
	      These  variables	control	 in  which  directory  temporary files
	      (e.g., those who contain the input and output  when  interfacing
	      with  translators) are created.  TMPDIR is only read if SPOT_TM-
	      PDIR does	not exist.  If none of these environment variables ex-
	      ist,  or	if their value is empty, files are created in the cur-
	      rent directory.

       SPOT_TMPKEEP
	      When this	variable is defined, temporary files are not  removed.
	      This is mostly useful for	debugging.

       SPOT_XCNF
	      Assign  a	 folder	 path  to this variable	to generate XCNF files
	      whenever SAT-based minimization is used -	the file  is  outputed
	      as  "incr.xcnf"  in  the specified directory. This feature works
	      only with	an external SAT-solver.	See SPOT_SATSOLVER to know how
	      to  provide  one.	 Also  note that this needs an incremental ap-
	      proach  without	restarting   the   encoding   i.e   "sat-mini-
	      mize=3,param=-1"	for  ltl2tgba  and ltl2tgta or "incr,param=-1"
	      for autfilt (see sat-minimize options described above or autfilt
	      man page).  The XCNF format is the one used by the SAT incremen-
	      tal competition.

BIBLIOGRAPHY
       1.     Christian	Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing  the
	      Powerset Construction for	Restricted Classes of I-Automata. Pro-
	      ceedings of ATVA'07.  LNCS 4762.

	      Describes	the WDBA-minimization algorithm	implemented  in	 Spot.
	      The algorithm used for the tba-det options is also a generaliza-
	      tion (to TBA instead of BA) of what they	describe  in  sections
	      3.2 and 3.3.

       2.     TomA!A!  Babiak,	Thomas	Badie,	Alexandre  Duret-Lutz,	MojmAr
	      KAetAnskA1/2, Jan	StrejAek: Compositional	Approach to Suspension
	      and  Other  Improvements	to  LTL	 Translation.	Proceedings of
	      SPIN'13.	LNCS 7976.

	      Describes	the compositional suspension, the simulation-based re-
	      ductions,	and the	SCC-based simplifications.

       3.     RA1/4diger  Ehlers:  Minimising  Deterministic BA1/4chi Automata
	      Precisely	using SAT Solving.  Proceedings	of SAT'10.  LNCS 6175.

	      Our SAT-based minimization  procedures  are  generalizations  of
	      this paper to deal with TBA or TGBA.

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

	      Describes	 the  stutter-invariance  checks  that can be selected
	      through SPOT_STUTTER_CHECK.

       5.     Javier Esparza, Jan KAetAnskA1/2 and Salomon Sickert: One	 Theo-
	      rem to Rule Them All: A Unified Translation of LTL into I-Autom-
	      ata.  Proceedings	of LICS'18.  To	appear.

	      Describes	(among other things) the constructions used for	trans-
	      lating  formulas	of  the	form GF(guarantee) or FG(safety), that
	      can be disabled with -x gf-guarantee=0.

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
       ltl2tgba(1) ltl2tgta(1) dstar2tgba(1) autfilt(1)

spot-x (spot) 2.9.3		   July	2020			     SPOT-X(7)

NAME | SYNOPSIS | DESCRIPTION | SAT-MINIMIZE VALUES | ENVIRONMENT VARIABLES | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO

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

home | help