Answered by:
Can I use Combination on state variables?
Question

I'm wondering how to apply the combination technique to state variables. The examples I saw so far are for parameters. For example, I have 2 state variables, each can have 3 possible values, and an action that will change the values of the 2 state variables. Like this
void ruleMatch(string data)
{
//change the value of the 2 state variables
}
I want all values generated by, pairwise for example, to be covered in the action. Currently I change the rule to
void ruleMatch(state A, state B)
{
state1 = A;
state2 = B;
}
and use Combination.Pairwise in cord to generate all conditions. However since I change the interface it cannot run test. Hence I don't think this is the right way. Any advice? Thanks.
Friday, December 31, 2010 4:20 AM
Answers

In this case, 3 state variables of an Enum with 3 values will generate 27 combinations in total. I put in all these combinations this way
[Rule]
static void ruleMatch(string data)
{
var x = RuntimeSupport.Value<ScanState>();
var y = RuntimeSupport.Value<ScanState>();
var z = RuntimeSupport.Value<ScanState>();
ScanState ss1, ss2, ss3;
int c = 0,i, j, k;
for (i = 0; i < 3; i++)
for (j = 0; j < 3; j++)
for (k = 0; k < 3; k++)
{
ss1 = (i == 0) ? ScanState.cant_tell : (i == 1) ? ScanState.match : (i == 2) ? ScanState.not_match : ScanState.not_match;
ss2 = (j == 0) ? ScanState.cant_tell : (j == 1) ? ScanState.match : (j == 2) ? ScanState.not_match : ScanState.not_match;
ss3 = (k == 0) ? ScanState.cant_tell : (k == 1) ? ScanState.match : (k == 2) ? ScanState.not_match : ScanState.not_match;
Condition.IfThen(data == "A"+ c.ToString(), x == ss1 & y == ss2 & z == ss3);
c++;
}
Combination.Pairwise(x, y, z);
Combination.Expand(x, y, z);
stateA = x;
stateB = y;
stateC = z;
}
with config in cord
config C
{
action abstract static void SUT.ruleMatch(string data)
where data in {"A0","A1","A2","A3","A4","A5","A6","A7","A8","A9","A10","A11","A12","A13","A14","A15","A16","A17","A18","A19","A20","A21","A22","A23","A24","A25","A26"};
}
Unlike in cord script, you can invoke pairwise without giving domain for Enum variables, like this
action abstract static void SUT.sync_scanEx(ScanState a, ScanState b, ScanState c)
where
{.
Combination.Pairwise(a,b,c);
.};
this looks not intuitive. However the result is acceptable, 9 states and 81 steps. This is the solution I can think of so far.
 Marked as answer by u8526505 Friday, January 14, 2011 10:49 AM
Thursday, January 13, 2011 11:30 PM
All replies

Hi, u8526505,
I am not sure what you mean by "combination on state variables". From a specific source state, after a specific transition with concrete parameter values, state update should be deterministic, i.e. there is one single target state. Can you tell me more information about the system that you want to test? I am not clear why after ruleMatch(string data), there could be many possible target states.
Thanks,
Xiang
 Proposed as answer by Xiang LiModerator Sunday, January 2, 2011 5:12 AM
