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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
d54c5e8e653828dc90971b10ff892c35c3389290	Apalache	Eq	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ac6175c5351c5c620a04f082801fd7391868efc1	Apalache	Eq	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
da924680287b9fc2c32facea7af237a13d8e50b3	Apalache	Ne	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
816242a6736d065a696bc1c1c5e47d539e96e231	Apalache	Ne	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
bf6053f24ebf0c6227d7cf5b30943032deb0f86a	Apalache	Let	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
f807f627d8c2b85b64609a65e06dc44190a1a42f	Apalache	Let	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
4dc600eb1dbf5ef9d98fa05c4bdb26885c6b4bfa	Apalache	Set0	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
882aabb13c0c90b407a6b9e6864b6862913dcc10	Apalache	Set0	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
2bafd18f631db6e0eeecaeb5926a06b1e3b1cbeb	Apalache	Set1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c5e863824e59789e16ed770a097644fefc5d2593	Apalache	Set1	DefFunRecursive	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
47b22afb8cbaec790926a5420446a3f8462b56d8	Apalache	Fun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
3aedb214c7b061020f87af53ffc51f3766f2a0bf	Apalache	Fun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
d31e1ee5d08300f59b5b051d92fb4bd4ba591e64	Apalache	In	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
40f3e5ef48d492b9d0159fc1a8552aacd220f873	Apalache	In	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
f48d5b5334a5c075e79218524313ecc1ef539d2f	Apalache	NotIn	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
275f83f7189345fc84a602a90464c54b786a941e	Apalache	NotIn	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
fea252f99362b8e2c9b583e20f31437533026ec1	Apalache	Record	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c41f46236b9a0deab6a0ab75046b911103aa2a0a	Apalache	Record	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
3ffa895c2f3e08330d3676e3f7a2654726006619	Apalache	Tuple	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ea775a9f64e76b3c49bbaff0879293e4bad1b115	Apalache	Tuple	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
991080016df7b4a87ff350f16ece7553bdbcd4d5	Apalache	FunApp	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
4b51e4ce0c65d8a9047e6803bcfa27665964beca	Apalache	FunApp	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
aa5392bc0869e89bde5088be9e82ae04069e3c73	Apalache	Except0	DefFunRecursive	True	Failed: TLC result is correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. Moreover, in this case, Apalache produces result, which violates TLA+ CHOOSE semantics	Model Under Test Equivalent Model
fd438e654d87e6c621db9cc8ef25d6b1e6c7a8d1	Apalache	Except0	DefFunRecursive	False	Failed: TLC result is correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. Moreover, in this case, Apalache produces result, which violates TLA+ CHOOSE semantics	Model Under Test Equivalent Model
0b89261df606041a51c75d2eec967992c1340ea1	Apalache	Except1Fun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
13c59c9a29dd3987fadf1b2648e381773d39ad58	Apalache	Except1Fun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
eb4957fe58abc2dadab0ed1c1ef3cf53149657f3	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
2137d85496f87c322dc2359ab8588ac6b70a96f1	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
23bb2eaad08c4fd8f87fa308ed10fc70a43879c2	Apalache	Except1Rec	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
609f5bf93810fe40d25b1fbcf0f8982520027e93	Apalache	Except1Rec	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
3dfbe2f464364dbd2dc9bacb7f13f53625c44993	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
8dada14b6be6206a4f39fc12732bfda0341c1df6	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
1a6afa488893224bb332b49e780468a531508b5f	Apalache	Except2Fun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
fcbf5e3640cf03a9de95ffbfaded05249ab5ea73	Apalache	Except2Fun	DefFunRecursive	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
9efd7b350dc6132bec71b789f64f97ac1323be37	Apalache	DefFun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
3b38398cc64eadd5ac3dffd699728329a5039d11	Apalache	DefFun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
b3dce058374d06ac1b809700698877e7ebf70bca	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
7fd10fcf12ba649d36ce183a2b06cdef993fd5be	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
aeef740d8931ed3915ebce0ee0ca2bdf91b0db45	Apalache	DefFunRecursive	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
a0670f1df081fd369127b74dd97d6f7f97aa295b	Apalache	DefFunRecursive	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
f050d95ad4433564ac80fa502efe4db218623a5b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c4e627bcc5f4eaa9a8d5455fe363167658d84512	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
5b4fd581b51b9eb26f6693c095f5d48d2f271d1c	Apalache	Def0	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
20ad6cb51bc8b7df21de843541d426c6fae02d6f	Apalache	Def0	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
b761d26c5ceaa378d4f6db750185fef554c01d4e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
2fd0173f7ae31cf4a32d97d5d6bbad26f36dad7d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
ecc46143ca53f1f394eb5bfcd9d9e244a634dc1e	Apalache	Def1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
efb4e80e6554d5bf33566b9a3641c0dd48572497	Apalache	Def1	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
eda37c8d968deb6630193643150916a499e8eae2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ba2a72639363f18529f703b9a5535bb40b34cea5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
11eab07035be22d4ba5176aa95e1f2a78e247547	Apalache	Def2	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c442d92911b870e7aca35aed9d0b9f52d5e6cfb4	Apalache	Def2	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
0a75374c94729e5e22d64950ee0ce466e79d8ac0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
9d3c1bbefe2a4a68f0543fd065d2212a69361fcb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
01a2c1535e3e8cecef8ee2898961b14947a72fad	Apalache	Def1Recursive	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
85bf85a104452081d79ae406970d7df494d138a8	Apalache	Def1Recursive	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
3b02b3aa92db45e49e354d19e3eeedcfae9398d3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
e0fbdc38d36ef0a4d99a5f83c3e0981bfbe0a109	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
60198255058df2b00c2886c5457845fae429cb14	Apalache	Extends	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
fb105c45970cf4186c713527ff1cd484a1c755c5	Apalache	Extends	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
f9fdbed333aa1b66b38e07c1afc4b9c9a53bbc2c	Apalache	ExtendsInDifferentFolder	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
b6470f228672a3b00f302c7036bf735b75fef320	Apalache	ExtendsInDifferentFolder	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
5ae96488e6fba7d6b024fb03d98165e4641dedf1	Apalache	Variable	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
0bbadb63613a395f4e80e1513b842480d249940a	Apalache	Variable	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
61e402327165977efb2829c388d41f9f1be436d5	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
5c1535a9873a165bebfd5ff3cf113c8626d980b7	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
5a6b671a02f158cbcf52e11947dbd85d90c8e4aa	Apalache	Constant	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ed6e9394fc54249d391f765d3f14c8b2d53f80a2	Apalache	Constant	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
11b7877695a5ec510f905708523dc1fbc00dfe0d	Apalache	ConstantRank1	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
af5bd03ad4cd6f29b8fdea199b421bfecdc63ef4	Apalache	ConstantRank1	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
84a85c6123da11c1c989d246e94c22da29e6fcfc	Apalache	Instance	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
86f1824bbf2d31f530a4306a79187ad27c7c7e3d	Apalache	Instance	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
2cb2aaa3fcda0e105a4dc38b51e7046bfab2444c	Apalache	InstanceWith	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
39aa868e04d0c76e8f30c237fd1fc649665c0446	Apalache	InstanceWith	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
81cc67f8c4d5d1b9190b966b108587f3a3e0059e	Apalache	InstanceNamed	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
1aaa4ee5fab9e61a91bf9ed30cfa2755497bc062	Apalache	InstanceNamed	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
0926b73218dfd4924a79f8c700d5a00bc74ef306	Apalache	InstanceNamedWith	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
b4b5ed9f45c091d1417c01c04316a0c8e121da90	Apalache	InstanceNamedWith	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
2d54bafbc8e0f1bbca27a6b2d9feb538d99d01e0	Apalache	InstanceInFolder	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
90c8b2833502c8492349e0685ef86ad7887dee84	Apalache	InstanceInFolder	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
4b64a99be6e9a1404aa99cf8f23151c4db85517b	Apalache	InstanceWithInFolder	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
294848b6a47dfa42b2720c474363957badfe39aa	Apalache	InstanceWithInFolder	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
df47369244f3338fa1e0775852324c31077e094c	Apalache	InstanceNamedInFolder	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
6eabd10761fb7ba06a9a38da4cd87e078eaf87f1	Apalache	InstanceNamedInFolder	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
ba321dac148f75167d57fac269c0731f25073aeb	Apalache	InstanceNamedWithInFolder	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
19464527ad7b85fe45eb7d5e56d38bf8e30cb3ae	Apalache	InstanceNamedWithInFolder	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
2af28ccb72f493e69ca3800a5041c18f6bdd4260	Apalache	Lambda	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
02ddfc57ce01c103363a0a1cf063abc4598e1be5	Apalache	Lambda	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
8780140b5517082be0f86dab9cb62fe0027d12db	Apalache	IfThen	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
b978e2514b0aadce49459deed17314287a1ffa0b	Apalache	IfThen	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
02972dc1ae8703adbed855f53c8359a277966ebf	Apalache	IfElse	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
3f5407d2411c36b209e318a303c8b8ceda6cfe1b	Apalache	IfElse	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
32238dc277d8ef11fa08b5cfcb6cf0ca5e2e6f89	Apalache	Domain	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c200f0dbc3836824ee7d5ad79df7ced88740354b	Apalache	Domain	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
aefc3d3ca8b4a0a9e8dda1473532c702474ada1b	Apalache	Unchanged	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
db2a5a8113f292de8ce39804fa06bdb1374b501b	Apalache	Unchanged	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
46afaa02174e3c23301920c941195cf39bd7a4d3	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
aa9ec4ca55866f9c29428a452db86a3bbd4e56cf	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
3ab6e68ce5dbc3642a3d43b5ba91ce144c3f2463	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	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
ab859765ad63d93288c651654cf0f97454bb189c	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	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
2386eb299bc770a6b7ae2919cbecb8a7fc9fa098	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c3e52dcd96bcedb3abd40484b20e8a9483bec403	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
aa2ac3571b45afc09c93493e6799deb0a9769b63	Apalache	BagBagIn	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
5beb3d66e3e293a943b550c33aa2333191bbc6c4	Apalache	BagBagIn	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
87dfd319b5c7b40396e7bddd4c665065e4ae0010	Apalache	BagCopiesIn	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
651f4a6d02ec7619bf8cd271b4232460af61b1c3	Apalache	BagCopiesIn	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
4488cfd857ee1a10619f32dfe51a5837b277650b	Apalache	SeqAppend	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
4ebbacab4dc600c3cddd3bd9c0896d3833dadb94	Apalache	SeqAppend	DefFunRecursive	False	Passed	Model Under Test Equivalent Model

Index

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