Avoiding data parameter repetition during exploration

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()
}

Answer 1

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 ...

Answer 2

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.

Answer 3

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").