prodigy.analysis.instructionhandler.while_handler

While loops.

The handler asks the current AnalysisSession which loop strategy to use for a loop and runs it. The six historic strategies are implemented and registered here; in the interactive CLI they show up in the same menu, with the same prompts, as before.

exception UnsupportedLoopError[source]

Bases: ForwardAnalysisError

The chosen strategy cannot handle this loop (e.g. EVT reasoning with conditioning).

exception InvariantRefutedError(message, details=None)[source]

Bases: VerificationError

A proposed invariant is not an invariant; details holds the evidence.

Parameters:
finite_mass(invariant, variables)[source]

Decides |I| < ∞ for a generating function I with non-negative coefficients.

Substitutes t for every variable; f(t) = I(t, …, t) has the same mass. For a rational f with f’s denominator q(0) ≠ 0, Pringsheim’s theorem says the radius of convergence is a singularity on the positive axis, so |I| < ∞ iff q has no root in (0, 1]; then |I| = f(1). Returns (None, None) when this cannot be decided (parameters, non-rational).

Parameters:
Return type:

Tuple[bool | None, Expr | None]

class WhileHandler[source]

Bases: InstructionHandler

static compute(instruction, prog_info, distribution, error_prob, config, analyzer)[source]

Computes the updated distribution after executing the instruction instruction on input distribution

Parameters:

  • instruction (SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery)

  • prog_info (Program)

  • distribution (Distribution)

  • error_prob (Distribution)

  • config (ForwardAnalysisConfig)

  • analyzer (Callable[[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery | Sequence[SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery], ProgramInfo, Distribution, Distribution, ForwardAnalysisConfig], Tuple[Distribution, Distribution]])

Return type:

tuple[Distribution, Distribution]