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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
640a5cf5364d6caff1d2a15c333ae1d2e5f85c08	Apalache	In	BoolTrue	True	Passed	Model Under Test Equivalent Model
6e940f6a9003363584a39ed56ec4b76c33a04916	Apalache	In	BoolTrue	False	Passed	Model Under Test Equivalent Model
a4541ea0c0616ffe6efb40a5c2333b461cad22bf	Apalache	In	BoolFalse	True	Passed	Model Under Test Equivalent Model
162d432a160919241ae93996ad57d842d149fc1b	Apalache	In	BoolFalse	False	Passed	Model Under Test Equivalent Model
718799844762de478a5fe4f61c54bcced95525ff	Apalache	In	BoolSet	True	Passed	Model Under Test Equivalent Model
3ee971595d81d5d00fdf97d9d032cb86bc420f28	Apalache	In	BoolSet	False	Passed	Model Under Test Equivalent Model
65ce41b483a2636da7a0606285d1e68e4127396e	Apalache	In	And	True	Passed	Model Under Test Equivalent Model
ffa6524a8879828fc800d7315f5fa46b2c1a23a1	Apalache	In	And	False	Passed	Model Under Test Equivalent Model
16fc86ea87cbbb64604bce770acd2bcdca69a82f	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	In	AndMultiLine	True	Passed	Model Under Test Equivalent Model
b3354d4f9e7775220f8063a755982dd7ceb2e6e1	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	In	AndMultiLine	False	Passed	Model Under Test Equivalent Model
dd73558a98f2e6f4ed10475ff1e6bcdc5361a361	Apalache	In	Imply	True	Passed	Model Under Test Equivalent Model
08a6d7c9ed0ad396e4e8c75b0d180a363493a948	Apalache	In	Imply	False	Passed	Model Under Test Equivalent Model
c01faef2df5deeee02540c37ff0324097a453d56	Apalache	In	Not	True	Passed	Model Under Test Equivalent Model
808f570465a6ac23e5ae888d79ab1f3a809e2174	Apalache	In	Not	False	Passed	Model Under Test Equivalent Model
28658ad66d625ba1839d528a0bcc79439de86ffd	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	In	Or	True	Passed	Model Under Test Equivalent Model
bf286efd5a8a2d6e05c79080eff22e5ebb1f21da	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	In	Or	False	Passed	Model Under Test Equivalent Model
e149b0326b5d83d249478a28346d9086e33abcfd	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	In	OrMultiLine	True	Passed	Model Under Test Equivalent Model
9e3e03fa7be6392a221c20094b61ea70a0dd4d6e	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	In	OrMultiLine	False	Passed	Model Under Test Equivalent Model
2c97f93cda295d21924a73e1a5cb47c5b3299517	Apalache	In	Eq	True	Passed	Model Under Test Equivalent Model
83d194b1e0960f33d17af10bfa736b58ec0f0697	Apalache	In	Eq	False	Passed	Model Under Test Equivalent Model
e75be4e0caaa60dc00b662d3aa723da4cac51f34	Apalache	In	Ne	True	Passed	Model Under Test Equivalent Model
f8e2359e693b218ce915a552628f4db5c4aba8e8	Apalache	In	Ne	False	Passed	Model Under Test Equivalent Model
cd830bd0efff8b79ab250cc90bcad631f1426adb	Apalache	In	Let	True	Passed	Model Under Test Equivalent Model
8a65292e6e4ee5c1635cb407486d9a75a2139102	Apalache	In	Let	False	Passed	Model Under Test Equivalent Model
9f9f23dc34a3921902962a318d676f2b007611ff	Apalache	In	SetEmpty	True	Passed	Model Under Test Equivalent Model
8efbcf19769fe049e32d6cef01cc305891bba58d	Apalache	In	SetEmpty	False	Passed	Model Under Test Equivalent Model
c46c61075a4d602e80010bc78e4b92ec34325533	Apalache	In	Set0	True	Passed	Model Under Test Equivalent Model
1e49103a311dfff02566df214836a6b5862c2248	Apalache	In	Set0	False	Passed	Model Under Test Equivalent Model
3b863e6217325abc25f14aa292cb796dba83a983	Apalache	In	Set1	True	Passed	Model Under Test Equivalent Model
9afb41abf400cb2aa7855cb087db35fa61cee6a9	Apalache	In	Set1	False	Passed	Model Under Test Equivalent Model
0baff7c1b4603055affee8e088df05829ab730b2	Apalache	In	Set2	True	Passed	Model Under Test Equivalent Model
b4e31ed97fcb3cc62be56c6154796732c28e20d5	Apalache	In	Set2	False	Passed	Model Under Test Equivalent Model
7c531193f77250f261767de9cfd715dcc639e373	Apalache	In	Fun	True	Passed	Model Under Test Equivalent Model
f6efff75a8c07b7b876eb94f01fd9f9d616d1201	Apalache	In	Fun	False	Passed	Model Under Test Equivalent Model
8523c13373a905b4738c273826f5e084b5c7462d	Apalache	In	In	True	Passed	Model Under Test Equivalent Model
d8ed2719b115301a59d67bc356a2585710e7b19c	Apalache	In	In	False	Passed	Model Under Test Equivalent Model
456dec3fab2e8e98f2f419c7611329596b796731	Apalache	In	NotIn	True	Passed	Model Under Test Equivalent Model
10179ce0ff73a4944cd467dcc3c8eb2e27d2978b	Apalache	In	NotIn	False	Passed	Model Under Test Equivalent Model
77aade69a87583f673b25b0af79254ad3a423eb5	Apalache	In	Exists	True	Passed	Model Under Test Equivalent Model
acf64dbe8cd7609fac078eef612b1ae86b1e883d	Apalache	In	Exists	False	Passed	Model Under Test Equivalent Model
83eced1aa8e1778c919a4e5f4ebe9799442a52f2	Apalache	In	Forall	True	Passed	Model Under Test Equivalent Model
67731f8a799b37b239abda8db527fa22de4a829c	Apalache	In	Forall	False	Passed	Model Under Test Equivalent Model
bfd5c00aaa9daf1be6fdf548644ad9f00d6516cb	Apalache	In	Choose	True	Passed	Model Under Test Equivalent Model
57e47f0fc54ad17c9d3a0e4e236b7855027ba554	Apalache	In	Choose	False	Passed	Model Under Test Equivalent Model
e76811d7f98d094d75f0589750753eb1f65fb8a0	Apalache	In	Record	True	Passed	Model Under Test Equivalent Model
797311527e7670a360f1a2a99f7b424bcf6ca31b	Apalache	In	Record	False	Passed	Model Under Test Equivalent Model
5563f52b0557c296fe9c9c64b1fefa1706d6fe08	Apalache	In	Tuple	True	Passed	Model Under Test Equivalent Model
0cedb3486cb89b58c131ffcf41a5aabcb944749d	Apalache	In	Tuple	False	Passed	Model Under Test Equivalent Model
4a813a1da83a1b10f959a2ca13a47d0663c64393	Apalache	In	TupleEmpty	True	Passed	Model Under Test Equivalent Model
254b1b243c78d8d78ddb8176f743de81d7a86a99	Apalache	In	TupleEmpty	False	Passed	Model Under Test Equivalent Model
b5017e2b23dc4eabdca6ed9bfd2d5932d6ff2327	Apalache	In	FunApp	True	Passed	Model Under Test Equivalent Model
eb2624d37d6ec8b3539f965362fe21b7e03e2c42	Apalache	In	FunApp	False	Passed	Model Under Test Equivalent Model
5a47849f4665291b8be141a3b71afb37ccc637eb	Apalache	In	Prime	True	Passed	Model Under Test Equivalent Model
075f8199098f8e80c7549a387fddf65d0da0ae15	Apalache	In	Prime	False	Passed	Model Under Test Equivalent Model
1462916011f34236efe0bf2ed5cb48f646f86374	Apalache	In	NumZero	True	Passed	Model Under Test Equivalent Model
834f00399a6239226fd84cc9b12d149edf4ab691	Apalache	In	NumZero	False	Passed	Model Under Test Equivalent Model
8958e3556ffd0715c937f472df3996d931f5eeda	Apalache	In	NumOne	True	Passed	Model Under Test Equivalent Model
40a000d184ddf924f6d817ea777423cf61c7932c	Apalache	In	NumOne	False	Passed	Model Under Test Equivalent Model
b6b6df802598b6da9af17ea63e3be7da59f89ea4	Apalache	In	NumMaxInt	True	Passed	Model Under Test Equivalent Model
5c0654444734603d5839b8dc6c0195d61be2da37	Apalache	In	NumMaxInt	False	Passed	Model Under Test Equivalent Model
a04494b354ec8ebaa55e95503c0b100f4d97fabe	Apalache	In	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
59c08f3a5d2ac57a7a2febfe56af6f888bd032dc	Apalache	In	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
7c008c140f8a4a51705dbffd099177c15541a2c3	Apalache	In	NumPlus	True	Passed	Model Under Test Equivalent Model
b928b07c5820bce7de2a33d3ebafd30f01b4fae4	Apalache	In	NumPlus	False	Passed	Model Under Test Equivalent Model
12a4cd713f1c7df713f05bad92ec840134a615b2	Apalache	In	NumMinus	True	Passed	Model Under Test Equivalent Model
a76d9fe04c247e53dd4c44c75e0187b92d0d5342	Apalache	In	NumMinus	False	Passed	Model Under Test Equivalent Model
6a0ab3e0d6efd5ddeb0dcec5f9051717a9399362	Apalache	In	NumMul	True	Passed	Model Under Test Equivalent Model
a31f2d9c478c5e31dd914a150bcf0840836054a0	Apalache	In	NumMul	False	Passed	Model Under Test Equivalent Model
c258317c8a15870d4cc3b523f2bc7578fdc9507a	Apalache	In	NumDiv	True	Passed	Model Under Test Equivalent Model
733ceb722503554718ef98aa2f36e14f089c9ea7	Apalache	In	NumDiv	False	Passed	Model Under Test Equivalent Model
56db03d47381a773b5fa786c09e4f187881ae171	Apalache	In	NumMod	True	Passed	Model Under Test Equivalent Model
e7896b91fee50954a8bac385b99c178a7fe82f89	Apalache	In	NumMod	False	Passed	Model Under Test Equivalent Model
93064032105949fc4b6c9fede25e32fe6e6a6cdd	Apalache	In	NumPow	True	Passed	Model Under Test Equivalent Model
198fd11362445f09f3c030839c604b208061877a	Apalache	In	NumPow	False	Passed	Model Under Test Equivalent Model
fdcc565456c0af133599d7cfffd7d6771b3e364d	Apalache	In	NumGt	True	Passed	Model Under Test Equivalent Model
d220a7764a06929f9f69f418d359939ff8d6052d	Apalache	In	NumGt	False	Passed	Model Under Test Equivalent Model
59e8f6dbd139573b3b20cc8280757bcec0e5262d	Apalache	In	NumGe	True	Passed	Model Under Test Equivalent Model
f1be5415e67af99a9340457f8926071343aa873a	Apalache	In	NumGe	False	Passed	Model Under Test Equivalent Model
e782b396c01ade52ec36c29ae3e11c7bbfd42677	Apalache	In	NumLt	True	Passed	Model Under Test Equivalent Model
4e4d878300abf0b284143e72d7e4773b0a92b827	Apalache	In	NumLt	False	Passed	Model Under Test Equivalent Model
9350e7bba357c81f36f5b234311f0c8556bffe32	Apalache	In	NumLe	True	Passed	Model Under Test Equivalent Model
cc3fb509e6ea231e2c59203477610f2f2da7223b	Apalache	In	NumLe	False	Passed	Model Under Test Equivalent Model
9442167e794e031754a3491cb34e4d10aeed015c	Apalache	In	DefFun	True	Passed	Model Under Test Equivalent Model
0b7888d030bfe2f04e556b104de0f9e72219aa8e	Apalache	In	DefFun	False	Passed	Model Under Test Equivalent Model
0fefb64e4c186545ea18f247b1a6b88c2b44b07c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDefFun	True	Passed	Model Under Test Equivalent Model
f075ea0b41a4052c7fb3dd3ad4314ea4443ff463	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDefFun	False	Passed	Model Under Test Equivalent Model
d31e1ee5d08300f59b5b051d92fb4bd4ba591e64	Apalache	In	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
40f3e5ef48d492b9d0159fc1a8552aacd220f873	Apalache	In	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
34ec4cc5dca46663b77b0ac53a357422bd9f7f94	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
440e9968d7e7b23694fd0230a5fd23c4804f1c2c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDefFunRecursive	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
29c1792fc93e5ac3e54bebb8c213e5c60e3bbfa8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef0	True	Passed	Model Under Test Equivalent Model
ec2a8e1875f4b36bfc5fbd207a350334b32f18b2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef0	False	Passed	Model Under Test Equivalent Model
de06326e11f56f2ccf4f879cad71db3937537b8f	Apalache	In	Def1	True	Passed	Model Under Test Equivalent Model
7c21521f946accc87ca5149dfaee4323cbc221ff	Apalache	In	Def1	False	Passed	Model Under Test Equivalent Model
294ede688d022ffdabae95ab1413fe109f0d8e6f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef1	True	Passed	Model Under Test Equivalent Model
2207fc879c727f673475d61da421bf2c522937c1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef1	False	Passed	Model Under Test Equivalent Model
58d315a33fe7a045f11041383ffac95950871ef3	Apalache	In	Def2	True	Passed	Model Under Test Equivalent Model
4fd2b68fadbdf91e0a53d5417ab9720a5340678c	Apalache	In	Def2	False	Passed	Model Under Test Equivalent Model
060051e051a1527f0fa11c893cd669bc03917e86	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef2	True	Passed	Model Under Test Equivalent Model
97c2f40e6f29a2cbee1f18aaf65ca015eab58d6b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef2	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
035181f57e434c5d24528312ae6b98256b0f7362	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
0d6acc2b3e4b54d0c604fffb54057170480b711a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	In	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
360b2a1ec0c60c559a938364ae6cd3f4b557b727	Apalache	In	Extends	True	Passed	Model Under Test Equivalent Model
bf703938ab6bb267b734305c14edd225ac9fe637	Apalache	In	Extends	False	Passed	Model Under Test Equivalent Model
7e8be95b3877b337bbab3eed401bf0280c1f055c	Apalache	In	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
3c74573af1ee266e7b79c93e75c0fed1d0026269	Apalache	In	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
dda3ae70adc9357cd6dc2e914032bbab64a77b19	Apalache	In	Variable	True	Passed	Model Under Test Equivalent Model
1b39d96129ff99596fddc891462fe9ad2b1c16d6	Apalache	In	Variable	False	Passed	Model Under Test Equivalent Model
1c2260baad40918920bc7f7626bffbb0079e5cfe	Apalache	In	Constant	True	Passed	Model Under Test Equivalent Model
c2a71ef48401966fc89b7dbdf4bb48e2b2527cbc	Apalache	In	Constant	False	Passed	Model Under Test Equivalent Model
056e5518d99b58c23a6a2f0fe8658d83e82b1735	Apalache	In	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
71d3cb0bd6f17ca0c87469338d06d6d932059fcf	Apalache	In	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
9d7433eeb66bdadf90e54af6e4ac346c7cbc0a1b	Apalache	In	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f912d0d3e6254c97da41e0d60aca17fee05cb7f1	Apalache	In	ConstantRank1	False	Passed	Model Under Test Equivalent Model
70802044075a32bd8511516444386ec3d3f20f87	Apalache	In	Instance	True	Passed	Model Under Test Equivalent Model
af0d4cf96778442a712d27fff9057ec9e0039465	Apalache	In	Instance	False	Passed	Model Under Test Equivalent Model
b8bdbe49101b09e3e8af2a4879c3be83a6084983	Apalache	In	InstanceWith	True	Passed	Model Under Test Equivalent Model
a347d76e0c059157820caa17428e62900066d005	Apalache	In	InstanceWith	False	Passed	Model Under Test Equivalent Model
5e8c75f7b6a18bda2dbc9b43666d6eb7183bed40	Apalache	In	InstanceNamed	True	Passed	Model Under Test Equivalent Model
d414c56332bc41a9b08ec10e5baae9df29b241d3	Apalache	In	InstanceNamed	False	Passed	Model Under Test Equivalent Model
d70d074e58d09cec4676496166cacba56425be1e	Apalache	In	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c6e9b487bef17cf38cf3ce57a3b878ce46380aaa	Apalache	In	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
049bff06d6a9d7ac84524861d91cabad94a0674f	Apalache	In	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
3ddad21c5812773ea46e85dd92a936a858784442	Apalache	In	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
40459e2b6529623897d4f2f0befa7c432ccff5bc	Apalache	In	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
e0ffa75878b980d75ed36dd172bf23708642e64b	Apalache	In	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
1ee65defdefc4a29413be4e23c990915240da35f	Apalache	In	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
86bcf07188dac4032cf01105882bfba02646de04	Apalache	In	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
ed2bc7282556564473617088ddec6a0676a33c6e	Apalache	In	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
fda960a2e62fa6088b07ff85e20e544c65db2d1a	Apalache	In	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
01e84074de3da0825a00585b094bd8beff2665de	Apalache	In	Enabled	True	Passed	Model Under Test Equivalent Model
2433487fab6117dd41c5ea3c47d29c30bbcbb86e	Apalache	In	Enabled	False	Passed	Model Under Test Equivalent Model
9b48bab97f695c94f7e9ab77d13e555a99611765	Apalache	In	Cross2	True	Passed	Model Under Test Equivalent Model
663b0d5250265fb9c9d591f12f506f4b8a7b48e9	Apalache	In	Cross2	False	Passed	Model Under Test Equivalent Model
9cedf0d4c5e11bfe0fba469d8c22188202c3eec6	Apalache	In	Cross3	True	Passed	Model Under Test Equivalent Model
0271e2794c361f95adc5fb662aa1bc812a360cd3	Apalache	In	Cross3	False	Passed	Model Under Test Equivalent Model
27c128f7f5b0d19d8c8ffb60c23746a36d3d0205	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))	In	FunSet	True	Passed	Model Under Test Equivalent Model
57a70dc853b46740fb3f57c5fe2e76af41754666	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))	In	FunSet	False	Passed	Model Under Test Equivalent Model
b5940710d5241bad83217963002f991ba2179888	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)	In	RecordSet	True	Passed	Model Under Test Equivalent Model
8700eef09672cefde024aad5d2793daf6d77707b	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)	In	RecordSet	False	Passed	Model Under Test Equivalent Model
07638d03119281582d50ffaa75173657870dade0	Apalache	In	SetDiff	True	Passed	Model Under Test Equivalent Model
76bd4a855c34a17da934464bea9ceb920eeec402	Apalache	In	SetDiff	False	Passed	Model Under Test Equivalent Model
6944782d2d75c7b8acf8d1b618cdc6349ff9cbc6	Apalache	In	SetUnion	True	Passed	Model Under Test Equivalent Model
4fe2a8ada2ab8032a1a4434e8ccd2c6632a455c4	Apalache	In	SetUnion	False	Passed	Model Under Test Equivalent Model
945012cf97fc05f68df74034acbc1373d92036f0	Apalache	In	SetIntersect	True	Passed	Model Under Test Equivalent Model
ec31348acd9d2607f5a82f289b79186ba5b70f45	Apalache	In	SetIntersect	False	Passed	Model Under Test Equivalent Model
73f89f6b570cf951f19dd203b206903305b91b78	Apalache	In	SubsetEq	True	Passed	Model Under Test Equivalent Model
c3d6cea1346664fc1fc0382612023ea8d00439ba	Apalache	In	SubsetEq	False	Passed	Model Under Test Equivalent Model
c951dee68907fd401bf6596cc142bd9fb7afc4a7	Apalache	In	IfCond	True	Passed	Model Under Test Equivalent Model
80eac861073e7f69b1381b9924421a42862495cb	Apalache	In	IfCond	False	Passed	Model Under Test Equivalent Model
3a26a9f26dec697918993c84cc92d241fb0c5122	Apalache	In	IfThen	True	Passed	Model Under Test Equivalent Model
1fb2479b22dbd719a26f9e2189f5823779f139a4	Apalache	In	IfThen	False	Passed	Model Under Test Equivalent Model
560c908055c2742d05f1257613463efb14c98a40	Apalache	In	IfElse	True	Passed	Model Under Test Equivalent Model
b308e7c12616fa624d6e30ff7abd5daa6eb5f04c	Apalache	In	IfElse	False	Passed	Model Under Test Equivalent Model
b01bca57354d7bc7dd9d9ba014b9b41f0fe401c3	Apalache	In	Subset	True	Passed	Model Under Test Equivalent Model
ec2d081c6aa15d16d62db9151e200bc112bfc0b7	Apalache	In	Subset	False	Passed	Model Under Test Equivalent Model
bec563c1b452a050895632ba40b41408dda890ef	Apalache	In	Domain	True	Passed	Model Under Test Equivalent Model
308785cb3b4c38f969981c1e3e023cbef1c89307	Apalache	In	Domain	False	Passed	Model Under Test Equivalent Model
7ac4ed896e45c191b7bdb22c4d1eb9491e722b79	Apalache	In	Union	True	Passed	Model Under Test Equivalent Model
d2362710be8fd755654b962e76dd3806b9cddf20	Apalache	In	Union	False	Passed	Model Under Test Equivalent Model
9143c191a43897a0d9e5d30770d615371b0e5e4c	Apalache	In	Unchanged	True	Passed	Model Under Test Equivalent Model
5f54a581d4ab64f833520d949e63afd950167504	Apalache	In	Unchanged	False	Passed	Model Under Test Equivalent Model
9a4f2c5ec0fe2bcf44f54c07bb303fbb5bdca5a9	Apalache	In	Equivalence	True	Passed	Model Under Test Equivalent Model
27c6cb08a99d2e4db9524b71590da38d275ec463	Apalache	In	Equivalence	False	Passed	Model Under Test Equivalent Model
ed77a60f22e7fb97829f2a3082d78dfcad1dd924	Apalache	In	StringEmpty	True	Passed	Model Under Test Equivalent Model
dd1ecc20ba4dc4087ca51982d1e29eddb74d8ca5	Apalache	In	StringEmpty	False	Passed	Model Under Test Equivalent Model
f68b4bab7268ead1ceb4f0826e9ff19e40d04d44	Apalache	In	String	True	Passed	Model Under Test Equivalent Model
5ae29c1838514df4042f8d21e9407204f0396bbf	Apalache	In	String	False	Passed	Model Under Test Equivalent Model
569658de138456a43f894978ae3f0a59cb27fabf	Apalache	In	SeqLen	True	Passed	Model Under Test Equivalent Model
e1187df0c2aedc760eeb6741afe2ed535417eb4f	Apalache	In	SeqLen	False	Passed	Model Under Test Equivalent Model
9add2131c1abf7d4ec58aa00c408be27bd391f9a	Apalache	In	SeqConcat	True	Passed	Model Under Test Equivalent Model
a8a7fc2adeb5eea6e44def384fd1f67ad03542f8	Apalache	In	SeqConcat	False	Passed	Model Under Test Equivalent Model
3e9a5d262c6c778d4b324a4150f3d1177cab9256	Apalache	In	SeqSeq	True	Passed	Model Under Test Equivalent Model
68b0919b779c9fae97f7ad96230b98381981e0e9	Apalache	In	SeqSeq	False	Passed	Model Under Test Equivalent Model
57467abad19a6ff7e1944ca8f5ee33899a5b1de0	Apalache	In	NatSet	True	Passed	Model Under Test Equivalent Model
54c7176ac91d77a1725d1c092c2502cabbbae0b8	Apalache	In	NatSet	False	Passed	Model Under Test Equivalent Model
e747106d5f66198ec2e801c3cfd2616cb1f975a1	Apalache	In	IntSet	True	Passed	Model Under Test Equivalent Model
d84904b2883396232e0217281725209e6f637e15	Apalache	In	IntSet	False	Passed	Model Under Test Equivalent Model
347e4ce30c32168e44ce7f2f77cd3f25d788df3d	Apalache	In	StringSet	True	Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)	Model Under Test Equivalent Model
5b442ba072d614832a279cd934bf72d58bd3e78a	Apalache	In	StringSet	False	Failed: TLC result is correct. Apalache does not support STRING expression (a set of all strings)	Model Under Test Equivalent Model
e7d72d3d122b51c75d999e9ecc61a144a45927e7	Apalache	In	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
8d69c357ebc1b38631dc7e156176a95858a064ed	Apalache	In	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
436f51adc70ec59fc3dac47d7b35df954ad27c2c	Apalache	In	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
ea4e578f9160a24cfa986b270bd1f9a720f518aa	Apalache	In	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d25c2eb5ad1eb8ece6ecf349e21cc13fa8b1e9c2	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	In	NumRange	True	Passed	Model Under Test Equivalent Model
484b9a59846900104d89c83f11473d8aaa12367a	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	In	NumRange	False	Passed	Model Under Test Equivalent Model
67217e3ee855048e108ecfa3182dd8ecf3b214b4	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	In	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
f0d735ae774201969656bd9c7e2d532c80646861	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	In	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
ff0487250ebc8f129a5517a5f1b8e7f2a1806926	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]]	In	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
f9da2c68a726c25fb0cd9e7d583e317c9131f75b	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]]	In	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
d4728ef479da1146e5a0c9d9cd4eb24fdaef8ac8	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	In	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
4571b02cce03f161f74f436fdec2fe1c75091e70	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	In	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
676e2336f89b2ce33ff52310a1682d3493d637d9	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	In	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
593c6e47b6e4181a13e273a4e302e3b49e01120c	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	In	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
53a26c9d2c5bf67e93b7275bcb93e3481c17f42d	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	In	TlcEval	True	Passed	Model Under Test Equivalent Model
9a15e016b36e38885c3a4042e4219ae854f97f2a	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	In	TlcEval	False	Passed	Model Under Test Equivalent Model
49146980793a80d2bb912565e30d01468ebee9c4	Apalache	In	BagBagToSet	True	Passed	Model Under Test Equivalent Model
2c70ae8ce9e92c139b6e3e861c8f7adfd6d4adaa	Apalache	In	BagBagToSet	False	Passed	Model Under Test Equivalent Model
f574836ac96bd2c15ef37f342a71d6a0c7b532ef	Apalache	In	BagSetToBag	True	Passed	Model Under Test Equivalent Model
3790607ffd3df962b24e52cfce7c28051e59860f	Apalache	In	BagSetToBag	False	Passed	Model Under Test Equivalent Model
3333965b6c77a346a9c6dfdfa55a87a991e8de98	Apalache	In	BagBagIn	True	Passed	Model Under Test Equivalent Model
b69b2dec7a6ea1a8fe930e19e54d4c33b466bad0	Apalache	In	BagBagIn	False	Passed	Model Under Test Equivalent Model
20de4fb7dbd902349d3a8b001aeaa02f9e47fa4a	Apalache	In	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
eeac84e54292ed05a8a66eb5d8166307bebfe66f	Apalache	In	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
54c429176f802513382b1de8fca37f9677f00386	Apalache	In	BagAddBag	True	Passed	Model Under Test Equivalent Model
bac715ef484bbda92309906006d1ef286babc8f0	Apalache	In	BagAddBag	False	Passed	Model Under Test Equivalent Model
dcad1cb4d69f55487422289e1d529fb823b4add1	Apalache	In	BagBagSub	True	Passed	Model Under Test Equivalent Model
ae2970c0b7daf2b84dbe22f24c632e1902c4e848	Apalache	In	BagBagSub	False	Passed	Model Under Test Equivalent Model
bfa6f38bfa13479af99b8d1db3fbf6eff718e527	Apalache	In	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
988f9dfcb931dbf41c37f4ad3ee117b4192c8ec4	Apalache	In	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
4ab2d41b97e68cc4effd64d6b74852d3d7843541	Apalache	In	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
9b7cb3b6fbab2c55bae7ffae9ac09627d29232bd	Apalache	In	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
4d7d567d46fe77ac36a499d199d48b4072cf6930	Apalache	In	BagBagUnion	True	Passed	Model Under Test Equivalent Model
23b4fae496ee96db87772223780bf2dcb3b85818	Apalache	In	BagBagUnion	False	Passed	Model Under Test Equivalent Model
724ec77b75a4b3d3d7462a19c3ef687639a892f5	Apalache	In	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
bacfd70f3ff9f773a48b1cbeb5de4d2bbfcdd39d	Apalache	In	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
92bec56fdfe45eecb00497ce47418212d14c8366	Apalache	In	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
7295980d8250442c5f321c1242f1832ca4edb72b	Apalache	In	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
d2530c0ce8b1d5c120e6acc752a8b935de6d3867	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	In	BagSubBag	True	Passed	Model Under Test Equivalent Model
9181b1abf2998fe5e13a16cb5a5d1605c3f0c432	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	In	BagSubBag	False	Passed	Model Under Test Equivalent Model
1836c75e82d3fcdb215e29ea893ce919d7579b66	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)	In	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
bb16f025cb035ee4847b500a6c5d0c10023afda0	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)	In	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
5b9ef08e7ac6101169cc38a9bb6003d56fba708c	Apalache	In	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
3fdaa7190b9bedaa515ebaf1b4708ca1e1545862	Apalache	In	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
204e2b34cc9a27862556f3a55f664159954a85e0	Apalache	In	SeqHead	True	Passed	Model Under Test Equivalent Model
d12d34831119feccf21833bdb07d79ddd13a57b6	Apalache	In	SeqHead	False	Passed	Model Under Test Equivalent Model
394739d4b7e0b6e1d9ca04481ee62edcb8bc07a7	Apalache	In	SeqTail	True	Passed	Model Under Test Equivalent Model
40d838f042a757f600120cc7087cadb5a0bc7b87	Apalache	In	SeqTail	False	Passed	Model Under Test Equivalent Model
89cc5bc84a895a2ad41652b0262a66ba02020a62	Apalache	In	SeqAppend	True	Passed	Model Under Test Equivalent Model
7dfe35ac77eaa9da565733240d994bae531e0459	Apalache	In	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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