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

Update the help text for the Couvreur/FM algorithm.

Browse source 
* wrap/python/ajax/ltl2tgba.html: Mention PSL.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-09 13:15:46 +02:00
parent b71eadd8e3
commit 2945668021
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -466,7 +466,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<div id="translator-tabs" class="tabs collapsible shadow">
<ul class="head">
<li>Translator Algorithm:</li>
<li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton. (This is the best algorithm of the three.)">Couvreur/FM</a></li>
<li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton. This is the best algorithm of the three, and the only one that has been extended to support PSL operators.">Couvreur/FM</a></li>
<li><a href="#tabs-tla" class="btip" title="Builds a purely symbolic automaton, using BDDs to encode the transition relation. The translation itself is fast (it uses a number of BDD operations that is linear in the size of the formula), but the resulting symbolic encoding is better used symbolically. If you develop it explicitly (e.g. to draw it, as on this page) the result can easily have an exponential number of states.">Couvreur/LaCIM</a></li>
<li><a href="#tabs-tta" class="btip" title="An implementation of Heikki Tauriainen's Ph.D. thesis algorithm to translate LTL formulas via very weak alternating automata with transition-based generalized acceptance conditions.">Tauriainen/TAA</a></li>
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>