From 78f932081be7de839a5b4d6df7e6ed4224a8a8b3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 3 Jun 2011 17:13:53 +0200
Subject: [PATCH] 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.
---
 ChangeLog                     |  7 ++++
 wrap/python/ajax/Makefile.am  |  3 +-
 wrap/python/ajax/protocol.txt | 73 +++++++++++++++++++++++++++++++++++
 3 files changed, 82 insertions(+), 1 deletion(-)
 create mode 100644 wrap/python/ajax/protocol.txt

diff --git a/ChangeLog b/ChangeLog
index 0ad41646d..8e7d6163f 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,10 @@
+2011-06-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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.
+
 2011-06-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* iface/dve2/README: Document state compression.
diff --git a/wrap/python/ajax/Makefile.am b/wrap/python/ajax/Makefile.am
index 23e80f9dd..bd360e9de 100644
--- a/wrap/python/ajax/Makefile.am
+++ b/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)
 
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
new file mode 100644
index 000000000..9f536a86d
--- /dev/null
+++ b/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