Overlap trace test cases in result of Combinatorial Test

[shinsahara]

Description

There are some overlap trace test cases in Combinatorial Test (CT)

Steps to Reproduce

1. Unzip the attached zip file There are 2 VDM++ files (Library.vdmpp, UseLibrary.vdmpp) in the zip file. Library4HoseiE_Smallest.zip

2. Mke a VDM++ project using unzipped VDM files

3. Run CT

Expected behavior: 24 (non0overlapping) test cases should be generated.

Actual behavior: 32 test cases generated. Following test cases are overlapped.

Test 000001 is same as Test 000002. Test 000003 is same as Test 000004 Test 000005 is same as Test 000006 Test 000007 is same as Test 000008 Test 000025 is same as Test 000026 Test 000027 is same as Test 000028 Test 000029 is same as Test 000030 Test 000031 is same as Test 000032

Reproduces how often: 100%

Versions

Overture Tool Version: 2.6.2 Build date: 2018 May 18 11:17 CEST macOS High Sierra version 10.13.6

Additional Information

VDMTools generate 24 trace test cases, and there is no overlapped case.

[nickbattle]

Is it the same with VDMJ? I'm on holiday at the moment, but will look at this when I get back.

[shinsahara]

It is the same with VDMJ as followings: Test1 is same as Test2, and Test3 is same as Test4

> load Library.vdmpp UseLibrary.vdmpp
Parsed 2 classes in 0.026 secs. No syntax errors
Type checked 2 classes in 0.016 secs. No type errors
Initialized 2 classes in 0.011 secs. 
Interpreter started
> runalltraces
-------------------------------------
runtrace UseLibrary`T3
Generated 32 tests in 0.006 secs. 
Test 1 = sL.add_user(mk_token("Larsen")); sL.add_user(mk_token("Larsen")); sL.add_book(mk_token("OO Construction_1")); sL.add_book(mk_token("OO Construction_1")); sL.borrow_book(mk_token("Larsen"), mk_token("OO Construction_1")); sL.borrow_book(mk_token("Larsen"), mk_token("OO Construction_1")); sL.remove_user(mk_token("Larsen")); sL.getAttributes()
Result = [(), Error 4071: Precondition failure: pre_add_user in 'Library' (Library.vdmpp) at line 21:11, INCONCLUSIVE]
Test 2 = sL.add_user(mk_token("Larsen")); sL.add_user(mk_token("Larsen")); sL.add_book(mk_token("OO Construction_1")); sL.add_book(mk_token("OO Construction_1")); sL.borrow_book(mk_token("Larsen"), mk_token("OO Construction_1")); sL.borrow_book(mk_token("Larsen"), mk_token("OO Construction_1")); sL.remove_user(mk_token("Larsen")); sL.getAttributes()
Test 2 FILTERED by test 1
Test 3 = sL.add_user(mk_token("Larsen")); sL.add_user(mk_token("Larsen")); sL.add_book(mk_token("VDM_1")); sL.add_book(mk_token("OO Construction_1")); sL.borrow_book(mk_token("Larsen"), mk_token("VDM_1")); sL.borrow_book(mk_token("Larsen"), mk_token("OO Construction_1")); sL.remove_user(mk_token("Larsen")); sL.getAttributes()
Result = [(), Error 4071: Precondition failure: pre_add_user in 'Library' (Library.vdmpp) at line 21:11, INCONCLUSIVE]
Test 4 = sL.add_user(mk_token("Larsen")); sL.add_user(mk_token("Larsen")); sL.add_book(mk_token("VDM_1")); sL.add_book(mk_token("OO Construction_1")); sL.borrow_book(mk_token("Larsen"), mk_token("VDM_1")); sL.borrow_book(mk_token("Larsen"), mk_token("OO Construction_1")); sL.remove_user(mk_token("Larsen")); sL.getAttributes()
Test 4 FILTERED by test 3
...

[nickbattle]

OK, now back from holiday. I think I can see what's happening. It's because you have "let a, b in set ...". For the duplicated tests, both a and b are set to the same value, but they are regarded as different "selections" from the set of possible permutations. You'll see that the second instances of the test are then filtered out (rather than being executed) since it knows that the first one failed.

I'll look into the expansion a bit more closely to clarify why it thinks they are different, but I'm pretty sure this is the root of the problem. It will probably be like saying that a=1, b=1 is different to b=1, a=1 - the result is the same, but the means of getting the result is different.

[nickbattle]

Hmmm... or it may just be the alternation that you have removing user1 or user2. When the two users are the same, the alternation expands to the same result, but the two paths to get there are "the same". I'll investigate a bit more...

[nickbattle]

OK, that does seem to be the "issue". When you have an alternation over N possibilities, when one or more of the possibilities is the same, you get duplicate tests. Ultimately, it is because the expansion engine does not generate a "set of tests" (which has no duplicates); it generates one test at a time by driving an iterator, which is more space efficient.

So... is this an error or a feature? :-)

[shinsahara]

I think this is not a feature. Because VDMTools generate correct combinatorial test cases. And, I think combination of set is like following:

  {{a,b} | a,b in set {1,...,4} & card {a,b} = 2} = 
      { { 1, 2 }, { 1, 3 }, { 1, 4 }, { 2, 3 }, { 2, 4 }, { 3, 4 } }

It's not

  {{1,2},{2,1},..., {3,4},{4,3}}

[nickbattle]

I agree with your point about sets - and this isn't the underlying problem here, that was just a guess when I first looked at your example. The actual problem is because of the alternation, when both sides of the alternation generate the same step. If you remove the alternation, Overture handles the sets correctly.

So I think the minimal example is:

        let p1 = mk_token("Sakoh"), p2 = mk_token("Sakoh") in
        (
            add_user(p1) | add_user(p2)
        )

That generates (in VDMJ):

Generated 2 tests in 0.006 secs. 
Test 1 = add_user(mk_token("Sakoh"))
Result = [mk_token("Sakoh"), PASSED]
Test 2 = add_user(mk_token("Sakoh"))
Result = [mk_token("Sakoh"), PASSED]
Executed in 0.03 secs. 
All tests passed

You're saying that VDMTools would only have one test here? An interesting point is that, although the two tests are "the same", they are generated by different paths through the trace and "use" different variables. So they would be regarded as different "shapes" in terms of shaped reduction.

[shinsahara]

I think your minimal example is not fit for my purpose.

I want to generate 4 tests in following.

T2: 
    let p1,p2 in set {mk_token("Sakoh"), mk_token("Larsen")} in 
        (
         sL.add_user(p1); sL.add_user(p2)
        )

That generates 4 tests that I wanted in Overture Tool and VDMTools:

>> traces UseLibrary`T2
Initializing specification ... done
Expanding UseLibrary`T1 ... done.
Expanding UseLibrary`T2 ... done.
Expanding UseLibrary`T3 ... done.
UseLibrary`T2: 4 cases
UseLibrary`T2 Case: 1 / 4
sL.add_user(mk_token("Sakoh")); sL.add_user(mk_token("Sakoh"))
/Users/sahara/workspace4_2.0.2/Library4HoseiE_Smallest/Library.vdmpp, l. 21, c. 8:
  Run-Time Error 58: 事前条件の評価結果がfalseです
sL.add_user(mk_token("Sakoh")): (no return value)
sL.add_user(mk_token("Sakoh")): exit <RuntimeError>
<OK>
UseLibrary`T2 Case: 2 / 4
sL.add_user(mk_token("Sakoh")); sL.add_user(mk_token("Larsen"))
sL.add_user(mk_token("Sakoh")): (no return value)
sL.add_user(mk_token("Larsen")): (no return value)
<OK>
UseLibrary`T2 Case: 3 / 4
sL.add_user(mk_token("Larsen")); sL.add_user(mk_token("Sakoh"))
sL.add_user(mk_token("Larsen")): (no return value)
sL.add_user(mk_token("Sakoh")): (no return value)
<OK>
UseLibrary`T2 Case: 4 / 4
sL.add_user(mk_token("Larsen")); sL.add_user(mk_token("Larsen"))
/Users/sahara/workspace4_2.0.2/Library4HoseiE_Smallest/Library.vdmpp, l. 21, c. 8:
  Run-Time Error 58: 事前条件の評価結果がfalseです
