diff --git a/wrap/python/ajax/css/ltl2tgba.css b/wrap/python/ajax/css/ltl2tgba.css index 51d5b6951..9937c9514 100644 --- a/wrap/python/ajax/css/ltl2tgba.css +++ b/wrap/python/ajax/css/ltl2tgba.css @@ -56,6 +56,21 @@ div.ltl2tgba { z-index:1; } +.ltldoc { + text-align: right; +} + +table.ltltable +{ + border-collapse:collapse; + font-size: 90%; +} + +.ltldocrow { + font-weight: bold; + vertical-align:top; +} + .ltl2tgba div.ui-widget-content { padding: 3px; margin: 2px 0px; diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 49efa0ce5..5d51945c1 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -228,7 +228,7 @@

-

LTL Formula to translateFold

+

LTL (or PSL) Formula to translateFold

Send
@@ -241,64 +241,108 @@ to refer to GFa as a proposition.
Conversely, in letter operators are not assumed to be operators if they are part of an identifier: aUb is an atomic proposition, unlike a U b and (a)U(b).

-
- +
+ - - + + + - - - - - + + + + + + - - - - - - - - - - - - - - - - + + + - + + + + + + + + + + + + + + + + + + + + + + -
Unary operators
(prefix)		Binary operators
(infix)		 ConstantsUnary operators (prefix)Binary operators (infix)
not:! ~and:& && - /\(strong) until:Utrue:1 - true
Booleanfalse:0 falsenot:! ~and:& && + /\implies:-> + --> + =>
eventually:F - <>or:| || - + \/weak until:Wfalse:0 - false
always:G - []implies:-> - --> - =>(weak) release:R - V
next:X ()equivalent:<-> - <--> - <=>strong release:Mtrue:1 true or:| || + + \/equivalent:<-> + <--> + <=>
xor:^ xorxor:xor ^
LTLeventually:F + <>(strong) until:Uweak until:W
always:G + [](weak) release:R + Vstrong release:M
next:X ()
+ + + SERE + ε:[*0] + Kleene star:[*] [*i..j] + concatenation:; + fusion:: + + + + goto:[->i..j] + intersection:&& /\ + NLM and:& + + + + nonconsec. rep.:[=i..j] + union:| || + \/ + + + + + + PSL + + weak closure:{s} + ∀-suffix impl.:{s}[]->p
{s}|->p
{s}(p) + NO ∀-suffix impl.:{s}[]=>p
{s}|=>p + + + + strong closure:{s}! + ∃-suffix impl.:{s}<>->p + NO ∃-suffix impl.:{s}<>=>p + + +