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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
2d2f45e342c2a40659c1963c305c39580e44ce8e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Replace spec with the same without comments
Except1RecWithAt OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
4efa87021eb91c05c3f8f35758d82bc0aea8f88f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Replace spec with the same without comments
Except1RecWithAt OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
540ce4a243c6976a4ba37d83d3aed305b639bfac TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Replace spec with the same without comments
Except1RecWithAt MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
6641d86efe8d1a322953bc7060b4fa8b504cdc84 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Replace spec with the same without comments
Except1RecWithAt MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
93579d662a5e98df969a9e33d383f2430c8bf972 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
889a22708a74ece6c26a6d6ffb85cc53fed5e0c6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
1e56b9f5deef7fa4aa8e2fbd0b372e38fb5b4172 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
eca583272a4e933322f1db5e3158b7bdb660cb21 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
184ce5a97fd5a2cfd30834c3cbdd955252c23552 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolSet True Passed
  • Model Under Test
  • Equivalent Model
5d7eb00186f039f19ef8b3bea5e9e575b4e71d88 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BoolSet False Passed
  • Model Under Test
  • Equivalent Model
83ed5fff341f881bcc5225bd8f2e2d15ebd3d9e1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt And True Passed
  • Model Under Test
  • Equivalent Model
f1d7f915673731a4c3939651b7b3731ae7ae46c9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt And False Passed
  • Model Under Test
  • Equivalent Model
533ec007b2468498b0cf7bfce431fbe07b0a3870 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1RecWithAt AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
258d3787aa5007b44de8b5d927454c0e0b0ea447 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Except1RecWithAt AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
cec07143875a0aadd2d977c00aca65973dae7c4a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Imply True Passed
  • Model Under Test
  • Equivalent Model
7414e03bd4f94ae697b2f920ddb7b8b28617bc1a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Imply False Passed
  • Model Under Test
  • Equivalent Model
3229fdb09a23b2df7d810559894a7563e672e845 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Not True Passed
  • Model Under Test
  • Equivalent Model
77be4eef3f4dc78f24a69244aa40274d456be958 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Not False Passed
  • Model Under Test
  • Equivalent Model
9d7bacba6ae918adae38ccd5402de46342b29e1f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1RecWithAt Or True Passed
  • Model Under Test
  • Equivalent Model
8e7d9e1d194cc347c98da06ece25859fa1510c57 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Except1RecWithAt Or False Passed
  • Model Under Test
  • Equivalent Model
5315a303f57f914d89279f5d473110ad683d751a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1RecWithAt OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
023178401f675ffea30a2f37e96169547016a0a1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Except1RecWithAt OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
240d1576fb3c232baf343b764146a15ffc14f5af TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Eq True Passed
  • Model Under Test
  • Equivalent Model
72dda7ce84ef9b478aa586134bace9d970096863 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Eq False Passed
  • Model Under Test
  • Equivalent Model
b7dbcac6c9529cd4563457fdbcbdec2b3445272e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Ne True Passed
  • Model Under Test
  • Equivalent Model
471893aeee11b1272b66e02862f86789e567dd1a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Ne False Passed
  • Model Under Test
  • Equivalent Model
4490481a7ac1162638de351eb1607061ad444c9f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Let True Passed
  • Model Under Test
  • Equivalent Model
aed804059ecab539d00c557bfbe43541aa42ebc4 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Let False Passed
  • Model Under Test
  • Equivalent Model
c0dfea64b0e844360a3df54dc9e91f851705ae23 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
c4a168146a2c3694b3254672237f474479313639 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
12e976241a925f92783d85c1d01eca79bc6b1904 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set0 True Passed
  • Model Under Test
  • Equivalent Model
0bb29fa0c52da06c3bbc4d54205c9594090219a9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set0 False Passed
  • Model Under Test
  • Equivalent Model
26281f2b1311b85b92a551d42119c91990efd02a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set1 True Passed
  • Model Under Test
  • Equivalent Model
07f0189a4a11a28829a941a86e579f27e4abf7c2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set1 False Passed
  • Model Under Test
  • Equivalent Model
f163c367655f22408de2f7c5b76b02a72308278b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set2 True Passed
  • Model Under Test
  • Equivalent Model
4696b1867c1ccb09c189b5163ed57d820024ecaa TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set2 False Passed
  • Model Under Test
  • Equivalent Model
db1ec0aaed3e8a3a63cd61d24159dcb22137132c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Fun True Passed
  • Model Under Test
  • Equivalent Model
408aa902977b99c0df9287a9f60abb2948af7885 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Fun False Passed
  • Model Under Test
  • Equivalent Model
2efd7beca87334798dda1a5dea5618acac1d1551 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt In True Passed
  • Model Under Test
  • Equivalent Model
659118eb57c456f05ec9daabefbcc8f75877a58d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt In False Passed
  • Model Under Test
  • Equivalent Model
d08e1020e6c2afd21ab302ea45e3522c67fc0815 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NotIn True Passed
  • Model Under Test
  • Equivalent Model
6eb603ef7ea825e0e0940099e6e0de86c3709f84 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NotIn False Passed
  • Model Under Test
  • Equivalent Model
c53379140a0a6fdec06509b9ee96ad7cdab4ed7f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Exists True Passed
  • Model Under Test
  • Equivalent Model
25dc159fcb84a14bc417c2f618b0984135622fe1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Exists False Passed
  • Model Under Test
  • Equivalent Model
a942a0e1e2fae9c9e1756a63e4d20b1721a090f8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Forall True Passed
  • Model Under Test
  • Equivalent Model
98ebd3f69a8cb960ba00e680a1cb7dd6fdd06ee6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Forall False Passed
  • Model Under Test
  • Equivalent Model
38c1d525cee9a10cb943da2f24d90b94dfcc9ab5 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Choose True Passed
  • Model Under Test
  • Equivalent Model
2cf31d5a6a943319c40ba05333303426835aedf0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Choose False Passed
  • Model Under Test
  • Equivalent Model
ee864f7db931fd57a13f13915816063b3eb7d2dd TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Record True Passed
  • Model Under Test
  • Equivalent Model
c73b2262ded03727c4e7bd2cb381f1fc4157eb77 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Record False Passed
  • Model Under Test
  • Equivalent Model
2b288bffadfb136eb76b425f947941b01863a75e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Tuple True Passed
  • Model Under Test
  • Equivalent Model
127a959fa1e054f5ecf5417d698e4bd79d53ee1b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Tuple False Passed
  • Model Under Test
  • Equivalent Model
9ddb5f14afa6043d8e7669abc805b487234618bf TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
4833a5a7a1178f5e36ca9127915b4ef2442a073f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
0d86c41cc570be91822501075cb0acb7956b8842 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt FunApp True Passed
  • Model Under Test
  • Equivalent Model
edf93fdcd1e43ed1ccc2a5218b1cc1388905fa7c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt FunApp False Passed
  • Model Under Test
  • Equivalent Model
2d97199f40c32dc8625deccd991974c51257d2b4 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Prime True Passed
  • Model Under Test
  • Equivalent Model
71687290f4887808e1d7fe220f3480808381f0d8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Prime False Passed
  • Model Under Test
  • Equivalent Model
1149feba3b864167581f55dd44b6d84e875a960d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumZero True Passed
  • Model Under Test
  • Equivalent Model
ce6c83f62d0e87c49f900c54965797023e10d6e6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumZero False Passed
  • Model Under Test
  • Equivalent Model
5c60799ccbeea52b2dd73d1187ac6a35be693071 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumOne True Passed
  • Model Under Test
  • Equivalent Model
18ad671ee1cdba08cc4972c13db3289506ecd070 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumOne False Passed
  • Model Under Test
  • Equivalent Model
1d8e8cabedcdf3049fdf67bae1d035fc92ecc00e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
9080bda1f87ba8c6800e81937dc025772b8cc917 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
7fc964f730ed30bda3b53af4ee9509796cdfcf2e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
194838203128d4c990edb2ff3f6c42b29203273d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
6dee216df3120201abaa6b7400ac2e064717e2a2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumPlus True Passed
  • Model Under Test
  • Equivalent Model
8a5437c0fb7c8bc5a73084a2faf6ca4eda2a51af TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumPlus False Passed
  • Model Under Test
  • Equivalent Model
577b94c287e464a01111a680d04b33d29a8a7078 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ff1ac7f0568b4f90c73c268e8bf34a1c9e17ad3e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMinus False Passed
  • Model Under Test
  • Equivalent Model
d98517384bc76b92348d3c45d5534aa70cc94e75 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMul True Passed
  • Model Under Test
  • Equivalent Model
6b741acd10dc9b6ee50f51412237d016ba70a0dd TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMul False Passed
  • Model Under Test
  • Equivalent Model
5d3339ae61c6dab5169ed9adaaf29f2b5f099911 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumDiv True Passed
  • Model Under Test
  • Equivalent Model
79189fe89501b4e33d77940fc0cffb5e43704024 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumDiv False Passed
  • Model Under Test
  • Equivalent Model
338fb26d526ae4579f461eb7d1c99f783bc21ced TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMod True Passed
  • Model Under Test
  • Equivalent Model
de78b0cd7e7cf386dcf372c7031be919e09d8c53 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumMod False Passed
  • Model Under Test
  • Equivalent Model
53837a3897d0c1510adac207f60a33a25fcefe50 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumPow True Passed
  • Model Under Test
  • Equivalent Model
7354ff7b0e4650e69babc0f74f14b72794abab1f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumPow False Passed
  • Model Under Test
  • Equivalent Model
32775217f4b523d3ca4c323f16cf38494921e8bd TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGt True Passed
  • Model Under Test
  • Equivalent Model
95224c623066e5b6d47aca5d09d13fdf3b475829 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGt False Passed
  • Model Under Test
  • Equivalent Model
7953e2cf24cf388a68232c9ca5e1495d28c9dda6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGe True Passed
  • Model Under Test
  • Equivalent Model
e9bee7413e846d421dd5ced419f9778f6d41cf3c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGe False Passed
  • Model Under Test
  • Equivalent Model
159f3636265793e81b1088f9026c745df489559d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumLt True Passed
  • Model Under Test
  • Equivalent Model
d6f77dcd5e891de0299529e9730f02490d13b480 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumLt False Passed
  • Model Under Test
  • Equivalent Model
9f22c2a3fd158640cff3ab516328710ea7c779dc TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumLe True Passed
  • Model Under Test
  • Equivalent Model
c16cbc1e2d10ff850041be6ea7332f661338edee TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumLe False Passed
  • Model Under Test
  • Equivalent Model
9644d47d724f57f391278c6ef4d00454dda91db0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt DefFun True Passed
  • Model Under Test
  • Equivalent Model
4ec0ee90cb4938b5a95bb41c9e6f74c0ca0dee13 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt DefFun False Passed
  • Model Under Test
  • Equivalent Model
3f8829160a201fe9b9771f4ff33a6460ea77ea80 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
00a322201a4b44f118db581a34944735df90ffae TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
3dfbe2f464364dbd2dc9bacb7f13f53625c44993 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt DefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
8dada14b6be6206a4f39fc12732bfda0341c1df6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt DefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
4d39057005041b5e8501c2d09e2e1ade5b754542 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
ca8804d8d840d2aae653a3faef8205f098eaf125 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
c586fc73a2930bdbb859a5f34d6039b163f0c7d2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def0 True Passed
  • Model Under Test
  • Equivalent Model
62f1d248d80f68c48fefee7a1fce60114a06f8aa TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def0 False Passed
  • Model Under Test
  • Equivalent Model
86721c093df02d1f8e753ee5cd73759ac82cabe3 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
2c4cab3022ee9b155fe43c3b05c7634f7600a32a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
8b73d2e15f7dd0f9c4ca0b60730311f35e206d93 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def1 True Passed
  • Model Under Test
  • Equivalent Model
4404e5a37c30f64e08144ba92785890156b8ec0d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def1 False Passed
  • Model Under Test
  • Equivalent Model
8cd91c092ba84bb004279c1dd41f946d3048d6b6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
c490a32b6dd4eae042700c262f20a89ff4d128b0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
165aa9260733a59479d2aacfbfaee920b0511682 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def2 True Passed
  • Model Under Test
  • Equivalent Model
6da3775d8f55315afcc07552e960d788dfe19c1b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def2 False Passed
  • Model Under Test
  • Equivalent Model
fc71119f443134e6e0e3ad21347971b595a9ce12 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
d8aff8b4f2bd04369b92089cae7d547d5af17314 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
cd904aa5a2f3fe6b87d862d89af17ce155923023 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
5ec1dc8246a9ee62ba15413c13956ec99a366873 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e32856a3065734fd5fbac76192209146835f0f84 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dc30c07a9cdb6815cb63dea9936f12c92808af6b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: LET definitions are reduced to global definitions
Except1RecWithAt LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e61b7e95607117c568bb00bd0763ed47b1601841 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Extends True Passed
  • Model Under Test
  • Equivalent Model
