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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
191edcca1760ef8804004f0eb30b340244d3ae46	Apalache	And	IfThen	True	Passed	Model Under Test Equivalent Model
1ff89852084c936aa8d3e7f3cde7a86dd3044d38	Apalache	And	IfThen	False	Passed	Model Under Test Equivalent Model
d0825be062af7674d7e6418c65710d917b260505	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	IfThen	True	Passed	Model Under Test Equivalent Model
5bcc82d2f98a53898bf27a1a298b268dda72898b	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	IfThen	False	Passed	Model Under Test Equivalent Model
8f74f4374a30c2e33b2f44dff216370ed0a0a929	Apalache	Imply	IfThen	True	Passed	Model Under Test Equivalent Model
50533942d60f01db240ab50d805673dc59ec2f32	Apalache	Imply	IfThen	False	Passed	Model Under Test Equivalent Model
51bdd4f1aad50d556a846b9dae29630e4c68a79f	Apalache	Not	IfThen	True	Passed	Model Under Test Equivalent Model
d4521746d8ab84aab0bec60f7a77f8ac2c9a5a7e	Apalache	Not	IfThen	False	Passed	Model Under Test Equivalent Model
f405d01b8a5fce7857a9305bccfa6e091d9e5f96	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	IfThen	True	Passed	Model Under Test Equivalent Model
44809be763ddc5f6417b4732cbfa394c59ade7dc	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	IfThen	False	Passed	Model Under Test Equivalent Model
7c2ca8ece82ef0331ff441d40e80ea25a3e2eb06	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	IfThen	True	Passed	Model Under Test Equivalent Model
8aaf652d167237e544db4ce86a1410157b399cf7	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	IfThen	False	Passed	Model Under Test Equivalent Model
60e8b720bb3784fbcb38ca8d654a783650a191cc	Apalache	AndProp	IfThen	True	Passed	Model Under Test Equivalent Model
2dc2cdc264ae197184b710a500749116f8121ac4	Apalache	AndProp	IfThen	False	Passed	Model Under Test Equivalent Model
abca9a517043807e3f682aa3b11028a6ecbfc8eb	Apalache	Boxed	IfThen	True	Passed	Model Under Test Equivalent Model
e7cc64aaeac8d15ed47bd16df9891ef0913a2991	Apalache	Boxed	IfThen	False	Passed	Model Under Test Equivalent Model
36a4bdfc7d26ec3df38af516db24e025abf3eb7c	Apalache	Eq	IfThen	True	Passed	Model Under Test Equivalent Model
a553a350d872bcb4ec149775ad0b6a72df9dcac5	Apalache	Eq	IfThen	False	Passed	Model Under Test Equivalent Model
0aab24710c83dea386f8674c65e19d58da0a4a5d	Apalache	Ne	IfThen	True	Passed	Model Under Test Equivalent Model
5026626e769b782cd25649c42aa898d728f5093b	Apalache	Ne	IfThen	False	Passed	Model Under Test Equivalent Model
6eb47e4baf39bdfcb8366217c9fef57e4de7a70c	Apalache	Let	IfThen	True	Passed	Model Under Test Equivalent Model
20c363dab8b8426d996609b98986b27c092276c3	Apalache	Let	IfThen	False	Passed	Model Under Test Equivalent Model
76bbbe502a970fa526833ec658d12433139f96fd	Apalache	Set0	IfThen	True	Passed	Model Under Test Equivalent Model
1d95054241c9267de36e2dc7cceed7ad1ea9cc1a	Apalache	Set0	IfThen	False	Passed	Model Under Test Equivalent Model
185c3a5838e2d500ab6ac1e907dc664a755a53ed	Apalache	Set1	IfThen	True	Passed	Model Under Test Equivalent Model
1b4e6c3b8084a2497a350aafdfbdebf59e1e57ac	Apalache	Set1	IfThen	False	Passed	Model Under Test Equivalent Model
9a0d1c94dcd4a3e99487ed3ca007793c40095fa0	Apalache	Set2	IfThen	True	Passed	Model Under Test Equivalent Model
053ae7c59342028321822a838c4ddacc649a172c	Apalache	Set2	IfThen	False	Passed	Model Under Test Equivalent Model
3bb07ada436c420fdabdd9f8e675891269549f38	Apalache	Fun	IfThen	True	Passed	Model Under Test Equivalent Model
be5000244f5a67a4c353af77552b473d41082e6e	Apalache	Fun	IfThen	False	Passed	Model Under Test Equivalent Model
3a26a9f26dec697918993c84cc92d241fb0c5122	Apalache	In	IfThen	True	Passed	Model Under Test Equivalent Model
1fb2479b22dbd719a26f9e2189f5823779f139a4	Apalache	In	IfThen	False	Passed	Model Under Test Equivalent Model
c13ed58ade77ff02c9491e011613c342ccc36eb5	Apalache	NotIn	IfThen	True	Passed	Model Under Test Equivalent Model
52dbe711bd66c7eeae1cc2726725426d3d326d33	Apalache	NotIn	IfThen	False	Passed	Model Under Test Equivalent Model
cffcdea3282830f2444ef8822fab1aeb2dc4a525	Apalache	Exists	IfThen	True	Passed	Model Under Test Equivalent Model
e8799b282f9b6b3a88b00c773da59125bfeba06d	Apalache	Exists	IfThen	False	Passed	Model Under Test Equivalent Model
eb8a12607233cf9200d18cc0c877b9a32b3781ec	Apalache	Forall	IfThen	True	Passed	Model Under Test Equivalent Model
cd60f8b06c48fa242728966a5ffa1682e11412c4	Apalache	Forall	IfThen	False	Passed	Model Under Test Equivalent Model
3bfe7ad72549f553b1ce304e92dd055de7fc7a42	Apalache	Choose	IfThen	True	Passed	Model Under Test Equivalent Model
69b2d19d4832ca2664f6111a6d8943d4ae4ea4b6	Apalache	Choose	IfThen	False	Passed	Model Under Test Equivalent Model
e766b024125fb911f9160e24e0dec1bb74e15041	Apalache	Record	IfThen	True	Passed	Model Under Test Equivalent Model
64eb29ffc71f867463b1f82428e4d92b68dcd222	Apalache	Record	IfThen	False	Passed	Model Under Test Equivalent Model
11bfcaf26cdbe36a87b1a1f9467058c182b402ae	Apalache	Tuple	IfThen	True	Passed	Model Under Test Equivalent Model
6cbdccbf733a15752c6987536ffb89c3163a2ab4	Apalache	Tuple	IfThen	False	Passed	Model Under Test Equivalent Model
5c434a376989301b58f0dede3ba2332a473b4069	Apalache	FunApp	IfThen	True	Passed	Model Under Test Equivalent Model
02a29d2832c01b57a58a19d04c35b334c2d3302c	Apalache	FunApp	IfThen	False	Passed	Model Under Test Equivalent Model
847edacf73724f48511d8918e8a696281c250b25	Apalache	Except0	IfThen	True	Passed	Model Under Test Equivalent Model
93b1561b2c6cba2bb659f2f88465bd7066a25a79	Apalache	Except0	IfThen	False	Passed	Model Under Test Equivalent Model
3acd9e02ff3eba70b4c59df01169103ea8c9edcd	Apalache	Except1Fun	IfThen	True	Passed	Model Under Test Equivalent Model
122cba913d2e220c10c0183c8b89b5571c498b57	Apalache	Except1Fun	IfThen	False	Passed	Model Under Test Equivalent Model
6a79bd19a7fd33882598a43c41b011334076737f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	IfThen	True	Passed	Model Under Test Equivalent Model
fe6950f31296351cf2329e20d6d3aeecba8b602f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	IfThen	False	Passed	Model Under Test Equivalent Model
227262dfbdd8f7d0bcd89b57f3b24db40c07eb90	Apalache	Except1Rec	IfThen	True	Passed	Model Under Test Equivalent Model
72657d90d3a4f9ae6291424bc33fc9752406ddd6	Apalache	Except1Rec	IfThen	False	Passed	Model Under Test Equivalent Model
d8ab2649dc05aaa64c76f1b59dfb9b649272263d	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	IfThen	True	Passed	Model Under Test Equivalent Model
4855581a26b9d46397e0b1b04d7730fc32865ecb	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	IfThen	False	Passed	Model Under Test Equivalent Model
21e18939400651c51d7e4f66e2b6b6402b72983f	Apalache	Except2Fun	IfThen	True	Passed	Model Under Test Equivalent Model
c16962b6b5c8c7770500829f1d5d5d5a3f8142de	Apalache	Except2Fun	IfThen	False	Passed	Model Under Test Equivalent Model
0ebe405f5ceaefbb5d6766792fbbf9290d10fbfb	Apalache	Except2FunTuple	IfThen	True	Passed	Model Under Test Equivalent Model
ad09bc13adeb1511627de2b615ca112709c23b78	Apalache	Except2FunTuple	IfThen	False	Passed	Model Under Test Equivalent Model
80411eb5a14807cb14ed33e0ba8b4491d0c19fc1	Apalache	Prime	IfThen	True	Passed	Model Under Test Equivalent Model
cecee3fd3bee9d7932738b5ea96abad38258811b	Apalache	Prime	IfThen	False	Passed	Model Under Test Equivalent Model
4ad89b44d203c0907475ce219796fc6b33fdbd6c	Apalache	NumUnaryMinus	IfThen	True	Passed	Model Under Test Equivalent Model
0cdebd86e0e25c09c5e96d33db9ffcfeba8fc24c	Apalache	NumUnaryMinus	IfThen	False	Passed	Model Under Test Equivalent Model
37ca26561db6905ad01eb7eaa27097f2914493aa	Apalache	NumPlus	IfThen	True	Passed	Model Under Test Equivalent Model
4e5590b7ca5b5f9d576c43286c4c068bb51a6a2e	Apalache	NumPlus	IfThen	False	Passed	Model Under Test Equivalent Model
0860811137b089d064e691a2cfcc535c889b6c25	Apalache	NumMinus	IfThen	True	Passed	Model Under Test Equivalent Model
a65cd5a589dcc4d3bc4ee8a4769f087a3616950a	Apalache	NumMinus	IfThen	False	Passed	Model Under Test Equivalent Model
289b5891e6b34c9a87a4d356ce9f7d2e2a40e857	Apalache	NumMul	IfThen	True	Passed	Model Under Test Equivalent Model
40c7b244537a6294bce199d4e908024916a74ba3	Apalache	NumMul	IfThen	False	Passed	Model Under Test Equivalent Model
b27b28834d901fa027586af060cef2727c35e27c	Apalache	NumDiv	IfThen	True	Passed	Model Under Test Equivalent Model
c794f7ca5d266fbe16f168721bbbea67aaf6094c	Apalache	NumDiv	IfThen	False	Passed	Model Under Test Equivalent Model
69bb7ca96ef28bbc2067c4ef96ddbc7a79f63d18	Apalache	NumMod	IfThen	True	Passed	Model Under Test Equivalent Model
d5ce54211da0baae983aa00f3401cb85e3f8b3f6	Apalache	NumMod	IfThen	False	Passed	Model Under Test Equivalent Model
5d32367afaba4123e2efbf01f5a2e1494c9d814b	Apalache	NumPow	IfThen	True	Passed	Model Under Test Equivalent Model
6e7b63a04a8f618fec920b98bfcff14f42cb9b2d	Apalache	NumPow	IfThen	False	Passed	Model Under Test Equivalent Model
a0def85c7aa5bcce4473296cff11e6a80db72a27	Apalache	NumGt	IfThen	True	Passed	Model Under Test Equivalent Model
698a06b4d6e95486c4cc8523f92ddf38ffd4ed9a	Apalache	NumGt	IfThen	False	Passed	Model Under Test Equivalent Model
2c2da0e4b02ca9d950c46c01db16f254b4374bc0	Apalache	NumGe	IfThen	True	Passed	Model Under Test Equivalent Model
44b3a6d2cbf3b891bcb232ca697b20c631892ae9	Apalache	NumGe	IfThen	False	Passed	Model Under Test Equivalent Model
fe766c40333c46bb5ff9df02f64025fab3b9c01c	Apalache	NumLt	IfThen	True	Passed	Model Under Test Equivalent Model
eefb67e735d2be5e0a9b42740a051b2fa3cef464	Apalache	NumLt	IfThen	False	Passed	Model Under Test Equivalent Model
8585bd703b5cb566febfe100277a82c7f6542482	Apalache	NumLe	IfThen	True	Passed	Model Under Test Equivalent Model
7b2e7b33373074e9cd7c1c9627a7f3967e613c27	Apalache	NumLe	IfThen	False	Passed	Model Under Test Equivalent Model
becf9751cab3640de9f971c7bfa56d2e8b0238b1	Apalache	DefFun	IfThen	True	Passed	Model Under Test Equivalent Model
653923068849a9684d1449d67340d9e7b79bcc34	Apalache	DefFun	IfThen	False	Passed	Model Under Test Equivalent Model
3f72b46535aa86e4bb84b3eecc6cf7a185befbcf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	IfThen	True	Passed	Model Under Test Equivalent Model
09b926d75aa20fa7669d4cf590e34793c518dc50	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	IfThen	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
df1ec8f1fe8aa2f833d85b29c41f384d1c1b8800	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	IfThen	True	Passed	Model Under Test Equivalent Model
0cde363a24f070859b353f99458ad78ce27ccf1e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	IfThen	False	Passed	Model Under Test Equivalent Model
a5f5bd93fe5d60095e6b283403a6762cec1a5537	Apalache	Def0	IfThen	True	Passed	Model Under Test Equivalent Model
ebd6f19b630196dadd992f0976bf267528f372a0	Apalache	Def0	IfThen	False	Passed	Model Under Test Equivalent Model
cf7cbdca40456888b6ceea0d2d920f9a175ec306	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	IfThen	True	Passed	Model Under Test Equivalent Model
8f89234840ac1cdd1aa70524c0bada3a0a3a4be0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	IfThen	False	Passed	Model Under Test Equivalent Model
91eca33a4521d550073970e4977777ac7fa37e0d	Apalache	Def1	IfThen	True	Passed	Model Under Test Equivalent Model
e6337964ec553bd8eebdd124fee3c3e01b154605	Apalache	Def1	IfThen	False	Passed	Model Under Test Equivalent Model
0c3cc313882e349aea2c280809beaafdc19bf302	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	IfThen	True	Passed	Model Under Test Equivalent Model
7318f6c3e8ab91dc3e138b87ffffa4bd5592580c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	IfThen	False	Passed	Model Under Test Equivalent Model
3aa194f654755e3d83ab97ab76ab804a33e74d80	Apalache	Def2	IfThen	True	Passed	Model Under Test Equivalent Model
7cae04d802d9f8920865f06e0ca90d278d8172d6	Apalache	Def2	IfThen	False	Passed	Model Under Test Equivalent Model
c42263c0a7594c14ac43e222e8f694fcb9ada74a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	IfThen	True	Passed	Model Under Test Equivalent Model
8bc02b5a0a677f824d71b05c02ac641127c63d51	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	IfThen	False	Passed	Model Under Test Equivalent Model
32df71760d0d32777e1c1118d40a96a652a70560	Apalache	Def1Recursive	IfThen	True	Passed	Model Under Test Equivalent Model
57c72688c75b5de8d71cbbadafd74cf72e674c2b	Apalache	Def1Recursive	IfThen	False	Passed	Model Under Test Equivalent Model
cf44f25309ad26580ae9c26325e54b38b0cb1c25	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	IfThen	True	Passed	Model Under Test Equivalent Model
8578d611ef5ceb4391fd967fc23619596abcf9bf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	IfThen	False	Passed	Model Under Test Equivalent Model
c7583d3aa82ba816d06d847da04fdf9f4b41aa2b	Apalache	Extends	IfThen	True	Passed	Model Under Test Equivalent Model
2a01d19d962001616465c9456dfc4b91049d4573	Apalache	Extends	IfThen	False	Passed	Model Under Test Equivalent Model
2845019886a9791e3590238bab83eafcb7766d57	Apalache	ExtendsInDifferentFolder	IfThen	True	Passed	Model Under Test Equivalent Model
38b51393f1e3a315ae248ae89f504131492c2b05	Apalache	ExtendsInDifferentFolder	IfThen	False	Passed	Model Under Test Equivalent Model
1ebb22e4a5e73267300e352de4052965b43ebef0	Apalache	Variable	IfThen	True	Passed	Model Under Test Equivalent Model
7bbdb20a1066e67895caad4a557f6df49c98b7b5	Apalache	Variable	IfThen	False	Passed	Model Under Test Equivalent Model
48eea4a423a787fa185cd6c4a93badb36e15f56d	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	IfThen	True	Passed	Model Under Test Equivalent Model
e6775ab5488dd78e3fef68a32d99a433f1483ab8	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	IfThen	False	Passed	Model Under Test Equivalent Model
f813bc2d515bb7b8dbafac2b40aff5004be5eb2d	Apalache	Constant	IfThen	True	Passed	Model Under Test Equivalent Model
85f36be59da6d4e8be046849aa4f7cee1416462a	Apalache	Constant	IfThen	False	Passed	Model Under Test Equivalent Model
5624d05076f56ebbf370a24cfb0709c9c00f5f45	Apalache	ConstantRank1	IfThen	True	Passed	Model Under Test Equivalent Model
b1f9e22786b22190ea389073b82c8c52b217b21b	Apalache	ConstantRank1	IfThen	False	Passed	Model Under Test Equivalent Model
27c1a8532a051417a72f993617136c31117ac9fe	Apalache	Instance	IfThen	True	Passed	Model Under Test Equivalent Model
64bc6ac23bce0bf87b50b0035f07f29a73cf92c5	Apalache	Instance	IfThen	False	Passed	Model Under Test Equivalent Model
3061b2336bf585390c6e5062a0fb0a4422c32c95	Apalache	InstanceWith	IfThen	True	Passed	Model Under Test Equivalent Model
9748fdf97de15b6482edad1a7a2aff17a52d2ee2	Apalache	InstanceWith	IfThen	False	Passed	Model Under Test Equivalent Model
0248470cddb047d0c68f091a5127e8d2bdd84591	Apalache	InstanceNamed	IfThen	True	Passed	Model Under Test Equivalent Model
e5fb010a4a5069a3534d35a21c564d6465c1bc88	Apalache	InstanceNamed	IfThen	False	Passed	Model Under Test Equivalent Model
c1cef71264629776e3c055817394cfb246f2820e	Apalache	InstanceNamedWith	IfThen	True	Passed	Model Under Test Equivalent Model
d018a9105a781ba25e53fbf2a49995d42a224caa	Apalache	InstanceNamedWith	IfThen	False	Passed	Model Under Test Equivalent Model
74f864efc9652263ae1986b1c2fadf92c9457efa	Apalache	InstanceInFolder	IfThen	True	Passed	Model Under Test Equivalent Model
bd517185f7850c8119c0a99c030035b0b1215c3c	Apalache	InstanceInFolder	IfThen	False	Passed	Model Under Test Equivalent Model
cd6dd8d811c90d6e686129efdf26f7fa13d54af5	Apalache	InstanceWithInFolder	IfThen	True	Passed	Model Under Test Equivalent Model
3f6a879eae5165643a7b8d503cb92f614e20e8e7	Apalache	InstanceWithInFolder	IfThen	False	Passed	Model Under Test Equivalent Model
e25b94b9efe8c13ad617514b7332d666ee8bc8b7	Apalache	InstanceNamedInFolder	IfThen	True	Passed	Model Under Test Equivalent Model
93e67e5f0cbfdaf9f199c246daebffeeaf101b4c	Apalache	InstanceNamedInFolder	IfThen	False	Passed	Model Under Test Equivalent Model
a053d1893039c1e6da188758bceaf51125a3f76e	Apalache	InstanceNamedWithInFolder	IfThen	True	Passed	Model Under Test Equivalent Model
f10369d63da8a38d80dca3b3a20c05767edff73f	Apalache	InstanceNamedWithInFolder	IfThen	False	Passed	Model Under Test Equivalent Model
00bf49032c9db14dd81bcae5879d0fa369456722	Apalache	Enabled	IfThen	True	Passed	Model Under Test Equivalent Model
5ac2681ada6d1e6ceb9db2d2d3f41c09cc730d28	Apalache	Enabled	IfThen	False	Passed	Model Under Test Equivalent Model
72cebba49dbc4c733e0799d0239d4b6f5f0c56bb	Apalache	Assume	IfThen	True	Passed	Model Under Test Equivalent Model
ceaa8bda28291e69ac68d2a6b4e1e81cef93cd71	Apalache	Assume	IfThen	False	Passed	Model Under Test Equivalent Model
7302129c8ed12a8c6e22ccf72fcb4d7447fe81e4	Apalache	AssumeNamed	IfThen	True	Passed	Model Under Test Equivalent Model
e41ef845833ad52d553c58b8077bbb88bbc0df5c	Apalache	AssumeNamed	IfThen	False	Passed	Model Under Test Equivalent Model
eea10d4f6ee8cd0589ded205014124380cc11c06	Apalache	Lambda	IfThen	True	Passed	Model Under Test Equivalent Model
669d94e6929ed4d122641457b3989b83f3b759f9	Apalache	Lambda	IfThen	False	Passed	Model Under Test Equivalent Model
a1649550413514bac13d24f81f180a6943ab8a16	Apalache	Cross2	IfThen	True	Passed	Model Under Test Equivalent Model
c30f66efe940b1a3175542db506ca9ee20c40d3b	Apalache	Cross2	IfThen	False	Passed	Model Under Test Equivalent Model
415810ac62b229c81b7630299940df3ab3aa582e	Apalache	Cross3	IfThen	True	Passed	Model Under Test Equivalent Model
01b3d08d469f63a0fcc4653550d3c5461b94a2d4	Apalache	Cross3	IfThen	False	Passed	Model Under Test Equivalent Model
7fba67ba5e2799c4fddc3fd554e37bc494dbf472	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	IfThen	True	Passed	Model Under Test Equivalent Model
9d8c7d0f8c62c9ccaae732d0bd5b1261ff0a849f	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	IfThen	False	Passed	Model Under Test Equivalent Model
cb7314f78446dbbab6c3f29ae2e171d8d93a465e	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	IfThen	True	Passed	Model Under Test Equivalent Model
a51f4495aacee6a17ac9c0553b319bdd54e8b7c7	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	IfThen	False	Passed	Model Under Test Equivalent Model
7f7307d677136e5a5fc7b2470d32f6d4389b97d3	Apalache	SetDiff	IfThen	True	Passed	Model Under Test Equivalent Model
a38d0bd66c26e45af9dfeae13fd255b59e206fca	Apalache	SetDiff	IfThen	False	Passed	Model Under Test Equivalent Model
8db252af25f2685c38ef0d57067e66d464cf009a	Apalache	SetUnion	IfThen	True	Passed	Model Under Test Equivalent Model
de3e3be8620a4acfbdefaee4b941c1662e202301	Apalache	SetUnion	IfThen	False	Passed	Model Under Test Equivalent Model
41439f21d2fe7380eb6f0f1ebd4612655b4db142	Apalache	SetIntersect	IfThen	True	Passed	Model Under Test Equivalent Model
66590ede403043ca7feb3e79de78dd40c684a6ac	Apalache	SetIntersect	IfThen	False	Passed	Model Under Test Equivalent Model
dd5685adf45589f689b7e32ca681c9f44be15061	Apalache	SubsetEq	IfThen	True	Passed	Model Under Test Equivalent Model
189bb0e5114370d39dc509da7dfca8f19ff84679	Apalache	SubsetEq	IfThen	False	Passed	Model Under Test Equivalent Model
988145162afce7e238c0a4cb76cd9e1b93c6e013	Apalache	IfCond	IfThen	True	Passed	Model Under Test Equivalent Model
125dd2aa2ca5c90774e9f522d49cbe720006730b	Apalache	IfCond	IfThen	False	Passed	Model Under Test Equivalent Model
998b9b6228b992aa0455bd192c3623c2e10a8dc6	Apalache	IfThen	IfThen	True	Passed	Model Under Test Equivalent Model
7cc1ac09ab633f4eb4de6281c0da2a924134946a	Apalache	IfThen	IfThen	False	Passed	Model Under Test Equivalent Model
ab23907dd8a405557eaad84ccd42ca9a5f256f70	Apalache	IfElse	IfThen	True	Passed	Model Under Test Equivalent Model
1d2254649cd20a169d8b3fe1dfff114cde0c1bfd	Apalache	IfElse	IfThen	False	Passed	Model Under Test Equivalent Model
2fe44aff93c469f446749fb471c8a15a75d56f04	Apalache	Subset	IfThen	True	Passed	Model Under Test Equivalent Model
940869abe45e882178782319844fb5e11e261030	Apalache	Subset	IfThen	False	Passed	Model Under Test Equivalent Model
6b4b7f392852c2d5b2b9d47a4048197597084e54	Apalache	Domain	IfThen	True	Passed	Model Under Test Equivalent Model
0f11d49e7bef588fb07fd125a711d23750ebaacc	Apalache	Domain	IfThen	False	Passed	Model Under Test Equivalent Model
ae5a4856361897f137f65a0cde0e563d47f01d06	Apalache	Union	IfThen	True	Passed	Model Under Test Equivalent Model
db645a18564ae7c1dd89c12b25bc80f85a5ee353	Apalache	Union	IfThen	False	Passed	Model Under Test Equivalent Model
0794f119f42045b612c5e8f4668e850883bea330	Apalache	Unchanged	IfThen	True	Passed	Model Under Test Equivalent Model
bf98381c4247ea4366786bbb013407f4e6f97f64	Apalache	Unchanged	IfThen	False	Passed	Model Under Test Equivalent Model
32b19f8e9f26f0f0fcad69adac639ec865fac4e4	Apalache	Equivalence	IfThen	True	Passed	Model Under Test Equivalent Model
07c718d4fa2cca6c68d57c562a4d001d08c846de	Apalache	Equivalence	IfThen	False	Passed	Model Under Test Equivalent Model
aafce8f75272524f6d1cde21a4b34ee711382b3f	Apalache	SeqLen	IfThen	True	Passed	Model Under Test Equivalent Model
2d8426e5a230ecb029231b560e5e7ee820b4560d	Apalache	SeqLen	IfThen	False	Passed	Model Under Test Equivalent Model
ff387ad92fe0e872b0979bcc8d53bbd09401972f	Apalache	SeqConcat	IfThen	True	Passed	Model Under Test Equivalent Model
a2877dddb92d722215e94a234b350529f3888586	Apalache	SeqConcat	IfThen	False	Passed	Model Under Test Equivalent Model
3aa9f83955c7f33617d9aa9d0d223f9b13e66720	Apalache	SeqSeq	IfThen	True	Passed	Model Under Test Equivalent Model
7348e351ae6450809d9a7599bc0da4d86495709f	Apalache	SeqSeq	IfThen	False	Passed	Model Under Test Equivalent Model
5e2d35ac41b430887a2d1398ef0b509e6ae8a96a	Apalache	SeqSelectSeq	IfThen	True	Passed	Model Under Test Equivalent Model
baa30c860cb18c8123af3ca7b95aa7a02814e904	Apalache	SeqSelectSeq	IfThen	False	Passed	Model Under Test Equivalent Model
d3c2cfaeeeb2c82150599c240ba89099d3ad029d	Apalache	SeqSubSeq	IfThen	True	Passed	Model Under Test Equivalent Model
ee141f9431588c5e353feb8c292f8a1269c8abbb	Apalache	SeqSubSeq	IfThen	False	Passed	Model Under Test Equivalent Model
ba0cc593d407ddb8e3f972472fc3177534c715b4	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	IfThen	True	Passed	Model Under Test Equivalent Model
3e72542f4cbacc5812b9fba10863a048aa19c0d3	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	IfThen	False	Passed	Model Under Test Equivalent Model
974c1f3db283ae371eafb533326d60b9a4c8f13c	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	IfThen	True	Passed	Model Under Test Equivalent Model
74424c60171bece101939e8b880409920a4702db	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	IfThen	False	Passed	Model Under Test Equivalent Model
db671be30267064b35604e596c41a4affe0d9a87	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	IfThen	True	Passed	Model Under Test Equivalent Model
bba4031779ecf68f589fe631d0cb9f67c643f135	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	IfThen	False	Passed	Model Under Test Equivalent Model
aba620854905b63133e9dd8633a830d3cb19b94a	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	IfThen	True	Passed	Model Under Test Equivalent Model
99a30ec01dde29f5b9a8507185984cb5360c14c2	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	IfThen	False	Passed	Model Under Test Equivalent Model
65c5c7bad8792686d9ba3379d006ac21c2d02ef8	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	IfThen	True	Passed	Model Under Test Equivalent Model
b8ae6bc6c1039022599bca86c83457ce4868aec1	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	IfThen	False	Passed	Model Under Test Equivalent Model
8f8f379084ebd9203ff4c7e3acd4bd4b2001d779	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	IfThen	True	Passed	Model Under Test Equivalent Model
c11c1ccbb612bf41ac6e5df6c06f80498bfe49db	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	IfThen	False	Passed	Model Under Test Equivalent Model
a924f59133a21532cb4d3485a790bf6cb07c86e1	Apalache	BagBagToSet	IfThen	True	Passed	Model Under Test Equivalent Model
c541da2df8641976d83bb11836100947b3992679	Apalache	BagBagToSet	IfThen	False	Passed	Model Under Test Equivalent Model
7d5b9aac7caa7b4b787c17c9a4043124f367723a	Apalache	BagSetToBag	IfThen	True	Passed	Model Under Test Equivalent Model
72048a996b2430560587f8fdf3748646cfda1cf2	Apalache	BagSetToBag	IfThen	False	Passed	Model Under Test Equivalent Model
e6d90164e4b32033c73891417dd463c9220700d6	Apalache	BagBagIn	IfThen	True	Passed	Model Under Test Equivalent Model
22bec79cef5bfb02b5ebad132dde195d7d793b6a	Apalache	BagBagIn	IfThen	False	Passed	Model Under Test Equivalent Model
5301bce8eb359239402c86d0d8000eca699913e7	Apalache	BagAddBag	IfThen	True	Passed	Model Under Test Equivalent Model
f71abcc57aa27b47ce0d17ca289360e53519e4f7	Apalache	BagAddBag	IfThen	False	Passed	Model Under Test Equivalent Model
0ef75add33f92b3a1e59587b32d688b3c95b0c4e	Apalache	BagBagSub	IfThen	True	Passed	Model Under Test Equivalent Model
59dcbfe26f385bd2d8f71312dc33ae8029ea5243	Apalache	BagBagSub	IfThen	False	Passed	Model Under Test Equivalent Model
8214d61640649851eb68d03881f7490635b1b118	Apalache	BagCopiesIn	IfThen	True	Passed	Model Under Test Equivalent Model
a288ecad7d590b7af714c53efea251434c6e9689	Apalache	BagCopiesIn	IfThen	False	Passed	Model Under Test Equivalent Model
a65ec76282cb7fe20ebaab41d9f53ee753c861f4	Apalache	BagSubsetEqBag	IfThen	True	Passed	Model Under Test Equivalent Model
8cda625b52fcae0429ee15b1015659310ee421df	Apalache	BagSubsetEqBag	IfThen	False	Passed	Model Under Test Equivalent Model
20e040c2937ee3966ab4930d1d1b21577851beab	Apalache	BagBagUnion	IfThen	True	Passed	Model Under Test Equivalent Model
5d460eb37cca564beb60dadbb1b658273298326c	Apalache	BagBagUnion	IfThen	False	Passed	Model Under Test Equivalent Model
cd1df6945a83360c8356d275356659c7e9ab36d5	Apalache	BagBagCardinality	IfThen	True	Passed	Model Under Test Equivalent Model
aabac09b24c3579aaa28f8477547f4089b4c54d8	Apalache	BagBagCardinality	IfThen	False	Passed	Model Under Test Equivalent Model
dd4ff2fdb3abe3f411b4a9c16a52e53f75fdb2f0	Apalache	BagBagOfAll	IfThen	True	Passed	Model Under Test Equivalent Model
921b34173389d06d5e25171a2ac0db0f25c97904	Apalache	BagBagOfAll	IfThen	False	Passed	Model Under Test Equivalent Model
7adc13e7f8da22e8b74cdef76934740f65109939	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	IfThen	True	Passed	Model Under Test Equivalent Model
13b01cf0f7b8b513c805f5e058cff6f1d70ca385	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	IfThen	False	Passed	Model Under Test Equivalent Model
23b28627989d704f85a7f76ef6e0bee335fbc673	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	IfThen	True	Passed	Model Under Test Equivalent Model
e4692b6eb3c4bca42bab9dc03de09fe779dd09ed	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	IfThen	False	Passed	Model Under Test Equivalent Model
18f524b764ce85f1c3df9f17d389cabfe5721d27	Apalache	FiniteSetsCardinality	IfThen	True	Passed	Model Under Test Equivalent Model
0eb0cf2d956dbf8e81566a9ede677d0b74cd0b6b	Apalache	FiniteSetsCardinality	IfThen	False	Passed	Model Under Test Equivalent Model
9f9b731f650db07265624b9e8ec439fbb9faee6c	Apalache	SeqHead	IfThen	True	Passed	Model Under Test Equivalent Model
019e651872cbc49131e370e7cea1b77bfb60cb1c	Apalache	SeqHead	IfThen	False	Passed	Model Under Test Equivalent Model
6ba066cbf06f8135eca3592485b9a9813932b796	Apalache	SeqTail	IfThen	True	Passed	Model Under Test Equivalent Model
ed4371afc118d57db855bb7052a2ef11b177420f	Apalache	SeqTail	IfThen	False	Passed	Model Under Test Equivalent Model
e8f23e03577f0d79bbc6fd8d5f397297170d3ab3	Apalache	SeqAppend	IfThen	True	Passed	Model Under Test Equivalent Model
5a872583c9aaf11c0c350cba82e6514fe21d1257	Apalache	SeqAppend	IfThen	False	Passed	Model Under Test Equivalent Model

Index

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