sL.add_user(mk_token("Larsen")): (no return value)
sL.add_user(mk_token("Larsen")): exit <RuntimeError>
<OK>

[nickbattle]

Are you sure? When I try that test with Overture 2.6.2 and VDMJ, they produce 8 tests.

[nickbattle]

Oh! Sorry, I have a version with an alternation instead of just two calls:

        let p1, p2 in set { mk_token("Sakoh"), mk_token("Larsen") } in
        (
            add_user(p1) | add_user(p2)
        )

[shinsahara]

Your minimum example generates 4 tests in VDMTools and Overture Tool.

We have gone back. My T3 test generate 24 tests in VDMTools, and 32 tests in Overture Tool and vdmj. And I feel generating 24 tests is good for tester.

[nickbattle]

I can see why removing duplicates is useful. But the problem is that in general that is quite an expensive thing to do - to know that a test has been generated already, you need to keep the previously generated tests. Overture and VDMJ don't generate all of the tests to start with and then execute them, they generate each test iteratively and keep minimal information about failed results (for stem filtering). That means millions of tests can be generated without taking up too much space.

Do you know how VDMTools does its duplicate removal?

[shinsahara]

I don't know how VDMTools does its duplicate removal? But, from VDMTools output, VDMTools seems to keep generated data.

>> traces UseLibrary`T2
Initializing specification ... done
Expanding UseLibrary`T1 ... done.
Expanding UseLibrary`T2 ... done.
Expanding UseLibrary`T3 ... done.
UseLibrary`T2: 4 cases

I'll ask Dr. Kei Sato.

[nickbattle]

From some simple experiments with VDMTools, it looks like the set of tests generated is treated as a "set" - no duplicates - regardless of how or where the test was generated in the trace.

VDMJ treats different parts of the trace as (potentially) different "shapes" even if they result in the same test output. So for example, if the trace below is reduced using the "shapes varnames" method, the second "copy" of the output is included as it is a different "shape" (regarding the variable names used to generate it). So even reducing to 10% includes one test of each distinct shape:

    T:
        let p1 = mk_token("Sakoh"), p2 = mk_token("Sakoh") in
        (
            x.add_user(p1) | x.add_user(p2)
        ) |
        let p3 = mk_token("Sakoh"), p4 = mk_token("Sakoh") in
        (
            x.add_user(p3) | x.add_user(p4)
        )

> filter 10
Trace filter currently 10.0% RANDOM (seed 0)
> filter shapes_varnames
Trace filter currently 10.0% SHAPES_VARNAMES (seed 0)
> runtrace T`T
Generated 4 tests in 0.015 secs. 
Test 1 = x.add_user(mk_token("Sakoh"))
Result = [mk_token("Sakoh"), PASSED]
Test 3 = x.add_user(mk_token("Sakoh"))
Result = [mk_token("Sakoh"), PASSED]
Executed in 0.031 secs. 
All tests passed
>

[shinsahara]

Yes, Nick. VDMTools uses "set" for generating test. Dr. Kei Sato replied that he've implemented following specification:

https://github.com/vdmtools/vdmtools/blob/master/spec/traces-spec/expanded.vdm