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

Add more ltl3ba options.

* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add options 'o' and 'p'.
* wrap/python/ajax/spot.in: Handle these, and use '-v' to check
version.
parent 689f56f4
......@@ -540,15 +540,23 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="checkbox" name="l3" value="l" checked>
LTL simplifications
</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>
<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 class="rtip" title="<font color='red'><b>FIXME</b></font>: missing description">
<INPUT type="checkbox" name="l3" value="o" checked>
on-the-fly simplifications
</label><br>
</div>
<label class="rtip" title="<font color='red'><b>FIXME</b></font>: missing description">
<INPUT type="checkbox" name="l3" value="p" checked>
a-posteriori simplifications
</label><br>
<label class="rtip" title="Compute Strongly Connected Components to simplify the automaton">
<INPUT type="checkbox" name="l3" value="C" checked>
SCC simplifications
......
......@@ -84,6 +84,8 @@ LTL3BA processing options if t=l3 (pick many)
l3=C SCC simplifications
l3=M more deterministic output
l3=S direct simulation
l3=o on-the-fly simplifications
l3=p a-posteriori simplifications
Automaton simplifications (pick many)
......
......@@ -341,7 +341,7 @@ if output_type == 'v':
if output_type == 'v3':
import subprocess
try:
l3proc = subprocess.Popen(['@LTL3BA@', '-V'], stdout=subprocess.PIPE)
l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE)
(ver, err) = l3proc.communicate()
err = l3proc.returncode
except:
......@@ -505,7 +505,7 @@ elif translator == 'ta':
automaton = spot.ltl_to_taa(f, dict, refined_rules)
elif translator == 'l3':
l3out = '-T'
l3opt = { '-l', '-P', '-A', '-c', '-C' }
l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p' }
for lo in form.getfirst('lo', 'T'):
if lo == 'U':
l3out = '-U'
......@@ -524,6 +524,10 @@ elif translator == 'l3':
l3opt.add('-M')
elif l3 == 'S':
l3opt.add('-S')
elif l3 == 'o':
l3opt.remove('-o')
elif l3 == 'p':
l3opt.remove('-p')
args = ["@LTL3BA@", l3out]
args.extend(l3opt)
args.extend(['-f', spot.to_spin_string(f)])
......
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