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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
f4520e56f9fae6f02ff8978fece2961c9c5054b5	Apalache	Eq	SeqTail	True	Passed	Model Under Test Equivalent Model
e0df7913a45914e27fe1d695a62ec3df96bc805d	Apalache	Eq	SeqTail	False	Passed	Model Under Test Equivalent Model
6b38137e037f191c01e94bb0353cb660a087f3c3	Apalache	Ne	SeqTail	True	Passed	Model Under Test Equivalent Model
c0e136056f1c47be5898be42602c2eadf497ac84	Apalache	Ne	SeqTail	False	Passed	Model Under Test Equivalent Model
d8c2c95ba67036fdeb382f3cf292fb2d1dcd535a	Apalache	Let	SeqTail	True	Passed	Model Under Test Equivalent Model
999175260707bd9d1a518606385e1098e3100c31	Apalache	Let	SeqTail	False	Passed	Model Under Test Equivalent Model
fbf77ae647369b8ca123bab34bd436a97a6f21a9	Apalache	Set0	SeqTail	True	Passed	Model Under Test Equivalent Model
a8e3a12562b368b4fd678746bddf88651fb24788	Apalache	Set0	SeqTail	False	Passed	Model Under Test Equivalent Model
3468d92c79ee336309c1af581186e6c8c90c84fa	Apalache	Set1	SeqTail	True	Passed	Model Under Test Equivalent Model
3829e9773c414a8d3da2c5b5ca0434a57f2da936	Apalache	Set1	SeqTail	False	Passed	Model Under Test Equivalent Model
d385bd8696cf2f10b334c5fc79fd96b154de902d	Apalache	Set2	SeqTail	True	Passed	Model Under Test Equivalent Model
4485ba7f507901a033abd921e20cb8e2c570387a	Apalache	Set2	SeqTail	False	Passed	Model Under Test Equivalent Model
f42bda6a2c75b521bc9339062a17a3bc660d98de	Apalache	Fun	SeqTail	True	Passed	Model Under Test Equivalent Model
da70f9e6c34ea4b236fc1b52990ca6653c7844f1	Apalache	Fun	SeqTail	False	Passed	Model Under Test Equivalent Model
394739d4b7e0b6e1d9ca04481ee62edcb8bc07a7	Apalache	In	SeqTail	True	Passed	Model Under Test Equivalent Model
40d838f042a757f600120cc7087cadb5a0bc7b87	Apalache	In	SeqTail	False	Passed	Model Under Test Equivalent Model
deb3a166239fe3237942aa488adbc83106619c99	Apalache	NotIn	SeqTail	True	Passed	Model Under Test Equivalent Model
21a4293cf813bb3f9f59d291dfe8a5ef3b34e2a3	Apalache	NotIn	SeqTail	False	Passed	Model Under Test Equivalent Model
4bbba3803e3b308f0730b715a5c0ec6f43983bda	Apalache	Record	SeqTail	True	Passed	Model Under Test Equivalent Model
9480281110f8df3b98c52b3ff1322c08aaf56d1d	Apalache	Record	SeqTail	False	Passed	Model Under Test Equivalent Model
47cbabfc2ff17618de02a039d9fe2df75b57492a	Apalache	Tuple	SeqTail	True	Passed	Model Under Test Equivalent Model
656471cabc670f639b4a744100dba6c2014c076d	Apalache	Tuple	SeqTail	False	Passed	Model Under Test Equivalent Model
b180a5b4624bd8aea0a581e8da5e3aacda085a61	Apalache	FunApp	SeqTail	True	Failed: SeqTail produces empty sequence and TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
b340fe3b08248a58461c6d0e26d654c6462d3059	Apalache	FunApp	SeqTail	False	Failed: SeqTail produces empty sequence and TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
e12db5064497d0de3d9b20ce5bd6ff71169cd11b	Apalache	Except0	SeqTail	True	Failed: Except0 uses CHOOSE to select an argument. CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
8a70e1ffbdd262912cbcd8e82292579147ec57a7	Apalache	Except0	SeqTail	False	Failed: Except0 uses CHOOSE to select an argument. CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
4ace3759f4b4824d03fe8fbf6af407a90a2713e3	Apalache	Except1Fun	SeqTail	True	Passed	Model Under Test Equivalent Model
49b45d467ac86e8aa2c6265a4c851d4a353f0881	Apalache	Except1Fun	SeqTail	False	Passed	Model Under Test Equivalent Model
8dd7caf7386e47f264033a8cba37cb7bcea5a947	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqTail	True	Passed	Model Under Test Equivalent Model
046381475e2a1f7a8b238928603bba91e93ac15d	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	SeqTail	False	Passed	Model Under Test Equivalent Model
26b3544024670e7f9aea20ecb35da31a75a13cdf	Apalache	Except1Rec	SeqTail	True	Passed	Model Under Test Equivalent Model
3c0cbc40202614c54d6d94c9d736cbfa4b2f8828	Apalache	Except1Rec	SeqTail	False	Passed	Model Under Test Equivalent Model
94cb5528739d21ef32a6331ac39ebb1b6fa1bea7	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqTail	True	Passed	Model Under Test Equivalent Model
2398cba01fb2bc130b6fae7b1e4f385894604899	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	SeqTail	False	Passed	Model Under Test Equivalent Model
8e38806eb2b791a8a5f251ea877ee6dfd5096238	Apalache	Except2Fun	SeqTail	True	Passed	Model Under Test Equivalent Model
b1ce641d43117366c18476322f3e6c862e0a8c70	Apalache	Except2Fun	SeqTail	False	Passed	Model Under Test Equivalent Model
945374b63a22a23bb3d2828dc18412c18812fc24	Apalache	Prime	SeqTail	True	Passed	Model Under Test Equivalent Model
6df8e0b32ce5e53d4028c496541763d9c8917fac	Apalache	Prime	SeqTail	False	Passed	Model Under Test Equivalent Model
1f9ac648800f5e536c327acd425d8a5470b9add6	Apalache	DefFun	SeqTail	True	Passed	Model Under Test Equivalent Model
e88c9ecfd06fd23fbfe4a9a5f1e9c6e338dced23	Apalache	DefFun	SeqTail	False	Passed	Model Under Test Equivalent Model
ddd26ff2688cfc715f08f2e700d981ceb63889cb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqTail	True	Passed	Model Under Test Equivalent Model
76c1ee8793efc20ffc574ad5a59875aab80a2497	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	SeqTail	False	Passed	Model Under Test Equivalent Model
9c7a34e79059c0c2aa0fa95ab9f7aca42b854949	Apalache	DefFunRecursive	SeqTail	True	Passed	Model Under Test Equivalent Model
5b8da886933cc5091202bc689f086eb52bbacf85	Apalache	DefFunRecursive	SeqTail	False	Passed	Model Under Test Equivalent Model
2f8ba48e4c239d1cd5d6b4999a3437d9b6ddd2ff	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqTail	True	Passed	Model Under Test Equivalent Model
5bd09c68835c7af7cbf47727cf3602bda75070df	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	SeqTail	False	Passed	Model Under Test Equivalent Model
90cc3208e6f37bd64669a8cf480fbec2841516ee	Apalache	Def0	SeqTail	True	Passed	Model Under Test Equivalent Model
7300af812e9c0405e17cdcf9343e9e8d0db016cc	Apalache	Def0	SeqTail	False	Passed	Model Under Test Equivalent Model
040ae552d87d3042e98039f485b6385f625c4a79	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqTail	True	Passed	Model Under Test Equivalent Model
8d3ce4fd03c3ac803e4002a187f79747eab6d21b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	SeqTail	False	Passed	Model Under Test Equivalent Model
70ea49ce445407f60bae052f194315e31caa1a55	Apalache	Def1	SeqTail	True	Passed	Model Under Test Equivalent Model
55ef4ec6f5cc895f4abdebfd464d9ec5091b8047	Apalache	Def1	SeqTail	False	Passed	Model Under Test Equivalent Model
aafa03dee3dc69e3ab7f77bbed42c1ab7821b97f	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqTail	True	Passed	Model Under Test Equivalent Model
219030e342244b2f7e9bad043e123a9b7b3d53e1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	SeqTail	False	Passed	Model Under Test Equivalent Model
17ea59f1d1ecfec961e3a86480c1521d1e4781eb	Apalache	Def2	SeqTail	True	Passed	Model Under Test Equivalent Model
ddd4d20b831882982c7015bcc5b5c3379809f0a8	Apalache	Def2	SeqTail	False	Passed	Model Under Test Equivalent Model
c82e2e80d0847fcea6b01b28c5fdfe8afce4d47e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqTail	True	Passed	Model Under Test Equivalent Model
4f3af0cb0e5b5e924ee33eabdbe3490a6b228e8b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	SeqTail	False	Passed	Model Under Test Equivalent Model
dfabd37ef951872c6c08a76034ccacfe67f05f31	Apalache	Def1Recursive	SeqTail	True	Passed	Model Under Test Equivalent Model
e1ce7892e98235af8bd53547fb12b6c4f8d5f82b	Apalache	Def1Recursive	SeqTail	False	Passed	Model Under Test Equivalent Model
51847f603687cfec26c847ece7a0e13b3fd2fb64	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqTail	True	Passed	Model Under Test Equivalent Model
f6f9033deac6d93adcca8d685ccc1bbbebe0e027	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	SeqTail	False	Passed	Model Under Test Equivalent Model
ccea100c75194e28894bf8a1a82ac17be47391b8	Apalache	Extends	SeqTail	True	Passed	Model Under Test Equivalent Model
d358346462a1f7de9a26a78453b22345b3b75b69	Apalache	Extends	SeqTail	False	Passed	Model Under Test Equivalent Model
3be0059883d6795496029c2da83caff7c241eee9	Apalache	ExtendsInDifferentFolder	SeqTail	True	Passed	Model Under Test Equivalent Model
c3fa9eb21f0ec7a99a99a4df258e84d783a0e661	Apalache	ExtendsInDifferentFolder	SeqTail	False	Passed	Model Under Test Equivalent Model
79f393b8da8d6af59b3bd053ba0d7b79b77d4da1	Apalache	Variable	SeqTail	True	Passed	Model Under Test Equivalent Model
335668ea5e7c56b604b7c3aaf15d56e16f29a829	Apalache	Variable	SeqTail	False	Passed	Model Under Test Equivalent Model
6f5a82ecbad85e1b2f13af848e019c195c716212	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqTail	True	Passed	Model Under Test Equivalent Model
074554577f68963ff92f9eb88802c4d8a5cc085d	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	SeqTail	False	Passed	Model Under Test Equivalent Model
ed00b33cc5edde4b895e2172f222ee066625c1dc	Apalache	Constant	SeqTail	True	Passed	Model Under Test Equivalent Model
e17d71f419666b7da6d350aac89678b352ab0abb	Apalache	Constant	SeqTail	False	Passed	Model Under Test Equivalent Model
d9508b0d4ebc1c5124a3089aed3b06cc1557e74a	Apalache	ConstantRank1	SeqTail	True	Passed	Model Under Test Equivalent Model
1217720be320fc300cd64e1563e6c9068d7fbae6	Apalache	ConstantRank1	SeqTail	False	Passed	Model Under Test Equivalent Model
ef311779ec41593eab15064ee3a7fd2929b88660	Apalache	Instance	SeqTail	True	Passed	Model Under Test Equivalent Model
d2fd1cc0ca2b2768b907394b943258d9bb5974cb	Apalache	Instance	SeqTail	False	Passed	Model Under Test Equivalent Model
8c7ad456321478e36d377b2a201e182fbc67b0f4	Apalache	InstanceWith	SeqTail	True	Passed	Model Under Test Equivalent Model
b0cfee773c8cca6634af8c7e3b03ff2a734d8235	Apalache	InstanceWith	SeqTail	False	Passed	Model Under Test Equivalent Model
70a6a63fc0e7deb89b9cbc15f6d5cf40a9565fb6	Apalache	InstanceNamed	SeqTail	True	Passed	Model Under Test Equivalent Model
c33fbde6d902737cc782b03f88fbcf0f3656907c	Apalache	InstanceNamed	SeqTail	False	Passed	Model Under Test Equivalent Model
3ddbd61c8b3bc7d676cc2141bc2eddd13c0d8390	Apalache	InstanceNamedWith	SeqTail	True	Passed	Model Under Test Equivalent Model
ca3b9428035e7b8affa0fa4f0a060b18ccb1d12e	Apalache	InstanceNamedWith	SeqTail	False	Passed	Model Under Test Equivalent Model
76b3b4b2a32a146556edf6e69582d5dcf14cd634	Apalache	InstanceInFolder	SeqTail	True	Passed	Model Under Test Equivalent Model
d6ef66fd8673139110e458b0995b5263ef7d6ac0	Apalache	InstanceInFolder	SeqTail	False	Passed	Model Under Test Equivalent Model
a8f86df3a98eff6b9f0f94a3b07dbae4818bcb74	Apalache	InstanceWithInFolder	SeqTail	True	Passed	Model Under Test Equivalent Model
5264a62e7b44a37d53ce9d186c65528307ad5260	Apalache	InstanceWithInFolder	SeqTail	False	Passed	Model Under Test Equivalent Model
a24b139bf76b899816e5afebe75f2a26d286a690	Apalache	InstanceNamedInFolder	SeqTail	True	Passed	Model Under Test Equivalent Model
223615b6a74295448fa2077a96e99e2c17c2866e	Apalache	InstanceNamedInFolder	SeqTail	False	Passed	Model Under Test Equivalent Model
1e31130c489790c069a62f885ad58be99810f766	Apalache	InstanceNamedWithInFolder	SeqTail	True	Passed	Model Under Test Equivalent Model
c767c5b7038780363dc3dcf2d5a6aea55619ab60	Apalache	InstanceNamedWithInFolder	SeqTail	False	Passed	Model Under Test Equivalent Model
aa79f780f6eb83e1cba719393893d7191024c3dd	Apalache	Lambda	SeqTail	True	Passed	Model Under Test Equivalent Model
21a5186cd3a2538fcd392b321177293bd85b446c	Apalache	Lambda	SeqTail	False	Passed	Model Under Test Equivalent Model
e172c730f9c6133566465f3489c57cc3ff4040de	Apalache	IfThen	SeqTail	True	Passed	Model Under Test Equivalent Model
839cc2f32fe9419ac03f3952335051b68578cb28	Apalache	IfThen	SeqTail	False	Passed	Model Under Test Equivalent Model
f6edac514b431c453fdc2b16c432522615ac71f1	Apalache	IfElse	SeqTail	True	Passed	Model Under Test Equivalent Model
10125f95e1e298ef8a3ea767a411b32780999303	Apalache	IfElse	SeqTail	False	Passed	Model Under Test Equivalent Model
486ee5c024c31a69b10dce2ea66b542cedce161a	Apalache	Unchanged	SeqTail	True	Passed	Model Under Test Equivalent Model
85c7c78b7a91810a8724e7917f404b45c475aaf7	Apalache	Unchanged	SeqTail	False	Passed	Model Under Test Equivalent Model
7a247acecda2bbf04712eda67fe4848810b60f41	Apalache	SeqLen	SeqTail	True	Passed	Model Under Test Equivalent Model
a36e5cdad98dcb9f6cb7020f8c9c2ac4c987b3bd	Apalache	SeqLen	SeqTail	False	Passed	Model Under Test Equivalent Model
4d9ff1d88061025fa3b13241f03903f8ed509311	Apalache	SeqConcat	SeqTail	True	Passed	Model Under Test Equivalent Model
106879e05bb18d9718033932d164c0c1a74d4297	Apalache	SeqConcat	SeqTail	False	Passed	Model Under Test Equivalent Model
1fff3c05a2ebe383d49a90249a6b59b403e762fc	Apalache	SeqSelectSeq	SeqTail	True	Passed	Model Under Test Equivalent Model
dec0f8b26e82a949d02966b797b88ddc59506865	Apalache	SeqSelectSeq	SeqTail	False	Passed	Model Under Test Equivalent Model
093b5c2b34aba6e26c00c1c26704f40caadb0ddd	Apalache	SeqSubSeq	SeqTail	True	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
899e9ddba7041cce422b9427fc6de31ff23e1c06	Apalache	SeqSubSeq	SeqTail	False	Failed: TLC requires the second argument of SeqSubSeq to be in domain of the sequence and returns an error otherwise. Apalache always returns some sequence	Model Under Test Equivalent Model
470e916f99b63e964e411608b19cc2a0d71f96db	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqTail	True	Passed	Model Under Test Equivalent Model
8bf887803ea67e0d4fe3284ffdc7556cb6ccd4e4	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	SeqTail	False	Passed	Model Under Test Equivalent Model
3e29c6d3bf4ab82efd1a54378c7d2f03462f9249	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqTail	True	Passed	Model Under Test Equivalent Model
96d546d49be56cbc0c50909882892a929469d9c9	TLC with reduction strategy: Case Feature: SortSeq(S) is reduced to equivalent sort implementation	TlcSortSeq	SeqTail	False	Passed	Model Under Test Equivalent Model
780cb464dab30b09011f33a4acb0066ffc34d338	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqTail	True	Passed	Model Under Test Equivalent Model
ddd237336b810daee519cec67fb5875c8ba0b028	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	SeqTail	False	Passed	Model Under Test Equivalent Model
a635d2e91aaf1d6cd0da73d99e288ccb23277834	Apalache	BagBagIn	SeqTail	True	Passed	Model Under Test Equivalent Model
9ec4ec7e3bc8456edd3ddf0aebfe1e4deb8b7e7a	Apalache	BagBagIn	SeqTail	False	Passed	Model Under Test Equivalent Model
729b78b06674f78af88a2673e381762ecabc4296	Apalache	BagCopiesIn	SeqTail	True	Passed	Model Under Test Equivalent Model
8a59a936d229623297fe4709831f4718c4b37920	Apalache	BagCopiesIn	SeqTail	False	Passed	Model Under Test Equivalent Model
40a2cd5141b4338d90ceb2a6ef7eb7dc3bf39f4b	Apalache	SeqHead	SeqTail	True	Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
b40b7b84fd06cc86dbc07d7161924a9dc068e129	Apalache	SeqHead	SeqTail	False	Failed: Head of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
a025967b62b9b305dac3dc23e62d7dc08fce8dac	Apalache	SeqTail	SeqTail	True	Failed: Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
1fd80d772f693595c15cddcefe33d780e62ce1d5	Apalache	SeqTail	SeqTail	False	Failed: Tail of empty sequence results in error in TLC. Apalache is unable to detect such an error and instead returns arbitrary value	Model Under Test Equivalent Model
c4c49339754f16cbb5824a429d57f4e89eff6ad1	Apalache	SeqAppend	SeqTail	True	Passed	Model Under Test Equivalent Model
8772c595232d31651255d9b362d65305384418c0	Apalache	SeqAppend	SeqTail	False	Passed	Model Under Test Equivalent Model

Index

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