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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
b8fd3a9394214400d2e581905731de88264a501c	Apalache	And	Prime	True	Passed	Model Under Test Equivalent Model
15682286b5323d157b3fb35656e604c40c39abda	Apalache	And	Prime	False	Passed	Model Under Test Equivalent Model
a57e7fe5d0db9460f264941881bd3a570d39a5ed	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Prime	True	Passed	Model Under Test Equivalent Model
60d4299d5907a548a2a4b2f0185de9792c9fe3fd	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Prime	False	Passed	Model Under Test Equivalent Model
5c201d5768c4ae3cdcec1c8a9fe9f8a53a2af70d	Apalache	Imply	Prime	True	Passed	Model Under Test Equivalent Model
0caa844e21455bb9a1aa1b63a48dc6b55a822ee4	Apalache	Imply	Prime	False	Passed	Model Under Test Equivalent Model
3dfed61c451f9c4ed1b62cc7ddcfec7d83fa62f1	Apalache	Not	Prime	True	Passed	Model Under Test Equivalent Model
8dbcebc70d0963cb6ad56aebeb49dff454fa12ac	Apalache	Not	Prime	False	Passed	Model Under Test Equivalent Model
a1ed3bd37f329de61ecdc2bde84a143c79a074ba	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Prime	True	Passed	Model Under Test Equivalent Model
5b6eeb69c0b2c293230082e9dd54ebac6a2e3637	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Prime	False	Passed	Model Under Test Equivalent Model
ca25533eeb4b38baa53643ac8668a0c87eebd509	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Prime	True	Passed	Model Under Test Equivalent Model
bec6bb483bbe3c2a535d67e5b94d64d384303240	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Prime	False	Passed	Model Under Test Equivalent Model
ad42606209e55850cf2b9a2aa99ccd818f109dba	Apalache	Boxed	Prime	True	Passed	Model Under Test Equivalent Model
4ce214492980ee32823fee5af6a49349cb527302	Apalache	Boxed	Prime	False	Passed	Model Under Test Equivalent Model
63600974cbb5cd4e06289882572808f550a2690a	Apalache	Eq	Prime	True	Passed	Model Under Test Equivalent Model
91af409318633e11c1baa55490cb79005226ffa6	Apalache	Eq	Prime	False	Passed	Model Under Test Equivalent Model
129f150b3232c70b700710f8a12f4aa64d0bfcb6	Apalache	Ne	Prime	True	Passed	Model Under Test Equivalent Model
e785733c086bc4c483c8a13ca948ae52884f7a90	Apalache	Ne	Prime	False	Passed	Model Under Test Equivalent Model
fecb1c8c5bbfcf5e455f8bd2941bf294787427bd	Apalache	Let	Prime	True	Passed	Model Under Test Equivalent Model
f4d648a5920cd0e3cec194dced5ccb1bba3d9e85	Apalache	Let	Prime	False	Passed	Model Under Test Equivalent Model
744d62474fa1aea30d06e0571f94efd9451b7158	Apalache	Set0	Prime	True	Passed	Model Under Test Equivalent Model
484602886fdab596252b41868959306da6e4ca4f	Apalache	Set0	Prime	False	Passed	Model Under Test Equivalent Model
5a09d0b44db5d286b677ae5bba9a7def5d743f4b	Apalache	Set1	Prime	True	Passed	Model Under Test Equivalent Model
b2efff8c391c6679f4d86c2febabd7802e1ff000	Apalache	Set1	Prime	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
1f5614d98017ee26a118bc0a5141b214e2d626e8	Apalache	Fun	Prime	True	Passed	Model Under Test Equivalent Model
2d4a67aed76df0da169abeaeca9cff5213373106	Apalache	Fun	Prime	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
8b972ee0299d28fd90aea57e3ea256cc76e6e5e0	Apalache	NotIn	Prime	True	Passed	Model Under Test Equivalent Model
e5c620977e04152fed7ca0b13860483b3a065098	Apalache	NotIn	Prime	False	Passed	Model Under Test Equivalent Model
253234aab29f13790e177e8572cb9593093c253d	Apalache	Exists	Prime	True	Passed	Model Under Test Equivalent Model
7fbdcd7abf96ffb5ae7fb46f96aa25a958b9296e	Apalache	Exists	Prime	False	Passed	Model Under Test Equivalent Model
f67ce6be250fee94102b71540e92987991fe8e1a	Apalache	Forall	Prime	True	Passed	Model Under Test Equivalent Model
e2bd8f315a52ebe8bd03ab860e99cd18c3234770	Apalache	Forall	Prime	False	Passed	Model Under Test Equivalent Model
b9f3d8e711282828d92e27c533085dae5d539420	Apalache	Choose	Prime	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
b97daa0d0f86ec9dcc7a7729ac2289f9802425f7	Apalache	Choose	Prime	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
4913276bf159fafc2ba6936db5fd30d1f2044cc8	Apalache	Record	Prime	True	Passed	Model Under Test Equivalent Model
4443ebba1b0d803978c4ed227521016168ed0b51	Apalache	Record	Prime	False	Passed	Model Under Test Equivalent Model
ffa5ab3dc9caa70a581b7893f64c5cf958243ba4	Apalache	Tuple	Prime	True	Passed	Model Under Test Equivalent Model
6cd42de79928deaf5ba9d67c2d8840029e9d33db	Apalache	Tuple	Prime	False	Passed	Model Under Test Equivalent Model
cb00cc7a3e02a8b28b27c68815f069c687843cd5	Apalache	FunApp	Prime	True	Passed	Model Under Test Equivalent Model
b13d460e80061c3558dbdd2248960255a04cb6e4	Apalache	FunApp	Prime	False	Passed	Model Under Test Equivalent Model
1f3461ba36d17c925343c566828f1eb2ca63d961	Apalache	Except0	Prime	True	Passed	Model Under Test Equivalent Model
54785af79d1e84b281bd23dc876d1c01f0bf09c8	Apalache	Except0	Prime	False	Passed	Model Under Test Equivalent Model
31e956943743cbfae444713338580e09050a87ff	Apalache	Except1Fun	Prime	True	Passed	Model Under Test Equivalent Model
361b4726c24116a2a545d4e81a3b9f78872a4b54	Apalache	Except1Fun	Prime	False	Passed	Model Under Test Equivalent Model
9a436690019f39514b485a5555f61ee62f788afe	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Prime	True	Passed	Model Under Test Equivalent Model
12484122bc1f6c40a30ce14efeb9f3941c662b19	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Prime	False	Passed	Model Under Test Equivalent Model
64143ff95512cae9349337eb6c3de45f40506fa7	Apalache	Except1Rec	Prime	True	Passed	Model Under Test Equivalent Model
a9857992f3475995821b8defc7b17d9dc259189b	Apalache	Except1Rec	Prime	False	Passed	Model Under Test Equivalent Model
2d97199f40c32dc8625deccd991974c51257d2b4	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Prime	True	Passed	Model Under Test Equivalent Model
71687290f4887808e1d7fe220f3480808381f0d8	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Prime	False	Passed	Model Under Test Equivalent Model
0b5baef17c1c54d6fdd454a0ef765664d714699b	Apalache	Except2Fun	Prime	True	Passed	Model Under Test Equivalent Model
2a486c2ba07b019026d0bcc24e1a870dab617dfd	Apalache	Except2Fun	Prime	False	Passed	Model Under Test Equivalent Model
5b4a3e9f4385b775b98b660c7a4564784ea2baa3	Apalache	Except2FunTuple	Prime	True	Passed	Model Under Test Equivalent Model
159faca663b41530ed092f7c4a390ad9ec9ece79	Apalache	Except2FunTuple	Prime	False	Passed	Model Under Test Equivalent Model
c17b9c6bfefa25acf7bc7bf8880dd288afe08382	Apalache	NumUnaryMinus	Prime	True	Passed	Model Under Test Equivalent Model
0faa8dcd4017aff22a6f7331fb6814950c30415d	Apalache	NumUnaryMinus	Prime	False	Passed	Model Under Test Equivalent Model
5ca54822877656eff9de7db57abf723acf5d06f6	Apalache	NumPlus	Prime	True	Passed	Model Under Test Equivalent Model
c978dffc72af8a04fc58b67b22092a2516c3665c	Apalache	NumPlus	Prime	False	Passed	Model Under Test Equivalent Model
53b734034c5fdd4f14c64fbc1768f4f4d017bd3c	Apalache	NumMinus	Prime	True	Passed	Model Under Test Equivalent Model
5fa6b10e6576167615bdf53640ee272347aecfe1	Apalache	NumMinus	Prime	False	Passed	Model Under Test Equivalent Model
c6ac31d0ced4a5450f7ffe390072b95da074fc50	Apalache	NumMul	Prime	True	Passed	Model Under Test Equivalent Model
c4722c6df71e2e8a62d38f7414ee16b66446e36f	Apalache	NumMul	Prime	False	Passed	Model Under Test Equivalent Model
63e56b3fbd052171060bc65bd37726c1bc51a6d2	Apalache	NumDiv	Prime	True	Passed	Model Under Test Equivalent Model
dd050389ac69c22f1479c579f958dc9f6a98390a	Apalache	NumDiv	Prime	False	Passed	Model Under Test Equivalent Model
e1dd69e7cf0b5aa59f636689484a74abc3c5a34e	Apalache	NumMod	Prime	True	Passed	Model Under Test Equivalent Model
77de0618573cf4eb83198fd6f0fe7e3b9a9bedca	Apalache	NumMod	Prime	False	Passed	Model Under Test Equivalent Model
c5cb3999eb2f612f0f1c3024b1aa7dcb35277956	Apalache	NumPow	Prime	True	Passed	Model Under Test Equivalent Model
d7cadd6e078375690e39500d5c2884a2dba6c84c	Apalache	NumPow	Prime	False	Passed	Model Under Test Equivalent Model
214e9c2fb5e24a15f26cd58eecb846a104bf1076	Apalache	NumGt	Prime	True	Passed	Model Under Test Equivalent Model
10eb9dc463c3cfceecc254af4da2248d37f5b96c	Apalache	NumGt	Prime	False	Passed	Model Under Test Equivalent Model
08b87dccd5be19df515a0a3d59d57359e90f3d1f	Apalache	NumGe	Prime	True	Passed	Model Under Test Equivalent Model
0d65b8aa705e7a301829f9519c79a2317a71947d	Apalache	NumGe	Prime	False	Passed	Model Under Test Equivalent Model
c03e7ec7b5f3b7a775e688a4041ac17ca6bbf7b8	Apalache	NumLt	Prime	True	Passed	Model Under Test Equivalent Model
53357f89202d6a10c977d590020b970e13ef1510	Apalache	NumLt	Prime	False	Passed	Model Under Test Equivalent Model
ba7330926280feac79eeba289c3f956a504bc674	Apalache	NumLe	Prime	True	Passed	Model Under Test Equivalent Model
219b2179fa14318750968039ba136ba81e881b64	Apalache	NumLe	Prime	False	Passed	Model Under Test Equivalent Model
6a29a041aa0a3b80a672ddb24b9958a3d1fa17ba	Apalache	DefFun	Prime	True	Passed	Model Under Test Equivalent Model
f15058c86ea98faa2ef00f4e3d1dbe8c104008de	Apalache	DefFun	Prime	False	Passed	Model Under Test Equivalent Model
5a7bf6e4f3bce3084b9df7e2f94988e869ebd5cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Prime	True	Passed	Model Under Test Equivalent Model
461592241f4e3d4d712c4a75626c6a45da3e6924	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Prime	False	Passed	Model Under Test Equivalent Model
02d4d784289402a891e96f252ff6369bab6b9574	Apalache	DefFunRecursive	Prime	True	Passed	Model Under Test Equivalent Model
133ec67e7467a31b767850c0290471c1dc3d3ab3	Apalache	DefFunRecursive	Prime	False	Passed	Model Under Test Equivalent Model
dd06a1f777fec3fff02cf257a154ca72f2b33002	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Prime	True	Passed	Model Under Test Equivalent Model
9203b5ffb93499d6bcf5e80f4b184133986f2d79	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Prime	False	Passed	Model Under Test Equivalent Model
2d23269c32be7d8c37783e53cb2f770dda845bef	Apalache	Def0	Prime	True	Passed	Model Under Test Equivalent Model
1e80c491abbe788a3516db08574ff77783e561d2	Apalache	Def0	Prime	False	Passed	Model Under Test Equivalent Model
184c335f538091b8680465d20fe199e30b2300ac	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Prime	True	Passed	Model Under Test Equivalent Model
2d8e09c9dbfc82db275096b6f123cbf3ce4f759d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Prime	False	Passed	Model Under Test Equivalent Model
ca6b95fc307ed909030494d452081ad2f2697b24	Apalache	Def1	Prime	True	Passed	Model Under Test Equivalent Model
bdf315726129a0a178264a4aeb030a6079435947	Apalache	Def1	Prime	False	Passed	Model Under Test Equivalent Model
f7132d280c46e3db8eb9dcff91504d17354eb8f1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Prime	True	Passed	Model Under Test Equivalent Model
e8142ff980648af20d971858a870279713a15a4c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Prime	False	Passed	Model Under Test Equivalent Model
c4ad70bd08f3224499d444cd370e9fee04c61d1c	Apalache	Def2	Prime	True	Passed	Model Under Test Equivalent Model
913bb88e0dabc5801f4d27c54856c82b52180004	Apalache	Def2	Prime	False	Passed	Model Under Test Equivalent Model
c068418e1ae21b7734a9034a9539c55e42f7390b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Prime	True	Passed	Model Under Test Equivalent Model
fb1c6729357902ddb257b1ac04fed419f974b281	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Prime	False	Passed	Model Under Test Equivalent Model
ce7d8a2eeb506a85fd5e5cf024569fd41bff85f7	Apalache	Def1Recursive	Prime	True	Passed	Model Under Test Equivalent Model
633c99ecd42f38e58a7dec16d47b96ab75110cc1	Apalache	Def1Recursive	Prime	False	Passed	Model Under Test Equivalent Model
995b80b0c0e44397fc5237a5f3a119262e5f2217	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Prime	True	Passed	Model Under Test Equivalent Model
e3c582dfc01f60a19fa710b1ec871eb60125ea44	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Prime	False	Passed	Model Under Test Equivalent Model
7efd268c753744c702e379df0b3c767008a70a38	Apalache	Extends	Prime	True	Passed	Model Under Test Equivalent Model
34fe9e0017efe7813239a698b2b006f500da800e	Apalache	Extends	Prime	False	Passed	Model Under Test Equivalent Model
2bafe1e31d63680a5f8e38bedc8bcfe66959092e	Apalache	ExtendsInDifferentFolder	Prime	True	Passed	Model Under Test Equivalent Model
2cc695f10165951f7f0cc5a058461ec9802840fe	Apalache	ExtendsInDifferentFolder	Prime	False	Passed	Model Under Test Equivalent Model
5a2f5137de28cd777694c8be8b02b4586c1ebccc	Apalache	Variable	Prime	True	Passed	Model Under Test Equivalent Model
07510a1cdb125aa4d52ed5152df7c7c7812fb35c	Apalache	Variable	Prime	False	Passed	Model Under Test Equivalent Model
bed5e89d4d971f29ed469ed06faed79ef3187975	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Prime	True	Passed	Model Under Test Equivalent Model
13ccb77b855d4527b0801041f0fe5f06a57222e2	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Prime	False	Passed	Model Under Test Equivalent Model
a1d9a610999004e017744cedf1c9988c024d6dc7	Apalache	Instance	Prime	True	Passed	Model Under Test Equivalent Model
9a0b3ce8f6b4e5ef0e1ef3f46d6a2009d74515b1	Apalache	Instance	Prime	False	Passed	Model Under Test Equivalent Model
710a4ae21b9704cc24ff1ce8c200eb9388b3e2e4	Apalache	InstanceWith	Prime	True	Passed	Model Under Test Equivalent Model
9f40f6e88e31470d72e066b74ad773949a1d29c6	Apalache	InstanceWith	Prime	False	Passed	Model Under Test Equivalent Model
2642cdecba01c6a37595287bd68b2d405555f712	Apalache	InstanceNamed	Prime	True	Passed	Model Under Test Equivalent Model
bb65238c9253914800bcd46596ca9a73677db591	Apalache	InstanceNamed	Prime	False	Passed	Model Under Test Equivalent Model
f7ff1f8e21396f7a0f2074d94ca24df9d3600d81	Apalache	InstanceNamedWith	Prime	True	Passed	Model Under Test Equivalent Model
86f5bba37a03621c89697c871cc7b6bece598405	Apalache	InstanceNamedWith	Prime	False	Passed	Model Under Test Equivalent Model
ffac7bec91bdb29c27c89ebea4007a885951c63a	Apalache	InstanceInFolder	Prime	True	Passed	Model Under Test Equivalent Model
ccec58ec6ff2b6943011327dae8fb5cbb4515912	Apalache	InstanceInFolder	Prime	False	Passed	Model Under Test Equivalent Model
8ac5c67e0cdc3b45c0f0985ac38e0b45ff4d18b6	Apalache	InstanceWithInFolder	Prime	True	Passed	Model Under Test Equivalent Model
118a8474bc18f05251cac016df2552be3f50e4c3	Apalache	InstanceWithInFolder	Prime	False	Passed	Model Under Test Equivalent Model
0bd016754e4dc36ac4cf92139049734777e8dfc2	Apalache	InstanceNamedInFolder	Prime	True	Passed	Model Under Test Equivalent Model
0f162b80637bdbefc0d52e2d63ec7e276462059f	Apalache	InstanceNamedInFolder	Prime	False	Passed	Model Under Test Equivalent Model
13b71f5c7948c6de6ab1f42bd85db98e2043bde1	Apalache	InstanceNamedWithInFolder	Prime	True	Passed	Model Under Test Equivalent Model
ddc45b373c5f61a37ff8ec4e90239144750ddb06	Apalache	InstanceNamedWithInFolder	Prime	False	Passed	Model Under Test Equivalent Model
3f3001acd9119182626f3574409308511d49d62e	Apalache	Enabled	Prime	True	Failed: TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form	Model Under Test Equivalent Model
c7f97baecf90cb807d26ee99123473a6f8b317f7	Apalache	Enabled	Prime	False	Failed: TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form	Model Under Test Equivalent Model
4f6d34b2623b6b74fd6b9a72113b95da12a6dad8	Apalache	Lambda	Prime	True	Passed	Model Under Test Equivalent Model
2bf67c952db7a50a385bd35e229daefd3e34023e	Apalache	Lambda	Prime	False	Passed	Model Under Test Equivalent Model
c529d9531b1df4e102ee7ee207e9ce93395d30a2	Apalache	Cross2	Prime	True	Passed	Model Under Test Equivalent Model
b28765ca1b7b57fd1635c13c3fcb1f8c355bb92f	Apalache	Cross2	Prime	False	Passed	Model Under Test Equivalent Model
ce7eed1e617470a52064690170277e6310f0131e	Apalache	Cross3	Prime	True	Passed	Model Under Test Equivalent Model
f2f28edcecb3d6724625fa5e57f666ed77ada0cb	Apalache	Cross3	Prime	False	Passed	Model Under Test Equivalent Model
6a3aeea0c7ac7575c75a954822d665981a1ddc2b	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	Prime	True	Passed	Model Under Test Equivalent Model
7c448e43256aa0557534c0e6978f726fbeade1d2	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	Prime	False	Passed	Model Under Test Equivalent Model
8294aaa9fa245fea1c0a991ca33873a1ba488d39	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	Prime	True	Passed	Model Under Test Equivalent Model
327f19642068d4740009398b57d2f124198d3a08	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	Prime	False	Passed	Model Under Test Equivalent Model
9254992bcfbf659d7b21d737ad7957750ddfd2f3	Apalache	SetDiff	Prime	True	Passed	Model Under Test Equivalent Model
d449fd3ad2727aeadb5d02b4a00bcda78495b47b	Apalache	SetDiff	Prime	False	Passed	Model Under Test Equivalent Model
391e0b725cba9f8ff10dc127834f17a6f56922a2	Apalache	SetUnion	Prime	True	Passed	Model Under Test Equivalent Model
230bb7d8da2aae1966617efbc7c79630c7a6c650	Apalache	SetUnion	Prime	False	Passed	Model Under Test Equivalent Model
2ecbec2642fbadf7f3e339fa118bf6571499be21	Apalache	SetIntersect	Prime	True	Passed	Model Under Test Equivalent Model
53ab05cfe4c6719549d2154dedafdb50fb360316	Apalache	SetIntersect	Prime	False	Passed	Model Under Test Equivalent Model
62a14a85805b8bbad45d7662f508d10bb0bafda7	Apalache	SubsetEq	Prime	True	Passed	Model Under Test Equivalent Model
559fd77953a515ad68488554733ec7cb51618e36	Apalache	SubsetEq	Prime	False	Passed	Model Under Test Equivalent Model
5541bd1232289c8241b615955bffa5eb5dbbf027	Apalache	IfCond	Prime	True	Passed	Model Under Test Equivalent Model
ef76214524a4af1a6be5dbdb8d0b00c52f753162	Apalache	IfCond	Prime	False	Passed	Model Under Test Equivalent Model
a3d5ed39f814923334df841a0931500b2138303d	Apalache	IfThen	Prime	True	Passed	Model Under Test Equivalent Model
2faf483918c4f92f009a6d7a740cef01154c4641	Apalache	IfThen	Prime	False	Passed	Model Under Test Equivalent Model
1f816d2c009cc706e9a795d4d188803cf84144fc	Apalache	IfElse	Prime	True	Passed	Model Under Test Equivalent Model
eb6186604a51c317c0c50cc8df60f7d701f7e274	Apalache	IfElse	Prime	False	Passed	Model Under Test Equivalent Model
9645120f8debcf0d1c656e5b7cb6fdeb2cc60397	Apalache	Subset	Prime	True	Passed	Model Under Test Equivalent Model
20d661e75d4405a4961c30b08ee825b43582a3ee	Apalache	Subset	Prime	False	Passed	Model Under Test Equivalent Model
92304b23b22c82ec6703e23c430c06eb07e444d5	Apalache	Domain	Prime	True	Passed	Model Under Test Equivalent Model
c7c11f755b261eb964fa70560d627c89ecba817c	Apalache	Domain	Prime	False	Passed	Model Under Test Equivalent Model
32fa408404e86168d3eeb84e738ba9d11e169bf1	Apalache	Union	Prime	True	Passed	Model Under Test Equivalent Model
98f631837631216047060f49ddf24db6372a8331	Apalache	Union	Prime	False	Passed	Model Under Test Equivalent Model
6f8165beae91f4a90f6ca18f490e41690682a85f	Apalache	Equivalence	Prime	True	Passed	Model Under Test Equivalent Model
9926e38b82f247386ff4653b27fb334da007f2da	Apalache	Equivalence	Prime	False	Passed	Model Under Test Equivalent Model
23593e7e01ca9c3386888aae17c904fe7a16eceb	Apalache	SeqLen	Prime	True	Passed	Model Under Test Equivalent Model
3e0cf30db1e2daa2517db5949d73264f394da5c1	Apalache	SeqLen	Prime	False	Passed	Model Under Test Equivalent Model
2094e300a13b057694f448ce89aefb9cc8d93e7f	Apalache	SeqConcat	Prime	True	Passed	Model Under Test Equivalent Model
c88304f9e00eeca31ff5d64e9c3da7911a0167ec	Apalache	SeqConcat	Prime	False	Passed	Model Under Test Equivalent Model
13e590c6f19b4b93b743e1fa1c9eea37cc133015	Apalache	SeqSeq	Prime	True	Passed	Model Under Test Equivalent Model
9047603c3e5be7fa78aa956d8471d748a4ddb0a4	Apalache	SeqSeq	Prime	False	Passed	Model Under Test Equivalent Model
1db799412c616648cd5ee5c58392d7935dd0781a	Apalache	SeqSelectSeq	Prime	True	Passed	Model Under Test Equivalent Model
06f0384c0728743f216324c0a065a24b29706e7e	Apalache	SeqSelectSeq	Prime	False	Passed	Model Under Test Equivalent Model
94feca230080b5db33510cc25ff24c51b9db97d5	Apalache	SeqSubSeq	Prime	True	Passed	Model Under Test Equivalent Model
18ff2e878980780658e2866e3bb32ae6dafbd2c7	Apalache	SeqSubSeq	Prime	False	Passed	Model Under Test Equivalent Model
8dce0153123e51fcba173b0d7bf790d7428e1d84	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	Prime	True	Passed	Model Under Test Equivalent Model
b5776e9f44f5044f43e50381e131c89e851af7a7	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	Prime	False	Passed	Model Under Test Equivalent Model
6f2cd44d0ff4213abb61e1b205233e93f6904a18	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Prime	True	Passed	Model Under Test Equivalent Model
d00b1ec1f9ba76bdde285b33d264c37430e9e694	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Prime	False	Passed	Model Under Test Equivalent Model
f82baf83c1121d975d8a2b5c29901c3b9b5542c8	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	Prime	True	Passed	Model Under Test Equivalent Model
8a3f4c8b8438d096ee2eca023de42faac2372fa6	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	Prime	False	Passed	Model Under Test Equivalent Model
bc345542f26c5a075d0d66d974c98333d9cdd8d4	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Prime	True	Passed	Model Under Test Equivalent Model
8f298dd21aa72cdb4ec9962a249b94ddb4dca976	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	Prime	False	Passed	Model Under Test Equivalent Model
8e41c822a79abf79f292cbdf16d9bebead39f279	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Prime	True	Passed	Model Under Test Equivalent Model
dbca4a2e9931c86e730208e65a63868608f63a23	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	Prime	False	Passed	Model Under Test Equivalent Model
53f744bdc0da241a6cabb5f7be854607d8b041d8	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Prime	True	Passed	Model Under Test Equivalent Model
46c12091363e7c56d9ffbacd4de2290787353c83	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Prime	False	Passed	Model Under Test Equivalent Model
cb242e1f7e1e9d09ada80fd5ba823ecd7d7954cc	Apalache	BagBagToSet	Prime	True	Passed	Model Under Test Equivalent Model
bc134dc1af44637148997625a5705d385725521e	Apalache	BagBagToSet	Prime	False	Passed	Model Under Test Equivalent Model
3c96ec19eb18efabcf6d41a1128049ce467ad4d7	Apalache	BagSetToBag	Prime	True	Passed	Model Under Test Equivalent Model
2a3d75c3680ec8cccaa7aa18635bea86331a773a	Apalache	BagSetToBag	Prime	False	Passed	Model Under Test Equivalent Model
ed012e88b17687f77e2e7105a87a8fb378dd9222	Apalache	BagBagIn	Prime	True	Passed	Model Under Test Equivalent Model
184f7134205893377bfabbe7e6b37029c54d60bf	Apalache	BagBagIn	Prime	False	Passed	Model Under Test Equivalent Model
a8e1451b45f7b6726e78ac6054b99e0ead0d9a64	Apalache	BagAddBag	Prime	True	Passed	Model Under Test Equivalent Model
68258b309ed9db0f1a48c6904b4e05797335d190	Apalache	BagAddBag	Prime	False	Passed	Model Under Test Equivalent Model
9918b5cfc55607839595e3b520dcf144f4035552	Apalache	BagBagSub	Prime	True	Passed	Model Under Test Equivalent Model
c47f66f87c74780d69823594a700c7fb15fe2d8f	Apalache	BagBagSub	Prime	False	Passed	Model Under Test Equivalent Model
8fd41b6e52b97610e4b1e3d4fb671cfdf04d7828	Apalache	BagCopiesIn	Prime	True	Passed	Model Under Test Equivalent Model
3d93e0c452ba5649d8923ea5d76c9e19bc307451	Apalache	BagCopiesIn	Prime	False	Passed	Model Under Test Equivalent Model
c5c64bb46fa7b7b0ae147cb0995236d6692641ac	Apalache	BagSubsetEqBag	Prime	True	Passed	Model Under Test Equivalent Model
edc6cbf73a16b48b5273140cbe65136a56576e45	Apalache	BagSubsetEqBag	Prime	False	Passed	Model Under Test Equivalent Model
845a5887c5f8154b0abe0551d7fa8e2fc60cc691	Apalache	BagBagUnion	Prime	True	Passed	Model Under Test Equivalent Model
6b42a1772a2596d262639193d2250cf23847ea39	Apalache	BagBagUnion	Prime	False	Passed	Model Under Test Equivalent Model
09b80fd98a6608a6ace07dd12dfd4893e70da6a9	Apalache	BagBagCardinality	Prime	True	Passed	Model Under Test Equivalent Model
d77f3c4278769f31dcad536f4156c40203223196	Apalache	BagBagCardinality	Prime	False	Passed	Model Under Test Equivalent Model
9e096ef361205ff186a3a5e299963ff725ce281a	Apalache	BagBagOfAll	Prime	True	Passed	Model Under Test Equivalent Model
5eada67e3b49d7c47e74b169018786c5e8c90462	Apalache	BagBagOfAll	Prime	False	Passed	Model Under Test Equivalent Model
9e5db5dbe03b241b3fc2b38fdcf2ec6b92dd7a3b	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Prime	True	Passed	Model Under Test Equivalent Model
e7e497e3fd5a0cbfbbcf25992af5fe638d613af8	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	Prime	False	Passed	Model Under Test Equivalent Model
da1d7d9e454d49298325d05229db6e263dd18673	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	Prime	True	Passed	Model Under Test Equivalent Model
2633cb4eee6b54cfd3858f7dcd061c14faa8a02f	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	Prime	False	Passed	Model Under Test Equivalent Model
a2335d94f64d86b93c269dd8303100433705c7ff	Apalache	FiniteSetsCardinality	Prime	True	Passed	Model Under Test Equivalent Model
4fd5c7eaa56988d4fa7dafb4571ffd3eeff52365	Apalache	FiniteSetsCardinality	Prime	False	Passed	Model Under Test Equivalent Model
727e030fd21e34b95d57925a9191c6015bfe23f2	Apalache	SeqHead	Prime	True	Passed	Model Under Test Equivalent Model
eadde176d4fe38ecd37226791d63a7a37d78c800	Apalache	SeqHead	Prime	False	Passed	Model Under Test Equivalent Model
55aa45430186f3e4e466ad4a020213b04f77f290	Apalache	SeqTail	Prime	True	Passed	Model Under Test Equivalent Model
016e6a26d887a17cf667bc7625cba442a38b669a	Apalache	SeqTail	Prime	False	Passed	Model Under Test Equivalent Model
bfc40f78f510ddeee00631190f10ac576d4f59a9	Apalache	SeqAppend	Prime	True	Passed	Model Under Test Equivalent Model
b3e3725733af50a0b86245c90caefb509b1562c5	Apalache	SeqAppend	Prime	False	Passed	Model Under Test Equivalent Model

Index

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