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 FiniteSetsIsFiniteSet; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
fbb5e3b4ec985739ce931382c87baf463b8cbf0a TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet BoolSet True Passed
  • Model Under Test
  • Equivalent Model
2f94b53d1bc4b6752667e40e87ea37490b1eed27 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet BoolSet False Passed
  • Model Under Test
  • Equivalent Model
ca2a3a0a77287beace6f7217e51b189a667aa07d TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Let True Passed
  • Model Under Test
  • Equivalent Model
9df8cb4da00452f5d006dd65b8f593bab1ab0521 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Let False Passed
  • Model Under Test
  • Equivalent Model
e6346cfb2957113187edb9f22f86634b5a207b11 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
244c3ebad5c482f8d68bc414fe3f9ebdc35784e3 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
0d3d81fd2f07d4f7198dfb3c7a81bdce26b7d29f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Set0 True Passed
  • Model Under Test
  • Equivalent Model
2d4d3d4bd250d78285058878d7bb5cfff4b2f9ad TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Set0 False Passed
  • Model Under Test
  • Equivalent Model
76f2aa28f579244f3ef4c9ee05b1bd9cf7a3da32 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Set1 True Passed
  • Model Under Test
  • Equivalent Model
a954c412070e683115aed11c2b7bd725185ce78f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Set1 False Passed
  • Model Under Test
  • Equivalent Model
0bf56d634f507f062fdd6beffd59bc1807502d22 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Set2 True Passed
  • Model Under Test
  • Equivalent Model
5bc256c1a6657e00d80d42eaec28369fda13d56e TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Set2 False Passed
  • Model Under Test
  • Equivalent Model
f2295961761894c69f84f24a35cecc5736bc5f69 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Choose True Passed
  • Model Under Test
  • Equivalent Model
dccee0b86e5feaab903492c97912258dfe621aba TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Choose False Passed
  • Model Under Test
  • Equivalent Model
0fe06d0d0975eb64eb1181d7c5af492e57b453ed TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet FunApp True Passed
  • Model Under Test
  • Equivalent Model
b2edbd7ffa504c52fb573d52c4707cad807d3b7b TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet FunApp False Passed
  • Model Under Test
  • Equivalent Model
da1d7d9e454d49298325d05229db6e263dd18673 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Prime True Passed
  • Model Under Test
  • Equivalent Model
2633cb4eee6b54cfd3858f7dcd061c14faa8a02f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Prime False Passed
  • Model Under Test
  • Equivalent Model
010fc68fed07d361f2ab297ca745f202c24c37c5 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def0 True Passed
  • Model Under Test
  • Equivalent Model
fbb5f16682e48948597afa4f2da23deadb0f81d6 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def0 False Passed
  • Model Under Test
  • Equivalent Model
6d2f7778acb875228a89b76fc3738dd9d323d6f9 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
fff93bdcc3888176fb291272e9a55d839d2eb574 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
e65af7f6953e11ce63bd4863a007aa4860ddbbdb TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def1 True Passed
  • Model Under Test
  • Equivalent Model
c266843fcacf8cb51425c8439ede996086277209 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def1 False Passed
  • Model Under Test
  • Equivalent Model
c56c3ff81f1066debb54652b59b01273fac5edc1 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
cc21b40a98e782c35c3f2ed2d556e65b673acf01 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
2f67b0de460d09772a05d9c3154d75cac289f8d5 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def2 True Passed
  • Model Under Test
  • Equivalent Model
38475eacd2c8bb169404d63e9ed11e8081de08ee TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def2 False Passed
  • Model Under Test
  • Equivalent Model
d907e2b8ae4f12e89f63c96e037166b9b920afb4 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
bf023488dcebe223d9033e453556d27a6d83d498 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
8d87c35e87ae553addce88735fc47fce0daf4787 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
2f3c217ce9ac5120e7ec4b218e4f302afb0d8290 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
8fe390c008cf801151e722eedf223ed78ef787b0 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ee18db25f5fc9f8c89bd235617ca6c801c1c11d7 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: LET definitions are reduced to global definitions
FiniteSetsIsFiniteSet LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
5219d6ce7d173820d7770a2b0c909d890dce727f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Extends True Passed
  • Model Under Test
  • Equivalent Model
e6777e30ea0c9985959ec80f11ba8337c1c80c65 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Extends False Passed
  • Model Under Test
  • Equivalent Model
