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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
93260058bb7ea1f75e63204a3cdbf811136aba4f	Apalache	And	IfCond	True	Passed	Model Under Test Equivalent Model
cc30efb1bcad44905f03b3b7a858eb6dd98d8fc9	Apalache	And	IfCond	False	Passed	Model Under Test Equivalent Model
9843a1da5fc5dae1d863dde765086d7adfbbe22f	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	IfCond	True	Passed	Model Under Test Equivalent Model
a582ed1ada7c4a63ed62178f8ec29f79d310f6a7	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	IfCond	False	Passed	Model Under Test Equivalent Model
8fe30239537ef1da41240c2b687236ab8f900d8b	Apalache	Imply	IfCond	True	Passed	Model Under Test Equivalent Model
f3313d2be80cf47c9430e02a64d5503f236c47dd	Apalache	Imply	IfCond	False	Passed	Model Under Test Equivalent Model
944a31b263af64efc5c82fd5d9f737efa0c0da81	Apalache	Not	IfCond	True	Passed	Model Under Test Equivalent Model
125769fe2f70c8efdf61659ac4dc89d24d31cc7b	Apalache	Not	IfCond	False	Passed	Model Under Test Equivalent Model
9daf2e036193f6ff03b91e26efcf243b54ea866e	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	IfCond	True	Passed	Model Under Test Equivalent Model
af7ab025746747e77896a20ddcb217f8af50fa95	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	IfCond	False	Passed	Model Under Test Equivalent Model
e37c00189accf2773067c485e5822de2c9ef9237	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	IfCond	True	Passed	Model Under Test Equivalent Model
0e02fd214ea6cd326a166606a87f98192363b5cd	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	IfCond	False	Passed	Model Under Test Equivalent Model
ef2c4b6b4fdcc995aaae89d1a9b97b6d3f9e3ffc	Apalache	AndProp	IfCond	True	Passed	Model Under Test Equivalent Model
774afc9ea23f3d36a6277dfe4bcbb57b3cb67e93	Apalache	AndProp	IfCond	False	Passed	Model Under Test Equivalent Model
5faa9f34e5510ffd2a34dad415a0035b1d16c6ab	Apalache	Boxed	IfCond	True	Passed	Model Under Test Equivalent Model
970e8369f5c4b3b4322d8639d02ceaf603cd742c	Apalache	Boxed	IfCond	False	Passed	Model Under Test Equivalent Model
1a92bb20164455556738adf8a53909ade39bf162	Apalache	Eq	IfCond	True	Passed	Model Under Test Equivalent Model
ace5d1be65e6fb8cc3e9804ad3e3991612ec5e1e	Apalache	Eq	IfCond	False	Passed	Model Under Test Equivalent Model
d60086af239f09e67aa46d1c05002bc4e8fb3e1d	Apalache	Ne	IfCond	True	Passed	Model Under Test Equivalent Model
67e7329f7e8666ee9684bd2c1bd95da460f95805	Apalache	Ne	IfCond	False	Passed	Model Under Test Equivalent Model
21cc17eaaa6d50307ffb77a0c9baa380bd98f411	Apalache	Let	IfCond	True	Passed	Model Under Test Equivalent Model
cc11b8cc68fbfd572a320b902332bb039e8459b9	Apalache	Let	IfCond	False	Passed	Model Under Test Equivalent Model
e5c3a6cdcf6319659d82ca90140ff0fc496b043c	Apalache	Set0	IfCond	True	Passed	Model Under Test Equivalent Model
e7304e5a050014edb85863e2c07970372db72f4f	Apalache	Set0	IfCond	False	Passed	Model Under Test Equivalent Model
6c04c0e434c71d6068f3964a839132a88815fec5	Apalache	Set1	IfCond	True	Passed	Model Under Test Equivalent Model
4c0870987ee80c0efcccafbec38c0d9a3e9f64af	Apalache	Set1	IfCond	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
78f5343b35bcc3da0ad31b56fa2e4c970b1c9bf5	Apalache	Fun	IfCond	True	Passed	Model Under Test Equivalent Model
2152bec2ab7c0ae99336d988bb55f3b4db279e8c	Apalache	Fun	IfCond	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
2c2de631c33ab05472737cf63f5031530df9906f	Apalache	NotIn	IfCond	True	Passed	Model Under Test Equivalent Model
0bda7928ad802de767f912b6caabde818a49198a	Apalache	NotIn	IfCond	False	Passed	Model Under Test Equivalent Model
62a5248e4b3606d94a4d0e2ce917d2b098a5e062	Apalache	Exists	IfCond	True	Passed	Model Under Test Equivalent Model
253a342b74a8e96fafe2769cbda8ef368f31abd0	Apalache	Exists	IfCond	False	Passed	Model Under Test Equivalent Model
e015fb9a0983941de177e9d67016e755c093a515	Apalache	Forall	IfCond	True	Passed	Model Under Test Equivalent Model
3e55afa137ff42dbb03ddf8e1e083e49cfef8403	Apalache	Forall	IfCond	False	Passed	Model Under Test Equivalent Model
77453c4acdbe0cb2587ba3ec9825f3f34b79901e	Apalache	Choose	IfCond	True	Passed	Model Under Test Equivalent Model
e116dc06b2d531f54ea9e31252174a6b8a8dd0f1	Apalache	Choose	IfCond	False	Passed	Model Under Test Equivalent Model
1d6d08faca220fbe8f1a6761cca1d83c3a545ff1	Apalache	Record	IfCond	True	Passed	Model Under Test Equivalent Model
e0f0c210a222335dee21e62dc9e713ea576c5da9	Apalache	Record	IfCond	False	Passed	Model Under Test Equivalent Model
add06bf8016c001fc83a4cc7c0d9cad3e29317e0	Apalache	Tuple	IfCond	True	Passed	Model Under Test Equivalent Model
8558109aebc21b5b86646141fec152fe7a9f3d4b	Apalache	Tuple	IfCond	False	Passed	Model Under Test Equivalent Model
5cd7f0ce64754ecbb70caffd1744a2caafb678f7	Apalache	FunApp	IfCond	True	Passed	Model Under Test Equivalent Model
ad95b77709069e2b39cfa84bd0fa2a49168cf72f	Apalache	FunApp	IfCond	False	Passed	Model Under Test Equivalent Model
708cf034e05d6e4d690f0391a029716adafe19fe	Apalache	Except0	IfCond	True	Passed	Model Under Test Equivalent Model
fce4e78ea18a361ea4a592980da932400e8299ce	Apalache	Except0	IfCond	False	Passed	Model Under Test Equivalent Model
420e7140f82eafb47ca30b72d14f24a437c54f5e	Apalache	Except1Fun	IfCond	True	Passed	Model Under Test Equivalent Model
70e49d4d6e2c25c548ddc0bcf5b64b7a58ea5379	Apalache	Except1Fun	IfCond	False	Passed	Model Under Test Equivalent Model
6c8d49e2c84971e8e6b8af07f8eb10ca5e16fa63	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	IfCond	True	Passed	Model Under Test Equivalent Model
09028ef9aefcb717c492e673559f3b5b6ced7c85	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	IfCond	False	Passed	Model Under Test Equivalent Model
3d5be81a7c1ab416e2b32c90adcbe4665f66a060	Apalache	Except1Rec	IfCond	True	Passed	Model Under Test Equivalent Model
3aecdb7a799e93758d8b6cef8096f78d68c1a613	Apalache	Except1Rec	IfCond	False	Passed	Model Under Test Equivalent Model
8dd43f9c05d898c23e6a25f70e6a39c726ddfe59	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	IfCond	True	Passed	Model Under Test Equivalent Model
a7184dff2677e75f1037504506368bbc17b38b7e	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	IfCond	False	Passed	Model Under Test Equivalent Model
94c4adf8616713ccee143a1c10e2e41b19961349	Apalache	Except2Fun	IfCond	True	Passed	Model Under Test Equivalent Model
8946faf9d1c1be958803c200226a2a7ee669b6e0	Apalache	Except2Fun	IfCond	False	Passed	Model Under Test Equivalent Model
a5295f67ff6a3b93287b7970b536edda0ed035b5	Apalache	Except2FunTuple	IfCond	True	Passed	Model Under Test Equivalent Model
44b751d04ba1d327db7d028e2312a5db24a0a6c1	Apalache	Except2FunTuple	IfCond	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
efaf7732eafd56c48f59558b9dc76a2fe21d5b7f	Apalache	NumUnaryMinus	IfCond	True	Passed	Model Under Test Equivalent Model
1f59abdcca3dd52e43137930fc3f70f2f49cb775	Apalache	NumUnaryMinus	IfCond	False	Passed	Model Under Test Equivalent Model
5dd01dacba7906e39bf1a54db3f552da5b576afa	Apalache	NumPlus	IfCond	True	Passed	Model Under Test Equivalent Model
6533ae8f6e18dc666b87232d1789390c5125eeea	Apalache	NumPlus	IfCond	False	Passed	Model Under Test Equivalent Model
b868b50b748970cd37aaec094bc12bbc96c8994a	Apalache	NumMinus	IfCond	True	Passed	Model Under Test Equivalent Model
0486d76bcd94dd30790fa6b5ffb244993dce4b6c	Apalache	NumMinus	IfCond	False	Passed	Model Under Test Equivalent Model
078068d22cabbe7bd501b533a9d0e1968444ef3c	Apalache	NumMul	IfCond	True	Passed	Model Under Test Equivalent Model
32d67182be32f27a727251eef9c0cdb391d6ff7b	Apalache	NumMul	IfCond	False	Passed	Model Under Test Equivalent Model
3dc8abf664fecafdbfca67cdda08f846994fdce4	Apalache	NumDiv	IfCond	True	Passed	Model Under Test Equivalent Model
a2dff2ac9fad78bc9aff995b8050370b891bc3e4	Apalache	NumDiv	IfCond	False	Passed	Model Under Test Equivalent Model
d71f13529609e7f03ca2cdb83040cf0c82995913	Apalache	NumMod	IfCond	True	Passed	Model Under Test Equivalent Model
bae8613fb70c009489dfbbe2b86f88df57c4234b	Apalache	NumMod	IfCond	False	Passed	Model Under Test Equivalent Model
eb7796812c02f684d9cd9512ff68f08320109323	Apalache	NumPow	IfCond	True	Passed	Model Under Test Equivalent Model
7287678f29467b1734d36084ea60867d262e7b83	Apalache	NumPow	IfCond	False	Passed	Model Under Test Equivalent Model
f2007b06254848b2fdc2c7e180246604c3fe6bed	Apalache	NumGt	IfCond	True	Passed	Model Under Test Equivalent Model
3995ae35a5eabc53a1b5b5e9afd71f11ef2ae29f	Apalache	NumGt	IfCond	False	Passed	Model Under Test Equivalent Model
40fbb529f22b5926d4e76b908b92f85d4d856cb2	Apalache	NumGe	IfCond	True	Passed	Model Under Test Equivalent Model
68c2669bd358039024941f1983c731310badc9d0	Apalache	NumGe	IfCond	False	Passed	Model Under Test Equivalent Model
d5f37a983d5493f9521d0843bd69cc06da155830	Apalache	NumLt	IfCond	True	Passed	Model Under Test Equivalent Model
1f6c3d5e01bed0909f84d86ee9b183a90b0b4da9	Apalache	NumLt	IfCond	False	Passed	Model Under Test Equivalent Model
3041112e792f0be0339b070e78112a545eb1e2c4	Apalache	NumLe	IfCond	True	Passed	Model Under Test Equivalent Model
f3f673a56eafb74697cd5ee4444d69324ced79c4	Apalache	NumLe	IfCond	False	Passed	Model Under Test Equivalent Model
0e1f44eb0133a04b92daed03669ca405d0d49301	Apalache	DefFun	IfCond	True	Passed	Model Under Test Equivalent Model
514b5d287edb62a82c89d769dea89047d5d7cbac	Apalache	DefFun	IfCond	False	Passed	Model Under Test Equivalent Model
73f61e6298ad50e1b5e09d91f5b066d0d0baec2f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	IfCond	True	Passed	Model Under Test Equivalent Model
5d1c01f28a38b8519719821e04efeb73f710f5f1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	IfCond	False	Passed	Model Under Test Equivalent Model
0b1c34ce77108bb7475e6811cb39ef3095c68e55	Apalache	DefFunRecursive	IfCond	True	Passed	Model Under Test Equivalent Model
15b6a6bc04deefba6bb1c29d4520938c6a42a76c	Apalache	DefFunRecursive	IfCond	False	Passed	Model Under Test Equivalent Model
0ad789fc9ab9c4a57b193e8042b6460b75851446	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	IfCond	True	Passed	Model Under Test Equivalent Model
2a7614a708b23fb033bf1d6ab8d1f24fc7b7455b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	IfCond	False	Passed	Model Under Test Equivalent Model
0e9e7bb6acabd152e7d170c0f6fa77c82ba743c6	Apalache	Def0	IfCond	True	Passed	Model Under Test Equivalent Model
7e3a2dcf78f479435bd0a9b641134ca02b1f1d99	Apalache	Def0	IfCond	False	Passed	Model Under Test Equivalent Model
a57d5f62703eb61d3904d7cd19489ae5ba71c087	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	IfCond	True	Passed	Model Under Test Equivalent Model
3a2d5f98d34750d17c68c2cbfbd3b7b2fa8901e4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	IfCond	False	Passed	Model Under Test Equivalent Model
79b624dc87221e4c02b59bf48722225fb1285551	Apalache	Def1	IfCond	True	Passed	Model Under Test Equivalent Model
929ca68e4a38e621c79623c21bf17eebec219834	Apalache	Def1	IfCond	False	Passed	Model Under Test Equivalent Model
b448206fa91594fa08e12712562a9a5475d15e15	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	IfCond	True	Passed	Model Under Test Equivalent Model
341237aea599739eb28b614217622b85f47e8270	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	IfCond	False	Passed	Model Under Test Equivalent Model
2a5064f12a3ba0fa3b6dd8640b6d0cf0a50da1c3	Apalache	Def2	IfCond	True	Passed	Model Under Test Equivalent Model
42444f5d6bb35565b9b856437c962c30cfc347b6	Apalache	Def2	IfCond	False	Passed	Model Under Test Equivalent Model
d5b7da85c46ebbe539268be60856593ab32ba717	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	IfCond	True	Passed	Model Under Test Equivalent Model
f96b00a9a8634d2df0b65c64e4c38c058eb166a7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	IfCond	False	Passed	Model Under Test Equivalent Model
8de65950fe8a5727fcb888d5b98eea238f9a636d	Apalache	Def1Recursive	IfCond	True	Passed	Model Under Test Equivalent Model
5a9fe16142f8b2dae886e7d3d71cba13807e5402	Apalache	Def1Recursive	IfCond	False	Passed	Model Under Test Equivalent Model
25fb96c3a788fa7905eeb0c1d97c3d2c8e8e34d3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	IfCond	True	Passed	Model Under Test Equivalent Model
fb42309104dccd73835b3812b44e779f4096c892	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	IfCond	False	Passed	Model Under Test Equivalent Model
35b88692b5b310323a371efb494d0970c9b954f7	Apalache	Extends	IfCond	True	Passed	Model Under Test Equivalent Model
1473b360373edc360e034bcbf5b8e2b5f6c76649	Apalache	Extends	IfCond	False	Passed	Model Under Test Equivalent Model
a206734f2d31ca90ca5877b05fd09cf20267ff0c	Apalache	ExtendsInDifferentFolder	IfCond	True	Passed	Model Under Test Equivalent Model
e61bc79adee43733b694ba0596886a9a6cb9efdc	Apalache	ExtendsInDifferentFolder	IfCond	False	Passed	Model Under Test Equivalent Model
47052fda3cb27f6274d90e94a5b46682d79f7875	Apalache	Variable	IfCond	True	Passed	Model Under Test Equivalent Model
51e83f4d5ec7bd6482ec1e05bdc496aed18cedd9	Apalache	Variable	IfCond	False	Passed	Model Under Test Equivalent Model
3cf800bca5180dc607165437a7b75800b0ed56fe	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	IfCond	True	Passed	Model Under Test Equivalent Model
cc260e33d40b4972169d5fb47b47667000e78621	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	IfCond	False	Passed	Model Under Test Equivalent Model
e478bc98aa9104da20c9eff254fbf00e12c1d401	Apalache	Constant	IfCond	True	Passed	Model Under Test Equivalent Model
aab7ee1873d503ddf564d24f20174f89240c1014	Apalache	Constant	IfCond	False	Passed	Model Under Test Equivalent Model
da110be380ee154794af80f1536220821b7af359	Apalache	ConstantRank1	IfCond	True	Passed	Model Under Test Equivalent Model
18e68f6f50311e98152d4739eaf5b6eb4ad3b7c9	Apalache	ConstantRank1	IfCond	False	Passed	Model Under Test Equivalent Model
d572869da01421c0a541e368a04e1251e17ce102	Apalache	Instance	IfCond	True	Passed	Model Under Test Equivalent Model
3e28eccccaa33e6dc29a52a3c75a80cb3d231ee3	Apalache	Instance	IfCond	False	Passed	Model Under Test Equivalent Model
8691314bc46867fbebd8c435030b9c6fec81fdff	Apalache	InstanceWith	IfCond	True	Passed	Model Under Test Equivalent Model
4019a74af39f519007315b76d1cea75ff275df20	Apalache	InstanceWith	IfCond	False	Passed	Model Under Test Equivalent Model
841117cdab871e71cd5529a37c65ab71f0f9017c	Apalache	InstanceNamed	IfCond	True	Passed	Model Under Test Equivalent Model
64b1e2b8085bfae9ec82a15e4a4b3b508f1595e5	Apalache	InstanceNamed	IfCond	False	Passed	Model Under Test Equivalent Model
9ce22a60fd4b79965d207fce0e9b71d6d6dc9d9d	Apalache	InstanceNamedWith	IfCond	True	Passed	Model Under Test Equivalent Model
4271ae2981ac257995b7a53e182466ddb2e220d2	Apalache	InstanceNamedWith	IfCond	False	Passed	Model Under Test Equivalent Model
fa3a54fbf833a45fb31828c41b942a7063ab304b	Apalache	InstanceInFolder	IfCond	True	Passed	Model Under Test Equivalent Model
d5bbd75716e641a328b9de64f533855641d411dd	Apalache	InstanceInFolder	IfCond	False	Passed	Model Under Test Equivalent Model
c8a8c82e16a85e9dc19a2fa8f3501014c115e9c6	Apalache	InstanceWithInFolder	IfCond	True	Passed	Model Under Test Equivalent Model
ec3360a58b609cf83eea6f73db57c2f2a683cc79	Apalache	InstanceWithInFolder	IfCond	False	Passed	Model Under Test Equivalent Model
43839ab801a011a980b6fc25871ff8694e11fab0	Apalache	InstanceNamedInFolder	IfCond	True	Passed	Model Under Test Equivalent Model
63aebfa6f83d3429f6bdb93c61eba5b94d45987e	Apalache	InstanceNamedInFolder	IfCond	False	Passed	Model Under Test Equivalent Model
57dbb30a8830a74ab81a91cfef09a7cb600770c9	Apalache	InstanceNamedWithInFolder	IfCond	True	Passed	Model Under Test Equivalent Model
8cb1eb259d03cb66d72c10a048cc1aa93e3e0244	Apalache	InstanceNamedWithInFolder	IfCond	False	Passed	Model Under Test Equivalent Model
de434e270e057b8a743b7e9d44cc3b408542e761	Apalache	Enabled	IfCond	True	Passed	Model Under Test Equivalent Model
9aae582d87f3946dbee1b81102a4a68fcdb7b582	Apalache	Enabled	IfCond	False	Passed	Model Under Test Equivalent Model
e25336e6b8a1736390e405d5ed1be3f8c32c19b5	Apalache	Assume	IfCond	True	Passed	Model Under Test Equivalent Model
baa4b34fee31f590342255e1e1abe2123dd1c7a3	Apalache	Assume	IfCond	False	Passed	Model Under Test Equivalent Model
07f87504239c4f87954d7e072e5955e45d79530f	Apalache	AssumeNamed	IfCond	True	Passed	Model Under Test Equivalent Model
d80ed5b95d8b6e1ee414df0f86a813e7c40ccbb2	Apalache	AssumeNamed	IfCond	False	Passed	Model Under Test Equivalent Model
2fdf684ea85e2b34300e50c19c52aebcca5c5f76	Apalache	Lambda	IfCond	True	Passed	Model Under Test Equivalent Model
5587653c7e3f831fd71521693ea4de354fcb2863	Apalache	Lambda	IfCond	False	Passed	Model Under Test Equivalent Model
4f99a4cf4453e177a96848d4a5ed6ab5615ad688	Apalache	Cross2	IfCond	True	Passed	Model Under Test Equivalent Model
7be54e29d2fbad200709a341c20a4533821b5072	Apalache	Cross2	IfCond	False	Passed	Model Under Test Equivalent Model
acd6cb0cd567dd6a31a5e55df87683d99d24d117	Apalache	Cross3	IfCond	True	Passed	Model Under Test Equivalent Model
c8a08a2b40e4f5da710cccfc03b646ba79e13730	Apalache	Cross3	IfCond	False	Passed	Model Under Test Equivalent Model
29556e05f0172395868c878381ded3732b2a068a	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	IfCond	True	Passed	Model Under Test Equivalent Model
db70ceef9c6338872295d9be7738d4e129bb9f3b	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	IfCond	False	Passed	Model Under Test Equivalent Model
6493a24c6a946f16a8d9b3a078993d18d2d4ffde	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	IfCond	True	Passed	Model Under Test Equivalent Model
4653f37c2ad45d9655a167829db6f326a5503164	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	IfCond	False	Passed	Model Under Test Equivalent Model
28de05b2294345fcb32917f08ea49f1c48365c65	Apalache	SetDiff	IfCond	True	Passed	Model Under Test Equivalent Model
e6b27023ba1ea24381f3e91b8496ebc1a77fcbdb	Apalache	SetDiff	IfCond	False	Passed	Model Under Test Equivalent Model
09881ee8078a5f97e63dada96f98ead2112677ec	Apalache	SetUnion	IfCond	True	Passed	Model Under Test Equivalent Model
f7bf07297e239c70e16cd2309d2de86ff186dbb1	Apalache	SetUnion	IfCond	False	Passed	Model Under Test Equivalent Model
fcb89fe06a22d6302ff3fb87ddc0d9622a1a7a54	Apalache	SetIntersect	IfCond	True	Passed	Model Under Test Equivalent Model
fb3d8c25d8af47a651780365594234425f87a15e	Apalache	SetIntersect	IfCond	False	Passed	Model Under Test Equivalent Model
9f13afcd1db8cb952f1510eac6812be2edf2b613	Apalache	SubsetEq	IfCond	True	Passed	Model Under Test Equivalent Model
a44fb8cec0587c753bbc1c65b22ff951586b7c86	Apalache	SubsetEq	IfCond	False	Passed	Model Under Test Equivalent Model
dca1025cecf5e00f39c12fc75ea69bcf493cc413	Apalache	IfCond	IfCond	True	Passed	Model Under Test Equivalent Model
4f3ac5ad0bb3717cfc337677eead9f0e921a183e	Apalache	IfCond	IfCond	False	Passed	Model Under Test Equivalent Model
2148f4386fb1b5d548aaaec62c170af32235051f	Apalache	IfThen	IfCond	True	Passed	Model Under Test Equivalent Model
fbf31ec92b399bb41936aac2e10d9d58182576ef	Apalache	IfThen	IfCond	False	Passed	Model Under Test Equivalent Model
8a732b0ce2bdcec811d100ea1f8e83a2f00e57d7	Apalache	IfElse	IfCond	True	Passed	Model Under Test Equivalent Model
b4c76bf7350ac1ce337e0808fbb10711ce4628bb	Apalache	IfElse	IfCond	False	Passed	Model Under Test Equivalent Model
cbdfb420faaf8ea51f1ce9129a10adeb3919ddcb	Apalache	Subset	IfCond	True	Passed	Model Under Test Equivalent Model
25640eb27990e77de0ed147be434580ee252bbef	Apalache	Subset	IfCond	False	Passed	Model Under Test Equivalent Model
96be80444072c588e07c7dc20081b2287b47bd05	Apalache	Domain	IfCond	True	Passed	Model Under Test Equivalent Model
9344488fb2e4159089936702a586716d12328e57	Apalache	Domain	IfCond	False	Passed	Model Under Test Equivalent Model
4244e583825f7651d25576e9ed665c215896abbf	Apalache	Union	IfCond	True	Passed	Model Under Test Equivalent Model
4c92879bf750b4de2886626f2ed93cd96ae6bebe	Apalache	Union	IfCond	False	Passed	Model Under Test Equivalent Model
d18ac0dd74402d75a27478cbe694067d9c0c6131	Apalache	Unchanged	IfCond	True	Passed	Model Under Test Equivalent Model
163314ebd441da67c2e024eda41f7137ade244af	Apalache	Unchanged	IfCond	False	Passed	Model Under Test Equivalent Model
6c61a567c219702fa1909206d9fafb27cfec2fd6	Apalache	Equivalence	IfCond	True	Passed	Model Under Test Equivalent Model
107da1b4cd5a89cd2416b185f888e8da942b8678	Apalache	Equivalence	IfCond	False	Passed	Model Under Test Equivalent Model
d62d3b7550baa32831087a8f0dd5b34b8cbb3d58	Apalache	SeqLen	IfCond	True	Passed	Model Under Test Equivalent Model
1b748d25ac9057236f537f20295ada9b449df0bd	Apalache	SeqLen	IfCond	False	Passed	Model Under Test Equivalent Model
a0e7839e5ada6071e95ae82fa3f459f6194fb7c0	Apalache	SeqConcat	IfCond	True	Passed	Model Under Test Equivalent Model
e908a323b3cf4f16212e7d94430615ede0156a1d	Apalache	SeqConcat	IfCond	False	Passed	Model Under Test Equivalent Model
6ab7793438241a51472db8e32ffeb8dc1e6e1568	Apalache	SeqSeq	IfCond	True	Passed	Model Under Test Equivalent Model
ebf949d7f90c022d101d24664534ad0c287ae7ad	Apalache	SeqSeq	IfCond	False	Passed	Model Under Test Equivalent Model
ce4ff7481f2f74daadc505bbb53e294d1c07a652	Apalache	SeqSelectSeq	IfCond	True	Passed	Model Under Test Equivalent Model
03ac7b56a42e23af6537ad6e530f786bb0adc35a	Apalache	SeqSelectSeq	IfCond	False	Passed	Model Under Test Equivalent Model
f9f4eaafd2815e134fdc5bcc31d1cb4a0e258fe7	Apalache	SeqSubSeq	IfCond	True	Passed	Model Under Test Equivalent Model
36441e3673aceb7636fba3b399e261fbf63a873f	Apalache	SeqSubSeq	IfCond	False	Passed	Model Under Test Equivalent Model
e796ad56e1d0d35f17df1659ee54c6661fb73cac	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	IfCond	True	Passed	Model Under Test Equivalent Model
9a94dc26c487e3c5e106be3a8299e96d19fce335	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	IfCond	False	Passed	Model Under Test Equivalent Model
43d0f7d5b086add62d5b900f63ca69271c7bd2d0	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	IfCond	True	Passed	Model Under Test Equivalent Model
594c83de82b1d40db18ecb63cd69acf30103f8ce	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	IfCond	False	Passed	Model Under Test Equivalent Model
1f614ffd4f5ab721793a5a4343d191bd22fcfbd0	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	IfCond	True	Passed	Model Under Test Equivalent Model
a7847ff36dbd1e2ba42f4560facf2852f2ce82f5	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	IfCond	False	Passed	Model Under Test Equivalent Model
2dc1f72e403c29f881fadb229d696d6e32d3979e	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	IfCond	True	Passed	Model Under Test Equivalent Model
15cf594d51d1c10d05727115925048dd96106518	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	IfCond	False	Passed	Model Under Test Equivalent Model
683ca9afec2a6e56aa5dbdcf81cb8db946e7cb45	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	IfCond	True	Passed	Model Under Test Equivalent Model
34e043e0d4c6cc3f01f8f2ee0422ed8e0f4d17b6	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	IfCond	False	Passed	Model Under Test Equivalent Model
241a6c887ce8cb181cba95846fb8fc3054f3192b	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	IfCond	True	Passed	Model Under Test Equivalent Model
2235b88e31172dc68339b9f0ccc31973e8a780a3	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	IfCond	False	Passed	Model Under Test Equivalent Model
3ebc5312cdce5ed60f3cc7ff2e6c6bdd46d68de7	Apalache	BagBagToSet	IfCond	True	Passed	Model Under Test Equivalent Model
fa438a8efa5439f31b82db88a564bb306452ef4d	Apalache	BagBagToSet	IfCond	False	Passed	Model Under Test Equivalent Model
8e98fffdfd67f6828bc48263483af18fbca33d52	Apalache	BagSetToBag	IfCond	True	Passed	Model Under Test Equivalent Model
bbe964f8e8d2868d8743a095fdbe0fa9ad810dd0	Apalache	BagSetToBag	IfCond	False	Passed	Model Under Test Equivalent Model
fbab098ffa0bcb5e73257331c8fe8ba71147f401	Apalache	BagBagIn	IfCond	True	Passed	Model Under Test Equivalent Model
0a8cba3fd9888e7c714985d66c8ed5fe4ddb6d6f	Apalache	BagBagIn	IfCond	False	Passed	Model Under Test Equivalent Model
ec50b3f9379251c24aa90970e72bcfff0d48aacb	Apalache	BagAddBag	IfCond	True	Passed	Model Under Test Equivalent Model
1a5a22e66418ac7a6e56f1a26b8b2b6f2ccedb18	Apalache	BagAddBag	IfCond	False	Passed	Model Under Test Equivalent Model
96004a7a0bfa86a1912d05fc39c68f3b7a483361	Apalache	BagBagSub	IfCond	True	Passed	Model Under Test Equivalent Model
c61fb01f834f27c6d99966b6309e9ea8cd93d7e4	Apalache	BagBagSub	IfCond	False	Passed	Model Under Test Equivalent Model
64e84d862cdf200adf50882a18175b1170e2e1d7	Apalache	BagCopiesIn	IfCond	True	Passed	Model Under Test Equivalent Model
3340b46b19064cc549d33367fa4cb4d8fbea40c2	Apalache	BagCopiesIn	IfCond	False	Passed	Model Under Test Equivalent Model
05d981eb2a832badc1776666890bd3435b82789c	Apalache	BagSubsetEqBag	IfCond	True	Passed	Model Under Test Equivalent Model
63f2d3ef2bcc3b6ad800289fa2f4775e49fc2009	Apalache	BagSubsetEqBag	IfCond	False	Passed	Model Under Test Equivalent Model
3063769ee281ff93b41c69363f24dcaf448f7037	Apalache	BagBagUnion	IfCond	True	Passed	Model Under Test Equivalent Model
8766022f27ab2b753a449295d90f7f3eda41b243	Apalache	BagBagUnion	IfCond	False	Passed	Model Under Test Equivalent Model
78f0ac95ed4fe3accde368e3042ea2441f06c0ab	Apalache	BagBagCardinality	IfCond	True	Passed	Model Under Test Equivalent Model
5be170b0b195ae7ded381b565303d92e497a48c3	Apalache	BagBagCardinality	IfCond	False	Passed	Model Under Test Equivalent Model
e687c887160138fc190f5f6daee52854af59f239	Apalache	BagBagOfAll	IfCond	True	Passed	Model Under Test Equivalent Model
c9f8c91dd427553e732ae0077db98905ef09d428	Apalache	BagBagOfAll	IfCond	False	Passed	Model Under Test Equivalent Model
1b0a8e81f85988a84525e287f8e304543eea49a0	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	IfCond	True	Passed	Model Under Test Equivalent Model
21476ef178c65982fc473274bcdb4d20e689650b	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	IfCond	False	Passed	Model Under Test Equivalent Model
1648225c2d3e793373ee68d057ff44b9119fab7c	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	IfCond	True	Passed	Model Under Test Equivalent Model
f127314385b261fb05ae0d677440f9bc2a5a9f5c	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	IfCond	False	Passed	Model Under Test Equivalent Model
4218054b73e9b778c75507ede6afb750427dfafe	Apalache	FiniteSetsCardinality	IfCond	True	Passed	Model Under Test Equivalent Model
9505dca16961caa88ec3aed227e62c4ebcd63817	Apalache	FiniteSetsCardinality	IfCond	False	Passed	Model Under Test Equivalent Model
d8c254303e582b434be2ffdefc2b9b05ea373624	Apalache	SeqHead	IfCond	True	Passed	Model Under Test Equivalent Model
0c8155ade0fb3fdd54f7d43232bbd9a7fee46c20	Apalache	SeqHead	IfCond	False	Passed	Model Under Test Equivalent Model
5186219e588a9a8c9d0deedf7c6c398f340c7bdd	Apalache	SeqTail	IfCond	True	Passed	Model Under Test Equivalent Model
2dc041c9bb2fac4f182182e7b3fedecf060108b2	Apalache	SeqTail	IfCond	False	Passed	Model Under Test Equivalent Model
bb49e8c6ffabc3feb7836216f1593bb61a486344	Apalache	SeqAppend	IfCond	True	Passed	Model Under Test Equivalent Model
8f68d3ab810605f52164141e202c9ae3f9eebf2a	Apalache	SeqAppend	IfCond	False	Passed	Model Under Test Equivalent Model

Index

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