locked
Parameter combination RRS feed

  • Question

  • I always have some confusion around parameter combination. Most of the time, the combination works fine when the values of each parameter want to interact with others to generate a meaningful parameter matrix. But sometimes, I need the parameters to be strictly in the combination I want. For example, I have an action Foo(param1, param2, param3) and I want to specify all the parameters with determined groups such as (A, true, false), (B, false, true), etc instead of having the model generate the combination for me.

    I used to have a concatenated string such as A|true|false and then parse the string by myself in the model. Is there a better way doing this?

    Friday, June 18, 2010 12:19 AM

Answers

  • Yes, seeds do this:

    action static void MyClass.Foo(string s, bool b1, bool b2) where
    {
         Combination.Seeded(s == "A", b1 == true, b2 = false);
    }

    This will garantee that the desired combination appears among the ones provided by Spec Explorer. You can specify more than one seeded combination in additional Seeded statements.

    If you want this to be the only combination, you can use Condition.IsTrue(s=="A" & b1 == true & b2 == false), and you can use disjunction to specify more than one: Condition.IsTrue((s=="A" & b1 == true & b2 == false) | (s=="B" & b1 == false & b2 == true))

    Nico

    Friday, June 18, 2010 12:55 AM
    Moderator

All replies

  • Yes, seeds do this:

    action static void MyClass.Foo(string s, bool b1, bool b2) where
    {
         Combination.Seeded(s == "A", b1 == true, b2 = false);
    }

    This will garantee that the desired combination appears among the ones provided by Spec Explorer. You can specify more than one seeded combination in additional Seeded statements.

    If you want this to be the only combination, you can use Condition.IsTrue(s=="A" & b1 == true & b2 == false), and you can use disjunction to specify more than one: Condition.IsTrue((s=="A" & b1 == true & b2 == false) | (s=="B" & b1 == false & b2 == true))

    Nico

    Friday, June 18, 2010 12:55 AM
    Moderator
  • Awesome. Thanks.
    Friday, June 18, 2010 1:09 AM
  • Hi,

    I'm using the bind statement for assigning parameters. I am not sure how I would use the Combination capability to restrict combinations of parameters in conjunction with the bind statement.

    machine SubOnePubOneScenario() : Main where ForExploration = false
    {
       let SoftwareBusAdapterImpl subConn, SoftwareBusAdapterImpl pubConn
          
       in
    
       ConnSetup(subConn);
       ConnSetup(pubConn);
       
       (subConn.Subscribe* ||| subConn.SubscribeCallback* ||| pubConn.Publish* ||| subConn.GetNextMsg(_)*);
       
       ConnTearDown(subConn);
       ConnTearDown(pubConn);
    }
    
    machine SubOnePubOneDemoProgram() : Main where ForExploration = true
    {
      construct accepting paths for
    
       bind Subscribe({"test.>"}, _),
            SubscribeCallback({"callback.test.>"}, {1}, _),
            Publish({"test.xxx", "callback.test.xxx"}, _)
       
       in
    
       (SubOnePubOneScenario;exit) || ModelProgram
    }

    I want to make sure when Subscribe is called with "test.>" the Publish method is called with "test.xxx" only. Similarly, when SubscribeCallback is called with "callback.test.>" the Publish method  is called with "callback.test.xxx" only.

    Monday, September 10, 2012 7:48 PM
  • Hi Dharma11,

    since the parameters are correlated over different steps, I see no chance to do this with a bind/seed statement.
    I think you have to use a let-statement or model it inside your program model...

    Wednesday, September 12, 2012 3:00 PM
  • Hi,

    OK, thanks. I have one more question related to choosing parameter values, in that I call foo+ but I want to avoid certain tests (they are redundant most likely)

    For example, the trace foo("a"), foo("b") is the same as foo("b"), foo("a").  I do I let the Spec Explorer know this abstraction strategy to reduce the size of the state space and the number of tests.

    Thanks,

    Dharma

    Thursday, September 13, 2012 5:03 PM
  • Hi Dharma,

    my idea for the rule "foo(string s)" is the following:

    * If in your model the scenario foo("a") stores "s" in a state variable then the scenario foo("b") will result in a different state.
    This can be prevented, if the parameter "s" is kept symbolic (since your model has only one code path and no - if (s=="Bob" ...).
    You can do this already today with "Combination.KeepUnexpanded(s)" and "Combination.Strategy(CombinationStrategy.Coverage);"
    This is the full symbolic exploration (mentioned in several places, the class video etc.).

    * There are several limitations. The one here: Often the exploration (test case etc.) will include finally only the relevant and correct test cases, but finally the symbolic value "s" is still a symbol and in the SE relaease 3.5 is not "approved/enabled" to fill in concrete values.
    So the test case will have transitions like "foo(s1)" and in the state browser constraints like "#0 : s1 == "Bob"". It is good enough for analysis, but not for test execution.

    * A solution with changing the program model for today is to build a rule representing two steps at once:
    "foo(string s1, string s2)" and use "Combination.Strategy(CombinationStrategy.Coverage);".

    * Another is again the let statement - here the full advice: 
    "How about using “let” statements to create parameter combinations across action invocations?
    You can still use operators such as “&” to represent different temporal orderings.
    You might also need to lift some of the conditions from the model program to Cord,
    since you will want the expansion point to occur before rules are triggered"


    • Edited by bububa Friday, September 14, 2012 12:52 PM
    Friday, September 14, 2012 12:49 PM
  • Hi,

    Thanks for your support. I see your point related to using the let statement. In the past, I indeed passed a string argument to my machine. However, it was not sufficient when I use a "foo(s)+" for example on the action. It reuses the same input argument "s" for all repetition, which is not enough for my scenario of interest. I want the repetition to apply different input values. Thus, I removed that idea of passing an input parameter to my machine.

    I probably misled you to propose foo with two arguments. Let me put my concrete model data here for discussion. I am testing a pub-sub architecture. A subscriber can subscribe to one or more messages. Thus I put "Subscribe+" in the cord, which means having two arguments of foo is not relevant here. Inside my model, I have a configuration const to limit the number of subscriptions to avoid state space explosion.

    In "SubscribeDemoProgram", I have just used two string inputs for demo and discussion purposes although the real program has to be tested for many different types of input strings. You can see from the exploration graph that I get possibly redundant paths. For example, the path that swaps "xy" and "x.abc.uvw" can be treated together as one, instead of swapping them to generate more paths/tests.

    Is there any way I can do that using Spec Explorer?

    config SubscribeCfg : Main
    {
      action void SoftwareBusAdapterImpl.Subscribe(
            string subject, bool result) 
            
      where subject in {"xy", "x.abc.uvw", "test.*.>", "test.*.*.>", "*",
                    "test.>.x", "test>", "test.a*.b", "test..a", "test.a.", ".a.test", "test b", "x/a", "x\\a"};
    
    }
    
    machine SubscribeModelProgram() : Main where ForExploration = false
    {
        construct model program from SubscribeCfg where scope = "SoftwareBus_TestProject.Connection"
    }
    
    machine SubscribeScenario() : Main where ForExploration = true
    {
       let SoftwareBusAdapterImpl conn
    
       in
    
       new conn.SoftwareBusAdapterImpl;
       (
         conn.Create;
         (
            conn.Connect;
            conn.Subscribe+;
            conn.Disconnect;
         )+;
         conn.Destroy+
       )
    }
    
    machine SubscribeDemoProgram() : Main where ForExploration = true
    {
      // NOTE: bind parameters have to be a subset of local config parameters
      
      bind Subscribe({"xy", "x.abc.uvw"}, _)
                         
      in 
       
      (SubscribeScenario;exit) || SubscribeModelProgram
    }
    
    machine SubscribeDemoTestSuite() : Main where TestEnabled = true
    {
        construct test cases where strategy = "shorttests" for SubscribeDemoProgram
    }
    



    • Edited by Dharma11 Friday, September 14, 2012 2:31 PM
    Friday, September 14, 2012 2:29 PM
  • Lets have a scope. If you say 'let int a in Foo(a)+', the same value of 'a' will be used in all iterations. Whereas if you say '(let int a in Foo(a))+' there will be a different value for 'a' in each iteration.

    Regarding your "redundant paths", it seems like you want to use a "state coverage" strategy. That is, you want test cases to cover all your states, regardless of the steps that get you there. Unfortunately, Spec Explorer only supports "step coverage" strategies. That is, every step in the graph will appear in at least one test case.

    HOWEVER, you can use requirement coverage to prune a graph before constructing test cases. So if you add requirement capture statements to your model program so that your equivalent paths end up covering the same requirement, you can then use selective requirement coverage to only keep one path.

    Friday, September 14, 2012 4:36 PM
    Moderator