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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
a4fa2167cb1fae3759135f7fec206820d9f5c5e4	Apalache	Eq	SeqConcat	True	Passed	Model Under Test Equivalent Model
5dc2e1706042e4f8be8e08e16fd2d749011208b0	Apalache	Eq	SeqConcat	False	Passed	Model Under Test Equivalent Model
4adccc9c7805cd6e8e77541383350e45a5864b40	Apalache	Ne	SeqConcat	True	Passed	Model Under Test Equivalent Model
16162eaa2a626965710680854e58ae16d24cafad	Apalache	Ne	SeqConcat	False	Passed	Model Under Test Equivalent Model
cd500fbde7d4221191e0399329a28fb2cbc5331f	Apalache	Let	SeqConcat	True	Passed	Model Under Test Equivalent Model
4c37adaef03b332589bac03d5b12d6d06c355958	Apalache	Let	SeqConcat	False	Passed	Model Under Test Equivalent Model
f9a2085ac3d218de371c34cdfdf03e2d7f8317c8	Apalache	Set0	SeqConcat	True	Passed	Model Under Test Equivalent Model
808fa026a4a2791baa94707dc8fbb0b577e387e7	Apalache	Set0	SeqConcat	False	Passed	Model Under Test Equivalent Model
a2b47f99b5c175b2568ba727bd79f1d54d4e38e8	Apalache	Set1	SeqConcat	True	Passed	Model Under Test Equivalent Model
7b4293b62bcae56e51e78ade148441e498c9c49d	Apalache	Set1	SeqConcat	False	Passed	Model Under Test Equivalent Model
dd89a57df30226c25d1df12d0c102ff5e6dba67d	Apalache	Set2	SeqConcat	True	Passed	Model Under Test Equivalent Model
ac10bf9a2be781eba7e99141fa9bae1aeb049f6a	Apalache	Set2	SeqConcat	False	Passed	Model Under Test Equivalent Model
9bc83b2cf9957a38b446eef951ec9f37a490b8d5	Apalache	Fun	SeqConcat	True	Passed	Model Under Test Equivalent Model
372628104e8a7d51e135700d72987d46447ce54e	Apalache	Fun	SeqConcat	False	Passed	Model Under Test Equivalent Model
9add2131c1abf7d4ec58aa00c408be27bd391f9a	Apalache	In	SeqConcat	True	Passed	Model Under Test Equivalent Model
a8a7fc2adeb5eea6e44def384fd1f67ad03542f8	Apalache	In	SeqConcat	False	Passed	Model Under Test Equivalent Model
26e19ab2425e3cf239e96a23b90819115092ae87	Apalache	NotIn	SeqConcat	True	Passed	Model Under Test Equivalent Model
97ed219615adc2649add57edd4dd154be22464b9	Apalache	NotIn	SeqConcat	False	Passed	Model Under Test Equivalent Model
bc63bd58a0fa0d2abf3bf3ba8a9c55fdd042b5bb	Apalache	Record	SeqConcat	True	Passed	Model Under Test Equivalent Model
c2a2016350127051ad240b3c310c90f62fc9894f	Apalache	Record	SeqConcat	False	Passed	Model Under Test Equivalent Model
11af5c5bbd29ba3ff9159264e6f6cdfb0f46d74a	Apalache	Tuple	SeqConcat	True	Passed	Model Under Test Equivalent Model
bb50326ba044ae57c8ccc81a0cbb1bc353802e38	Apalache	Tuple	SeqConcat	False	Passed	Model Under Test Equivalent Model
efab1f87ff3037f32b12688918c72c1b26663db7	Apalache	FunApp	SeqConcat	True	Passed	Model Under Test Equivalent Model
b04ed020ebc93141a5f5d3ea96d9f64ad413ddb9	Apalache	FunApp	SeqConcat	False	Passed	Model Under Test Equivalent Model
1388c118def13e467811caae1e2c5aa49f9d1e13	Apalache	Except0	SeqConcat	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, SeqConcat function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
9d9e6f88b9f6d5ce7ea072d881d513f0f97ccb57	Apalache	Except0	SeqConcat	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, SeqConcat function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
d9ed32645d2a0e603706bf1d878f456712fcadf6	Apalache	Except1Fun	SeqConcat	True	Passed	Model Under Test Equivalent Model
251af34439095ef9278a735d2405f5b0b9ea46f3	Apalache	Except1Fun	SeqConcat	False	Passed	Model Under Test Equivalent Model
01cb51c3bcafc56548132a3467fc27e7af9a7ef2	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqConcat	True	Passed	Model Under Test Equivalent Model
e80d734b0bbac40226c492bf4942dcb9b69926e9	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqConcat	False	Passed	Model Under Test Equivalent Model
01274723f9f1b8ee9a741ca97dc0791101162d9a	Apalache	Except1Rec	SeqConcat	True	Passed	Model Under Test Equivalent Model
ae6ce36e3ca7915f525f89796d9e480ab392319c	Apalache	Except1Rec	SeqConcat	False	Passed	Model Under Test Equivalent Model
ab60c2086502db49296459bcd4d1047944de1526	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqConcat	True	Passed	Model Under Test Equivalent Model
a371e80bcd2b0ad618d1ec6efc5d450599915dfc	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqConcat	False	Passed	Model Under Test Equivalent Model
6745cee984910016d616f0733183f4eb7a8a2064	Apalache	Except2Fun	SeqConcat	True	Passed	Model Under Test Equivalent Model
b91e4bd8d17124138c5f5ce95518980f03b56b55	Apalache	Except2Fun	SeqConcat	False	Passed	Model Under Test Equivalent Model
137498003d58135d791702ef9b9d3c6747b14b3d	Apalache	Prime	SeqConcat	True	Passed	Model Under Test Equivalent Model
5031dcb80133cc37049aebae2d8650eb559d28e8	Apalache	Prime	SeqConcat	False	Passed	Model Under Test Equivalent Model
358dd8b141f009994f0592915df07b8eee89260c	Apalache	DefFun	SeqConcat	True	Passed	Model Under Test Equivalent Model
7d7b52176c7aaa43d9e6c102f24caf7d439da680	Apalache	DefFun	SeqConcat	False	Passed	Model Under Test Equivalent Model
62525f05999f3e054e9fe63247452fd359e6b7f3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqConcat	True	Passed	Model Under Test Equivalent Model
269a07961efb5bc4b81534268d2aa5c8384a8909	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqConcat	False	Passed	Model Under Test Equivalent Model
4bfb06763b9e90510a5473c00b00a93944bf271b	Apalache	DefFunRecursive	SeqConcat	True	Passed	Model Under Test Equivalent Model
3f22434daf48c78836afa6286778ff2e979b22cd	Apalache	DefFunRecursive	SeqConcat	False	Passed	Model Under Test Equivalent Model
d83558b77d7c3fa19ee8d209ced10b73ba75cdd1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqConcat	True	Passed	Model Under Test Equivalent Model
74e7e9e87abb9f9516a9a07757a7edf56f86ec23	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqConcat	False	Passed	Model Under Test Equivalent Model
260ee2dd033f8cb0f5bcff1af791d3d6cebcc275	Apalache	Def0	SeqConcat	True	Passed	Model Under Test Equivalent Model
678935083c0812e31233e6d3a4c94ed432a4e24f	Apalache	Def0	SeqConcat	False	Passed	Model Under Test Equivalent Model
45622d9d3664a443f19b8f5b4a8d044f17a9154e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqConcat	True	Passed	Model Under Test Equivalent Model
a8428c18ec6f18a1504a2e925bf473408541b118	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqConcat	False	Passed	Model Under Test Equivalent Model
8ed8cd8abc40925309defcfe44c9b64f75e9820f	Apalache	Def1	SeqConcat	True	Passed	Model Under Test Equivalent Model
3ea8757a8ed777223ad4e3af4d845498ef3b3aee	Apalache	Def1	SeqConcat	False	Passed	Model Under Test Equivalent Model
8b3d61751d90bb8c1e91857aacec555861c6c3f0	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqConcat	True	Passed	Model Under Test Equivalent Model
8c20b0697476682986b91703bba5b894796ffb64	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqConcat	False	Passed	Model Under Test Equivalent Model
db2eca54ef7663c0001fd7058187bf5a6f999678	Apalache	Def2	SeqConcat	True	Passed	Model Under Test Equivalent Model
ad422d7876902915b6bd55975397178e6cbf9816	Apalache	Def2	SeqConcat	False	Passed	Model Under Test Equivalent Model
8076a4ff704ae9db293f975e198490b41ecf8767	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqConcat	True	Passed	Model Under Test Equivalent Model
a4c3122079db1a6c9acf712e0e197f0bb74bcdfd	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqConcat	False	Passed	Model Under Test Equivalent Model
a440b597d076dfc4c8afe9104af07e3693312dc9	Apalache	Def1Recursive	SeqConcat	True	Passed	Model Under Test Equivalent Model
2e736f7bd7d690f0cdd219b7bec248d8c134dc1f	Apalache	Def1Recursive	SeqConcat	False	Passed	Model Under Test Equivalent Model
dbe0ac354ab243ae7aa2f5b60b4a3127ab8dbd32	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqConcat	True	Passed	Model Under Test Equivalent Model
7a2e0101226923838324d59553c932ece817e269	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqConcat	False	Passed	Model Under Test Equivalent Model
ce9f9c8c04bb2368bc91b85085e339a4996c3924	Apalache	Extends	SeqConcat	True	Passed	Model Under Test Equivalent Model
0ec2d3af8c76e950333bcdaab025392c58c37fb1	Apalache	Extends	SeqConcat	False	Passed	Model Under Test Equivalent Model
76f9d71948d76d1266846e8572544aa25d3c373a	Apalache	ExtendsInDifferentFolder	SeqConcat	True	Passed	Model Under Test Equivalent Model
884e8dff2e764ef73eb5dcca470fa84aea9f24cb	Apalache	ExtendsInDifferentFolder	SeqConcat	False	Passed	Model Under Test Equivalent Model
a4aaa8771973357e394fb75d1d9edaec66196a29	Apalache	Variable	SeqConcat	True	Passed	Model Under Test Equivalent Model
b170c07fcdf4cf6a5be61dd0731c8a6528644e06	Apalache	Variable	SeqConcat	False	Passed	Model Under Test Equivalent Model
b4e96a3bb45ad0e938340ae91cd44f35af7a68c2	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqConcat	True	Passed	Model Under Test Equivalent Model
1a1a41ce8a3cec048beeacc66ed45bd7d650c194	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqConcat	False	Passed	Model Under Test Equivalent Model
8153ff7ea68fd0a7c27bdd9508b4fbea5de3753b	Apalache	Constant	SeqConcat	True	Passed	Model Under Test Equivalent Model
65d87087b66b73d08541a6e29e9e88cd949bc4da	Apalache	Constant	SeqConcat	False	Passed	Model Under Test Equivalent Model
6447548a96b696c47ed1b36a14581266369fac2a	Apalache	ConstantRank1	SeqConcat	True	Passed	Model Under Test Equivalent Model
4df250f34488bac2a3cb98c08870c9cfc3d33591	Apalache	ConstantRank1	SeqConcat	False	Passed	Model Under Test Equivalent Model
02b2bc2653aac5053b490280b39146765593058e	Apalache	Instance	SeqConcat	True	Passed	Model Under Test Equivalent Model
90e4a75d024b79559c98f77f5dbab2d2d72c2b15	Apalache	Instance	SeqConcat	False	Passed	Model Under Test Equivalent Model
449113738f692c2ea84105c8e416623b3ae63956	Apalache	InstanceWith	SeqConcat	True	Passed	Model Under Test Equivalent Model
21452302cd90f6f46a1c426a613656bf543e8a8c	Apalache	InstanceWith	SeqConcat	False	Passed	Model Under Test Equivalent Model
9090717358b50e319245d5927676a000fc11c6a3	Apalache	InstanceNamed	SeqConcat	True	Passed	Model Under Test Equivalent Model
cefdff889fcfbb6b6faf2338c9047b69ae5899bf	Apalache	InstanceNamed	SeqConcat	False	Passed	Model Under Test Equivalent Model
7fde190ef03c16012fb85fb0c19b9773b22c5cb7	Apalache	InstanceNamedWith	SeqConcat	True	Passed	Model Under Test Equivalent Model
63669592386164305ed67efd389ef5d6f3f9e9ad	Apalache	InstanceNamedWith	SeqConcat	False	Passed	Model Under Test Equivalent Model
da964dcb620149d5697ca4a639e4b4bcc4a921dd	Apalache	InstanceInFolder	SeqConcat	True	Passed	Model Under Test Equivalent Model
98ce98c68d4a350aec939915b3b5ebb5d02a2572	Apalache	InstanceInFolder	SeqConcat	False	Passed	Model Under Test Equivalent Model
79219f50b4241471aa7a275639a97f62f6f2f5dc	Apalache	InstanceWithInFolder	SeqConcat	True	Passed	Model Under Test Equivalent Model
a6736eb9a16c4b86cbc15a0960ee7141f878979b	Apalache	InstanceWithInFolder	SeqConcat	False	Passed	Model Under Test Equivalent Model
05ab5f08c85fe0990c5830b78b929e045b9e69b5	Apalache	InstanceNamedInFolder	SeqConcat	True	Passed	Model Under Test Equivalent Model
baa5bfa693d54b39056645a99dc664cfa57c1967	Apalache	InstanceNamedInFolder	SeqConcat	False	Passed	Model Under Test Equivalent Model
c4b5447047949773977d04fa0720b4d24ea65ee6	Apalache	InstanceNamedWithInFolder	SeqConcat	True	Passed	Model Under Test Equivalent Model
faf5c002fd72c36af71dc640b2d48f0da8bf3fa9	Apalache	InstanceNamedWithInFolder	SeqConcat	False	Passed	Model Under Test Equivalent Model
c8eafb801d4efa0159cbafd28b802fde48ec4106	Apalache	Lambda	SeqConcat	True	Passed	Model Under Test Equivalent Model
83188a46e6111cf1e7960b0d779c66f31f829c3d	Apalache	Lambda	SeqConcat	False	Passed	Model Under Test Equivalent Model
6a237f3ca89787c994a7bb6b29b935dfdf3d3b2c	Apalache	IfThen	SeqConcat	True	Passed	Model Under Test Equivalent Model
a966a103fe685a188a41119696b91c77ed6ecb19	Apalache	IfThen	SeqConcat	False	Passed	Model Under Test Equivalent Model
6060b17184b8558ba532a4568e5a2b370467c963	Apalache	IfElse	SeqConcat	True	Passed	Model Under Test Equivalent Model
a114e9e1a551b737c2d3a72b142d2e5e13bc9bba	Apalache	IfElse	SeqConcat	False	Passed	Model Under Test Equivalent Model
e824578f8641bece609c142ad631a5283ec26c12	Apalache	Unchanged	SeqConcat	True	Passed	Model Under Test Equivalent Model
582da95962268d365c45cc32cdd81da3d26ab89e	Apalache	Unchanged	SeqConcat	False	Passed	Model Under Test Equivalent Model
f8d7f0745abe82007eb27b9f3f370b5c8dcbe068	Apalache	SeqLen	SeqConcat	True	Passed	Model Under Test Equivalent Model
3978720031e0254dd7fbf0165bf8420415490e9a	Apalache	SeqLen	SeqConcat	False	Passed	Model Under Test Equivalent Model
d26ad0465d3a60025c1a040d1bb8de011fa18c24	Apalache	SeqConcat	SeqConcat	True	Passed	Model Under Test Equivalent Model
7bbbb2ca278b921f55b19b5ef00a90c85b2d0d22	Apalache	SeqConcat	SeqConcat	False	Passed	Model Under Test Equivalent Model
2b5f77cea9e979860b97401ffb3ca7196a1b3b1e	Apalache	SeqSelectSeq	SeqConcat	True	Passed	Model Under Test Equivalent Model
c227e5fbc24d14cae52b50c990f18af941208d0f	Apalache	SeqSelectSeq	SeqConcat	False	Passed	Model Under Test Equivalent Model
ab5739439a2474d4671140cea8b204def228e8b9	Apalache	SeqSubSeq	SeqConcat	True	Passed	Model Under Test Equivalent Model
ffd9f92596c46f4d30730d73c7f42787f6070ca2	Apalache	SeqSubSeq	SeqConcat	False	Passed	Model Under Test Equivalent Model
d99e52674e4b0b8685684bf88b1029e12e982570	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqConcat	True	Passed	Model Under Test Equivalent Model
a65d94fd71ea6443c6642052627c11ed43967cca	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqConcat	False	Passed	Model Under Test Equivalent Model
51c5655c220892f4e8cbfc831aba29a32de9d5bd	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqConcat	True	Passed	Model Under Test Equivalent Model
2b60edbb84dc41df8d48fd2951176d5dde38e1c7	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqConcat	False	Passed	Model Under Test Equivalent Model
77458b1e3840c881c0e881d2b4fa147c1ae86c67	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqConcat	True	Passed	Model Under Test Equivalent Model
8d1f7fed665dcc64f62a17c1b86afcdf7746d5db	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqConcat	False	Passed	Model Under Test Equivalent Model
71f92575dc6081108edbf4b5efbdb8d6b2c9d185	Apalache	BagBagIn	SeqConcat	True	Passed	Model Under Test Equivalent Model
8fb1bbf13028b68f66dec204420ad7ffdec7f4f1	Apalache	BagBagIn	SeqConcat	False	Passed	Model Under Test Equivalent Model
860f2a257ddadf77100e87713fcf90be4e6be456	Apalache	BagCopiesIn	SeqConcat	True	Passed	Model Under Test Equivalent Model
d63a6ce51a8521f2961b93bc9c6af9bb06ca2c25	Apalache	BagCopiesIn	SeqConcat	False	Passed	Model Under Test Equivalent Model
a2b7062f084c5147ce3e7cd355f1899fb6ae2499	Apalache	SeqHead	SeqConcat	True	Passed	Model Under Test Equivalent Model
6a241d0f4cb85632b268e9c9d24182b12f99738e	Apalache	SeqHead	SeqConcat	False	Passed	Model Under Test Equivalent Model
9f33fa5bc15d37ddc2e3638f1055b3eafb7c7a2b	Apalache	SeqTail	SeqConcat	True	Passed	Model Under Test Equivalent Model
20d8df5698da4f8f56ab9e81363c8e5bfcb98ce4	Apalache	SeqTail	SeqConcat	False	Passed	Model Under Test Equivalent Model
9d4d64b481e21bdbeca536b5cf46b379b46b1d0e	Apalache	SeqAppend	SeqConcat	True	Passed	Model Under Test Equivalent Model
97ac351f5ca5a9d04fe2e267d66f77dcd1739176	Apalache	SeqAppend	SeqConcat	False	Passed	Model Under Test Equivalent Model

Index

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