Probabilistic B (pB) [2,8] extends classical B  to incorporate probabilistic updates together with the specification of quantitative safety properties. As for classical B, probabilistic B formulates safety as inductive invariants which can be checked mechanically relative to the program code. In the case that the invariants cannot be shown to be inductive, classical B uses model checking to allow experimental investigation, returning a counterexample execution trace in the case that the safety condition is violated. In this paper we introduce YAGA which provides similar support for probabilistic B and quantitative safety specifications. YAGA automatically interprets quantitative safety and the pB machine as a model checking problem to investigate the presence of counterexamples. Since inductive invariants characterise a strong form of safety, we are able to identify the specific point at which failure occurs as individual counterexample traces, which can then be ranked for importance, for example according to the probability of occurrence.