prodigy.analysis.evtinvariants.invariant_verification

Analyzer

Computes the semantics of instructions (compute_semantics).

alias of 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]]

evt_invariant_check(loop, prog_info, distribution, invariant, config, analyzer)[source]

Checks whether invariant is a fixed point of the EVT operator Ψ(I) = distribution + ⟦body⟧(⟨I⟩_guard), solving for the invariant’s parameters if needed.

Return type:

Tuple[Distribution, Distribution, List[Dict[str, str]]]

Returns:

the terminating part ⟨I⟩_¬guard, the invariant I itself (with the first solution substituted) and all solutions found.

Raises:

VerificationError – if the invariant cannot be validated.

Parameters:
evt_invariant_verification(loop, prog_info, distribution, invariant, config, analyzer)[source]

Like evt_invariant_check(), but returns only the terminating part.

Parameters:
Return type:

Distribution