compute_prob01_states

compute_prob01_states(
model,
property: Property,
) → tuple[BitVector, BitVector]

Compute the states satisfying a reachability or until property with probability 0 and with probability 1.

The property has the form F psi or phi U psi (unbounded), optionally within a probability operator, e.g. Pmax=? [F "goal"]. The computation is purely graph-based. For nondeterministic models, the probability operator must specify the optimization direction, e.g. Pmax=? [F "goal"].

Parameters:

  • model – Sparse model.

  • property – Property (or formula) describing the reachability or until objective.

Returns:

Tuple (prob0, prob1) of the states with probability 0 and with probability 1.