Shin Sahara

Please open "System Prefernces" and select "Security & Privacy" icon. You can find "Overture.app" was blcocked ... stetement, and the button "Open Anyway" Push "Open Anyway" button, then you can...

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

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

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

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

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

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