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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
6bc89f8c035d41d77f5af9372809c55cdc02bbbe	Apalache	Eq	NumZero	True	Passed	Model Under Test Equivalent Model
99bd7064f26c39cfa4a88aedcbfe768222db6aed	Apalache	Eq	NumZero	False	Passed	Model Under Test Equivalent Model
d1ef23301e83bd53ae53c4591d291d70f10b82fc	Apalache	Ne	NumZero	True	Passed	Model Under Test Equivalent Model
56c5b03431c61c72e70866fb2bbf44dd50d371ae	Apalache	Ne	NumZero	False	Passed	Model Under Test Equivalent Model
2b037cb7c85641e3b76ab1c57fccaf1bbbe5d83c	Apalache	Let	NumZero	True	Passed	Model Under Test Equivalent Model
76734c5c8a2b05ea60b3b6bdce59d8b2051f3809	Apalache	Let	NumZero	False	Passed	Model Under Test Equivalent Model
15ef555f15f184dd49e5092ee825f143fa6aa19e	Apalache	Set0	NumZero	True	Passed	Model Under Test Equivalent Model
9822fa94aa959ece11bc1bcb30711fbdf285283c	Apalache	Set0	NumZero	False	Passed	Model Under Test Equivalent Model
b91affa915a5a392418a5d9cf183472b65fc0691	Apalache	Set1	NumZero	True	Passed	Model Under Test Equivalent Model
9c0f0d295d24e99b21b26a4a1595253b9ef97cc1	Apalache	Set1	NumZero	False	Passed	Model Under Test Equivalent Model
0787a1e9df22d4756a7613c6f916372fd3a8f9f1	Apalache	Set2	NumZero	True	Passed	Model Under Test Equivalent Model
22020b954a5bc196d7ec5cb59f9a1fe81526f461	Apalache	Set2	NumZero	False	Passed	Model Under Test Equivalent Model
c9cd816c7194966800bd396c5d25f7e650157af7	Apalache	Fun	NumZero	True	Passed	Model Under Test Equivalent Model
6a7eddf6de51ef2d4d970cb3ce329a79210f90d5	Apalache	Fun	NumZero	False	Passed	Model Under Test Equivalent Model
1462916011f34236efe0bf2ed5cb48f646f86374	Apalache	In	NumZero	True	Passed	Model Under Test Equivalent Model
834f00399a6239226fd84cc9b12d149edf4ab691	Apalache	In	NumZero	False	Passed	Model Under Test Equivalent Model
317bb4b592c41361c693c4023536a06b96a88df4	Apalache	NotIn	NumZero	True	Passed	Model Under Test Equivalent Model
d2ae2f369ad188c06c88431854ddee6d122daf85	Apalache	NotIn	NumZero	False	Passed	Model Under Test Equivalent Model
2130653de461e84dad1d91a4903081fa234d09a2	Apalache	Record	NumZero	True	Passed	Model Under Test Equivalent Model
ef618bfdcc8a3681c4bbc3f33497c3697795cbce	Apalache	Record	NumZero	False	Passed	Model Under Test Equivalent Model
e6edc8fe554760dd8dbab07ff83a54e3a8435fc8	Apalache	Tuple	NumZero	True	Passed	Model Under Test Equivalent Model
6637e9226e7315f93cb511edf3dbc27cb30f2870	Apalache	Tuple	NumZero	False	Passed	Model Under Test Equivalent Model
736f98e047db9970be2efbbda5b28537dc1a6a18	Apalache	FunApp	NumZero	True	Passed	Model Under Test Equivalent Model
671ff60a83132a0bbba961ead37b8a5e63d84b60	Apalache	FunApp	NumZero	False	Passed	Model Under Test Equivalent Model
04580a52ebcc7599a7f8c96c1d73d32341deafc7	Apalache	Except1Fun	NumZero	True	Passed	Model Under Test Equivalent Model
e4ffb5ff8f93f513ae4f2ee34d6ea35be39842db	Apalache	Except1Fun	NumZero	False	Passed	Model Under Test Equivalent Model
4dcc8795858f41c35b4f5432eabcc5b0a676136c	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumZero	True	Passed	Model Under Test Equivalent Model
84b05b9fd65538756210c7dda0efe3f59e15ec7b	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumZero	False	Passed	Model Under Test Equivalent Model
954c6ed9d0f278d2cf126f6967329e43c71bf6a7	Apalache	Except1Rec	NumZero	True	Passed	Model Under Test Equivalent Model
01f1969d8be22af9dcf614b8a23cc96b99a320c2	Apalache	Except1Rec	NumZero	False	Passed	Model Under Test Equivalent Model
1149feba3b864167581f55dd44b6d84e875a960d	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumZero	True	Passed	Model Under Test Equivalent Model
ce6c83f62d0e87c49f900c54965797023e10d6e6	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumZero	False	Passed	Model Under Test Equivalent Model
fcbb5c2935e8f28d93aece697c190f47ae88f109	Apalache	Except2Fun	NumZero	True	Passed	Model Under Test Equivalent Model
b26e777ee832fb45d139659764d4d39125212989	Apalache	Except2Fun	NumZero	False	Passed	Model Under Test Equivalent Model
731f571c9b539d43c3dbae1001d60d093181d08f	Apalache	Prime	NumZero	True	Passed	Model Under Test Equivalent Model
6c5ef3409de0b1f91b1e0cee6c3341e0d2f75ec3	Apalache	Prime	NumZero	False	Passed	Model Under Test Equivalent Model
2d28236b2843b83996e999d37aca07af2d10c835	Apalache	NumUnaryMinus	NumZero	True	Passed	Model Under Test Equivalent Model
e3bf3e9c4c7cc80c3f618ae29d748f9ced4b6fa8	Apalache	NumUnaryMinus	NumZero	False	Passed	Model Under Test Equivalent Model
3a432d87048cc6e88216cea20da079a7122e25d0	Apalache	NumPlus	NumZero	True	Passed	Model Under Test Equivalent Model
12e4ddc125b7117c7d6d1ff646ad17dda69fe82b	Apalache	NumPlus	NumZero	False	Passed	Model Under Test Equivalent Model
98bc4bd38cc099aacc0a3740e9ea896926baa579	Apalache	NumMinus	NumZero	True	Passed	Model Under Test Equivalent Model
71ff20a747c0233ac7543317a55f5387cdc18145	Apalache	NumMinus	NumZero	False	Passed	Model Under Test Equivalent Model
e36df0fb99ee8e1665460e21bd165180026defd6	Apalache	NumMul	NumZero	True	Passed	Model Under Test Equivalent Model
42785fbe752daf77f0a0dba602d1d891c044e5f3	Apalache	NumMul	NumZero	False	Passed	Model Under Test Equivalent Model
f038b07f3bbefed3f8035fdfbe0eda40fed586cf	Apalache	NumDiv	NumZero	True	Passed	Model Under Test Equivalent Model
731e63204398d6b5a132d1c928d2559572c0b2b3	Apalache	NumDiv	NumZero	False	Passed	Model Under Test Equivalent Model
212bd0286394d4cc94895933c5393b22a97a3fc1	Apalache	NumMod	NumZero	True	Passed	Model Under Test Equivalent Model
8c995354e7f319fd187a0f559af169764f89eb32	Apalache	NumMod	NumZero	False	Passed	Model Under Test Equivalent Model
bb537fb4e59fad75791e4157ba3853200272d43f	Apalache	NumPow	NumZero	True	Passed	Model Under Test Equivalent Model
67e7b5a1d5eab95b17ae77678234f273ac66d382	Apalache	NumPow	NumZero	False	Passed	Model Under Test Equivalent Model
8ef05b1da259fd11ef78ab75e856efc469343ad7	Apalache	NumGt	NumZero	True	Passed	Model Under Test Equivalent Model
84198dd4d859748dbfacfbbf9112d666fd35c3f9	Apalache	NumGt	NumZero	False	Passed	Model Under Test Equivalent Model
91cb91cc692f9e06672ebf8b22cca0dacf648cd7	Apalache	NumGe	NumZero	True	Passed	Model Under Test Equivalent Model
cc1c8347a7f27ed49c59857b3b675376e7285cd5	Apalache	NumGe	NumZero	False	Passed	Model Under Test Equivalent Model
6e2d0d1255b92bae4a06d7be63a5fbcfb1468e36	Apalache	NumLt	NumZero	True	Passed	Model Under Test Equivalent Model
3ec7a8f8a7aee08ada2910d0061cc16e74723509	Apalache	NumLt	NumZero	False	Passed	Model Under Test Equivalent Model
7a2302fa517366e7f2d56d84d5d9b5c747d2e1aa	Apalache	NumLe	NumZero	True	Passed	Model Under Test Equivalent Model
3fe45041a841456d2e7ed9fb76808f0c17da52fd	Apalache	NumLe	NumZero	False	Passed	Model Under Test Equivalent Model
f131342f30596956ba608c8c9ac5ab68b5d4cc13	Apalache	DefFun	NumZero	True	Passed	Model Under Test Equivalent Model
b93db1fd90504974f22e30e6720f8ffcfaab6836	Apalache	DefFun	NumZero	False	Passed	Model Under Test Equivalent Model
9fe1a768eef3e891c642c400e6080b79d2b46dd8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumZero	True	Passed	Model Under Test Equivalent Model
6b34f92659140aa3e96390ebf2eb15a52d059e3d	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumZero	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
01d0557657468abe5ed9e70b54903a5a98c67d5c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumZero	True	Passed	Model Under Test Equivalent Model
7f2fa44ef4e8f58384e3c21bdbb7cbdb7e5e434e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumZero	False	Passed	Model Under Test Equivalent Model
976f35bd73906609314ae2b24b10ae8479ad8d6a	Apalache	Def0	NumZero	True	Passed	Model Under Test Equivalent Model
f35f99719a9daad6fec9aa7f908b0b8c3827b22d	Apalache	Def0	NumZero	False	Passed	Model Under Test Equivalent Model
6c80284b5cb8f6bfda7273b3e41eff31063d777c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumZero	True	Passed	Model Under Test Equivalent Model
18e0d35d98145448e1db563d61d3892646886524	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumZero	False	Passed	Model Under Test Equivalent Model
1f72d0f1ccfc8e5ed0f0b373f560020e46bc51de	Apalache	Def1	NumZero	True	Passed	Model Under Test Equivalent Model
48b7db5835658a46be82bcc1212cd040b98661c1	Apalache	Def1	NumZero	False	Passed	Model Under Test Equivalent Model
033f91da5daab223f44d61be243a6230bd780aa7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumZero	True	Passed	Model Under Test Equivalent Model
51e68c32137b86d415449dd49e473739c0d62064	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumZero	False	Passed	Model Under Test Equivalent Model
1f40f6f4a3a520546dec933e64a5c160d84d0ab8	Apalache	Def2	NumZero	True	Passed	Model Under Test Equivalent Model
7e7b3a11ce41fbb3ff7826bb04b2b2724737e88c	Apalache	Def2	NumZero	False	Passed	Model Under Test Equivalent Model
fb7b24ee9397c31af51ba8afce85e590858f99c8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumZero	True	Passed	Model Under Test Equivalent Model
357220bb135089124ea96aa42cf837bf003438fe	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumZero	False	Passed	Model Under Test Equivalent Model
58b734ae9cba892e4f6c1ec2464462dcf434e03a	Apalache	Def1Recursive	NumZero	True	Passed	Model Under Test Equivalent Model
0537d2675a4d0c411e0701f55db4795139e78121	Apalache	Def1Recursive	NumZero	False	Passed	Model Under Test Equivalent Model
e507ef90b024b2570826f642f9ff01dd5970b3ba	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumZero	True	Passed	Model Under Test Equivalent Model
0febed50cc6a42144e74e78a4962d43a2cde89c9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumZero	False	Passed	Model Under Test Equivalent Model
0c947f6be722e1708a343e9c3bb5aee94203ff23	Apalache	Extends	NumZero	True	Passed	Model Under Test Equivalent Model
c6108499531c5ecf98ba0431e002482ec69b115f	Apalache	Extends	NumZero	False	Passed	Model Under Test Equivalent Model
33b41e2f6673df0cdbb9b3fa87fff62fbe47c316	Apalache	ExtendsInDifferentFolder	NumZero	True	Passed	Model Under Test Equivalent Model
399bc2d4820d9a7ac4439ef84518b3499b742dd1	Apalache	ExtendsInDifferentFolder	NumZero	False	Passed	Model Under Test Equivalent Model
c6cf6d229f864e67e50f65835f8a5ea30cc09987	Apalache	Variable	NumZero	True	Passed	Model Under Test Equivalent Model
75435491c479687d294b0622b5cf73971aa3e192	Apalache	Variable	NumZero	False	Passed	Model Under Test Equivalent Model
607e96899d237d69cfab8d2a7a0693681151b608	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumZero	True	Passed	Model Under Test Equivalent Model
7aeb8a84b22667ae710e31dc217ba5efdda7282b	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumZero	False	Passed	Model Under Test Equivalent Model
9799e0e2d606182132373ff918c002e4b682357d	Apalache	Constant	NumZero	True	Passed	Model Under Test Equivalent Model
0f974caf36d4a01aa9a01efa21384f2da541754a	Apalache	Constant	NumZero	False	Passed	Model Under Test Equivalent Model
2aeed6fb7fd9ec27b5f8e119a50c7b726f779ac9	Apalache	ConstantRank1	NumZero	True	Passed	Model Under Test Equivalent Model
8814b66ed4c88b73c57d51fa5cd22ccba47244c7	Apalache	ConstantRank1	NumZero	False	Passed	Model Under Test Equivalent Model
4d96b3c69db5fa951ebbfc5801713df6f8c84e9b	Apalache	Instance	NumZero	True	Passed	Model Under Test Equivalent Model
58d5eaa9c81eec56e02ae653c6beef5a5dbfa6e0	Apalache	Instance	NumZero	False	Passed	Model Under Test Equivalent Model
a2a7d56e592d5bf0f94d23abe224385618a17fd4	Apalache	InstanceWith	NumZero	True	Passed	Model Under Test Equivalent Model
2e064815ff9c11e927c3b01aa99b4c5569cf5825	Apalache	InstanceWith	NumZero	False	Passed	Model Under Test Equivalent Model
547a5597088be7877a481288d6cb52ccb666d671	Apalache	InstanceNamed	NumZero	True	Passed	Model Under Test Equivalent Model
c6f93f18175a6a0bcd874799c2d295b93cbe2ada	Apalache	InstanceNamed	NumZero	False	Passed	Model Under Test Equivalent Model
4984992df531440f5d71dcefb2b4e99a054a27b8	Apalache	InstanceNamedWith	NumZero	True	Passed	Model Under Test Equivalent Model
a19e64ba23301a430ec5eee3d71e244b027627cb	Apalache	InstanceNamedWith	NumZero	False	Passed	Model Under Test Equivalent Model
74a3954793737d3b2a26892a40f64e0515cadbe1	Apalache	InstanceInFolder	NumZero	True	Passed	Model Under Test Equivalent Model
ba004ebe7afd4e5d0603136e015dcec914c51e84	Apalache	InstanceInFolder	NumZero	False	Passed	Model Under Test Equivalent Model
abdd3ba1d6f848b8fdd59eebf7cf30c2d24c350c	Apalache	InstanceWithInFolder	NumZero	True	Passed	Model Under Test Equivalent Model
10995d57a9ab1e4045e222e71e90b1f69fb97cb8	Apalache	InstanceWithInFolder	NumZero	False	Passed	Model Under Test Equivalent Model
827e00a66dc298dfeecbee4414424fe6eaf7b1ae	Apalache	InstanceNamedInFolder	NumZero	True	Passed	Model Under Test Equivalent Model
5d6504a124b485197e34b24d67b90ccc4fc31f13	Apalache	InstanceNamedInFolder	NumZero	False	Passed	Model Under Test Equivalent Model
d8c2f4d6bc3d3f767731e7dec795384b978011ad	Apalache	InstanceNamedWithInFolder	NumZero	True	Passed	Model Under Test Equivalent Model
99264b402b51d4eb8937603aa4c8ef02c7ea38f5	Apalache	InstanceNamedWithInFolder	NumZero	False	Passed	Model Under Test Equivalent Model
4f037cab30a446cd1af0984c53b748a4cd6d4507	Apalache	Lambda	NumZero	True	Passed	Model Under Test Equivalent Model
b3888c7d7fae718d6e70e51bdc33553dadf24417	Apalache	Lambda	NumZero	False	Passed	Model Under Test Equivalent Model
afe70384e2ddad64a4bd05c1709fc93dfeae7b0a	Apalache	IfThen	NumZero	True	Passed	Model Under Test Equivalent Model
220c015179ff8d0c99042b31f18557d40c7d40ce	Apalache	IfThen	NumZero	False	Passed	Model Under Test Equivalent Model
af6abb23df4da8460a32aaa88f15a9c228d9bc63	Apalache	IfElse	NumZero	True	Passed	Model Under Test Equivalent Model
8c4745a205dd656c1222429f541149ae74e979af	Apalache	IfElse	NumZero	False	Passed	Model Under Test Equivalent Model
d8dbd14e750f63f4c0ef00069bf06116e3e77532	Apalache	Unchanged	NumZero	True	Passed	Model Under Test Equivalent Model
c9ba94cf49ce2fcba0bfb3bcba7132cae3d85655	Apalache	Unchanged	NumZero	False	Passed	Model Under Test Equivalent Model
e482c5a76e7f757e9d4a414b2d9e947d4f9f9d5a	Apalache	SeqSubSeq	NumZero	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
82060af70766c1abbf3b87848db5bee5b514b36c	Apalache	SeqSubSeq	NumZero	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
d8815819943881ab04a39450f9902b6903d53505	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	NumZero	True	Passed	Model Under Test Equivalent Model
79dbf85907fac4a0610401b3a9ee17df07eac628	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	NumZero	False	Passed	Model Under Test Equivalent Model
bc07107b406c9747f56f331a004eec1ff085940c	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumZero	True	Passed	Model Under Test Equivalent Model
33c673ada05527a2ccb7da9711377cc3c285b078	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumZero	False	Passed	Model Under Test Equivalent Model
814458335367b0ae569bb2cdf73648e0cb074a44	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumZero	True	Passed	Model Under Test Equivalent Model
251485109dcc48170b91eef6bbf51d73ac1b91d4	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumZero	False	Passed	Model Under Test Equivalent Model
c0d2daab9b2c47a155f1139ad6f6f321d2e28894	Apalache	BagBagIn	NumZero	True	Passed	Model Under Test Equivalent Model
caaa663acc679582890ab7fd993b04d9dd514aee	Apalache	BagBagIn	NumZero	False	Passed	Model Under Test Equivalent Model
5066eb5f262ed1fd89bdc0f583e920d9f9bb8fa3	Apalache	BagCopiesIn	NumZero	True	Passed	Model Under Test Equivalent Model
a2f2ae232cd328d3cafdb12ee75165ce63936257	Apalache	BagCopiesIn	NumZero	False	Passed	Model Under Test Equivalent Model
925d92730b3d932a62ec1df9037b9ef18421ff0e	Apalache	SeqAppend	NumZero	True	Passed	Model Under Test Equivalent Model
67b272b6583643db63ad7146ce3a64cf765a23bd	Apalache	SeqAppend	NumZero	False	Passed	Model Under Test Equivalent Model

Index

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