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

Apply Jan's comments on ltl3ba's interface.

Browse source 
* wrap/python/ajax/ltl2tgba.html: Adjust text.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-14 19:57:03 +02:00
parent 5c04022505
commit b0193e1418
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -559,11 +559,11 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="checkbox" name="l3" value="l" checked> <INPUT type="checkbox" name="l3" value="l" checked>
LTL simplifications LTL simplifications
</label><br> </label><br>
<label class="rtip" title="See next tooltip for an explanation of suspension. This version disables suspension in the intermediate alternating automaton, where it is only used for one step."> <label class="rtip" title="See next tooltip for an explanation of suspension. LTL3BA supports suspension also in the construction of an intermediate alternating automaton, where it is only used for one step.">
<INPUT type="checkbox" name="l3" value="A" checked> <INPUT type="checkbox" name="l3" value="A" checked>
suspension in alternating automaton suspension in alternating automaton
</label><br> </label><br>
<label class="rtip" title="Suspension is a technique to postpone the verification of some subformulae. Any easy way to picture it is to look at the formula <span class='formula'>F(a)&amp;GF(b)</span>: the <span class='formula'>GF(b)</span> part does not need to be checked before some <span class='formula'>a</span> has been seen. On this example, suspension amounts to translating <span class='formula'>F(a&amp;GF(b))</span> but the technique is more general than such LTL rewritings."> <label class="rtip" title="Suspension is a technique to postpone the verification of some subformulae. An easy way to picture it is to look at the formula <span class='formula'>F(a)&amp;GF(b)</span>: the <span class='formula'>GF(b)</span> part does not need to be checked before some <span class='formula'>a</span> has been seen. On this example, suspension amounts to translating <span class='formula'>F(a&amp;GF(b))</span> but the technique is more general than such LTL rewritings.">
<INPUT type="checkbox" name="l3" value="P" checked> <INPUT type="checkbox" name="l3" value="P" checked>
suspension in TGBA suspension in TGBA
</label><br> </label><br>