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