Commit ce2bb052 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add compositional suspension to the web interface.

* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add options for compositional suspension.
* wrap/python/ajax/spot.in: Implement them.
* wrap/python/spot.i: Export compsusp().
parent 53c69235
......@@ -568,6 +568,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<li><a href="#tabs-tla" class="btip" title="Builds a purely symbolic automaton, using BDDs to encode the transition relation. The translation itself is fast (it uses a number of BDD operations that is linear in the size of the formula), but the resulting symbolic encoding is better used symbolically. If you develop it explicitly (e.g. to draw it, as on this page) the result can easily have an exponential number of states.">Couvreur/LaCIM</a></li>
<li><a href="#tabs-tta" class="btip" title="An implementation of Heikki Tauriainen's Ph.D. thesis algorithm to translate LTL formulas via very weak alternating automata with transition-based generalized acceptance conditions.">Tauriainen/TAA</a></li>
<li><a href="#tabs-tl3" class="btip" title="An improved version of LTL2BA, overhauled by Tomáš Babiak during his Ph.D., and described at TACAS'12.<br>LTL3BA is not part of Spot. Options in this tab correspond to options offered by LTL3BA, and have some overlap with the options offered by Spot upstream and downstream.">LTL3BA</a></li>
<li><a href="#tabs-tcs" class="btip" title="Compositionnal suspension.<br>Work in progress.">Comp.Susp.</a></li>
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
</ul>
<input type="hidden" name="t" value="fm">
......@@ -646,6 +647,28 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
direct simulation on BA
</label><br>
</div>
<div id="tabs-tcs">
<label class="rtip" title="Apply WDBA minimization on intermediate automaton. We can only do it if the input formula is an obligation (in this case there is nothing to suspend and the automaton we process is already the final one) or if the intermediate automaton has the shape of a guarantee property.">
<INPUT type="checkbox" name="cs" value="w" checked>
WDBA minimization of intermediate automaton
</label><br>
<label class="rtip" title="Apply direct simulation on intermediate automaton. This is only done when the WDBA minimization could not work.">
<INPUT type="checkbox" name="cs" value="s" checked>
direct simulation on intermediate automaton
</label><br>
<label class="rtip" title="Start suspension on transitions that enter accepting SCCs instead of waiting to be in the SCC.">
<INPUT type="checkbox" name="cs" value="e">
early start of suspended automata
</label><br>
<label class="rtip" title="Output the intermediate automaton with labels showing where suspended formulae should be attached.">
<INPUT type="checkbox" name="cs" value="c">
do not compose suspended formulas (for debugging)
</label><br>
<label class="rtip" title="Consider obligation subformulas as atomic propositions initially, and compose their WDBA-minimized translation.">
<INPUT type="checkbox" name="cs" value="o">
compose WDBA-minimized obligation sub-formulas
</label><br>
</div>
</div>
</div>
<div id="autsimp-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
......
......@@ -63,6 +63,7 @@ Translator algorithm (pick one)
t=la Couvreur/LaCIM
t=ta Tauriainen/TAA
t=l3 LTL3BA
t=cs Compositional Suspension
Couvreur/FM options if t=fm (pick many)
......@@ -95,6 +96,14 @@ LTL3BA processing options if t=l3 (pick many)
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
......
......@@ -91,7 +91,7 @@ if not script:
return True
return False
server_address=('',8000)
server_address=('', 8000)
if not os.access(imgdir, os.F_OK):
# 493 = 0755 but we would have to write 0755 or 0o755
# depending on the python version...
......@@ -577,6 +577,23 @@ elif translator == 'l3':
unbufprint('</div>')
automaton = 0
finish()
elif translator == 'cs':
donot_inject = False
cs_nowdba = True
cs_nosimul = True
cs_early_start = False
for cs in form.getlist('cs'):
if cs == 'c':
donot_inject = True
elif cs == 'w':
cs_nowdba = False
elif cs == 's':
cs_nosimul = False
elif cs == 'e':
cs_early_start = True
automaton = spot.compsusp(f, dict, cs_nowdba, cs_nosimul,
cs_early_start, donot_inject)
# Monitor output
if output_type == 'm':
......
......@@ -98,6 +98,7 @@ namespace std {
#include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/compsusp.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh"
......@@ -197,6 +198,7 @@ using namespace spot;
%feature("new") spot::ltl_to_taa;
%feature("new") spot::ltl_to_tgba_fm;
%feature("new") spot::ltl_to_tgba_lacim;
%feature("new") spot::compsusp;
%feature("new") spot::minimize_wdba;
%feature("new") spot::minimize_monitor;
%feature("new") spot::scc_filter;
......@@ -294,6 +296,7 @@ using namespace spot;
%include "tgbaalgos/ltl2taa.hh"
%include "tgbaalgos/ltl2tgba_fm.hh"
%include "tgbaalgos/ltl2tgba_lacim.hh"
%include "tgbaalgos/compsusp.hh"
%include "tgbaalgos/magic.hh"
%include "tgbaalgos/minimize.hh"
%include "tgbaalgos/neverclaim.hh"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment