Skip to main content

extract_from_inner_globally_helper

Function extract_from_inner_globally_helper 

Source
fn extract_from_inner_globally_helper(
    expr: NonNegatedELTLExpression,
    appears_in_conj: bool,
) -> Result<ErrorTarget, ExtractionError>
Expand description

Helper function to extract the target of an ELTL formula that appears inside of an outer []

The result is an Invariant or a Repeat target. appears_in_conj specifies whether inner constraints have until now only appeared in a conjunction. Only if this is the case, distributivity holds and an inner globally operator can be parsed as a simple conjunct