Document the protocol used between ltl2tgba.html and spot.py.

* wrap/python/ajax/protocol.txt: New file.
* wrap/python/ajax/Makefile.am (EXTRA_DIST): Add it.

wrap/python/ajax/Makefile.am

@@ -37,7 +37,8 @@ EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css	\
   css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png	\
   css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png		\
   css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png	\
-  css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png
+  css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png      \
+  protocol.txt
 
 CLEANFILES = $(nodist_noinst_SCRIPTS)
 

wrap/python/ajax/protocol.txt

@@ -0,0 +1,73 @@
+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