Skip to main content

extract_from_inner_eventually_helper

Function extract_from_inner_eventually_helper 

Source
fn extract_from_inner_eventually_helper(
    expr: NonNegatedELTLExpression,
    ev_not_in_conj: bool,
) -> Result<Disjunction<ErrorTarget>, ExtractionError>
Expand description

Extract the targets of an ELTL formula that is inside an outer <>

The result is a disjunction of Reach and Repeat targets. ev_not_in_conj is true if until now, constraints inside the eventually have not yet appeared in a conjunction. Only then can we apply distributivity and remove nested <>