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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
bd3e98798a0fff4e8e75e24995e45df809bf4512	Apalache	Eq	SeqLen	True	Passed	Model Under Test Equivalent Model
a882d822aa2e6f8740f5e68c31fed02efa72597d	Apalache	Eq	SeqLen	False	Passed	Model Under Test Equivalent Model
f5d1f50294de386ac5d81b005a324cfb0930855e	Apalache	Ne	SeqLen	True	Passed	Model Under Test Equivalent Model
03b5dff48afe0f225291add700d56ab72931a442	Apalache	Ne	SeqLen	False	Passed	Model Under Test Equivalent Model
0427a1d7a77a11d2151c606a1e626ef0f6ab0fd8	Apalache	Let	SeqLen	True	Passed	Model Under Test Equivalent Model
a95541ec83ae43e3e8fae8cfe24aa1a0eb1433d2	Apalache	Let	SeqLen	False	Passed	Model Under Test Equivalent Model
99eaada77545876aa977173c51fb836d780f7dcc	Apalache	Set0	SeqLen	True	Passed	Model Under Test Equivalent Model
9c1bb3ab10af1b767227069fc5680f45710c389f	Apalache	Set0	SeqLen	False	Passed	Model Under Test Equivalent Model
c3b40be2dd519181b839c591f88816911f2a104c	Apalache	Set1	SeqLen	True	Passed	Model Under Test Equivalent Model
f6f84811fdea8525b0e01fdb5b93452095981d75	Apalache	Set1	SeqLen	False	Passed	Model Under Test Equivalent Model
6ce2802ed1093f0c54cc91d8e9ab345f88f35b8d	Apalache	Set2	SeqLen	True	Passed	Model Under Test Equivalent Model
e1d3ebc588d0cc76601ad0bc0b9acbd9b192ecbf	Apalache	Set2	SeqLen	False	Passed	Model Under Test Equivalent Model
b4f52f28b8d84fe2247410462656415293e28550	Apalache	Fun	SeqLen	True	Passed	Model Under Test Equivalent Model
ed754f7305f956e831adad7e6dfadb7453f5a83f	Apalache	Fun	SeqLen	False	Passed	Model Under Test Equivalent Model
569658de138456a43f894978ae3f0a59cb27fabf	Apalache	In	SeqLen	True	Passed	Model Under Test Equivalent Model
e1187df0c2aedc760eeb6741afe2ed535417eb4f	Apalache	In	SeqLen	False	Passed	Model Under Test Equivalent Model
becc182c05065a2c38c09074f5403450538eb219	Apalache	NotIn	SeqLen	True	Passed	Model Under Test Equivalent Model
aadf369c06f72d800b292e2d89aa012190f70c9f	Apalache	NotIn	SeqLen	False	Passed	Model Under Test Equivalent Model
27a7b0c09ae36a567e1f1c9091b431c79c52640b	Apalache	Record	SeqLen	True	Passed	Model Under Test Equivalent Model
092af55a50d9a6f43813e866b3860c1d7f8b6ac6	Apalache	Record	SeqLen	False	Passed	Model Under Test Equivalent Model
ce41463fba3c4061219ce4b6706a88a534b64655	Apalache	Tuple	SeqLen	True	Passed	Model Under Test Equivalent Model
97517ec5860a2ef23207ff92bfeddb625fdddd16	Apalache	Tuple	SeqLen	False	Passed	Model Under Test Equivalent Model
83d789a6ec0a2a37f2c2db34d01288bb1a20a283	Apalache	FunApp	SeqLen	True	Passed	Model Under Test Equivalent Model
fde6032c852dbcec04a04c8362a64785817145bb	Apalache	FunApp	SeqLen	False	Passed	Model Under Test Equivalent Model
9a9da1e179e443e82283c690a48d3cdf68a203c6	Apalache	Except1Fun	SeqLen	True	Passed	Model Under Test Equivalent Model
11b1de98ae6295be422d0f7cb440304af3cc0727	Apalache	Except1Fun	SeqLen	False	Passed	Model Under Test Equivalent Model
96c7e13c51a5839393936ce0f456ca69f9e20b63	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqLen	True	Passed	Model Under Test Equivalent Model
69f90cb3338fd5f53f2fa21f9292d39801dafe0e	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqLen	False	Passed	Model Under Test Equivalent Model
ca64ac782b474625606d0c415d52766cf6dc94cb	Apalache	Except1Rec	SeqLen	True	Passed	Model Under Test Equivalent Model
f7f373ec2e27408af75e9f80ade2aaf616bbf255	Apalache	Except1Rec	SeqLen	False	Passed	Model Under Test Equivalent Model
99a1af680d8df2c6bb2ee15da983d8bac40562a4	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqLen	True	Passed	Model Under Test Equivalent Model
a9e12580d0c236976c57f294c05c06d69ab620f0	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqLen	False	Passed	Model Under Test Equivalent Model
c4b44af6d6ef757abc73bdb9a442c4979b8e8cce	Apalache	Except2Fun	SeqLen	True	Passed	Model Under Test Equivalent Model
17e436e3eb96fce2f270dd85665f95d68218aedc	Apalache	Except2Fun	SeqLen	False	Passed	Model Under Test Equivalent Model
2b08740dace24b6c3201ab4b75852eb314c15c4c	Apalache	Prime	SeqLen	True	Passed	Model Under Test Equivalent Model
e9cfbaa5bbaa645f759a7c3c30d1e560362b317a	Apalache	Prime	SeqLen	False	Passed	Model Under Test Equivalent Model
e92a7fdcde8eb86bd03a7693ae7a786aaf1e6836	Apalache	NumUnaryMinus	SeqLen	True	Passed	Model Under Test Equivalent Model
c12d20a3f4fb85aedd0d57ceaeeb2ce199e9ce5f	Apalache	NumUnaryMinus	SeqLen	False	Passed	Model Under Test Equivalent Model
ecd85705225b40fffa13e2676088631fda3a75a2	Apalache	NumPlus	SeqLen	True	Passed	Model Under Test Equivalent Model
865f6949dd2ac7d772b1a6962afc41ba7e534c55	Apalache	NumPlus	SeqLen	False	Passed	Model Under Test Equivalent Model
91917c92f3137a09d58c0eb91c455f1451a2f79a	Apalache	NumMinus	SeqLen	True	Passed	Model Under Test Equivalent Model
2790f9cf4e3006afac3f8bd9d3efc550755d6044	Apalache	NumMinus	SeqLen	False	Passed	Model Under Test Equivalent Model
18d7f00bc0e16ee69ffbe6080555d92ffc931879	Apalache	NumMul	SeqLen	True	Passed	Model Under Test Equivalent Model
39525a8b1188ac8464a6dba6004b3e2751e7e1b5	Apalache	NumMul	SeqLen	False	Passed	Model Under Test Equivalent Model
0e8b83db0bd8c3e609d47ff323f4b4b0a680ddf2	Apalache	NumDiv	SeqLen	True	Passed	Model Under Test Equivalent Model
54fb88d1b4c086334123587740bf9d16d2d18b8b	Apalache	NumDiv	SeqLen	False	Passed	Model Under Test Equivalent Model
186fb7d31d49712becba5beb76f0d2f37033a684	Apalache	NumMod	SeqLen	True	Passed	Model Under Test Equivalent Model
af1a3c859717490b13c087529479fb478a13eb63	Apalache	NumMod	SeqLen	False	Passed	Model Under Test Equivalent Model
84b52cbf599aa55d5977f1fd2ebbfbd9b3a4adcb	Apalache	NumPow	SeqLen	True	Passed	Model Under Test Equivalent Model
bf934c0b8bc5dab1a14e0ce1e2c3559427b8aed0	Apalache	NumPow	SeqLen	False	Passed	Model Under Test Equivalent Model
305f51d074417881e597b8805954d879ec63ff2b	Apalache	NumGt	SeqLen	True	Passed	Model Under Test Equivalent Model
821dbe2d403f1268687897ab9d7cf0e3922f2ef9	Apalache	NumGt	SeqLen	False	Passed	Model Under Test Equivalent Model
9b3c1fe1b76ee9f871501a724756413a1259a050	Apalache	NumGe	SeqLen	True	Passed	Model Under Test Equivalent Model
0bceb841651ab1d31b69cc742e7725b761fee3e1	Apalache	NumGe	SeqLen	False	Passed	Model Under Test Equivalent Model
005cd21aaca46285d29e8debc63e185eb3a2f059	Apalache	NumLt	SeqLen	True	Passed	Model Under Test Equivalent Model
fd20965308e047275e89bb3060e2bb5f81b16c43	Apalache	NumLt	SeqLen	False	Passed	Model Under Test Equivalent Model
fb2af25fd421f8fe1cd541c1c306bceaf8758884	Apalache	NumLe	SeqLen	True	Passed	Model Under Test Equivalent Model
befe62a808c9e8a1c84b4039e0faf3650b949163	Apalache	NumLe	SeqLen	False	Passed	Model Under Test Equivalent Model
5e655a0317a2c34fe6db6d9204b71bfc419e9c57	Apalache	DefFun	SeqLen	True	Passed	Model Under Test Equivalent Model
3ad2c5f8224fbb673c20a4778b26a9e24b2268b7	Apalache	DefFun	SeqLen	False	Passed	Model Under Test Equivalent Model
ee2b3fb4cd8c86caacc7be5a4476f0a909d8878c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqLen	True	Passed	Model Under Test Equivalent Model
72bb32f24902d83d30ccb3410811a3fb6679f589	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqLen	False	Passed	Model Under Test Equivalent Model
5886df4aa4f7c245db12a4d93a94d11a5156a78a	Apalache	DefFunRecursive	SeqLen	True	Passed	Model Under Test Equivalent Model
2c97b69b9da7da9ec44aaba0ed2009e60bd5bd80	Apalache	DefFunRecursive	SeqLen	False	Passed	Model Under Test Equivalent Model
b34fd5b3dc659702f083e4522d42737022194373	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqLen	True	Passed	Model Under Test Equivalent Model
0cb269d2e55f87e41c5958440a7b0e0bdf7bcb94	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqLen	False	Passed	Model Under Test Equivalent Model
71e4c5e97f0baeb17ba2bddd36c49136effad7f7	Apalache	Def0	SeqLen	True	Passed	Model Under Test Equivalent Model
5ff9b8bb06432f8bd71eafeb414acbd5372fa41b	Apalache	Def0	SeqLen	False	Passed	Model Under Test Equivalent Model
d5bfb852660adc0a7c9cd24ee3896dff2be42e0e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqLen	True	Passed	Model Under Test Equivalent Model
e065e1feb54b5c474b3c0ee8ebcd75f59e8e853f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqLen	False	Passed	Model Under Test Equivalent Model
c6fd04dac62f826f96eb478a054b9e529080b9c6	Apalache	Def1	SeqLen	True	Passed	Model Under Test Equivalent Model
c7a4eaab357269a4360ec76a045887229a5fe0b6	Apalache	Def1	SeqLen	False	Passed	Model Under Test Equivalent Model
60258c4cf0f7103144fedaf5e08056358a0c19e5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqLen	True	Passed	Model Under Test Equivalent Model
7426260e8dfe188b66ccb208555216aa3677de0b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqLen	False	Passed	Model Under Test Equivalent Model
9620f490d98fd71863be9084da626cd1da6d15e1	Apalache	Def2	SeqLen	True	Passed	Model Under Test Equivalent Model
95143c4d7303280f8814c2166d72d27abb04ae83	Apalache	Def2	SeqLen	False	Passed	Model Under Test Equivalent Model
e2e65caf3d0157bb85628a2c05eea5f0ac2f97b2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqLen	True	Passed	Model Under Test Equivalent Model
73e06833eb583e2d188e971da2cb18362ed47d6a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqLen	False	Passed	Model Under Test Equivalent Model
b34ee9f48191a1654473a4d379b78bcf37cb325c	Apalache	Def1Recursive	SeqLen	True	Passed	Model Under Test Equivalent Model
5683094fbad7e8f223c0eca18a30cb44c0c53e62	Apalache	Def1Recursive	SeqLen	False	Passed	Model Under Test Equivalent Model
9bae6e5067e25d8c6feff240840a4bdc6fe62006	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqLen	True	Passed	Model Under Test Equivalent Model
ebb79db7fa92c3ff553763100fb7e9681ef153f7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqLen	False	Passed	Model Under Test Equivalent Model
76b3a644a9a50a2079173628478ad9de0128e0b5	Apalache	Extends	SeqLen	True	Passed	Model Under Test Equivalent Model
df78ec29c6c60576d25b50bf80203f7074e5717a	Apalache	Extends	SeqLen	False	Passed	Model Under Test Equivalent Model
af6d9215acac98809d4b9bf0257eed434c33a083	Apalache	ExtendsInDifferentFolder	SeqLen	True	Passed	Model Under Test Equivalent Model
20a52c0facef200479d41b36d885a341529c78d5	Apalache	ExtendsInDifferentFolder	SeqLen	False	Passed	Model Under Test Equivalent Model
3b52544e3856149af47e8aa553b60aa31e52311a	Apalache	Variable	SeqLen	True	Passed	Model Under Test Equivalent Model
c91432dfde1a0ad852600750e2cc3a5fa8aaa49b	Apalache	Variable	SeqLen	False	Passed	Model Under Test Equivalent Model
e758a79aea6897cedc5db1313a07724be69fb377	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqLen	True	Passed	Model Under Test Equivalent Model
23a80c79b874074699ae183e9ae4d7de9d83ab52	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqLen	False	Passed	Model Under Test Equivalent Model
68abf4910499f1d7cd22d3e659e86fe8a50a2f77	Apalache	Constant	SeqLen	True	Passed	Model Under Test Equivalent Model
5f6d8cca86e102585073bcf71bde0116acb32975	Apalache	Constant	SeqLen	False	Passed	Model Under Test Equivalent Model
74dfda55d33cdcd030ebf7f37c3d5250b01fc3ab	Apalache	ConstantRank1	SeqLen	True	Passed	Model Under Test Equivalent Model
dbd8f391a1a9a117aaa4d93460ceab5ad4601c47	Apalache	ConstantRank1	SeqLen	False	Passed	Model Under Test Equivalent Model
9d3e64badf2574dd79d7c911e86267067c90ef35	Apalache	Instance	SeqLen	True	Passed	Model Under Test Equivalent Model
82477bfc218d05a72c1ab8d0033e1ce61f36df12	Apalache	Instance	SeqLen	False	Passed	Model Under Test Equivalent Model
2969a31491962eb044d388ac8da50a9e98658c6b	Apalache	InstanceWith	SeqLen	True	Passed	Model Under Test Equivalent Model
523e73d92a04cb7daf9ef87221e1bce12f2a8e14	Apalache	InstanceWith	SeqLen	False	Passed	Model Under Test Equivalent Model
d7a5cddc1f8dfd78218e6326566f801f53347711	Apalache	InstanceNamed	SeqLen	True	Passed	Model Under Test Equivalent Model
0dc503d628cee5829389383f873efbad1399fd67	Apalache	InstanceNamed	SeqLen	False	Passed	Model Under Test Equivalent Model
bca86727abe40e6a808817641cde4c1983d05445	Apalache	InstanceNamedWith	SeqLen	True	Passed	Model Under Test Equivalent Model
d40194c692f425e6c1553892b417c38e5b08ee1c	Apalache	InstanceNamedWith	SeqLen	False	Passed	Model Under Test Equivalent Model
e1f7ab4eeaf94ca9f4236baf23f21066cf4552a6	Apalache	InstanceInFolder	SeqLen	True	Passed	Model Under Test Equivalent Model
10a44c3109f7c331ed287f40f3a7cfa8a1a5c94e	Apalache	InstanceInFolder	SeqLen	False	Passed	Model Under Test Equivalent Model
5996825c864bdb04d4c7d71ec245f1f7c88dda47	Apalache	InstanceWithInFolder	SeqLen	True	Passed	Model Under Test Equivalent Model
c95b2d6e3d8dd148dbc942b953e53eae881c68c6	Apalache	InstanceWithInFolder	SeqLen	False	Passed	Model Under Test Equivalent Model
bc47fbb604e4b90ca99291a2b54778c10d73f40c	Apalache	InstanceNamedInFolder	SeqLen	True	Passed	Model Under Test Equivalent Model
f7f7232c5ff8bfb54fe63f55f679ca797e231735	Apalache	InstanceNamedInFolder	SeqLen	False	Passed	Model Under Test Equivalent Model
a6d6277f3ea1e94169f104ad80330b5fa32da1d9	Apalache	InstanceNamedWithInFolder	SeqLen	True	Passed	Model Under Test Equivalent Model
4b7e1e670839b39d3d7fca75f219e4391765ecb8	Apalache	InstanceNamedWithInFolder	SeqLen	False	Passed	Model Under Test Equivalent Model
6d839b8f4eae3cfdb796e9c333674d30b4ea3b51	Apalache	Lambda	SeqLen	True	Passed	Model Under Test Equivalent Model
e638e36c7f68d7eaef2d6f3b263e0b83e29eddd9	Apalache	Lambda	SeqLen	False	Passed	Model Under Test Equivalent Model
26aac5f135d015f0173978f04c4122bbca4f847b	Apalache	IfThen	SeqLen	True	Passed	Model Under Test Equivalent Model
3712d9d0526789a74072498d9bc3c11953675991	Apalache	IfThen	SeqLen	False	Passed	Model Under Test Equivalent Model
3689a0f5aa9192e6d31e99afadf9d7c3c1c61bff	Apalache	IfElse	SeqLen	True	Passed	Model Under Test Equivalent Model
68f063f7c481e9eb1125fd310e7e8aa2880185cd	Apalache	IfElse	SeqLen	False	Passed	Model Under Test Equivalent Model
83dedf2cce82780b2aa9e10853d7a12aa9ac7c83	Apalache	Unchanged	SeqLen	True	Passed	Model Under Test Equivalent Model
3b792ece826a2c385b8aae552dfbe1bfceb164fe	Apalache	Unchanged	SeqLen	False	Passed	Model Under Test Equivalent Model
598ac9f2427e7fb3e20383fb5ec45968216f431b	Apalache	SeqSubSeq	SeqLen	True	Passed	Model Under Test Equivalent Model
1169139ea84fe6806dfb312ee6a8476e60981b14	Apalache	SeqSubSeq	SeqLen	False	Passed	Model Under Test Equivalent Model
0e95a5eb27beaaef4135fb43a654532238d16d88	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	SeqLen	True	Passed	Model Under Test Equivalent Model
ae7ac63f2b2716613a3cd82dc1c0b6cb11a7e787	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	SeqLen	False	Passed	Model Under Test Equivalent Model
c3ccf9c69adb6555537fd6a43ca164c2db8f2c66	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqLen	True	Passed	Model Under Test Equivalent Model
50ec207fc4d6804ab6e4143d63b46c4624d9da85	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqLen	False	Passed	Model Under Test Equivalent Model
ffde67212a90450a4411967fad7790f5945adcd8	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqLen	True	Passed	Model Under Test Equivalent Model
8a439ca6a11fb062feabe028416ad635ed7d3d21	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqLen	False	Passed	Model Under Test Equivalent Model
9efae0eed0eecd7f34c9ad12a1118efcda4bf484	Apalache	BagBagIn	SeqLen	True	Passed	Model Under Test Equivalent Model
eb565612430f9d5ce960957c990c770e1f867c47	Apalache	BagBagIn	SeqLen	False	Passed	Model Under Test Equivalent Model
1a6fefa205832080f90ea5dc3cbd60553d3fb1ed	Apalache	BagCopiesIn	SeqLen	True	Passed	Model Under Test Equivalent Model
24f4ae86d2f0533b3adcaea6d63cf2a25a95d4f6	Apalache	BagCopiesIn	SeqLen	False	Passed	Model Under Test Equivalent Model
f994d0ce9e0a9da3cca480171476e89e736e641d	Apalache	SeqAppend	SeqLen	True	Passed	Model Under Test Equivalent Model
44eae72946dc3b266db4e865a9f68b40a07a222a	Apalache	SeqAppend	SeqLen	False	Passed	Model Under Test Equivalent Model

Index

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