34c3c1cedc
* wrap/python/: Rename to... * python/: ... this. * wrap/: Delete. * Makefile.am, README, configure.ac, debian/python3-spot.examples, debian/rules, doc/org/.dir-locals.el.in, doc/org/init.el.in, spot/sanity/ipynb.test: Adjust.
124 lines
2.8 KiB
Text
124 lines
2.8 KiB
Text
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=l LBT 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)
|
|
|
|
mf=d deterministic
|
|
mf=n nondeterministic
|
|
|
|
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
|
|
t=cs Compositional Suspension
|
|
|
|
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
|
|
|
|
Compositional Suspension options (pick many)
|
|
|
|
cs=w WDBA minimization
|
|
cs=s simulation
|
|
cs=e early start of suspended automatas
|
|
cs=c do not compose suspended formulae (for debugging)
|
|
cs=o compose obligation subformulae
|
|
|
|
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.
|