Skip to main content

extract_error_formula

taco_model_checker::internal_spec::extraction

Function extract_error_formula 

Source 
fn extract_error_formula(
    expr: NonNegatedELTLExpression,
) -> Result<ErrorFormula, ExtractionError>
Expand description

Error formula of an ELTL formula without negations

Temporal operators at the top level become targets. Atoms at the top level restrict the initial configuration. && distributes over the disjunction of atoms. Atoms of one || are merged where a sound merge exists.