Exporting test scripts from Spec Explorer

Question

Hi,

Is there a method available in Spec Explorer to export the test scripts to a third party Test management tool?

Balaji

Answer 1

Test "scripts" are just unit tests in C#. You can define your own attributes and your test class base, which is how we produce test cases for different (unit) test case management tools here at Microsoft. If you want to generate them in a completely different format, you can choose one of two approaches:

1. Create a test adapter that outputs the target format when invoked from the test cases, then run the test cases against your adapter.

2. Write a post-processor that consumes Spec Explorer test cases in the form of an exploration graphs and translates them into the format of your choice, then launch the post-processor from withing Spec Explorer.

Best,

Nico

Answer 2

Hi Nico,

> 1. Create a test adapter that outputs the target format when invoked from the test cases, then run the test cases against your adapter.

This is a good suggestion I also thought of. But how would the adapter embed the test oracle (i.e., assertion) with the expected value. The test oracle is part of the spec explorer model.

If we do not embed the assertion (with the target format) in the test adapter, we are not testing anything. Instead we are just running the methods of the system under test.

Any thoughts?

Dharma

Answer 3

Yes Dharma. This is a very good point. You would have to limit your oracle to return values, and add them as a parameter to your model, so that it gets passed to the adapter and recorded in the output when the calls are made.

Nico

Answer 4

thanks, Nico. I am trying to understand what does it mean by "parameter to the model" in your reply.

Let us assume we have two functions int f() and int g() in the model. Also, assume we have f() and g() in the adapter. When adapter's f() or g() is called during test execution, how could I pass the return value of model's f() function to the adapter's f() function so that I could print my test cases to the target format?

Are there any examples of passing "parameter to the model"?

 

Answer 5

You would add a parameter to both f and g, representing the return value. Your model would then have rules only for the valid return values.

Let's say you have a counter and functions f() and g() are actually Add1() and Subtract1(), respectively, both returning the current value of the counter.

You would then write rules such as:

[Rule]

void Add1(int result)
{
      Condition.IsTrue(result == ++counter);
}

void Subtract1(int result)
{
      Condition.IsTrue(result == --counter);
}

Alternatively, you can leave Add1 and Subtract1 as parameterless actions and use the state checker pattern. The idea behind both approaches is the same: the model will pass the expected return value as an argument to the adapter, so the adapter can choose how to check it. In this particular case, it would generate the oracle in the target format.

Best,

Nico

Answer 6

Nico, I think I got both the approaches you suggested.

If I only work with one or two actions in the model, either of the approaches is definitely fine. In my model, I have 10 actions. This means I have to keep adding a checker for each action as well as the maintaining the state of the return code for each action. Thus, the model and adapter implementation is becoming more complex. Moreover, the cord has to be adjusted well so that each action and its corresponding checkers are called as one atomic action without any interleaving. When I looked at the explored model, checkers tend to "dominant" the model.

I am not sure whether the checker pattern is ideal for me.

I'm thinking of making use of IPostProcessor method to analyse the exploration graph.

Is it possible to get the return code value for each non-void action using the Transition class?

Answer 7

The checker pattern wouldn't require one checker per action. You would just check whether the model state at each point matches the implementation state.

If you are using the return values of your actions as your oracle, then the first approach (add a parameter for the return value) is definitely the way to go. Spec Explorer doesn't really treat return values that differently from input parameters.

Yes, I believe the Transition class will give you the return values and output arguments. It has an Action property of type ActionInvocation. This, in turn, has a property called Arguments, which is an array of SerializableExpression. The array includes an expression for the receiver (for instance-based actions) and the return value (for non-void actions). I'm not sure about the positions, but it should be easy to figure it out.

Best,

Nico

Answer 8

Nico,

I tried the first approach and could pass the expected value to the adapter. I would also add that the model has become somewhat complex because of one or more Condition.IsTrue statements for each action. In addition, it is a different way of thinking (at least to me), meaning that we let the SpecExplorer to choose a return value for us instead of we returning it from our model.

I am concerned about maintaining links between custom test formats and explored state machines. 

If I do not have state names in the generated test (custom format), test failures are difficult to reason about. Also, I am completely disconnected from the explored state machines. 

Is there any good way to pass the current state name to the adapter so that I could at least put the state name (as a comment in the generated test case) before invoking the action of the SUT?

Answer 9

No. State names are transparent to the model, and even vary for the same model program. You can pass some information that conceptually identifies the state, instead. It has to be computed from state data.

Answer 10

Hi Nico,

Is it possible to name the generated test files with a running  suffix 1, 2, 3,...? The reason is that I have my exported test cases and when they fail, I want to be able to trace to the test case generated by the SpecExplorer and then to the exploration graph to identify states and transitions that led to failures.

Any comments?

Dharma

Answer 11

Nico,

I got into an issue when I used the first approach, in that the result out parameter was not reset when I call my action two consecutive times. I noticed that it reused the result value obtained from the prior execution, and thus Condition.IsTrue(...) fails.

machine MyScenario() : Main where ForExploration = false
{
   let string in_subject, bool result
      where
      {.
         Condition.In(in_subject, "test.FILL.test3", "test.a*.b");
      .}
   in

    new MyAdapterImpl;_.foo(in_subject, result){2};
}

Here the "foo" method expects a string input and "returns" the result. Any possibility to instruct spec explorer to avoid reusing result from prior executions?

I tried to remove the result from the declaration and replaced the foo call by "_".

new MyAdapterImpl;_.foo(in_subject, _){2};

It appears to work well. But I want to confirm with you that "_" will let spec explorer choose a value for the result based on Condition.IsTrue(...).

Thanks for your support.

Answer 12

I'm not sure I understand what you mean by "prior executions". Spec Explorer doesn't execute code. It explores it, meaning it will show all possible traces as different branches. There is no real notion of "prior", as branches can be explored in any order. Now if you mean that the value of result is fixed for each trace, that's exactly the effect of the let statement: it binds a value to a name so you can refer to that value by a name in each trace.

If you want the value of the second parameter to vary from one call to the next one on a single trace, you shouldn't bind it with a let statement outside the loop (your loop is the {2} after the call to foo). You can do so by using a placeholder (as you show above), or by moving the let inside the loop:

machine MyScenario() : Main where ForExploration = false
{
   let string in_subject
      where
      {.
         Condition.In(in_subject, "test.FILL.test3", "test.a*.b");
      .}
   in

    new MyAdapterImpl;(let bool result in _.foo(in_subject, result)){2};
}

Best,

Nico

Answer 13

Nico,

Yes, I meant that the value of result is fixed for each trace, which I do not want. I did not know that my assumption about "_" is also OK. Good to know that I can also move the let inside the loop.

Thanks a lot.

Dharma