Commit 852cd0d5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltl2tgba.html: Add testing automata options.

* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt,
wrap/python/ajax/ Here.
parent 27a2de33
......@@ -70,23 +70,48 @@
$("#ltl3ba-U").attr('checked', true);
$("#to-s").change(function() {
if ($(this).is(':checked')) {
$("#to-l").change(function() {
if ($(this).is(':checked')) {
$("#tf-t,#tf-g").change(function() {
if ($(this).is(':checked')) {
$("#tf-a").change(function() {
if ($(this).is(':checked')) {
$("#to-l,#to-s").attr('disabled', true);
function hideOrShowPanels(output, duration) {
switch (output)
case 'f':
case 'm':
case 'a':
case 't':
case 'r':
......@@ -125,7 +150,7 @@
$.spotvars.autoupdate = true;
$.spotvars.internalchange = false;
var o = $('input[name="o"]').val();
......@@ -506,17 +531,17 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<div id="tabs-ot">
Translate the (simplified) formula as:<br>
Translate the (simplified) formula into a Büchi automaton, and then convert it into:<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">
<INPUT id="tf-t" type="radio" name="tf" value="t">
a Testing Automaton (TA)
<label class="rtip" title="GTA are testing automata extended with multiple Büchi acceptance conditions.">
<INPUT type="radio" name="tf" value="g">
<INPUT id="tf-g" type="radio" name="tf" value="g">
a Generalized Testing Automaton (GTA)
<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>
<INPUT id="tf-a" type="radio" name="tf" value="a" checked>
a Transition-based Generalized Testing Automaton (TGTA)
......@@ -644,6 +669,23 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="text" maxlength="40" name="eo" value="">
<div id="tester-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
<h3 class="ui-widget-header ui-corner-all head">Testing Automaton Options<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
<label class="rtip" title="Divert all livelock accepting paths to a single livelock acceptance state.">
<INPUT id="to-l" type="checkbox" name="to" value="l">
use a catch-all livelock state
<label class="rtip" title="Ensure that all livelock accepting states are also Büchi-accepting, so that the testing automaton can be tested for emptiness in a single pass.">
<INPUT id="to-s" type="checkbox" name="to" value="s" checked>
produce a single-pass testing automaton
<label class="rtip" title="Merge bisimilar states in the final testing automaton.">
<INPUT type="checkbox" name="to" value="m" checked>
merge bisimilar states
<div id="results" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
<h3 id="results-head" class="ui-widget-header ui-corner-all head">Results<span class="ui-icon ui-icon-circle-arrow-n restip">Fold</span></h3>
......@@ -100,6 +100,12 @@ Automaton simplifications (pick many)
as=wd WDBA minimiztion
as=ds Direct Simulation reduction
Testing Automaton options (pick many)
to=l add a catch-all livelock state
to=s produce single-pass variant
to=m merge bisimilar states
Global options
g=8 Enable UTF-8 output.
......@@ -655,16 +655,29 @@ if output_type == 'a':
# Testing automaton Output
if output_type == 't':
livelock = False
singlepass = False
bisimulation = False
for to in form.getlist('to'):
if to == 'l':
livelock = True
elif to == 's':
singlepass = True
elif to == 'm':
bisimulation = True
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)
if bisimulation:
tautomaton = spot.minimize_tgta(tautomaton)
issba = False
tautomaton = spot.tgba_to_ta(degen, propset,
False, False, False, False)
tautomaton = spot.minimize_ta(tautomaton)
issba, True, singlepass, livelock)
if bisimulation:
tautomaton = spot.minimize_ta(tautomaton)
dont_run_dot = print_stats(tautomaton)
render_automaton(tautomaton, dont_run_dot, False)
render_automaton(tautomaton, dont_run_dot, issba)
tautomaton = 0
degen = 0
automaton = 0
Supports Markdown
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