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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
15edfd7a85b3fbea3c5be61294ace4510e83bd45	Apalache	And	Def1Recursive	True	Passed	Model Under Test Equivalent Model
713fb2f4f12aa304412b24715430f1852f4722b5	Apalache	And	Def1Recursive	False	Passed	Model Under Test Equivalent Model
0f57d3eaed3f37fd0bdde593ff10eeb49fb37a85	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b39ef5e7a23d7f82abbfb07050ff55f37e88a111	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e07b31a2d4dbd75b431b968b7849c5a8c373adb5	Apalache	Imply	Def1Recursive	True	Passed	Model Under Test Equivalent Model
9783eb09bfcf6e4357d92c315340422962659d4a	Apalache	Imply	Def1Recursive	False	Passed	Model Under Test Equivalent Model
4896231436275e3e2bb94a5ad56148ef2db09736	Apalache	Not	Def1Recursive	True	Passed	Model Under Test Equivalent Model
21e8f84e69d1a65113e6763863ac64a94b949b9a	Apalache	Not	Def1Recursive	False	Passed	Model Under Test Equivalent Model
9a51755095fd6785d39d7f0afd523a37a1089ac2	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def1Recursive	True	Passed	Model Under Test Equivalent Model
afd190c177819ca9e70fd4543b87a18cb626e8cc	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Def1Recursive	False	Passed	Model Under Test Equivalent Model
01e44b7c85114262cd45c9ca1f38db7df353f2c1	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3dcf011c8f9799f0562e7e5dcd78bdf05eb03a96	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Def1Recursive	False	Passed	Model Under Test Equivalent Model
ea45a092f35a1079dabb16dfceddf8a8a40b3265	Apalache	AndProp	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d1af571805ff92212c8cae7f7e41a258eb769763	Apalache	AndProp	Def1Recursive	False	Passed	Model Under Test Equivalent Model
fa54cf770fbdf63592adea26535523cd2e0629e2	Apalache	Boxed	Def1Recursive	True	Passed	Model Under Test Equivalent Model
08349c57d402705385349c3cbb94153e3d807016	Apalache	Boxed	Def1Recursive	False	Passed	Model Under Test Equivalent Model
fe2f3fffe9cb0415125a3f432ae57498cdb82994	Apalache	Eq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f8706d31d6c59361fd55e5629d863d4d52e089a6	Apalache	Eq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
16a8bfa7e1621a5fc5a9a507f03ee27f078794c7	Apalache	Ne	Def1Recursive	True	Passed	Model Under Test Equivalent Model
13f5b9197fcb5bf9d208a5e403fc066335cab6c9	Apalache	Ne	Def1Recursive	False	Passed	Model Under Test Equivalent Model
34ad5a557cc07357fcdeb21e388c1cdff45925b2	Apalache	Let	Def1Recursive	True	Passed	Model Under Test Equivalent Model
941c0efef5183bd02182ad365ae658b9b2157168	Apalache	Let	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a35935b230447432d1fcfe3522ce9b8e3aecb0dd	Apalache	Set0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3c70daf1567cf8b51e9e2b6c5096ddedcb0c416a	Apalache	Set0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
eb8bf81541b9319a5940ed23771118492ba43673	Apalache	Set1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
6d997c80f3ca93661fc543899dae3dc0c31d2364	Apalache	Set1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e07a22a65197b47e65fca02f938d232d66c1b0c6	Apalache	Set2	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1ad62d3d61ff313c934aaba486da85a6712fd211	Apalache	Set2	Def1Recursive	False	Passed	Model Under Test Equivalent Model
62af23ac4192d85b746157328d9fdb65ace2f679	Apalache	Fun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1bd0a0764cf947b11558d93103adade0b2c0b2e1	Apalache	Fun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
6e548a40c23e06718e3acc7975b1b70a7bb7e9c4	Apalache	In	Def1Recursive	True	Passed	Model Under Test Equivalent Model
2a322a1ea361622ca6a972d3f5a648f09e5bc226	Apalache	In	Def1Recursive	False	Passed	Model Under Test Equivalent Model
622a9ba1869638a23f3df5b0d8fb8571cdb6c71f	Apalache	NotIn	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d16078f1011a3e1cbd8e20f200043086eb25b77e	Apalache	NotIn	Def1Recursive	False	Passed	Model Under Test Equivalent Model
7ff9232fc49e7439f93746a16ecc2298d50f9e7b	Apalache	Exists	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f5ae8b2cf7ba4e3f0b242ca845743a82da53575e	Apalache	Exists	Def1Recursive	False	Passed	Model Under Test Equivalent Model
0a5449487f2f5c3801cc869d848d8f40793cf51a	Apalache	Forall	Def1Recursive	True	Passed	Model Under Test Equivalent Model
625fe45051442aa717fb6fd56eb144d34d95f8a6	Apalache	Forall	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c1d892b27fc3f942069c75141a333f7f62c003c0	Apalache	Choose	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d2901fca5f9b8c389e5f394f4bf11db6ab18aebb	Apalache	Choose	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e5bb025ef8c852811fe6546b9630609c267284aa	Apalache	Record	Def1Recursive	True	Passed	Model Under Test Equivalent Model
5c77da7195cf87874ea9fa70c7cabee377f6ad6b	Apalache	Record	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a9ab769ce0d63a6c72c56a96f2f4bdb90e266836	Apalache	Tuple	Def1Recursive	True	Passed	Model Under Test Equivalent Model
5ac494f7dac2038fd1580b152c47ca0e0e18abd2	Apalache	Tuple	Def1Recursive	False	Passed	Model Under Test Equivalent Model
0c78036e5449af6f093b61f4b07c6ad3ac695f58	Apalache	FunApp	Def1Recursive	True	Passed	Model Under Test Equivalent Model
adb0269c991e2239b8c01977dc5b40ac1f8cdbab	Apalache	FunApp	Def1Recursive	False	Passed	Model Under Test Equivalent Model
3a9625ed3b88c1ad9799c49b149c627218da719a	Apalache	Except0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
ca9bed1dcb44753f2ba9e40efcfd65ebb3cae658	Apalache	Except0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
36d721a7f6817b19a9675fa2804195e1386f7294	Apalache	Except1Fun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
7adffe5fe45449ad8aae22ba296c96207a6b1574	Apalache	Except1Fun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a1c1a28220f493f1ae704126b5e1db52026b88ae	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def1Recursive	True	Passed	Model Under Test Equivalent Model
9469dc7485341fe6a918a7c70198c7e5e28d1ddf	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Def1Recursive	False	Passed	Model Under Test Equivalent Model
4fe2c10696550d126e22f8f4d940e06215fe4638	Apalache	Except1Rec	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b8d4aa8802eceec85fd8cce115e8aceacdefe5ca	Apalache	Except1Rec	Def1Recursive	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
37f5fa7593cd47007548ddbce0d15105ce33a7bb	Apalache	Except2Fun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
40425520a1bcb2f2393e2e3ec4fb6b65da243360	Apalache	Except2Fun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
9e9affdd26c4ce968c8f32e3f9033dcac9e50290	Apalache	Except2FunTuple	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3c43febdb571d1705c30eaeac80f1ae7743ae00b	Apalache	Except2FunTuple	Def1Recursive	False	Passed	Model Under Test Equivalent Model
2d13a43ea368b30a614897bcdf219bfd111c401c	Apalache	Prime	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d13a05ac34b71c3ba2270c2b057f50ab546c5d8a	Apalache	Prime	Def1Recursive	False	Passed	Model Under Test Equivalent Model
3d7297a98b6cdeaa343ea62baca008f814d90480	Apalache	NumUnaryMinus	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3d40b8560341704122af0c1b944a3183f3942d67	Apalache	NumUnaryMinus	Def1Recursive	False	Passed	Model Under Test Equivalent Model
73c116d5e77c666731009b6ae9af74bd828a463a	Apalache	NumPlus	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d1ec61d98c335b1c6b5aeede423ce1de1e16b707	Apalache	NumPlus	Def1Recursive	False	Passed	Model Under Test Equivalent Model
44083c3675623b6e8cf3760972e235f7213c2614	Apalache	NumMinus	Def1Recursive	True	Passed	Model Under Test Equivalent Model
990212ac33fb45b7ac530b7c49ca94b8eadd229b	Apalache	NumMinus	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f1258ad8d81f0ca4f1d97a171e241e778d068934	Apalache	NumMul	Def1Recursive	True	Passed	Model Under Test Equivalent Model
e3f83c9d2abb0f4b978d8e153f4d72de21d6a914	Apalache	NumMul	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e7ea8c576677f6987a72819d0303d009a6d217f1	Apalache	NumDiv	Def1Recursive	True	Passed	Model Under Test Equivalent Model
43ba074e79de1639d890e9950aa69bfe753e6ff9	Apalache	NumDiv	Def1Recursive	False	Passed	Model Under Test Equivalent Model
6bd319eb196b034efce9ded67086dfb5e3472c1e	Apalache	NumMod	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f7445d00c5df2721813cdf3b93f2ee26c69ae581	Apalache	NumMod	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a077a8779c4d40cafbf437d2cd724d2e96a68ab2	Apalache	NumPow	Def1Recursive	True	Passed	Model Under Test Equivalent Model
0b584e552b94e451533350a9b80a5060214b6d9d	Apalache	NumPow	Def1Recursive	False	Passed	Model Under Test Equivalent Model
8afee4149bc5185e38e0555798aadace997db4f0	Apalache	NumGt	Def1Recursive	True	Passed	Model Under Test Equivalent Model
cd9a28fb311c6ab7d07cbc0a18de768a82b8f2ed	Apalache	NumGt	Def1Recursive	False	Passed	Model Under Test Equivalent Model
49a8c3f62d313d29d303f4917dcffa8ab41ec076	Apalache	NumGe	Def1Recursive	True	Passed	Model Under Test Equivalent Model
dc7e5ece7587a141ae23bbd4d7b91e7e5c1b0a41	Apalache	NumGe	Def1Recursive	False	Passed	Model Under Test Equivalent Model
9394ca47020e0d451c83a624c023c0e60b413147	Apalache	NumLt	Def1Recursive	True	Passed	Model Under Test Equivalent Model
0cd1532518215ad490b1154701f3ee882c77b14b	Apalache	NumLt	Def1Recursive	False	Passed	Model Under Test Equivalent Model
78d957114e85cd2d25a88b20fba6317ce1a29b51	Apalache	NumLe	Def1Recursive	True	Passed	Model Under Test Equivalent Model
7425c5368ab290b6edca810ea47a64f29b0aec0e	Apalache	NumLe	Def1Recursive	False	Passed	Model Under Test Equivalent Model
7d0ac65f923fe941e11f734468d369ced03b33be	Apalache	DefFun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b38d2b93f29d841264b57bd2f8ec7f149b757d38	Apalache	DefFun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
084fa3888e7d644b3212f851233ae46fafa8f89c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f7a2d0262a4374daf8e035f800023008f0beec80	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
259cf02de8d399737b00d33dd88d9ae1e34af234	Apalache	DefFunRecursive	Def1Recursive	True	Passed	Model Under Test Equivalent Model
aacbc8255f2280c323c1f35c548eba2971cdefa7	Apalache	DefFunRecursive	Def1Recursive	False	Passed	Model Under Test Equivalent Model
ae2b741ff82977eca4ca857aac6fcf873cfe08b6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1aae3ab6d7eae1534bad7ade24d5a73dbfada0d6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Def1Recursive	False	Passed	Model Under Test Equivalent Model
4f65a980489316154e3aa3cc26b28febe0194e95	Apalache	Def0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
17a64bd5ea88c5dfea3110ffac4d16954d076d7c	Apalache	Def0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a993b96e1ab6bc824bac4f58a4199330fdd4f47a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
16c920966f79ca8c90069a9b3484aa31df4ee0b9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b4fbba4d895a8c87751176e066d3bac459034c7c	Apalache	Def1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b96185cd2e25fd5b5db6e5eb274694f6f5d146b6	Apalache	Def1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c0db27afa615cd6f13f55e44791f97d7d2f213b3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3ec1209c2beb6c65d28ca5396a82b1ad93b0f5ae	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
886dbe487d19f5085994d56d2a94f9f2412581db	Apalache	Def2	Def1Recursive	True	Passed	Model Under Test Equivalent Model
af818a3b8170cd55dc552bee878d84c7e5374956	Apalache	Def2	Def1Recursive	False	Passed	Model Under Test Equivalent Model
be4d008105e256cadd37495a86b38347d7d2ce30	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def1Recursive	True	Passed	Model Under Test Equivalent Model
589c41efeb1f5c8e770a39cd23a5138517a5f010	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Def1Recursive	False	Passed	Model Under Test Equivalent Model
82a20a5ad02ffecf62ec90bfafe0c0ee3dab2c20	Apalache	Def1Recursive	Def1Recursive	True	Passed	Model Under Test Equivalent Model
7c8e3e55e49e5a185e0cca0e20b82e681eedc5a2	Apalache	Def1Recursive	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b759100cbf91d767d81d06f523c6696384207514	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def1Recursive	True	Passed	Model Under Test Equivalent Model
ae723c42aacab051d1fc7efdc38c11b9951c0f67	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Def1Recursive	False	Passed	Model Under Test Equivalent Model
ad350d3276f2811a955f2ed53b2d61e74d974b0e	Apalache	Extends	Def1Recursive	True	Passed	Model Under Test Equivalent Model
0e765c0f5a0cbe9294217c021f8944f82cd204ed	Apalache	Extends	Def1Recursive	False	Passed	Model Under Test Equivalent Model
a54dc940f3da46ad8edc0fa8321ddfa26c9663bb	Apalache	ExtendsInDifferentFolder	Def1Recursive	True	Passed	Model Under Test Equivalent Model
744487f4b6b9192fd2b0425a91eb2705f1728a0f	Apalache	ExtendsInDifferentFolder	Def1Recursive	False	Passed	Model Under Test Equivalent Model
dead5be7ef8d5cb9528afbb3f19b20d9dfdf3a9c	Apalache	Variable	Def1Recursive	True	Passed	Model Under Test Equivalent Model
a736de12a9d62c8a9d24638e9e380e91d4d71f04	Apalache	Variable	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b17435aa8d8d6567438ac7e9fc62d35de11b0c0a	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def1Recursive	True	Passed	Model Under Test Equivalent Model
033dcc4b8b54a72b8072e9193579ae376fc0a9b5	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Def1Recursive	False	Passed	Model Under Test Equivalent Model
80b6d29fe93c8dff158fcf33d1889d5e8bf3afd7	Apalache	Constant	Def1Recursive	True	Passed	Model Under Test Equivalent Model
592e9e8a7ea4e0e83a260cc6efd924d732a4cc73	Apalache	Constant	Def1Recursive	False	Passed	Model Under Test Equivalent Model
42d47b52ffdc46e2226cd8125fa5a2dbecdc7d9c	Apalache	ConstantRank1	Def1Recursive	True	Passed	Model Under Test Equivalent Model
32b910c14e20d3ad962824bfc4d7eb08a30fb0a5	Apalache	ConstantRank1	Def1Recursive	False	Passed	Model Under Test Equivalent Model
57e2c800c95177d7f3933fc9a3d5fe8a50dfdee3	Apalache	Instance	Def1Recursive	True	Passed	Model Under Test Equivalent Model
a76c313f7a4b54b2592400092997d061597d62e0	Apalache	Instance	Def1Recursive	False	Passed	Model Under Test Equivalent Model
56fb9bdd4440a42023a507c4220fe246274786ce	Apalache	InstanceWith	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3e78a8eecac7da2b4bc865baee2356ae388cdec2	Apalache	InstanceWith	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c7676c9119e289289bba50b245e06ad7c606aed3	Apalache	InstanceNamed	Def1Recursive	True	Passed	Model Under Test Equivalent Model
665029201f3d7d47d291d065222cddfa7c73d3f5	Apalache	InstanceNamed	Def1Recursive	False	Passed	Model Under Test Equivalent Model
d04a66e0b59754f8ff1edba9c0bfe3be2e9b8210	Apalache	InstanceNamedWith	Def1Recursive	True	Passed	Model Under Test Equivalent Model
a5892fcc4e413fb4c173dd35d6cbf747c2f02b82	Apalache	InstanceNamedWith	Def1Recursive	False	Passed	Model Under Test Equivalent Model
c29f540c5b52c7c24122ca3912be2e948098ea61	Apalache	InstanceInFolder	Def1Recursive	True	Passed	Model Under Test Equivalent Model
51af4589c6f3d685d8dc19887f2050e3732d1912	Apalache	InstanceInFolder	Def1Recursive	False	Passed	Model Under Test Equivalent Model
94b61768f52fa17dafdd6d230829db5f2109d100	Apalache	InstanceWithInFolder	Def1Recursive	True	Passed	Model Under Test Equivalent Model
baf904b3cc8385abef2d5f8f0c94e0e1ae527694	Apalache	InstanceWithInFolder	Def1Recursive	False	Passed	Model Under Test Equivalent Model
627099c0d7441cc520b847c5d8ee3f9296c21d1d	Apalache	InstanceNamedInFolder	Def1Recursive	True	Passed	Model Under Test Equivalent Model
a0b36a225315073db7a858ead9968a5f9191b725	Apalache	InstanceNamedInFolder	Def1Recursive	False	Passed	Model Under Test Equivalent Model
0352bd344ed5314c7674806134a499f572281982	Apalache	InstanceNamedWithInFolder	Def1Recursive	True	Passed	Model Under Test Equivalent Model
501c48dfe004a38007b0ead3cbbee5de36e1497c	Apalache	InstanceNamedWithInFolder	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f50e224946e1954faf6cd2f828b5409a660da506	Apalache	Enabled	Def1Recursive	True	Passed	Model Under Test Equivalent Model
8bd0b1e0cf17dccd431453e24980d0ef99b27573	Apalache	Enabled	Def1Recursive	False	Passed	Model Under Test Equivalent Model
176c667c92d7c4c77ccb2efbda51417006189ea2	Apalache	Assume	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1fde01ccf66764d165d9d0541618fdc0e93d4c2b	Apalache	Assume	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f4d31af67ae7202115aabc716fecbd23110b522c	Apalache	AssumeNamed	Def1Recursive	True	Passed	Model Under Test Equivalent Model
4bf561a7bef14c6f319e34e658352bfe40d2f98a	Apalache	AssumeNamed	Def1Recursive	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
3635b9f401e6e54882784c1334b1d155bbc971c2	Apalache	Cross2	Def1Recursive	True	Passed	Model Under Test Equivalent Model
c0e730ebc0e8d93cc509aaa1813b3278ea4e4a08	Apalache	Cross2	Def1Recursive	False	Passed	Model Under Test Equivalent Model
5e0328920d0be1f6539fb05326dae02884bc556c	Apalache	Cross3	Def1Recursive	True	Passed	Model Under Test Equivalent Model
c64602f7c9a31fed0f7223a7dc4c099d842952c9	Apalache	Cross3	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b2e81680a67b73065be87d321364835e263e01e6	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	Def1Recursive	True	Passed	Model Under Test Equivalent Model
6ad3867777e3bd157e9f64423894516211e71532	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	Def1Recursive	False	Passed	Model Under Test Equivalent Model
661a545a94653fa8c05f38ef18c90880dd7483d2	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	Def1Recursive	True	Passed	Model Under Test Equivalent Model
4c1b01d1ebed66bd896a69317447a4e634a0db44	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	Def1Recursive	False	Passed	Model Under Test Equivalent Model
332417e636454c0ee4ae54295e6d16fafd78c00f	Apalache	SetDiff	Def1Recursive	True	Passed	Model Under Test Equivalent Model
9d6fc06c443ec2ea0d25498fa975ce2286e35ed5	Apalache	SetDiff	Def1Recursive	False	Passed	Model Under Test Equivalent Model
7f754562d8a58e0399721d8f0baddf475df73227	Apalache	SetUnion	Def1Recursive	True	Passed	Model Under Test Equivalent Model
b4d7dde28b8a602741482a571d0b1c31866fda7e	Apalache	SetUnion	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b4e304555983afac4d271a433c8c5c2f036483fe	Apalache	SetIntersect	Def1Recursive	True	Passed	Model Under Test Equivalent Model
2b711c0c8a06a466153a3a65acaecf97060fba60	Apalache	SetIntersect	Def1Recursive	False	Passed	Model Under Test Equivalent Model
99a24bdac04d029232fdf18a1340589add5fe89f	Apalache	SubsetEq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
167bc6111dc8a6863ca67e024cf9a001fa8450c9	Apalache	SubsetEq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
597b99e074a7879314bcc8912303e825919e837e	Apalache	IfCond	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3a6dc3789bf1716f461b6a211c383de7e07aa1fe	Apalache	IfCond	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e230b0f0940fd5e27ceaf556b46af75921979904	Apalache	IfThen	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d522db8ae6887fd664ff39ab95fe6f787d8136d7	Apalache	IfThen	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f213d83d7c4c625b770ab9154c6b1eb3efadb2ec	Apalache	IfElse	Def1Recursive	True	Passed	Model Under Test Equivalent Model
051ab1fb7ae020f3551c86dfd1f54dd15f5da601	Apalache	IfElse	Def1Recursive	False	Passed	Model Under Test Equivalent Model
77d55aac26af8ede48ac41d2d57e4a61258676df	Apalache	Subset	Def1Recursive	True	Passed	Model Under Test Equivalent Model
449884b06824c68bf2da258a7a11e1063a238d57	Apalache	Subset	Def1Recursive	False	Passed	Model Under Test Equivalent Model
426bf08b90b3c87607ed3fe4407be85a77c3bf5b	Apalache	Domain	Def1Recursive	True	Passed	Model Under Test Equivalent Model
16011e3dfe9c233f49cf7dfbf2ee6e41aa20a91c	Apalache	Domain	Def1Recursive	False	Passed	Model Under Test Equivalent Model
25cc55a13f088109e706bdf08e37f0210e45d67d	Apalache	Union	Def1Recursive	True	Passed	Model Under Test Equivalent Model
9a853201d4ab3ad6c6e07b3d563a9bf16950a4ac	Apalache	Union	Def1Recursive	False	Passed	Model Under Test Equivalent Model
7398422264a9641f23c013f9cc22e5fac8de6560	Apalache	Unchanged	Def1Recursive	True	Passed	Model Under Test Equivalent Model
f154f450f54419423a65fc74f7b60292e5164d36	Apalache	Unchanged	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f80b9dd743bca9a3669bbda72fef35dd3e2c42a3	Apalache	Equivalence	Def1Recursive	True	Passed	Model Under Test Equivalent Model
da3eab18fef0b7dfca5a2d665e27b03fb08a54cc	Apalache	Equivalence	Def1Recursive	False	Passed	Model Under Test Equivalent Model
13d35000ac38ea7228777ea600a64641dbdb1789	Apalache	SeqLen	Def1Recursive	True	Passed	Model Under Test Equivalent Model
6c4cfb79a866f1b86c8b347cf4859e48b446d1e4	Apalache	SeqLen	Def1Recursive	False	Passed	Model Under Test Equivalent Model
daee200ec2b9e76613eb11bc39d15004f406e6b6	Apalache	SeqConcat	Def1Recursive	True	Passed	Model Under Test Equivalent Model
577fb4d87e5a329e6ca82f76ffec85614571a254	Apalache	SeqConcat	Def1Recursive	False	Passed	Model Under Test Equivalent Model
d7d565ff6ea95ef97b0c841a3c110c558fbdb8fb	Apalache	SeqSeq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
fd5e4dfc98989b2b2d1aa7ce318c5f93d55ed8eb	Apalache	SeqSeq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b094f90f122eb7875ad88f40e7828fee8cb09647	Apalache	SeqSelectSeq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
fbc6e8f01a36d0f250156117649680d819bca1f3	Apalache	SeqSelectSeq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
67b73efeafdde041147a92d5b095bf7c2f4f0b68	Apalache	SeqSubSeq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1b093c337cb30207a1d55d3aa80a5a080f8aeabf	Apalache	SeqSubSeq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
3bf58e54756956c2efb464d94f1de0f1aea4bfd1	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	NumRange	Def1Recursive	True	Passed	Model Under Test Equivalent Model
c41d0a591b94f612e2eec2e390baddf1ca0ac2f6	TLC with reduction strategy: Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	NumRange	Def1Recursive	False	Passed	Model Under Test Equivalent Model
33390c559c07550ebdecb65f8ee4d150e102cfdc	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
d54797112b1245af1761ab0a9597a382fff2f4cd	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
330ba6f19bc3803e575e271baa796b0facef3c60	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	Def1Recursive	True	Passed	Model Under Test Equivalent Model
3978d8a47eca02de0e69c73b09a04d946d9b67f9	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	Def1Recursive	False	Passed	Model Under Test Equivalent Model
35111e9dad0ef29d6185427b87fa5496e441d825	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def1Recursive	True	Passed	Model Under Test Equivalent Model
1a48ae6071c3412536852befac8711af46d5fc99	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Def1Recursive	False	Passed	Model Under Test Equivalent Model
db7f829c7345550151ea8a2b7aa942ed15a5ba67	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
57c109c2b6ea87dcf7c9ee7b2a698f765aa4ae64	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e3d571e14e2fc1aca866b1bff5ee4c67ab8f791d	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def1Recursive	True	Passed	Model Under Test Equivalent Model
14fb969f4fdfa4cd18600ab7ae725813973a8bd1	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Def1Recursive	False	Passed	Model Under Test Equivalent Model
b510f44c08ea3131560e1bd4d7c68e0819910222	Apalache	BagBagToSet	Def1Recursive	True	Passed	Model Under Test Equivalent Model
60dca716cbc0e1f6fe411fc1808e917d97efe411	Apalache	BagBagToSet	Def1Recursive	False	Passed	Model Under Test Equivalent Model
3ec746cf58ae43cb4e99c8f01ffc6d80ca0829a3	Apalache	BagSetToBag	Def1Recursive	True	Passed	Model Under Test Equivalent Model
dae36bf900a04fba65a52d3207a98cc8351402a3	Apalache	BagSetToBag	Def1Recursive	False	Passed	Model Under Test Equivalent Model
8afe768d50ddc9898acd56437d98581c99bf6d63	Apalache	BagBagIn	Def1Recursive	True	Passed	Model Under Test Equivalent Model
bdb2a70d5071deca1c615a5ded2647150b83dddc	Apalache	BagBagIn	Def1Recursive	False	Passed	Model Under Test Equivalent Model
0bee3290bb73cf23f3a53ca69dfa68339ecfa765	Apalache	BagAddBag	Def1Recursive	True	Passed	Model Under Test Equivalent Model
6679caa023df85947c2a53636e1dea19e3c00ced	Apalache	BagAddBag	Def1Recursive	False	Passed	Model Under Test Equivalent Model
9ed01d36d4e2e72b45f00f4226e12835aa1e6369	Apalache	BagBagSub	Def1Recursive	True	Passed	Model Under Test Equivalent Model
732915111ebaef2e27c225c269df15647bb1b35b	Apalache	BagBagSub	Def1Recursive	False	Passed	Model Under Test Equivalent Model
f496a23e7470916c577de4b377a269ac8d286b6d	Apalache	BagCopiesIn	Def1Recursive	True	Passed	Model Under Test Equivalent Model
9315ad91c045501d95d1738110e5993b72a172a5	Apalache	BagCopiesIn	Def1Recursive	False	Passed	Model Under Test Equivalent Model
999acc050b055865f0b356b6c3b3bce390b20791	Apalache	BagSubsetEqBag	Def1Recursive	True	Passed	Model Under Test Equivalent Model
e5e3a2ac5bc25b2c3fd7ceef36245f5407d3e2e7	Apalache	BagSubsetEqBag	Def1Recursive	False	Passed	Model Under Test Equivalent Model
2cd7e54bab075637912a3b12c2d9ad1103811670	Apalache	BagBagUnion	Def1Recursive	True	Passed	Model Under Test Equivalent Model
bc4b1e6230f9b2a6049ad4ce195f5add0307babb	Apalache	BagBagUnion	Def1Recursive	False	Passed	Model Under Test Equivalent Model
08b123d7f24384e57b9fc7a9f062df66122e8eba	Apalache	BagBagCardinality	Def1Recursive	True	Passed	Model Under Test Equivalent Model
853845aedf8429d059d07b3ab17d2adde206afab	Apalache	BagBagCardinality	Def1Recursive	False	Passed	Model Under Test Equivalent Model
607284fdd30945d7cdff51b2b5200f517598867c	Apalache	BagBagOfAll	Def1Recursive	True	Passed	Model Under Test Equivalent Model
c3dcd807b7cc24c53d2cf56d2d43bd17d4fb1e8a	Apalache	BagBagOfAll	Def1Recursive	False	Passed	Model Under Test Equivalent Model
e0fa0ab8966ea7f249379f5e6e71837bd34c590e	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def1Recursive	True	Passed	Model Under Test Equivalent Model
66ccadb9ab2162d34d7b403c648d7defa0abd386	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Def1Recursive	False	Passed	Model Under Test Equivalent Model
8d87c35e87ae553addce88735fc47fce0daf4787	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Def1Recursive	True	Passed	Model Under Test Equivalent Model
2f3c217ce9ac5120e7ec4b218e4f302afb0d8290	TLC with reduction strategy: Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	FiniteSetsIsFiniteSet	Def1Recursive	False	Passed	Model Under Test Equivalent Model
6e30a0296d377f209ff335bbb558390e9bbc6798	Apalache	FiniteSetsCardinality	Def1Recursive	True	Passed	Model Under Test Equivalent Model
08fc88bfa8034d1ed63dd12cafe80dca43f2aabd	Apalache	FiniteSetsCardinality	Def1Recursive	False	Passed	Model Under Test Equivalent Model
996cfee789dae6223a2bf80dae528f7863cbbabe	Apalache	SeqHead	Def1Recursive	True	Passed	Model Under Test Equivalent Model
ea39f4ce603c323cc57a6fdb115e0f6524e0921c	Apalache	SeqHead	Def1Recursive	False	Passed	Model Under Test Equivalent Model
44aa79698dd07d49139b4636b0f7c39875887ff3	Apalache	SeqTail	Def1Recursive	True	Passed	Model Under Test Equivalent Model
35b91ea61e90d23359c5a865de1fc4224fbe6355	Apalache	SeqTail	Def1Recursive	False	Passed	Model Under Test Equivalent Model
2e03cf4b2d5a804b924c6b1b38a12480454de019	Apalache	SeqAppend	Def1Recursive	True	Passed	Model Under Test Equivalent Model
eff4828a022ad3cc35029bbefd64ec0eed3e02e1	Apalache	SeqAppend	Def1Recursive	False	Passed	Model Under Test Equivalent Model

Index

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