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

Preliminary work on integrating LTL3BA in ltl2tgba.html.

* wrap/python/ajax/ltl2tgba.html: Add a dedicated tab with
two columns of options.
* wrap/python/ajax/css/ltl2tgba.css: Support for two columns.
* wrap/python/ajax/protocol.txt: Document new options.
* wrap/python/ajax/spot.in: Handle the new options.
* wrap/python/ajax/Makefile.am: Substitude LTL3BA in spot.in.
parent 7ceca326
......@@ -50,6 +50,7 @@ spot.py: $(srcdir)/spot.in Makefile
-e 's|[@]top_builddir[@]|@top_builddir@|g' \
-e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \
-e 's|[@]DOT[@]|@DOT@|g' \
-e 's|[@]LTL3BA[@]|@LTL3BA@|g' \
<$(srcdir)/spot.in >spot.tmp
chmod +x spot.tmp
mv -f spot.tmp $@
......
......@@ -88,6 +88,11 @@ table.ltltable
float: right;
}
.colleft {
float: left;
width: 49%;
}
.ltl2tgba .head .ui-icon {
float: right;
margin: 1px 0px;
......
......@@ -54,6 +54,17 @@
}
})
$("#ltl3ba-T").change(function() {
if ($(this).is(':checked')) {
$("#ltl3ba-S").removeAttr('checked');
}
})
$("#ltl3ba-S").change(function() {
if ($(this).is(':checked')) {
$("#ltl3ba-U").attr('checked', true);
}
})
function hideOrShowPanels(output, duration) {
switch (output)
{
......@@ -469,6 +480,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton. This is the best algorithm of the three, and the only one that has been extended to support PSL operators.">Couvreur/FM</a></li>
<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 class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
</ul>
<input type="hidden" name="t" value="fm">
......@@ -503,6 +515,42 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
language containment
</label><br>
</div>
<div id="tabs-tl3">
Use <a href="http://sourceforge.net/projects/ltl3ba/">LTL3BA</a> to build:
<label class="rtip" title="Stop LTL3BA once it has built a Transition-based Generalized Büchi Automaton. Spot will take it from here and optionally apply more optimizations.">
<INPUT id="ltl3ba-T" type="radio" name="lo" value="T" checked>
a TGBA
</label> or <label class="rtip" title="Run LTL3BA until it produces its final Büchi Automaton. Spot will consider this BA has a TGBA if further optimizations have been requested below.">
<INPUT id="ltl3ba-U" type="radio" name="lo" value="U">
a BA
</label></br>
<div class="colleft">
<label class="rtip" title="LTL simplifications performed in LTL3BA are independent of those Spot may have performed upstream.">
<INPUT type="checkbox" name="l3" value="l" checked>
LTL simplifications
</label><br>
<label class="rtip" title="Suspension is a technique to postpone the verification some subformulae. Any easy way to picture it is to look at the formula <span class='formula'>F(a)&GF(b)</span>: the <span class='formula'>GF(b)</span> part need not be checked before some <span class='formula'>a</span> has been seen. On this example, suspension amounts to translating <span class='formula'>F(a&GF(b))</span> but the technique is more general than such LTL rewritings.">
<INPUT type="checkbox" name="l3" value="P" checked>
suspension in TGBA
</label><br>
<label class="rtip" title="See previous tooltip for an explanation of suspension. This version disables suspension in the intermediate alternating automaton, where it is only used for one step.">
<INPUT type="checkbox" name="l3" value="A" checked>
suspension in alternating automaton
</label><br>
</div>
<label class="rtip" title="Compute Strongly Connected Components to simplify the automaton">
<INPUT type="checkbox" name="l3" value="C" checked>
SCC simplifications
</label><br>
<label class="rtip" title="Try to improve the automaton's determinism when building it. This may produce larger automata.">
<INPUT type="checkbox" name="l3" value="M">
more deterministic output
</label><br>
<label class="rtip" title="Compute a direct (a.k.a strong fair) simulation relation to reduce the size of the Büchi automaton.">
<INPUT id="ltl3ba-S" type="checkbox" name="l3" value="S">
direct simulation on BA
</label><br>
</div>
</div>
</div>
<div id="autsimp-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
......@@ -516,7 +564,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="checkbox" name="as" value="wd">
minimize obligation properties
</label><br>
<label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b>. This might also improve the determinism as a side effect.">
<label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA. This might also improve the determinism as a side effect.">
<INPUT type="checkbox" name="as" value="ds">
direct simulation
</label><br>
......
......@@ -53,22 +53,37 @@ Translator algorithm (pick one)
t=fm Couvreur/FM
t=la Couvreur/LaCIM
t=ta Tauriainen/TAA
t=l3 LTL3BA
Couvreur/FM options if f=fm (pick many)
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 f=la
Couvreur/LA options if t=la
la=sp Symbolic Pruning
Tauriainen/TAA options if f=ta
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
Automaton simplifications (pick many)
as=ps Prune SCC
......
......@@ -452,13 +452,16 @@ if output_type == 'f':
translator = form.getfirst('t', 'fm')
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
print ('''<div class="error">The PSL formula %s
unbufprint('''<div class="error">The PSL formula %s
cannot be translated using this algorithm. Please use Couveur/FM.'''
% format_formula(f, 'span'));
% format_formula(f, 'span'))
finish()
dict = spot.bdd_dict()
# Should the automaton be displayed as a SBA?
issba = False
if translator == 'fm':
exprop = False
symb_merge = False
......@@ -485,12 +488,53 @@ elif translator == 'ta':
if form.getfirst('ta', '') == 'lc':
refined_rules = True
automaton = spot.ltl_to_taa(f, dict, refined_rules)
# Should it be displayed as a SBA?
issba = False
elif translator == 'l3':
l3out = '-T'
l3opt = { '-l', '-P', '-A', '-c', '-C' }
for lo in form.getfirst('lo', 'T'):
if lo == 'U':
l3out = '-U'
issba = True
for l3 in form.getlist('l3'):
if l3 == 'l':
l3opt.remove('-l')
elif l3 == 'P':
l3opt.remove('-P')
elif l3 == 'A':
l3opt.remove('-A')
elif l3 == 'C':
l3opt.remove('-C')
l3opt.remove('-c')
elif l3 == 'M':
l3opt.add('-M')
elif l3 == 'S':
l3opt.add('-S')
args = ["@LTL3BA@", l3out]
args.extend(l3opt)
args.extend(['-f', spot.to_spin_string(f)])
import subprocess
l3file = tmpdir + "/aut"
l3aut = open(l3file, "w+")
l3proc = subprocess.Popen(args, stdout=l3aut)
l3aut.close()
ret = l3proc.wait()
if ret != 0:
unbufprint('''<div class="error">ltl3ba exited with error %s</div>'''
% ret)
finish()
tpel = spot.empty_tgba_parse_error_list()
automaton = spot.tgba_parse(l3file, tpel, dict, env)
if tpel:
unbufprint('''<div class="error">failed to read ltl3ba's output</div>''')
unbufprint('<div class="parse-error">')
err = spot.format_tgba_parse_errors(spot.get_cout(), "output", tpel)
unbufprint('</div>')
automaton = 0
finish()
# Monitor output
if output_type == 'm':
issba = False
automaton = spot.scc_filter(automaton)
automaton = spot.minimize_monitor(automaton)
unbufprint('<div class="automata-stats">')
......@@ -534,6 +578,7 @@ if prune_scc:
# degeneralization or simulation is requested: keeping those that
# lead to accepting states usually helps.
automaton = spot.scc_filter(automaton, not (degen or direct_simul))
issba = False
if wdba_minimize:
minimized = spot.minimize_obligation_new(automaton, f)
......@@ -546,6 +591,7 @@ if wdba_minimize:
if direct_simul:
automaton = spot.simulation(automaton)
issba = False
if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton)
......
Supports Markdown
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