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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
6ec3b5255a459eb1cbed2afbfb2339fdc716d930	Apalache	Eq	NumMod	True	Passed	Model Under Test Equivalent Model
4debe9e5f9c105128cb4f01513ba5f9540481e41	Apalache	Eq	NumMod	False	Passed	Model Under Test Equivalent Model
84eef8ad07ebbd4491f9e19e72f6bfa8736a4fc0	Apalache	Ne	NumMod	True	Passed	Model Under Test Equivalent Model
f85228084018c3b2f0395252cc5d1c9d6ab64479	Apalache	Ne	NumMod	False	Passed	Model Under Test Equivalent Model
2abdb626b5324ea278c80541f0da7d6d3b799fc1	Apalache	Let	NumMod	True	Passed	Model Under Test Equivalent Model
c3b59277785b3b7ec46f2b77f23088904326c04e	Apalache	Let	NumMod	False	Passed	Model Under Test Equivalent Model
c753825e8e4c09965cbdffa9847d8e88950a3810	Apalache	Set0	NumMod	True	Passed	Model Under Test Equivalent Model
d299417aa9b51c984b50bea2e3b4984eb61f4851	Apalache	Set0	NumMod	False	Passed	Model Under Test Equivalent Model
d135c8a059728460eba81c397e5d626a76f052fe	Apalache	Set1	NumMod	True	Passed	Model Under Test Equivalent Model
c3ab31f6cc67358d870ffaac401dea32ff607e26	Apalache	Set1	NumMod	False	Passed	Model Under Test Equivalent Model
70505a99daafbedb99c4d4dc6343c6eb65f8d82b	Apalache	Set2	NumMod	True	Passed	Model Under Test Equivalent Model
e4e216f6dee7f1b4adb12e9cb60c839ac967ef7c	Apalache	Set2	NumMod	False	Passed	Model Under Test Equivalent Model
47f15c81e11e192780a2f51f13fa3c66753ff05c	Apalache	Fun	NumMod	True	Passed	Model Under Test Equivalent Model
9aed9abb2363bc464271f526c7422b486d3455e9	Apalache	Fun	NumMod	False	Passed	Model Under Test Equivalent Model
56db03d47381a773b5fa786c09e4f187881ae171	Apalache	In	NumMod	True	Passed	Model Under Test Equivalent Model
e7896b91fee50954a8bac385b99c178a7fe82f89	Apalache	In	NumMod	False	Passed	Model Under Test Equivalent Model
8c37e3bd3fb24afd0d41288b7d17ca6a62351a7e	Apalache	NotIn	NumMod	True	Passed	Model Under Test Equivalent Model
e545f64212be3a3bbd3107a0f0b71297b024d11f	Apalache	NotIn	NumMod	False	Passed	Model Under Test Equivalent Model
dbf97a6e4363cfa1c9fceecaad8bb7235c8e18d7	Apalache	Record	NumMod	True	Passed	Model Under Test Equivalent Model
66081fffbea2e9e7427f64820eb2294aa50df84a	Apalache	Record	NumMod	False	Passed	Model Under Test Equivalent Model
c8acbc3bfe9b478b5055eacfed4f86fcab658f3e	Apalache	Tuple	NumMod	True	Passed	Model Under Test Equivalent Model
75e5789253948a7a8405d957690d38178bfb4b6d	Apalache	Tuple	NumMod	False	Passed	Model Under Test Equivalent Model
c62f83c3c0ce3a9628fb7856dbaa565947514213	Apalache	FunApp	NumMod	True	Passed	Model Under Test Equivalent Model
7d6798068a73feb099f7b3d3d1af296d78dca3c1	Apalache	FunApp	NumMod	False	Passed	Model Under Test Equivalent Model
9034a60883d209ed0e2db6f71601f22306879363	Apalache	Except1Fun	NumMod	True	Passed	Model Under Test Equivalent Model
a0f97be00d37534c6d92b64507b8b0842854fc78	Apalache	Except1Fun	NumMod	False	Passed	Model Under Test Equivalent Model
162bd91319d244bb9e322b0575b57216dcf1f3a4	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumMod	True	Passed	Model Under Test Equivalent Model
f476f66fdec05b46fa0bba195fdcfaa55fcb161f	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	NumMod	False	Passed	Model Under Test Equivalent Model
06e78fe7da78f9a2a74d845b9b18c564922c8d3b	Apalache	Except1Rec	NumMod	True	Passed	Model Under Test Equivalent Model
784af1d79308b2226fdf89eb5ca6c29c7e8095ba	Apalache	Except1Rec	NumMod	False	Passed	Model Under Test Equivalent Model
338fb26d526ae4579f461eb7d1c99f783bc21ced	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumMod	True	Passed	Model Under Test Equivalent Model
de78b0cd7e7cf386dcf372c7031be919e09d8c53	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	NumMod	False	Passed	Model Under Test Equivalent Model
3f6f705395b9b7c9c8da4c3796d869fabec70d21	Apalache	Except2Fun	NumMod	True	Passed	Model Under Test Equivalent Model
021bc6f26c169d63d432cd774d1c34f985f9d5cc	Apalache	Except2Fun	NumMod	False	Passed	Model Under Test Equivalent Model
b0ff955af455971075e6ad7f91ea430566ebe373	Apalache	Prime	NumMod	True	Passed	Model Under Test Equivalent Model
085c0a3edb3fe1f33ec4e5006448a800c6ae0467	Apalache	Prime	NumMod	False	Passed	Model Under Test Equivalent Model
114417685a2540404c857cf1e98f4c91e6f47806	Apalache	NumUnaryMinus	NumMod	True	Passed	Model Under Test Equivalent Model
bc0cf3041355495fa024ea2b2637fc7a71c99441	Apalache	NumUnaryMinus	NumMod	False	Passed	Model Under Test Equivalent Model
2936633a108f12b4b1c21cecf85b5562df993cfa	Apalache	NumPlus	NumMod	True	Passed	Model Under Test Equivalent Model
6e9f850bbbb24b873c5cbacb19f094467521fa19	Apalache	NumPlus	NumMod	False	Passed	Model Under Test Equivalent Model
fe59afb13e4c09b08ffd22ea5ac8b792d8ed09ec	Apalache	NumMinus	NumMod	True	Passed	Model Under Test Equivalent Model
a1e943cc0fa46072d90bebcc40d831eb9e639ddb	Apalache	NumMinus	NumMod	False	Passed	Model Under Test Equivalent Model
e71d5c5ac535b7d5527d22a387e369c2cc40384b	Apalache	NumMul	NumMod	True	Passed	Model Under Test Equivalent Model
7818e64f96167f77784d1a17a53d87f56ee3ca68	Apalache	NumMul	NumMod	False	Passed	Model Under Test Equivalent Model
2179eecb49a6a65a5e0532d1db65da362c1bc9e7	Apalache	NumDiv	NumMod	True	Passed	Model Under Test Equivalent Model
4f3df857e988abc59e0bc0cf2319f2e514943676	Apalache	NumDiv	NumMod	False	Passed	Model Under Test Equivalent Model
30e8f9164c05577cf38e667043d894fada5d762f	Apalache	NumMod	NumMod	True	Passed	Model Under Test Equivalent Model
d7b7ff84e2ecdaecefb6d39384b3ca99f2989f2a	Apalache	NumMod	NumMod	False	Passed	Model Under Test Equivalent Model
d6ea8ad92179dc99310e0a882a1b98a0e7a7318a	Apalache	NumPow	NumMod	True	Passed	Model Under Test Equivalent Model
3e8d4f7a83addf47614666197d0d0a42fed7072d	Apalache	NumPow	NumMod	False	Passed	Model Under Test Equivalent Model
5e95be6dfd57fd2665a077f0add299f6075e36b1	Apalache	NumGt	NumMod	True	Passed	Model Under Test Equivalent Model
47f1b43315d1ec065745d94437152ff5eaf0d2d4	Apalache	NumGt	NumMod	False	Passed	Model Under Test Equivalent Model
d70c5e8b3179e51f1dc3b3245f1e1ba4aa3fddf2	Apalache	NumGe	NumMod	True	Passed	Model Under Test Equivalent Model
9397af8a03b6f64df1057a8e9acc76ebc5e150ad	Apalache	NumGe	NumMod	False	Passed	Model Under Test Equivalent Model
5f58265c64b514ce660a795b905191cf3e91f31f	Apalache	NumLt	NumMod	True	Passed	Model Under Test Equivalent Model
5b016d6bafe4e392ca8d71b5d870d46243a2fd56	Apalache	NumLt	NumMod	False	Passed	Model Under Test Equivalent Model
57e1331391a47006a0ca0cbb4cf897cfda1860af	Apalache	NumLe	NumMod	True	Passed	Model Under Test Equivalent Model
9c93c8432b677d6e29539267ca0dd95680789c12	Apalache	NumLe	NumMod	False	Passed	Model Under Test Equivalent Model
1df72a62a1d7749cd85418186a764da717fbfb3d	Apalache	DefFun	NumMod	True	Passed	Model Under Test Equivalent Model
cb37779c0d2bd90feb0d9d5c7338f252aabb9054	Apalache	DefFun	NumMod	False	Passed	Model Under Test Equivalent Model
b28c1c2bcaa36ff60a8ecbd7b649bea61f1796d5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumMod	True	Passed	Model Under Test Equivalent Model
7dc34878a0ba86919eb6dd4c71c8aa4e90f4c1a3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	NumMod	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
0b48240428d0dbd4bd9d008b542907312ec1ab01	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumMod	True	Passed	Model Under Test Equivalent Model
a45e1d1b3627c8b5f466997eb426e66fe4883cd8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	NumMod	False	Passed	Model Under Test Equivalent Model
fddb3942509265fe17c86b3115622851cdde349e	Apalache	Def0	NumMod	True	Passed	Model Under Test Equivalent Model
18f37534edb750f74d9a01ac1ff6b940b96cdc73	Apalache	Def0	NumMod	False	Passed	Model Under Test Equivalent Model
ed4cdc938a75c3f29c14c5584c7d31e43c7e6a20	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumMod	True	Passed	Model Under Test Equivalent Model
97c4d41931c08688c2f49fad5208bfd6cfa655dd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	NumMod	False	Passed	Model Under Test Equivalent Model
791d4e601c0f6fb539ad194c33727b53e7d8906a	Apalache	Def1	NumMod	True	Passed	Model Under Test Equivalent Model
8e0c15f24724787e15a63638a6bcb8ad85efbdcf	Apalache	Def1	NumMod	False	Passed	Model Under Test Equivalent Model
7a92081fd430c43bed4bf94f618a7d3d890872a5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumMod	True	Passed	Model Under Test Equivalent Model
a70b5430ba8acbf7a5dc6d5080e58d855bf71858	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	NumMod	False	Passed	Model Under Test Equivalent Model
af6efdec00336a2dd8a87a43a3981c6ed86e6608	Apalache	Def2	NumMod	True	Passed	Model Under Test Equivalent Model
9c38ae4ddf1fc093b701a5e55b660c98244cc397	Apalache	Def2	NumMod	False	Passed	Model Under Test Equivalent Model
00156b14409d2472b63948829cb7d2d8542df988	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumMod	True	Passed	Model Under Test Equivalent Model
acf56084a7b2195881dc4e02baf0c1b5d60aa719	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	NumMod	False	Passed	Model Under Test Equivalent Model
658cd73baef25e62a026c904e85b632f66e0a442	Apalache	Def1Recursive	NumMod	True	Passed	Model Under Test Equivalent Model
4678eeb68bea9397a56794da21b4d1867a29c6ae	Apalache	Def1Recursive	NumMod	False	Passed	Model Under Test Equivalent Model
192233088a514a668d607af0480b65622911e9f8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumMod	True	Passed	Model Under Test Equivalent Model
36249ac6528232baf913df8bbe99354625c738ba	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	NumMod	False	Passed	Model Under Test Equivalent Model
5f2b2e25d45d94da39b9022d72a6ef56db86abe0	Apalache	Extends	NumMod	True	Passed	Model Under Test Equivalent Model
ab576775ef08c270045b9c9982ae01c346eda7ce	Apalache	Extends	NumMod	False	Passed	Model Under Test Equivalent Model
7f7949f0fcd6e641419a5de55caf186b06a3f917	Apalache	ExtendsInDifferentFolder	NumMod	True	Passed	Model Under Test Equivalent Model
6e1cf4e02cd8933380fa91bc2c84e802b6bbf979	Apalache	ExtendsInDifferentFolder	NumMod	False	Passed	Model Under Test Equivalent Model
6a3dd472327c5b22cc9ba8987b124bf6b211c0cb	Apalache	Variable	NumMod	True	Passed	Model Under Test Equivalent Model
e2068398f6655c7c8e297be5f17fcaec3f33fb91	Apalache	Variable	NumMod	False	Passed	Model Under Test Equivalent Model
1b074f2bf7a1e02d8bf0c4de2e73ce1e32002c13	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumMod	True	Passed	Model Under Test Equivalent Model
efc8f4edb59993cde7cb820ea6e08d715b4e2bb2	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	NumMod	False	Passed	Model Under Test Equivalent Model
d5a2f0c7ef67961bb464fa5274481c91b140ebbb	Apalache	Constant	NumMod	True	Passed	Model Under Test Equivalent Model
e71a26ede4925a0b51c02a7305a15f86f46ea57e	Apalache	Constant	NumMod	False	Passed	Model Under Test Equivalent Model
32202bfa7b25cfcb3f8ef223a40e99f2eaf6a8af	Apalache	ConstantRank1	NumMod	True	Passed	Model Under Test Equivalent Model
b273a27a24f09aa9ca13954d0511383c9c9bfa8b	Apalache	ConstantRank1	NumMod	False	Passed	Model Under Test Equivalent Model
083c5944592858a7f22ab8790da670070ea8607a	Apalache	Instance	NumMod	True	Passed	Model Under Test Equivalent Model
edb7a251cbe88eb88a9ac0a6c887ec12d59546da	Apalache	Instance	NumMod	False	Passed	Model Under Test Equivalent Model
4d8793a24301661e647c26fef6763fec3f7b8e6c	Apalache	InstanceWith	NumMod	True	Passed	Model Under Test Equivalent Model
6e06b514b5c188a6a756ff3c2bc2c16225f8f5f1	Apalache	InstanceWith	NumMod	False	Passed	Model Under Test Equivalent Model
82e26df716225a56382b67926b3e0278d21adca1	Apalache	InstanceNamed	NumMod	True	Passed	Model Under Test Equivalent Model
74bdced51d13baf8d63352d2d2472a1f93ab1ef9	Apalache	InstanceNamed	NumMod	False	Passed	Model Under Test Equivalent Model
58b45ae15d96a4b67d1417bb3a845bf748258501	Apalache	InstanceNamedWith	NumMod	True	Passed	Model Under Test Equivalent Model
b4488815dc9060a05c493332fc2485220f5cc735	Apalache	InstanceNamedWith	NumMod	False	Passed	Model Under Test Equivalent Model
728e7a0287a66275a12fb0027d9f74f9c055ad41	Apalache	InstanceInFolder	NumMod	True	Passed	Model Under Test Equivalent Model
40ac3004e17668f64f62791fad82ce5f39fc8295	Apalache	InstanceInFolder	NumMod	False	Passed	Model Under Test Equivalent Model
2b6b6f6dab87b861bb38f044a30acdbd7dd8b367	Apalache	InstanceWithInFolder	NumMod	True	Passed	Model Under Test Equivalent Model
41b6078f0ca59955aca0ac89aec4ab7f2b91af6b	Apalache	InstanceWithInFolder	NumMod	False	Passed	Model Under Test Equivalent Model
16287c072bc78e3f8e34eca6268e6b2b3f5a9eac	Apalache	InstanceNamedInFolder	NumMod	True	Passed	Model Under Test Equivalent Model
6691a2bd1a8264d4db12599073bb06e7103930ac	Apalache	InstanceNamedInFolder	NumMod	False	Passed	Model Under Test Equivalent Model
90be98f9107b7bd90e44707cce92cfac51616eaf	Apalache	InstanceNamedWithInFolder	NumMod	True	Passed	Model Under Test Equivalent Model
702faeeb207b91f665f0f709054f88bee71d0e44	Apalache	InstanceNamedWithInFolder	NumMod	False	Passed	Model Under Test Equivalent Model
678d8edc903445263cef0afa6dd828b446b66f34	Apalache	Lambda	NumMod	True	Passed	Model Under Test Equivalent Model
4b941f265e044c8e38db6ef8fbe24a8414cef261	Apalache	Lambda	NumMod	False	Passed	Model Under Test Equivalent Model
02eb85d7253349f85c06fa9793db26c6551a06a6	Apalache	IfThen	NumMod	True	Passed	Model Under Test Equivalent Model
94b8341223281ce26747964cd77cd468cdd2ab16	Apalache	IfThen	NumMod	False	Passed	Model Under Test Equivalent Model
73d0e3f57dff3dbcc7545219c6e120ad4c8ab866	Apalache	IfElse	NumMod	True	Passed	Model Under Test Equivalent Model
01ffdf6a346e466355e8ab0716b8372f2b538e4a	Apalache	IfElse	NumMod	False	Passed	Model Under Test Equivalent Model
8a2150dc1efd9abb2166f41841f808d54ab4ba8c	Apalache	Unchanged	NumMod	True	Passed	Model Under Test Equivalent Model
3c4359b8aad191ee9579d34685b160e78223b205	Apalache	Unchanged	NumMod	False	Passed	Model Under Test Equivalent Model
3ec1b130d755a4171f0ea760edbdb6c70a983152	Apalache	SeqSubSeq	NumMod	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
40bd407efeb40fb2903926bdab5cf529bacfed8a	Apalache	SeqSubSeq	NumMod	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
1509485f43f11a759d075035b335eb826c15d70e	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	NumMod	True	Passed	Model Under Test Equivalent Model
d8ed3755a42d4a80063e6fd37f4d7cd8fa09f9eb	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	NumMod	False	Passed	Model Under Test Equivalent Model
1fd339a218ad09128b18094a5377b536f0788e0a	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumMod	True	Passed	Model Under Test Equivalent Model
27a470c19f9952f1d143201badaa19e653a1fe16	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	NumMod	False	Passed	Model Under Test Equivalent Model
3f0ca684d1b173594a175af6cfc152eefb31ccb0	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumMod	True	Passed	Model Under Test Equivalent Model
d6a2ae5361579283eef1c75e3fc85d483d2929cd	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	NumMod	False	Passed	Model Under Test Equivalent Model
29484ae07ab910e06c07628cc9da18b741f16284	Apalache	BagBagIn	NumMod	True	Passed	Model Under Test Equivalent Model
53a2438755ee183cd697f752903bbb4747cca825	Apalache	BagBagIn	NumMod	False	Passed	Model Under Test Equivalent Model
2dd86e93b41db3fff110085ee54d3d3cffe4610c	Apalache	BagCopiesIn	NumMod	True	Passed	Model Under Test Equivalent Model
d7dec039060f36405ca70c7e24bd86120c4e6cda	Apalache	BagCopiesIn	NumMod	False	Passed	Model Under Test Equivalent Model
8010ce266e3e7e10c86b43053c0d800cf0593a06	Apalache	SeqAppend	NumMod	True	Passed	Model Under Test Equivalent Model
9141eaaae379181cc134113bf75e4d6511fdeb9d	Apalache	SeqAppend	NumMod	False	Passed	Model Under Test Equivalent Model

Index

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