From ce2bb052cbc23d89fa7fa9dc8232994b1c09baa4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 27 Apr 2013 10:13:46 +0200 Subject: [PATCH] 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(). --- wrap/python/ajax/ltl2tgba.html | 23 +++++++++++++++++++++++ wrap/python/ajax/protocol.txt | 9 +++++++++ wrap/python/ajax/spot.in | 19 ++++++++++++++++++- wrap/python/spot.i | 3 +++ 4 files changed, 53 insertions(+), 1 deletion(-) diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index b8a156af3..9d76a7eab 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -568,6 +568,7 @@ an identifier: aUb is an atomic proposition, unlike
  • Couvreur/LaCIM
  • Tauriainen/TAA
  • LTL3BA
    • +
  • Comp.Susp.
  • Fold
    • @@ -646,6 +647,28 @@ an identifier: aUb is an atomic proposition, unlike direct simulation on BA
    +
    +
    +
    +
    +
    +
    +
    diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt index 72d40f990..374ffb283 100644 --- a/wrap/python/ajax/protocol.txt +++ b/wrap/python/ajax/protocol.txt @@ -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 diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 12fd131a5..2057f9a48 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -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('
    ') 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': diff --git a/wrap/python/spot.i b/wrap/python/spot.i index a078f1edf..e91149c6a 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -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"