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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
583bdc6b68b3fc503748593d9b79829b84ffdc93	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set2	OneLineComment	True	Passed	Model Under Test Equivalent Model
a67d797c218cdd40ee2fc45fd6faaa7c61936b35	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set2	OneLineComment	False	Passed	Model Under Test Equivalent Model
00f1a1d4dee6aef83b39e15bb06c30fa38257d3c	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set2	MultiLineComment	True	Passed	Model Under Test Equivalent Model
06c565f260ece63643682f8219633e4ec0199618	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Set2	MultiLineComment	False	Passed	Model Under Test Equivalent Model
85e8af4d0eabec6001850abe5c089c405f55f236	Apalache	Set2	BoolTrue	True	Passed	Model Under Test Equivalent Model
54504b579f568f7bb7e72f3e2c71e0ab764bb984	Apalache	Set2	BoolTrue	False	Passed	Model Under Test Equivalent Model
f928a6d04712d14d5ac0ec7296fa98fadf2470af	Apalache	Set2	BoolFalse	True	Passed	Model Under Test Equivalent Model
a3ad33ede5fca116c67b64440e406c4bb98108f3	Apalache	Set2	BoolFalse	False	Passed	Model Under Test Equivalent Model
a55bca863bee2a9caf6dec1803ed94b54b40d802	Apalache	Set2	BoolSet	True	Passed	Model Under Test Equivalent Model
a0f6464645a0f6e27840c127e374734aea18c705	Apalache	Set2	BoolSet	False	Passed	Model Under Test Equivalent Model
53580c96fca888df598dbe2a03a5c786e123711c	Apalache	Set2	And	True	Passed	Model Under Test Equivalent Model
2bdff88b939a033ccc0b39545c45d86a78290f18	Apalache	Set2	And	False	Passed	Model Under Test Equivalent Model
be452db73c83632fba375cfba2bc0613d44768a7	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Set2	AndMultiLine	True	Passed	Model Under Test Equivalent Model
7ad18c88cf14cc1a73a6de58dc769c8ca37c64ce	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Set2	AndMultiLine	False	Passed	Model Under Test Equivalent Model
33e7db235133b1cb755bbccd621842f1b13a58f2	Apalache	Set2	Imply	True	Passed	Model Under Test Equivalent Model
6f5482c1f4eed94b7a5de7c14217a28a6afe8a1c	Apalache	Set2	Imply	False	Passed	Model Under Test Equivalent Model
32ced51d7bad6caf609a4c50261bf822dbc2851f	Apalache	Set2	Not	True	Passed	Model Under Test Equivalent Model
e90de7743fb232f037e638ecd064f1865fd68085	Apalache	Set2	Not	False	Passed	Model Under Test Equivalent Model
7214d1ba981c6c64725a14690393f673d5dcd837	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Set2	Or	True	Passed	Model Under Test Equivalent Model
cedef707e29d29fc1f2d5a8d12a13ac993e2d8e1	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Set2	Or	False	Passed	Model Under Test Equivalent Model
c5906e353e0c095011eee7ecbf7451089dbfab9d	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Set2	OrMultiLine	True	Passed	Model Under Test Equivalent Model
f3eddac0f10530b47104a50af69d42b2ecf35de6	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Set2	OrMultiLine	False	Passed	Model Under Test Equivalent Model
6d804f73c3a5f911f982bac2b069f0ab9edf68b7	Apalache	Set2	Eq	True	Passed	Model Under Test Equivalent Model
95b347204986f996bd4e769d9c12e433460ec212	Apalache	Set2	Eq	False	Passed	Model Under Test Equivalent Model
1d0573d69a874b42ccda3b82c19369b1543fdb9e	Apalache	Set2	Ne	True	Passed	Model Under Test Equivalent Model
73aefcd248061c250ec5389b99568b0d97b93a84	Apalache	Set2	Ne	False	Passed	Model Under Test Equivalent Model
df1a355a5b933cb9ebdec21e06ed2388d2506016	Apalache	Set2	Let	True	Passed	Model Under Test Equivalent Model
98bed916b5e1461502faeabe0e956910365b21ae	Apalache	Set2	Let	False	Passed	Model Under Test Equivalent Model
99f69e968f378d777007b7e8a1f8c06759a108af	Apalache	Set2	SetEmpty	True	Passed	Model Under Test Equivalent Model
8350d6b68338817685dadc9177339a7262189fd6	Apalache	Set2	SetEmpty	False	Passed	Model Under Test Equivalent Model
4920420437000010f862ca566172e38a39a201c2	Apalache	Set2	Set0	True	Passed	Model Under Test Equivalent Model
50218a0e287364d2df68b3780add12ba39d1af0e	Apalache	Set2	Set0	False	Passed	Model Under Test Equivalent Model
89bb8ebb57a1bce8760c2d6bc5662a20a926dee5	Apalache	Set2	Set1	True	Passed	Model Under Test Equivalent Model
c66659e3e601ad7fb675bd0d7c03ee108150cf60	Apalache	Set2	Set1	False	Passed	Model Under Test Equivalent Model
424ab54c3792f3dbb573a3e0f86bdc07b0263ce6	Apalache	Set2	Set2	True	Passed	Model Under Test Equivalent Model
89ffcc238b6073552d6bba98dd76f2a8235b1fa1	Apalache	Set2	Set2	False	Passed	Model Under Test Equivalent Model
471c3474904f97a59f9a7fc23a4d3d3c0694fbb7	Apalache	Set2	Fun	True	Passed	Model Under Test Equivalent Model
ca5247593b533e0b75bc27692922ed845e20046d	Apalache	Set2	Fun	False	Passed	Model Under Test Equivalent Model
58cefc6e1e01dea6bba6d673d5fa242f8bc107e7	Apalache	Set2	In	True	Passed	Model Under Test Equivalent Model
4789a949d0fd33ce514cb1505af0a78ed8311ace	Apalache	Set2	In	False	Passed	Model Under Test Equivalent Model
1c1b514c7db1636e816586b00099a05fae6f7bdd	Apalache	Set2	NotIn	True	Passed	Model Under Test Equivalent Model
fdb75b3b4f724d6222a0d2cead5fda5aaaed85f1	Apalache	Set2	NotIn	False	Passed	Model Under Test Equivalent Model
b32dfa3fdbe2faa1e49a8f8f7951d17ecb1ef290	Apalache	Set2	Exists	True	Passed	Model Under Test Equivalent Model
b3ff89cf279ae41aa9aaad855ac953e88976efbf	Apalache	Set2	Exists	False	Passed	Model Under Test Equivalent Model
6ae14c726d224fb7f3ca53c93439c1d2bd420812	Apalache	Set2	Forall	True	Passed	Model Under Test Equivalent Model
25d8db4c6808f8f79c18cc4ca1781fbfab777893	Apalache	Set2	Forall	False	Passed	Model Under Test Equivalent Model
c7bab1fadea3ed99b428f2c1f30d55a3234b7b39	Apalache	Set2	Choose	True	Passed	Model Under Test Equivalent Model
7e590ebff5cbcb4b956d86cd0b969161b78f3240	Apalache	Set2	Choose	False	Passed	Model Under Test Equivalent Model
d2d67a4e64b55f7583aca9ea2992bf39d1f9f1bc	Apalache	Set2	Record	True	Passed	Model Under Test Equivalent Model
8a1e81eab8e52191dda7097c97d8ee79e081c1f8	Apalache	Set2	Record	False	Passed	Model Under Test Equivalent Model
61c99906e16b36ed6a9b80dee08291c23f3de330	Apalache	Set2	Tuple	True	Passed	Model Under Test Equivalent Model
5722e003a5f851eebdaac51efcf211355d35ccf4	Apalache	Set2	Tuple	False	Passed	Model Under Test Equivalent Model
2f3c2a45d5c517d708597199587dbd7adeafcd4c	Apalache	Set2	TupleEmpty	True	Passed	Model Under Test Equivalent Model
4336372eae4ce5073eff1b008b1526ca1b94642a	Apalache	Set2	TupleEmpty	False	Passed	Model Under Test Equivalent Model
7b4ff9a807b6edf739146496479f1d28edab96ab	Apalache	Set2	FunApp	True	Passed	Model Under Test Equivalent Model
931b7f830096ccd52670e5b89dbb1d3124420e09	Apalache	Set2	FunApp	False	Passed	Model Under Test Equivalent Model
c3a25c35562c83e2f8efcf3e8be3d04f92eeee35	Apalache	Set2	Prime	True	Passed	Model Under Test Equivalent Model
3b754917419b81b751bcc7d93022bf0691c88ee7	Apalache	Set2	Prime	False	Passed	Model Under Test Equivalent Model
0787a1e9df22d4756a7613c6f916372fd3a8f9f1	Apalache	Set2	NumZero	True	Passed	Model Under Test Equivalent Model
22020b954a5bc196d7ec5cb59f9a1fe81526f461	Apalache	Set2	NumZero	False	Passed	Model Under Test Equivalent Model
3070d856f592455c1e2f46fba1fb37a0438810f1	Apalache	Set2	NumOne	True	Passed	Model Under Test Equivalent Model
52124197cd92d8b1988fb184b05867e9799d0892	Apalache	Set2	NumOne	False	Passed	Model Under Test Equivalent Model
19ecd84495ab8c599fd4aaa5efed5e442dc1b73e	Apalache	Set2	NumMaxInt	True	Passed	Model Under Test Equivalent Model
34e7b535ee83dd4f099d4dd3f741147d0f819717	Apalache	Set2	NumMaxInt	False	Passed	Model Under Test Equivalent Model
05bdb2c7e72853e52371a506cf0a30cfd019e2fd	Apalache	Set2	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
d2ae253a1e76d6b1f7601a69152cdc37a7eae8d4	Apalache	Set2	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
5d5b0e7a28ad5d9ca87464bb90086a5af14c8800	Apalache	Set2	NumPlus	True	Passed	Model Under Test Equivalent Model
bfa70f4e4cf690ed1e3916f848c305c20670d5db	Apalache	Set2	NumPlus	False	Passed	Model Under Test Equivalent Model
fbb2429a42e7c5dc7eb774dac9a3cf721d53c2a1	Apalache	Set2	NumMinus	True	Passed	Model Under Test Equivalent Model
9560d180d50fe40ec3b0c8a07296f711b147754e	Apalache	Set2	NumMinus	False	Passed	Model Under Test Equivalent Model
f67614374742574bac20508d489f0339da82d16a	Apalache	Set2	NumMul	True	Passed	Model Under Test Equivalent Model
aab1eda73e7ec04eeb5aa4a19d670d202c1e68f2	Apalache	Set2	NumMul	False	Passed	Model Under Test Equivalent Model
d1e02ca1a81684621627c7f3bde18c888812ea8b	Apalache	Set2	NumDiv	True	Passed	Model Under Test Equivalent Model
207071138e9aa398999b77576cad79e080bf5fa1	Apalache	Set2	NumDiv	False	Passed	Model Under Test Equivalent Model
70505a99daafbedb99c4d4dc6343c6eb65f8d82b	Apalache	Set2	NumMod	True	Passed	Model Under Test Equivalent Model
e4e216f6dee7f1b4adb12e9cb60c839ac967ef7c	Apalache	Set2	NumMod	False	Passed	Model Under Test Equivalent Model
e9a9ea63c54a49d33216f699cd8bb85c425ac19e	Apalache	Set2	NumPow	True	Passed	Model Under Test Equivalent Model
65021d86cc505a3de7a81f38848545d59d401a13	Apalache	Set2	NumPow	False	Passed	Model Under Test Equivalent Model
091c6404135616917e0450296e9803e75b9ac57d	Apalache	Set2	NumGt	True	Passed	Model Under Test Equivalent Model
2f408964cf3ae51b98cd141f46aba214cd19594f	Apalache	Set2	NumGt	False	Passed	Model Under Test Equivalent Model
cecccb33c07f680426f44fb93bcd8726a43a2c5d	Apalache	Set2	NumGe	True	Passed	Model Under Test Equivalent Model
c2f411ddeb3b9e561a2a12c7d13842c37d761775	Apalache	Set2	NumGe	False	Passed	Model Under Test Equivalent Model
579671e26c1e711e2fd12017f4b6b45289c20cb0	Apalache	Set2	NumLt	True	Passed	Model Under Test Equivalent Model
b0344fa00be8fef63fe709200fc8742b0473cbdb	Apalache	Set2	NumLt	False	Passed	Model Under Test Equivalent Model
3ee63be0b2c185b352908f7abe96a716854f1621	Apalache	Set2	NumLe	True	Passed	Model Under Test Equivalent Model
7dc1612d82e36d3f4003fa7944fbaee6bd87658a	Apalache	Set2	NumLe	False	Passed	Model Under Test Equivalent Model
27562ed9b6c4c318425578d52b7f6e77a765a4c4	Apalache	Set2	DefFun	True	Passed	Model Under Test Equivalent Model
6570b3db39156d87685bcce50fb98df19d97b024	Apalache	Set2	DefFun	False	Passed	Model Under Test Equivalent Model
185faeed65c64ac1d872aab93b45a5d62c1328ee	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDefFun	True	Passed	Model Under Test Equivalent Model
8538f647a5444e29ceb8d7280fc1bbd4a1d1e4e7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDefFun	False	Passed	Model Under Test Equivalent Model
55cfe46c56e240a45314442b898669ad6f4c3d13	Apalache	Set2	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
6a6f775358911d81cd64ce4d518cf7f46d8355db	Apalache	Set2	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
3bc0497f76da97fa825f6e6ed00cdf1433bd01d9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
b72770877acac4bdfdbf414d87cf114f2aa2efc8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDefFunRecursive	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
4284dad668f13557a993e36d14e7c0d4ac65926e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef0	True	Passed	Model Under Test Equivalent Model
ba007b696ed1161d9ddffeb373053df9b63de7f2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef0	False	Passed	Model Under Test Equivalent Model
763d88dd9f18955c8e2810025de09a6e96d6ea8f	Apalache	Set2	Def1	True	Passed	Model Under Test Equivalent Model
e3b6703ba1071e04df0e2e8f4b4df477eef09bd2	Apalache	Set2	Def1	False	Passed	Model Under Test Equivalent Model
7bed4d5db4ba24a4063f1bbb38bb2ea8463149a6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef1	True	Passed	Model Under Test Equivalent Model
621e82f887dfca3f83a928c1105a53a4a33f8154	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef1	False	Passed	Model Under Test Equivalent Model
e96926c72504148b336a55bd0b72879b45e7b958	Apalache	Set2	Def2	True	Passed	Model Under Test Equivalent Model
2562f5dfdabc0247d0dde1209ecfeca775be2c82	Apalache	Set2	Def2	False	Passed	Model Under Test Equivalent Model
2aece2a2df029d2e8022572522f474a8f3787bbe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef2	True	Passed	Model Under Test Equivalent Model
d574051a34559c809d2e9344d8b21566a9fb7ad7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef2	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
595733b34f9c440a2e6975b85bee5781b9eeb70a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
99900a26c556054f4168ff727ec01afe8a39fcdf	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Set2	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
9aa67a13fbead96b39d1975b93a60034502136a7	Apalache	Set2	Extends	True	Passed	Model Under Test Equivalent Model
ae4f4e33b43000485db3b2fd01538448d0e5f1c3	Apalache	Set2	Extends	False	Passed	Model Under Test Equivalent Model
d3e1c1f67dd93dfb2ca8236605f7aaf1956edc57	Apalache	Set2	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
ebe1bf22b3a5e1a0a7a02b26fb6a1f56af549797	Apalache	Set2	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
8d9290fefb66826f9ed20e7986810904c37b2657	Apalache	Set2	Variable	True	Passed	Model Under Test Equivalent Model
a11c291b06bb6b8b597a60399d96fc86361fb5f5	Apalache	Set2	Variable	False	Passed	Model Under Test Equivalent Model
35858d9c6257ff800b95abd64492c2eec2abbbbc	Apalache	Set2	Constant	True	Passed	Model Under Test Equivalent Model
d6cc032c0ca0161c9d88943b920baf84dc75a4b6	Apalache	Set2	Constant	False	Passed	Model Under Test Equivalent Model
a8337ea5bbbc303f88a9b13a4a9250ba61b07f42	Apalache	Set2	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
230de7a47aacd7f995662a2341dac17d69f31825	Apalache	Set2	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
aa52804299fa0901d8286ee4d52f297a598c47e7	Apalache	Set2	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f3e1078d502edf6aa52418a550c6080df8f2578e	Apalache	Set2	ConstantRank1	False	Passed	Model Under Test Equivalent Model
7e6f881dc51ef9a26e52990cbee0a4fbd8638175	Apalache	Set2	Instance	True	Passed	Model Under Test Equivalent Model
8a841cd71b6d44a581a21bda996b814b1b0e8abe	Apalache	Set2	Instance	False	Passed	Model Under Test Equivalent Model
c42521330c7e0098f09c6b3694c0158c2994fbde	Apalache	Set2	InstanceWith	True	Passed	Model Under Test Equivalent Model
cec6926a13ad09d84cac0c29328ece2cdd66998f	Apalache	Set2	InstanceWith	False	Passed	Model Under Test Equivalent Model
b4167ab7958052458e3cecfe1b4c674e2848cf67	Apalache	Set2	InstanceNamed	True	Passed	Model Under Test Equivalent Model
8e0173ecec5cea72457085a8e4130352c62a8f9c	Apalache	Set2	InstanceNamed	False	Passed	Model Under Test Equivalent Model
fef76ae84dc336b8aa312a6a8f9d39e435ccdaa5	Apalache	Set2	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
c669b4f3771be9a1364d754733970021d50a613b	Apalache	Set2	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
f4d0c572c229bc8af2edd5c1c4741a4a2d017d17	Apalache	Set2	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
0839231220f9d2f3328a54e9d47ba12fc3f0b862	Apalache	Set2	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
22f936e441d86b9ba0466a01d65023de46d1de61	Apalache	Set2	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
ff3d83591206124570435bd44685880edcad5a54	Apalache	Set2	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
69cf15acd277db2d252c734c54b78aca1223f56a	Apalache	Set2	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
f301d7318174bb1af21e7d39a652700bba59a4c8	Apalache	Set2	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
1866cc8069401f9f6cee854bbad97c490cb1c0cd	Apalache	Set2	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
7843c28d532559c531cb544bf5491b6197d8e202	Apalache	Set2	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
660906175528ff330bd8c72769a9c16cc60280fa	Apalache	Set2	Enabled	True	Passed	Model Under Test Equivalent Model
d2daf911ad42ff9c4c57db9711a22092cdfaae68	Apalache	Set2	Enabled	False	Passed	Model Under Test Equivalent Model
f321686d1da654ca6f349e9a1830623a645db0b8	Apalache	Set2	Cross2	True	Passed	Model Under Test Equivalent Model
22bcf1cc94bac734dd03d55651c43db919922f42	Apalache	Set2	Cross2	False	Passed	Model Under Test Equivalent Model
d8b4003c69c724ad42cc27f5f27964703aac04ad	Apalache	Set2	Cross3	True	Passed	Model Under Test Equivalent Model
e7a3acd4cd89bfecd46b5872faf3b4d9146b40a1	Apalache	Set2	Cross3	False	Passed	Model Under Test Equivalent Model
d652803f884d575228f18d65b8441a391c9dbd9e	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))	Set2	FunSet	True	Passed	Model Under Test Equivalent Model
189635d11c777db0c48f5e012b0212a5386ec5ac	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))	Set2	FunSet	False	Passed	Model Under Test Equivalent Model
000f1e04728cc8b41a44f3c74162b467339b9c60	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)	Set2	RecordSet	True	Passed	Model Under Test Equivalent Model
2ec7dfdfe49e37e80291b90a2c5caf8ef3561373	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)	Set2	RecordSet	False	Passed	Model Under Test Equivalent Model
cda1dd7d55a54877e701690f7b90286b002fe46c	Apalache	Set2	SetDiff	True	Passed	Model Under Test Equivalent Model
0e8f1d840ad7a6133eb0798a5dbb0e8968a72a3f	Apalache	Set2	SetDiff	False	Passed	Model Under Test Equivalent Model
4f8032e8e4a3cb3aecabc603feb44951313dc987	Apalache	Set2	SetUnion	True	Passed	Model Under Test Equivalent Model
cc7f91e14a7b6c366d0f7ce5627c5af9276588dd	Apalache	Set2	SetUnion	False	Passed	Model Under Test Equivalent Model
6bdd483831240eea328fb6525ebb08944e473753	Apalache	Set2	SetIntersect	True	Passed	Model Under Test Equivalent Model
59295e8f4c3f775d3068ece1dc81d4ba6497cda5	Apalache	Set2	SetIntersect	False	Passed	Model Under Test Equivalent Model
a0e9bb7750a9bfc392d95abbc94f5052a2ab023d	Apalache	Set2	SubsetEq	True	Passed	Model Under Test Equivalent Model
ead598d05059d5bab6068558f66c2b7692fa1d67	Apalache	Set2	SubsetEq	False	Passed	Model Under Test Equivalent Model
db0c23931f3c875f037a4520d29576818d4a5070	Apalache	Set2	IfCond	True	Passed	Model Under Test Equivalent Model
afca60299f8938eed123f09613ae8d020c9d245d	Apalache	Set2	IfCond	False	Passed	Model Under Test Equivalent Model
9a0d1c94dcd4a3e99487ed3ca007793c40095fa0	Apalache	Set2	IfThen	True	Passed	Model Under Test Equivalent Model
053ae7c59342028321822a838c4ddacc649a172c	Apalache	Set2	IfThen	False	Passed	Model Under Test Equivalent Model
ae1e6c184a04b0d373a390173982556f1cb66373	Apalache	Set2	IfElse	True	Passed	Model Under Test Equivalent Model
814c8ef95d9df274e9ebe54214a9965a519ac146	Apalache	Set2	IfElse	False	Passed	Model Under Test Equivalent Model
da9589de3d5948945714e59e6e481f6a23a95f1e	Apalache	Set2	Subset	True	Passed	Model Under Test Equivalent Model
4925273512a688985182a4e5f841607df1cf6489	Apalache	Set2	Subset	False	Passed	Model Under Test Equivalent Model
7e64a3fc9c96b3f6863b20ba9ea5faa4c9378d4e	Apalache	Set2	Domain	True	Passed	Model Under Test Equivalent Model
fefc391a8c1618ca551cbcda975d50715e51cd41	Apalache	Set2	Domain	False	Passed	Model Under Test Equivalent Model
62dd8ea4384b1f60277fe5f9ec69ab4303aa8cb7	Apalache	Set2	Union	True	Passed	Model Under Test Equivalent Model
b0af1feafcbf5e3b2120cea961e886dca7a13f3a	Apalache	Set2	Union	False	Passed	Model Under Test Equivalent Model
9a1798308a46d09409656d3afe65eeaf45759638	Apalache	Set2	Unchanged	True	Passed	Model Under Test Equivalent Model
2636bdc05f744665738366b4d01061b3a5f3c56c	Apalache	Set2	Unchanged	False	Passed	Model Under Test Equivalent Model
1b2d3be5e6c37dd8c2644849c6f81b93e2217bf2	Apalache	Set2	Equivalence	True	Passed	Model Under Test Equivalent Model
ea060b7c375b49f92641623bc29e47f60fef3019	Apalache	Set2	Equivalence	False	Passed	Model Under Test Equivalent Model
11fae848cf6c6aa8d7da17610a492cb35fe2b983	Apalache	Set2	StringEmpty	True	Passed	Model Under Test Equivalent Model
b39b02b6a407c1b3ee2ecea1eedf8be0fb12973d	Apalache	Set2	StringEmpty	False	Passed	Model Under Test Equivalent Model
1a8db90ed031ce7b3deef917daeea2fef0ab848e	Apalache	Set2	String	True	Passed	Model Under Test Equivalent Model
7f648feb7af1d793526ab81bb0245bd6c8264c7b	Apalache	Set2	String	False	Passed	Model Under Test Equivalent Model
6ce2802ed1093f0c54cc91d8e9ab345f88f35b8d	Apalache	Set2	SeqLen	True	Passed	Model Under Test Equivalent Model
e1d3ebc588d0cc76601ad0bc0b9acbd9b192ecbf	Apalache	Set2	SeqLen	False	Passed	Model Under Test Equivalent Model
dd89a57df30226c25d1df12d0c102ff5e6dba67d	Apalache	Set2	SeqConcat	True	Passed	Model Under Test Equivalent Model
ac10bf9a2be781eba7e99141fa9bae1aeb049f6a	Apalache	Set2	SeqConcat	False	Passed	Model Under Test Equivalent Model
bd29f794563a4148726da6bb1f7f0f056496f24f	Apalache	Set2	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
340812dcf5e72a8c14bdd3c1cf3a12d104553271	Apalache	Set2	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
ae095567b714baf3be6a20f3286437bf55eeae15	Apalache	Set2	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
3de6bb1d66e5dcf0d932ddeac7f79bd2d219427c	Apalache	Set2	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
d14f348ca87e398b7b72d2b914801c14d97b7701	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	Set2	NumRange	True	Passed	Model Under Test Equivalent Model
95f6740c3e0e85ca9bae3fb8128689a3150dad15	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	Set2	NumRange	False	Passed	Model Under Test Equivalent Model
7e4fe2f3630f5d870c3c1ddb55f9a1380a3c4335	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Set2	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
702ca35b1996dc27818c7c718b159130f0f44ea6	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Set2	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
2eede76c11ace992e7dbcf2b38db7d92ee934e60	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]]	Set2	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
7aeb4f81cda6de6213f0dda96d616d0a4c1298fb	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]]	Set2	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
b97f5648ca688bd4a9dbfd10ade47cee413ea959	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Set2	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
a4b935f1b42c6914e5709549a4a87f1864bd6238	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Set2	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
50b2711f0999abbd071f98bf0258bc48d7421506	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Set2	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
486c4921f11862c627c4aa437d5edc861eced92b	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Set2	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
ceaa8eed41e731d6c2218a0be5c7eda32fb89e28	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Set2	TlcEval	True	Passed	Model Under Test Equivalent Model
731414a6df0dc6d0bda727c24f81507d53e87ac4	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Set2	TlcEval	False	Passed	Model Under Test Equivalent Model
8ba806ccd19599d7a45d00df1ec584c3dbd4319e	Apalache	Set2	BagBagToSet	True	Passed	Model Under Test Equivalent Model
b90177e6a9b68c0e1e33de2685097bf246a58d71	Apalache	Set2	BagBagToSet	False	Passed	Model Under Test Equivalent Model
aa81ff2961505081cfba61e5c8d1ee56876719db	Apalache	Set2	BagSetToBag	True	Passed	Model Under Test Equivalent Model
c64aebebfce3fb9fc3d360edb6fe28f6b8bd2179	Apalache	Set2	BagSetToBag	False	Passed	Model Under Test Equivalent Model
981655d9b5f67db81716ef6cb38ab260ee0f3fcc	Apalache	Set2	BagBagIn	True	Passed	Model Under Test Equivalent Model
57ba2804b8d63f42e3e9ec897e2e393936539363	Apalache	Set2	BagBagIn	False	Passed	Model Under Test Equivalent Model
f3d6c6f3f57ad1f99b792b74934b774f525717be	Apalache	Set2	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
34377d24b8c035c8710262f90d07a15999857230	Apalache	Set2	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
1d1aee41449d508ddd6057fe467e27b1a503b727	Apalache	Set2	BagAddBag	True	Passed	Model Under Test Equivalent Model
2f25031558d677a488f75df75cb6376e35343c88	Apalache	Set2	BagAddBag	False	Passed	Model Under Test Equivalent Model
bf11da463bb437cadbea0497576c20e7c6ed38db	Apalache	Set2	BagBagSub	True	Passed	Model Under Test Equivalent Model
49390e19e232e5742e72ab9b1c1dae93336d23b0	Apalache	Set2	BagBagSub	False	Passed	Model Under Test Equivalent Model
5043f4bf5fc3a13074e6db0ea8d53c712cefb818	Apalache	Set2	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
f6b48973e8c215b2cc665ac9afe961a7c14655dc	Apalache	Set2	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
d21274d685795c958eba5cdef9602aadf3e6da73	Apalache	Set2	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
9a5908e58d9c80243fb699c49dea3410d24015c5	Apalache	Set2	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
ea63dbb269ba21b0ee1dadfdf39f7f01002b4167	Apalache	Set2	BagBagUnion	True	Passed	Model Under Test Equivalent Model
a4f63f8caa338f17c89f6e766e3252df83c39a03	Apalache	Set2	BagBagUnion	False	Passed	Model Under Test Equivalent Model
abbdb2942fc76771f13103e96ffc295cf59a5012	Apalache	Set2	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
8954901a667a886fa710ae0ce2f0091dc965e3a5	Apalache	Set2	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
d913f005eb8a4c7fd7b1bada28a5c489313e82d0	Apalache	Set2	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
bea2949d053a6f684df68242e6ba2a15433279ba	Apalache	Set2	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
3fe5449abc3e51e056c0127dab92c7ca5cadab74	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Set2	BagSubBag	True	Passed	Model Under Test Equivalent Model
e37e75f71a80af30811e9cafa77a4ae2f1262c3d	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Set2	BagSubBag	False	Passed	Model Under Test Equivalent Model
82ab2eb536554b3ef70f118280a2285c77aeee8d	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)	Set2	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
3198c7726636c52cff5556e35681de6b508117b6	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)	Set2	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
1a47dec0cfe0eaa7a376d9e3972bc92d72c96d32	Apalache	Set2	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
ad049fc2619db34c763e08bcc65cfd72fd474ad4	Apalache	Set2	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
87b5e92476659a86c26ffd537a3802bd7a55b6b0	Apalache	Set2	SeqHead	True	Passed	Model Under Test Equivalent Model
ac689ef737af0a51ec72d4f842d00be475383be7	Apalache	Set2	SeqHead	False	Passed	Model Under Test Equivalent Model
d385bd8696cf2f10b334c5fc79fd96b154de902d	Apalache	Set2	SeqTail	True	Passed	Model Under Test Equivalent Model
4485ba7f507901a033abd921e20cb8e2c570387a	Apalache	Set2	SeqTail	False	Passed	Model Under Test Equivalent Model
15e8485859419f9c4099fef4a19b6c07847edb14	Apalache	Set2	SeqAppend	True	Passed	Model Under Test Equivalent Model
7d4b1ba53b793e635fd3091430caef27ca475df8	Apalache	Set2	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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