locked
Avoiding data parameter repetition during exploration RRS feed

  • Question

  • Hi,

    Is there a way to tell Spec Explorer to use unique values for arguments during exploration?

    For example, how can I make sure the Subscribe method is explored without using the same data again and again? 

    I want to avoid sequence such as:

    Subscribe("*"), Subscribe("*") during exploration. Instead I prefer Subscribe("*"), Subscribe("test.>").

    // Test Scenario: One subscriber and two publishers
    
    
    
    machine SubOnePubTwoScenario() : Main where ForExploration = false
    {
       let SoftwareBusAdapterImpl subConn, 
           SoftwareBusAdapterImpl pubConn, 
           SoftwareBusAdapterImpl pubConn2
    
       in
    
       ConnSetup(subConn);
       ConnSetup(pubConn);
       ConnSetup(pubConn2);
    
       (subConn.Subscribe+ ||| subConn.GetNextMsg(_)+ ||| pubConn.Publish+ ||| pubConn2.Publish+)+;
    
       ConnTearDown(subConn);
       ConnTearDown(pubConn);
       ConnTearDown(pubConn2);
    }
    
    machine SubOnePubTwoProgram() : Main where ForExploration = true
    {
       bind Subscribe({"*", "test.>"}, _),
            Publish({"test", "test.xxx"}, _)
       
       in
    
       (SubOnePubTwoScenario;exit) || ModelProgram
    }
    
    machine SubOnePubTwoTestSuite() : Main where TestEnabled = true
    {
        construct test cases where strategy = "shorttests" for SubOnePubTwoProgram()
    }


    Saturday, August 18, 2012 1:30 AM

All replies

  • Hi Dharma,

    In your preferred sequence the rule parameter selection depends on prior steps (history).
    So probably you have to implement a "helping" container state variable (e.g. Modeling.Set<string>), which keeps track of the selections which are already made.

    An unavoidable general side effect: additional states appear ...

    Monday, August 20, 2012 3:36 PM
  • Thanks. Yes, the idea of letting the model track the data is good but at the cost of increasing complexity. I was thinking that we have some way to control it using cord. Apparently that is not the case if I understand your comment.
    Tuesday, August 21, 2012 7:59 PM
  • Hi Dharma,

    in cord a simple idea is using a scenario, including again new control states:

    Subscribe("*");AllModel?;Subscribe("test.>");AllModel?

    Using a similar definition of "AllModel" from your thread here: http://social.msdn.microsoft.com/Forums/en-US/specexplorer/thread/a3fd169f-1ac5-4bb2-98a9-68f891efda21 - "AllModel" should now exclude all stimuli of your model (You could include certain stimuli again with something like "(AllModel ||| Publish)"):

    But:
    When symbolic exploration is fully developed in Spec Explorer there could be a way without generating new control states. In full symbolic exploration all parameters/states are kept symbolic in the exploration result until in a final step a solution with concrete values is found (a posteriori). In this final "grounding step" the Spec Explorer developers could in theory provide a cord-command which tries to use as many different values from a given set (through the full exploration, a kind of soft constraint) for a given parameter type (here the string argument of "Subscribe").

    Wednesday, August 22, 2012 3:27 PM