de31847f2a0fde3646b1e41494ab7942e51c2378 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Extends False Passed
  • Model Under Test
  • Equivalent Model
f9ef88489cce1f774fc929105e8c876981aa58c8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
68182d60ee2b4affa11815d7d0c0ca1c5dac47ac TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
603cd135f4249d6ca68c8cc73770c5dc369d96a2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Variable True Passed
  • Model Under Test
  • Equivalent Model
0bd88ae1918ea7a2f192e7527da79a355aacccf6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Variable False Passed
  • Model Under Test
  • Equivalent Model
5ca4ea991c730f53f9cb20814bbcc147add8cb7b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Constant True Passed
  • Model Under Test
  • Equivalent Model
d56ffb3b89d63b0500f47065a5992d8dd6ba866f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Constant False Passed
  • Model Under Test
  • Equivalent Model
af79c12240bd21c520c889b4a933a36ff1ba3a8c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f89a11650d91c57e240d7d13705cbe85c12fcad9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
00e264526dcea1f815c908a7dfd3244627145f98 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Instance True Passed
  • Model Under Test
  • Equivalent Model
a4d8d2d4fa4fc6d909f2684b48aaafa61a0b5d1d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Instance False Passed
  • Model Under Test
  • Equivalent Model
e6bf998eacd5605f36b1c3d7708e8096b0dee969 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
339b31382eb7267a1aa731c98ca86644cd5ca9ce TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
dfc57043c719d2f4f9cd8b003cf1fe4a5cbc69f0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
ef09d7539b4275f121a2f5a0d147d91f13fc8562 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
9622b9ca48c95154e909d896da669cd26c2a49fc TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
4f1f80beb412601b44fe415b6e795b301f3fd6e8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
1da9a178c80817be9f723a46d988aeb882611fbb TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f0abe957eeebb792e3df7e504eb598370bbc7270 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
26dd69598d6e004973c8d0046e1f9f7323b3cd34 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a3544100b80feae1bd122b9a2286c9d5f4712304 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
37d315cdfdf8092f09c84ad69e8d58c873a0cf1c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
fafc7fc029a9d66386a252564e3cd523434f1287 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
a5c3995d0069ad6f71c9e03983ff23b68d4ad77d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
cbbef3ac2b224013c00f80c4021cb9fa9d43fb19 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
479af36a3f22d65bc6dad5fb0da7ef04cc3ed3dc TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Enabled True Passed
  • Model Under Test
  • Equivalent Model
bfe0fab9c95642a705d28d9e06624cd24d50ec1b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Enabled False Passed
  • Model Under Test
  • Equivalent Model
b58d86f78362c31042a32b9df6134178fdb8066f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Cross2 True Passed
  • Model Under Test
  • Equivalent Model
a085d69614e523cf96c10605b17e62b913c6bf38 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Cross2 False Passed
  • Model Under Test
  • Equivalent Model
c1961f726a54489ca91059f4367847014a22cafc TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Cross3 True Passed
  • Model Under Test
  • Equivalent Model
48a0b3c521a7726654759d147261a76f130c24b1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Cross3 False Passed
  • Model Under Test
  • Equivalent Model
1b7e1d6e54fa7e32b169690b05802f9138e4e6c6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • 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))
Except1RecWithAt FunSet True Passed
  • Model Under Test
  • Equivalent Model
294a0f602a93948279fdefce61b0cbd060ccb256 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • 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))
Except1RecWithAt FunSet False Passed
  • Model Under Test
  • Equivalent Model
f7aad6f932c082d8c42298ef5cb693bf04fa0734 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • 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)
Except1RecWithAt RecordSet True Passed
  • Model Under Test
  • Equivalent Model
2ecffba2a49818237ab287fc0caf6e88298977e5 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • 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)
Except1RecWithAt RecordSet False Passed
  • Model Under Test
  • Equivalent Model
209c144bb538fe8800d6e9b415d8464532b52b1a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetDiff True Passed
  • Model Under Test
  • Equivalent Model
4cfda656bbfc64202be8573fb4e23315eda57e25 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetDiff False Passed
  • Model Under Test
  • Equivalent Model
d600753a85fd024e28dade6f475e9720fff16a0b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetUnion True Passed
  • Model Under Test
  • Equivalent Model
08905fc38ac557fe4a568c1e574e51f1c02af224 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetUnion False Passed
  • Model Under Test
  • Equivalent Model
