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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
c8eb4b6a4ae416728b2c31cf6fffdf5b6c73930c	Apalache	And	FunApp	True	Passed	Model Under Test Equivalent Model
cc14e5033924706b44e2fc209680c59b1362ad9a	Apalache	And	FunApp	False	Passed	Model Under Test Equivalent Model
3b078d8ba9ca3012b8cf18e24299de44d7b94fe7	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	FunApp	True	Passed	Model Under Test Equivalent Model
deaae78b3e85232f4aa9ba79d1a8fed51e05d139	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	FunApp	False	Passed	Model Under Test Equivalent Model
2beac356ab1631cbebf69a5e374b661f37d01eff	Apalache	Imply	FunApp	True	Passed	Model Under Test Equivalent Model
d928ef064cc04996938fed8308f827f32f64efca	Apalache	Imply	FunApp	False	Passed	Model Under Test Equivalent Model
c6e6ba9cc8b45e000f2bcef68b8963fa71ecb6bb	Apalache	Not	FunApp	True	Passed	Model Under Test Equivalent Model
17b802026ef628c00fc70fa61922186f152d9b45	Apalache	Not	FunApp	False	Passed	Model Under Test Equivalent Model
a271dc27d29ae659a361845f72787f1eee68a87c	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	FunApp	True	Passed	Model Under Test Equivalent Model
89b0d45578fc1860c96ac0fc1d8e0d6b4ab97a04	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	FunApp	False	Passed	Model Under Test Equivalent Model
d094aa46382e2e8b1f4be7a19c5e20b17f65571c	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	FunApp	True	Passed	Model Under Test Equivalent Model
33aca9ff7b1ec74d66c50f18e602114f491b9bf8	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	FunApp	False	Passed	Model Under Test Equivalent Model
68d4ba16ed078ae915d8d650479f2ceb714347d4	Apalache	AndProp	FunApp	True	Passed	Model Under Test Equivalent Model
ba74835a1a078068183ddb5291d259d942ad302a	Apalache	AndProp	FunApp	False	Passed	Model Under Test Equivalent Model
c09e7b8a6b55e00c3fe286a884d6a7ba476ac139	Apalache	Boxed	FunApp	True	Passed	Model Under Test Equivalent Model
9d0983c008e2934a23d43d22dd2a4a89a89c68e3	Apalache	Boxed	FunApp	False	Passed	Model Under Test Equivalent Model
d6bade8a45f80452d15f94be0501a0d23fdfdddc	Apalache	Eq	FunApp	True	Passed	Model Under Test Equivalent Model
431784ed49fca48bef28c80891b0c7cbbcc498bb	Apalache	Eq	FunApp	False	Passed	Model Under Test Equivalent Model
9de6f6043e944227ec5db202ef34e6ef06f2c4d8	Apalache	Ne	FunApp	True	Passed	Model Under Test Equivalent Model
1cfd4cf6aee16fb39c2a4c12f41ae225820a4d8c	Apalache	Ne	FunApp	False	Passed	Model Under Test Equivalent Model
d75d4f484312da2e4d3d65d88c2af3cba1b323a7	Apalache	Let	FunApp	True	Passed	Model Under Test Equivalent Model
f7a56637239b89afe0a7b7b28a294aca64f620ac	Apalache	Let	FunApp	False	Passed	Model Under Test Equivalent Model
e3e4395aec1cfc495133a60b613b93898c5cd965	Apalache	Set0	FunApp	True	Passed	Model Under Test Equivalent Model
c81026f1a282e5f06661838f32b9ca6e69951bcf	Apalache	Set0	FunApp	False	Passed	Model Under Test Equivalent Model
b7112a156649efe74ed2a8bb0a80652cbcde792c	Apalache	Set1	FunApp	True	Passed	Model Under Test Equivalent Model
c5988a2fb21b7c3f69aae5d5ba0b50043bdbe199	Apalache	Set1	FunApp	False	Passed	Model Under Test Equivalent Model
7b4ff9a807b6edf739146496479f1d28edab96ab	Apalache	Set2	FunApp	True	Passed	Model Under Test Equivalent Model
931b7f830096ccd52670e5b89dbb1d3124420e09	Apalache	Set2	FunApp	False	Passed	Model Under Test Equivalent Model
64245786aea3ffbb4474022802d71bcb6a016c0d	Apalache	Fun	FunApp	True	Passed	Model Under Test Equivalent Model
146b7f85ac5e63e4b55ee87e4a8b3b457f7322c4	Apalache	Fun	FunApp	False	Passed	Model Under Test Equivalent Model
b5017e2b23dc4eabdca6ed9bfd2d5932d6ff2327	Apalache	In	FunApp	True	Passed	Model Under Test Equivalent Model
eb2624d37d6ec8b3539f965362fe21b7e03e2c42	Apalache	In	FunApp	False	Passed	Model Under Test Equivalent Model
7f3ef8eae2543873ea1d99546632eea57ccbb110	Apalache	NotIn	FunApp	True	Passed	Model Under Test Equivalent Model
2951045f6c5a1779e228d9a70107cf8d12b68e53	Apalache	NotIn	FunApp	False	Passed	Model Under Test Equivalent Model
1afe202b8279350f0e888eceb1cadbdb80690cf4	Apalache	Exists	FunApp	True	Passed	Model Under Test Equivalent Model
3d9808f9c8b886d0fc71ea37fd4d9695c4f147d9	Apalache	Exists	FunApp	False	Passed	Model Under Test Equivalent Model
257ffa40d61b51c75dadcec9d665d1c87f07c858	Apalache	Forall	FunApp	True	Passed	Model Under Test Equivalent Model
67aee127ee35313d309f7d5fc74f9fa8bab6ffef	Apalache	Forall	FunApp	False	Passed	Model Under Test Equivalent Model
5f7e166c77dc6a3e74fb480b6e119cf58b0e3420	Apalache	Choose	FunApp	True	Passed	Model Under Test Equivalent Model
d5b4ca944a18fe4a68327e76a630f85c4ce0838b	Apalache	Choose	FunApp	False	Passed	Model Under Test Equivalent Model
3a89e1c6f54d52364a6a206ac49eb3a17c58cc0c	Apalache	Record	FunApp	True	Passed	Model Under Test Equivalent Model
18d8809d3e388d5c4c13fac278e0c9a14f9c25cc	Apalache	Record	FunApp	False	Passed	Model Under Test Equivalent Model
a0155333d2e85b9d251af31d65674989009b9196	Apalache	Tuple	FunApp	True	Passed	Model Under Test Equivalent Model
5a99b3df741b170146560c947c208649f16eb956	Apalache	Tuple	FunApp	False	Passed	Model Under Test Equivalent Model
59601f7b08f17e976629808295cd70a7f75a0502	Apalache	FunApp	FunApp	True	Passed	Model Under Test Equivalent Model
24c5e73972831495bea5a070456a0373496d6e0f	Apalache	FunApp	FunApp	False	Passed	Model Under Test Equivalent Model
86fe0ed35a238c5bfbf25555ffee23ba61b41614	Apalache	Except0	FunApp	True	Passed	Model Under Test Equivalent Model
edca9210011f2eabc4038615724698115b515db4	Apalache	Except0	FunApp	False	Passed	Model Under Test Equivalent Model
8bcf8d2e40cd3c08a7b8196b8827ffcdfa873198	Apalache	Except1Fun	FunApp	True	Passed	Model Under Test Equivalent Model
35232392003964841d9b3a4219e9f3ce6a539083	Apalache	Except1Fun	FunApp	False	Passed	Model Under Test Equivalent Model
0230394b8f02c83c09003725042b0d1a87781753	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	FunApp	True	Passed	Model Under Test Equivalent Model
728ec11f801fe3194f99781e5ea666a64662a8d1	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	FunApp	False	Passed	Model Under Test Equivalent Model
4a04820fa02a60cedf65f02c0f68c597ec1e2b20	Apalache	Except1Rec	FunApp	True	Passed	Model Under Test Equivalent Model
81617e59678ac0ef84d67598c22dc5dcfd73cb0a	Apalache	Except1Rec	FunApp	False	Passed	Model Under Test Equivalent Model
0d86c41cc570be91822501075cb0acb7956b8842	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	FunApp	True	Passed	Model Under Test Equivalent Model
edf93fdcd1e43ed1ccc2a5218b1cc1388905fa7c	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	FunApp	False	Passed	Model Under Test Equivalent Model
ef1c7ef93bc7d143e99ba4d007e3ef42333cf0a0	Apalache	Except2Fun	FunApp	True	Passed	Model Under Test Equivalent Model
5769f6de4ee36e32098e7ec0f0367a1a8dd09f93	Apalache	Except2Fun	FunApp	False	Passed	Model Under Test Equivalent Model
8a929cd4d1e6eee662af912019a348a5610b5256	Apalache	Except2FunTuple	FunApp	True	Passed	Model Under Test Equivalent Model
40b0289af3c0b1c7a9ca25d040d1a0433690f86a	Apalache	Except2FunTuple	FunApp	False	Passed	Model Under Test Equivalent Model
b83c84bf2b6236a7c98fbaa9a3d35376cc2b44d4	Apalache	Prime	FunApp	True	Passed	Model Under Test Equivalent Model
618b1a5b58ac8b0227968f15105080bb21083176	Apalache	Prime	FunApp	False	Passed	Model Under Test Equivalent Model
72ce7d919e1c50d98bd417af17e3ba35b6af5949	Apalache	NumUnaryMinus	FunApp	True	Passed	Model Under Test Equivalent Model
d28e4ed94f4b6c7967075ac9ded598a0d57c4057	Apalache	NumUnaryMinus	FunApp	False	Passed	Model Under Test Equivalent Model
8bab4baa6098053ed6ee390490a6cdbc4450d7f3	Apalache	NumPlus	FunApp	True	Passed	Model Under Test Equivalent Model
3f34d00430f4518b73720877c3b02056b7b89f52	Apalache	NumPlus	FunApp	False	Passed	Model Under Test Equivalent Model
ff633f99178f89f73bae17fa93dbb0b0c5ce6887	Apalache	NumMinus	FunApp	True	Passed	Model Under Test Equivalent Model
f8d3fc4edfb2c4c811d1fe490c3ab6d21ad0e73c	Apalache	NumMinus	FunApp	False	Passed	Model Under Test Equivalent Model
9f9b03e9a735d37d524f60e5daa6acd41153a2fe	Apalache	NumMul	FunApp	True	Passed	Model Under Test Equivalent Model
540c4e6401b9dc41775ccd9426a03815f9173502	Apalache	NumMul	FunApp	False	Passed	Model Under Test Equivalent Model
9f6d048e5bceb75acc0e4d97b141de194ac763c5	Apalache	NumDiv	FunApp	True	Passed	Model Under Test Equivalent Model
1cfda8c959a81902cbee921d6722767aa688ff09	Apalache	NumDiv	FunApp	False	Passed	Model Under Test Equivalent Model
4601ab57aacd7c6614a8dccb2f5f2c6ce3a5aabe	Apalache	NumMod	FunApp	True	Passed	Model Under Test Equivalent Model
bc345174118b6d8f5226ccd7e1458d546e8595dc	Apalache	NumMod	FunApp	False	Passed	Model Under Test Equivalent Model
4a8c62c338abb2fd4634ba8404d0330aad37df7b	Apalache	NumPow	FunApp	True	Passed	Model Under Test Equivalent Model
ff80e41e5e05f9bb9056ed6bef0c21051859db0c	Apalache	NumPow	FunApp	False	Passed	Model Under Test Equivalent Model
d31ba9b574abab71c8056e4344e549a51632eb0f	Apalache	NumGt	FunApp	True	Passed	Model Under Test Equivalent Model
e5fb607fd0960f53056a31e8a4f1c375e16bbd41	Apalache	NumGt	FunApp	False	Passed	Model Under Test Equivalent Model
4dbd1fcae8b653a16686da95b6272597981a6480	Apalache	NumGe	FunApp	True	Passed	Model Under Test Equivalent Model
fef0de07550b8533bfb87309ecc6868f1c915e56	Apalache	NumGe	FunApp	False	Passed	Model Under Test Equivalent Model
2c675d0f32721e6dae9caf2cb5106714a4d1f162	Apalache	NumLt	FunApp	True	Passed	Model Under Test Equivalent Model
95f5f89d7fd2cd5dff1d53442db46ab80f2351c9	Apalache	NumLt	FunApp	False	Passed	Model Under Test Equivalent Model
4b5a47a65d344d105b9c04c112c4d3372e616890	Apalache	NumLe	FunApp	True	Passed	Model Under Test Equivalent Model
93c4f9ae8ba91977ecaa8c571cbaab9a35c29ade	Apalache	NumLe	FunApp	False	Passed	Model Under Test Equivalent Model
823ab31ad4e2e7a1b475452dcba1927581c56aa1	Apalache	DefFun	FunApp	True	Passed	Model Under Test Equivalent Model
36f489eab67c1a4f9ae630db78a7d1da1ea81e63	Apalache	DefFun	FunApp	False	Passed	Model Under Test Equivalent Model
554a52588a2cb65e72260b4fa4e547faaf04843d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	FunApp	True	Passed	Model Under Test Equivalent Model
d7ebc22fe5587c379de453b2b621d370b2848a66	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	FunApp	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
f55f22b22a673f7fe25bf93f148224af808f006e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	FunApp	True	Passed	Model Under Test Equivalent Model
ec46b7577f7dddf9735e2d6cdded8f280c51b53f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	FunApp	False	Passed	Model Under Test Equivalent Model
5b77d086dfb866aca7379c43d7e5164bc0c66bb1	Apalache	Def0	FunApp	True	Passed	Model Under Test Equivalent Model
faabc0be7fc4de0d30a5e564bc3db099e60d6026	Apalache	Def0	FunApp	False	Passed	Model Under Test Equivalent Model
45826a23aae893d4615f6fe74ef600d6118a5820	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	FunApp	True	Passed	Model Under Test Equivalent Model
9ac299359336c8651641f268228a23f063e870b4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	FunApp	False	Passed	Model Under Test Equivalent Model
64c6d0c61889ab297ad6087a6b99c45551a49140	Apalache	Def1	FunApp	True	Passed	Model Under Test Equivalent Model
f2ff4ced1bc3454ee9bde30fe0b92bbe3f32522e	Apalache	Def1	FunApp	False	Passed	Model Under Test Equivalent Model
1bbf8ed3327362487cbe044624fe9050992b5c7b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	FunApp	True	Passed	Model Under Test Equivalent Model
89e33cc6fdf3c8d8a72aafe991ddd7d8106d1f03	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	FunApp	False	Passed	Model Under Test Equivalent Model
c19975da39e34f7b3588eb2125ab2a45a24146f3	Apalache	Def2	FunApp	True	Passed	Model Under Test Equivalent Model
ce222959d11e319a65228d6aecb20f19814a9e45	Apalache	Def2	FunApp	False	Passed	Model Under Test Equivalent Model
c899c492a028973f24bdb55b2e142d8065790578	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	FunApp	True	Passed	Model Under Test Equivalent Model
0d92f3cd35ba1f305291d36bb2501b1cb5aacdaf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	FunApp	False	Passed	Model Under Test Equivalent Model
dd975a35b914f809a30c9c9dc363290719227a95	Apalache	Def1Recursive	FunApp	True	Passed	Model Under Test Equivalent Model
5beb04191d177ee547b9529dc81502c883b38b32	Apalache	Def1Recursive	FunApp	False	Passed	Model Under Test Equivalent Model
7d427b6f4e7587a3a2534381e016ba222f1734ac	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	FunApp	True	Passed	Model Under Test Equivalent Model
7eef74d9bda63b2ae416625acd217527600421a3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	FunApp	False	Passed	Model Under Test Equivalent Model
288ce0d50a32933e81ad223741072f472a0f958a	Apalache	Extends	FunApp	True	Passed	Model Under Test Equivalent Model
2110d7bb699f3b7ec75d82d76dec6bca70165444	Apalache	Extends	FunApp	False	Passed	Model Under Test Equivalent Model
b39d7d406b3b51b3a67403df8ccda29ade0fe540	Apalache	ExtendsInDifferentFolder	FunApp	True	Passed	Model Under Test Equivalent Model
390afb91e260510de5fabbfd255faa7fc8a04ad6	Apalache	ExtendsInDifferentFolder	FunApp	False	Passed	Model Under Test Equivalent Model
d0c5814f1f71b8891417363f929c869a0945cfed	Apalache	Variable	FunApp	True	Passed	Model Under Test Equivalent Model
c45aa20ae6e8a9d79f115e76d90924401b663502	Apalache	Variable	FunApp	False	Passed	Model Under Test Equivalent Model
8c9c79e59d7faa6da50fe801ea0b2a8acedffb3b	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	FunApp	True	Passed	Model Under Test Equivalent Model
56baf1f66c452bdcc2221f517e8ee7a23dabbb75	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	FunApp	False	Passed	Model Under Test Equivalent Model
8638b27ed04a1d7c223dc426ca92b21a4130bd6a	Apalache	Constant	FunApp	True	Passed	Model Under Test Equivalent Model
21067629af377f84c64dd04e827e81ae2588bd09	Apalache	Constant	FunApp	False	Passed	Model Under Test Equivalent Model
4b75764c20ae5159dbfaa69837e77a84f26911dd	Apalache	ConstantRank1	FunApp	True	Passed	Model Under Test Equivalent Model
ef9377292acc5d253a71f7d64ef3bf93178e7c8e	Apalache	ConstantRank1	FunApp	False	Passed	Model Under Test Equivalent Model
eaff91da5e11b5c8de104da3b4880b66d481f226	Apalache	Instance	FunApp	True	Passed	Model Under Test Equivalent Model
ffcde4ecaf0d200e0e6650490ad8b9d7438b04af	Apalache	Instance	FunApp	False	Passed	Model Under Test Equivalent Model
1d0512e93678c1e25d5d23cb7ec850f40c91300e	Apalache	InstanceWith	FunApp	True	Passed	Model Under Test Equivalent Model
ce18e80eb80a2004ba684907b757d6398eb96ac8	Apalache	InstanceWith	FunApp	False	Passed	Model Under Test Equivalent Model
20c9382428b4070e89fb1a47ce7e1edfec247a8b	Apalache	InstanceNamed	FunApp	True	Passed	Model Under Test Equivalent Model
94cd6add36c7a22f2f337c12b9192ee5f5b3dbf4	Apalache	InstanceNamed	FunApp	False	Passed	Model Under Test Equivalent Model
c57f4b77031d05d2c0fb3772ecd2be017097ca7c	Apalache	InstanceNamedWith	FunApp	True	Passed	Model Under Test Equivalent Model
209db169dafa30e228c61c32ac503829e10ff61c	Apalache	InstanceNamedWith	FunApp	False	Passed	Model Under Test Equivalent Model
04eef732ca3ff126c030f21ec67d03170b253960	Apalache	InstanceInFolder	FunApp	True	Passed	Model Under Test Equivalent Model
c2e58424e8d152d735c6989f53fbd40a028978a2	Apalache	InstanceInFolder	FunApp	False	Passed	Model Under Test Equivalent Model
e735aecad907abce60044e6a051c46f3ff8e5eaa	Apalache	InstanceWithInFolder	FunApp	True	Passed	Model Under Test Equivalent Model
c0dd5e3634db13824cf1cd1e3f6b557cc246f33c	Apalache	InstanceWithInFolder	FunApp	False	Passed	Model Under Test Equivalent Model
a816a8137d11b4e92bea9cdfc897730d42b350f3	Apalache	InstanceNamedInFolder	FunApp	True	Passed	Model Under Test Equivalent Model
05e2b7b5ee2dca6f641a9e4eb558d6e3da3ab9d0	Apalache	InstanceNamedInFolder	FunApp	False	Passed	Model Under Test Equivalent Model
a5029fd9355272b0931f650568c5050022576eef	Apalache	InstanceNamedWithInFolder	FunApp	True	Passed	Model Under Test Equivalent Model
cc147fa56c0d290f2cfe8e343732f8c396cbc653	Apalache	InstanceNamedWithInFolder	FunApp	False	Passed	Model Under Test Equivalent Model
d860b9838009d08e00a4f786bf315d75c6729874	Apalache	Enabled	FunApp	True	Passed	Model Under Test Equivalent Model
18297d8e53a5b775d1ec919c7915392d73380937	Apalache	Enabled	FunApp	False	Passed	Model Under Test Equivalent Model
5bcc00b89787c3fe878e67d2898bdbc850db657c	Apalache	Assume	FunApp	True	Passed	Model Under Test Equivalent Model
22821b66d469783b5f9e59603976b212fe2abcdb	Apalache	Assume	FunApp	False	Passed	Model Under Test Equivalent Model
c41814cda2ff58ac1f000b0b27fa24d88f5ec46a	Apalache	AssumeNamed	FunApp	True	Passed	Model Under Test Equivalent Model
041a1bcc54aca37da3cc4c81ddf22b513dd4eb21	Apalache	AssumeNamed	FunApp	False	Passed	Model Under Test Equivalent Model
b1f0968dd4ef50f6a1cf115d9c56af374d1b0b50	Apalache	Lambda	FunApp	True	Passed	Model Under Test Equivalent Model
f9ab8fb3290e9453e641cadb92e78c8e8177f56b	Apalache	Lambda	FunApp	False	Passed	Model Under Test Equivalent Model
fdfa418691a20e5c656af2925596b20e5cdce8f0	Apalache	Cross2	FunApp	True	Passed	Model Under Test Equivalent Model
82129ce4035cab735eb5ed5bdd53eba66a6f6e62	Apalache	Cross2	FunApp	False	Passed	Model Under Test Equivalent Model
e12f3d0e069b2349d89456f10f5d181cf436b723	Apalache	Cross3	FunApp	True	Passed	Model Under Test Equivalent Model
373ee57578f9dbee487b9129afa62a4b01a7a00c	Apalache	Cross3	FunApp	False	Passed	Model Under Test Equivalent Model
8a538005b64639745d5f0eda5f4fb2d2f536b3b5	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	FunApp	True	Passed	Model Under Test Equivalent Model
a2bdece0b4b6e939cc7a258e0eb0377109437f1d	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	FunApp	False	Passed	Model Under Test Equivalent Model
4e53c6742c600569b9342d373d22f3f4cd3d9c02	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	FunApp	True	Passed	Model Under Test Equivalent Model
e31c1b88b4a9c49c083446176c79ee40cd0b5f60	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	FunApp	False	Passed	Model Under Test Equivalent Model
379aa8f13a9aa6f3f2edd4efb2b70d8de007df51	Apalache	SetDiff	FunApp	True	Passed	Model Under Test Equivalent Model
47d5ab33a19e8d82e6f69220c7c7b2cce8b2c03e	Apalache	SetDiff	FunApp	False	Passed	Model Under Test Equivalent Model
2334b461227c5033cfa96043f5c3480bf12947e5	Apalache	SetUnion	FunApp	True	Passed	Model Under Test Equivalent Model
878e6246a2793dcc6f39a39a443cca1eebe52406	Apalache	SetUnion	FunApp	False	Passed	Model Under Test Equivalent Model
3bda1ba1ac3aa738b34fbbaf8339432f8a2e79d6	Apalache	SetIntersect	FunApp	True	Passed	Model Under Test Equivalent Model
2845245673c9d45b794ade2935c53697d6f296cd	Apalache	SetIntersect	FunApp	False	Passed	Model Under Test Equivalent Model
d77a7fd0a37a947ea3971429251c2ec5898c6d60	Apalache	SubsetEq	FunApp	True	Passed	Model Under Test Equivalent Model
2bce7e58419c27b80304836a633e0781f00f02b6	Apalache	SubsetEq	FunApp	False	Passed	Model Under Test Equivalent Model
acdeb4dfe1a94d7e9585a83fb87273222bfa1e5d	Apalache	IfCond	FunApp	True	Passed	Model Under Test Equivalent Model
f783886a101a14537297d7230d04c8395d296be7	Apalache	IfCond	FunApp	False	Passed	Model Under Test Equivalent Model
a65d058a75557f37b20b1248befb98ea90b04035	Apalache	IfThen	FunApp	True	Passed	Model Under Test Equivalent Model
b8aededf6a3a52a2121bc057c0a24d9369735106	Apalache	IfThen	FunApp	False	Passed	Model Under Test Equivalent Model
1e7c2f09a55503d3845ba876ad917dcdec175ebb	Apalache	IfElse	FunApp	True	Passed	Model Under Test Equivalent Model
8fd35c0f435dd5688e1aeedcc61bdd986bf6262b	Apalache	IfElse	FunApp	False	Passed	Model Under Test Equivalent Model
d0936637cbcefebd5ebeb809d18e89ede242e431	Apalache	Subset	FunApp	True	Passed	Model Under Test Equivalent Model
a2de11ccda1c91256262683343a34602e349dd63	Apalache	Subset	FunApp	False	Passed	Model Under Test Equivalent Model
2b78423e2bfe6f581cda515f9951cfec1ef565db	Apalache	Domain	FunApp	True	Passed	Model Under Test Equivalent Model
5086daa513c9bef3509fb6e6f389aa4ee9a60d98	Apalache	Domain	FunApp	False	Passed	Model Under Test Equivalent Model
a79139f9adbab2fd4a9ab9439274fb3730d6b639	Apalache	Union	FunApp	True	Passed	Model Under Test Equivalent Model
84044592f93191b589b9bd01fd6a67f6a2549dfa	Apalache	Union	FunApp	False	Passed	Model Under Test Equivalent Model
1614c9eb8dd255a743c7b103504fcd7d5bdf71e2	Apalache	Unchanged	FunApp	True	Passed	Model Under Test Equivalent Model
731b346250042a577830d007f2652c3d3e2e8539	Apalache	Unchanged	FunApp	False	Passed	Model Under Test Equivalent Model
f1487128ab2e1f4a7d3f84d25645eb2a0022cfde	Apalache	Equivalence	FunApp	True	Passed	Model Under Test Equivalent Model
5e1051133f0a4c8e61551168bb3a4e2597b5eb57	Apalache	Equivalence	FunApp	False	Passed	Model Under Test Equivalent Model
0121151b97e7d8fdbad378e76411ea05af876205	Apalache	SeqLen	FunApp	True	Passed	Model Under Test Equivalent Model
b45fabb14491b1ce522272dab28b8b16078a2eab	Apalache	SeqLen	FunApp	False	Passed	Model Under Test Equivalent Model
bdc7443e61cadaf366e4c5f45d639365a701337f	Apalache	SeqConcat	FunApp	True	Passed	Model Under Test Equivalent Model
2e484f42d8b8188ce72cfefc8a9d1e34e7904d27	Apalache	SeqConcat	FunApp	False	Passed	Model Under Test Equivalent Model
77f4ab894d81ad331b09e0294b6c9b18513a9558	Apalache	SeqSeq	FunApp	True	Passed	Model Under Test Equivalent Model
99dcf86c0aff4b7d6b0cb1a6393ba6cbd2713677	Apalache	SeqSeq	FunApp	False	Passed	Model Under Test Equivalent Model
24aa86637a74c5cb90d46bd597e32eac04c77c95	Apalache	SeqSelectSeq	FunApp	True	Passed	Model Under Test Equivalent Model
fd444ebe62f0c49c2f8447407655191cd4ad1be0	Apalache	SeqSelectSeq	FunApp	False	Passed	Model Under Test Equivalent Model
1ed5b3da6d2d149d6755d064826b322541a10192	Apalache	SeqSubSeq	FunApp	True	Passed	Model Under Test Equivalent Model
90959f858809186b8b95d65774dc90fe5e8034ef	Apalache	SeqSubSeq	FunApp	False	Passed	Model Under Test Equivalent Model
0ddf01d76eb4ba6121495ae875cd13aa875e4b87	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	FunApp	True	Passed	Model Under Test Equivalent Model
398c89b0fe89f1cac6dedbe45b0159c84ce9614d	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	FunApp	False	Passed	Model Under Test Equivalent Model
37035be2293f5a3e47d48d221a2a40f24fd77609	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	FunApp	True	Passed	Model Under Test Equivalent Model
bbb168686f7273460df767f7c67a4484e374b452	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	FunApp	False	Passed	Model Under Test Equivalent Model
884bc6926eab116cb4a542b67085c4617f96a5bc	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	FunApp	True	Passed	Model Under Test Equivalent Model
4c85a3e7be3ab3ee7a64e9acc01eaff6ca3779c7	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	FunApp	False	Passed	Model Under Test Equivalent Model
c577d052dc08e84aff43fe6741f212bdf3c60447	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	FunApp	True	Passed	Model Under Test Equivalent Model
e18f3384c1014c2fc4f1c9950001300c8a070861	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	FunApp	False	Passed	Model Under Test Equivalent Model
c910307e4edb67dea697b2cccd84ab8a3f2d7d87	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	FunApp	True	Passed	Model Under Test Equivalent Model
e74804270deb5c49d2dfefb1d7cca31d17a377ed	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	FunApp	False	Passed	Model Under Test Equivalent Model
825209bb144690adf846e9ce2206cb9b59329e38	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	FunApp	True	Passed	Model Under Test Equivalent Model
52f4d985da8ad334d8cb3f59e0d96d0f662e39f4	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	FunApp	False	Passed	Model Under Test Equivalent Model
3106ec571d436d8e6711bd1587620998706caf28	Apalache	BagBagToSet	FunApp	True	Passed	Model Under Test Equivalent Model
7a1e26defba44155b7ae32cf1835f0519bccc2a4	Apalache	BagBagToSet	FunApp	False	Passed	Model Under Test Equivalent Model
63aa7c3b28ff4b79c154ab8d7bcd2bc1bc5277d7	Apalache	BagSetToBag	FunApp	True	Passed	Model Under Test Equivalent Model
52cdfc4c21ee2e286265b16a960c9358fe84afbe	Apalache	BagSetToBag	FunApp	False	Passed	Model Under Test Equivalent Model
2daffb1b933b69ed250dc989d8b5e6f28a430334	Apalache	BagBagIn	FunApp	True	Passed	Model Under Test Equivalent Model
75b8eaaac068a75f78e200de325043cd4d4c990c	Apalache	BagBagIn	FunApp	False	Passed	Model Under Test Equivalent Model
c086cbf2ec63b0e1fc9dba0f0a1295581aeb1b60	Apalache	BagAddBag	FunApp	True	Passed	Model Under Test Equivalent Model
c9cf81e95496fa146c9917063262e52e94b26fa3	Apalache	BagAddBag	FunApp	False	Passed	Model Under Test Equivalent Model
461959f5a9c61407e45c86b0ee978df494fa5333	Apalache	BagBagSub	FunApp	True	Passed	Model Under Test Equivalent Model
5430459ee2687c0cecf71420c1089f126e2351fe	Apalache	BagBagSub	FunApp	False	Passed	Model Under Test Equivalent Model
c527780735c501397962aeea1099213bd005c679	Apalache	BagCopiesIn	FunApp	True	Passed	Model Under Test Equivalent Model
132c3cc01502f7f9d2daf955967181e22012b655	Apalache	BagCopiesIn	FunApp	False	Passed	Model Under Test Equivalent Model
99fd89fbb9033dfd95690e00bc94e0d83c23320c	Apalache	BagSubsetEqBag	FunApp	True	Passed	Model Under Test Equivalent Model
9d4cd06dd44589676a40a4741b3013fd96826146	Apalache	BagSubsetEqBag	FunApp	False	Passed	Model Under Test Equivalent Model
ca29cc94ebc293d94c6bee44862f61627dd3cbb9	Apalache	BagBagUnion	FunApp	True	Passed	Model Under Test Equivalent Model
3a8dcd1054088c6030b151749f34d01c49d7b83f	Apalache	BagBagUnion	FunApp	False	Passed	Model Under Test Equivalent Model
345adcd94c4128f3757138a6b3cb392d0675b86c	Apalache	BagBagCardinality	FunApp	True	Passed	Model Under Test Equivalent Model
2c8196e264c0e81ba09266ed4caeb54875bd5674	Apalache	BagBagCardinality	FunApp	False	Passed	Model Under Test Equivalent Model
def7dda91d500256ef537b463471e65669348af8	Apalache	BagBagOfAll	FunApp	True	Passed	Model Under Test Equivalent Model
644ec63f5aa2bf8bdd70ed22875700bec0222690	Apalache	BagBagOfAll	FunApp	False	Passed	Model Under Test Equivalent Model
34f3b4446852c406a62f3f0742bd043bfcde7486	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	FunApp	True	Passed	Model Under Test Equivalent Model
6bb2c1830c5f5dd419c4da79d8a56e5dbb8360e8	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	FunApp	False	Passed	Model Under Test Equivalent Model
0fe06d0d0975eb64eb1181d7c5af492e57b453ed	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	FunApp	True	Passed	Model Under Test Equivalent Model
b2edbd7ffa504c52fb573d52c4707cad807d3b7b	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	FunApp	False	Passed	Model Under Test Equivalent Model
4383172109379fff727555eea72c6090df62385e	Apalache	FiniteSetsCardinality	FunApp	True	Passed	Model Under Test Equivalent Model
38e8fff75cd8009ad5dd2754e324591c18a49b27	Apalache	FiniteSetsCardinality	FunApp	False	Passed	Model Under Test Equivalent Model
1f99f4330840e72d380adea6072f0bea17dc0e11	Apalache	SeqHead	FunApp	True	Passed	Model Under Test Equivalent Model
9b4f3daaeec7064f41ceed4bfc3ec388904b431f	Apalache	SeqHead	FunApp	False	Passed	Model Under Test Equivalent Model
9f236c2cdfc3f61718dd9a83223065b2ab3998e8	Apalache	SeqTail	FunApp	True	Passed	Model Under Test Equivalent Model
453969ff0097c6115f554d24437b4766129da1c4	Apalache	SeqTail	FunApp	False	Passed	Model Under Test Equivalent Model
c99aaf97a4af299b3048a49875271f6ab749fc92	Apalache	SeqAppend	FunApp	True	Passed	Model Under Test Equivalent Model
50e1a313ba783a27967dc405c4e8923936ac99b2	Apalache	SeqAppend	FunApp	False	Passed	Model Under Test Equivalent Model

Index

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