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=lf    allow larger formulas
  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
  o=t     output testing automaton
  o=v3    output LTL3BA's version  (no other argument needed)

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

  ff=o    Spot syntax
  ff=i    Spin syntax
  ff=g    graphviz output of the AST
  ff=p    property dump

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

Type of testing automaton if o=t (pick one)

  tf=t    TA
  tf=g    GTA
  tf=a    TGTA

Translator algorithm (pick one)

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

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

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

Couvreur/LA options if t=la

  la=sp   Symbolic Pruning

Tauriainen/TAA options if t=ta

  ta=lc   refined rules based on Language Containment

LTL3BA output options if t=l3 (pick one)

  lo=T    output a TGBA
  lo=U    output a BA

LTL3BA processing options if t=l3 (pick many)

  l3=l    LTL formula simplification
  l3=P    suspension in TGBA construction
  l3=A    suspension in alternating automaton construction
  l3=C    SCC simplifications
  l3=M    more deterministic output
  l3=S    direct simulation
  l3=o    on-the-fly simplifications
  l3=p    a-posteriori simplifications

Automaton simplifications (pick many)

  as=ps   Prune SCC
  as=wd   WDBA minimiztion
  as=ds   Direct Simulation reduction
  as=rs   Reverse Simulation reduction
  as=is   Iterated Simulation reduction (disables ds and rs)

Testing Automaton options (pick many)

  to=l    add a catch-all livelock state
  to=s    produce single-pass variant
  to=m    merge bisimilar states

Global options

  g=8     Enable UTF-8 output.