ee7482bc2657de78a504537c047b163473bf16fb TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
079c429c076aea433f584e9ecd702b050ab22dd8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
03928a7d98f416bcc52f2234716136af8181d859 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
745e2864ba7f85c5aa402ee63643da424513e4c9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
8dd43f9c05d898c23e6a25f70e6a39c726ddfe59 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfCond True Passed
  • Model Under Test
  • Equivalent Model
a7184dff2677e75f1037504506368bbc17b38b7e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfCond False Passed
  • Model Under Test
  • Equivalent Model
d8ab2649dc05aaa64c76f1b59dfb9b649272263d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfThen True Passed
  • Model Under Test
  • Equivalent Model
4855581a26b9d46397e0b1b04d7730fc32865ecb TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfThen False Passed
  • Model Under Test
  • Equivalent Model
4354787c0f3a8485e3afc09f01ae3eef0633a43b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfElse True Passed
  • Model Under Test
  • Equivalent Model
64bbaaa276a08da39dc9e7a1b890a2fed3fd3b10 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt IfElse False Passed
  • Model Under Test
  • Equivalent Model
5b31e4a5d427773758aa0e3e6882e07d00c848cf TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Subset True Passed
  • Model Under Test
  • Equivalent Model
e90ea7aaafe3cf88958706dda20c9860901a986d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Subset False Passed
  • Model Under Test
  • Equivalent Model
2441fedef58a1aceccf8c39d31c54eabddfc0f81 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Domain True Passed
  • Model Under Test
  • Equivalent Model
2c97eef4c9960fec4a3c55821557fff9b8635867 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Domain False Passed
  • Model Under Test
  • Equivalent Model
7b1e191dfdee270197caef2991376b201320f4ba TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Union True Passed
  • Model Under Test
  • Equivalent Model
5dbe12f789b877040962206e94b09777d21f92aa TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Union False Passed
  • Model Under Test
  • Equivalent Model
395669ebcb92fef4a08c5e6a1a50424b30281218 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Unchanged True Passed
  • Model Under Test
  • Equivalent Model
392eec0e47be6727b4b24630a8ac6f410033204e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Unchanged False Passed
  • Model Under Test
  • Equivalent Model
33a5b68db3940fde58fbfa76228e5160b3f5e901 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Equivalence True Passed
  • Model Under Test
  • Equivalent Model
964e8190235de416aa08d8f5f6eb1e4aadd67b9f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Equivalence False Passed
  • Model Under Test
  • Equivalent Model
19be286116f17d8973e9b5c53c46d3b6b8cb3e00 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
6635e542a53ebd712dc27994f74b1745ced80010 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
4f18820e0a4ed0db87252e3f8d9d3dbd30ea59e6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt String True Passed
  • Model Under Test
  • Equivalent Model
6588685dbc201a4a4a56f9c0d77a861240744801 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt String False Passed
  • Model Under Test
  • Equivalent Model
99a1af680d8df2c6bb2ee15da983d8bac40562a4 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqLen True Passed
  • Model Under Test
  • Equivalent Model
a9e12580d0c236976c57f294c05c06d69ab620f0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqLen False Passed
  • Model Under Test
  • Equivalent Model
ab60c2086502db49296459bcd4d1047944de1526 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
a371e80bcd2b0ad618d1ec6efc5d450599915dfc TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
f9a10f220a4b09fb9ade82ec671d40dcc611e573 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
7f3bfbf6b82f2dc7bceeaa0a750ac303cdfc8173 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
7c01ca0f0b2412a69f636de8997dee9cfe6b2889 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
9a6c671e344e3cb9d211bd1b95bef659aa283230 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
efc9c210e2a397a58b86f96e97df67f59c746991 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • 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
Except1RecWithAt NumRange True Passed
  • Model Under Test
  • Equivalent Model
60d933842379a0816a394960599780d398e40d0c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • 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
Except1RecWithAt NumRange False Passed
  • Model Under Test
  • Equivalent Model
eba4732113944b35946818e951bda2da0e5308d1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1RecWithAt TlcSingletonFun True Passed
  • Model Under Test
  • Equivalent Model
1175b21d387287e35523930b7416386dcab2659a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Except1RecWithAt TlcSingletonFun False Passed
  • Model Under Test
  • Equivalent Model
2791ba2c9ecf0b31e183c059acc5b252e2859d13 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
Except1RecWithAt TlcExtendFun True Passed
  • Model Under Test
  • Equivalent Model
