This outlines the arguments passed by ltl2tgba.html to spot.py.


Specifying the formula to work with

  f=...   the formula

Formula simplifications (pick many)

  r=br    enable Basic Reductions
  r=si    enable Syntactic Implications
  r=eu    enable Eventuality and Universality
  r=lc    enable Language Containment

Choosing the desired output (pick one)

  o=v     output version  (no other argument needed)
  o=f     output formula
  o=m     output monitor
  o=a     output automaton
  o=r     output run

Type of formula output if o=f (pick one)

  ff=o    Spot syntax
  ff=i    Spin syntax
  ff=g    graphviz

Type of automaton if o=a (pick one)

  af=t    TGBA
  af=s    SBA
  af=i    Spin neverclaim

Type of monitor if o=m (pick one -- no choice)

  mf=d

Type of automaton for run if o=r (pick one)

  ra=t    run on TGBA
  ra=s    run on SBA

Type of run output if o=r (pick one)

  rf=p    print run as text
  rf=d    draw run

Translator algorithm (pick one)

  t=fm    Couvreur/FM
  t=la    Couvreur/LaCIM
  t=ta    Tauriainen/TAA

Couvreur/FM options if f=fm (pick many)

  fm=od   Optimize Determinism
  fm=sm   Symbolic Merge
  fm=bp   Branching Postponement
  fm=fl   Fair-Loop approximations

Couvreur/LA options if f=la

  la=sp   Symbolic Pruning

Tauriainen/TAA options if f=ta

  ta=lc   refined rules based on Language Containment

Automaton simplifications (pick many)

  as=ps   Prune SCC
  as=wd   WDBA minimiztion