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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
0aa1de6fc665abc40ad01024e9e760cb7a037d84	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Prime	OneLineComment	True	Passed	Model Under Test Equivalent Model
f9d084fa55da4d4c2452ebf2674e80060b9791d6	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Prime	OneLineComment	False	Passed	Model Under Test Equivalent Model
7de9a2ca0c894782e58814aab11ac475cf694ff5	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Prime	MultiLineComment	True	Passed	Model Under Test Equivalent Model
3c150e03a9b24daedb6009adb772c23ecdc21653	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Prime	MultiLineComment	False	Passed	Model Under Test Equivalent Model
5cd51d8a461fe01b4757c5bea4da5f557f7d69dd	Apalache	Prime	BoolTrue	True	Passed	Model Under Test Equivalent Model
a787514660a16b0a49a28e89b03821fe3df7d05e	Apalache	Prime	BoolTrue	False	Passed	Model Under Test Equivalent Model
3e8d1719329d99212c42e65c339cb41faac80cb4	Apalache	Prime	BoolFalse	True	Passed	Model Under Test Equivalent Model
f9014c53213517944c6e654253c28fc68739ed83	Apalache	Prime	BoolFalse	False	Passed	Model Under Test Equivalent Model
fbb0afedce1f66e31469490c2476c8115dcd853c	Apalache	Prime	BoolSet	True	Passed	Model Under Test Equivalent Model
113457b48f15a472bd3c6b72804bc748fba38cb1	Apalache	Prime	BoolSet	False	Passed	Model Under Test Equivalent Model
c991ad52bae67ecf7024102ac2d7d746d4589c10	Apalache	Prime	And	True	Passed	Model Under Test Equivalent Model
cf9893eb0ea13a1b22ac855ea1f85cc482735a53	Apalache	Prime	And	False	Passed	Model Under Test Equivalent Model
6db1b01792a4dfd8610063d6be18705d31afc4f2	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Prime	AndMultiLine	True	Passed	Model Under Test Equivalent Model
f1f79cb3fb2101e4c6cce8add8a9b939a1da3217	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Prime	AndMultiLine	False	Passed	Model Under Test Equivalent Model
678bc9a800b1be91bd2e5404a2cfd85db4570701	Apalache	Prime	Imply	True	Passed	Model Under Test Equivalent Model
75948ef3d28c63ae3b9a14d8989bed957fd5a428	Apalache	Prime	Imply	False	Passed	Model Under Test Equivalent Model
443ca44ac58fac6bc25f093f7c38e8492fe7c495	Apalache	Prime	Not	True	Passed	Model Under Test Equivalent Model
194f8f56fd4fdfedf7e0b4f4a06bfd32c1ad792d	Apalache	Prime	Not	False	Passed	Model Under Test Equivalent Model
9507de26dc8e0bf188fea1cb7eb6ee7e7eb6bfd4	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Prime	Or	True	Passed	Model Under Test Equivalent Model
5cd58aaf02555a39c1575b8813d25965a13d0d99	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Prime	Or	False	Passed	Model Under Test Equivalent Model
2bfb0a2f22ca5c25452efb2550d17306164ced0c	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Prime	OrMultiLine	True	Passed	Model Under Test Equivalent Model
8f6218b1b52f7816ed9b8c8fb99ab0f3238df6b3	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Prime	OrMultiLine	False	Passed	Model Under Test Equivalent Model
1478e79f54daef4780775ade744c2a652a35663f	Apalache	Prime	Eq	True	Passed	Model Under Test Equivalent Model
922e961910972a55811584bdbcbfaa1fefb84125	Apalache	Prime	Eq	False	Passed	Model Under Test Equivalent Model
cdc91a8b00cef6afa16ad6a004a673fbdef984c3	Apalache	Prime	Ne	True	Passed	Model Under Test Equivalent Model
b3238436806e684ae39a4bc89c203a4e8db1edde	Apalache	Prime	Ne	False	Passed	Model Under Test Equivalent Model
e15d6f9aad481d7076374e1715b0eb963e7616ea	Apalache	Prime	Let	True	Passed	Model Under Test Equivalent Model
543027166735956225ab7db0092cc27956557499	Apalache	Prime	Let	False	Passed	Model Under Test Equivalent Model
c252b95de3cc991676c2c5e300b93993bcadbe44	Apalache	Prime	SetEmpty	True	Passed	Model Under Test Equivalent Model
a5ffae47bab27ff59c0db6e19a458279c1b597a1	Apalache	Prime	SetEmpty	False	Passed	Model Under Test Equivalent Model
d72cf3a5f56c1e34eb60fb377acbf6964fa5d57f	Apalache	Prime	Set0	True	Passed	Model Under Test Equivalent Model
e0ee75982ec63c577a1d5756cd0bf0d248df535b	Apalache	Prime	Set0	False	Passed	Model Under Test Equivalent Model
0271b578fea21d1444e45c6167ee3bcd11f7bcdb	Apalache	Prime	Set1	True	Passed	Model Under Test Equivalent Model
4a5029562ae36f925588716870309754b1795848	Apalache	Prime	Set1	False	Passed	Model Under Test Equivalent Model
85a797f21bcaf5cdaa3b3bbdd48373e5ea50d1a9	Apalache	Prime	Set2	True	Passed	Model Under Test Equivalent Model
45808ab7ca15ddf89da9835f67d9fc08aa4ff27d	Apalache	Prime	Set2	False	Passed	Model Under Test Equivalent Model
7f13979c3f4105d400c4b73f15c4375421d17d7a	Apalache	Prime	Fun	True	Passed	Model Under Test Equivalent Model
b7f19a14a6842d9585a06edcd96deb8248e2291d	Apalache	Prime	Fun	False	Passed	Model Under Test Equivalent Model
484a2d81e558f65312905ada7fb21c5ecc05a7dc	Apalache	Prime	In	True	Passed	Model Under Test Equivalent Model
129665e100479fde152207dae67277269a079c21	Apalache	Prime	In	False	Passed	Model Under Test Equivalent Model
beadff560b2cdacdc72fabe4e8d1a19798340d44	Apalache	Prime	NotIn	True	Passed	Model Under Test Equivalent Model
8b2cf484b18bb1ede9b23c65392cc744e7ae33d1	Apalache	Prime	NotIn	False	Passed	Model Under Test Equivalent Model
4162b3c9b4040a3e9be1ec54bacb8f6773513d29	Apalache	Prime	Exists	True	Passed	Model Under Test Equivalent Model
11dbdebf053d201660054ef9cd1cd87ae8fa43f3	Apalache	Prime	Exists	False	Passed	Model Under Test Equivalent Model
f5f9c0630f45cfc79526bc144ba3f6cc27c6c2b9	Apalache	Prime	Forall	True	Passed	Model Under Test Equivalent Model
b9f69440b39a321126809e136c0ce5308504ceca	Apalache	Prime	Forall	False	Passed	Model Under Test Equivalent Model
97cabd6913b7921979337c1146228a5838d2aa58	Apalache	Prime	Choose	True	Passed	Model Under Test Equivalent Model
100118bd3def1b16de268c8d43c92646224a9a09	Apalache	Prime	Choose	False	Passed	Model Under Test Equivalent Model
72767c20198d59d8b30b9c266a0d25675713566f	Apalache	Prime	Record	True	Passed	Model Under Test Equivalent Model
b8120086fc7a4bf83deda2fc41d9c68f23e26e5f	Apalache	Prime	Record	False	Passed	Model Under Test Equivalent Model
470adf896d06d36dce81e3fe64df806d5e1f0043	Apalache	Prime	Tuple	True	Passed	Model Under Test Equivalent Model
dd88fa92e2b8d9836a504f86db9a01223f959864	Apalache	Prime	Tuple	False	Passed	Model Under Test Equivalent Model
a0efb9330fa37c6b054b34d1fadff967b9f38813	Apalache	Prime	TupleEmpty	True	Passed	Model Under Test Equivalent Model
666d51a01d1e37c3c4fa42b282e6966bd04804ff	Apalache	Prime	TupleEmpty	False	Passed	Model Under Test Equivalent Model
b83c84bf2b6236a7c98fbaa9a3d35376cc2b44d4	Apalache	Prime	FunApp	True	Passed	Model Under Test Equivalent Model
618b1a5b58ac8b0227968f15105080bb21083176	Apalache	Prime	FunApp	False	Passed	Model Under Test Equivalent Model
731f571c9b539d43c3dbae1001d60d093181d08f	Apalache	Prime	NumZero	True	Passed	Model Under Test Equivalent Model
6c5ef3409de0b1f91b1e0cee6c3341e0d2f75ec3	Apalache	Prime	NumZero	False	Passed	Model Under Test Equivalent Model
d3d4a7e20e4d94ec538897173552d217516a3e74	Apalache	Prime	NumOne	True	Passed	Model Under Test Equivalent Model
3919f15e5227b3666960555425b46a75f7661357	Apalache	Prime	NumOne	False	Passed	Model Under Test Equivalent Model
2ec813f8d56a4c49aac152c233d15341889ec5d1	Apalache	Prime	NumMaxInt	True	Passed	Model Under Test Equivalent Model
ee9d10a61e455fbd8d80cdf5fca3c6e985611c6e	Apalache	Prime	NumMaxInt	False	Passed	Model Under Test Equivalent Model
a17f30013d0b8f3a9e83f839448a6c3e0bdfd967	Apalache	Prime	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
0fb97c3f59ccd7870adef6ceeed319293e754dae	Apalache	Prime	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
18399ecbf63d99d1ae692d0d9fee8b4e49cfba02	Apalache	Prime	NumPlus	True	Passed	Model Under Test Equivalent Model
3ee17945cc1c6d4e1a63fdfce36e1ee7878c7405	Apalache	Prime	NumPlus	False	Passed	Model Under Test Equivalent Model
2a05258c1ede9cb6b51ac36d6dcc68e52fd9f7ba	Apalache	Prime	NumMinus	True	Passed	Model Under Test Equivalent Model
fa5ae43a057c017e5c6a2780639780fc21a36f74	Apalache	Prime	NumMinus	False	Passed	Model Under Test Equivalent Model
a373e98e1560e313cc6b60f9cf86329362a9f4f8	Apalache	Prime	NumMul	True	Passed	Model Under Test Equivalent Model
c859555c7bca7c436c26d1f6f69659951dd9be31	Apalache	Prime	NumMul	False	Passed	Model Under Test Equivalent Model
f70c88c397ffa90213d7bae87880ba6fd744cae8	Apalache	Prime	NumDiv	True	Passed	Model Under Test Equivalent Model
cf8ab6fc1911bf6938b0cadffd54c074111b23f2	Apalache	Prime	NumDiv	False	Passed	Model Under Test Equivalent Model
b0ff955af455971075e6ad7f91ea430566ebe373	Apalache	Prime	NumMod	True	Passed	Model Under Test Equivalent Model
085c0a3edb3fe1f33ec4e5006448a800c6ae0467	Apalache	Prime	NumMod	False	Passed	Model Under Test Equivalent Model
ede093653d404fbe4bd7537da7bf3ef85d693355	Apalache	Prime	NumPow	True	Passed	Model Under Test Equivalent Model
2b117f83766757a7c5d694e97fb3d4c9f57f28d0	Apalache	Prime	NumPow	False	Passed	Model Under Test Equivalent Model
a5c42aa01ddb37d8a589415a4a179afecc24d00b	Apalache	Prime	NumGt	True	Passed	Model Under Test Equivalent Model
56b386439073772df393e3b078d07609ff4ccb96	Apalache	Prime	NumGt	False	Passed	Model Under Test Equivalent Model
e3698e3a43aada7755a28cefda0c26eb4badbe03	Apalache	Prime	NumGe	True	Passed	Model Under Test Equivalent Model
3235781fef640776cbda13a42098279d01ced5a2	Apalache	Prime	NumGe	False	Passed	Model Under Test Equivalent Model
11e3e5127ab0d409b1abbe500de4f9a1d7aca0d2	Apalache	Prime	NumLt	True	Passed	Model Under Test Equivalent Model
e7eab39752639c9bc1dc46a69520f5998dce1b3c	Apalache	Prime	NumLt	False	Passed	Model Under Test Equivalent Model
cdb271883f3cadf0be2124ed908845646aec7551	Apalache	Prime	NumLe	True	Passed	Model Under Test Equivalent Model
ef921aa525add1761a264a46adee7d2c1d6e04f8	Apalache	Prime	NumLe	False	Passed	Model Under Test Equivalent Model
0c4a0f969eab4a6cde77707ca3bbfb36cb497a82	Apalache	Prime	DefFun	True	Passed	Model Under Test Equivalent Model
743a3e0724c17be37f5a9b8522a1e1abfd3c1980	Apalache	Prime	DefFun	False	Passed	Model Under Test Equivalent Model
4031f1806527b26a8d072f7709e7d8cc2befd8a9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDefFun	True	Passed	Model Under Test Equivalent Model
085515d1b15ad29ed66a4af5e06ff635e1a1bff0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDefFun	False	Passed	Model Under Test Equivalent Model
65339758a031ec94867a3d3d37d891c6de19433b	Apalache	Prime	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
b5f553b30d1a119a0eda18c59ff35070d8678f35	Apalache	Prime	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
d7bb2c570418f60e3bebc4358ef0188d01bf06d2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
140920e17a60357d9a210a7e383bfb0f3a89eddd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
aad663a28c49a497208f86223a6ed2b9aa1b2086	Apalache	Prime	Def0	True	Passed	Model Under Test Equivalent Model
cc1c39f980f8f5d0e5f489853a4e254871ebfe4a	Apalache	Prime	Def0	False	Passed	Model Under Test Equivalent Model
d18c213cb18ab9bfbe4bb6f8a512a7686e085e32	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef0	True	Passed	Model Under Test Equivalent Model
6da1169f1d44ff305bdfb40f916cfde3988ddbd9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef0	False	Passed	Model Under Test Equivalent Model
a6806906ac35b3c22d9b344df02aaa203069a560	Apalache	Prime	Def1	True	Passed	Model Under Test Equivalent Model
eca1245946d3ef807b68fc5428739a25aec5d170	Apalache	Prime	Def1	False	Passed	Model Under Test Equivalent Model
5e162855345db9dc87842fbf70c6f89604513b3b	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef1	True	Passed	Model Under Test Equivalent Model
bd2efdfdb94a9239d81eab833b02df9cfab5e5b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef1	False	Passed	Model Under Test Equivalent Model
8e41d91557dd22de764761ac00b124cca83eb93a	Apalache	Prime	Def2	True	Passed	Model Under Test Equivalent Model
628a25f71006e8201ea85990c6ab391e66b78b47	Apalache	Prime	Def2	False	Passed	Model Under Test Equivalent Model
7ab3e0875d14fc6a5480f7712bc449fa9d08498f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef2	True	Passed	Model Under Test Equivalent Model
533e007df4e2e5b65e900f0175c83276e9addaa8	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef2	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
991971e85931e9ff5612caeb2a07577c71c327ad	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
0f6de1c011983af2d3169a837d08d8a81f00ebd0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Prime	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
df8b27c5016687db20ad07bec36da9ed75234493	Apalache	Prime	Extends	True	Passed	Model Under Test Equivalent Model
efb17692fa65794e17987c0948660aafcd9049f9	Apalache	Prime	Extends	False	Passed	Model Under Test Equivalent Model
6763f6cc045f879ea2c2985b16512e9e7603972b	Apalache	Prime	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
fc6e78629143ea9f39ae71edcdc18eefe88cc0ae	Apalache	Prime	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
56b01d6b1e6cc8b22d8d87f3812815c6c6f274f5	Apalache	Prime	Variable	True	Passed	Model Under Test Equivalent Model
383390720ff861a4d59712842528d6bb14c34766	Apalache	Prime	Variable	False	Passed	Model Under Test Equivalent Model
8a8f5b84b44ea914355b7ddf6e07beeb6ab93172	Apalache	Prime	Constant	True	Passed	Model Under Test Equivalent Model
c94dfb79fc4affcb4e3ea84cb02ec6abefa10f95	Apalache	Prime	Constant	False	Passed	Model Under Test Equivalent Model
44b68a33c8efe4dd44e72eaa8597f75aef6bc61a	Apalache	Prime	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
a1ee2055ae77c21e0a34246173a9f1ff040de41c	Apalache	Prime	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
e7b805ee68422172316e9f876708443ae0b0d23d	Apalache	Prime	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e17576b8f0ab16c7d87041e1e037360449d06326	Apalache	Prime	ConstantRank1	False	Passed	Model Under Test Equivalent Model
6d09a2920b94a2596442de117218e88f15f473ad	Apalache	Prime	Instance	True	Passed	Model Under Test Equivalent Model
c53e6bd0469a7e75c9e0eb1aebb9d8a538a01178	Apalache	Prime	Instance	False	Passed	Model Under Test Equivalent Model
79643192b9c608fd2159a72ddd103d15b58b2c31	Apalache	Prime	InstanceWith	True	Passed	Model Under Test Equivalent Model
3ba7e14b6d5f4b97d4a1d4ff5bc9a7e086be8f55	Apalache	Prime	InstanceWith	False	Passed	Model Under Test Equivalent Model
94aca8a8ebbe6e4f5e62925ecd54a1ece898610b	Apalache	Prime	InstanceNamed	True	Passed	Model Under Test Equivalent Model
677a6de6f94b22556892a560728120e20fc886e8	Apalache	Prime	InstanceNamed	False	Passed	Model Under Test Equivalent Model
65e5984f19f42dff6226280be5ff6f83ea9657bf	Apalache	Prime	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
1f81389fe5a13287045d6047a973f05c15773517	Apalache	Prime	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
a5b4f36c3cd62967746f7081496dc14b0fe19164	Apalache	Prime	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
4e2e76f2e097eb31fde07c1ea5458f831be366f1	Apalache	Prime	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
4f37a665fb71b6842c18a59fc05d418af06c1fc2	Apalache	Prime	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
ef6d3baa65322e5d633caa22cf3f6268c57f4ce3	Apalache	Prime	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
a75584e4d07b70511f85ff1669f771e7a47ad99b	Apalache	Prime	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
18162e5d05606836ecc1e493185e7932f2396ca8	Apalache	Prime	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
b8edbe607797bda53f421d97b5a8145bb32ef006	Apalache	Prime	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
2bba8a5f6c3ab487b66269605d2c7ae3c89725bc	Apalache	Prime	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
c3861b249cbb9b62e9e98f1c1d23ad400ae8975f	Apalache	Prime	Enabled	True	Passed	Model Under Test Equivalent Model
ea1e49fc0b3f8cd4e414650c4923d1abd3acf333	Apalache	Prime	Enabled	False	Passed	Model Under Test Equivalent Model
74784d2d653c2eb03695c207ff8cef195702905a	Apalache	Prime	Cross2	True	Passed	Model Under Test Equivalent Model
0a796f7d961cd3175781a3819308acf6861d2a66	Apalache	Prime	Cross2	False	Passed	Model Under Test Equivalent Model
0652909d2f5650d9d14c917aea8e59139f6a344a	Apalache	Prime	Cross3	True	Passed	Model Under Test Equivalent Model
7f28f70aa1b72fab8927e3facd8a96f74f5f9bd0	Apalache	Prime	Cross3	False	Passed	Model Under Test Equivalent Model
d321d693e8a02545466580c8003e113567f1e8af	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))	Prime	FunSet	True	Passed	Model Under Test Equivalent Model
a2554a7783bef89b762f92d807355315e0276c3a	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))	Prime	FunSet	False	Passed	Model Under Test Equivalent Model
ea1a921abcd473d325a49a591c816cafda38a763	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)	Prime	RecordSet	True	Passed	Model Under Test Equivalent Model
31e0b585c4c8676d864241e10da5808879f24c42	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)	Prime	RecordSet	False	Passed	Model Under Test Equivalent Model
cd526195a276765842ed20d8c2cfd138e3dcbf37	Apalache	Prime	SetDiff	True	Passed	Model Under Test Equivalent Model
905fa37922e5509cb529e39234c0fa91489251a0	Apalache	Prime	SetDiff	False	Passed	Model Under Test Equivalent Model
5d16ffcd250148517046e88a99d5a35d308239b4	Apalache	Prime	SetUnion	True	Passed	Model Under Test Equivalent Model
4f29d36647086820f816ff16424076ebc824a3a7	Apalache	Prime	SetUnion	False	Passed	Model Under Test Equivalent Model
7fe00311e52d25da166407ba7c4ea7182ea543a8	Apalache	Prime	SetIntersect	True	Passed	Model Under Test Equivalent Model
926baf20ffea86a8794de89ff61279843968eccb	Apalache	Prime	SetIntersect	False	Passed	Model Under Test Equivalent Model
05fe350874feca2135c971d0502e010daa8f085d	Apalache	Prime	SubsetEq	True	Passed	Model Under Test Equivalent Model
ad3d502fb7e0c6527054b9078f4e4746ba079243	Apalache	Prime	SubsetEq	False	Passed	Model Under Test Equivalent Model
e8cf05025f3733d1e5e1ad96bc1052d4afdf291e	Apalache	Prime	IfCond	True	Passed	Model Under Test Equivalent Model
2ae4f5224de8fc2b71971554613c65044c8b141d	Apalache	Prime	IfCond	False	Passed	Model Under Test Equivalent Model
80411eb5a14807cb14ed33e0ba8b4491d0c19fc1	Apalache	Prime	IfThen	True	Passed	Model Under Test Equivalent Model
cecee3fd3bee9d7932738b5ea96abad38258811b	Apalache	Prime	IfThen	False	Passed	Model Under Test Equivalent Model
f8e31894923564781eac7cff215f29c48be324de	Apalache	Prime	IfElse	True	Passed	Model Under Test Equivalent Model
f26d65bd5d93fc0ed12b6c408364a0f339e06e3f	Apalache	Prime	IfElse	False	Passed	Model Under Test Equivalent Model
295072cd68dc892752447e42d0a4b0aa5d2dcb45	Apalache	Prime	Subset	True	Passed	Model Under Test Equivalent Model
be8489df6f163c090b00fa5d3ece7ac7afa77b23	Apalache	Prime	Subset	False	Passed	Model Under Test Equivalent Model
ff92bcb8e34b9d497c89f13df8cea226cbd3e108	Apalache	Prime	Domain	True	Passed	Model Under Test Equivalent Model
bacc76631983d7b97114d266237dc3b4de3fd6c5	Apalache	Prime	Domain	False	Passed	Model Under Test Equivalent Model
26fc51299992a301c1d0ca12df049d8aea30b3f6	Apalache	Prime	Union	True	Passed	Model Under Test Equivalent Model
c234425d52538134f302fb04ea3dca59f6a897db	Apalache	Prime	Union	False	Passed	Model Under Test Equivalent Model
765d528889dbc769940095fa1e786fb97e8df016	Apalache	Prime	Equivalence	True	Passed	Model Under Test Equivalent Model
be47085c344587f4cfc27cf8eed9ef8316ea1470	Apalache	Prime	Equivalence	False	Passed	Model Under Test Equivalent Model
440d037664ae9b3f2fa71e2f259a0ad95ea295fd	Apalache	Prime	StringEmpty	True	Passed	Model Under Test Equivalent Model
192bb1c1074f321c9269fcf7019204e96ef66b4c	Apalache	Prime	StringEmpty	False	Passed	Model Under Test Equivalent Model
6c2a45ce8c94cd587b1266e50f00bb3fd18a9106	Apalache	Prime	String	True	Passed	Model Under Test Equivalent Model
9e75883aad5ea0aad7b726d3c7ac168bae752fec	Apalache	Prime	String	False	Passed	Model Under Test Equivalent Model
2b08740dace24b6c3201ab4b75852eb314c15c4c	Apalache	Prime	SeqLen	True	Passed	Model Under Test Equivalent Model
e9cfbaa5bbaa645f759a7c3c30d1e560362b317a	Apalache	Prime	SeqLen	False	Passed	Model Under Test Equivalent Model
137498003d58135d791702ef9b9d3c6747b14b3d	Apalache	Prime	SeqConcat	True	Passed	Model Under Test Equivalent Model
5031dcb80133cc37049aebae2d8650eb559d28e8	Apalache	Prime	SeqConcat	False	Passed	Model Under Test Equivalent Model
148dbf857b187bb18dd094bf84ec9498434d81bf	Apalache	Prime	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
abf2bef8af699d2bb28c87439a15e216cea05040	Apalache	Prime	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
5d9b267b69c1a68994be6369f865739138905b17	Apalache	Prime	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
b21a3a1e3a1b047759c129370191ad755020ad33	Apalache	Prime	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
838302380b02c41f9d3ac4839c852d846e25752d	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	Prime	NumRange	True	Passed	Model Under Test Equivalent Model
d42c995cfae3811eac4c24c9653121027b5e5f32	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	Prime	NumRange	False	Passed	Model Under Test Equivalent Model
e17f4dc17de9e6c322eef6904149dd98a8036b13	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Prime	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
242b89ce03f0045f1cdce7b3b0732a68243e58c2	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Prime	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
890cf5f3e02d9ce49075d68736339e6254123687	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]]	Prime	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
54bc5776674f76f25b338c274332ecea54fe5ba6	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]]	Prime	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
2401e7389ab807839a2435c6eb4d9f4fa29c84bb	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Prime	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
9ba28b6c225379e2536068f3730dc66bdf039d41	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	Prime	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
e047af7f5770a71a3ad81b21c32b13354047241d	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Prime	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
6aa802ccb1a16316c5a6298b0d118bc03fbec94a	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Prime	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
9a0651d34f48909b43e686c7144caa6aef627ef3	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Prime	TlcEval	True	Passed	Model Under Test Equivalent Model
a071bceef9e4d7cf224491fe977253258d145261	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Prime	TlcEval	False	Passed	Model Under Test Equivalent Model
531b9731d85561ef27506581561a1aad50b4b01a	Apalache	Prime	BagBagToSet	True	Passed	Model Under Test Equivalent Model
bda7e58e5c3353897de70cd914ed60ea02f9124d	Apalache	Prime	BagBagToSet	False	Passed	Model Under Test Equivalent Model
234933abc89717fdc4a3265b21a56f9ab87b5676	Apalache	Prime	BagSetToBag	True	Passed	Model Under Test Equivalent Model
695605b7453042df4074d81d4c9cb7f871171bb3	Apalache	Prime	BagSetToBag	False	Passed	Model Under Test Equivalent Model
1ba3caa76c8693c0f595a246ffb3202b15e0bd87	Apalache	Prime	BagBagIn	True	Passed	Model Under Test Equivalent Model
19e346b644738f3891bbae4eadb1fbd02e83430f	Apalache	Prime	BagBagIn	False	Passed	Model Under Test Equivalent Model
0ce2fd4ff297b83d0fe848bfba22368ff24b4e20	Apalache	Prime	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
e5017729032eaf5ee543b2960e9228aed29216a5	Apalache	Prime	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
5b0759a2d8e250dba3b063411c1d205d17ac40d3	Apalache	Prime	BagAddBag	True	Passed	Model Under Test Equivalent Model
0e3ff9b055b0c58d4bf595cea45ae6739e3ae0d9	Apalache	Prime	BagAddBag	False	Passed	Model Under Test Equivalent Model
924ee53862a58f0165f39bd63e310e6059498cbf	Apalache	Prime	BagBagSub	True	Passed	Model Under Test Equivalent Model
860de1f57c1b30be7d6f6dec855c5e72a409496b	Apalache	Prime	BagBagSub	False	Passed	Model Under Test Equivalent Model
bcb753006be14353a16802995ab98c94da602821	Apalache	Prime	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
44718cbd4de81f59ed0f967a1b22aec35467eecf	Apalache	Prime	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
6956cca1ab274e1c2d67e327af3c8b8270ff9c98	Apalache	Prime	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
b621278ee0d06f14a0192feef84acb24e5c26a41	Apalache	Prime	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
fa27784bf29e51c5f452444a52c2051381c05c2d	Apalache	Prime	BagBagUnion	True	Passed	Model Under Test Equivalent Model
6c5ddb645eea96da673e338f1e2a303c7124b5ca	Apalache	Prime	BagBagUnion	False	Passed	Model Under Test Equivalent Model
11a447bea9b8df48ab88fdc1d16418f23837425c	Apalache	Prime	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
5a1a8e03ff1988731354026af5dbef5fbdb6c5f9	Apalache	Prime	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
8c2862a39a21eabc5e5f1a29c0f12804deb62bb4	Apalache	Prime	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
b4f56eac009657c5cbd92f5735dc6d29623a4cab	Apalache	Prime	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
3b92d8d3ced0179ea0ef9cbfe883bee9a8184cf0	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Prime	BagSubBag	True	Passed	Model Under Test Equivalent Model
3984d106717ac52fc55365e6fa3b26484d476c61	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	Prime	BagSubBag	False	Passed	Model Under Test Equivalent Model
4616915118fd1a697884a006f96b6e337d1b2c61	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)	Prime	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
7fdcae9fd61ac3f48b3cee4d708ee5a7475151ca	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)	Prime	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
49d730a27099ae0cf633840fb15a4da6524bfe6e	Apalache	Prime	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
8d0115b04c26c4430474f3fdfcca41aed10b8752	Apalache	Prime	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
d372d9a1853c9992c01aef357e08de1cac1a9042	Apalache	Prime	SeqHead	True	Passed	Model Under Test Equivalent Model
10c886dad81873dceb328a8aeffbde7ab5d5f2ce	Apalache	Prime	SeqHead	False	Passed	Model Under Test Equivalent Model
945374b63a22a23bb3d2828dc18412c18812fc24	Apalache	Prime	SeqTail	True	Passed	Model Under Test Equivalent Model
6df8e0b32ce5e53d4028c496541763d9c8917fac	Apalache	Prime	SeqTail	False	Passed	Model Under Test Equivalent Model
966515da4a58ae8648d7dd06a8c755a8de991731	Apalache	Prime	SeqAppend	True	Passed	Model Under Test Equivalent Model
9b80fae17bbe9e9713c92bc5f43bc3158dd50402	Apalache	Prime	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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