f3cef757cc6b8c8ab8256b5ffb515dbb8780941d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
Except1RecWithAt TlcExtendFun False Passed
  • Model Under Test
  • Equivalent Model
e1e6f70cfc34d39094416ee178216424df81d578 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1RecWithAt TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
1715169133242cec1ad392b3864ae39e34044cfa TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Except1RecWithAt TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
0250b34b0baa6a5780c15989d054f2a8c39595b2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1RecWithAt TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
130af58758d8c27570881e5c2548f84dccab3031 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1RecWithAt TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
c3d0ae8839b5fb77bb1d0aaed32bced66851bf04 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1RecWithAt TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f23b165c6027cda24b64991e33e702ee0c68b24e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: TLCEval(expr) is reduced to just expr
Except1RecWithAt TlcEval False Passed
  • Model Under Test
  • Equivalent Model
6f5f5d57eadd56333fe31a1cd20b182e819ff1cc TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
9248c4759e7d82f3b460ec16ee8792204a49edb3 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
9bc2433b993b81a47426a25fffa1fe6be475f77f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagSetToBag True Passed
  • Model Under Test
  • Equivalent Model
4ec8c61f6b00a24bc9e29f04e6f46a32785a7b23 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagSetToBag False Passed
  • Model Under Test
  • Equivalent Model
dae30049a3b60238cba55c9ac40fedbc19f4b099 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
b2f550b970ae84e1e3e98ad90a965e2eee87d623 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
71b628e4d2d30fd9853cc4af6d0ac1de19e50f66 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagEmptyBag True Passed
  • Model Under Test
  • Equivalent Model
ed5df4011c4352fd72b390735b2219306557d59c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagEmptyBag False Passed
  • Model Under Test
  • Equivalent Model
49e1472f024eaf1f76603d4428c2f02ea6a1ec13 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagAddBag True Passed
  • Model Under Test
  • Equivalent Model
baba7737c1675d392fc1020f55da47dc8d210389 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagAddBag False Passed
  • Model Under Test
  • Equivalent Model
6d68567234721ec9e60a6863ee09f2fc2fa2d049 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagSub True Passed
  • Model Under Test
  • Equivalent Model
8abec1250a32c74a5a61487d84ea0933dd65c348 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagSub False Passed
  • Model Under Test
  • Equivalent Model
eed693444d269bd9daceee69572c58e51769b172 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
92d676869c2cbd11f158fe4027c94659f0d81854 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
d28d4ce336e5d7715d74bd73d0c8a9e268632376 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
7e174916e39bffe1b74faa6c29af52d95060adb9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
745d84370292fb182f7d2fcc849045fb66d04eb7 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
5ec2062275efb51d964f2bf57561e0b4a0c8f768 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
2b9b69a299b7282069ff27101c0c361ac067a559 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
ce8699241043a1e23f4d3f2dcfe01b9c582a2f8b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
8db17b737776c2e0dc32e28174e9fd58b0e609a0 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagOfAll True Passed
  • Model Under Test
  • Equivalent Model
7ce5a69b9920519ea3f20cf8441a80ff7f76a3d6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagOfAll False Passed
  • Model Under Test
  • Equivalent Model
60b74805d2bb78095d2b898e5e794bdfee629282 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1RecWithAt BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
84dd46c991f19ec17a9bbb972b8c2780bc29bf96 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1RecWithAt BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
4522f31987c35843a55f252f437297e2518fc202 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1RecWithAt FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
f5dc1b68e7ec74828f7a09afb51cf534037ba2b7 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Except1RecWithAt FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
e3793868ae631bf1c6c727cf3bb5ed0b843d6527 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
526f9c8dd62e5439f6f685d4b33b49ce7b2084d9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
31de2ca409a90a76bdc89fd95a04ff668709367c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqHead True Passed
  • Model Under Test
  • Equivalent Model
9f380281d320a1080b3a9f5383a094a888cad150 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqHead False Passed
  • Model Under Test
  • Equivalent Model
94cb5528739d21ef32a6331ac39ebb1b6fa1bea7 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqTail True Passed
  • Model Under Test
  • Equivalent Model
2398cba01fb2bc130b6fae7b1e4f385894604899 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqTail False Passed
  • Model Under Test
  • Equivalent Model
c6114de411d8f5ab83efd7c6bd60184e0c35247b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
d072a78a4ddbd13b520e70789fbd3704cbaf47f4 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SeqAppend False Passed
  • Model Under Test
  • Equivalent Model