prodigy.analysis.equivalence.equivalence_check¶
- generate_equivalence_test_distribution(program, config)[source]¶
Generates a second-order PGF, dependent on the given variables in a program. This SOP can be used to check equivalences of two programs.
- Parameters:
program (
Program)config (
ForwardAnalysisConfig)
- Return type:
Tuple[Distribution,Dict[str,str]]
- check_equivalence(program, other_program, config, analyzer)[source]¶
This method uses the fact that we can sometimes determine program equivalence, by checking the equality of two parametrized infinite-state Distributions.
If they are equivalent, also returns a list of constraints under which this holds (which may be empty if they are always equal). If not, also returns a counterexample. If the solution cannot be determined (returns None), also returns the difference of the second order distributions generated by the invariant and the once unrolled while loop of the program. If this difference can be made equal to 0, the programs are equivalent. :type config:
ForwardAnalysisConfig:param config: The configuration. :type program:Program:param program: The first program :type other_program:Program:param other_program: The second program :type 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]] :param analyzer: :params analyzer: The analyzer.