Sunday, January 2, 2011 5:11 AMModerator 
Hi, Xiang,
Thanks for the reply. Sorry for not making my question clear. Here is more details about ruleMatch. In my implementation, there are 2 set of rules. Each will have its own matching state. So the code may look like this
void ruleMatch(string data)
{
stateA = resultOfMatchingInRuleSetA(); //the result can be one of (A1,A2,A3)
stateB = resultOfMatchingInRuleSetB(); //the result can be one of (B1,B2,B3)
}
I am not sure if I understand your answer correctly. It seems that I need to decide all state pairs for (stateA,stateB) first and find all possible values of the parameter that can reach all these state pairs. So I implement my rule for ruleMatch like this
[Rule]
void ruleMatch(string data)
{
if (data == "dataForPair1") {stateA = A1; stateB = B1} //just for example that pair1 is (A1,B1)
if (data == "dataForPair2") ...
...
if (data == "dataForPairN") ...
}
and restrict the parameter values in Cord with
action static void SUT.ruleMatch(string data)
where data in {"dataForPair1","dataForPair2",...,"dataForPairN"};
But I don't know how to leverage Combination class to generate all states for me in this way.
Sunday, January 2, 2011 10:28 PM 
Yes, the latter one is what I mean.
I have a question for you original thought:
void ruleMatch(string data)
{
stateA = resultOfMatchingInRuleSetA(); //the result can be one of (A1,A2,A3)
stateB = resultOfMatchingInRuleSetB(); //the result can be one of (B1,B2,B3)
}
What I am not clear is that why the return value of "resultOfMatchingInRuleSetA()" can be nondeterministic. If it is nondeterministic, how does it return different possible values? Can you share me the code of resultOfMatchingInRuleSetA? Is it returning values randomly?
Monday, January 3, 2011 1:46 AMModerator 
If you think of A1,A2,A3 as "match","not match" and "can't tell", will it make more sense? I think the implementation is too complicated to be shown here but it does not matter not knowing the implementation details. I only need all possible outputs in my model program. The output is an enumerate of values like "match","not match" or "can't tell" as I just mentioned. There are more than 2 sets of rules in the actual implementation. What I want is to generate as many states tuples, e.g. (A1,B1,C1,...,N1), among all these sets of rules as possible but not total possible combinations. That's why I want to use pairwise.
In most examples I've seen, I may need to come out a set of values for the parameters and let it explore the possible states as the revised example in my last reply. However in this case it seems I need reverse the flow. I want to define a set of state tuples first and then create the parameters based on them. Hope I make my question clear enough this time.
Monday, January 3, 2011 10:23 PM 
Hi, u8526505,
Maybe I did not express my thoughts clearly, let me clarify.
if the interface is ruleMatch(string data), then the system must have different return values by different "data", right? The structure should be something like:
if (...) return A1; if (...) return A2; if (...) return A3;
If you think you only need all possible outputs in your model program, then the model might not reflect the design. For example, your model has different state touples, however, the input parameter "string data" cannot determine the return value, which is not true. If you pairwised these state variables (let's assume we can do it), then for a specific string "s", if the expected return value is A1, however, after pairwise, the model thought the expected return value is A2, then everything is incorrect.
If i understand your case correctly, I think you do not want to put the complex algorithm in your model, which makes sense, my suggestion would be abstracting out the algorithm, using an adapter instead of invoke system call directly.
 Proposed as answer by Xiang LiModerator Tuesday, January 4, 2011 3:08 AM
Tuesday, January 4, 2011 3:07 AMModerator 
By the way, i think reversing the flow is not supported in Spec Explorer.
It seems like you pairwise the state varaibles first, then let the tool detect quilified parameters for you, which is difficult.
Tuesday, January 4, 2011 3:12 AMModerator 
The input parameter can determine exactly one result in each rule set. Suppose I have 2 rule sets, after ruleMatch() returns, I have one state pair. See this example
enum state {match, not_match, cant_tell};
state stateA,stateB;
void ruleMatch(string data)
{
stateA = resultOfMatchingInRuleSetA();
stateB = resultOfMatchingInRuleSetB();
}
Suppose passing "x" results in a pair (stateA,stateB) = (state.not_match, state.match), and passing "y" results in (stateA,stateB) = (state.cant_tell, state.match). Now I can have as many state pairs as I need if I can define the right set of parameters. But the problem also appear here  how can I get the right sets of parameters?
OK, put my method aside, for a correct usage of Spec Explorer. How should I proceed from scratch on this case? Thanks.
Tuesday, January 4, 2011 10:30 AM 
Hi, sorry I misunderstood your question, actualy indicating combination of states works, you can write the code like:
void ruleMatch(string data)
{
stateA = resultOfMatchingInRuleSetA();
stateB = resultOfMatchingInRuleSetB();
Combination.Pairwise(stateA, stateB);
}
you can use other combination APIs as well.
Tuesday, January 4, 2011 2:54 PMModerator 
I still cannot get it to function as what I expect. I cannot see how Combination.Pairwise() takes any effects on the result. Here is the model I used. Could you take a look to see what's wrong here? Thanks.
Config.cord
config C
{
action abstract static void SUT.ruleMatch(string data) where data in {"A","B","C"};
...
}
machine M() : C where ForExploration = true
{
construct model program from C where namespace = "MBT.Model"
}
Model.cs
namespace MBT
{
enum MatchState {match, not_match, cant_tell};
static class Model
{
static MatchState stateA, stateB;
[Rule]
static void ruleMatch(string data)
{
if (data == "A")
{
stateA = ScanState.cant_tell;
stateB = ScanState.cant_tell;
}
if (data == "B")
{
stateA = ScanState.not_match;
stateB = ScanState.cant_tell;
}
if (data == "C")
{
stateA = ScanState.match;
stateB = ScanState.not_match;
}
Combination.Pairwise(stateA, stateB);
}
}
}Wednesday, January 5, 2011 1:56 AM 
Hi, first, I want to mention that your code actually reflects your expectation because doing pairwise for stateA and stateB has the same effect with doing fully combination. So you will observe "A", "B" and "C" at the same time.
Second, if you increase the number of "if" statement (adding "D", "E", "F" ...), you're right that you cannot get what you expected; there would be a deep SpecExplorer design issue that the logical operator ( or &&) and "if" statement will result in a new exploration branch, so pairwise is invoked multiple times actually. The workaround is using other operators like "" and "&" or other expressions to replace current expression. If you try the code below, you will find it works because "%" will not result in branching. So maybe you can have a look at your code and see if you can replace current "if" statement.
Model.cs:
namespace SpecExplorer8
{
static class AccumulatorModelProgram
{
static int a;
static int b;
[Rule]
static void Add(int x)
{
a = F1(x);
b = F2(x);
Combination.Pairwise(a, b);
}
public static int F1(int x)
{
return x % 2;
}
public static int F2(int x)
{
return x % 3;
}
}
}cord:
action abstract static void Accumulator.Add(int x) where x in {0..100};
...
 Proposed as answer by Xiang LiModerator Wednesday, January 5, 2011 5:15 AM
Wednesday, January 5, 2011 5:14 AMModerator 
What I observed from your example is that Combination.Pairwise() actual does "steps reduction" instead of "states generation" while the latter is the one I need. It removes steps connecting the same nodes but having different parameter. The total number of state pairs is actually decided by your F1() and F2() functions. If I extends you example from 2 state variables to 3 and let each have the possible value from (0,1,2), then there will be 27 tuples in total. If I let each tuple appearing in the Add() function, Spec Explorer will depict all 27 states in the diagram even Combination.Pairwise() is in use. I don't think that's what pairwise usually does. I used pict.exe to generate the tuples and there are only 9 in total. That's what I expect. Do I misunderstand the usage of pairwise in Spec Explorer?
For the "if" issue, could you elaborate on that? In terms of "steps reduction" , it does work in my example by removing steps connection the same nodes. Thanks.
Thursday, January 6, 2011 1:52 AM 
Hi, first, I want to mention that states generation can be implemented by SpecExplorer combination API. I do not know how you extend the code, but please try the code below, you will find that Spec Explorer will not depict all 27 states. Of course our combination cannot guarantee the optimal result, so the states number is 11 not 9.
namespace SpecExplorer8
{
/// <summary>
/// An example model program.
/// </summary>
static class AccumulatorModelProgram
{
static int a;
static int b;
static int c;[Rule]
static void Add(int x, int y, int z)
{
Condition.IsTrue(x > 0 & x < 100);
Condition.IsTrue(y > 0 & y < 100);
Condition.IsTrue(z > 0 & z < 100);
a = F(x);
b = F(y);
c = F(z);
Combination.Pairwise(a, b, c);
}public static int F(int x)
{
return x % 3;
}
}
}For the "if" issue, in .Net, if you have a look at IL, "if" will be compiled to a "goto" and result in branches, so when Spec Explorer execute the IL, it cannot do combination for these different branches. Logical operators "" and "&&" have the same issue. However, if you use arithmetic operators such as "" and "&", or other mathematical expressions, it will not be compiled to "goto" in IL, that is also our recommendations.
For your case, I recommend you to translate the "if" to boolean expressions, and use "&" and "" to replace "&&" and "". If you think translating the logical expression is too difficult, I provide a workaorund below, where a symbolic value is created in the rule method, and we use the symbolic value to do pairwise.
namespace MBT
{
enum ScanState { match, not_match, cant_tell };static class Model
{
static ScanState stateA, stateB;[Rule]
static void ruleMatch(string data)
{
var x = RuntimeSupport.Value<ScanState>();
var y = RuntimeSupport.Value<ScanState>();
Condition.IfThen(data == "A", x == ScanState.cant_tell & y == ScanState.cant_tell);
Condition.IfThen(data == "B", x == ScanState.not_match & y == ScanState.cant_tell);
Condition.IfThen(data == "C", x == ScanState.match & y == ScanState.not_match);Combination.Pairwise(x, y);
stateA = x;
stateB = y;
}
}
} Proposed as answer by Xiang LiModerator Thursday, January 6, 2011 3:46 AM
Thursday, January 6, 2011 3:46 AMModerator 
Is it equivalent to
[Rule]
static void Add(int x, int y, int z)
{
a = x;
b = y;
c = z;
}with cord
action abstract static void AccumulatorModelProgram.Add(int x,int y, int z)
where x in {0..2}, y in {0..2},z in {0..2}
{.
Combination.Pairwise(x,y,z);
.};
There are 12 states generated. I also noticed you changed the interface from single parameter to three and I think this goes back to my first question: do I need to change my interface to use state as parameter to make pairwise work?
By the way, I found
Condition.IsTrue(x > 0 & x < 10);
Condition.IsTrue(y > 0 & y < 10);
Condition.IsTrue(z > 0 & z < 10);generate more states and steps than
Condition.IsTrue(x > 0 & x < 100);
Condition.IsTrue(y > 0 & y < 100);
Condition.IsTrue(z > 0 & z < 100);I'm wondering how to choose the best parameter domain?
Thursday, January 6, 2011 10:33 PM 
Yes, it is equivalent to your example.
I did not mean to change the interface, I just use the Add sample to illustrate how parameter generation works in Spec Explorer. You do not need to change your interface, as I mentioned in last reply:
For your case, I recommend you to translate the "if" to boolean expressions, and use "&" and "" to replace "&&" and "". If you think translating the logical expression is too difficult, I provide a workaorund below, where a symbolic value is created in the rule method, and we use the symbolic value to do pairwise.
namespace MBT
{
enum ScanState { match, not_match, cant_tell };static class Model
{
static ScanState stateA, stateB;[Rule]
static void ruleMatch(string data)
{
var x = RuntimeSupport.Value<ScanState>();
var y = RuntimeSupport.Value<ScanState>();
Condition.IfThen(data == "A", x == ScanState.cant_tell & y == ScanState.cant_tell);
Condition.IfThen(data == "B", x == ScanState.not_match & y == ScanState.cant_tell);
Condition.IfThen(data == "C", x == ScanState.match & y == ScanState.not_match);Combination.Pairwise(x, y);
stateA = x;
stateB = y;
}
}
}For your second question, I am sorry that there is no way to choose the best parameter domain. Spec Explorer cannot guaratee to find the optimal parameter combinations because calculating optimal solution will be very inefficient. Howerver, if you choose "pairwise", although it is not the optimal result, it will not give many combinations, the number is still a reasonable number.
 Proposed as answer by Xiang LiModerator Friday, January 7, 2011 9:07 AM
Friday, January 7, 2011 9:07 AMModerator 
I follow your suggestion to write the following rule with 3 state variables
[Rule]
static void ruleMatch(string data)
{
var x = RuntimeSupport.Value<ScanState>();
var y = RuntimeSupport.Value<ScanState>();
var z = RuntimeSupport.Value<ScanState>();
Condition.IfThen(data == "A1", x == ScanState.not_match & y == ScanState.cant_tell & z == ScanState.match);
Condition.IfThen(data == "A2", x == ScanState.cant_tell & y == ScanState.match & z == ScanState.cant_tell);
Condition.IfThen(data == "A3", x == ScanState.match & y == ScanState.not_match & z == ScanState.match);
Condition.IfThen(data == "A4", x == ScanState.cant_tell & y == ScanState.cant_tell & z == ScanState.not_match);
Condition.IfThen(data == "A5", x == ScanState.match & y == ScanState.match & z == ScanState.not_match);
Condition.IfThen(data == "A6", x == ScanState.not_match & y == ScanState.not_match & z == ScanState.cant_tell);
Condition.IfThen(data == "A7", x == ScanState.cant_tell & y == ScanState.match & z == ScanState.match);
Condition.IfThen(data == "A8", x == ScanState.match & y == ScanState.cant_tell & z == ScanState.cant_tell);
Condition.IfThen(data == "A9", x == ScanState.not_match & y == ScanState.match & z == ScanState.not_match);
Condition.IfThen(data == "A10", x == ScanState.cant_tell & y == ScanState.not_match & z == ScanState.not_match);
Combination.Pairwise(x, y, z);
stateA = x;
stateB = y;
stateC = z;
}
and cord
config Main
{
action abstract static void SUT.ruleMatch(string data)
where data in {"A1","A2","A3","A4","A5","A6","A7","A8","A9","A10"};
}
The result confuses me very much.
1. There are too many states, 21 in total
2. There are nodes with complete identical state values
3. The value of each state variable is x, x1, x2, ... instead of actual state values like match or not_match
4. This line Combination.Pairwise(x, y, z); actually does nothing IMO. I get exactly the same result when removing it.
So what am I missing here?
Monday, January 10, 2011 11:17 PM 
Hi, first, I tried your project and did not find nodes with complete identical state values.
Second, the x, x1, x2 is the effect of creating symbolic values in model, if you have a look at "constraints" in state browser, you will find many constraints of x, x1, x2, etc. these constraints can calculate the ground value of x, y and z.That is why we do not recommend users to use symbolic values. You can add
Combination.Expand(x, y, z);
After Combination.Pairwise(x, y, z); to expand the values.
Thrid, as I mentioned before, our pairwise cannot guarantee optimal result, so it is possible that A1 ... A10 has the same effect with full combination. So if you have more possible values, you will find pairwise works. For example, you can try to update the code to let A10 has the same effect with A9:
Condition.IfThen(data == "A9", x == ScanState.not_match & y == ScanState.match & z == ScanState.not_match);
Condition.IfThen(data == "A10", x == ScanState.not_match & y == ScanState.match & z == ScanState.not_match);
Then you will find there will be 9 steps in exploration result, A10 does not appear.
Tuesday, January 11, 2011 4:41 AMModerator 
1. The identical values I saw is, for example both nodes have (x1,x2,x3). So you mean they actually represent different values, right?
2. After I added Combination.Expand(x, y, z), the states reduced to 11. I don't even change the code for A10 as you suggested. Is this required for pairwise to work properly?
3. Changing the code for A10 as you suggested but without Combination.Expand(x, y, z) still results in 19 states. Why?
4. How will you construct the domain for the parameter of ruleMatch(string data)? In my case, I used pict.exe to generate these 10 combinations and decided to use 10 values for the parameter. It doesn't make sense for me to use it this way but I don't know what is correct.
Thanks.
Tuesday, January 11, 2011 10:32 PM 
For 1, yes, you are right, x1, x2 and x3 have different constraints, which means they're different states. However, you should expand the parameters to do the testing because symbolic exploration has not been fully supported.
For 2 and 3, can you attach the code of the whole cord file? I guess we used different machines to explore, actually I only explored one step by :
machine M() : C where ForExploration = true
{
(ruleMatch)
(construct model program from C where namespace = "MBT.Model")
}For 4, I think the best way is to let SpecExplorer choose parameters for you. Since you have indicated "pairwise", you should provide the full domain; if you have calculate the domain using pict, then you do not leverage the parameter combination of Spec Explorer.
Thanks,
Xiang
Wednesday, January 12, 2011 12:44 AMModerator 
1. The main difference between the cord files we used is I only use construct model program from C where namespace = "MBT.Model" in my machine. I think you will get the same result as mine by removing (ruleMatch)
2. I think my problem is How to let SpecExplorer choose parameters for me? In this case, what does "provide the full domain" mean?
Thanks.
Wednesday, January 12, 2011 10:31 PM 
OK, I have tried the full model. You're right that expanding will reduce the number of states because as I said, symbolic exploration is not fully supported, so we do not recommend users to use symbolic values. You should expand values always.
For your second question, I mean you can indicate all possible parameter values, and let SE to choose the proper paramters for you. For example, you might have more than 20 possible values: A1, A2 ... A20, ....and finally, Spec Explorer chooses A1, A2 ... A10 for you because pairwise works.
Thursday, January 13, 2011 5:42 AMModerator 
In this case, 3 state variables of an Enum with 3 values will generate 27 combinations in total. I put in all these combinations this way
[Rule]
static void ruleMatch(string data)
{
var x = RuntimeSupport.Value<ScanState>();
var y = RuntimeSupport.Value<ScanState>();
var z = RuntimeSupport.Value<ScanState>();
ScanState ss1, ss2, ss3;
int c = 0,i, j, k;
for (i = 0; i < 3; i++)
for (j = 0; j < 3; j++)
for (k = 0; k < 3; k++)
{
ss1 = (i == 0) ? ScanState.cant_tell : (i == 1) ? ScanState.match : (i == 2) ? ScanState.not_match : ScanState.not_match;
ss2 = (j == 0) ? ScanState.cant_tell : (j == 1) ? ScanState.match : (j == 2) ? ScanState.not_match : ScanState.not_match;
ss3 = (k == 0) ? ScanState.cant_tell : (k == 1) ? ScanState.match : (k == 2) ? ScanState.not_match : ScanState.not_match;
Condition.IfThen(data == "A"+ c.ToString(), x == ss1 & y == ss2 & z == ss3);
c++;
}
Combination.Pairwise(x, y, z);
Combination.Expand(x, y, z);
stateA = x;
stateB = y;
stateC = z;
}
with config in cord
config C
{
action abstract static void SUT.ruleMatch(string data)
where data in {"A0","A1","A2","A3","A4","A5","A6","A7","A8","A9","A10","A11","A12","A13","A14","A15","A16","A17","A18","A19","A20","A21","A22","A23","A24","A25","A26"};
}
Unlike in cord script, you can invoke pairwise without giving domain for Enum variables, like this
action abstract static void SUT.sync_scanEx(ScanState a, ScanState b, ScanState c)
where
{.
Combination.Pairwise(a,b,c);
.};
this looks not intuitive. However the result is acceptable, 9 states and 81 steps. This is the solution I can think of so far.
 Marked as answer by u8526505 Friday, January 14, 2011 10:49 AM
Thursday, January 13, 2011 11:30 PM 
Yes, that is what i mean by "providing the full domain". Can you tell me why it is not intuitive, do you mean you do not need to provide the parameter domain but SpecExplorer will detect it intelligently?Friday, January 14, 2011 12:46 AMModerator

Two reasons
1. Yes. In cord script, this is doable for a parameter of Enum type. Just as I mentioned.
2. The second reason is my lack of knowledge about Spec Explorer. I don't know I need to use RuntimeSupport.Value() first, then Condition.IfThen() to avoid the problems which may be caused by using "if" statement and finally the key method Combination.Expand() to get a satisfying results. I doubted I can come out the final solution by just reading the documents in MSDN and samples (which I almost did) without the long discussion with you.
Friday, January 14, 2011 5:47 AM 
Hi, u8526505,
For your first question, yes, you're right that for enum type it is doable because Spec Explorer can get the domain. But for string, current Spec Explorer does not have intelligent way to generate arbitrary strings. For C# primitive types, expanding domains for string and decimal is not supported.
For your second question, actually that is not because lacking of knowlege :) using RuntimeSupport.Value is actually not recommended because symbolic exploration is not fully supported. However, seems it is the only workaround for your case because of the branching issue I mentioned before, that is actually a Spec Explorer design issue. I agree with you that for complex issues, reading online document is not enough, but feel free to contact me if you encounter any issue in the future.
Your feedback is really valuable for us.
Thanks,
Xiang
Friday, January 14, 2011 6:01 AMModerator