diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index e7a4f8075da0ab3efa91156b4ec42018579164f2..69b510ce327509c492e68b5f7913329fcd5fad9c 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -439,6 +439,7 @@ an identifier: aUb is an atomic proposition, unlike
  • Monitor
  • Büchi Automaton
  • Büchi Run
    • +
  • Testing Automaton
  • Fold
    • @@ -504,6 +505,21 @@ an identifier: aUb is an atomic proposition, unlike draw an accepting run on top of the automaton
    +
    + Translate the (simplified) formula as:
    +
    +
    +
    +
    diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt index e17843b6ba5cfad2f31c90dca00812d4f86a9e6e..18bc1118efda4266df8fa313deef95719c17dd62 100644 --- a/wrap/python/ajax/protocol.txt +++ b/wrap/python/ajax/protocol.txt @@ -20,6 +20,7 @@ Choosing the desired output (pick one) o=m output monitor o=a output automaton o=r output run + o=t output testing automaton o=v3 output LTL3BA's version (no other argument needed) Type of formula output if o=f (pick one) @@ -49,6 +50,12 @@ Type of run output if o=r (pick one) rf=p print run as text rf=d draw run +Type of testing automaton if o=t (pick one) + + tf=t TA + tf=g GTA + tf=a TGTA + Translator algorithm (pick one) t=fm Couvreur/FM diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index ac54f4d60bdd992743ba3b8100d267c84acb0b2f..1c13bc8fee830b5e5b345abd714e2650cf1ca973 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -287,7 +287,10 @@ However you may download the 1: unbufprint("s") - count = automaton.number_of_acceptance_conditions() - if count > 0: - unbufprint(", %d acceptance condition" % count) - if count > 1: - unbufprint("s") - acc = automaton.all_acceptance_conditions() - unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc)) - else: - unbufprint(", no acceptance condition (all cycles are accepting)") + if hasattr(automaton, 'number_of_acceptance_conditions'): + count = automaton.number_of_acceptance_conditions() + if count > 0: + unbufprint(", %d acceptance condition" % count) + if count > 1: + unbufprint("s") + acc = automaton.all_acceptance_conditions() + unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc)) + else: + unbufprint(", no acceptance condition (all cycles are accepting)") unbufprint("

    \n") # Decide whether we will render the automaton or not. # (A webserver is not a computation center...) @@ -578,10 +582,15 @@ for s in form.getlist('as'): elif s == 'ds': direct_simul = True +ta_type = None +buchi_type = None + if output_type == 'a': buchi_type = form.getfirst('af', 't') elif output_type == 'r': buchi_type = form.getfirst('ra', 't') +elif output_type == 't': + ta_type = form.getfirst('tf', 't') else: unbufprint("Unkown output type 'o=%s'.\n" % output_type) automaton = 0 @@ -589,12 +598,18 @@ else: degen = False neverclaim = False -if buchi_type == 's': + +if buchi_type == 's' or ta_type == 't': degen = True elif buchi_type == 'i': degen = True neverclaim = True +if output_type == 't': + ta_type = form.getfirst('tf', 't') + if ta_type == 't': + degen = True + if prune_scc: # Do not suppress all useless acceptance conditions if # degeneralization or simulation is requested: keeping those that @@ -638,6 +653,23 @@ if output_type == 'a': automaton = 0 finish() +# Testing automaton Output +if output_type == 't': + propset = spot.atomic_prop_collect_as_bdd(f, automaton) + if ta_type == 'a': + tautomaton = spot.tgba_to_tgta(degen, propset) + tautomaton = spot.minimize_tgta(tautomaton) + else: + tautomaton = spot.tgba_to_ta(degen, propset, + False, False, False, False) + tautomaton = spot.minimize_ta(tautomaton) + dont_run_dot = print_stats(tautomaton) + render_automaton(tautomaton, dont_run_dot, False) + tautomaton = 0 + degen = 0 + automaton = 0 + finish() + # Buchi Run Output if output_type == 'r': diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 44b2b0966575b30c6ed661390d6aacc7d9259c76..83a9b6cc49e35480bbd50a59581bb544bcd84602 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -73,6 +73,7 @@ namespace std { #include "ltlvisit/simplify.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" +#include "ltlvisit/apcollect.hh" #include "tgba/bdddict.hh" #include "tgba/bddprint.hh" @@ -111,6 +112,15 @@ namespace std { #include "tgbaparse/public.hh" +#include "ta/ta.hh" +#include "ta/tgta.hh" +#include "ta/taexplicit.hh" +#include "ta/tgtaexplicit.hh" +#include "taalgos/tgba2ta.hh" +#include "taalgos/dotty.hh" +#include "taalgos/stats.hh" +#include "taalgos/minimize.hh" + using namespace spot::ltl; using namespace spot; %} @@ -176,6 +186,7 @@ using namespace spot; %include "ltlvisit/simplify.hh" %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" +%include "ltlvisit/apcollect.hh" %feature("new") spot::emptiness_check::check; %feature("new") spot::emptiness_check_instantiator::construct; @@ -197,6 +208,8 @@ using namespace spot; %feature("new") spot::simulation; %feature("new") spot::degeneralize; %feature("new") spot::tgba_parse; +%feature("new") spot::tgba_to_ta; +%feature("new") spot::tgba_to_tgta; // Help SWIG with namespace lookups. #define ltl spot::ltl @@ -261,6 +274,17 @@ using namespace spot; %include "tgbaparse/public.hh" +%include "ta/ta.hh" +%include "ta/tgta.hh" +%include "ta/taexplicit.hh" +%include "ta/tgtaexplicit.hh" +%include "taalgos/tgba2ta.hh" +%include "taalgos/dotty.hh" +%include "taalgos/stats.hh" +%include "taalgos/minimize.hh" + + + #undef ltl %extend spot::ltl::formula {