Tests by plug feature Def0; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b7d76362b86d36ca3543471b8028c1c3b1aa1d38	Apalache	And	Def0	True	Passed	Model Under Test Equivalent Model
6a6d327ea007e4ed8fdee09901546951f7c11f9c	Apalache	And	Def0	False	Passed	Model Under Test Equivalent Model
f047a721c3f524da05c9432dbe981375b8a4bda3	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def0	True	Passed	Model Under Test Equivalent Model
d959057a7a7174a9149529b4506d45b2f57b77c2	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def0	False	Passed	Model Under Test Equivalent Model
ed220a5de70e24104dcc7c3b08bee97fb0acaf96	Apalache	Imply	Def0	True	Passed	Model Under Test Equivalent Model
eabc480755ab50bf02411b509483df9b95d587a1	Apalache	Imply	Def0	False	Passed	Model Under Test Equivalent Model
18d2b6f5a286cf5235fbfb5efc3ca80898588160	Apalache	Not	Def0	True	Passed	Model Under Test Equivalent Model
66cbdbd7a3ae66df309ac8365dea79b150b7d9e7	Apalache	Not	Def0	False	Passed	Model Under Test Equivalent Model
76f7ebe7321872009e49befff95a08c74d0dab05	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def0	True	Passed	Model Under Test Equivalent Model
43ff5f615ed5396711b78b39f96e076e3f92719f	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def0	False	Passed	Model Under Test Equivalent Model
501ab6654546c5e331a9a75af3e2d4335cb9c59c	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def0	True	Passed	Model Under Test Equivalent Model
03cc4dba90d702dbae131d0138e09d41918f320d	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def0	False	Passed	Model Under Test Equivalent Model
2d6ac45cc30ae7476814e5f9ef6a6f1b84caf5e2	Apalache	AndProp	Def0	True	Passed	Model Under Test Equivalent Model
df31bb030d93cc86a3cc906df71830578aa97dd4	Apalache	AndProp	Def0	False	Passed	Model Under Test Equivalent Model
a725ad75a005e64b0b48f4ec335ce2fe3583bdcd	Apalache	Boxed	Def0	True	Passed	Model Under Test Equivalent Model
8d36fa76205a24e00b0928119ad850f1e7549dd1	Apalache	Boxed	Def0	False	Passed	Model Under Test Equivalent Model
d2af982bc8c0d820c11c11897d2d3119b1ab76f2	Apalache	Eq	Def0	True	Passed	Model Under Test Equivalent Model
5ab18365101b48afcaddf7a61844bf4c7cd1945d	Apalache	Eq	Def0	False	Passed	Model Under Test Equivalent Model
146a7b4ee5372d79f81b28f1897cb9ba9599f8fb	Apalache	Ne	Def0	True	Passed	Model Under Test Equivalent Model
ad5d1eaa4f335cf4ad69ab2dbfb676120a4d89f4	Apalache	Ne	Def0	False	Passed	Model Under Test Equivalent Model
68ec03057badb4c04781e87e8f3580962e508a17	Apalache	Let	Def0	True	Passed	Model Under Test Equivalent Model
5409acadd520c495f33ea074e8a19e8a10608ff1	Apalache	Let	Def0	False	Passed	Model Under Test Equivalent Model
5b84ab34ee0894f3f816ce3bd3181ecd1ff62f25	Apalache	Set0	Def0	True	Passed	Model Under Test Equivalent Model
629141aa041e31c3cc314d1c4538791a225eaf23	Apalache	Set0	Def0	False	Passed	Model Under Test Equivalent Model
6e10be9af1b598c189ecf86c60c353ef3f1ad3c9	Apalache	Set1	Def0	True	Passed	Model Under Test Equivalent Model
66ebc8236348f596bbcabc86959ed16a37e65ede	Apalache	Set1	Def0	False	Passed	Model Under Test Equivalent Model
8004ecbdd406a3ecfaf85f183b07ce1f156e22e9	Apalache	Set2	Def0	True	Passed	Model Under Test Equivalent Model
1e9e9703208ac2bdbd580b7b332d070a3e6ccc11	Apalache	Set2	Def0	False	Passed	Model Under Test Equivalent Model
1b3dde6dbe23e369796aa3322100157cf8a72417	Apalache	Fun	Def0	True	Passed	Model Under Test Equivalent Model
7dbe65a091fca6f93e1d192f844c1a3b9d99f83e	Apalache	Fun	Def0	False	Passed	Model Under Test Equivalent Model
c492c0a79d37d65286f68beef4bdbbc14ec669bc	Apalache	In	Def0	True	Passed	Model Under Test Equivalent Model
b5c42774d6ba37699336ebf625ce9b33e71a31dd	Apalache	In	Def0	False	Passed	Model Under Test Equivalent Model
5b966b649ae7948f2b3c56ffe71596712ae1e3a0	Apalache	NotIn	Def0	True	Passed	Model Under Test Equivalent Model
1aeb663779de9ea9e4dbc3a0ce89697b88fd858c	Apalache	NotIn	Def0	False	Passed	Model Under Test Equivalent Model
ae1eceb90a58ea4bc1ec2c6d4ec635acc64bf411	Apalache	Exists	Def0	True	Passed	Model Under Test Equivalent Model
b4bca5e75340e5384d4905eca52c2ec36b2cdd68	Apalache	Exists	Def0	False	Passed	Model Under Test Equivalent Model
cff1c96a1b8a0e175e2562b343b2f7a8e5d08d11	Apalache	Forall	Def0	True	Passed	Model Under Test Equivalent Model
d286390173fd5ed126c2981c5f66bbab1814d747	Apalache	Forall	Def0	False	Passed	Model Under Test Equivalent Model
2d548aa55a36296a643ad5c4f042d85e27ed85fb	Apalache	Choose	Def0	True	Passed	Model Under Test Equivalent Model
0eb0a775c1dcc2b23a5f42c364f1f687541551a7	Apalache	Choose	Def0	False	Passed	Model Under Test Equivalent Model
cfdf1cd41666f4aa271a1738c4de15ca025025c4	Apalache	Record	Def0	True	Passed	Model Under Test Equivalent Model
321c56fdb0c9965550d01b630645cb1e949377d2	Apalache	Record	Def0	False	Passed	Model Under Test Equivalent Model
69219c18016c35073af7ccb28e1a1c64ed263b77	Apalache	Tuple	Def0	True	Passed	Model Under Test Equivalent Model
c5251c8bfc953eb4a539d288be22c48eb8fb9c0a	Apalache	Tuple	Def0	False	Passed	Model Under Test Equivalent Model
b0cb2f76fd006f4ef8ad7e68e09e97b48607adc3	Apalache	FunApp	Def0	True	Passed	Model Under Test Equivalent Model
2379556892eaec43d2288e0c6924d704a65fe63f	Apalache	FunApp	Def0	False	Passed	Model Under Test Equivalent Model
2b619cdc86b110502af010e07236edb1067cd515	Apalache	Except0	Def0	True	Passed	Model Under Test Equivalent Model
731022db13ae16c5477916a54511f8ec547b0f64	Apalache	Except0	Def0	False	Passed	Model Under Test Equivalent Model
5de6210550ae75b2eb1a3b896eea77ca490cce3f	Apalache	Except1Fun	Def0	True	Passed	Model Under Test Equivalent Model
33ded0b76d567db843f88f8bab1ebac403272257	Apalache	Except1Fun	Def0	False	Passed	Model Under Test Equivalent Model
e4fbb15127c093916811dc8192f9278af8f1836b	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def0	True	Passed	Model Under Test Equivalent Model
60905a22a6044efffc3c66f6098bae077908534e	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def0	False	Passed	Model Under Test Equivalent Model
b4e1cdb9e1fb5f3d66bea0f499455ab32d1cf741	Apalache	Except1Rec	Def0	True	Passed	Model Under Test Equivalent Model
e680e45a7bae9cdc75e9b7c00d0f1cda0bc4401d	Apalache	Except1Rec	Def0	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
dd96f3f11c8ea85691458ea20f56df8c8541bfe3	Apalache	Except2Fun	Def0	True	Passed	Model Under Test Equivalent Model
9cf77670849c851602ee8f039ccfdeabfc8fafa8	Apalache	Except2Fun	Def0	False	Passed	Model Under Test Equivalent Model
84a9ecb8c8158c2bf787c924814ca5011ffdcbff	Apalache	Except2FunTuple	Def0	True	Passed	Model Under Test Equivalent Model
e6882df03439781c9c54be76202ca9bce8d90199	Apalache	Except2FunTuple	Def0	False	Passed	Model Under Test Equivalent Model
aad663a28c49a497208f86223a6ed2b9aa1b2086	Apalache	Prime	Def0	True	Passed	Model Under Test Equivalent Model
cc1c39f980f8f5d0e5f489853a4e254871ebfe4a	Apalache	Prime	Def0	False	Passed	Model Under Test Equivalent Model
b93d23237f7bef2a6c4b3715d43398f0ccd6fa93	Apalache	NumUnaryMinus	Def0	True	Passed	Model Under Test Equivalent Model
1968a91fee4cc5a66ee6aae3c669003795ade25f	Apalache	NumUnaryMinus	Def0	False	Passed	Model Under Test Equivalent Model
9ed4f8c02bcb5b80ab5f44c24720406bec8dadc7	Apalache	NumPlus	Def0	True	Passed	Model Under Test Equivalent Model
62d6f25c0709d703f81869271bcb2584a03b3865	Apalache	NumPlus	Def0	False	Passed	Model Under Test Equivalent Model
a3ce983665f60ff854988df0005bd3e3b83ce65c	Apalache	NumMinus	Def0	True	Passed	Model Under Test Equivalent Model
975b274edbb1c5a7f99ba117812f87ee2dc772dc	Apalache	NumMinus	Def0	False	Passed	Model Under Test Equivalent Model
f82973559d1555158076e8f99648a713f2049bce	Apalache	NumMul	Def0	True	Passed	Model Under Test Equivalent Model
f3c9b72cf66fb58a06ea2800731506db15493ac3	Apalache	NumMul	Def0	False	Passed	Model Under Test Equivalent Model
ca2fd40b4bb513ffb5c833207df4c2826e0db841	Apalache	NumDiv	Def0	True	Passed	Model Under Test Equivalent Model
39b95c4b628a4230fa1e122fd5d728eb03f79995	Apalache	NumDiv	Def0	False	Passed	Model Under Test Equivalent Model
aa035c2c663fdc4716b334eaf3484010ef6f2942	Apalache	NumMod	Def0	True	Passed	Model Under Test Equivalent Model
3f03d512c46c728a76d0111901cdf6af8f46bc1a	Apalache	NumMod	Def0	False	Passed	Model Under Test Equivalent Model
075060063646a75813cfb1bd023ab866b5e97a86	Apalache	NumPow	Def0	True	Passed	Model Under Test Equivalent Model
f0067d186f1041f4100a4f578ee0d9840ae4968a	Apalache	NumPow	Def0	False	Passed	Model Under Test Equivalent Model
1253aa3b469318f1b3cfb629f0a825ea899aa069	Apalache	NumGt	Def0	True	Passed	Model Under Test Equivalent Model
0b1ffa2cf23459f5cfd72cad7b27554500aa6248	Apalache	NumGt	Def0	False	Passed	Model Under Test Equivalent Model
e19dfeedaef1968f45ec14b99cf274f90a113425	Apalache	NumGe	Def0	True	Passed	Model Under Test Equivalent Model
30daaef2ee34139287e3123b8d0e210a46173e2b	Apalache	NumGe	Def0	False	Passed	Model Under Test Equivalent Model
bc0d94ef7c2daced6d1593d9299a866869719b84	Apalache	NumLt	Def0	True	Passed	Model Under Test Equivalent Model
b35b8971434d9c73a8ed62e3af22e08863718ed5	Apalache	NumLt	Def0	False	Passed	Model Under Test Equivalent Model
c0ce135104433a06ddd7afc07fd9492816b71a47	Apalache	NumLe	Def0	True	Passed	Model Under Test Equivalent Model
d5414f19873b521630423d44e14efb27b2677887	Apalache	NumLe	Def0	False	Passed	Model Under Test Equivalent Model
a9ef7106a085aca5597a552bbf0e7229c74d1eea	Apalache	DefFun	Def0	True	Passed	Model Under Test Equivalent Model
c26eb145ab2df38e41363f9e4178e2e09f796c73	Apalache	DefFun	Def0	False	Passed	Model Under Test Equivalent Model
c626f8c79377727181994469df926d7dd918d7b7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def0	True	Passed	Model Under Test Equivalent Model
386e8cb10cc4d33e1c9c072d6a39c1be3f9be780	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def0	False	Passed	Model Under Test Equivalent Model
7f7fd1120727f04a81091eb1f0fabe46d2c87252	Apalache	DefFunRecursive	Def0	True	Passed	Model Under Test Equivalent Model
9ca893b060539d5210c91086f264f7ec484c5f2d	Apalache	DefFunRecursive	Def0	False	Passed	Model Under Test Equivalent Model
0211a733c7842fb4b6b7bbf62e9b967fb09b7bba	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def0	True	Passed	Model Under Test Equivalent Model
065eae54f26810d8aa413424dd0d76af11c7744b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def0	False	Passed	Model Under Test Equivalent Model
64962902d9a3f498344e0c2feedbb7ad949cb772	Apalache	Def0	Def0	True	Passed	Model Under Test Equivalent Model
80a9f6a090832fe2c64e5d4d1fc25e78308e1ab9	Apalache	Def0	Def0	False	Passed	Model Under Test Equivalent Model
31d546a74ebce4b21c2e623529bd4bdeef07525a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def0	True	Passed	Model Under Test Equivalent Model
d8a65e1e2830a1aea4a924485b9bf76fd1f4eff7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def0	False	Passed	Model Under Test Equivalent Model
4093b068199c3a07a1c7ce2b7e20a06be31000eb	Apalache	Def1	Def0	True	Passed	Model Under Test Equivalent Model
03dbfd8da02eaef70596cb2073acfbc02c903b3a	Apalache	Def1	Def0	False	Passed	Model Under Test Equivalent Model
4026b0981b097f75a698b3dc0a2b6648544522c1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def0	True	Passed	Model Under Test Equivalent Model
ae2345efad578627ad665a7ae4786159e8277550	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def0	False	Passed	Model Under Test Equivalent Model
a9dc4ddf938e4e0a15ef4992389cde15681cb292	Apalache	Def2	Def0	True	Passed	Model Under Test Equivalent Model
3380455cb55bc4755f17c2e1f680a0a6aa2524c4	Apalache	Def2	Def0	False	Passed	Model Under Test Equivalent Model
2fc7d2b8a3fa6703bf06a481786240891c189cb5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def0	True	Passed	Model Under Test Equivalent Model
6201ad1b19e568c5339977764ec801698f7d0bea	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def0	False	Passed	Model Under Test Equivalent Model
53aad11ab3cf06192ab08dcc1a6c4ccfb281594d	Apalache	Def1Recursive	Def0	True	Passed	Model Under Test Equivalent Model
9469f6ba82df200241f3d0d028516d7011262b04	Apalache	Def1Recursive	Def0	False	Passed	Model Under Test Equivalent Model
c067b608c54a1fe743e6d50f28e58cfd28c2fd3f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def0	True	Passed	Model Under Test Equivalent Model
af14a17fa5d25957c978e102f54d0f680d1422b1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def0	False	Passed	Model Under Test Equivalent Model
4cbdb4d63a9c75088b5c332e4584671138f6a616	Apalache	Extends	Def0	True	Passed	Model Under Test Equivalent Model
77ba17d0643520e0d028f7debee8307770100fe7	Apalache	Extends	Def0	False	Passed	Model Under Test Equivalent Model
a00c942bfd8871e82cafab243feb8ef1cf0d9b28	Apalache	ExtendsInDifferentFolder	Def0	True	Passed	Model Under Test Equivalent Model
201bc1527f3f8a569cff275c383c54c94e72424a	Apalache	ExtendsInDifferentFolder	Def0	False	Passed	Model Under Test Equivalent Model
b924c073e84f7612814a3193c3683ed34a03db57	Apalache	Variable	Def0	True	Passed	Model Under Test Equivalent Model
4b1ebbe89d90935e8a13c11dd7208424a0b251f7	Apalache	Variable	Def0	False	Passed	Model Under Test Equivalent Model
49828925a4d6f58d6b3ac6aedb880a13edb1d5fa	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def0	True	Passed	Model Under Test Equivalent Model
acc9e24cae5ae4f63da2ee810bab6aef328f782f	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def0	False	Passed	Model Under Test Equivalent Model
b0a1ce531968fe999aab0137aa9e6247f133837a	Apalache	Constant	Def0	True	Passed	Model Under Test Equivalent Model
e3b95523e654f7316e21c4de16b4f213a0dedf9a	Apalache	Constant	Def0	False	Passed	Model Under Test Equivalent Model
961e54ea949c9b3438cf7949939bad84ac2177b5	Apalache	ConstantRank1	Def0	True	Passed	Model Under Test Equivalent Model
fc282dc52ef089ca4ec6a54c29d41eb158d7eeef	Apalache	ConstantRank1	Def0	False	Passed	Model Under Test Equivalent Model
884fe48fd23345eb3bae28d457a1e7414af4a87e	Apalache	Instance	Def0	True	Passed	Model Under Test Equivalent Model
18b6b46071b0a9d2dafab572c1af0d5352789783	Apalache	Instance	Def0	False	Passed	Model Under Test Equivalent Model
30435098c01b98d42ff6c141add977016bc68645	Apalache	InstanceWith	Def0	True	Passed	Model Under Test Equivalent Model
81b24f92cf39a9dbde1f271bff17fdbdce47f5d3	Apalache	InstanceWith	Def0	False	Passed	Model Under Test Equivalent Model
9a40631532dfa50f1b1f276b9f013c0f645954ad	Apalache	InstanceNamed	Def0	True	Passed	Model Under Test Equivalent Model
f0c93cb98540b37fc766cf5a7a4c3980e24db7c7	Apalache	InstanceNamed	Def0	False	Passed	Model Under Test Equivalent Model
a975a0055bdab7e48bd600bbaf8a9679d97ca6da	Apalache	InstanceNamedWith	Def0	True	Passed	Model Under Test Equivalent Model
170e32449cc1ae2b6c9837b8e923840002ae5a09	Apalache	InstanceNamedWith	Def0	False	Passed	Model Under Test Equivalent Model
50f30a512d5d24b8b8e802f2486210c79383fcaf	Apalache	InstanceInFolder	Def0	True	Passed	Model Under Test Equivalent Model
817f84f12fb86580428d7dae0cd14d67399109af	Apalache	InstanceInFolder	Def0	False	Passed	Model Under Test Equivalent Model
dd981588df0200619cdddaf0a4ffb537f19154fe	Apalache	InstanceWithInFolder	Def0	True	Passed	Model Under Test Equivalent Model
0a9844c2db7d02def490b7e24be17ce0fbb4258b	Apalache	InstanceWithInFolder	Def0	False	Passed	Model Under Test Equivalent Model
7113a2efc2605c69eab3936881d82345c429d0f4	Apalache	InstanceNamedInFolder	Def0	True	Passed	Model Under Test Equivalent Model
5996a8d3952ca13cfd3e2209b16ca7d36c513431	Apalache	InstanceNamedInFolder	Def0	False	Passed	Model Under Test Equivalent Model
c1cd9e8d2931d29109068cf8ceaa43a379d86418	Apalache	InstanceNamedWithInFolder	Def0	True	Passed	Model Under Test Equivalent Model
b0edb551380338a9971130a553a916bbd1723000	Apalache	InstanceNamedWithInFolder	Def0	False	Passed	Model Under Test Equivalent Model
4faa93a1b713bbf8ca3c57e30198a179a1414d44	Apalache	Enabled	Def0	True	Passed	Model Under Test Equivalent Model
ce0a2a4607c4a6603813f5c8f81ec54559e81640	Apalache	Enabled	Def0	False	Passed	Model Under Test Equivalent Model
da917272e4ea53b6a4115aa4321e838b007b6148	Apalache	Assume	Def0	True	Passed	Model Under Test Equivalent Model
881c59d8dd7cf0bb069b3e5c14ab004bf3407289	Apalache	Assume	Def0	False	Passed	Model Under Test Equivalent Model
906f13aa3f429a4f0212b1108b3da8573ecbfcde	Apalache	AssumeNamed	Def0	True	Passed	Model Under Test Equivalent Model
114276802369fd5534759d09268ce510f0a64546	Apalache	AssumeNamed	Def0	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
c9da08f043dacaa4889e0735d94b52135012c413	Apalache	Cross2	Def0	True	Passed	Model Under Test Equivalent Model
b201c47caa43f3e217a72c779c03e4c0ad57a60a	Apalache	Cross2	Def0	False	Passed	Model Under Test Equivalent Model
8c60ceffc6726e196f9c50c05c9a02f23c429c4d	Apalache	Cross3	Def0	True	Passed	Model Under Test Equivalent Model
e0eeb0840ba7eb72dbb1dd24b4a1ee3fbab6ced9	Apalache	Cross3	Def0	False	Passed	Model Under Test Equivalent Model
76ffee42d12cd7319205dff9c6f5007133369946	TLC with reduction strategy: Case 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))	FunSet	Def0	True	Passed	Model Under Test Equivalent Model
1ece0817fbb045898000edcdeceeaf90560aaa9a	TLC with reduction strategy: Case 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))	FunSet	Def0	False	Passed	Model Under Test Equivalent Model
2d9e16367dbd5490e4fe44e27a3f314d7839db4e	TLC with reduction strategy: Case 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)	RecordSet	Def0	True	Passed	Model Under Test Equivalent Model
9ca037f3f93950a38f525d5f5c195e5e2c87e04d	TLC with reduction strategy: Case 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)	RecordSet	Def0	False	Passed	Model Under Test Equivalent Model
432c4541bdc1a33ede7070351c758e9420301ad6	Apalache	SetDiff	Def0	True	Passed	Model Under Test Equivalent Model
618f00b11e31ebfb5bbd11b4b8cb755cc7e2179a	Apalache	SetDiff	Def0	False	Passed	Model Under Test Equivalent Model
45703cce322b22cb9fa780f6fbb7a5d35c10d9f5	Apalache	SetUnion	Def0	True	Passed	Model Under Test Equivalent Model
d66b93097e05f669d1f8d4ced0f7ddac9a890a93	Apalache	SetUnion	Def0	False	Passed	Model Under Test Equivalent Model
93e3b2a051e5c2cda9ec0f6e01feda56d33711cc	Apalache	SetIntersect	Def0	True	Passed	Model Under Test Equivalent Model
baa6503572ca11da7bd54adfbadebdeee74da5da	Apalache	SetIntersect	Def0	False	Passed	Model Under Test Equivalent Model
964e852f8d5be63ab8d4957bea2993e69dee1233	Apalache	SubsetEq	Def0	True	Passed	Model Under Test Equivalent Model
3056d99863b375a8a63dd8e7ceb54c96c30d8d30	Apalache	SubsetEq	Def0	False	Passed	Model Under Test Equivalent Model
7fd09bdc0322eb87796f12ea483378773329f828	Apalache	IfCond	Def0	True	Passed	Model Under Test Equivalent Model
45dbb2dc01582d20d5371b5caad3af19a295cf9b	Apalache	IfCond	Def0	False	Passed	Model Under Test Equivalent Model
c021427f1410229d3f7323f9d843f1ac9aeb51f5	Apalache	IfThen	Def0	True	Passed	Model Under Test Equivalent Model
50127b25dd1f52b5ec3865de05e7c917302b6795	Apalache	IfThen	Def0	False	Passed	Model Under Test Equivalent Model
e357fbed40e56afc181012a2d01ec20f94dc3362	Apalache	IfElse	Def0	True	Passed	Model Under Test Equivalent Model
3c25591551697502c5e3891b38d11f619abbe587	Apalache	IfElse	Def0	False	Passed	Model Under Test Equivalent Model
e86e0a7d750429c8c82d58395f71a570a9fa2932	Apalache	Subset	Def0	True	Passed	Model Under Test Equivalent Model
629f77f71674b9cea5a6fe5a538564a0649df8c8	Apalache	Subset	Def0	False	Passed	Model Under Test Equivalent Model
9b35ea3219296bb4091c5c5411035ca01f81e642	Apalache	Domain	Def0	True	Passed	Model Under Test Equivalent Model
774db65943744cd60ab084b8f83522ae843a685e	Apalache	Domain	Def0	False	Passed	Model Under Test Equivalent Model
cff0df6e86732471085955460f4659c1af26f532	Apalache	Union	Def0	True	Passed	Model Under Test Equivalent Model
df45cd2554d32c1da51b784d6dd48606f407a454	Apalache	Union	Def0	False	Passed	Model Under Test Equivalent Model
0c35a8524613d5b6bfbbef0466557eedb9878afe	Apalache	Unchanged	Def0	True	Passed	Model Under Test Equivalent Model
4b032ca039d38c33c3e0d5e3864e2a0aee8bdc44	Apalache	Unchanged	Def0	False	Passed	Model Under Test Equivalent Model
8ba4a881de6bb72f661c2c513ba9ad3dac848209	Apalache	Equivalence	Def0	True	Passed	Model Under Test Equivalent Model
3e0b7542ef1e0881f3e9a02705d2faf4c20d8cd6	Apalache	Equivalence	Def0	False	Passed	Model Under Test Equivalent Model
e887d1609923d169f0c9ea9c9eee5eddb6e9c0c6	Apalache	SeqLen	Def0	True	Passed	Model Under Test Equivalent Model
5bea690250775df2093c07d8a76453de77b17364	Apalache	SeqLen	Def0	False	Passed	Model Under Test Equivalent Model
4f5e511f1beb87ed8cb9ae7aeb97dd5e8c96bf3b	Apalache	SeqConcat	Def0	True	Passed	Model Under Test Equivalent Model
636256366104216054c097c4f93d884ca63044be	Apalache	SeqConcat	Def0	False	Passed	Model Under Test Equivalent Model
9fc2abbd07ff9041504263437c113489abaa41ed	Apalache	SeqSeq	Def0	True	Passed	Model Under Test Equivalent Model
b1eb75964d132fc2affe88c944f8cf5d0b938ecf	Apalache	SeqSeq	Def0	False	Passed	Model Under Test Equivalent Model
fd5f0634593aba3bfdb6a47e16a7056c53efb6b1	Apalache	SeqSelectSeq	Def0	True	Passed	Model Under Test Equivalent Model
49b655550d47e7eb0546bef9ac3a5d687f2de098	Apalache	SeqSelectSeq	Def0	False	Passed	Model Under Test Equivalent Model
3542e22feddeb747531034083bfbc09b9471a81c	Apalache	SeqSubSeq	Def0	True	Passed	Model Under Test Equivalent Model
905de5c5d9be96733e791dd6d371108725216364	Apalache	SeqSubSeq	Def0	False	Passed	Model Under Test Equivalent Model
5869e2e535c874d0f73115adf3607d49becd3dab	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	NumRange	Def0	True	Passed	Model Under Test Equivalent Model
a098a295eadfc19dc23a13018b252d2debcb3800	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	NumRange	Def0	False	Passed	Model Under Test Equivalent Model
aa80e1a148a704bb0c9ee82da750ef860e641d9d	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def0	True	Passed	Model Under Test Equivalent Model
04158e7409e03db1ee294f2e2c3d6036f69256c5	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def0	False	Passed	Model Under Test Equivalent Model
94c4c789412563b8c099da024012311a80e81627	TLC with reduction strategy: Case 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]]	TlcExtendFun	Def0	True	Passed	Model Under Test Equivalent Model
247ac28cc29818d508a13edde95fa6cbfac986af	TLC with reduction strategy: Case 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]]	TlcExtendFun	Def0	False	Passed	Model Under Test Equivalent Model
15cc42783c2ae862ae49e49daddaff6218d7e34c	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def0	True	Passed	Model Under Test Equivalent Model
19036903735ef0c025afdd60316e1eee6d9d0661	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def0	False	Passed	Model Under Test Equivalent Model
6172dca1d52b9a5089c3db835da0f4ab0d0b74b9	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def0	True	Passed	Model Under Test Equivalent Model
4ac6a6acf372a87dfd2a536dddde661ad2c285d1	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def0	False	Passed	Model Under Test Equivalent Model
65cf7ab010d81d455638e06d16c25fcf0d7a1bd8	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def0	True	Passed	Model Under Test Equivalent Model
2bc6b58d506321941fb69ae59ccdb24ec45894fc	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def0	False	Passed	Model Under Test Equivalent Model
37c365d8fb32792597e873f2ee7eabff3f0a1fab	Apalache	BagBagToSet	Def0	True	Passed	Model Under Test Equivalent Model
183273e77dacf2be36a57ab6a5c5d1aa1a123cc8	Apalache	BagBagToSet	Def0	False	Passed	Model Under Test Equivalent Model
2c49299c3f296b02c834e39337bda8836533593d	Apalache	BagSetToBag	Def0	True	Passed	Model Under Test Equivalent Model
0c3f57308840214cd18a6f4f516cf433bb1df007	Apalache	BagSetToBag	Def0	False	Passed	Model Under Test Equivalent Model
c1a99303af8da1bb2b7409bafb5e0a6db0e37731	Apalache	BagBagIn	Def0	True	Passed	Model Under Test Equivalent Model
51c6808d75d32ad5a5f6e4621ad2b33969472f7e	Apalache	BagBagIn	Def0	False	Passed	Model Under Test Equivalent Model
50f590c77df2bdcbd013529108ee717f777c2b5e	Apalache	BagAddBag	Def0	True	Passed	Model Under Test Equivalent Model
e63ca797261512279a7dfc66d1c7e26b1eb50854	Apalache	BagAddBag	Def0	False	Passed	Model Under Test Equivalent Model
69a3d9f06be7dad4b04e638fe7e94e1fb6a1308e	Apalache	BagBagSub	Def0	True	Passed	Model Under Test Equivalent Model
34de02ca27054794860cfdf1672f6248981c8662	Apalache	BagBagSub	Def0	False	Passed	Model Under Test Equivalent Model
a25754b86422c8242f0fee263d970dcbe0f1ff37	Apalache	BagCopiesIn	Def0	True	Passed	Model Under Test Equivalent Model
2817e27b38b522238e4add041976330bb85247a7	Apalache	BagCopiesIn	Def0	False	Passed	Model Under Test Equivalent Model
4248db723890664d1993905003c0f3ceb43a1be2	Apalache	BagSubsetEqBag	Def0	True	Passed	Model Under Test Equivalent Model
34ffb4ce8e2424741cbe12f43bfb8cb667400140	Apalache	BagSubsetEqBag	Def0	False	Passed	Model Under Test Equivalent Model
24198af2cce11aee945ff269e9a885f178c2a5d9	Apalache	BagBagUnion	Def0	True	Passed	Model Under Test Equivalent Model
b508286ce1f452d2b73c74416beb27510a988a2e	Apalache	BagBagUnion	Def0	False	Passed	Model Under Test Equivalent Model
e6dc0c7d05f821c10af4a82b528cb4b640a74156	Apalache	BagBagCardinality	Def0	True	Passed	Model Under Test Equivalent Model
e4a14ff501ddc30184da7f2fe16a5a2f5dca3d45	Apalache	BagBagCardinality	Def0	False	Passed	Model Under Test Equivalent Model
2b580d1d67ef4e69328319d8b8e9f100bc93e6d4	Apalache	BagBagOfAll	Def0	True	Passed	Model Under Test Equivalent Model
a912808efca8a716cf2778ca87c32b74ed69567d	Apalache	BagBagOfAll	Def0	False	Passed	Model Under Test Equivalent Model
f982d7399b599717fb70678f774063619923d1df	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def0	True	Passed	Model Under Test Equivalent Model
e468cc790a68517ed03d858586bf2360923daa94	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def0	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
8e7f98bc6d23b8577db5e05966d5020d7117a1f8	Apalache	FiniteSetsCardinality	Def0	True	Passed	Model Under Test Equivalent Model
36d6bc035e7fff1553862134e2408a372fb7d7ee	Apalache	FiniteSetsCardinality	Def0	False	Passed	Model Under Test Equivalent Model
83354d6c048ba4a55c2137c9c348b0f966b1f34b	Apalache	SeqHead	Def0	True	Passed	Model Under Test Equivalent Model
525ccec070447ae0872a999e8efe78552d207d15	Apalache	SeqHead	Def0	False	Passed	Model Under Test Equivalent Model
006dbf16a08e9c46027c234ffaaf86359482e4c0	Apalache	SeqTail	Def0	True	Passed	Model Under Test Equivalent Model
8267e85ff8eccabdbb3febf2671232bc2f0465dc	Apalache	SeqTail	Def0	False	Passed	Model Under Test Equivalent Model
bae20536397e4fe0aec022e9ffe1422a622b6ddd	Apalache	SeqAppend	Def0	True	Passed	Model Under Test Equivalent Model
e97863d45bd071a5258871a3ba52a57485c17d22	Apalache	SeqAppend	Def0	False	Passed	Model Under Test Equivalent Model

Index

Tests by plug feature Def0; CLI Option: -workers 1