Skip to content

Commit

Permalink
revert inequality
Browse files Browse the repository at this point in the history
  • Loading branch information
stefan-aws committed Mar 20, 2024
1 parent ef05f90 commit 07df18f
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions tests/Tests.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -32,15 +32,15 @@ module Tests {
var empiricalMean := empiricalSum / n as real;
var diff := RealArith.Abs(empiricalMean - trueMean);
var threshold := 4.0 * 4.0 * trueVariance / n as real;
if diff * diff >= threshold {
if diff * diff > threshold {
print "Test failed: ", description, "\n";
print "True mean: ", trueMean, "\n";
print "Empirical mean: ", empiricalMean, "\n";
print "Difference between empirical and true mean: ", diff, "\n";
print "squared difference: ", diff * diff, "\n";
print "sigma squared: ", trueVariance / n as real, "\n";
}
expect diff * diff < threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5.";
expect diff * diff <= threshold, "Empirical mean should be within 3 sigma of true mean. This individual test may fail with probability of about 6.3e-5.";
}

method TestUniformPowerOfTwo(n: nat, u: nat, r: DafnyVMC.Random)
Expand Down

0 comments on commit 07df18f

Please sign in to comment.