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

* wrap/python/cgi-bin/ltl2tgba.in: Document W and M operators.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2010-04-12 16:10:45 +02:00
parent e6809b8c66
commit aa5426b2fb
2 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2010-04-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* wrap/python/cgi-bin/ltl2tgba.in: Document W and M operators.
2010-04-12 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-04-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
More LTL reductions for W and M. More LTL reductions for W and M.

13
wrap/python/cgi-bin/ltl2tgba.in
View file

@ -346,7 +346,7 @@ an identifier: <code>aUb</code> is an atomic proposition, unlike
<td align="right">not:</td><td><code>!</code></td> <td align="right">not:</td><td><code>!</code></td>
<td align="right">and:</td><td><code>&</code> <code>&&</code> <td align="right">and:</td><td><code>&</code> <code>&&</code>
<code>.</code> <code>/\</code></td> <code>.</code> <code>/\</code></td>
<td align="right">xor:</td><td><code>^</code> <code>xor</code></td> <td align="right">(strong) until:</td><td><code>U</code></td>
<td align="right">true:</td><td><code>1</code> <td align="right">true:</td><td><code>1</code>
<code>true</code></td> <code>true</code></td>
</tr> </tr>
@ -356,7 +356,7 @@ an identifier: <code>aUb</code> is an atomic proposition, unlike
<td align="right">or:</td><td><code>|</code> <code>||</code> <td align="right">or:</td><td><code>|</code> <code>||</code>
<code>+</code> <code>\/</code></td> <code>+</code> <code>\/</code></td>
<td align="right">until:</td><td><code>U</code></td> <td align="right">weak until:</td><td><code>W</code></td>
<td align="right">false:</td><td><code>0</code> <td align="right">false:</td><td><code>0</code>
<code>false</code></td> <code>false</code></td>
</tr> </tr>
@ -365,7 +365,7 @@ an identifier: <code>aUb</code> is an atomic proposition, unlike
<code>[]</code></td> <code>[]</code></td>
<td align="right">implies:</td><td><code>-&gt;</code> <td align="right">implies:</td><td><code>-&gt;</code>
<code>=&gt;</code></td> <code>=&gt;</code></td>
<td align="right">release:</td><td><code>R</code> <td align="right">(weak) release:</td><td><code>R</code>
<code>V</code></td> <code>V</code></td>
<td></td><td></td> <td></td><td></td>
</tr> </tr>
@ -373,10 +373,15 @@ an identifier: <code>aUb</code> is an atomic proposition, unlike
<td align="right">next:</td><td><code>X</code> <code>()</code></td> <td align="right">next:</td><td><code>X</code> <code>()</code></td>
<td align="right">equivalent:</td><td><code>&lt;-&gt;</code> <td align="right">equivalent:</td><td><code>&lt;-&gt;</code>
<code>&lt;=&gt;</code></td> <code>&lt;=&gt;</code></td>
<td align="right">strong release:</td><td><code>M</code></td>
<td></td><td></td>
</tr>
<tr>
<td></td><td></td>
<td align="right">xor:</td><td><code>^</code> <code>xor</code></td>
<td></td><td></td> <td></td><td></td>
<td></td><td></td> <td></td><td></td>
</tr> </tr>
</tbody> </tbody>
</table></td></tr></table>""" </table></td></tr></table>"""