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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
063a3e15d2f5b71c40f6be2cb679d41efc5cc364	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Lambda	OneLineComment	True	Passed	Model Under Test Equivalent Model
b14cee145e0b9b3965c96f1abc6d3fa857814302	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Lambda	OneLineComment	False	Passed	Model Under Test Equivalent Model
0b2e0ce649567fc1f36c9b614f78c19a9ca89a4a	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Lambda	MultiLineComment	True	Passed	Model Under Test Equivalent Model
1aab90aba709b5f678ba2447f4c9834e2ba9f4fd	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Lambda	MultiLineComment	False	Passed	Model Under Test Equivalent Model
1656b0239965b32e9e8d836d3075b2d55d15c59a	Apalache	Lambda	BoolTrue	True	Passed	Model Under Test Equivalent Model
be724b3106283d090b05ec11a25a31d5c064a05c	Apalache	Lambda	BoolTrue	False	Passed	Model Under Test Equivalent Model
98f6a57bd6736530c61a3d28468e53305c2e1ba7	Apalache	Lambda	BoolFalse	True	Passed	Model Under Test Equivalent Model
50ea1e9f54ff3874c4e28ef3cab6e925a226ea5e	Apalache	Lambda	BoolFalse	False	Passed	Model Under Test Equivalent Model
d2d9b20bc670c5cc255988f0329661b2a6f01d65	Apalache	Lambda	BoolSet	True	Passed	Model Under Test Equivalent Model
9e128778ad2caef95476d398dab68de35eacc864	Apalache	Lambda	BoolSet	False	Passed	Model Under Test Equivalent Model
fb0ea992400043826e0e2dd293af5a5a42d7b976	Apalache	Lambda	And	True	Passed	Model Under Test Equivalent Model
b1acdc641bd2ed8f01824b87a2c588f9ba3c2b3c	Apalache	Lambda	And	False	Passed	Model Under Test Equivalent Model
46445949b0e87133a8641c23e5fbc244d3caf689	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Lambda	AndMultiLine	True	Passed	Model Under Test Equivalent Model
154d4bb5f4bf87dd5f213811d778390693820520	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Lambda	AndMultiLine	False	Passed	Model Under Test Equivalent Model
010406c9841522b35a1f7b4d04e15e8718786064	Apalache	Lambda	Imply	True	Passed	Model Under Test Equivalent Model
f57a3015ea236f861ce0316d18b6b19909279d14	Apalache	Lambda	Imply	False	Passed	Model Under Test Equivalent Model
5ad8f1468be36eb0fd6b3108fed35827132cf032	Apalache	Lambda	Not	True	Passed	Model Under Test Equivalent Model
f7b76d27b6954261b997535d72efcbe60aa6d13e	Apalache	Lambda	Not	False	Passed	Model Under Test Equivalent Model
90d9739bd1d6afe8cae660f6ebbcda3911a58b87	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Lambda	Or	True	Passed	Model Under Test Equivalent Model
fec5d9cc99c80bb0ba6f7ae1b0f33a3112449845	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Lambda	Or	False	Passed	Model Under Test Equivalent Model
1ef347f4354a39cf223212284b51745863760157	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Lambda	OrMultiLine	True	Passed	Model Under Test Equivalent Model
84e2dc3090f15ce856f9590f927d56456a5f45ed	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Lambda	OrMultiLine	False	Passed	Model Under Test Equivalent Model
b4b5c11bcafc3902f696b5cd9f1bb5abde17e5df	Apalache	Lambda	AndProp	True	Passed	Model Under Test Equivalent Model
f303aa5e42691b3a13ccb23436d27cc53f9d5e88	Apalache	Lambda	AndProp	False	Passed	Model Under Test Equivalent Model
b25a22e9df9367b51dc51b5adb0e198e943d03b5	Apalache	Lambda	Boxed	True	Failed: TLC does not support boxed operator in LAMBDA expressions and reports an error	Model Under Test Equivalent Model
4435a5467f708d6ab63fc8edd9966dbc27a3e96e	Apalache	Lambda	Boxed	False	Failed: TLC does not support boxed operator in LAMBDA expressions and reports an error	Model Under Test Equivalent Model
6f6bc9d9e74963b03c2eeba8bedfd12e348b721c	Apalache	Lambda	Eq	True	Passed	Model Under Test Equivalent Model
7321a06c816ecda5c3e5847a4d3fecfe4d7fde0e	Apalache	Lambda	Eq	False	Passed	Model Under Test Equivalent Model
cf1048a911bac5be62eefc006ac411ef8209a8ea	Apalache	Lambda	Ne	True	Passed	Model Under Test Equivalent Model
006c59cdc786749b10209a9d48ba1f4362787c5f	Apalache	Lambda	Ne	False	Passed	Model Under Test Equivalent Model
e5b044149ebbc21ca8f7114d6f8631bb447f2f5f	Apalache	Lambda	Let	True	Passed	Model Under Test Equivalent Model
3494b027929168b299115d7adeb0f3df138f5b90	Apalache	Lambda	Let	False	Passed	Model Under Test Equivalent Model
d049425cd6bb270ca61ac3036abd179e62176759	Apalache	Lambda	SetEmpty	True	Passed	Model Under Test Equivalent Model
b68078ed13fd785ba530c0d7322fd8a146a1fe5b	Apalache	Lambda	SetEmpty	False	Passed	Model Under Test Equivalent Model
13ad0e1b4c7c1b82acf5d5d3f9e9203943f86156	Apalache	Lambda	Set0	True	Passed	Model Under Test Equivalent Model
d9b0dfb56c67f141e1e074f3844ca7a12571175f	Apalache	Lambda	Set0	False	Passed	Model Under Test Equivalent Model
4ff48ca21a2c9f563f26a0ed04075d01bb8b11f4	Apalache	Lambda	Set1	True	Passed	Model Under Test Equivalent Model
f7f35d0f2c1656563160891fb6fe4437f3ace7ea	Apalache	Lambda	Set1	False	Passed	Model Under Test Equivalent Model
b052856fdc1197c0286c38af0ab2dd9b4b0d9069	Apalache	Lambda	Set2	True	Passed	Model Under Test Equivalent Model
97d58d460bec5e3095423f307cdb356c01e4b86f	Apalache	Lambda	Set2	False	Passed	Model Under Test Equivalent Model
bced6d61a750336a1bb1800ef7b9ff39b4a4eb3e	Apalache	Lambda	Fun	True	Passed	Model Under Test Equivalent Model
b20f547cd73d14029dd8a25497d15dc57b58bf0c	Apalache	Lambda	Fun	False	Passed	Model Under Test Equivalent Model
119cfef18be70ffeeea9496ef7a8f9ae7e919d3f	Apalache	Lambda	In	True	Passed	Model Under Test Equivalent Model
a409c2089a4afd620edb783886b5edea39e5712c	Apalache	Lambda	In	False	Passed	Model Under Test Equivalent Model
e39dbb7195c8a96f29a1a2de2afe73930f9ffc31	Apalache	Lambda	NotIn	True	Passed	Model Under Test Equivalent Model
47c7f0a48d4a3518ea936f4e8d3e0da5b30947de	Apalache	Lambda	NotIn	False	Passed	Model Under Test Equivalent Model
1c15a66f277e42aa838b9487b12a49b4c0437648	Apalache	Lambda	Exists	True	Passed	Model Under Test Equivalent Model
dfd76f2a8d6583bbca288d3899cc11993ca62ffd	Apalache	Lambda	Exists	False	Passed	Model Under Test Equivalent Model
949fcede39d65c8eef26c1ffbe56060063ee5200	Apalache	Lambda	Forall	True	Passed	Model Under Test Equivalent Model
7253c14011ca84f19048909b1d9df5b96d19db5d	Apalache	Lambda	Forall	False	Passed	Model Under Test Equivalent Model
0a6094d460eeaabea885a1f97183b3f37c3662b4	Apalache	Lambda	Choose	True	Passed	Model Under Test Equivalent Model
d8fc305124c2318d1510ecd1f1ec812786dbede0	Apalache	Lambda	Choose	False	Passed	Model Under Test Equivalent Model
c2148e1070e84860a6e477cc52f1770ed5975b2e	Apalache	Lambda	Record	True	Passed	Model Under Test Equivalent Model
0b4f2e07d2ade199f863843227aed14cb065bc54	Apalache	Lambda	Record	False	Passed	Model Under Test Equivalent Model
e67225c10934de7f67643beff679f77226bcbefb	Apalache	Lambda	Tuple	True	Passed	Model Under Test Equivalent Model
61fbc9c06ab9dffeff64e6867b9a3ba761d1c3e0	Apalache	Lambda	Tuple	False	Passed	Model Under Test Equivalent Model
185a73404334cb2f9e93e476ff531f47fad99872	Apalache	Lambda	TupleEmpty	True	Passed	Model Under Test Equivalent Model
607dff5c04cb01163a580e28374c9136baa21a2b	Apalache	Lambda	TupleEmpty	False	Passed	Model Under Test Equivalent Model
b1f0968dd4ef50f6a1cf115d9c56af374d1b0b50	Apalache	Lambda	FunApp	True	Passed	Model Under Test Equivalent Model
f9ab8fb3290e9453e641cadb92e78c8e8177f56b	Apalache	Lambda	FunApp	False	Passed	Model Under Test Equivalent Model
4f6d34b2623b6b74fd6b9a72113b95da12a6dad8	Apalache	Lambda	Prime	True	Passed	Model Under Test Equivalent Model
2bf67c952db7a50a385bd35e229daefd3e34023e	Apalache	Lambda	Prime	False	Passed	Model Under Test Equivalent Model
4f037cab30a446cd1af0984c53b748a4cd6d4507	Apalache	Lambda	NumZero	True	Passed	Model Under Test Equivalent Model
b3888c7d7fae718d6e70e51bdc33553dadf24417	Apalache	Lambda	NumZero	False	Passed	Model Under Test Equivalent Model
55ad1d527879be5e780f9c8655f6c04e0d3e3cb9	Apalache	Lambda	NumOne	True	Passed	Model Under Test Equivalent Model
418fd1632906fb710e49a119641a9e892047caf2	Apalache	Lambda	NumOne	False	Passed	Model Under Test Equivalent Model
c976fccd4d4cf00ae5758a9ce7e8931113ccecfe	Apalache	Lambda	NumMaxInt	True	Passed	Model Under Test Equivalent Model
38c035989d9623ce390c96c280033ff33d650bd2	Apalache	Lambda	NumMaxInt	False	Passed	Model Under Test Equivalent Model
d01bb0ce92d5b7372ebc49eeb17c9074a7bbe1b6	Apalache	Lambda	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
1a617722fb6f59fdf5fc5787726cd30d0dd623a7	Apalache	Lambda	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
4571513c699248c168df867bf2c4cfc355287f90	Apalache	Lambda	NumPlus	True	Passed	Model Under Test Equivalent Model
fcb8f41d88a7a60e1197bb57358f2a61426a4dda	Apalache	Lambda	NumPlus	False	Passed	Model Under Test Equivalent Model
083298025451bcd0e04800f65757f1d9844dc397	Apalache	Lambda	NumMinus	True	Passed	Model Under Test Equivalent Model
5f2cb5a0acff8f9f425b02fd3aaa84df0e0917a2	Apalache	Lambda	NumMinus	False	Passed	Model Under Test Equivalent Model
9ccc73628963b299db19045ba8557228ef3576eb	Apalache	Lambda	NumMul	True	Passed	Model Under Test Equivalent Model
4aad55266094d1833b1941fb79311bc2542a3726	Apalache	Lambda	NumMul	False	Passed	Model Under Test Equivalent Model
d5b755a83e33f168695b28ff21b9726e7934bee6	Apalache	Lambda	NumDiv	True	Passed	Model Under Test Equivalent Model
28c4b90b18bb68985e6a31975954bb1ae0190d28	Apalache	Lambda	NumDiv	False	Passed	Model Under Test Equivalent Model
678d8edc903445263cef0afa6dd828b446b66f34	Apalache	Lambda	NumMod	True	Passed	Model Under Test Equivalent Model
4b941f265e044c8e38db6ef8fbe24a8414cef261	Apalache	Lambda	NumMod	False	Passed	Model Under Test Equivalent Model
4a423a76e9b8533fbc40d6217e9169c58c51496a	Apalache	Lambda	NumPow	True	Passed	Model Under Test Equivalent Model
c7435930673c1081b99de6794e782ac470c52f12	Apalache	Lambda	NumPow	False	Passed	Model Under Test Equivalent Model
2a10bd4e62da01fe7ca9c77c8d782f9d005238c7	Apalache	Lambda	NumGt	True	Passed	Model Under Test Equivalent Model
683afa699c6e77b736a23a5041608c2b8d12ecf7	Apalache	Lambda	NumGt	False	Passed	Model Under Test Equivalent Model
3dc1cb0f989d7336a9a089e9530987fb8e245fd9	Apalache	Lambda	NumGe	True	Passed	Model Under Test Equivalent Model
ce1d352d570b31f00f85d6a1a3660a9e47051065	Apalache	Lambda	NumGe	False	Passed	Model Under Test Equivalent Model
cb377b74dfae58e33736184529ecc4428c162af1	Apalache	Lambda	NumLt	True	Passed	Model Under Test Equivalent Model
2db6a90a4cd4b21be80108cae2ccfc2159138446	Apalache	Lambda	NumLt	False	Passed	Model Under Test Equivalent Model
95076204d44a1b19800909bcdf610de37bf719a5	Apalache	Lambda	NumLe	True	Passed	Model Under Test Equivalent Model
73a69490d1df50d7dc08068048ee01099a57333a	Apalache	Lambda	NumLe	False	Passed	Model Under Test Equivalent Model
ecfc7e6190d3defc85533c240473818e6937efa7	Apalache	Lambda	DefFun	True	Passed	Model Under Test Equivalent Model
1314ba482e7acd652918e39adf695faa171094ae	Apalache	Lambda	DefFun	False	Passed	Model Under Test Equivalent Model
c046ee0870cc236f990ce24be32770e72860a833	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDefFun	True	Passed	Model Under Test Equivalent Model
d27b975951bc90629f63cba8c5f8851ac99e729b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDefFun	False	Passed	Model Under Test Equivalent Model
2af28ccb72f493e69ca3800a5041c18f6bdd4260	Apalache	Lambda	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
02ddfc57ce01c103363a0a1cf063abc4598e1be5	Apalache	Lambda	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
97ba3cba73522dfc5b52435b6b0eaef64c33d127	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
d8592b55b603e05ade93373c3434be8b12b939a7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
d0053f0cdc817691f3254a35ddec2773ec03829b	Apalache	Lambda	Def0	True	Passed	Model Under Test Equivalent Model
1820c57576a136644d91285d1888966692206231	Apalache	Lambda	Def0	False	Passed	Model Under Test Equivalent Model
9922d82ea7173e762e2e989afe0807ba64d03c95	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef0	True	Passed	Model Under Test Equivalent Model
e01f86a296d09584b56d0ed8c080a09602c86549	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef0	False	Passed	Model Under Test Equivalent Model
43c602a079fe36f4da4643b1b13ed9c2b924ce99	Apalache	Lambda	Def1	True	Passed	Model Under Test Equivalent Model
81e5d55607dbfc17b8985585bb9bf6a51691cfb0	Apalache	Lambda	Def1	False	Passed	Model Under Test Equivalent Model
30d02dc13d60f833ff4787c14c692e2346a9016d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef1	True	Passed	Model Under Test Equivalent Model
fd1705e06244008c69077eb943a6b7e19464c71b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef1	False	Passed	Model Under Test Equivalent Model
7b7b1b08c561ff596fd9d781f05e1bf01fc3d656	Apalache	Lambda	Def2	True	Passed	Model Under Test Equivalent Model
805110db68ab2e2e981419691ed073181d4b7a8e	Apalache	Lambda	Def2	False	Passed	Model Under Test Equivalent Model
67c30e614e6e1a25207d190c0eddf02b363b8a3a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef2	True	Passed	Model Under Test Equivalent Model
5147c313e07a72bbe05488fa41aa79ff32b8b417	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef2	False	Passed	Model Under Test Equivalent Model
5eb32f0d3462e2ffd44a89695634d67a5e5e6638	Apalache	Lambda	Def1Recursive	True	Passed	Model Under Test Equivalent Model
71aaeac7d39d7ac19820ac5e6aa484a08372fdb6	Apalache	Lambda	Def1Recursive	False	Passed	Model Under Test Equivalent Model
af938c3c43bd463301c339a470d339d48311ba70	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
749a3b29eff22c98423cc18fc423ca8b1a580cb9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Lambda	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
fab917075bf9c7b6e224e39e49801446ec36a739	Apalache	Lambda	Extends	True	Passed	Model Under Test Equivalent Model
90a6e439286370ec6fa739e9c5d35fd19f98c261	Apalache	Lambda	Extends	False	Passed	Model Under Test Equivalent Model
2a0b1ac91a696089c245734815869dd6cedb75a6	Apalache	Lambda	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
adf18be2adea5151f3bfce5ddffea290864ad917	Apalache	Lambda	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
357ea49b57aae256b86ec2af0baba61b4f0f4370	Apalache	Lambda	Variable	True	Passed	Model Under Test Equivalent Model
2ad7365971ed588f0e8f3aca69f2ad7c52df153e	Apalache	Lambda	Variable	False	Passed	Model Under Test Equivalent Model
29046a9cfee3dc21eac4e7c5ad8ac79d014e5a72	Apalache	Lambda	Constant	True	Passed	Model Under Test Equivalent Model
ee5e539f73b8d1769896b7544bf62a436e09f99b	Apalache	Lambda	Constant	False	Passed	Model Under Test Equivalent Model
3b5001dde714b93021887b1d766d2ffec63ee68b	Apalache	Lambda	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
da709d3f87e246d84fd2f1771a8076f518f7d9de	Apalache	Lambda	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
c6ba49d5151b7cbcd08913b38dff4d4463e9b7a0	Apalache	Lambda	ConstantRank1	True	Passed	Model Under Test Equivalent Model
10c7023c1764d1225b9ce4e7607cba5d23b2a7b9	Apalache	Lambda	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ae1b44cf1437005b3f2599e35059851ad9883f5c	Apalache	Lambda	Instance	True	Passed	Model Under Test Equivalent Model
f2b94d36c82925faa00720c2ea8aafce3233474d	Apalache	Lambda	Instance	False	Passed	Model Under Test Equivalent Model
b0768969d06c4b44bf5cb8297ee1348fe9c3c169	Apalache	Lambda	InstanceWith	True	Passed	Model Under Test Equivalent Model
2861d8281b46e34c223fe37e3f317b4f580fc87f	Apalache	Lambda	InstanceWith	False	Passed	Model Under Test Equivalent Model
926e194aa44ad22596584e18706deec1b246a656	Apalache	Lambda	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8a76fe061c38794313224e2f1cb91e0ca6b61ab2	Apalache	Lambda	InstanceNamed	False	Passed	Model Under Test Equivalent Model
25cc50f9c786a5183f518bbc48ca74a572856bf5	Apalache	Lambda	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
be995b813cb36b978dd658f491ea68b931cbce48	Apalache	Lambda	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
0b59c51b50e4a12864b87acc13b8b922bfb10d8d	Apalache	Lambda	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
c58f648f764357c8c836e7374d85feeb8e15a980	Apalache	Lambda	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
0390fd122a523087ba03338d7dbe1facf4162da9	Apalache	Lambda	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
5b68d2bc2d3c37e4619667aa75d4395b15ea0076	Apalache	Lambda	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
94497c0355235c8197c6da0cfab8aef61a77e181	Apalache	Lambda	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
e8902f2d8f017fc8d229fe28efac46821fb09f4b	Apalache	Lambda	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
2617267928950c16d62404c430b31040da9002c4	Apalache	Lambda	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
defe866cb13c185d3a26a0b76cc0556beb17f9ae	Apalache	Lambda	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
73edbe7175e12de4586e6310055719ae987ce291	Apalache	Lambda	Enabled	True	Passed	Model Under Test Equivalent Model
d55b0c31529dbe4d78f6378a6bb966e5d0750b0b	Apalache	Lambda	Enabled	False	Passed	Model Under Test Equivalent Model
f64a4b1d07b2c43b922294aaa4c6073014cebc59	Apalache	Lambda	Cross2	True	Passed	Model Under Test Equivalent Model
68690b8f3bb2b9d820a7a3082649336792bc46b9	Apalache	Lambda	Cross2	False	Passed	Model Under Test Equivalent Model
2644b2fcc898546239e2c01119da9e6e5c4263d9	Apalache	Lambda	Cross3	True	Passed	Model Under Test Equivalent Model
1260f84d403f42607c8924b12716e0d37f88cb7a	Apalache	Lambda	Cross3	False	Passed	Model Under Test Equivalent Model
fb795918afc1cda730e792fc2e0659d5416a1ccb	TLC with reduction strategy: 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))	Lambda	FunSet	True	Passed	Model Under Test Equivalent Model
b472b50080703cbbe26fd70db6d83905ac9eb920	TLC with reduction strategy: 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))	Lambda	FunSet	False	Passed	Model Under Test Equivalent Model
357bede6315bae19fc00250b83d711370b404920	TLC with reduction strategy: 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)	Lambda	RecordSet	True	Passed	Model Under Test Equivalent Model
c778c4714705bc535a29b9f200bb07465ed3c463	TLC with reduction strategy: 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)	Lambda	RecordSet	False	Passed	Model Under Test Equivalent Model
7af318eb39c338456cbf3569f27a60376fb548e2	Apalache	Lambda	SetDiff	True	Passed	Model Under Test Equivalent Model
4efdea427cff715e94672671f3e1ba5222b820ba	Apalache	Lambda	SetDiff	False	Passed	Model Under Test Equivalent Model
b6d4207eac7a977ff5e708d03510a9f7782963c0	Apalache	Lambda	SetUnion	True	Passed	Model Under Test Equivalent Model
a49973b821c6f57549e62c6adabe6619688f6bbf	Apalache	Lambda	SetUnion	False	Passed	Model Under Test Equivalent Model
bfe77d387705ab469d206bc0d0910be74e19d6c3	Apalache	Lambda	SetIntersect	True	Passed	Model Under Test Equivalent Model
92dc77c10af5fa5e0e020cccb69ae9529b6e4979	Apalache	Lambda	SetIntersect	False	Passed	Model Under Test Equivalent Model
810e4cd5b6144041cacbed11d236e25c8aab94ee	Apalache	Lambda	SubsetEq	True	Passed	Model Under Test Equivalent Model
b88c56bab7c072e947cb6b764adb0c76d673a401	Apalache	Lambda	SubsetEq	False	Passed	Model Under Test Equivalent Model
2fdf684ea85e2b34300e50c19c52aebcca5c5f76	Apalache	Lambda	IfCond	True	Passed	Model Under Test Equivalent Model
5587653c7e3f831fd71521693ea4de354fcb2863	Apalache	Lambda	IfCond	False	Passed	Model Under Test Equivalent Model
eea10d4f6ee8cd0589ded205014124380cc11c06	Apalache	Lambda	IfThen	True	Passed	Model Under Test Equivalent Model
669d94e6929ed4d122641457b3989b83f3b759f9	Apalache	Lambda	IfThen	False	Passed	Model Under Test Equivalent Model
65f4905de6665fb7023d95f856a64d9e98051ba7	Apalache	Lambda	IfElse	True	Passed	Model Under Test Equivalent Model
86d3ceaf6260ef6a5d1052cb8a536f3531e3d90c	Apalache	Lambda	IfElse	False	Passed	Model Under Test Equivalent Model
fc4aaa7686f17d7b9a5657a59fb45e2dda60d514	Apalache	Lambda	Subset	True	Passed	Model Under Test Equivalent Model
967ccbc3d512b486f99bc819f4f3049cacdb4d0a	Apalache	Lambda	Subset	False	Passed	Model Under Test Equivalent Model
a1a941f533080657135a40448b5de865d7d64165	Apalache	Lambda	Domain	True	Passed	Model Under Test Equivalent Model
e2f4f79bee5c04415b74fd793f750f12adc1a400	Apalache	Lambda	Domain	False	Passed	Model Under Test Equivalent Model
9c7d4576581c44e25042dd80f4efaa3974c70779	Apalache	Lambda	Union	True	Passed	Model Under Test Equivalent Model
00be486b5f180738018bddb970be89411b8a10cd	Apalache	Lambda	Union	False	Passed	Model Under Test Equivalent Model
c71b3aad5adf026cc0a3cf684c3a5070f75034f7	Apalache	Lambda	Unchanged	True	Passed	Model Under Test Equivalent Model
7d6727edfcb332796350e9c10d51c2aea06fac23	Apalache	Lambda	Unchanged	False	Passed	Model Under Test Equivalent Model
f1243afefb39647974c6a0262cf630f0ae92b029	Apalache	Lambda	Equivalence	True	Passed	Model Under Test Equivalent Model
86bbf869e3f3e207d05aac038a876df17ca43a7a	Apalache	Lambda	Equivalence	False	Passed	Model Under Test Equivalent Model
5a00370243b1ee34165f5aeb13c0308e6f4b9317	Apalache	Lambda	StringEmpty	True	Passed	Model Under Test Equivalent Model
947608e75dddcb170fc69962e43607d9f702e04b	Apalache	Lambda	StringEmpty	False	Passed	Model Under Test Equivalent Model
fd85efdc9e2981d715c4a86fcdfc172c34c7dd55	Apalache	Lambda	String	True	Passed	Model Under Test Equivalent Model
dbea79b52dea60f567a8ec5b5478730b8fde6d00	Apalache	Lambda	String	False	Passed	Model Under Test Equivalent Model
6d839b8f4eae3cfdb796e9c333674d30b4ea3b51	Apalache	Lambda	SeqLen	True	Passed	Model Under Test Equivalent Model
e638e36c7f68d7eaef2d6f3b263e0b83e29eddd9	Apalache	Lambda	SeqLen	False	Passed	Model Under Test Equivalent Model
c8eafb801d4efa0159cbafd28b802fde48ec4106	Apalache	Lambda	SeqConcat	True	Passed	Model Under Test Equivalent Model
83188a46e6111cf1e7960b0d779c66f31f829c3d	Apalache	Lambda	SeqConcat	False	Passed	Model Under Test Equivalent Model
bd15ecf3f087dd933cb121156e68458ec9676b56	Apalache	Lambda	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
36ce90cb715e0c4aecb36002c0e6d2a15291534c	Apalache	Lambda	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
ba23acc8a21bd5b779fc279212bce57065f15678	Apalache	Lambda	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
21e4bff41ac722653d677797e949f4b8e1a62479	Apalache	Lambda	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
e2ad287bf697741930c05ef04436a43d0684fea6	TLC with reduction strategy: 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	Lambda	NumRange	True	Passed	Model Under Test Equivalent Model
c8a359508b0988d08d057afcb75479edf41a35c7	TLC with reduction strategy: 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	Lambda	NumRange	False	Passed	Model Under Test Equivalent Model
04bf02a3f7ab1281965d76c0a814e35195b106c0	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Lambda	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
5987bf986e8700cdb26c324dd4168251b58f7fb6	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Lambda	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
5dd00e1480f3caaa9edb4708174de031d7a4fa91	TLC with reduction strategy: 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]]	Lambda	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
dca746bfb474e76a9d3fd16cfdf9c88d6c3d97a1	TLC with reduction strategy: 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]]	Lambda	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
cb5f382ec001fb8267ed2955759b565fdb9615ab	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Lambda	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
438c19e3e606d5a64f66d1e6f9dfd7b98d37ddff	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Lambda	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
bdcda349ffecfde46ee45938e3712d87cf7d4988	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Lambda	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
73a09f1779c15d27394617e988ccd472769d9e55	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Lambda	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
95cfafb2d46d111fb7082455114a0c02404f42be	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Lambda	TlcEval	True	Passed	Model Under Test Equivalent Model
cda654c44e128b9c8b0eba6a1ba4d8b1e05cbbc3	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Lambda	TlcEval	False	Passed	Model Under Test Equivalent Model
8356e3f4413058fe1c27b744540907f455e2ac2d	Apalache	Lambda	BagBagToSet	True	Passed	Model Under Test Equivalent Model
bac3ac78de6e0a2c72f66e7e499be62a616a8c0b	Apalache	Lambda	BagBagToSet	False	Passed	Model Under Test Equivalent Model
8d5c835a0dd06cf8c9055d11e11155d89af78d99	Apalache	Lambda	BagSetToBag	True	Passed	Model Under Test Equivalent Model
63b06297133db179066d9984609f7782499d6cc1	Apalache	Lambda	BagSetToBag	False	Passed	Model Under Test Equivalent Model
fac7e309a67a799e682f0939b26e5b2a71f8c3b8	Apalache	Lambda	BagBagIn	True	Passed	Model Under Test Equivalent Model
139704ca64b5a0a0376b1a8b4694c7ace507fcf4	Apalache	Lambda	BagBagIn	False	Passed	Model Under Test Equivalent Model
a8fd79e07f3ddf1ff68ead857053e84537de4d4e	Apalache	Lambda	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
a16b30616c002b2f029533df6998cd1a18bb4d21	Apalache	Lambda	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
49546f45ddb118725ac9ff4322929436debba9f1	Apalache	Lambda	BagAddBag	True	Passed	Model Under Test Equivalent Model
e5e279aa5f6d2cd1b33c779693aef4b8da5beded	Apalache	Lambda	BagAddBag	False	Passed	Model Under Test Equivalent Model
bb287ef0c69b8548cb935edeb1358f01e2d57298	Apalache	Lambda	BagBagSub	True	Passed	Model Under Test Equivalent Model
b1562b25af6a5e8eec4be939342a9bd3b333ae1f	Apalache	Lambda	BagBagSub	False	Passed	Model Under Test Equivalent Model
53b21611f3e1d7519b07a5d7ae9b73dd8a1b1c1a	Apalache	Lambda	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
31ed1fec7a29d68fc5c5025ff08787ef4ae0ac74	Apalache	Lambda	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
af17cdf2f0c846829cba4c72278a60820b579ae4	Apalache	Lambda	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
99e3bc8c325c181aa5118180988ff7f19993ce97	Apalache	Lambda	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
5b728aac08f5a3b58deb68f7ec1cf12b1f4faff1	Apalache	Lambda	BagBagUnion	True	Passed	Model Under Test Equivalent Model
e4fb27e48a68ee231b8d6caf31bd8335d91356c5	Apalache	Lambda	BagBagUnion	False	Passed	Model Under Test Equivalent Model
d2502e6d696e5f69b2c905dca189dfeb7c6ad259	Apalache	Lambda	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
12cca94b33ef81e3d045cee8bd2285b6309a057f	Apalache	Lambda	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
a942cb994b060c986d3539229be6624a7369353f	Apalache	Lambda	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
62465e21897a7ed58669acdf4a6652647f1c3d30	Apalache	Lambda	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
e4f49c13a9b0c5d9987001929c86cad03de2373b	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Lambda	BagSubBag	True	Passed	Model Under Test Equivalent Model
c07ada86138f8c99e807958f7d70d4b1593a2fb1	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Lambda	BagSubBag	False	Passed	Model Under Test Equivalent Model
bfca393c69a91a7336e49655c7cc19f0d244461f	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Lambda	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
cce936c6701ae43d0f8060145bd261044db5dfef	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Lambda	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
132acd7b7f8569209a706546cb3f4cf202136e21	Apalache	Lambda	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
1b0d15d96d968d062ea73813fcaac94c278d0216	Apalache	Lambda	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
1e334cc10209c1a49f6068eea29a76583db52562	Apalache	Lambda	SeqHead	True	Passed	Model Under Test Equivalent Model
317db677952e94852a94b893e8d241a06f4c0015	Apalache	Lambda	SeqHead	False	Passed	Model Under Test Equivalent Model
aa79f780f6eb83e1cba719393893d7191024c3dd	Apalache	Lambda	SeqTail	True	Passed	Model Under Test Equivalent Model
21a5186cd3a2538fcd392b321177293bd85b446c	Apalache	Lambda	SeqTail	False	Passed	Model Under Test Equivalent Model
12870e229ab7b1dd272be62a6bd5194f45ce514d	Apalache	Lambda	SeqAppend	True	Passed	Model Under Test Equivalent Model
76cb6beacea18c4b2a75114dc1a79a34fc644e47	Apalache	Lambda	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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