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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
c512219a3563b9511c6a702f69aa738b33d81d5f	Apalache	And	SeqHead	True	Passed	Model Under Test Equivalent Model
65c0bb6c20e70cbcc699c639c9ac82b3feed45e6	Apalache	And	SeqHead	False	Passed	Model Under Test Equivalent Model
5df9e18740e3de073766419123217f4f503bc440	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	SeqHead	True	Passed	Model Under Test Equivalent Model
7a675f6bf3bdc44f5148bd03afbd706ece424de0	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	SeqHead	False	Passed	Model Under Test Equivalent Model
781649b73558e63d26bed988f6891f43972442f5	Apalache	Imply	SeqHead	True	Passed	Model Under Test Equivalent Model
b04271bf5ec5a04fb2d8c002caff1370c6389abe	Apalache	Imply	SeqHead	False	Passed	Model Under Test Equivalent Model
295cee2f26dbf4f56610b92afda6c057679aebc4	Apalache	Not	SeqHead	True	Passed	Model Under Test Equivalent Model
f4c53ab4ba441083595d5e8af1934a5d7d5bddc3	Apalache	Not	SeqHead	False	Passed	Model Under Test Equivalent Model
36512f46a98602696315a8030ca8f7b5a5fe48c6	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	SeqHead	True	Passed	Model Under Test Equivalent Model
0ac15a24f40fdfa8852322d1c6057cc0bfed73e6	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	SeqHead	False	Passed	Model Under Test Equivalent Model
4bd8640b446576bca9773d3b1153ea3e55cae561	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	SeqHead	True	Passed	Model Under Test Equivalent Model
345006ee1064b7b0872747829fba7ac8bfbcd242	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	SeqHead	False	Passed	Model Under Test Equivalent Model
8adab3f487246dfcdf04a0086b7ceea323dc012e	Apalache	AndProp	SeqHead	True	Passed	Model Under Test Equivalent Model
087c0008503ea6185f828c98cf5ffecfed4dd9a5	Apalache	AndProp	SeqHead	False	Passed	Model Under Test Equivalent Model
a039d377f222bd5139495635171f287de96eceea	Apalache	Boxed	SeqHead	True	Passed	Model Under Test Equivalent Model
8dc65aca6f913aa1b4e5941812a157f2ae906461	Apalache	Boxed	SeqHead	False	Passed	Model Under Test Equivalent Model
d4d119843a6e27001e2f01fef854b01ffc4a77ab	Apalache	Eq	SeqHead	True	Passed	Model Under Test Equivalent Model
92542d1eb208311198b8025f1fffc390c48a6f53	Apalache	Eq	SeqHead	False	Passed	Model Under Test Equivalent Model
5c38aaf986a043a08ee899c5d0c058027b700596	Apalache	Ne	SeqHead	True	Passed	Model Under Test Equivalent Model
c6e741e9cc4561c6dc858daa2cac4ed8417ab6bd	Apalache	Ne	SeqHead	False	Passed	Model Under Test Equivalent Model
b2b471d147a98c7c6c4192bad1e0dff94a250d25	Apalache	Let	SeqHead	True	Passed	Model Under Test Equivalent Model
b7473182780da65ad1067325217ec909e3892cf5	Apalache	Let	SeqHead	False	Passed	Model Under Test Equivalent Model
0dc8a7f4dd0f54ba23d542c9051efc85de37c7b5	Apalache	Set0	SeqHead	True	Passed	Model Under Test Equivalent Model
a01d629ce6ef92c9e38ad6702ed28e10e6ae574f	Apalache	Set0	SeqHead	False	Passed	Model Under Test Equivalent Model
fa5139d0a79b17676e988d90f051ca3f66b502ce	Apalache	Set1	SeqHead	True	Passed	Model Under Test Equivalent Model
e395642614945e84d640f80dd068a17e1a63b1d6	Apalache	Set1	SeqHead	False	Passed	Model Under Test Equivalent Model
87b5e92476659a86c26ffd537a3802bd7a55b6b0	Apalache	Set2	SeqHead	True	Passed	Model Under Test Equivalent Model
ac689ef737af0a51ec72d4f842d00be475383be7	Apalache	Set2	SeqHead	False	Passed	Model Under Test Equivalent Model
4e23f542e99fbae72b63f916ebca38bdd07b353f	Apalache	Fun	SeqHead	True	Passed	Model Under Test Equivalent Model
ca5ed26734833540c36f88339d2fb8e7fdf75d07	Apalache	Fun	SeqHead	False	Passed	Model Under Test Equivalent Model
204e2b34cc9a27862556f3a55f664159954a85e0	Apalache	In	SeqHead	True	Passed	Model Under Test Equivalent Model
d12d34831119feccf21833bdb07d79ddd13a57b6	Apalache	In	SeqHead	False	Passed	Model Under Test Equivalent Model
585c817eaf963fc83ed0d1f12662478b14a925d1	Apalache	NotIn	SeqHead	True	Passed	Model Under Test Equivalent Model
9029f18442546132906ae697e907f1992524df9f	Apalache	NotIn	SeqHead	False	Passed	Model Under Test Equivalent Model
f7df349975c76f4644791da923dd9a637f9b9c9b	Apalache	Exists	SeqHead	True	Passed	Model Under Test Equivalent Model
d396c936081195a136c435204ff48529c427fa07	Apalache	Exists	SeqHead	False	Passed	Model Under Test Equivalent Model
9bdae37ee65772dc78391b136f2f274fadf5d68c	Apalache	Forall	SeqHead	True	Passed	Model Under Test Equivalent Model
7a07891739df18ff94d2cf902ccfb6520b2e979d	Apalache	Forall	SeqHead	False	Passed	Model Under Test Equivalent Model
cdfb9a899775459e4d3a26e1647a80f225898c8e	Apalache	Choose	SeqHead	True	Passed	Model Under Test Equivalent Model
73e400922f0b6bf773c7a7ce170101ab5a351874	Apalache	Choose	SeqHead	False	Passed	Model Under Test Equivalent Model
4c533603977cd5ba01ff747dc37e75f8717a7dcc	Apalache	Record	SeqHead	True	Passed	Model Under Test Equivalent Model
691a7dd5994921372739d395b11752528a6cad29	Apalache	Record	SeqHead	False	Passed	Model Under Test Equivalent Model
f4a92ca39cab876c6bc445e6a5bd2a4bbcc85279	Apalache	Tuple	SeqHead	True	Passed	Model Under Test Equivalent Model
86ec29bf95bac72da2af46d6617d37b48e30ba46	Apalache	Tuple	SeqHead	False	Passed	Model Under Test Equivalent Model
1e2580effe2b7f7d9945f333b2b272b64b1aaed1	Apalache	FunApp	SeqHead	True	Passed	Model Under Test Equivalent Model
3dbdb3eea2156ff1b04e720a68be6b2c41e43da9	Apalache	FunApp	SeqHead	False	Passed	Model Under Test Equivalent Model
343b1f3370aeb1b321256fe34ac84dc471355a11	Apalache	Except0	SeqHead	True	Passed	Model Under Test Equivalent Model
2b28b5a1686ba56e3a5dc317bc94c3dad53ae950	Apalache	Except0	SeqHead	False	Passed	Model Under Test Equivalent Model
314e23c84b3483297cea1e375ab766d9b8926fd5	Apalache	Except1Fun	SeqHead	True	Passed	Model Under Test Equivalent Model
0f9eec7852e047b0e473ff0c22454298d80dab9a	Apalache	Except1Fun	SeqHead	False	Passed	Model Under Test Equivalent Model
bb91ed832bcdbbf10c63171bec0e70bf4187969d	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqHead	True	Passed	Model Under Test Equivalent Model
2dee1104f65fcdf11507a4b3029809395cf050d8	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqHead	False	Passed	Model Under Test Equivalent Model
9bdbef6d2c332a1baef9eb4dc541b17e707102c4	Apalache	Except1Rec	SeqHead	True	Passed	Model Under Test Equivalent Model
4fa1643ce601beae2b014a0ba26d0541590a8324	Apalache	Except1Rec	SeqHead	False	Passed	Model Under Test Equivalent Model
31de2ca409a90a76bdc89fd95a04ff668709367c	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqHead	True	Passed	Model Under Test Equivalent Model
9f380281d320a1080b3a9f5383a094a888cad150	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqHead	False	Passed	Model Under Test Equivalent Model
f05bd0c07bd80e156af6f4953c96d574f734f80a	Apalache	Except2Fun	SeqHead	True	Passed	Model Under Test Equivalent Model
96cdd7758ff3ba605e2bde1c3946384c03e78e28	Apalache	Except2Fun	SeqHead	False	Passed	Model Under Test Equivalent Model
8280742ea3e56b842ff4ec502d83a76280a1789a	Apalache	Except2FunTuple	SeqHead	True	Passed	Model Under Test Equivalent Model
e07222fc04d5e683ffa86838fadd478e22a961f0	Apalache	Except2FunTuple	SeqHead	False	Passed	Model Under Test Equivalent Model
d372d9a1853c9992c01aef357e08de1cac1a9042	Apalache	Prime	SeqHead	True	Passed	Model Under Test Equivalent Model
10c886dad81873dceb328a8aeffbde7ab5d5f2ce	Apalache	Prime	SeqHead	False	Passed	Model Under Test Equivalent Model
b62bc47becca50fcfeb38656ec08a617aa6d15fa	Apalache	NumUnaryMinus	SeqHead	True	Passed	Model Under Test Equivalent Model
fbdc24b39812a0585cfe88de4bbd1e8de1292d5c	Apalache	NumUnaryMinus	SeqHead	False	Passed	Model Under Test Equivalent Model
b1b529778846eb6a8da5a342f52668348d136a7b	Apalache	NumPlus	SeqHead	True	Passed	Model Under Test Equivalent Model
34477ce80f6a591194ed514d0ada84b547ff6799	Apalache	NumPlus	SeqHead	False	Passed	Model Under Test Equivalent Model
bc62c8687c638d9a42d0c9658a06070b4e1935f1	Apalache	NumMinus	SeqHead	True	Passed	Model Under Test Equivalent Model
09b9b99ca28e303bd55bd0b7bcd7c8d4456d30f0	Apalache	NumMinus	SeqHead	False	Passed	Model Under Test Equivalent Model
adb5800556f2ef2f46a2218e4b7bfa3c183f0b72	Apalache	NumMul	SeqHead	True	Passed	Model Under Test Equivalent Model
531b1692033932e93f452841618bd7cf6dce5e88	Apalache	NumMul	SeqHead	False	Passed	Model Under Test Equivalent Model
6fe077472aa24659bad7e3ffd7f905455d3a490e	Apalache	NumDiv	SeqHead	True	Passed	Model Under Test Equivalent Model
c98ff60199fe10f0adb7529f9095bb2f20394330	Apalache	NumDiv	SeqHead	False	Passed	Model Under Test Equivalent Model
9faed85e8f83c6bcf2f4c41c11a17d38e23cac0d	Apalache	NumMod	SeqHead	True	Passed	Model Under Test Equivalent Model
85c759c2606906e9c2b5f7407afa8313b0610d18	Apalache	NumMod	SeqHead	False	Passed	Model Under Test Equivalent Model
13e190307245c44a818451416278c016e9dfe34e	Apalache	NumPow	SeqHead	True	Passed	Model Under Test Equivalent Model
b58aa8ee0f7b7a7d3b8da49daf830b81aa7e48c8	Apalache	NumPow	SeqHead	False	Passed	Model Under Test Equivalent Model
eb64731c8fa37ab67e4e3235f17e61e66029638a	Apalache	NumGt	SeqHead	True	Passed	Model Under Test Equivalent Model
b839fe4a94e2b0beac481c9ca23e3b30101da283	Apalache	NumGt	SeqHead	False	Passed	Model Under Test Equivalent Model
af93a9c6552fae79bf1da24211a314702a3786e6	Apalache	NumGe	SeqHead	True	Passed	Model Under Test Equivalent Model
76ef7da9f7509e50ad74275d82763fdd2480c003	Apalache	NumGe	SeqHead	False	Passed	Model Under Test Equivalent Model
08cdcb32d91023044dd86aa0c84b300b4bb65107	Apalache	NumLt	SeqHead	True	Passed	Model Under Test Equivalent Model
d446429245780915093bbe6fc31d4727cde52a46	Apalache	NumLt	SeqHead	False	Passed	Model Under Test Equivalent Model
c635a50232a03314d5af6d95a20d49e35052ceda	Apalache	NumLe	SeqHead	True	Passed	Model Under Test Equivalent Model
fd2839bc211ca13daaa88709d753cf3eff3b7f5a	Apalache	NumLe	SeqHead	False	Passed	Model Under Test Equivalent Model
0ce96891874d5762f64e4e554bad8e0efdafa703	Apalache	DefFun	SeqHead	True	Passed	Model Under Test Equivalent Model
97363a7f07e8428b2bdbb2623388ddbcb7506e10	Apalache	DefFun	SeqHead	False	Passed	Model Under Test Equivalent Model
8fc43dc032129265718d0b7c09c3e64339beed68	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqHead	True	Passed	Model Under Test Equivalent Model
da1b36df620cd74d6f5d265792015f285a626f25	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqHead	False	Passed	Model Under Test Equivalent Model
559281a89c747a4046b075110b6187830aa59190	Apalache	DefFunRecursive	SeqHead	True	Passed	Model Under Test Equivalent Model
254c6fc88054ce2d8a424d44a0b0a411128f541e	Apalache	DefFunRecursive	SeqHead	False	Passed	Model Under Test Equivalent Model
39a7d965b5f6359eb99145c4fe888d2527b1a759	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqHead	True	Passed	Model Under Test Equivalent Model
52f787c447fdbdf0ddde27757ee0bf178d2eb229	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqHead	False	Passed	Model Under Test Equivalent Model
0220ecbf114db746620694ff3b83aec5aa7f5519	Apalache	Def0	SeqHead	True	Passed	Model Under Test Equivalent Model
8b3cb7521ce40c0b5ab3aaf4d973d5814899ac30	Apalache	Def0	SeqHead	False	Passed	Model Under Test Equivalent Model
2381f305b9efd5d804ca9c064a05cd4de322b60e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqHead	True	Passed	Model Under Test Equivalent Model
2bc29aff69f3f177621f014216a6e050639c5a64	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqHead	False	Passed	Model Under Test Equivalent Model
b526b5bbb0c3ddefabd0f396dd0c3817216b3a39	Apalache	Def1	SeqHead	True	Passed	Model Under Test Equivalent Model
1e9200949a4b43c0f9ec43a5e2dd6de3311acbbf	Apalache	Def1	SeqHead	False	Passed	Model Under Test Equivalent Model
d47e13a13512d6543410f2dc65aa7705bb20db94	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqHead	True	Passed	Model Under Test Equivalent Model
7ffa03bb86488d08fe771e5fb1c436540b7200f3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqHead	False	Passed	Model Under Test Equivalent Model
b70103f7ebc6a092543c770f503696dc8a57ddd0	Apalache	Def2	SeqHead	True	Passed	Model Under Test Equivalent Model
06b80920a37ac5b4bc398c6f4dbbc115cf877711	Apalache	Def2	SeqHead	False	Passed	Model Under Test Equivalent Model
7d76e38f6aca67af7868094b77d94c2bc06a5ab7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqHead	True	Passed	Model Under Test Equivalent Model
2dc1bfa406e1cc195c9bceae8b76ae9bbdbac28f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqHead	False	Passed	Model Under Test Equivalent Model
c21b7b266cac30622435f3814e911619f20be3ce	Apalache	Def1Recursive	SeqHead	True	Passed	Model Under Test Equivalent Model
d3f3b939dbaf69f2786a4571f0a995cb503713bc	Apalache	Def1Recursive	SeqHead	False	Passed	Model Under Test Equivalent Model
852bf909a8d48261418a09dfb030bdd3388c755a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqHead	True	Passed	Model Under Test Equivalent Model
8dda9eeb05692e93e6e54d57c600bec73b6af96b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqHead	False	Passed	Model Under Test Equivalent Model
26c0653faab3ca94d1ce46f7324f243c8efea767	Apalache	Extends	SeqHead	True	Passed	Model Under Test Equivalent Model
947bd84d55b0f34200deb00925204e76aac65e29	Apalache	Extends	SeqHead	False	Passed	Model Under Test Equivalent Model
1d5da3ef8faafa97a96c9ada4bf2eead83f92de8	Apalache	ExtendsInDifferentFolder	SeqHead	True	Passed	Model Under Test Equivalent Model
ad8cfaebe2cfa704d67192eab917ccbd7448d24e	Apalache	ExtendsInDifferentFolder	SeqHead	False	Passed	Model Under Test Equivalent Model
da3bdd9bc8655dd66343efc13af4723e6467c696	Apalache	Variable	SeqHead	True	Passed	Model Under Test Equivalent Model
ed7c4bc0d84726a2e945fc4b5024500fb07f89c1	Apalache	Variable	SeqHead	False	Passed	Model Under Test Equivalent Model
e2769749cfd168182d5e74efcab24b862cb3ebe6	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqHead	True	Passed	Model Under Test Equivalent Model
97c299ff9663825acf5f0327748d4e5060f48aa5	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqHead	False	Passed	Model Under Test Equivalent Model
7d0c5acb441de688f3fdb838a121a8faa6f9cfbc	Apalache	Constant	SeqHead	True	Passed	Model Under Test Equivalent Model
45027525c9daac475db0d6f379e3d0b0d56e5fd6	Apalache	Constant	SeqHead	False	Passed	Model Under Test Equivalent Model
0fcce1aff30f44cd0c8d5554d7b2e7c0a4ad6989	Apalache	ConstantRank1	SeqHead	True	Passed	Model Under Test Equivalent Model
05782dea8c4d9f34c132ca0d782ae2b10e286381	Apalache	ConstantRank1	SeqHead	False	Passed	Model Under Test Equivalent Model
049cbbecd732041d17fde3ed435ab1f993c50d69	Apalache	Instance	SeqHead	True	Passed	Model Under Test Equivalent Model
e463447df1eb16357fc4d196ba646fe273c72149	Apalache	Instance	SeqHead	False	Passed	Model Under Test Equivalent Model
73d57f11175aaac680c562ae961e3de5d7cae988	Apalache	InstanceWith	SeqHead	True	Passed	Model Under Test Equivalent Model
092e3d79080b215c593df1900ca7260124a6d44e	Apalache	InstanceWith	SeqHead	False	Passed	Model Under Test Equivalent Model
4c60efc80dbdd28acbf6578e6447436a32ffba85	Apalache	InstanceNamed	SeqHead	True	Passed	Model Under Test Equivalent Model
9adab204162ffc27ae7073757e0f00fe5f2d2c10	Apalache	InstanceNamed	SeqHead	False	Passed	Model Under Test Equivalent Model
89e5ad9e48ef8f73b6871f88a28f9ee07156e23d	Apalache	InstanceNamedWith	SeqHead	True	Passed	Model Under Test Equivalent Model
746f0b502f708d2558a3f83a5919536b36b77004	Apalache	InstanceNamedWith	SeqHead	False	Passed	Model Under Test Equivalent Model
b26f0b7118652e1074dc9ae6821aa9b7da135b35	Apalache	InstanceInFolder	SeqHead	True	Passed	Model Under Test Equivalent Model
26706a902001d40a11734f0b75c77a7468b256f3	Apalache	InstanceInFolder	SeqHead	False	Passed	Model Under Test Equivalent Model
8ccdc6c19854a621f6885c9fd96289af6f1ee39f	Apalache	InstanceWithInFolder	SeqHead	True	Passed	Model Under Test Equivalent Model
a6694a4329397d55b970cc063d97d6af29d8a21b	Apalache	InstanceWithInFolder	SeqHead	False	Passed	Model Under Test Equivalent Model
2058780f327630874e86d5e1c5105cb00a0bd702	Apalache	InstanceNamedInFolder	SeqHead	True	Passed	Model Under Test Equivalent Model
95241e721a1d82a47793f5aa49ee9a77be9438cc	Apalache	InstanceNamedInFolder	SeqHead	False	Passed	Model Under Test Equivalent Model
17c4dab18b4f21fca5dd8c059536026394528fef	Apalache	InstanceNamedWithInFolder	SeqHead	True	Passed	Model Under Test Equivalent Model
6a74b29a5ea61170c213b0e08cc61e1937fcfc7d	Apalache	InstanceNamedWithInFolder	SeqHead	False	Passed	Model Under Test Equivalent Model
791e7c9ab7a35abce819905fcc80ce0c047a6782	Apalache	Enabled	SeqHead	True	Passed	Model Under Test Equivalent Model
bd695a2e71bcfb69e23f82eeb3e8641eb39e151a	Apalache	Enabled	SeqHead	False	Passed	Model Under Test Equivalent Model
d7f6ecd8d08e9146513dee334b7fc5fb14efefd9	Apalache	Assume	SeqHead	True	Passed	Model Under Test Equivalent Model
ca0420a0600e7b1d9a5c6bf8657637798f9668d1	Apalache	Assume	SeqHead	False	Passed	Model Under Test Equivalent Model
8a4d8e53dcaaae1ff04c6b5567cc1c05ca152a2e	Apalache	AssumeNamed	SeqHead	True	Passed	Model Under Test Equivalent Model
0ea3177c398a6a7ca5d4a4463beda71f63e79eaa	Apalache	AssumeNamed	SeqHead	False	Passed	Model Under Test Equivalent Model
1e334cc10209c1a49f6068eea29a76583db52562	Apalache	Lambda	SeqHead	True	Passed	Model Under Test Equivalent Model
317db677952e94852a94b893e8d241a06f4c0015	Apalache	Lambda	SeqHead	False	Passed	Model Under Test Equivalent Model
720b73c889abb15182955928917752ec720bfe39	Apalache	Cross2	SeqHead	True	Passed	Model Under Test Equivalent Model
7db5afd3a0ccbfa401abd82dba5998ab4cf46730	Apalache	Cross2	SeqHead	False	Passed	Model Under Test Equivalent Model
447f05781fc360c48e5fee6143f232f3cb4b57b3	Apalache	Cross3	SeqHead	True	Passed	Model Under Test Equivalent Model
e556480a8954fdefdefea093d464fe18f51a3be6	Apalache	Cross3	SeqHead	False	Passed	Model Under Test Equivalent Model
6034569e550613251a36a8bafa1d09506c308f44	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	SeqHead	True	Passed	Model Under Test Equivalent Model
49c978281fc2d140c96f77f935a3d3cd46b9f11c	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	SeqHead	False	Passed	Model Under Test Equivalent Model
7005d85f6ae76ee3576055e36659bf50cba47d74	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	SeqHead	True	Passed	Model Under Test Equivalent Model
643cc30b31dbaad66e1512e80f1f3d755bde142f	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	SeqHead	False	Passed	Model Under Test Equivalent Model
35ff6a727939f360083f4009153b819709dd25a6	Apalache	SetDiff	SeqHead	True	Passed	Model Under Test Equivalent Model
9c3e6693f8754bff86ed51491a36a7556189e737	Apalache	SetDiff	SeqHead	False	Passed	Model Under Test Equivalent Model
b193c6541fe455447bfed7baf57796d4db9e24c3	Apalache	SetUnion	SeqHead	True	Passed	Model Under Test Equivalent Model
c30d18fbb181b0bdc4b8bebfde1b49473202d1f8	Apalache	SetUnion	SeqHead	False	Passed	Model Under Test Equivalent Model
80766efd1ad00fe9d67f4d8b58cd6a74c5557612	Apalache	SetIntersect	SeqHead	True	Passed	Model Under Test Equivalent Model
8254e24c3925464be320e66d990bd1a85d8b5144	Apalache	SetIntersect	SeqHead	False	Passed	Model Under Test Equivalent Model
1ce7b6b2fd2777a6e9d70dbe053821c3f58964a2	Apalache	SubsetEq	SeqHead	True	Passed	Model Under Test Equivalent Model
360bedfb27df4f4a0801acccbe1ae8689d78d98f	Apalache	SubsetEq	SeqHead	False	Passed	Model Under Test Equivalent Model
236b0746bb07bf3f934961dcc1ee78e88d4e4709	Apalache	IfCond	SeqHead	True	Passed	Model Under Test Equivalent Model
6dc18df976302ab2d94ca6c030d93384105d2f61	Apalache	IfCond	SeqHead	False	Passed	Model Under Test Equivalent Model
8acdc0137969bf2324116b79384dccf97c9ccf28	Apalache	IfThen	SeqHead	True	Passed	Model Under Test Equivalent Model
0f74dd6d76dd1a81a4052277fd38f3f577604690	Apalache	IfThen	SeqHead	False	Passed	Model Under Test Equivalent Model
86a7bed360a50dd399cae098a877ea6d13f4ad94	Apalache	IfElse	SeqHead	True	Passed	Model Under Test Equivalent Model
293af290a551610f00b588dee0dab22d0a837e20	Apalache	IfElse	SeqHead	False	Passed	Model Under Test Equivalent Model
c553c61921282b4161fe4c5d11f1b54e84dc50e5	Apalache	Subset	SeqHead	True	Passed	Model Under Test Equivalent Model
79ec1238cae7457dcead6a72d672ed95c72ff4b6	Apalache	Subset	SeqHead	False	Passed	Model Under Test Equivalent Model
3e3be0578ea3643ef27e90aa9fdffcf3405a08c6	Apalache	Domain	SeqHead	True	Passed	Model Under Test Equivalent Model
53ef9984666deb57f97ae5ce6a993f09ccf09b0d	Apalache	Domain	SeqHead	False	Passed	Model Under Test Equivalent Model
ad8ef50f1d0b45346be31303bf0c3150888403b2	Apalache	Union	SeqHead	True	Passed	Model Under Test Equivalent Model
355b0051ba396cf3a6913e852ff29b1816021b7e	Apalache	Union	SeqHead	False	Passed	Model Under Test Equivalent Model
dc7ebb2bccfa5f51ca711740c38725f3bfa266f0	Apalache	Unchanged	SeqHead	True	Passed	Model Under Test Equivalent Model
86ff6237e717cd65b3a160c26e9f1be943b3e09f	Apalache	Unchanged	SeqHead	False	Passed	Model Under Test Equivalent Model
143ea9b989a626d5aa4487e2d5ec6ac51ddff6f0	Apalache	Equivalence	SeqHead	True	Passed	Model Under Test Equivalent Model
95442647bb3c84289d4ea28ea83933e643b47909	Apalache	Equivalence	SeqHead	False	Passed	Model Under Test Equivalent Model
6aa577f812a2690fd0e2701fd2b5190600f79360	Apalache	SeqLen	SeqHead	True	Passed	Model Under Test Equivalent Model
fc55b06a88301bcde2dc4e49c4b64e765a754b3b	Apalache	SeqLen	SeqHead	False	Passed	Model Under Test Equivalent Model
60b8e45f31bb0ff0f517c99515494fd6837aff75	Apalache	SeqConcat	SeqHead	True	Passed	Model Under Test Equivalent Model
bad303f4c4829b53a2735759150c48ec8be3344e	Apalache	SeqConcat	SeqHead	False	Passed	Model Under Test Equivalent Model
8f51ae4a33308bf6997b86239c78d0a16155d77d	Apalache	SeqSeq	SeqHead	True	Passed	Model Under Test Equivalent Model
b743da75483d8cb21f7bd827a7f288827c3adec4	Apalache	SeqSeq	SeqHead	False	Passed	Model Under Test Equivalent Model
a06aade442b70f1d56c59fb90d9c86a86a21c5a4	Apalache	SeqSelectSeq	SeqHead	True	Passed	Model Under Test Equivalent Model
1b295c95699b49bdaef56a99580ca720235ea57e	Apalache	SeqSelectSeq	SeqHead	False	Passed	Model Under Test Equivalent Model
05893f40ad00e7a82f92d83e9f07d464ea6a9c95	Apalache	SeqSubSeq	SeqHead	True	Passed	Model Under Test Equivalent Model
62df1eb406f01047e91a3d62c36e810656b324a1	Apalache	SeqSubSeq	SeqHead	False	Passed	Model Under Test Equivalent Model
ead603e37614112cd22b8ca6fa7fadf88e103197	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	SeqHead	True	Passed	Model Under Test Equivalent Model
933a66adf5f1bb169d9b7c9bc958f0e8f59a5cc5	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	SeqHead	False	Passed	Model Under Test Equivalent Model
de7a8f10a0cd873449cee8ca6f2c31cdaf87e64b	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqHead	True	Passed	Model Under Test Equivalent Model
94e3a82bee27db9ba8b2a87a61d3a988cfdfce24	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqHead	False	Passed	Model Under Test Equivalent Model
ed79e0f5ba310b71df0f41dd4370bf3b6cf87064	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	SeqHead	True	Passed	Model Under Test Equivalent Model
d8c45d2401a813838365d675f84f9f4e3138c45b	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	SeqHead	False	Passed	Model Under Test Equivalent Model
1d1030093473d323ebc1c401358a652cb9e0a884	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	SeqHead	True	Passed	Model Under Test Equivalent Model
293a418a2b50cb78485ee6b8239d96f068368be2	TLC with reduction strategy: Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	TlcPermuteFun	SeqHead	False	Passed	Model Under Test Equivalent Model
5d383d0de9047d6315e029b0769147929a59e02d	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqHead	True	Passed	Model Under Test Equivalent Model
4e592bd68e2e8bc1dfc40380533503b8215a3d77	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqHead	False	Passed	Model Under Test Equivalent Model
a6efaa222dc1fa1af95fc5ced8f9f6d017bb7247	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqHead	True	Passed	Model Under Test Equivalent Model
612841233f12a71c41abec502e83e4671983e665	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqHead	False	Passed	Model Under Test Equivalent Model
a8e1812e997438a2b3026e3ab188d1a4c0e375bd	Apalache	BagBagToSet	SeqHead	True	Passed	Model Under Test Equivalent Model
68aa068b1dc30cbc03ae70169c85408aaa03117b	Apalache	BagBagToSet	SeqHead	False	Passed	Model Under Test Equivalent Model
d4a7e7bb55a05cb3a545c175628c34c8bac2ae79	Apalache	BagSetToBag	SeqHead	True	Passed	Model Under Test Equivalent Model
6777aa2e21f5572a2ef0e66e309d11df36c5b998	Apalache	BagSetToBag	SeqHead	False	Passed	Model Under Test Equivalent Model
afa9d2fd28bb33858729d7507e39955368f88e2e	Apalache	BagBagIn	SeqHead	True	Passed	Model Under Test Equivalent Model
b52a06d392c0ebf8e40400b025deb19161e54561	Apalache	BagBagIn	SeqHead	False	Passed	Model Under Test Equivalent Model
874bf2479a6b631eb80cf8b838bcb53fa95b43bd	Apalache	BagAddBag	SeqHead	True	Passed	Model Under Test Equivalent Model
a83be4d563062ba7b1539f3b5eafc0ce08c42479	Apalache	BagAddBag	SeqHead	False	Passed	Model Under Test Equivalent Model
a13bab5a8182ed9748e6b25ddd4f85e47c7280c6	Apalache	BagBagSub	SeqHead	True	Passed	Model Under Test Equivalent Model
98da7c2c0aeda42d41638daba40c4e2b2966d534	Apalache	BagBagSub	SeqHead	False	Passed	Model Under Test Equivalent Model
2ed56604f22a37b2562d5a1020525609bc48bdaf	Apalache	BagCopiesIn	SeqHead	True	Passed	Model Under Test Equivalent Model
345eb41ed90abddf0f789e8b38542d866ff63263	Apalache	BagCopiesIn	SeqHead	False	Passed	Model Under Test Equivalent Model
a5e4305c6afc59713c8fad729a0bf37aec5fee3e	Apalache	BagSubsetEqBag	SeqHead	True	Passed	Model Under Test Equivalent Model
c3bd0f8a5c4170e8c57acfc3a760483296e213fd	Apalache	BagSubsetEqBag	SeqHead	False	Passed	Model Under Test Equivalent Model
c7b36a125502398b6c8a180e0fa43d8d04599b9b	Apalache	BagBagUnion	SeqHead	True	Passed	Model Under Test Equivalent Model
8b5a9448842b24f38c6089fab1957752a538df80	Apalache	BagBagUnion	SeqHead	False	Passed	Model Under Test Equivalent Model
f0914f5057d6a6e6a37686e98f9ece59f0782a59	Apalache	BagBagCardinality	SeqHead	True	Passed	Model Under Test Equivalent Model
0abbad6541f0959e2d4779d2e439f9dae6d2720f	Apalache	BagBagCardinality	SeqHead	False	Passed	Model Under Test Equivalent Model
0b7d6f84a4fc23a207fcfca95163ce31e9b5c9a7	Apalache	BagBagOfAll	SeqHead	True	Passed	Model Under Test Equivalent Model
b430164d1285e6900e6dda23270ec9c9907911a8	Apalache	BagBagOfAll	SeqHead	False	Passed	Model Under Test Equivalent Model
8a1309d932c9f53322bb0c61125434c68967ba8f	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	SeqHead	True	Passed	Model Under Test Equivalent Model
e166c18829a13e6801100c1c8af6ef70e1385793	TLC with reduction strategy: Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation	BagSubBag	SeqHead	False	Passed	Model Under Test Equivalent Model
a51e076c5aba0312946753a258e3ba7fc704cc46	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	SeqHead	True	Passed	Model Under Test Equivalent Model
3289c9aef9a78a542944a87bf39475f71f30ec5f	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	SeqHead	False	Passed	Model Under Test Equivalent Model
7658647f8953a11414e2cd9655f83968abe314ed	Apalache	FiniteSetsCardinality	SeqHead	True	Passed	Model Under Test Equivalent Model
f786b7c02f4bbe3e7689ef59792189317103feb5	Apalache	FiniteSetsCardinality	SeqHead	False	Passed	Model Under Test Equivalent Model
206eee6c7b08a142bf18b646a826dc4951390797	Apalache	SeqHead	SeqHead	True	Passed	Model Under Test Equivalent Model
d226ed08096d6836d0d24cb312db935961d33c17	Apalache	SeqHead	SeqHead	False	Passed	Model Under Test Equivalent Model
d0ad9f56ab4969f82cc33bec4cc4d756c3814ffc	Apalache	SeqTail	SeqHead	True	Passed	Model Under Test Equivalent Model
96fe0c106ec086809aa69305152c64469b51bbe0	Apalache	SeqTail	SeqHead	False	Passed	Model Under Test Equivalent Model
35f1191034d89f028b0c36321eec7e4d827b2a50	Apalache	SeqAppend	SeqHead	True	Passed	Model Under Test Equivalent Model
71c065eb44c5ed27602c52533665dfcb46e69962	Apalache	SeqAppend	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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