Tests by case feature SeqSeq; CLI Option: -workers 1

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
edddd2465a0eeda20d0c22697985dc9943443302	Apalache	SeqSeq	BoolSet	True	Passed	Model Under Test Equivalent Model
e59ab48d382b59546562ad885622efb5c59bb6d2	Apalache	SeqSeq	BoolSet	False	Passed	Model Under Test Equivalent Model
9eff50885eceeef15b93ad460aa5ef124822d9e9	Apalache	SeqSeq	Let	True	Passed	Model Under Test Equivalent Model
4c6773c89039a78b51cdf9e6fad4b459272e4c43	Apalache	SeqSeq	Let	False	Passed	Model Under Test Equivalent Model
3ed12ca388e79012b240d1f010b3742b43ee5a32	Apalache	SeqSeq	SetEmpty	True	Passed	Model Under Test Equivalent Model
7b068aab3f0e111a205063c88c07c0419cae79f1	Apalache	SeqSeq	SetEmpty	False	Passed	Model Under Test Equivalent Model
b5523b7f65e9f4e4ccbcdda14c64222f335f95ac	Apalache	SeqSeq	Set0	True	Passed	Model Under Test Equivalent Model
49ee8b08393433b9723837f44f8db0358c7ea917	Apalache	SeqSeq	Set0	False	Passed	Model Under Test Equivalent Model
275028cf8a193ac5c01d8951d4ff665c7382188b	Apalache	SeqSeq	Set1	True	Passed	Model Under Test Equivalent Model
d59baf9dc1623816134121128c2d205bea7ee502	Apalache	SeqSeq	Set1	False	Passed	Model Under Test Equivalent Model
c553224269f36340be8ff0add9b1e1a8f5eb4209	Apalache	SeqSeq	Set2	True	Passed	Model Under Test Equivalent Model
9fc5ecebc244abaf10dfa28077f1a1cdf3668bd8	Apalache	SeqSeq	Set2	False	Passed	Model Under Test Equivalent Model
2b8527a039f2637ab0c2283408008f95d9924d33	Apalache	SeqSeq	Choose	True	Passed	Model Under Test Equivalent Model
6a24a28b54e428ab444a0d84bfbb631b9a580bf5	Apalache	SeqSeq	Choose	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
13e590c6f19b4b93b743e1fa1c9eea37cc133015	Apalache	SeqSeq	Prime	True	Passed	Model Under Test Equivalent Model
9047603c3e5be7fa78aa956d8471d748a4ddb0a4	Apalache	SeqSeq	Prime	False	Passed	Model Under Test Equivalent Model
9fc2abbd07ff9041504263437c113489abaa41ed	Apalache	SeqSeq	Def0	True	Passed	Model Under Test Equivalent Model
b1eb75964d132fc2affe88c944f8cf5d0b938ecf	Apalache	SeqSeq	Def0	False	Passed	Model Under Test Equivalent Model
dcf34520e8eab4094332194615a3a1224523f686	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef0	True	Passed	Model Under Test Equivalent Model
2ca9b0d3fd8a0c8aeebb6a16275ca9ede96118b5	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef0	False	Passed	Model Under Test Equivalent Model
1171e3e66a46c23ee7d1baa4f6bcacecfa6c8590	Apalache	SeqSeq	Def1	True	Passed	Model Under Test Equivalent Model
70e22a049258d0441da2930764c260a180ebe998	Apalache	SeqSeq	Def1	False	Passed	Model Under Test Equivalent Model
8f09fcd914fc1756c9585448476727987e62ca39	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef1	True	Passed	Model Under Test Equivalent Model
e324d54e8c09146eebf15365032fab62c2b14214	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef1	False	Passed	Model Under Test Equivalent Model
d6f90c8af35fce14e979de7c6d3936fcda3c19e5	Apalache	SeqSeq	Def2	True	Passed	Model Under Test Equivalent Model
4d70dfc137ff755e229efe2d0de12fd717d2adaf	Apalache	SeqSeq	Def2	False	Passed	Model Under Test Equivalent Model
f7484f599561ba6ecf6973522f81230e0c2a2df9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef2	True	Passed	Model Under Test Equivalent Model
0305249785aeed64a2f7a90e1d386d4b8870afbe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef2	False	Passed	Model Under Test Equivalent Model
d7d565ff6ea95ef97b0c841a3c110c558fbdb8fb	Apalache	SeqSeq	Def1Recursive	True	Passed	Model Under Test Equivalent Model
fd5e4dfc98989b2b2d1aa7ce318c5f93d55ed8eb	Apalache	SeqSeq	Def1Recursive	False	Passed	Model Under Test Equivalent Model
adfcc24c37e64c9a507d90a113468425750fbccd	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
1f3ed7a0bd778195444edac754e9253e043e4d85	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	SeqSeq	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
b408013220f41c3ac51f85fa1f905bc7471dfdcb	Apalache	SeqSeq	Extends	True	Passed	Model Under Test Equivalent Model
52748114d4b5a738c5ae24859baef457dfdcba88	Apalache	SeqSeq	Extends	False	Passed	Model Under Test Equivalent Model
e7a70ef1cfe672ad5f29a2e9c2ae4776f125d7e6	Apalache	SeqSeq	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
1791c8201139b04ee033b05eb8f2bfac8b054990	Apalache	SeqSeq	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
10f9407d3048cd9bc465c5a2aa39c8a243ce585d	Apalache	SeqSeq	Variable	True	Passed	Model Under Test Equivalent Model
cfea068b8431cb74cd7f7b58ad5c0aa66b6ec47e	Apalache	SeqSeq	Variable	False	Passed	Model Under Test Equivalent Model
4ecc3ac22aa111fd81bf4f09711c82c681c350ba	Apalache	SeqSeq	Constant	True	Passed	Model Under Test Equivalent Model
31f0987dd363ed09707c53d3233125078aa75775	Apalache	SeqSeq	Constant	False	Passed	Model Under Test Equivalent Model
ef4fc1847bda9a95f8d116b4abbf4f33aadb4041	Apalache	SeqSeq	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ba759383cfe2e9ac7a27d5b5ff299bd0da770679	Apalache	SeqSeq	ConstantRank1	False	Passed	Model Under Test Equivalent Model
5b1df1b1d0002ac86125807fb93a9d8fa884f2e4	Apalache	SeqSeq	Instance	True	Passed	Model Under Test Equivalent Model
fbc9e978faf15254706914ca25ff8a27c2df36db	Apalache	SeqSeq	Instance	False	Passed	Model Under Test Equivalent Model
0a50a4aad2f2e5075cd44e1107ca99fff99faed2	Apalache	SeqSeq	InstanceWith	True	Passed	Model Under Test Equivalent Model
ef2ab75d2b19e85b35b235cef6d5344831b55319	Apalache	SeqSeq	InstanceWith	False	Passed	Model Under Test Equivalent Model
fe7e6cb82e2b242f2eee8d58ada3978633309f08	Apalache	SeqSeq	InstanceNamed	True	Passed	Model Under Test Equivalent Model
aeb62e5e766d8ee10dd639cc1c37eb8a3e3d4dbe	Apalache	SeqSeq	InstanceNamed	False	Passed	Model Under Test Equivalent Model
1e9e6e8268376503aedca3ade781c599b3b9566e	Apalache	SeqSeq	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
7d0992f3e8a14984573a1528500f6b2f7bb41c0b	Apalache	SeqSeq	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
3e23d9b183fcaa62a395a714768a5b967a936422	Apalache	SeqSeq	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
8eab66e89435e17c17238599c4d05d5feac8aed8	Apalache	SeqSeq	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
80af51657109e782610aeffd49c8b9e3768f1230	Apalache	SeqSeq	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
5ed7db65dcf1e1ee94770bd3797533c359305034	Apalache	SeqSeq	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
13127238d8e30502f707075d659890393053850b	Apalache	SeqSeq	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
06ed2f2708e43784b11d65113ab65d7a888e46d2	Apalache	SeqSeq	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
a395326bb0630f1d1b8c04914018aea299eba6d3	Apalache	SeqSeq	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
b651d9ca114d822ff26c9d9e2d070515f43adb87	Apalache	SeqSeq	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
73d35e6303f8197f8a10b163ed888fb5c5d325c8	Apalache	SeqSeq	Cross2	True	Passed	Model Under Test Equivalent Model
f8f6fb20d7a432b697756458b82b7b06198018a0	Apalache	SeqSeq	Cross2	False	Passed	Model Under Test Equivalent Model
70a73ae264fec9021cd6f2423891218714c20b0c	Apalache	SeqSeq	Cross3	True	Passed	Model Under Test Equivalent Model
af94c56f1f06e3f4af8c194217487c6d98c405ba	Apalache	SeqSeq	Cross3	False	Passed	Model Under Test Equivalent Model
f55f60b0b7150489df5851ce71acb05e4198a07e	TLC with reduction strategy: Plug 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))	SeqSeq	FunSet	True	Passed	Model Under Test Equivalent Model
1a8d1a3be3aad242b5cf7874ee063efd9c511f98	TLC with reduction strategy: Plug 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))	SeqSeq	FunSet	False	Passed	Model Under Test Equivalent Model
49e0c47c61dcc205ddf7e99f27abd1852fded1f8	TLC with reduction strategy: Plug 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)	SeqSeq	RecordSet	True	Passed	Model Under Test Equivalent Model
69273fad48b08886d68ce413775213853fdb9b7f	TLC with reduction strategy: Plug 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)	SeqSeq	RecordSet	False	Passed	Model Under Test Equivalent Model
f34dbb5e7b4d85a056aaddd9df14e279c89e247c	Apalache	SeqSeq	SetDiff	True	Passed	Model Under Test Equivalent Model
896641c522bf88122e5340555be5d084618ff9f5	Apalache	SeqSeq	SetDiff	False	Passed	Model Under Test Equivalent Model
ac607d85237a57ecd1eceef9c6b365182300b1d3	Apalache	SeqSeq	SetUnion	True	Passed	Model Under Test Equivalent Model
ac34bf4b2ceb269f2b99a169e3c50fef6c6ec6ac	Apalache	SeqSeq	SetUnion	False	Passed	Model Under Test Equivalent Model
495ec41fc537989bc02d6d3999e81e8a662d5946	Apalache	SeqSeq	SetIntersect	True	Passed	Model Under Test Equivalent Model
b60024d16f66654f58ba9969b9f79c45d7a14015	Apalache	SeqSeq	SetIntersect	False	Passed	Model Under Test Equivalent Model
6ab7793438241a51472db8e32ffeb8dc1e6e1568	Apalache	SeqSeq	IfCond	True	Passed	Model Under Test Equivalent Model
ebf949d7f90c022d101d24664534ad0c287ae7ad	Apalache	SeqSeq	IfCond	False	Passed	Model Under Test Equivalent Model
3aa9f83955c7f33617d9aa9d0d223f9b13e66720	Apalache	SeqSeq	IfThen	True	Passed	Model Under Test Equivalent Model
7348e351ae6450809d9a7599bc0da4d86495709f	Apalache	SeqSeq	IfThen	False	Passed	Model Under Test Equivalent Model
abb13b7fa19a22058ef71cee4dd3c475c240e939	Apalache	SeqSeq	IfElse	True	Passed	Model Under Test Equivalent Model
dd7f4696cb30fd8be8aabc5a4b4eaf0163fddef0	Apalache	SeqSeq	IfElse	False	Passed	Model Under Test Equivalent Model
274b58f49b919b6fefb3e95530a8396cb8f68813	Apalache	SeqSeq	Subset	True	Passed	Model Under Test Equivalent Model
59e6bcc2c4a7d7fd2599d801ee935e9c39d57f9a	Apalache	SeqSeq	Subset	False	Passed	Model Under Test Equivalent Model
3a64ad467a95389db49fda5e51a2aa4b7ab30c2b	Apalache	SeqSeq	Domain	True	Passed	Model Under Test Equivalent Model
fd934c0a2b54321bf22be7bc5cc7337e8cea76e4	Apalache	SeqSeq	Domain	False	Passed	Model Under Test Equivalent Model
a81897df44fa573f3569ec8f17424158a3c4295c	Apalache	SeqSeq	Union	True	Passed	Model Under Test Equivalent Model
0322777ec0aa0970e84b58553c74353b31a437b0	Apalache	SeqSeq	Union	False	Passed	Model Under Test Equivalent Model
565ea71bd4f22b6beb30f46e9e02300c44e50839	Apalache	SeqSeq	SeqSeq	True	Passed	Model Under Test Equivalent Model
9e40200b57c8392d0b74fcd69878b2b34f88d4b7	Apalache	SeqSeq	SeqSeq	False	Passed	Model Under Test Equivalent Model
e7d5262aa94a255dfbd4ba5e2f1e9a54c97c7e4f	Apalache	SeqSeq	NatSet	True	Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Nat)	Model Under Test Equivalent Model
2588a3aac4ad1d167993af497aa0ceab3769e752	Apalache	SeqSeq	NatSet	False	Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Nat)	Model Under Test Equivalent Model
c17231d50527c3e5fdfc42fbb77a8cb24db6f25b	Apalache	SeqSeq	IntSet	True	Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Int)	Model Under Test Equivalent Model
072786e1f8f0bf2d59e8b8468ac417a79ea7f6dc	Apalache	SeqSeq	IntSet	False	Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Int)	Model Under Test Equivalent Model
946adc71b46ca335f4f2296b5e2663058d378365	Apalache	SeqSeq	StringSet	True	Failed: TLC model check results are correct. Apalache does not support STRING (a set of all strings)	Model Under Test Equivalent Model
a181954a9ed6484934a9100b891c47b77136b55a	Apalache	SeqSeq	StringSet	False	Failed: TLC model check results are correct. Apalache does not support STRING (a set of all strings)	Model Under Test Equivalent Model
be0eb4e461138fd610c34566d14410479af4c41a	TLC with reduction strategy: Plug 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	SeqSeq	NumRange	True	Passed	Model Under Test Equivalent Model
faa46cefe499e9c0bd285f65e97089e8f0d35545	TLC with reduction strategy: Plug 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	SeqSeq	NumRange	False	Passed	Model Under Test Equivalent Model
6711d6aa60217297c00d2c0dd79410c4c4e233f6	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SeqSeq	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
f44d2461bcb27029745941109ea2ac675583a70b	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	SeqSeq	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
7c04912a77ffbd8a00e5bde97d90f73cb8ae35f7	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SeqSeq	TlcEval	True	Passed	Model Under Test Equivalent Model
2552da0bc856a40ad3c35d30191078f2bfc9e5f2	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	SeqSeq	TlcEval	False	Passed	Model Under Test Equivalent Model
fc411d8960a917ff61b8979ad1e6d3f9b8232222	Apalache	SeqSeq	BagBagToSet	True	Passed	Model Under Test Equivalent Model
1a2755b4b30e4af8e838265aaf8d9bcfac51991f	Apalache	SeqSeq	BagBagToSet	False	Passed	Model Under Test Equivalent Model
b903606e22f52fcb36e3b9670019bc11fa23c5b3	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SeqSeq	BagSubBag	True	Passed	Model Under Test Equivalent Model
a337f2f1bef4192bd9cecd63dc77c15f88d52a04	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	SeqSeq	BagSubBag	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

Index

Tests by case feature SeqSeq; CLI Option: -workers 1