pub fn reachability_step<F>(
    set: &mut GraphColoredVertices,
    universe: &GraphColoredVertices,
    variables: &[VariableId],
    step: F,
) -> bool
where F: Fn(VariableId, &GraphColoredVertices) -> GraphColoredVertices,
Expand description

Performs one reachability step using the saturation scheme.

The universe is an upper bound on what elements can be added to the set. Using variables you can restrict the considered transitions. Finally, step implements update in one variable.

Returns true if fixpoint has been reached.