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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
ff837de03037a26bf8f212b5008abda0745ddb38	Apalache	Eq	DefFun	True	Passed	Model Under Test Equivalent Model
86da3b905b7b6c5d0d8469ece1eda1f44430272d	Apalache	Eq	DefFun	False	Passed	Model Under Test Equivalent Model
4a7602354d41d5a85ef6eb572ae639fae72fbf9e	Apalache	Ne	DefFun	True	Passed	Model Under Test Equivalent Model
44c6f0f0a79fff1b9c5ecbe12962769b6be6ca2a	Apalache	Ne	DefFun	False	Passed	Model Under Test Equivalent Model
36dfd9b662283c3f4f0d53020a6c0c0a37488922	Apalache	Let	DefFun	True	Passed	Model Under Test Equivalent Model
dc7b623fc85abf1b81ff6dcc6f1a22968e5d0827	Apalache	Let	DefFun	False	Passed	Model Under Test Equivalent Model
acd7fd01a0eeb93f14760c2715ae3a974618fa8e	Apalache	Set0	DefFun	True	Passed	Model Under Test Equivalent Model
0c9db84a8c8ba08a575f8ecd448a28124a810a89	Apalache	Set0	DefFun	False	Passed	Model Under Test Equivalent Model
04aa7725e4e5a45e68f99d17ef06d8dda0dd46ae	Apalache	Set1	DefFun	True	Passed	Model Under Test Equivalent Model
6988767a1cdfc3e29775193ccab7cf4a46b93389	Apalache	Set1	DefFun	False	Passed	Model Under Test Equivalent Model
27562ed9b6c4c318425578d52b7f6e77a765a4c4	Apalache	Set2	DefFun	True	Passed	Model Under Test Equivalent Model
6570b3db39156d87685bcce50fb98df19d97b024	Apalache	Set2	DefFun	False	Passed	Model Under Test Equivalent Model
163bb7f4dfb30a1db92ea1f66c3ec826979d0507	Apalache	Fun	DefFun	True	Passed	Model Under Test Equivalent Model
dab478886af8a909b0499ca73b69f42ca5793570	Apalache	Fun	DefFun	False	Passed	Model Under Test Equivalent Model
9442167e794e031754a3491cb34e4d10aeed015c	Apalache	In	DefFun	True	Passed	Model Under Test Equivalent Model
0b7888d030bfe2f04e556b104de0f9e72219aa8e	Apalache	In	DefFun	False	Passed	Model Under Test Equivalent Model
ccfe776210b47174249be7225705802e9a4ccccb	Apalache	NotIn	DefFun	True	Passed	Model Under Test Equivalent Model
a2d33795b2519e05d004c613759e5c5aa8d131fe	Apalache	NotIn	DefFun	False	Passed	Model Under Test Equivalent Model
7256c462ad9a743577d4d62d6a506a5e4171046e	Apalache	Record	DefFun	True	Passed	Model Under Test Equivalent Model
787ec98c3041e2ce885813b836e6f5f9d272fb2a	Apalache	Record	DefFun	False	Passed	Model Under Test Equivalent Model
8876dd208c6e63080d7cd2a12449bf36e7a31054	Apalache	Tuple	DefFun	True	Passed	Model Under Test Equivalent Model
b9ae0ab59a1e6991bb0f2d86cc64df5cdc0cd7eb	Apalache	Tuple	DefFun	False	Passed	Model Under Test Equivalent Model
05ef20e73a72ac5ea7646c466226789dbb28c7f6	Apalache	FunApp	DefFun	True	Passed	Model Under Test Equivalent Model
b6d968d0280ea494d94e8fcdad304224ed4eeca5	Apalache	FunApp	DefFun	False	Passed	Model Under Test Equivalent Model
48cc251ea541814471a163c7cb8f3bc77c07d438	Apalache	Except0	DefFun	True	Passed	Model Under Test Equivalent Model
869fe856886620a59fb4bc3183c7ec18aeed6ed4	Apalache	Except0	DefFun	False	Passed	Model Under Test Equivalent Model
4b9437d54569183987e43acaea4c3132e532b4ac	Apalache	Except1Fun	DefFun	True	Passed	Model Under Test Equivalent Model
2016104c608eb18c9bab0db18bde57860ed230f5	Apalache	Except1Fun	DefFun	False	Passed	Model Under Test Equivalent Model
e208fe2e25bd398db50d6c842d2ade967462fc51	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	DefFun	True	Passed	Model Under Test Equivalent Model
b0b00119863bba34ad3f8dc27ec5075df52f23a0	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	DefFun	False	Passed	Model Under Test Equivalent Model
4fb85e0fe456e1c23fd933f53e089d6e261fe1a9	Apalache	Except1Rec	DefFun	True	Passed	Model Under Test Equivalent Model
69b84655c0fb72545ab4db5f8f9b0c5bb8949e7e	Apalache	Except1Rec	DefFun	False	Passed	Model Under Test Equivalent Model
9644d47d724f57f391278c6ef4d00454dda91db0	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	DefFun	True	Passed	Model Under Test Equivalent Model
4ec0ee90cb4938b5a95bb41c9e6f74c0ca0dee13	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	DefFun	False	Passed	Model Under Test Equivalent Model
dfbd636f891ac0330c64df6440b7802ebcf75caf	Apalache	Except2Fun	DefFun	True	Passed	Model Under Test Equivalent Model
cb4ba33fa627e47ac05e7104994efa7ef1243844	Apalache	Except2Fun	DefFun	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
b10e65556690ff7d16e7ffba97d90cdcb9870196	Apalache	DefFun	DefFun	True	Passed	Model Under Test Equivalent Model
e9cfdcb914d2ecd56fbcf33824e41dd2205f115c	Apalache	DefFun	DefFun	False	Passed	Model Under Test Equivalent Model
67b5861f7bd91b71fdd67d7e2888a79d3bc791c7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	DefFun	True	Passed	Model Under Test Equivalent Model
b7719ba3cc64dc1c743d87d2cf06149882840c4f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	DefFun	False	Passed	Model Under Test Equivalent Model
90efc249aaf5d80d8fa8d93531728bacfd932e8c	Apalache	DefFunRecursive	DefFun	True	Passed	Model Under Test Equivalent Model
6e9694b7db53001bd774409c44caa2064e47a6a3	Apalache	DefFunRecursive	DefFun	False	Passed	Model Under Test Equivalent Model
794fe50f78ba3c5c0b6250bbcd6cfeb4c84aff4f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	DefFun	True	Passed	Model Under Test Equivalent Model
d45e511a076576fd7fad9e9a24d82a53f6e154b8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	DefFun	False	Passed	Model Under Test Equivalent Model
7a2fe59cdb0fcfa0b4872cdef3c461eae7a2825d	Apalache	Def0	DefFun	True	Passed	Model Under Test Equivalent Model
a0afad5dc0e3cdd63611c18509005a94378379b7	Apalache	Def0	DefFun	False	Passed	Model Under Test Equivalent Model
3d296633d38eb2e8a81948154cf6293ddfc81497	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	DefFun	True	Passed	Model Under Test Equivalent Model
0bcf4f721821b263afd5ff04f254a63310ce657a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	DefFun	False	Passed	Model Under Test Equivalent Model
9896c3bfd98371454c1b028fe64d0232d21e963c	Apalache	Def1	DefFun	True	Passed	Model Under Test Equivalent Model
98f86f187368a7603bd5acaa7b714294ab255ef4	Apalache	Def1	DefFun	False	Passed	Model Under Test Equivalent Model
af8b40a5a0a73f26cf4ad6cb6014d36095617bff	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	DefFun	True	Passed	Model Under Test Equivalent Model
dc58cc30d04d54a9706d118ddd8f34cfeb11d8f8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	DefFun	False	Passed	Model Under Test Equivalent Model
8ec0857ab1662591954e732e1a6e76e81800af37	Apalache	Def2	DefFun	True	Passed	Model Under Test Equivalent Model
ad3657825096944a086bc59fce0b84d56516d1d8	Apalache	Def2	DefFun	False	Passed	Model Under Test Equivalent Model
bb40d25c5fe3e632973083e86e542b10ddba95f4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	DefFun	True	Passed	Model Under Test Equivalent Model
17c19e3c58980130644d093df66584949008f5c7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	DefFun	False	Passed	Model Under Test Equivalent Model
629562529fe7ce8ea09e79aaf5e724e8b6de7d3b	Apalache	Def1Recursive	DefFun	True	Passed	Model Under Test Equivalent Model
6f321bfd8d14be49a098e4baa424cf270566e307	Apalache	Def1Recursive	DefFun	False	Passed	Model Under Test Equivalent Model
86468b5c0e17658ce3fef2875bf771ec228275c6	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	DefFun	True	Passed	Model Under Test Equivalent Model
9722036c2480f9143359c16f2669d412243854cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	DefFun	False	Passed	Model Under Test Equivalent Model
c2c58ef63d24336493a3ceee7fc3c6434bcc7181	Apalache	Extends	DefFun	True	Passed	Model Under Test Equivalent Model
1c743de51991559b997a71fcfc8274a3201b17a0	Apalache	Extends	DefFun	False	Passed	Model Under Test Equivalent Model
195d999a805964b27e32939d2a72d44c9da17dcc	Apalache	ExtendsInDifferentFolder	DefFun	True	Passed	Model Under Test Equivalent Model
9c02e1cc9a6c5e9a1d8ebc248b8208d62a7cc253	Apalache	ExtendsInDifferentFolder	DefFun	False	Passed	Model Under Test Equivalent Model
8d7e6329a513afe1797145cd80bb1284a29b2e5a	Apalache	Variable	DefFun	True	Passed	Model Under Test Equivalent Model
340a695b045fc96b0821e6661c8fcff2a6fc42b4	Apalache	Variable	DefFun	False	Passed	Model Under Test Equivalent Model
74cf7d7994cf7db7042ebf1d1e94453a99047589	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	DefFun	True	Passed	Model Under Test Equivalent Model
d02894467b05ba009e998e0935c845ce53c481f3	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	DefFun	False	Passed	Model Under Test Equivalent Model
f726e23748c060e9a32827307094d1100761ea85	Apalache	Constant	DefFun	True	Passed	Model Under Test Equivalent Model
ec6ad61ed65e5a95ba32a8640901318b409fa4ba	Apalache	Constant	DefFun	False	Passed	Model Under Test Equivalent Model
8571f7f40e1a61a5e18f9d8bf906bc0d54334522	Apalache	ConstantRank1	DefFun	True	Passed	Model Under Test Equivalent Model
f5363138cf0314affa30d91b84b322659c1c5c37	Apalache	ConstantRank1	DefFun	False	Passed	Model Under Test Equivalent Model
02aa548dee7398affc5ff682b2f1c3bdaee5bc65	Apalache	Instance	DefFun	True	Passed	Model Under Test Equivalent Model
35c426480a9d884fb4a8041b6babc6cc84ea8180	Apalache	Instance	DefFun	False	Passed	Model Under Test Equivalent Model
fa6dd11b4a89a9f90118a9f9a67398d0e8703a94	Apalache	InstanceWith	DefFun	True	Passed	Model Under Test Equivalent Model
b713c3ccde96a3132609a2869bc87572833e99f2	Apalache	InstanceWith	DefFun	False	Passed	Model Under Test Equivalent Model
2ec23d462d619b853b26fad397068ce3ea81e2d2	Apalache	InstanceNamed	DefFun	True	Passed	Model Under Test Equivalent Model
f058720daf2c7c8c1e36a14e390a8ba42e50c1ce	Apalache	InstanceNamed	DefFun	False	Passed	Model Under Test Equivalent Model
c9eb4669dd1610332805d1e9046b162ec8df7280	Apalache	InstanceNamedWith	DefFun	True	Passed	Model Under Test Equivalent Model
b9086c8573ebb2f8b086502dbd97caedb4d86f99	Apalache	InstanceNamedWith	DefFun	False	Passed	Model Under Test Equivalent Model
438289990fbfbe4f8d55b3eebf52c5641f865a75	Apalache	InstanceInFolder	DefFun	True	Passed	Model Under Test Equivalent Model
964ab89130741b9419999b62c270a9d892d9b38b	Apalache	InstanceInFolder	DefFun	False	Passed	Model Under Test Equivalent Model
7a5ee769a04ff1037c4b060e4925bbdaddae9925	Apalache	InstanceWithInFolder	DefFun	True	Passed	Model Under Test Equivalent Model
aace6649524483d6b1bc72b9615031777b0b9fe5	Apalache	InstanceWithInFolder	DefFun	False	Passed	Model Under Test Equivalent Model
215acdfc66422810e68caff35aa7bb7b353e79ae	Apalache	InstanceNamedInFolder	DefFun	True	Passed	Model Under Test Equivalent Model
e2fdffe57708b37fc5851a4589cbfadcaa7ece11	Apalache	InstanceNamedInFolder	DefFun	False	Passed	Model Under Test Equivalent Model
7a74a712f7a4bf3919813604a484ce87ba3cf4d1	Apalache	InstanceNamedWithInFolder	DefFun	True	Passed	Model Under Test Equivalent Model
114d7c6a63b864ea70091893fe0626345ac21691	Apalache	InstanceNamedWithInFolder	DefFun	False	Passed	Model Under Test Equivalent Model
ecfc7e6190d3defc85533c240473818e6937efa7	Apalache	Lambda	DefFun	True	Passed	Model Under Test Equivalent Model
1314ba482e7acd652918e39adf695faa171094ae	Apalache	Lambda	DefFun	False	Passed	Model Under Test Equivalent Model
03b6c5dc9cadbad48bf76974c586b6c76cb1cce8	Apalache	IfThen	DefFun	True	Passed	Model Under Test Equivalent Model
7c203628a9057b7335dcf9047549f587faed2fe8	Apalache	IfThen	DefFun	False	Passed	Model Under Test Equivalent Model
b7e659eb86d958432178f3aef61f6151043fe9c6	Apalache	IfElse	DefFun	True	Passed	Model Under Test Equivalent Model
13f5ad37431d216e9b91b5836bbc021c4eb052c2	Apalache	IfElse	DefFun	False	Passed	Model Under Test Equivalent Model
5bcf9fafe9a93b4105d0a13936113ea4e1d36e1d	Apalache	Domain	DefFun	True	Passed	Model Under Test Equivalent Model
b2210e178018be3a01dc8f634d269ae97ba3da8a	Apalache	Domain	DefFun	False	Passed	Model Under Test Equivalent Model
fa278160b598e47aa11457b371f951ba782dbb59	Apalache	Unchanged	DefFun	True	Passed	Model Under Test Equivalent Model
d0476ea6622b69055860a7fd7ed49436d4787e64	Apalache	Unchanged	DefFun	False	Passed	Model Under Test Equivalent Model
f2a4b97db6cb993dfe7bc0d9d0638079cf2b53d4	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	DefFun	True	Passed	Model Under Test Equivalent Model
d3eda6f8391d82386a62007e1425ea3ae08e4d9a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	DefFun	False	Passed	Model Under Test Equivalent Model
793a757d454c809c75ff670ba021951109e18fd0	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	DefFun	True	Passed	Model Under Test Equivalent Model
c93d533d00d003841e69660a9eab0355976934d8	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	DefFun	False	Passed	Model Under Test Equivalent Model
4647264e4fae96c9724f33047d1d57945eecd1af	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	DefFun	True	Passed	Model Under Test Equivalent Model
38c8c3004bba7ba85ba127a99ba6a8a560225f7b	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	DefFun	False	Passed	Model Under Test Equivalent Model
daf406dd3186661c733d138c3168787fb2459f7f	Apalache	BagBagIn	DefFun	True	Passed	Model Under Test Equivalent Model
211c9bc8eb8a282ccd1d205ccded06b2d155069b	Apalache	BagBagIn	DefFun	False	Passed	Model Under Test Equivalent Model
88daaaf0d0f6c02befb4d28b8204aeb99b446ae9	Apalache	BagCopiesIn	DefFun	True	Passed	Model Under Test Equivalent Model
c6df6a44c549eea9dba2afeb8aa517a994ad5416	Apalache	BagCopiesIn	DefFun	False	Passed	Model Under Test Equivalent Model
7b538d48d905091dae75540b2e947eb4e8cc60b4	Apalache	SeqAppend	DefFun	True	Passed	Model Under Test Equivalent Model
d79f6c6d9e13f89b4cf98af8d17d26dfb0b83887	Apalache	SeqAppend	DefFun	False	Passed	Model Under Test Equivalent Model

Index

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