Pex - test case 6 (revisited)

Hello,

In the previous case I tried to come up with a scenario where a method takes a "complex" type instead of primitive types like integers of booleans. The exercise didn't go as expected. By the way , the latest downloadable version of Pex is 0.6.30728.0

To see whether pex still works on a method with primitive types, I re-wrote the method as follows.

  public PensionContribution DeterminePensionContribution2(
             uint aSalary, 
             uint aAge, 
             uint aServiceYears, 
             Contract aTypeContract)
        {
            //no pre-codition checks ....

            PensionContribution contribution = new PensionContribution();

            if (aSalary <= 3000)
            {
                if (aAge < 45)
                {
                    if (aTypeContract == Contract.FullTime)
                    {
                        contribution.BaseContribution = 80;
                        contribution.SupplementaryContribution = 15;
                    }
                    else
                    {
                        contribution.BaseContribution = 80;
                        contribution.SupplementaryContribution = 0;
                    }
                }
                else
                {
                    if (aServiceYears < 5)
                    {
                        contribution.BaseContribution = 80;
                        contribution.SupplementaryContribution = 15;
                    }
                    else
                    {
                        contribution.BaseContribution = 80;
                        contribution.SupplementaryContribution = 25;
                    }
                }
            }
            else
            {
                if (aAge < 45)
                {
                    if (aServiceYears < 5)
                    {
                        contribution.BaseContribution = 135;
                        contribution.SupplementaryContribution = 30;
                    }
                    else
                    {
                        if (aTypeContract == Contract.FullTime)
                        {
                            contribution.BaseContribution = 135;
                            contribution.SupplementaryContribution = 25;
                        }
                        else
                        {
                            contribution.BaseContribution = 135;
                            contribution.SupplementaryContribution = 20;
                        }
                    }
                }
                else
                {
                    if (aServiceYears < 5)
                    {
                        contribution.BaseContribution = 135;
                        contribution.SupplementaryContribution = 30;
                    }
                    else
                    {
                        contribution.BaseContribution = 135;
                        contribution.SupplementaryContribution = 20;

                    }
                }

            }
            return contribution;
        }

The PUT method looks like this.

      [PexMethod]
        public void PUTDeterminePensionContribution(
            [PexAssumeUnderTest]EmployeeServices target,
            uint aSalary,
            uint aAge,
            uint aServiceYears,
            Contract aTypeContract
        )
        {
            PexAssume.IsTrue(aAge > 18 && aAge < 75);
            PexAssume.IsTrue(aServiceYears > 0 && aServiceYears < 50);
            PexAssume.IsTrue(aSalary > 1400 && aSalary < 10000);
            PexAssume.IsTrue(aTypeContract == Contract.FullTime || aTypeContract == Contract.PartTime);

            PensionContribution result = target.DeterminePensionContribution
                (aSalary, aAge, aServiceYears, aTypeContract);
            PexValue.AddForValidation("BaseContribution", result.BaseContribution);
            PexValue.AddForValidation("SupplementaryContribution", result.SupplementaryContribution);

            if (aSalary <= 3000)
                Assert.IsTrue(result.BaseContribution == 80);
            if (aSalary > 3000)
                Assert.IsTrue(result.BaseContribution == 135);
            if (aSalary <= 3000 && aAge >= 45 && aServiceYears < 5)
                Assert.IsTrue(result.SupplementaryContribution == 15);
            if (aSalary <= 3000 && aAge < 45 && aTypeContract == Contract.FullTime)
                Assert.IsTrue(result.SupplementaryContribution == 15);
            if (aSalary <= 3000 && aAge >= 45 && aServiceYears >= 5)
                Assert.IsTrue(result.SupplementaryContribution == 25);
            if (aSalary > 3000 && aAge < 45 && aServiceYears >= 5 && aTypeContract == Contract.FullTime)
                Assert.IsTrue(result.SupplementaryContribution == 25);
            if (aSalary > 3000 && aAge < 45 && aServiceYears >= 5 && aTypeContract == Contract.PartTime)
                Assert.IsTrue(result.SupplementaryContribution == 20);
            if (aSalary > 3000 && aAge >= 45 && aServiceYears >= 5)
                Assert.IsTrue(result.SupplementaryContribution == 20);
            if (aSalary > 3000 && aServiceYears < 5)
                Assert.IsTrue(result.SupplementaryContribution == 30);
        }

In no time Pex finds the test cases for full block coverage

target	aSalary	aAge	aServiceYears	aTypeContract	BaseContribution	SupplementaryContribution	Summary/Exception	Error Message
1	...	8192	64	2	FullTime	135	30
2	...	8192	64	30	FullTime	135	20
3	...	8192	31	2	FullTime	135	30
4	...	8192	31	30	FullTime	135	25
5	...	1532	64	2	FullTime	80	15
6	...	1532	64	30	FullTime	80	25
7	...	1532	31	2	FullTime	80	15
8	...	8192	64	2	PartTime	135	30
9	...	1532	31	2	PartTime	80	0
10	...	8192	31	30	PartTime	135	20

So there is nothing "wrong" with the method under test. The problem when you investigate the output window, lies maybe in the calculation of the "age" and "serviceYears" properties.

00:00:00.0> starting execution
  00:00:00.0> reflecting tests
  00:00:00.3> TestProject1
    00:00:00.3> EmployeeTest
      00:00:00.3> DeterminePensionContributionIntern(Employee)
         maxconstraintsolvertime - 1s (constraint solver time out after 1 seconds)
        [execution]     4 runs
        [execution]    15 runs
        [test] (run 20) DeterminePensionContribution
        [test] (run 21) DeterminePensionContribution
        [execution]    21 runs, 49/81 blocks covered
        [test] (run 25) DeterminePensionContribution
        [execution]    29 runs, 49/81 blocks covered
        [execution]    41 runs, 49/81 blocks covered
        [modelsearch] could not flip 2 branches in a row
        [execution]    50 runs, 49/81 blocks covered
        [execution] imprecision at testingPEX.Employee.differenceInYears, offset 0x26
        [modelsearch] could not flip 4 branches in a row
        [execution]    77 runs (97,40% unique paths), 49/81 blocks covered
         timeout - 120s
         Timeout, 1 times
         MaxConstraintSolverTime, 60 times
        [coverage] 49/81 block (60,49%)

00:02:01.4> [finished] 3 generated tests (0 failures), 00:02:01.3757768.
 -- 0 critical errors, 0 errors, 0 warnings.

[reports] skipping report generation

  EXPLORATION SUCCESS


monitored process exited with Success (0)
finished

Pex needs to find dateTimes in order to test the conditions specified in the method. I used a helper method to calculate the years to date for the age and serviceyears:

   private uint differenceInYears(System.DateTime aDate1, System.DateTime aDate2)
        {
            //missing checks ....
            //approximative
            uint years = (uint)(aDate1.Year - aDate2.Year);
            if (aDate1.Month == aDate2.Month)
            {
                if (aDate2.Day < aDate1.Day) years = years - 1;
            }
            return years;
        }

Could it be the unsigned integer type declarations? Or are the assumptions wrongly formulated? Or both? What does "could not flip 2 branches in a row" mean?

I'll try to do some more test around this. Feel free to comment!

Thanks for reading.

Best regards,

Alexander