Spec Explorer on advanced constraints for combinations


Blog updates are long over due.   Hopefully I’ll get more regular.

The biggest thing for me is the final Release-To-Web version of Spec Explorer (SE) as DevLabs plugin for Visual Studio 2010 Professional.   I’ve had the pleasure of using SE for years within Microsoft.   It has been publicly available in various forms over the years (first from Microsoft Research (MSR), now from DevLabs).    This version of SE is the most suitable for broad usage with extensive documentation and examples.   SE has a complete product team of Dev, Test, and PM following typical Microsoft product processes.

 

Each incarnation has been making it easier for people to use it for State Based Modeling.    There is now even a full video series  of tutorials (four 90 minute lectures with demos – unfortunately screens aren’t always easy to read, but we know we need to re-record it).     If you want a short introduction, just watch the Channel 9 video, Spec Explorer: Model-Based Testing Made Practicable.  

 

I think one of the most overlooked features of Spec Explorer is its ability to do data combinatorics (in addition to or even independent of state based testing).   I still find Pairwise Independent Combinatorial Testing (PICT) Tool the easiest way to do pair-wise combinations of independent inputs for simple problems.   However, SE allows far fancier constraints than PICT.   One example for a fellow tester was verifying a travel site and they wanted to control Month, Day, and Year of dates for both departure and arrival.   You can’t do date comparisons in PICT (or other pair-wise tools I’m aware of). 

 

My fellow tester put forth their constraints as:

               Each trip had a start date and an end date.    Naturally, the end date could not be before that start date.

               Other things that had caused their application trouble in the past were: 

               Trips entirely in next year.  (DepartureThisYear = true or false)

               The representation of months and days as single or double digits (1/1, 1/31, 10/1, 12/31)

               They also looked at common booking patterns for tripLength in days (0 = same day, 1 = overnight trip, up to 60 days long).

               Finally, [minimum] days until the trip started (and not just the year) was of interest if it could be satisfied while satisfying the other constraints above.
                             (0 = start today, 1 = start tomorrow, up to 60 days)

Trips entirely in this year when possible [if the above constraints are already met].   (ReturnThisYear = true of false).

                              Note we have at most 3 legal combinations since ReturnThisYear=true and DepartureThisYear=false violates our first constraint.

 

I showed how a simple SE model and cord script could meet their needs.  You can also look at the Parameter Generation Walkthrough for other examples.

   

The parameters to be combined are:

        static string TravelDates(short DaysToDeparture, short TripLength,

            bool DepartureDay2Digits, bool DepartureMonth2Digits, bool DepartureThisYear,

            bool ReturnDay2Digits, bool ReturnMonth2Digits, bool ReturnThisYear)

with the constraints:

            ulong departureDate = TravelDate(DaysToDeparture, DepartureDay2Digits, DepartureMonth2Digits, DepartureThisYear);

            ulong returnDate = TravelDate(DaysToDeparture, ReturnDay2Digits, ReturnMonth2Digits, ReturnThisYear);

            Condition.IsTrue(returnDate >= departureDate);

 

We further restrict the integer value domains to make the problem tractable

             Condition.In(DaysToDeparture, 0,1,2,10,30,60);

             Condition.In(TripLength, 0,1,2,10,30,60);

All combinations (regardless of returnDate >= departureDate) would be 2,304.    Using

             Combination.Pairwise(DaysToDeparture, TripLength, DepartureDay2Digits, DepartureMonth2Digits, DepartureThisYear

                                 ,  ReturnDay2Digits, ReturnMonth2Digits, ReturnThisYear);

We have only 157.

 

Full Model, cord, and combinations are shown at end of this blog post.

When exploring the model, looking at any state shows you an example date satisfying the parameters.  For example:

 

 

BasicModel.cs:

using System;

using System.Collections.Generic;

using System.Text;

 

using Microsoft.Modeling;

using Microsoft.Xrt.Runtime;

 

