The procedure expression that triggered task $event is $expr.
EventKind$event $kind
Event $event is of kind $kind (one of "DO", "ACHIEVE", "NEWFACT", or "UNKNOWN".
EventParent$event $procedureInstance
The procedure instance that triggered $event is $procedureInstance.
EventPosted$event
The event $event has been posted since (RecordingAllEvents) has become true.
ExprChild$parentExpr $childExpr
$parentExpr has $childExpr as a subexpression.
ExprVariable$expr $variable
$expr has $variable as a free variable.
FailureResult$result
$result indicates failure.
PICurrentExpr$procedureInstance $expr
Procedure instance $procedureInstance has $expr as its current step.
PICurrentSubgoal$procedureInstance $event
Procedure instance $procedureInstance has $event as a current subgoal.
PICurrentValue$procedureInstance $var $value
In $procedureInstance, the variable $var is bound to $value.
PIProcedure$procedureInstance $procedure
$procedureInstance is an instance of $procedure.
PITriggeringEvent$procedureInstance $event
Procedure instance $procedureInstance was triggered by $event.
RecordingAllEvents
SPARK is recording all events posted for later retrieval using EventPosted.
Conclude this to start recording, retract it to stop (and forget what was recorded).