a832f2b03177926c5c5d04292843661b9269eff0 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
4c45b01dfeec021c6a0995d85b8259dd930a0e0b TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
d8e89f95a990df8b1f748e0efe96c37a990eac7b TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Variable True Passed
  • Model Under Test
  • Equivalent Model
ff26fb1d468ea799151723029b96e7bdd632b2dd TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Variable False Passed
  • Model Under Test
  • Equivalent Model
8f4feed34f9caadf55a82eedf5dc0f57fbb815ec TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Constant True Passed
  • Model Under Test
  • Equivalent Model
30a53113af8981ee708fbb1cf8d74f25bbc30c67 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Constant False Passed
  • Model Under Test
  • Equivalent Model
147e294cef7b7413c3665132b5073f9857355f61 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
3cf7ff7e2015b3a87b3ef50a8781e00abfe213be TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
28f4c073ee8e1a65a3daa11c2bba3ad8b66aa23d TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Instance True Passed
  • Model Under Test
  • Equivalent Model
c0075ebbf456cf270f49408a2646b503e9ab33f9 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Instance False Passed
  • Model Under Test
  • Equivalent Model
a223c83ad581eba4044b744b2174ff3f1dba5183 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
e4d87639c22ed326392a391cd8a83567308af02d TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
33442b56164be44ffb9b425f5c330316cfd609fe TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
24d77c3b813232f39bf75a8346419c9c2fb6f238 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
73eeec7a14be76b78983bdaae6439272fcd9b6b8 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
bc842f9549d7b407990449d71e2696294aa304ea TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
323bbb798ba96bb3643b84eff56e453956fbc7c5 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
387033c955e55aaf6e828e53745a84139375eaa4 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
ff090ec5e8ec5770500c6fc411e51ddbca0af658 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
24a217095e031b41aa8efb625d81040c5d0031e4 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
4ed3c50d4af7ad0ee737ffc3b37e6b9f581d5a03 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
f8dd919a64fb3531bd2e1c4fff5164767c31fc95 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
feac366d61d602ccd1622f1ed5ebfc9a4cb54764 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
0688644db827fc49d8e77bf52040168d1026b769 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
56a1adbae62689317af1f5a77aa2b0c815608749 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Cross2 True Passed
  • Model Under Test
  • Equivalent Model
6601bd2f759c2c5b2694014bacb9b82eddc6efe5 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Cross2 False Passed
  • Model Under Test
  • Equivalent Model
4edffca443a2033d87f540dea9fa6bd446838c32 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Cross3 True Passed
  • Model Under Test
  • Equivalent Model
4af2ccf5b9d341e81a40f964fe3abe386ec5436a TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Cross3 False Passed
  • Model Under Test
  • Equivalent Model
3eea33eac2f7693da725e77519887dbb75c911b0 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FiniteSetsIsFiniteSet FunSet True Passed
  • Model Under Test
  • Equivalent Model
7d92fcdffcb78d4e72b9573791cbb3d309840b7f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FiniteSetsIsFiniteSet FunSet False Passed
  • Model Under Test
  • Equivalent Model
65f50841c4f931a4e66d159204adb503f96e3070 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
FiniteSetsIsFiniteSet RecordSet True Passed
  • Model Under Test
  • Equivalent Model
99681ec0e3f3167d6c3b9f9d0a86f269eb3dfa41 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
FiniteSetsIsFiniteSet RecordSet False Passed
  • Model Under Test
  • Equivalent Model
1654c3d4707bf78035b9d468710c804ca7f20256 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetDiff True Passed
  • Model Under Test
  • Equivalent Model
c63c77a6f823a6be6e7c8e3faf8e9590f53ceab2 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetDiff False Passed
  • Model Under Test
  • Equivalent Model
282e79390ae050fdfc0f54bf640f10a476fe68d2 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetUnion True Passed
  • Model Under Test
  • Equivalent Model
9a00120b68332347989a59a86e12670e4b3e328d TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetUnion False Passed
  • Model Under Test
  • Equivalent Model
82ca2652e02cd82d86c55eaea98b6b6e829bc7a2 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
0ebd98acfcbadae3c9485d3ae2fbafdd5a22b95c TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
1648225c2d3e793373ee68d057ff44b9119fab7c TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IfCond True Passed
  • Model Under Test
  • Equivalent Model
