pub fn extract_state_predicates(expr: &TLExpr) -> HashSet<String>
Extract state predicates (non-temporal atomic propositions).
Useful for model checking to identify the atomic propositions that need to be evaluated in each state.