Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

Tests by case feature NumRange; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
1c435db27754adabc48962f3f91fb26e79c7a766 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: Replace spec with the same without comments
NumRange OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
805d6f82b99180273d831b1b0c52dc1608b195e0 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: Replace spec with the same without comments
NumRange OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
b5d262863964278e1e09d4a00ac6b5c495e20992 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: Replace spec with the same without comments
NumRange MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
32d39331af174fca266dc47fc7426bde7266bb90 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: Replace spec with the same without comments
NumRange MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
0b6c107e48cb51ccaee178196743993ac1cf158e TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Let True Passed
  • Model Under Test
  • Equivalent Model
1347a9f6b97f13aa30aa49c86bf7ea975ba511d3 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Let False Passed
  • Model Under Test
  • Equivalent Model
dfb87e51b4e1b16bd0cb56dd5d39949becc89319 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Choose True Passed
  • Model Under Test
  • Equivalent Model
d1b93c18dcde6f955dc4de712240a114c2cfe888 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Choose False Passed
  • Model Under Test
  • Equivalent Model
0ddf01d76eb4ba6121495ae875cd13aa875e4b87 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange FunApp True Passed
  • Model Under Test
  • Equivalent Model
398c89b0fe89f1cac6dedbe45b0159c84ce9614d TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange FunApp False Passed
  • Model Under Test
  • Equivalent Model
8dce0153123e51fcba173b0d7bf790d7428e1d84 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Prime True Passed
  • Model Under Test
  • Equivalent Model
b5776e9f44f5044f43e50381e131c89e851af7a7 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Prime False Passed
  • Model Under Test
  • Equivalent Model
d8815819943881ab04a39450f9902b6903d53505 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumZero True Passed
  • Model Under Test
  • Equivalent Model
79dbf85907fac4a0610401b3a9ee17df07eac628 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumZero False Passed
  • Model Under Test
  • Equivalent Model
4a3b2785a5c0734f2f9dba5868b18ee0c67905d0 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumOne True Passed
  • Model Under Test
  • Equivalent Model
4041a2a9af84ce7412a388c46025a3ecf14c060f TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumOne False Passed
  • Model Under Test
  • Equivalent Model
3d66d888c8c2cb42ad8fd99d3a385e1ea405a5c1 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
f0352d0ade27f06edf94ece5a71a69e3bedc854b TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
537a6af05b4868faf00d7baa80458fb9dc4fdd3e TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
f21d1084ec11990d95de773b402238192841b530 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
864b124ae2c1a38394bda5e247700760e4048fb5 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumPlus True Passed
  • Model Under Test
  • Equivalent Model
00c3c4264aa77cba8d9a788db9a23de6d38e76f0 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumPlus False Passed
  • Model Under Test
  • Equivalent Model
cb1724e1f84a64c7aa81e560946c27390afc8174 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ebbc2a299fd7bd38c1bce04fd8225a5ba7da397a TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMinus False Passed
  • Model Under Test
  • Equivalent Model
938c5a7033264af668b83dce031e5adb34bce711 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMul True Passed
  • Model Under Test
  • Equivalent Model
f52cf9b65362d59c170c2b80422cd879c622fee3 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMul False Passed
  • Model Under Test
  • Equivalent Model
541cdfdeae6e7e599eff2e8f5203afb290e6a797 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumDiv True Passed
  • Model Under Test
  • Equivalent Model
89aebb54c7cdc7424e9fe6e00c693ee03ffa8179 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumDiv False Passed
  • Model Under Test
  • Equivalent Model
1509485f43f11a759d075035b335eb826c15d70e TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMod True Passed
  • Model Under Test
  • Equivalent Model
d8ed3755a42d4a80063e6fd37f4d7cd8fa09f9eb TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumMod False Passed
  • Model Under Test
  • Equivalent Model
0da26381f618ada3ac434a5f049eba96d7b2a361 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumPow True Passed
  • Model Under Test
  • Equivalent Model
5f29a75ec685d4532168dfd577196af6e7c68907 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange NumPow False Passed
  • Model Under Test
  • Equivalent Model
5869e2e535c874d0f73115adf3607d49becd3dab TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def0 True Passed
  • Model Under Test
  • Equivalent Model
a098a295eadfc19dc23a13018b252d2debcb3800 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def0 False Passed
  • Model Under Test
  • Equivalent Model
ccf8cd5e78d8072423c172dab66d48513fd4ed6f TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2c9d27907897e8de1ffb41ec7711ad0518487588 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
fe822799e79c0450770189efc7cc658601a05683 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def1 True Passed
  • Model Under Test
  • Equivalent Model
026c1d1dac8f0a44f3705c46afa12050ec5c5934 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def1 False Passed
  • Model Under Test
  • Equivalent Model
fabdc1d5a2689cb52aaa7b8c35cd91fc7b732784 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
b6f5e078c3c23be70c2a33232eeede9ecd12a627 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
7973a89a00c2c0debf606007c09a5d0b1f96eb2e TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def2 True Passed
  • Model Under Test
  • Equivalent Model
da584d9492a4c4fb9fafc6034b5b29e38ac0b070 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def2 False Passed
  • Model Under Test
  • Equivalent Model