f127314385b261fb05ae0d677440f9bc2a5a9f5c TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IfCond False Passed
  • Model Under Test
  • Equivalent Model
23b28627989d704f85a7f76ef6e0bee335fbc673 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IfThen True Passed
  • Model Under Test
  • Equivalent Model
e4692b6eb3c4bca42bab9dc03de09fe779dd09ed TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IfThen False Passed
  • Model Under Test
  • Equivalent Model
59e51540c2c731b249b6c4a2ffcb71d74772a128 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IfElse True Passed
  • Model Under Test
  • Equivalent Model
2c8e5d254e96563245a4cf51a89214158fcfc249 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IfElse False Passed
  • Model Under Test
  • Equivalent Model
420d0fb2a36b7d10337b926e540910f19b7cba19 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Subset True Passed
  • Model Under Test
  • Equivalent Model
40ae7d32c3e1015fcd205fb468362366651a9073 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Subset False Passed
  • Model Under Test
  • Equivalent Model
d9ecd9f50450fafb80ab3944550a5b3af8509cac TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Domain True Passed
  • Model Under Test
  • Equivalent Model
f481f47354061e47cc38f9d6a5f7e513b67589bb TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Domain False Passed
  • Model Under Test
  • Equivalent Model
8acbc13aa5bdb017e65ee04db36edb24d821b169 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Union True Passed
  • Model Under Test
  • Equivalent Model
7046168ab14ff47729b51cd6ccdfb414ede46ba1 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Union False Passed
  • Model Under Test
  • Equivalent Model
38f365e60ab3097a0595d81dead517922c5438d3 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SeqSeq True Passed
  • Model Under Test
  • Equivalent Model
6717eac93ae3f40ec78c1b4da7e7db2ecf861a3c TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SeqSeq False Passed
  • Model Under Test
  • Equivalent Model
275ac05756ef0ddc2b9456215acedc8c959823f1 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet NatSet True Passed
  • Model Under Test
  • Equivalent Model
b266b317154a8085295880e8164e6fbe7c595ae7 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet NatSet False Passed
  • Model Under Test
  • Equivalent Model
665e71eddb22111536affb76507082a702dbd871 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IntSet True Passed
  • Model Under Test
  • Equivalent Model
d1e286a1084c37053079a3d12986c36f5b2afe9c TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet IntSet False Passed
  • Model Under Test
  • Equivalent Model
80365cdaa2bed0d9aa9511dfd48d4b9a31534e63 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet StringSet True Passed
  • Model Under Test
  • Equivalent Model
6a3afb40f2c51585c888ce7a17a59a625491fe38 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet StringSet False Passed
  • Model Under Test
  • Equivalent Model
97f9e92d60351a0f7234d19aa87daa18461b243b TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug 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
FiniteSetsIsFiniteSet NumRange True Passed
  • Model Under Test
  • Equivalent Model
daaf44334143d362150d0e60ded6e6e0cf974839 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug 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
FiniteSetsIsFiniteSet NumRange False Passed
  • Model Under Test
  • Equivalent Model
b2841fea811ed7aa2ca0e85e7448500fa10b70ae TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FiniteSetsIsFiniteSet TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
9ffbba8ef2da57992519aac88b370ce45c3af09a TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
FiniteSetsIsFiniteSet TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
0805939686d6928dbe2f9a6928805db423e932a6 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: TLCEval(expr) is reduced to just expr
FiniteSetsIsFiniteSet TlcEval True Passed
  • Model Under Test
  • Equivalent Model
337fadb8cb2cad6c748bca55589bec1d1837e345 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: TLCEval(expr) is reduced to just expr
FiniteSetsIsFiniteSet TlcEval False Passed
  • Model Under Test
  • Equivalent Model
4f97410cb623653ff9c6fadb7f8b13c5bbe0dfe6 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
fa4823b8d8a8ca15453c4c53ae5acacfcc0a3fe4 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
ab4dfa6398209f24514b72d463bcc19b903c2c70 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FiniteSetsIsFiniteSet BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
71d9dca7bb4371113d89657b48b193f104e5a323 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FiniteSetsIsFiniteSet BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
a51e076c5aba0312946753a258e3ba7fc704cc46 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SeqHead True Passed
  • Model Under Test
  • Equivalent Model
3289c9aef9a78a542944a87bf39475f71f30ec5f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet SeqHead False Passed
  • Model Under Test
  • Equivalent Model