rename wrap/python/ to python/

* 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.
2015-12-25 11:55:31 +01:00 · 2015-12-25 11:55:31 +01:00 · 34c3c1cedc
commit 34c3c1cedc
parent 74ec9c54c4
62 changed files with 24 additions and 48 deletions
--- a/python/ajax/protocol.txt
+++ b/python/ajax/protocol.txt
@ -0,0 +1,124 @@
+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.