prodigy.analysis.evtinvariants.invariant_synthesis

evt_invariant_synthesis(loop, prog_info, distribution, config, strategy, analyzer)

Parameters:

• loop (WhileInstr)

• prog_info (ProgramInfo)

• distribution (Distribution)

• config (ForwardAnalysisConfig)

• strategy (SynthesisStrategy)

• 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:

List[Tuple[Distribution, bool | None]]