B.12 Fluent and Assert

Fluents used in Linear Temporal Logic expressions are defined by two sets of action labels and an optional initialization expression that determines whether the fluent is initially true or false. The sets may be singletons, in which case a single action label may be defined. If initialization is omitted, by default, the fluent is initially false. A set of fluents may be declared using an index range.

 FluentDef:              fluent FluentIdent IndexRanges_opt                     =< ActionLabels, ActionLabels > Initially_opt Initially:               initially SimpleExpression

Example

 fluent Simple = <a,b> fluent Sets  = <{start,begin},{end,finish}> fluent Indexed[i:1..8]            = <a[i],b[i]> initially (i%2==0)

Assertions define properties expressed in Fluent Linear Temporal Logic (FLTL). Assertions are named FLTL formulae and they may be parameterized and used in the definition of more complex properties.

 AssertDef:              assert AssertIdent Param_opt = FLTLUnaryExpression FLTLOrExpr:              FLTLBinaryExpr              FLTLOrExpr || FLTLBinaryExpr FLTLBinaryExpr:              FLTLAndExpr              FLTLBinaryExpr U FLTLAndExpr    -- until              FLTLBinaryExpr W FLTLAndExpr    -- weak until              FLTLBinaryExpr -> FLTLAndExpr    -- implication              FLTLBinaryExpr <-> FLTLAndExpr  -- equivalence FLTLAndExpr:              FLTLUnaryExpr              FLTLAndExpr && FLTLUnaryExpr FLTLUnaryExpr:              FLTLBaseExpr              ! FLTLUnaryExpr    -- negation            X FLTLUnaryExpr    -- next time            <> FLTLUnaryExpr   -- eventually            [] FLTLUnaryExpr     -- always            forall Ranges FLTLUnaryExpr            exists Ranges FLTLUnaryExpr FLTLBaseExpr:              FluentIdent Ranges_opt              ActionLabels              AssertIdent Argument_opt            rigid SimpleExpression            ( FLTLOrExpr )

Uppercase identifiers in FLTL expressions refer either to fluent or assertion definitions. Lowercase identifiers refer to action labels. Where a set of action labels is used, this means the disjunction of the fluents representing each individual action as described in Chapter 14. The simple expression introduced by the keyword rigid is a boolean expression that must evaluate to either 0 false or 1 true.