Fluent
fluent

fluent FL = <{s1,…sn}, {e1..en}> initially B defines a  fluent FL that is initially true if the expression B is true and initially false if the expression B is false. FL becomes true immediately any of the initiating actions {s1,…sn}occur and false immediately any of the terminating actions {e1..en} occur. If the term initially B is omitted then FL is initially false.

Assertion
assert

assert PF = FLTL_Expression defines an FLTL property.

&&

conjunction    (and)

||

disjunction     (or)

!

negation         (not)

->

implication   ((A->B)≡ (!A || B))

<->

equivalence   ((A<->B) ≡(A->B)&&(B->A))

next time X F

iff F holds in the next instant.

always []F

iff F holds now and always in the future.

eventually <>F

iff F holds at some point in the future.

until P U Q

iff Q holds at some point in the future and P holds until then.

weak until P W Q

iff P holds indefinitely or P U Q

forall

forall [i:R] FL(i) conjunction of FL(i)

exists

exists [i:R] FL(i) disjunction of FL(i)