parameter generation for user defined complex types (using type binding)

Question

hello all

recently i was playing around with type binding and user defined types. i tried to generate values for a complex type in the same way as for structs or compound values, but i couldn't figure out how to do it.

tbh i do not really understand what spec explorer is doing here, to me it looks pretty strange.

the following is my test code, i edited the accumulator example, just ignore the naming of things.

using System;
using System.Collections.Generic;
using System.Text;
using System.Linq;

using Microsoft.Modeling;

namespace ComplexTypeTest
{
    public static class AccumulatorModelProgram
    {
        static LoginRequest lg = new LoginRequest();

        [Rule]
        static void testrule(LoginRequest loginRequest)
        {
            lg.pwd = "333";
        }

        [TypeBinding("IMPL2.LoginRequest")]
        public class LoginRequest
        {
            public String pwd;

        }
    }
}

namespace IMPL2
{
    public class LoginRequest
    {
        public String pwd;

        public LoginRequest()
        {
        }
    }
}

using ComplexTypeTest.Sample;
using ComplexTypeTest;
using IMPL2;

config Main 
{
    action abstract static void A.testrule(IMPL2.LoginRequest loginRequest);
}

config ParameterCombination: Main 
{
action abstract static void A.testrule(IMPL2.LoginRequest loginRequest)
where
{.
Condition.IsNotNull(loginRequest);
Condition.IsTrue(loginRequest.pwd == "111" || loginRequest.pwd == "222");

.};
}

machine AccumulatorModelProgram() : Main where ForExploration = true
{
    construct model program from Main 
}

machine DoubleAddScenario() : Main where ForExploration = true
{
    (testrule)*
}

machine SlicedAccumulatorModelProgram() : Main where ForExploration = true
{
    DoubleAddScenario || AccumulatorModelProgram
}

machine AccumulatorTestSuite() : Main where ForExploration = true, TestEnabled = true
{
    construct test cases where strategy = "ShortTests" for SlicedAccumulatorModelProgram()
}

ok, if you now explore the AccumulatorModelProgram machine, it will call testrule(...) two times (no parameter generation involved in the .cord file).

so, where does it take the imput parameters from? if you inspect the steps you will see that it uses the instance generated in the model file in

"static LoginRequest lg = new LoginRequest();"

in the first run pw == null, in the second run pw == "333"

i made a few tests and it seems spec explorer uses all available permanent (within model class variables) instances as input for the rule.

so my first question is... why is it doing this? i don't see any logic relation between action parameter instances and model class variables, or am i missing something?

if you now change the machine AccumulatorModelProgram so it uses ParameterCombination for construction, the exploration seems to run into an infinite loop not generating any states at all.

i tried different things to get spec explorer to generate a LoginRequest, but i couldn't figure it out. i guess i have to explicitely create new instances to use as input somehow, but i'm not sure.

so the main question for me is how does parameter generation in this case work? i would really appreciate if someone could explain to me how this works.

cheers

mkranz

Answer 1

Hi Mkranz,

the type-binding modeling element is used in other cases than structs,
compound values etc.
Use cases are shown in the examples and Nico has explained this here:

http://social.msdn.microsoft.com/Forums/de-DE/specexplorer/thread/89583a26-0cbf-4044-831d-c2ce86913b06 

So it is not made for comparing nested data from the system under test (in or out).
So it is also not used to send such generated data (parameter generation) to the
SUT. 

Hope this helps