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

Document the new operators in the on-line tools.

Browse source 
* wrap/python/ajax/ltl2tgba.html: Mention Goal's ~, -->, and <-->
operators.
* wrap/python/cgi-bin/ltl2tgba.in: Likewise.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-06 17:36:26 +01:00
parent c019a44c49
commit caaf0a80c2
3 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -197,7 +197,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
</thead>
<tbody>
<tr>
<td align="right">not:</td><td><span class="formula">!</span></td>
<td align="right">not:</td><td><span class="formula">!</span> <span class="formula">~</span></td>
<td align="right">and:</td><td><span class="formula">&</span> <span class="formula">&&</span>
<span class="formula">.</span> <span class="formula">/\</span></td>
<td align="right">(strong) until:</td><td><span class="formula">U</span></td>
@ -216,8 +216,9 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
</tr>
<tr>
<td align="right">always:</td><td><span class="formula">G</span>
<span class="formula">[]</span></td>
<span class="formula">[]</span></td>
<td align="right">implies:</td><td><span class="formula">-&gt;</span>
<span class="formula">--&gt;</span>
<span class="formula">=&gt;</span></td>
<td align="right">(weak) release:</td><td><span class="formula">R</span>
<span class="formula">V</span></td>
@ -226,6 +227,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<tr>
<td align="right">next:</td><td><span class="formula">X</span> <span class="formula">()</span></td>
<td align="right">equivalent:</td><td><span class="formula">&lt;-&gt;</span>
<span class="formula">&lt;--&gt;</span>
<span class="formula">&lt;=&gt;</span></td>
<td align="right">strong release:</td><td><span class="formula">M</span></td>
<td></td><td></td>