Function check_liveness 

pub fn check_liveness(
    init: &VerifyExpr,
    transition: &VerifyExpr,
    fairness: &[VerifyExpr],
    property: &VerifyExpr,
    max_k: u32,
) -> LivenessResult

Check a liveness property via bounded search.

The property should be the “eventually” part of G(F(property)). Fairness constraints are additional conditions that must hold infinitely often.