Commit 27a2de33 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

ltl2tgba.html: Preliminary support for TA

* wrap/python/spot.i: Add wrapper the new TA algorithms.
* wrap/python/ajax/ltl2tgba.html: Add a testing automaton tab.
* wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Support it.
parent 20c3f9f8
...@@ -439,6 +439,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike ...@@ -439,6 +439,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<li><a href="#tabs-om" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li> <li><a href="#tabs-om" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
<li><a href="#tabs-oa" class="btip" title="Translate the LTL formula into B&uuml;chi automaton.">B&uuml;chi Automaton</a></li> <li><a href="#tabs-oa" class="btip" title="Translate the LTL formula into B&uuml;chi automaton.">B&uuml;chi Automaton</a></li>
<li><a href="#tabs-or" class="btip" title="Translate the LTL formula into B&uuml;chi automaton, and exhibit an accepting run.">B&uuml;chi Run</a></li> <li><a href="#tabs-or" class="btip" title="Translate the LTL formula into B&uuml;chi automaton, and exhibit an accepting run.">B&uuml;chi Run</a></li>
<li><a href="#tabs-ot" class="btip" title="Translate the LTL formula into a Testing Automaton, or some variant.">Testing Automaton</a></li>
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li> <li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
</ul> </ul>
<input type="hidden" name="o"> <input type="hidden" name="o">
...@@ -504,6 +505,21 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike ...@@ -504,6 +505,21 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
draw an accepting run on top of the automaton draw an accepting run on top of the automaton
</label><br> </label><br>
</div> </div>
<div id="tabs-ot">
Translate the (simplified) formula as:<br>
<label class="rtip" title="Instead of reading valuations of all atomic propositions testing automata only watch the changes to these valuation. A transitions labeled by <span class='formula'>a</span> may be crossed only if these atomic proposition change in the system. Additionally, testing automata have two acceptance conditions: states can be Büchi accepting or livelock accepting (or both, or none).">
<INPUT type="radio" name="tf" value="t">
a Testing Automaton (TA)
</label><br>
<label class="rtip" title="GTA are testing automata extended with multiple Büchi acceptance conditions.">
<INPUT type="radio" name="tf" value="g">
a Generalized Testing Automaton (GTA)
</label><br>
<label class="rtip" title="TGTA are similar to TGBA except instead of reading valuations of all atomic propositions testing automata only watch the changes to these valuation. They have multiple Büchi acceptance conditions on transitions, but no livelock acceptance.">
<INPUT type="radio" name="tf" value="a" checked>
a Transition-based Generalized Testing Automaton (TGTA)
</label><br>
</div>
</div> </div>
</div> </div>
<div id="translator-tabs" class="tabs collapsible shadow"> <div id="translator-tabs" class="tabs collapsible shadow">
......
...@@ -20,6 +20,7 @@ Choosing the desired output (pick one) ...@@ -20,6 +20,7 @@ Choosing the desired output (pick one)
o=m output monitor o=m output monitor
o=a output automaton o=a output automaton
o=r output run o=r output run
o=t output testing automaton
o=v3 output LTL3BA's version (no other argument needed) o=v3 output LTL3BA's version (no other argument needed)
Type of formula output if o=f (pick one) Type of formula output if o=f (pick one)
...@@ -49,6 +50,12 @@ Type of run output if o=r (pick one) ...@@ -49,6 +50,12 @@ Type of run output if o=r (pick one)
rf=p print run as text rf=p print run as text
rf=d draw run 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) Translator algorithm (pick one)
t=fm Couvreur/FM t=fm Couvreur/FM
......
...@@ -287,7 +287,10 @@ However you may download the <a href="''' + cgi.escape(autprefix) ...@@ -287,7 +287,10 @@ However you may download the <a href="''' + cgi.escape(autprefix)
def render_automaton(automaton, dont_run_dot, issba, deco = None): def render_automaton(automaton, dont_run_dot, issba, deco = None):
dotsrc = spot.ostringstream() dotsrc = spot.ostringstream()
spot.dotty_reachable(dotsrc, automaton, issba, deco) if isinstance(automaton, spot.ta):
spot.dotty_reachable(dotsrc, automaton)
else:
spot.dotty_reachable(dotsrc, automaton, issba, deco)
render_dot_maybe(dotsrc.str(), dont_run_dot) render_dot_maybe(dotsrc.str(), dont_run_dot)
def render_formula(f): def render_formula(f):
...@@ -303,15 +306,16 @@ def print_stats(automaton): ...@@ -303,15 +306,16 @@ def print_stats(automaton):
unbufprint(", %d transition" % stats.transitions) unbufprint(", %d transition" % stats.transitions)
if stats.transitions > 1: if stats.transitions > 1:
unbufprint("s") unbufprint("s")
count = automaton.number_of_acceptance_conditions() if hasattr(automaton, 'number_of_acceptance_conditions'):
if count > 0: count = automaton.number_of_acceptance_conditions()
unbufprint(", %d acceptance condition" % count) if count > 0:
if count > 1: unbufprint(", %d acceptance condition" % count)
unbufprint("s") if count > 1:
acc = automaton.all_acceptance_conditions() unbufprint("s")
unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc)) acc = automaton.all_acceptance_conditions()
else: unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc))
unbufprint(", no acceptance condition (all cycles are accepting)") else:
unbufprint(", no acceptance condition (all cycles are accepting)")
unbufprint("</p>\n") unbufprint("</p>\n")
# Decide whether we will render the automaton or not. # Decide whether we will render the automaton or not.
# (A webserver is not a computation center...) # (A webserver is not a computation center...)
...@@ -578,10 +582,15 @@ for s in form.getlist('as'): ...@@ -578,10 +582,15 @@ for s in form.getlist('as'):
elif s == 'ds': elif s == 'ds':
direct_simul = True direct_simul = True
ta_type = None
buchi_type = None
if output_type == 'a': if output_type == 'a':
buchi_type = form.getfirst('af', 't') buchi_type = form.getfirst('af', 't')
elif output_type == 'r': elif output_type == 'r':
buchi_type = form.getfirst('ra', 't') buchi_type = form.getfirst('ra', 't')
elif output_type == 't':
ta_type = form.getfirst('tf', 't')
else: else:
unbufprint("Unkown output type 'o=%s'.\n" % output_type) unbufprint("Unkown output type 'o=%s'.\n" % output_type)
automaton = 0 automaton = 0
...@@ -589,12 +598,18 @@ else: ...@@ -589,12 +598,18 @@ else:
degen = False degen = False
neverclaim = False neverclaim = False
if buchi_type == 's':
if buchi_type == 's' or ta_type == 't':
degen = True degen = True
elif buchi_type == 'i': elif buchi_type == 'i':
degen = True degen = True
neverclaim = True neverclaim = True
if output_type == 't':
ta_type = form.getfirst('tf', 't')
if ta_type == 't':
degen = True
if prune_scc: if prune_scc:
# Do not suppress all useless acceptance conditions if # Do not suppress all useless acceptance conditions if
# degeneralization or simulation is requested: keeping those that # degeneralization or simulation is requested: keeping those that
...@@ -638,6 +653,23 @@ if output_type == 'a': ...@@ -638,6 +653,23 @@ if output_type == 'a':
automaton = 0 automaton = 0
finish() 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 # Buchi Run Output
if output_type == 'r': if output_type == 'r':
......
...@@ -73,6 +73,7 @@ namespace std { ...@@ -73,6 +73,7 @@ namespace std {
#include "ltlvisit/simplify.hh" #include "ltlvisit/simplify.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "ltlvisit/tunabbrev.hh" #include "ltlvisit/tunabbrev.hh"
#include "ltlvisit/apcollect.hh"
#include "tgba/bdddict.hh" #include "tgba/bdddict.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
...@@ -111,6 +112,15 @@ namespace std { ...@@ -111,6 +112,15 @@ namespace std {
#include "tgbaparse/public.hh" #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::ltl;
using namespace spot; using namespace spot;
%} %}
...@@ -176,6 +186,7 @@ using namespace spot; ...@@ -176,6 +186,7 @@ using namespace spot;
%include "ltlvisit/simplify.hh" %include "ltlvisit/simplify.hh"
%include "ltlvisit/tostring.hh" %include "ltlvisit/tostring.hh"
%include "ltlvisit/tunabbrev.hh" %include "ltlvisit/tunabbrev.hh"
%include "ltlvisit/apcollect.hh"
%feature("new") spot::emptiness_check::check; %feature("new") spot::emptiness_check::check;
%feature("new") spot::emptiness_check_instantiator::construct; %feature("new") spot::emptiness_check_instantiator::construct;
...@@ -197,6 +208,8 @@ using namespace spot; ...@@ -197,6 +208,8 @@ using namespace spot;
%feature("new") spot::simulation; %feature("new") spot::simulation;
%feature("new") spot::degeneralize; %feature("new") spot::degeneralize;
%feature("new") spot::tgba_parse; %feature("new") spot::tgba_parse;
%feature("new") spot::tgba_to_ta;
%feature("new") spot::tgba_to_tgta;
// Help SWIG with namespace lookups. // Help SWIG with namespace lookups.
#define ltl spot::ltl #define ltl spot::ltl
...@@ -261,6 +274,17 @@ using namespace spot; ...@@ -261,6 +274,17 @@ using namespace spot;
%include "tgbaparse/public.hh" %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 #undef ltl
%extend spot::ltl::formula { %extend spot::ltl::formula {
......
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