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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
638aa6ef91772a2eb217d54a38c1f71519499738	Apalache	Eq	SeqAppend	True	Passed	Model Under Test Equivalent Model
26c346784ddf4fd30a62d9d8bf4ba1d4f859e81f	Apalache	Eq	SeqAppend	False	Passed	Model Under Test Equivalent Model
992de4f57e3be98439b3be549e8190ac0cd5d32c	Apalache	Ne	SeqAppend	True	Passed	Model Under Test Equivalent Model
1595422c375a25a8e81217db0936bfbfdc2b30cb	Apalache	Ne	SeqAppend	False	Passed	Model Under Test Equivalent Model
f94782943e93881e37e996b0b2ba77c90abc2068	Apalache	Let	SeqAppend	True	Passed	Model Under Test Equivalent Model
73c3462e1a3d848552b95b0ef26a625e2e3a880e	Apalache	Let	SeqAppend	False	Passed	Model Under Test Equivalent Model
e07d47d003041fa2998ca886e856a731f082df19	Apalache	Set0	SeqAppend	True	Passed	Model Under Test Equivalent Model
31b49e5d7b3607785c694d925ba2e61ca209f8f8	Apalache	Set0	SeqAppend	False	Passed	Model Under Test Equivalent Model
06723c972f711a2771d305ec73a9d439eff148ea	Apalache	Set1	SeqAppend	True	Passed	Model Under Test Equivalent Model
a42a6d008f84f73d17ac5db317a3c6bcdfa443af	Apalache	Set1	SeqAppend	False	Passed	Model Under Test Equivalent Model
15e8485859419f9c4099fef4a19b6c07847edb14	Apalache	Set2	SeqAppend	True	Passed	Model Under Test Equivalent Model
7d4b1ba53b793e635fd3091430caef27ca475df8	Apalache	Set2	SeqAppend	False	Passed	Model Under Test Equivalent Model
7d88b7df824422016c3c7178025752d849d62d38	Apalache	Fun	SeqAppend	True	Passed	Model Under Test Equivalent Model
86b6b86901e2b30a7736bf44c4bda0c8ff85271b	Apalache	Fun	SeqAppend	False	Passed	Model Under Test Equivalent Model
89cc5bc84a895a2ad41652b0262a66ba02020a62	Apalache	In	SeqAppend	True	Passed	Model Under Test Equivalent Model
7dfe35ac77eaa9da565733240d994bae531e0459	Apalache	In	SeqAppend	False	Passed	Model Under Test Equivalent Model
000498945f5c3cb226ca07ac4871ece923279ac7	Apalache	NotIn	SeqAppend	True	Passed	Model Under Test Equivalent Model
aed591c61ef66ed7a0a7ab72c4c0c84c8c464407	Apalache	NotIn	SeqAppend	False	Passed	Model Under Test Equivalent Model
2878769febd379ed363b34e6f20aa9b1c4cd9b97	Apalache	Record	SeqAppend	True	Passed	Model Under Test Equivalent Model
eff7fac0be2feba9f099786ff3b2ca837c0c5ea5	Apalache	Record	SeqAppend	False	Passed	Model Under Test Equivalent Model
b207a68b4dcb3023d54f2d81cd7a354de4b51307	Apalache	Tuple	SeqAppend	True	Passed	Model Under Test Equivalent Model
46ffb4e681e2efeefc2965f9076df23bfe4060e0	Apalache	Tuple	SeqAppend	False	Passed	Model Under Test Equivalent Model
e5cac48fc5250c540ed8ec191837737ce2b60909	Apalache	FunApp	SeqAppend	True	Passed	Model Under Test Equivalent Model
2e272c2bc44d6ce9aa008e09572cfeb30deacf15	Apalache	FunApp	SeqAppend	False	Passed	Model Under Test Equivalent Model
cdb1ba69f63bc435b34e165b27031eac3bbd21eb	Apalache	Except0	SeqAppend	True	Failed: Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, Append function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
6b0fa28307d11363d42c7c9bcc0c47f188897158	Apalache	Except0	SeqAppend	False	Failed: Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, Append function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
e156cd1e7d5f8ec7a92c7bf98f1e8aa56ad7b824	Apalache	Except1Fun	SeqAppend	True	Passed	Model Under Test Equivalent Model
158404d90e72eab4f71080cd10c8bb39fab8b9e2	Apalache	Except1Fun	SeqAppend	False	Passed	Model Under Test Equivalent Model
fd5334794a5d5d37da5890f7c77f3e2aff8654b0	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqAppend	True	Passed	Model Under Test Equivalent Model
b1a22366b80b60463a5e4ca52c10b094b3596782	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqAppend	False	Passed	Model Under Test Equivalent Model
dc7af58ce8853374e2e76c7ce3fe5eb048349782	Apalache	Except1Rec	SeqAppend	True	Passed	Model Under Test Equivalent Model
b4095a93786bd8fde7ef8dab5e3118058eeed29b	Apalache	Except1Rec	SeqAppend	False	Passed	Model Under Test Equivalent Model
c6114de411d8f5ab83efd7c6bd60184e0c35247b	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqAppend	True	Passed	Model Under Test Equivalent Model
d072a78a4ddbd13b520e70789fbd3704cbaf47f4	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqAppend	False	Passed	Model Under Test Equivalent Model
bd8747da00d90f7028bf3f6178f2abe81bded4a1	Apalache	Except2Fun	SeqAppend	True	Passed	Model Under Test Equivalent Model
59b5d9eaf7c38a31139c329c23963848dba7510f	Apalache	Except2Fun	SeqAppend	False	Passed	Model Under Test Equivalent Model
966515da4a58ae8648d7dd06a8c755a8de991731	Apalache	Prime	SeqAppend	True	Passed	Model Under Test Equivalent Model
9b80fae17bbe9e9713c92bc5f43bc3158dd50402	Apalache	Prime	SeqAppend	False	Passed	Model Under Test Equivalent Model
fa4f46b6bfc9755fd7a5a9c7fdf088a6e6e51423	Apalache	DefFun	SeqAppend	True	Passed	Model Under Test Equivalent Model
a69e096f7abda6c6a75f4dd1fee9d618251a5459	Apalache	DefFun	SeqAppend	False	Passed	Model Under Test Equivalent Model
c4736b3d573e0235ca258ac57c22e72218b47f1a	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqAppend	True	Passed	Model Under Test Equivalent Model
0211d0a4aa4b77b92c887076297948437a423f88	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqAppend	False	Passed	Model Under Test Equivalent Model
e2391e501a933b81b6005ef477c8165fa80784d1	Apalache	DefFunRecursive	SeqAppend	True	Passed	Model Under Test Equivalent Model
60d98222e3861036573adae334cca63a25669ea3	Apalache	DefFunRecursive	SeqAppend	False	Passed	Model Under Test Equivalent Model
5bb7c90fbce016b85bf6fcaef996fd35f35963dc	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqAppend	True	Passed	Model Under Test Equivalent Model
b3a91c500258012fc9ddb7f9fa1a6855f6802479	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqAppend	False	Passed	Model Under Test Equivalent Model
4376ac46987a60b14fce3ba55934be8b12502600	Apalache	Def0	SeqAppend	True	Passed	Model Under Test Equivalent Model
733f494b1030927d6446db2deaa159dc1655ec89	Apalache	Def0	SeqAppend	False	Passed	Model Under Test Equivalent Model
cc05fe817b8925279f62ba715a8715ef02809010	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqAppend	True	Passed	Model Under Test Equivalent Model
54532ff20edbf71d3c05babb99630820b11febcf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqAppend	False	Passed	Model Under Test Equivalent Model
fde633b3e7ecf2b798c4fe93edfc43d9f93535f8	Apalache	Def1	SeqAppend	True	Passed	Model Under Test Equivalent Model
99f5cac9a3e44f5ce4ed2174273aad6f3490902f	Apalache	Def1	SeqAppend	False	Passed	Model Under Test Equivalent Model
26db714723df9b8c6f67015657d864a71e3d76ea	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqAppend	True	Passed	Model Under Test Equivalent Model
0b8ec3806d6f9c23935ca9db26ded59a05a7e439	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqAppend	False	Passed	Model Under Test Equivalent Model
ef7c9a82e1a4bd1445a92e0af274f6f7f56a8bff	Apalache	Def2	SeqAppend	True	Passed	Model Under Test Equivalent Model
94892b3c49573deee792f6bd06930640667422fa	Apalache	Def2	SeqAppend	False	Passed	Model Under Test Equivalent Model
1a45dd82a4dcc3ccb774e30b2d64b5386828577c	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqAppend	True	Passed	Model Under Test Equivalent Model
f4362461c7aa01e30f36a45187a3118dfb969c64	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqAppend	False	Passed	Model Under Test Equivalent Model
7837d3a3c9e20ba820c6c317097ed5594a8b1d08	Apalache	Def1Recursive	SeqAppend	True	Passed	Model Under Test Equivalent Model
ddac5f95754cd18c7d01ae810128898457962e80	Apalache	Def1Recursive	SeqAppend	False	Passed	Model Under Test Equivalent Model
0e3aed9597dabb937c8a912cfbcbc4b1364e6537	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqAppend	True	Passed	Model Under Test Equivalent Model
31079c1aca6a6424a0ed6836160eb604ccf3cda9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqAppend	False	Passed	Model Under Test Equivalent Model
c2af88fda02c482911205b5fc5492c6e9b6fcfd2	Apalache	Extends	SeqAppend	True	Passed	Model Under Test Equivalent Model
338c5b3c662899db1b98877458ab0e3f4ade9832	Apalache	Extends	SeqAppend	False	Passed	Model Under Test Equivalent Model
7b0fc082a3e1d896e55d6da02f3bee1c15c00db6	Apalache	ExtendsInDifferentFolder	SeqAppend	True	Passed	Model Under Test Equivalent Model
c4712223e8c8b5646f4d59e316439f54dbe0233d	Apalache	ExtendsInDifferentFolder	SeqAppend	False	Passed	Model Under Test Equivalent Model
eee8d174c27c15d3e2c13e9eba0dfa7dff23201e	Apalache	Variable	SeqAppend	True	Passed	Model Under Test Equivalent Model
e695c95dd4f4e9cde6408aac71799196e0f45184	Apalache	Variable	SeqAppend	False	Passed	Model Under Test Equivalent Model
81075a200634074c1f2a2e7e4132d38b52477c9c	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqAppend	True	Passed	Model Under Test Equivalent Model
326a629db16f9bc2a9eff7620d3d51ff22c675bd	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqAppend	False	Passed	Model Under Test Equivalent Model
199051aea8c5d371a79630ce380e4a7664de9975	Apalache	Constant	SeqAppend	True	Passed	Model Under Test Equivalent Model
515f75e9e4f949f8cb66f5fbef2a41e172078a24	Apalache	Constant	SeqAppend	False	Passed	Model Under Test Equivalent Model
04496550f6dc3723a69022966517f2c415ac1138	Apalache	ConstantRank1	SeqAppend	True	Passed	Model Under Test Equivalent Model
50c2e36de55a0591aec864d70f904fcf5f52e614	Apalache	ConstantRank1	SeqAppend	False	Passed	Model Under Test Equivalent Model
3e5c8ba397f74a09d80567ab7a44fe466c215526	Apalache	Instance	SeqAppend	True	Passed	Model Under Test Equivalent Model
e7250b7a03989e3696a3040c3bac5b465169eb0f	Apalache	Instance	SeqAppend	False	Passed	Model Under Test Equivalent Model
76e5711423565978a6895d719dac1806a054a37d	Apalache	InstanceWith	SeqAppend	True	Passed	Model Under Test Equivalent Model
6d92edf5fa09eb71e0de495f9212b1ecae62c8e8	Apalache	InstanceWith	SeqAppend	False	Passed	Model Under Test Equivalent Model
29ca2781565dae348cd020085608616e81042e74	Apalache	InstanceNamed	SeqAppend	True	Passed	Model Under Test Equivalent Model
37ea7189b0564e5e2941a08ad97f896573ebe369	Apalache	InstanceNamed	SeqAppend	False	Passed	Model Under Test Equivalent Model
453f23e47c5b21d0bc4e1f044fd774ee106be7d6	Apalache	InstanceNamedWith	SeqAppend	True	Passed	Model Under Test Equivalent Model
952db76d7afc2e6de30771ec557102471380dcd8	Apalache	InstanceNamedWith	SeqAppend	False	Passed	Model Under Test Equivalent Model
f9afe6527c1d40eb44d95614cebed4a3875c297d	Apalache	InstanceInFolder	SeqAppend	True	Passed	Model Under Test Equivalent Model
96299d34d30b7391d5928bb5d543a4231d0efc9a	Apalache	InstanceInFolder	SeqAppend	False	Passed	Model Under Test Equivalent Model
3ea7ab8d784b970fa113bdd87f074d91d4729e30	Apalache	InstanceWithInFolder	SeqAppend	True	Passed	Model Under Test Equivalent Model
e88fe0cbbbcfd8dd95f83f366e9bc138039f60f5	Apalache	InstanceWithInFolder	SeqAppend	False	Passed	Model Under Test Equivalent Model
407294cb299e8f210b397bbcf8dcfca865c7c35e	Apalache	InstanceNamedInFolder	SeqAppend	True	Passed	Model Under Test Equivalent Model
1de1078b23cb12eda2192d3c35264297c8d89081	Apalache	InstanceNamedInFolder	SeqAppend	False	Passed	Model Under Test Equivalent Model
d551939ea081809e97d50a5d9ac1f56ee3df7a07	Apalache	InstanceNamedWithInFolder	SeqAppend	True	Passed	Model Under Test Equivalent Model
697568aea1eed7ac05d9906344eb59029d8457a3	Apalache	InstanceNamedWithInFolder	SeqAppend	False	Passed	Model Under Test Equivalent Model
12870e229ab7b1dd272be62a6bd5194f45ce514d	Apalache	Lambda	SeqAppend	True	Passed	Model Under Test Equivalent Model
76cb6beacea18c4b2a75114dc1a79a34fc644e47	Apalache	Lambda	SeqAppend	False	Passed	Model Under Test Equivalent Model
112e2598ae021d2d2cd440981babec7cb6e5c84e	Apalache	IfThen	SeqAppend	True	Passed	Model Under Test Equivalent Model
5a633de8c43de798a09ce2afd72b96f214a7b7b0	Apalache	IfThen	SeqAppend	False	Passed	Model Under Test Equivalent Model
78d7e9072debf4bef2fef9e20d3bb73efeae7ed2	Apalache	IfElse	SeqAppend	True	Passed	Model Under Test Equivalent Model
c79aa7f5c4a307ebe39a5b9a15748eb64bd918d3	Apalache	IfElse	SeqAppend	False	Passed	Model Under Test Equivalent Model
cdf855eae24d8a2f7eec91351c69752e0ceb597d	Apalache	Unchanged	SeqAppend	True	Passed	Model Under Test Equivalent Model
dab557c306a94737fd39913c9c0f93672375d9bf	Apalache	Unchanged	SeqAppend	False	Passed	Model Under Test Equivalent Model
2ba366bdcc1947b9aa2ffb963e69155b102b0646	Apalache	SeqLen	SeqAppend	True	Passed	Model Under Test Equivalent Model
8cc3bfc3a99ac8916992498386c1b3b63226448a	Apalache	SeqLen	SeqAppend	False	Passed	Model Under Test Equivalent Model
cf223dd65aedfdc194def26de3f5f5469261bb9c	Apalache	SeqConcat	SeqAppend	True	Passed	Model Under Test Equivalent Model
e9b6b22ce18cfd87579f6a3c0121afed557a1130	Apalache	SeqConcat	SeqAppend	False	Passed	Model Under Test Equivalent Model
a8135cf0fdcb13feaa8dd98a58765ae0fb1e8200	Apalache	SeqSelectSeq	SeqAppend	True	Passed	Model Under Test Equivalent Model
cd9049b3f99103f0024b76ba1497162cb41ccf0e	Apalache	SeqSelectSeq	SeqAppend	False	Passed	Model Under Test Equivalent Model
3d8d17a8e5919843f8d02a7e909bad2638721163	Apalache	SeqSubSeq	SeqAppend	True	Passed	Model Under Test Equivalent Model
535900323370181632623f7d7439c7cfd914b4f3	Apalache	SeqSubSeq	SeqAppend	False	Passed	Model Under Test Equivalent Model
1067d048089f430bd7b6a2183ca269a1b565d5e9	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqAppend	True	Passed	Model Under Test Equivalent Model
cae0add6200d1fcfe49748eabf4c5cd622e2fb5e	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqAppend	False	Passed	Model Under Test Equivalent Model
a4c09b7a5131d95b847a6232f548d4a1a83a23b0	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqAppend	True	Passed	Model Under Test Equivalent Model
fb677dd820a985500bb7345aadd80ef5c5875ddf	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqAppend	False	Passed	Model Under Test Equivalent Model
8790e82a5549b14c8ced4070411f0837f321217f	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqAppend	True	Passed	Model Under Test Equivalent Model
5d9a0a75bb5bbdf82b2e1e3285e45646fed902b5	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqAppend	False	Passed	Model Under Test Equivalent Model
0183267ffeb13fa1c2e3848072a3d5908676713f	Apalache	BagBagIn	SeqAppend	True	Passed	Model Under Test Equivalent Model
7acfe93e547482ec75116e4177b20a4ea4bbd7d5	Apalache	BagBagIn	SeqAppend	False	Passed	Model Under Test Equivalent Model
87aec7f9340ef0713dc2970f8b32cd9196992683	Apalache	BagCopiesIn	SeqAppend	True	Passed	Model Under Test Equivalent Model
6f03802da4baf4b4447024e528c5da1897f55784	Apalache	BagCopiesIn	SeqAppend	False	Passed	Model Under Test Equivalent Model
244c4638e656c8b6c6ece14c2b98f3004584c793	Apalache	SeqHead	SeqAppend	True	Passed	Model Under Test Equivalent Model
a634e75f6b0453ce3247869dcdf71708e835a2c0	Apalache	SeqHead	SeqAppend	False	Passed	Model Under Test Equivalent Model
6f845a544faca4bede9ccbca51640c667f0f6fcd	Apalache	SeqTail	SeqAppend	True	Passed	Model Under Test Equivalent Model
d4f39ca71d422cb072688d4a4c40999406d7c79e	Apalache	SeqTail	SeqAppend	False	Passed	Model Under Test Equivalent Model
8a5895c4351cbe183dc6583e028231f7a986bd48	Apalache	SeqAppend	SeqAppend	True	Passed	Model Under Test Equivalent Model
efe6f83daccc597384eb85dd7134be837f679024	Apalache	SeqAppend	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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