[assembly:NativeType(typeof(System.DateTime))]

namespace Microsoft.Protocols.TestSuites.TravelDates

{

    static class Model

    {

        static string DepartAndReturn = "";

 

        static string DisplayState()

        {

            return DepartAndReturn;

        }

 

        [AcceptingStateCondition]

        public static bool IsAccepting

        {

             get

            {

                return (DepartAndReturn != ""); 

            }

           

        }

 

        [Rule]

        static string TravelDates(short DaysToDeparture, short TripLength,

            bool DepartureDay2Digits, bool DepartureMonth2Digits, bool DepartureThisYear,

            bool ReturnDay2Digits, bool ReturnMonth2Digits, bool ReturnThisYear)

        {

 

            //Contracts.Requires(DepartureThisYear & !DepartureMonth2Digits & System.DateTime.Now.Month < 10);

            ulong departureDate = TravelDate(DaysToDeparture, DepartureDay2Digits, DepartureMonth2Digits, DepartureThisYear);

           

            Condition.IsTrue(!(!DepartureThisYear & ReturnThisYear));   // Redundant with returnDate > departureDate

            ulong returnDate = TravelDate(DaysToDeparture, ReturnDay2Digits, ReturnMonth2Digits, ReturnThisYear);

 

            Condition.IsTrue(returnDate >= departureDate);

            DepartAndReturn = String.Format("Depart: {0:d}, Return: {1:d}", new DateTime((long)departureDate), new DateTime((long)returnDate));

            return DepartAndReturn;

        }

 

        // ThisYear fails if single digit month is needed and past Oct. 1.

        /// <summary>

        ///      Creates a date with number of days, then month, and then if possible year matching parameter criteria.

        /// </summary>

        /// <param name="DaysToDate">Number of days from Now that is earlies date could be.</param>

        /// <param name="Day2Digits">True if 2 digit days (e.g. 10, 31) are wanted.  Otherwise (false), Single digit days (1-9).</param>

        /// <param name="Month2Digits">True if 2 digit months (10-12) are wanted.  Otherwise (false), Single digit months (1-9).</param>

        /// <param name="ThisYear">True if date should be this year (if possible considering previous constraints).  Otherwise (false) next year.</param>

        /// <returns>ticks corresponding to date with characterstics defined by paremters.</returns>

        static ulong TravelDate(short DaysToDate, bool Day2Digits, bool Month2Digits, bool ThisYear)

        {

            DateTime startDate = DateTime.Now.AddDays(DaysToDate);   // Minimum departure time.

 

            // Choose 1 or 2 digits for days.

            if (Day2Digits)

            {

                if (startDate.Day < 10)

                {

                    startDate = startDate.AddDays(10 – startDate.Day + startDate.Millisecond % 18); // Make between 10 and 28

                }

            }

            else

            {

                if (startDate.Day >= 10)

                {   //Throw into next month:  Add remaining days of this month and then number between 1 and 9.

                    startDate = startDate.AddDays(DateTime.DaysInMonth(startDate.Year, startDate.Month) – startDate.Day

                                                    + startDate.Millisecond % 9); // Make between 1 and 9

                }

            }

 

            // Choose 1 or 2 digits for months.

            if (Month2Digits)

            {

                if (startDate.Month < 10)

                {

                    startDate = startDate.AddMonths(10 – startDate.Month + startDate.Millisecond % 3); // Make between 10 and 12

                }

            }

            else

            {

                if (startDate.Month >= 10)

                {

                    startDate = startDate.AddMonths(13 – startDate.Month + startDate.Millisecond % 9); // Make between 1 and 9

                }

            }

 

            if (!ThisYear && (startDate.Year == System.DateTime.Now.Year)) startDate.AddYears(1);

 

            return (ulong)startDate.Ticks;

        }

 

 

    }

}

 

 Rest of the example in a second post.

Advertisements

About testmuse

Software Test Architect in distributed computing.
This entry was posted in software testing. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s