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

Add cosimulation and iterated_simulations to the web interface.

* wrap/python/spot.i (cosimulation, iterated_simulations): Declare.
* wrap/python/ajax/spot.in, wrap/python/ajax/protocol.txt,
wrap/python/ajax/ltl2tgba.html: Add options to trigger these two
optimizations.
parent 84b6240a
......@@ -90,6 +90,16 @@
$("#to-l,#to-s").attr('disabled', true);
}
})
$("#as-ds,#as-rs").change(function() {
if ($(this).is(':checked')) {
$("#as-is").removeAttr('checked');
}
})
$("#as-is").change(function() {
if ($(this).is(':checked')) {
$("#as-ds,#as-rs").removeAttr('checked');
}
})
function hideOrShowPanels(output, duration) {
switch (output)
......@@ -645,11 +655,18 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="checkbox" name="as" value="wd">
determinize and minimize obligation properties
</label><br>
<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">
<label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA. Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>suffixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b>. This algorithm may also improve determinism as a side effect.">
<INPUT id="as-ds" type="checkbox" name="as" value="ds">
direct simulation
</label>
<label class="rtip" title="Attempt to reduce the automaton by using <b>reverse simulation</b> on the TGBA. Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>prefixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b> This can also improve codeterminism as a side effect.">
<INPUT id="as-rs" type="checkbox" name="as" value="rs">
reverse simulation
</label>
<label class="rtip" title="Apply <b>direct</b> and <b>reverse simulation</b> alternatively until the automaton is not reduced further.">
<INPUT id="as-is" type="checkbox" name="as" value="is">
iterated simulations
</label><br>
</div>
</div>
<div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
......
......@@ -99,6 +99,8 @@ 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)
......
......@@ -579,6 +579,8 @@ if output_type == 'm':
prune_scc = False
wdba_minimize = False
direct_simul = False
reverse_simul = False
iterated_simul = False
for s in form.getlist('as'):
if s == 'ps':
prune_scc = True
......@@ -586,6 +588,10 @@ for s in form.getlist('as'):
wdba_minimize = True
elif s == 'ds':
direct_simul = True
elif s == 'rs':
reverse_simul = True
elif s == 'is':
iterated_simul = True
ta_type = None
buchi_type = None
......@@ -631,9 +637,20 @@ if wdba_minimize:
issba = True
direct_simul = False # No need to simulate anymore
if direct_simul:
if direct_simul and not iterated_simul:
automaton = spot.simulation(automaton)
issba = False
if reverse_simul and not iterated_simul:
automaton = spot.cosimulation(automaton)
issba = False
if iterated_simul:
automaton = spot.iterated_simulations(automaton)
issba = False
if prune_scc and (direct_simul or reverse_simul):
# Make a second pass after the simulation, since these might leave
# extra acceptance conditions.
automaton = spot.scc_filter(automaton, not degen)
if degen or neverclaim:
degen = spot.degeneralize(automaton)
......
......@@ -206,6 +206,8 @@ using namespace spot;
%feature("new") spot::tgba::succ_iter;
%feature("new") spot::tgba_succ_iterator::current_state;
%feature("new") spot::simulation;
%feature("new") spot::cosimulation;
%feature("new") spot::iterated_simulations;
%feature("new") spot::degeneralize;
%feature("new") spot::tgba_parse;
%feature("new") spot::tgba_to_ta;
......
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