78f932081b
* wrap/python/ajax/protocol.txt: New file. * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add it.
73 lines
1.4 KiB
Text
73 lines
1.4 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=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
|