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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
2b2536bb5400627376ab53442a7f93b215355727	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFunRecursive	OneLineComment	True	Passed	Model Under Test Equivalent Model
729ae1c3fa35f28d63155bd93d114316104826e5	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFunRecursive	OneLineComment	False	Passed	Model Under Test Equivalent Model
5400d1be0c710744cab4e26e251f7aad63579a0d	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFunRecursive	MultiLineComment	True	Passed	Model Under Test Equivalent Model
fee51566dcbadd511915e80ce881619af12e029a	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	DefFunRecursive	MultiLineComment	False	Passed	Model Under Test Equivalent Model
00b51c2e8e66ddd196dcb177f265d52b94c07ff4	Apalache	DefFunRecursive	BoolTrue	True	Passed	Model Under Test Equivalent Model
93db5840cb55f3e038333fa0ca7c888bae0ff1aa	Apalache	DefFunRecursive	BoolTrue	False	Passed	Model Under Test Equivalent Model
67f24b292f61c0712f740aa1c9d745d59db25f9a	Apalache	DefFunRecursive	BoolFalse	True	Passed	Model Under Test Equivalent Model
e497e648eb76675220f5a5ea0b064cf9ff89c663	Apalache	DefFunRecursive	BoolFalse	False	Passed	Model Under Test Equivalent Model
f579fcad41d826073f074e6c75dc33abd464abb7	Apalache	DefFunRecursive	BoolSet	True	Passed	Model Under Test Equivalent Model
9499c9181d57f08b81f9cfb00897db24ee4ca3f2	Apalache	DefFunRecursive	BoolSet	False	Passed	Model Under Test Equivalent Model
91d87ad69372bef0983472d6a2bc85ca778b08ae	Apalache	DefFunRecursive	And	True	Passed	Model Under Test Equivalent Model
7f23713268ca0e1f460397ffebe0b0bfb5e3243e	Apalache	DefFunRecursive	And	False	Passed	Model Under Test Equivalent Model
4cdc4117680947896e7fc3dd735950d9522cf2ac	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	DefFunRecursive	AndMultiLine	True	Passed	Model Under Test Equivalent Model
bd99bdbc7c582df9388d4eed2edbfd65b85b2427	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	DefFunRecursive	AndMultiLine	False	Passed	Model Under Test Equivalent Model
bc5a1ecfe9a21190a946cc5e12049485e447f0f4	Apalache	DefFunRecursive	Imply	True	Passed	Model Under Test Equivalent Model
8ead7844beb4e824d402c5baca99c51f3e0e789b	Apalache	DefFunRecursive	Imply	False	Passed	Model Under Test Equivalent Model
e3b10ba64b0a3b0b1794bd5411a0ba8e330d787c	Apalache	DefFunRecursive	Not	True	Passed	Model Under Test Equivalent Model
db8684c8df227b7669c94220a58eb4114bd6b664	Apalache	DefFunRecursive	Not	False	Passed	Model Under Test Equivalent Model
046e4ad83fc913a72c8de7a18e3a975543bcf6d2	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	DefFunRecursive	Or	True	Passed	Model Under Test Equivalent Model
f973b85c54e71bfb9d812b92092c38305e93c829	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	DefFunRecursive	Or	False	Passed	Model Under Test Equivalent Model
377adfb3250d7bd3126c4e20aa7867460c6450ca	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	DefFunRecursive	OrMultiLine	True	Passed	Model Under Test Equivalent Model
9bd9082f1dc4bc8f2c9057aa9dcc9695028dd693	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	DefFunRecursive	OrMultiLine	False	Passed	Model Under Test Equivalent Model
525c9b34889a6b60fe205357fb2ddd0bfd735fca	Apalache	DefFunRecursive	Eq	True	Passed	Model Under Test Equivalent Model
3892e7347d198df2792c37605166c00344e46206	Apalache	DefFunRecursive	Eq	False	Passed	Model Under Test Equivalent Model
5ad12480f64b4b86050b84bb53b4760cc0a024ff	Apalache	DefFunRecursive	Ne	True	Passed	Model Under Test Equivalent Model
65323a11b51ff83512ef175ce2a870cc905f81fd	Apalache	DefFunRecursive	Ne	False	Passed	Model Under Test Equivalent Model
280da4d3753ead18c4ab4c27092b117cd0e37e09	Apalache	DefFunRecursive	Let	True	Passed	Model Under Test Equivalent Model
84e03a501d20f691179b6d468a915fded5dac89e	Apalache	DefFunRecursive	Let	False	Passed	Model Under Test Equivalent Model
2cba95ee14bcb7a3003f7a82ce514d5263e44345	Apalache	DefFunRecursive	SetEmpty	True	Passed	Model Under Test Equivalent Model
fc8f0109bd6a08a81fc7eedb41d7c999c2aa7a4a	Apalache	DefFunRecursive	SetEmpty	False	Passed	Model Under Test Equivalent Model
7eda246306da60eea3d3ce7ddf9bf1e5a904e585	Apalache	DefFunRecursive	Set0	True	Passed	Model Under Test Equivalent Model
529ccb927295e8b18e393dffca7c111512f7f28e	Apalache	DefFunRecursive	Set0	False	Passed	Model Under Test Equivalent Model
0b16d9d3f81bdb4fde9534f779ffea79c31ad4cb	Apalache	DefFunRecursive	Set1	True	Passed	Model Under Test Equivalent Model
06e25ed1db5f4126156509c432fa8c7ec8fc1503	Apalache	DefFunRecursive	Set1	False	Passed	Model Under Test Equivalent Model
6037a69a13c8cd5d00a1708d80126853d7bb4958	Apalache	DefFunRecursive	Set2	True	Passed	Model Under Test Equivalent Model
7a221620e089952895fb1b42b40a77db1ccf8d94	Apalache	DefFunRecursive	Set2	False	Passed	Model Under Test Equivalent Model
92de4c69c8bb4f10fbdbab32e76d446e7180452e	Apalache	DefFunRecursive	Fun	True	Passed	Model Under Test Equivalent Model
4ac741d6b56ec2167bf34cd5fc6f7562b3d8697c	Apalache	DefFunRecursive	Fun	False	Passed	Model Under Test Equivalent Model
7aabbd2a2f4dc2b1b7610dbf6c9012b1d372c4de	Apalache	DefFunRecursive	In	True	Passed	Model Under Test Equivalent Model
43d58a61606b246753858acd1bba14cffbd4518f	Apalache	DefFunRecursive	In	False	Passed	Model Under Test Equivalent Model
0e1640ac5788d45e87211a0781d8c6330f061731	Apalache	DefFunRecursive	NotIn	True	Passed	Model Under Test Equivalent Model
e179bc261f1792fe212730f98549a0e01daefa90	Apalache	DefFunRecursive	NotIn	False	Passed	Model Under Test Equivalent Model
5df4c4e3bc1a93dc94c1ecf0d0b9a2af59e375e5	Apalache	DefFunRecursive	Exists	True	Passed	Model Under Test Equivalent Model
a8ed4344e1ac25ea5e2f4f72bdded2b98614efe5	Apalache	DefFunRecursive	Exists	False	Passed	Model Under Test Equivalent Model
1a025312e2cb1d3474d8bd418c6e503d0b15892d	Apalache	DefFunRecursive	Forall	True	Passed	Model Under Test Equivalent Model
84cbc1c8a6fdc5c49d7446cc068229668dbd38eb	Apalache	DefFunRecursive	Forall	False	Passed	Model Under Test Equivalent Model
c5b43577668170539c71765c951cee0cae74e37e	Apalache	DefFunRecursive	Choose	True	Passed	Model Under Test Equivalent Model
aa4565b12138a21d6dfb9b6bcb94b029c91fa955	Apalache	DefFunRecursive	Choose	False	Passed	Model Under Test Equivalent Model
a530cde849db3966af2bcd8b29c6bb43ae666ac9	Apalache	DefFunRecursive	Record	True	Passed	Model Under Test Equivalent Model
bbdd53b6dc1871bc5895947b8c83c48eaba4a2da	Apalache	DefFunRecursive	Record	False	Passed	Model Under Test Equivalent Model
3fab6282753797a311c4e8a65260d14886f6ac42	Apalache	DefFunRecursive	Tuple	True	Passed	Model Under Test Equivalent Model
6c072d17aa7df0705583bd9de7fc172ca2b4612e	Apalache	DefFunRecursive	Tuple	False	Passed	Model Under Test Equivalent Model
e6b9d839bc2f3b2b2092e03f9f82ff7ff23e4837	Apalache	DefFunRecursive	TupleEmpty	True	Passed	Model Under Test Equivalent Model
8988e401be36fb37b932328e362f40faa56a0534	Apalache	DefFunRecursive	TupleEmpty	False	Passed	Model Under Test Equivalent Model
3e7315a992423620a8bd852efb8c1b762f3c4ec3	Apalache	DefFunRecursive	FunApp	True	Passed	Model Under Test Equivalent Model
b1bc2179919ee546bc1e157b92e71fc1bdac6d62	Apalache	DefFunRecursive	FunApp	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
154d496c96a5668677fbffc29d83b8f5e756aaf6	Apalache	DefFunRecursive	NumZero	True	Passed	Model Under Test Equivalent Model
ab77be07f59e761cdb025be66db27407e022c798	Apalache	DefFunRecursive	NumZero	False	Passed	Model Under Test Equivalent Model
a0274b9943bb787d5b9387ac0572b7597a160f77	Apalache	DefFunRecursive	NumOne	True	Passed	Model Under Test Equivalent Model
5330180a27de72ab1a594c7bc2177057866da66d	Apalache	DefFunRecursive	NumOne	False	Passed	Model Under Test Equivalent Model
e747ac181b904e794c6deb9babb29a07e5cdd7aa	Apalache	DefFunRecursive	NumMaxInt	True	Passed	Model Under Test Equivalent Model
91e2522fc086c7d12b9953816fd79943ff258bf5	Apalache	DefFunRecursive	NumMaxInt	False	Passed	Model Under Test Equivalent Model
607d7fcb9475a0269022ad549bd86bf4a628f153	Apalache	DefFunRecursive	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
5769a94ac3a404e55d525407c7a47dc51a2f565c	Apalache	DefFunRecursive	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
6ce32bf136e6d3979b55cefef2e428961b357d80	Apalache	DefFunRecursive	NumPlus	True	Passed	Model Under Test Equivalent Model
9068c4a6c1a5d2e91aee00eed0f0a00fa8def8da	Apalache	DefFunRecursive	NumPlus	False	Passed	Model Under Test Equivalent Model
6f48ee4f696647e7b28dec30e2d0aa0bb40e9685	Apalache	DefFunRecursive	NumMinus	True	Passed	Model Under Test Equivalent Model
8d609f3e119096a2282f858826ed0ac53d5fb280	Apalache	DefFunRecursive	NumMinus	False	Passed	Model Under Test Equivalent Model
48fa8ddadc07124517088b37a3c192bc8339b2ab	Apalache	DefFunRecursive	NumMul	True	Passed	Model Under Test Equivalent Model
e06aa68ef0fd108dddd752822d0d1c65dfaa1f4b	Apalache	DefFunRecursive	NumMul	False	Passed	Model Under Test Equivalent Model
2e169225355048daa632041b29dbbd2a392ebbe0	Apalache	DefFunRecursive	NumDiv	True	Passed	Model Under Test Equivalent Model
c3c1f3feaf64d41d43fd715cb894eee3c5c0b7dc	Apalache	DefFunRecursive	NumDiv	False	Passed	Model Under Test Equivalent Model
0b7afd10f356e5db7f51486945a3b7ef4963bcab	Apalache	DefFunRecursive	NumMod	True	Passed	Model Under Test Equivalent Model
5433c0ad7684a3dd1dddf52bc57afea60696979b	Apalache	DefFunRecursive	NumMod	False	Passed	Model Under Test Equivalent Model
6ca234219dd545ca4b974e7854d07aec4ac782a7	Apalache	DefFunRecursive	NumPow	True	Passed	Model Under Test Equivalent Model
f5ae9b1cb4c760ab68ae638b8b361127153212e7	Apalache	DefFunRecursive	NumPow	False	Passed	Model Under Test Equivalent Model
795b827025ed43555db0289ca883fc1e9d72b718	Apalache	DefFunRecursive	NumGt	True	Passed	Model Under Test Equivalent Model
849c424cda1714422c3ec57ef4cd2701f7a90643	Apalache	DefFunRecursive	NumGt	False	Passed	Model Under Test Equivalent Model
d0fa8910700c07d7ec7aef1d7dad70c214339808	Apalache	DefFunRecursive	NumGe	True	Passed	Model Under Test Equivalent Model
21671f28fcab2750e8c9018ae383f57bdc025c8f	Apalache	DefFunRecursive	NumGe	False	Passed	Model Under Test Equivalent Model
3d9bc0b6fcec7851fce503e644961f735262a89e	Apalache	DefFunRecursive	NumLt	True	Passed	Model Under Test Equivalent Model
632886c136ec945e1140dc9b701a6f81ca926e74	Apalache	DefFunRecursive	NumLt	False	Passed	Model Under Test Equivalent Model
a11be8158969c88a0625cb2fc9611c3e7ffb2629	Apalache	DefFunRecursive	NumLe	True	Passed	Model Under Test Equivalent Model
34361354adeb5e4e45328143024dbe32bf39abbe	Apalache	DefFunRecursive	NumLe	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
ca185d70a38330d0d45444210ab555a9c2a2e3ce	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDefFun	True	Passed	Model Under Test Equivalent Model
4fb714677a69dcf47d4f81d50e4198ac22ca9628	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDefFun	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
6d63fe433e6b5edf15b29a19968e8df508377325	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
c07480399249f5b8fedcb5ed97df70ac3e7ab852	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
7f7fd1120727f04a81091eb1f0fabe46d2c87252	Apalache	DefFunRecursive	Def0	True	Passed	Model Under Test Equivalent Model
9ca893b060539d5210c91086f264f7ec484c5f2d	Apalache	DefFunRecursive	Def0	False	Passed	Model Under Test Equivalent Model
304a4e7e9bc8f6b176ebf8f37a644c8c72e4d882	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef0	True	Passed	Model Under Test Equivalent Model
e8e7b392471478eb75c423e557b72d21cc2ff6ce	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef0	False	Passed	Model Under Test Equivalent Model
17315f2f6d7b8de3e65d8d6d039e62293df7fd23	Apalache	DefFunRecursive	Def1	True	Passed	Model Under Test Equivalent Model
ec2b673eb8e72bf5f050138737a9e6448c587ac1	Apalache	DefFunRecursive	Def1	False	Passed	Model Under Test Equivalent Model
90e03f1911c09c4b313f0efa9e4a7d7ee268a649	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef1	True	Passed	Model Under Test Equivalent Model
de34ed620899af17222ccdff8958b9f615be8157	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef1	False	Passed	Model Under Test Equivalent Model
1cd83a2eec22979a53f62734c65f797017619052	Apalache	DefFunRecursive	Def2	True	Passed	Model Under Test Equivalent Model
1049ebaa785a422f1d9f94c0517d14c394f4c551	Apalache	DefFunRecursive	Def2	False	Passed	Model Under Test Equivalent Model
1ca9b149a862a7e404931310e63677f457625e8a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef2	True	Passed	Model Under Test Equivalent Model
f55bcc34a21fa98d0e35d710ac40f85d189f3b4e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef2	False	Passed	Model Under Test Equivalent Model
259cf02de8d399737b00d33dd88d9ae1e34af234	Apalache	DefFunRecursive	Def1Recursive	True	Passed	Model Under Test Equivalent Model
aacbc8255f2280c323c1f35c548eba2971cdefa7	Apalache	DefFunRecursive	Def1Recursive	False	Passed	Model Under Test Equivalent Model
16c4989d5a68e6729959851a79e03b12ab68ecda	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
01574d5b3d8a55980c037a28c398f1e4731e59a7	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	DefFunRecursive	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
9356704c2c7b3ad8df0baf5cf8b63e94f04d9746	Apalache	DefFunRecursive	Extends	True	Passed	Model Under Test Equivalent Model
19f4f7e2e3fc070c288c4e9313dd3747e1138ef0	Apalache	DefFunRecursive	Extends	False	Passed	Model Under Test Equivalent Model
dcbd0aec5d8c69ac72c9e7a8836632bdc1ba0a3f	Apalache	DefFunRecursive	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
9e0d91338377215e965c47e71d1ed68c13f94819	Apalache	DefFunRecursive	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
35cb992812dfa574307b623bbf0975ad3e70767a	Apalache	DefFunRecursive	Variable	True	Passed	Model Under Test Equivalent Model
8f337a47e591a1698d93aecdfc07efc060dfd35f	Apalache	DefFunRecursive	Variable	False	Passed	Model Under Test Equivalent Model
a3d91f9ce2acacae5103c7ec67bd68708251cdd5	Apalache	DefFunRecursive	Constant	True	Passed	Model Under Test Equivalent Model
c61735051cea90677df17a0307d9bf47540154da	Apalache	DefFunRecursive	Constant	False	Passed	Model Under Test Equivalent Model
86ed9552ae6a26b1bbe7ec6d6b9d8e828fda4b06	Apalache	DefFunRecursive	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
6e03b7a57fd0eee774b3e36739d591ffeb599143	Apalache	DefFunRecursive	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
9952d43287b67b3c7da32cdc9fd60732013d2242	Apalache	DefFunRecursive	ConstantRank1	True	Passed	Model Under Test Equivalent Model
76d88883356026da40eef97c79716dc20db2efe2	Apalache	DefFunRecursive	ConstantRank1	False	Passed	Model Under Test Equivalent Model
27b03bb3e4f6cfae0277566bb603982cb809d0d4	Apalache	DefFunRecursive	Instance	True	Passed	Model Under Test Equivalent Model
d47795e82a40c3798ff34d9dc42e51cdb169efd3	Apalache	DefFunRecursive	Instance	False	Passed	Model Under Test Equivalent Model
46579236289d6f70fe8c8e33eae08b7dda744c54	Apalache	DefFunRecursive	InstanceWith	True	Passed	Model Under Test Equivalent Model
229eb2c3c033f34bc0cf339da6cb6c376fad4924	Apalache	DefFunRecursive	InstanceWith	False	Passed	Model Under Test Equivalent Model
fd6ba117c53593a2f48994e236025025236b8d05	Apalache	DefFunRecursive	InstanceNamed	True	Passed	Model Under Test Equivalent Model
9be42d095475a237850f1b847e74f9860ca08616	Apalache	DefFunRecursive	InstanceNamed	False	Passed	Model Under Test Equivalent Model
bc44b3c39b4444c162ad88b7740fd2045887caf9	Apalache	DefFunRecursive	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
5b0ba5b1f5f74792452662b479592f0e83126e2f	Apalache	DefFunRecursive	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
327e6b437c4baf5979eef9af8f5f8e547e68c957	Apalache	DefFunRecursive	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
621704ecae045678e1bcf83c3939105ed4cb5607	Apalache	DefFunRecursive	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
2059d94c0308d9ad8fe8a1db5a9b3c7c2d9dba20	Apalache	DefFunRecursive	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
8ea42d1ae6ff6c9e75f56b027a5d9bddc80cf760	Apalache	DefFunRecursive	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
19f760bd22fd05bab54394ade779af2207ceedc6	Apalache	DefFunRecursive	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
b5bd2b43ec6a5ca1711722f917f4bd3bb6ea7dfb	Apalache	DefFunRecursive	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
6552501a540f4af8b846f6129f63da962331870f	Apalache	DefFunRecursive	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
781f3ca0440fd257a531ce1bdb396450b4befcf6	Apalache	DefFunRecursive	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
678f157e65b8fec62c5c7b6b313c81b59d9f3086	Apalache	DefFunRecursive	Enabled	True	Passed	Model Under Test Equivalent Model
a2d980858fbaa009da5207d7f364eefda25ff7e9	Apalache	DefFunRecursive	Enabled	False	Passed	Model Under Test Equivalent Model
a5a0b8f6b59bd647ea623d95c209c4a81d09355c	Apalache	DefFunRecursive	Cross2	True	Passed	Model Under Test Equivalent Model
4c08fa1d3a15b3855eb87384099af038b3676503	Apalache	DefFunRecursive	Cross2	False	Passed	Model Under Test Equivalent Model
0be8f8a0ae7a92edcd0f609dfefa1e14f0bebf10	Apalache	DefFunRecursive	Cross3	True	Passed	Model Under Test Equivalent Model
7e2c6057a587a0b397d4eedcb5969140f729909f	Apalache	DefFunRecursive	Cross3	False	Passed	Model Under Test Equivalent Model
c0ed6d0706e68daa8526f9a44b22ffe26ce5a8e7	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	DefFunRecursive	FunSet	True	Passed	Model Under Test Equivalent Model
1d21886ecf441d709e118e02b3a5000427e66aa8	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	DefFunRecursive	FunSet	False	Passed	Model Under Test Equivalent Model
ad18daf77b83987e27f6770ef553bbea5326e869	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	DefFunRecursive	RecordSet	True	Passed	Model Under Test Equivalent Model
eb17fce6b498a3c6dd38242c506416dd24bb4629	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	DefFunRecursive	RecordSet	False	Passed	Model Under Test Equivalent Model
c09626a73f21859d2a3de5edd66cbd3e1c2ad0ee	Apalache	DefFunRecursive	SetDiff	True	Passed	Model Under Test Equivalent Model
db6eb9f1822da81592f4d53a0af710aa6cfce82f	Apalache	DefFunRecursive	SetDiff	False	Passed	Model Under Test Equivalent Model
14c3c42858b349c8773b8f8a4798e88b19513a23	Apalache	DefFunRecursive	SetUnion	True	Passed	Model Under Test Equivalent Model
b43378d8aeecba4c4f6c49c11e7096e0b20606b1	Apalache	DefFunRecursive	SetUnion	False	Passed	Model Under Test Equivalent Model
efe24a66f45ac5191860ee2f4bcd51772d727970	Apalache	DefFunRecursive	SetIntersect	True	Passed	Model Under Test Equivalent Model
c7509ee34609e9c6de2d42a98e3ebf76d707a229	Apalache	DefFunRecursive	SetIntersect	False	Passed	Model Under Test Equivalent Model
fc98a6e17a2c0ef25cbe9c8004881d80af8e7784	Apalache	DefFunRecursive	SubsetEq	True	Passed	Model Under Test Equivalent Model
f72e67d0debd4bcc4f5e0ee2f224400ff9897b79	Apalache	DefFunRecursive	SubsetEq	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
e925e66f2a4c226b99b250998d0b5f47a87838ae	Apalache	DefFunRecursive	IfThen	True	Passed	Model Under Test Equivalent Model
e153cecd33f456ca99b63c755171f3942e34e4df	Apalache	DefFunRecursive	IfThen	False	Passed	Model Under Test Equivalent Model
c6c15954d31430cc99ffa613399cea23ddde0900	Apalache	DefFunRecursive	IfElse	True	Passed	Model Under Test Equivalent Model
f9c711a98f2837dbbbbbf239c53478dfdf66f2b1	Apalache	DefFunRecursive	IfElse	False	Passed	Model Under Test Equivalent Model
e57ef7fce02faac9c8f305df28ac23c07479da32	Apalache	DefFunRecursive	Subset	True	Passed	Model Under Test Equivalent Model
20e03bc9ce7de30f31aa737eb5bbd0b15e712099	Apalache	DefFunRecursive	Subset	False	Passed	Model Under Test Equivalent Model
2066b0b55632f2bf5e66c14be07aba65da7e82d4	Apalache	DefFunRecursive	Domain	True	Passed	Model Under Test Equivalent Model
4f7ae2579572c359283da8f2f3b9e09c6a869f52	Apalache	DefFunRecursive	Domain	False	Passed	Model Under Test Equivalent Model
efd9420374720f39d9dca23a9f990d4df91615c9	Apalache	DefFunRecursive	Union	True	Passed	Model Under Test Equivalent Model
04f2ab9cb330371f68abe80c4863e5bdced9b955	Apalache	DefFunRecursive	Union	False	Passed	Model Under Test Equivalent Model
39e5e7b25dd37f4e16b31df488ba55b42bfb796e	Apalache	DefFunRecursive	Unchanged	True	Passed	Model Under Test Equivalent Model
3916461d707e0a0ccbe80c9abe96e0f84d7c40d9	Apalache	DefFunRecursive	Unchanged	False	Passed	Model Under Test Equivalent Model
4cd4843a8d908e55931bdbef5dc692f0ed23aef6	Apalache	DefFunRecursive	Equivalence	True	Passed	Model Under Test Equivalent Model
19182e8a3dac8c69de1992ee4e19f621666913ef	Apalache	DefFunRecursive	Equivalence	False	Passed	Model Under Test Equivalent Model
32bd07d495e41bfb1e22aab6e05ff03ff74c6987	Apalache	DefFunRecursive	StringEmpty	True	Passed	Model Under Test Equivalent Model
cf6689691ede6f3605047bf546168a26b5be2821	Apalache	DefFunRecursive	StringEmpty	False	Passed	Model Under Test Equivalent Model
41d7a79625f0793c32a22c86e733f4e6ab9a7464	Apalache	DefFunRecursive	String	True	Passed	Model Under Test Equivalent Model
df922ef09231b516cf21a69624060bc237336b22	Apalache	DefFunRecursive	String	False	Passed	Model Under Test Equivalent Model
5886df4aa4f7c245db12a4d93a94d11a5156a78a	Apalache	DefFunRecursive	SeqLen	True	Passed	Model Under Test Equivalent Model
2c97b69b9da7da9ec44aaba0ed2009e60bd5bd80	Apalache	DefFunRecursive	SeqLen	False	Passed	Model Under Test Equivalent Model
4bfb06763b9e90510a5473c00b00a93944bf271b	Apalache	DefFunRecursive	SeqConcat	True	Passed	Model Under Test Equivalent Model
3f22434daf48c78836afa6286778ff2e979b22cd	Apalache	DefFunRecursive	SeqConcat	False	Passed	Model Under Test Equivalent Model
590e96f02a140397a1a1fc973ff2671d02dc2130	Apalache	DefFunRecursive	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
64fb2b98de0ab6cdedbfbc4e7f5cf8f4d27bda5b	Apalache	DefFunRecursive	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
b76c9a588eaee2366b7f0069e455643d5e40eecb	Apalache	DefFunRecursive	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
63e0df2474f6e3acec940bcabda22b737db037c2	Apalache	DefFunRecursive	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
dc3b8aec21ffb91e103a3e972d990c9f6b22a674	TLC with reduction strategy: Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	DefFunRecursive	NumRange	True	Passed	Model Under Test Equivalent Model
21a11165de5db1f7c6947b244b8bc638573beba0	TLC with reduction strategy: Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	DefFunRecursive	NumRange	False	Passed	Model Under Test Equivalent Model
414333f807eb897db44d121c749b48cd42722f6b	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	DefFunRecursive	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
532aeffb96da30c073ed877cfa0b90eae09671cf	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	DefFunRecursive	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
11d8f2d81bdc6666d61fbbe9f43376a458a150f4	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	DefFunRecursive	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
fbc75c9d3fad0f729a6fa3390500e79ec41f3cd1	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	DefFunRecursive	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
40105ffa0d0421d260884b26b0187e830be4bc77	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	DefFunRecursive	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
a4a03dc60eded132cbd5c9bd3ab4327dda8bca0b	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	DefFunRecursive	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
7778c635ad3bde1c921b9e5407f807cb72903e5e	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	DefFunRecursive	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
9351a62ed6cac45c99855bcb8e09303d7e0df221	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	DefFunRecursive	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
48948b226429ac9a1ad4353f62e89eaded1c77f5	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	DefFunRecursive	TlcEval	True	Passed	Model Under Test Equivalent Model
a1d58c00b41812bd5b44f770e3ba243b7c2494ab	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	DefFunRecursive	TlcEval	False	Passed	Model Under Test Equivalent Model
c69223b1e3a66b0fc333586a3b48abd6e2a00219	Apalache	DefFunRecursive	BagBagToSet	True	Passed	Model Under Test Equivalent Model
6f0ddc58754535e4c41f3fc742e813c89f822944	Apalache	DefFunRecursive	BagBagToSet	False	Passed	Model Under Test Equivalent Model
1b377dbd3fb84f97c45fdbe10abef472e76e6e4c	Apalache	DefFunRecursive	BagSetToBag	True	Passed	Model Under Test Equivalent Model
7e7e12c55f15921ffb0b85c9dbe6dd272ffec470	Apalache	DefFunRecursive	BagSetToBag	False	Passed	Model Under Test Equivalent Model
89fc4ad72306bc1c1b06d692be5f2f2daff4c332	Apalache	DefFunRecursive	BagBagIn	True	Passed	Model Under Test Equivalent Model
4c06387edd31f678fa9ea99230a05d7de445821a	Apalache	DefFunRecursive	BagBagIn	False	Passed	Model Under Test Equivalent Model
f42c740c328f4dfabc4fdc48754a3e8b001c2880	Apalache	DefFunRecursive	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
cb1bfdf2058aa32bb4793835605efc24b72abaf9	Apalache	DefFunRecursive	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
5d4eee7ea5ab787fd117bc031c0ee981c1d705d2	Apalache	DefFunRecursive	BagAddBag	True	Passed	Model Under Test Equivalent Model
1a5de9a89bbe60612c3afa1f5e73c7e0c5c7acbb	Apalache	DefFunRecursive	BagAddBag	False	Passed	Model Under Test Equivalent Model
5e58ee712476857d3f142bb8c51625caf28fa32f	Apalache	DefFunRecursive	BagBagSub	True	Passed	Model Under Test Equivalent Model
21a3d840b519942f932adf9d9894ff5f8f34cafb	Apalache	DefFunRecursive	BagBagSub	False	Passed	Model Under Test Equivalent Model
bffa6456f94044090b28db18179e9caba4dc5288	Apalache	DefFunRecursive	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
8c2c34ead88b6ff3a8ced57cf3258ed2ce35648b	Apalache	DefFunRecursive	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
aafa0d5e7e42322188d101f67aa711a40aa1f166	Apalache	DefFunRecursive	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
f907723dd8b7b789e4f2ff7210e0b1d1160d69ab	Apalache	DefFunRecursive	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
e8b9a81642e999105368096acef510d2d4a16594	Apalache	DefFunRecursive	BagBagUnion	True	Passed	Model Under Test Equivalent Model
5d867656d1ff53fd45fd7f91f7906daef7482403	Apalache	DefFunRecursive	BagBagUnion	False	Passed	Model Under Test Equivalent Model
d4062254342a41dead8441eb270a433741f63b69	Apalache	DefFunRecursive	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
328ac07c48722984c6ca0fd30602a7a3f0b83736	Apalache	DefFunRecursive	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
7c6943937e154bb16d6039bbc228351bfbacf170	Apalache	DefFunRecursive	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
2c1048d284f6ae794182cae10a7dc090b81c9770	Apalache	DefFunRecursive	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
fdd60cc56404c5ef5627a40ebd16c513bafd82a5	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	DefFunRecursive	BagSubBag	True	Passed	Model Under Test Equivalent Model
f319811f98c0992462a07e5aaaed152b17b5be27	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	DefFunRecursive	BagSubBag	False	Passed	Model Under Test Equivalent Model
fe9c504702a229a6cd5f8f69ee108062b9d06a38	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	DefFunRecursive	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
148175114adf980967121319d5e64c68aabc26e9	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	DefFunRecursive	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
69d50bd0c4b4643bb198970e764fcf98174af49d	Apalache	DefFunRecursive	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
2ed7df0f07eae5eb1eabc94bb74ae4a6d9750ef2	Apalache	DefFunRecursive	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
559281a89c747a4046b075110b6187830aa59190	Apalache	DefFunRecursive	SeqHead	True	Passed	Model Under Test Equivalent Model
254c6fc88054ce2d8a424d44a0b0a411128f541e	Apalache	DefFunRecursive	SeqHead	False	Passed	Model Under Test Equivalent Model
9c7a34e79059c0c2aa0fa95ab9f7aca42b854949	Apalache	DefFunRecursive	SeqTail	True	Passed	Model Under Test Equivalent Model
5b8da886933cc5091202bc689f086eb52bbacf85	Apalache	DefFunRecursive	SeqTail	False	Passed	Model Under Test Equivalent Model
e2391e501a933b81b6005ef477c8165fa80784d1	Apalache	DefFunRecursive	SeqAppend	True	Passed	Model Under Test Equivalent Model
60d98222e3861036573adae334cca63a25669ea3	Apalache	DefFunRecursive	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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