99ea4f8b19db45aaeb2c5998d0178d94325d06cb TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
0900e58012ecf4ef36ffff66bcd052a3940792a8 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
3bf58e54756956c2efb464d94f1de0f1aea4bfd1 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c41d0a591b94f612e2eec2e390baddf1ca0ac2f6 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
982ec14b6d6e7dcf37f7fbefebaadb76e7d8f65e TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
7522d440871408f0a459f658d82f6e784c89eb76 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: LET definitions are reduced to global definitions
NumRange LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ff7363ffc91d2ca02a8881ff1b596f908fbe6ea6 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Extends True Passed
  • Model Under Test
  • Equivalent Model
3253d4bdcbabe7eb1be2d07786df51c37155407d TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Extends False Passed
  • Model Under Test
  • Equivalent Model
f4ac08ae9b55cd65d9e49b7fb8536813f5eed057 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
08c0a51b8f4c536e89250cb443a25a549548b5da TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
7f7565d23fd5ec4e4081383d27d8675d878bb06a TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Variable True Passed
  • Model Under Test
  • Equivalent Model
c14fdfdadd9726797bd90a64ca39317dfa2a843f TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Variable False Passed
  • Model Under Test
  • Equivalent Model
9a47e65c5b3cf192ee7c341f01418b37eac7cfca TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Constant True Passed
  • Model Under Test
  • Equivalent Model
6ac511a93ecfb91ac1c47b34285d8a1943c2c5d6 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Constant False Passed
  • Model Under Test
  • Equivalent Model
ddea6a60307bedfeef92fe3a2a05de4468727ad7 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
d3fb3c55c925f1b000f8c3c5810e2e2a4cdba253 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
b466bddc1d94d859e6299bf0e0c9aae125454981 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Instance True Passed
  • Model Under Test
  • Equivalent Model
4e7f5222ecb4a5b2fad1a02bc98109717dd769a5 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange Instance False Passed
  • Model Under Test
  • Equivalent Model
8530db1550c9257bb4b84eddec32589ed4f0e5cd TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
32c16a0928057d3447d609638fb18c8b28cdfae5 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
fe685207446205241cceec302c962160a260ae39 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
52c955f89139d18306434e137422cdc85f030ce1 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
ad7b2e682410f5cabebb8576fdb6b3013decb91c TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
db2b4e3d567eca100da1300ef076f34e494877bc TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
704141392015d62469eebe117aba794d0950161c TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
a95b604914753d80c88ae14fea231334f8c4f130 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
ba97fa5caf801873aa1cfe4016ee345a5f7d0df6 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
67580b379368653d2be3e1f2a4c4e6696787992d TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4add645da9a18435c457dd45f3736a59d42a46f0 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
02122cbaa95dc00b28def2f64b3cd51c9b35f504 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
b743b0ca451ce23e36830fdcf6541a4a2688391c TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
806ee843dbaaedf4e180ceb229fc65c1596b8502 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
e796ad56e1d0d35f17df1659ee54c6661fb73cac TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange IfCond True Passed
  • Model Under Test
  • Equivalent Model
9a94dc26c487e3c5e106be3a8299e96d19fce335 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange IfCond False Passed
  • Model Under Test
  • Equivalent Model
ba0cc593d407ddb8e3f972472fc3177534c715b4 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange IfThen True Passed
  • Model Under Test
  • Equivalent Model
3e72542f4cbacc5812b9fba10863a048aa19c0d3 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange IfThen False Passed
  • Model Under Test
  • Equivalent Model
46207fc0efa5370993eedff83bc0694d8581aae4 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange IfElse True Passed
  • Model Under Test
  • Equivalent Model
a6b153578816f65025bc545a8b33ab1e02cc31c6 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange IfElse False Passed
  • Model Under Test
  • Equivalent Model
0e95a5eb27beaaef4135fb43a654532238d16d88 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange SeqLen True Passed
  • Model Under Test
  • Equivalent Model
ae7ac63f2b2716613a3cd82dc1c0b6cb11a7e787 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange SeqLen False Passed
  • Model Under Test
  • Equivalent Model
4084a94abab568ebe34df92687b47102f4e5666f TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumRange TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3d5fa25714fefc450bc959f74907c56867859930 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumRange TlcEval False Passed
  • Model Under Test
  • Equivalent Model
92905afa993e630b46584b46cb37e10298d0b478 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
1bac6aea5a0456b5c46296d800e2585a119fc7cb TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
7e24606fd5ededf54c338c22d275e963a65aea0a TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
f3adec253491cf9d53d2b410944af4b5bfcafe39 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
7cc5ea77c10cfd9e94e3b3b6f18cfff2671a10f2 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
1fdf257c50d76d6de05f38b2fef8de4a0592c409 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
ead603e37614112cd22b8ca6fa7fadf88e103197 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange SeqHead True Passed
  • Model Under Test
  • Equivalent Model
933a66adf5f1bb169d9b7c9bc958f0e8f59a5cc5 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange SeqHead False Passed
  • Model Under Test
  • Equivalent Model