alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Add the simulation in the Spot web interface.

Browse source 
* wrap/python/ajax/spot.in: Add the simulation.
* wrap/python/ajax/protocol.txt: Add the direct simulation in the
automaton simplifications section.
* wrap/python/spot.i (simulation_new): Create a function which
takes an automaton and a call to the simulation with the good
template parameter.
* wrap/python/ajax/ltl2tgba.html: Add the direct simulation
checkbox.
This commit is contained in:
Thomas Badie 2012-04-15 13:12:29 +02:00
parent 085ea52bf5
commit dfcaed034e
4 changed files with 16 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
wrap/python/ajax/ltl2tgba.html
View file

@ -445,6 +445,11 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="checkbox" name="as" value="wd"> <INPUT type="checkbox" name="as" value="wd">
minimize obligation properties minimize obligation properties
</label><br> </label><br>
<label class="rtip" title="<b>Direct Simulation</b> tries to reduce the automaton with simulation reduction.">
<INPUT type="checkbox" name="as" value="rs">
direct simulation
</label><br>
</div> </div>
</div> </div>
<div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow"> <div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">

1
wrap/python/ajax/protocol.txt
View file

@ -71,3 +71,4 @@ Automaton simplifications (pick many)
as=ps Prune SCC as=ps Prune SCC
as=wd WDBA minimiztion as=wd WDBA minimiztion
as=rs Simulation reduction

7
wrap/python/ajax/spot.in
View file

@ -411,11 +411,14 @@ if output_type == 'm':
# Automaton simplifications # Automaton simplifications
prune_scc = False prune_scc = False
wdba_minimize = False wdba_minimize = False
simul_minimize = False
for s in form.getlist('as'): for s in form.getlist('as'):
if s == 'ps': if s == 'ps':
prune_scc = True prune_scc = True
elif s == 'wd': elif s == 'wd':
wdba_minimize = True wdba_minimize = True
elif s == 'rs':
simul_minimize = True
if output_type == 'a': if output_type == 'a':
buchi_type = form.getfirst('af', 't') buchi_type = form.getfirst('af', 't')
@ -447,6 +450,10 @@ if wdba_minimize:
minimized = 0 minimized = 0
degen = False # No need to degeneralize anymore degen = False # No need to degeneralize anymore
issba = True issba = True
simul_minimize = False # No need to simulate anymore
if simul_minimize:
automaton = spot.simulation(automaton)
if degen or neverclaim: if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton) degen = spot.tgba_sba_proxy(automaton)

4
wrap/python/spot.i
View file

@ -101,6 +101,7 @@
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
#include "tgbaalgos/simulation.hh"
using namespace spot::ltl; using namespace spot::ltl;
using namespace spot; using namespace spot;
@ -186,7 +187,7 @@ using namespace spot;
%feature("new") spot::tgba::get_init_state; %feature("new") spot::tgba::get_init_state;
%feature("new") spot::tgba::succ_iter; %feature("new") spot::tgba::succ_iter;
%feature("new") spot::tgba_succ_iterator::current_state; %feature("new") spot::tgba_succ_iterator::current_state;
%feature("new") spot::simulation;
// Help SWIG with namespace lookups. // Help SWIG with namespace lookups.
#define ltl spot::ltl #define ltl spot::ltl
%include "tgba/bdddict.hh" %include "tgba/bdddict.hh"
@ -230,6 +231,7 @@ using namespace spot;
%include "tgbaalgos/save.hh" %include "tgbaalgos/save.hh"
%include "tgbaalgos/sccfilter.hh" %include "tgbaalgos/sccfilter.hh"
%include "tgbaalgos/stats.hh" %include "tgbaalgos/stats.hh"
%include "tgbaalgos/simulation.hh"
#undef ltl #undef ltl
%extend spot::ltl::formula { %extend spot::ltl::formula {