bdeb87a6b0
* wrap/python/ajax/ltl2tgba.html: Add a checkbox and some code to keep it consistent with the basic rewriting checkbox. * wrap/python/ajax/spot.in: Deal with the new option. * wrap/python/ajax/protocol.txt: Document it.
76 lines
1.5 KiB
Text
76 lines
1.5 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
|
|
|
|
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
|
|
|
|
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
|
|
as=ds Direct Simulation reduction
|