From 1d724beabd04ea2deb8f7da827c98e4b5445fc23 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 19 Jan 2015 14:38:09 +0100 Subject: [PATCH] ltl2tgba.html: document [:*i..j] For issue #51. * wrap/python/ajax/ltl2tgba.html: Here. --- wrap/python/ajax/ltl2tgba.html | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 8042709ed..765f5253f 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -343,7 +343,7 @@ an identifier: aUb is an atomic proposition, unlike Constants - Unary operators (prefix) + Unary operators Binary operators (infix) @@ -400,10 +400,10 @@ an identifier: aUb is an atomic proposition, unlike - SERE ε:[*0] - Kleene star:[*] [*i..j] + Kleene star:[*] [+] [*i..j] concatenation:; fusion:: @@ -419,20 +419,26 @@ an identifier: aUb is an atomic proposition, unlike union:| || + \/ + + + iterated fusion:[:*] [:+] [:*i..j] + + + PSL weak closure:{s} - ∀-suffix impl.:{s}[]->p
{s}|->p
{s}(p) - NO ∀-suffix impl.:{s}[]=>p
{s}|=>p + triggers:{s}[]->p
{s}|->p
{s}(p) + Non-Ov. trigger:{s}[]=>p
{s}|=>p strong closure:{s}! - ∃-suffix impl.:{s}<>->p - NO ∃-suffix impl.:{s}<>=>p + seq:{s}<>->p + Non-Ov. seq:{s}<>=>p