Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
232876f3e2152f7d02679b9e00bca651ec1dbcfd TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqTail OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
6cb32fe15933796824a8bcbc7c5060bc5b0b2ba5 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqTail OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
befb7d3aa23769f8080617dbaad9990f453f2d6c TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqTail MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
7c617dae63c46ca4643787dd6909b47c8d9f8b28 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SeqTail MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
32da7a832813b1cdf53d9b2e2e576c30e6048c5f Apalache SeqTail Let True Passed
  • Model Under Test
  • Equivalent Model
7b26be91c74e03878217185d34a8402215f0e760 Apalache SeqTail Let False Passed
  • Model Under Test
  • Equivalent Model
8b71a908b9019391925b4378465f59d49b1232ab Apalache SeqTail Choose True Passed
  • Model Under Test
  • Equivalent Model
0a04b1c32f08d66076e714fc9675ddf06a5ec4c4 Apalache SeqTail Choose False Passed
  • Model Under Test
  • Equivalent Model
0d829414bd98d4084911d5677b3ec5f57c7d212f Apalache SeqTail Tuple True Passed
  • Model Under Test
  • Equivalent Model
5ab48fc2b473bca02991004ba9c98fa03b4b4a46 Apalache SeqTail Tuple False Passed
  • Model Under Test
  • Equivalent Model
cd16e1f8c4d71514b565193260eedc22a3183858 Apalache SeqTail TupleEmpty 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
fc8253e6317e8891a7069c098f558350613a8404 Apalache SeqTail TupleEmpty 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
9f236c2cdfc3f61718dd9a83223065b2ab3998e8 Apalache SeqTail FunApp True Passed
  • Model Under Test
  • Equivalent Model
453969ff0097c6115f554d24437b4766129da1c4 Apalache SeqTail FunApp False Passed
  • Model Under Test
  • Equivalent Model
55aa45430186f3e4e466ad4a020213b04f77f290 Apalache SeqTail Prime True Passed
  • Model Under Test
  • Equivalent Model
016e6a26d887a17cf667bc7625cba442a38b669a Apalache SeqTail Prime False Passed
  • Model Under Test
  • Equivalent Model
006dbf16a08e9c46027c234ffaaf86359482e4c0 Apalache SeqTail Def0 True Passed
  • Model Under Test
  • Equivalent Model
8267e85ff8eccabdbb3febf2671232bc2f0465dc Apalache SeqTail Def0 False Passed
  • Model Under Test
  • Equivalent Model
416df4a48f7ffca450c137c62bccbfffea40c9a1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
7831ff9c37b93cdec6517f8ebd3f6ba69d17300e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
ca6b4816528c57a161fe37bb892e62ec37203ca3 Apalache SeqTail Def1 True Passed
  • Model Under Test
  • Equivalent Model
d09ba199431597a36f2620d91d219d1a652fd882 Apalache SeqTail Def1 False Passed
  • Model Under Test
  • Equivalent Model
6b1870401c7cd0e9d9995211e478661f37f1adea TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
6be3dbdcc8d03a35ae07496eb96bb6efac15f221 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
617589e423d3766568aac482534a172146bc6810 Apalache SeqTail Def2 True Passed
  • Model Under Test
  • Equivalent Model
b20f244d07b99324e28da88368479902e6b99147 Apalache SeqTail Def2 False Passed
  • Model Under Test
  • Equivalent Model
4f09f31500ce5b9c7b6e6180b235638c8d3079cb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
d5692f28b7ecc2bc290e7c0dcbd192d01362d396 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
44aa79698dd07d49139b4636b0f7c39875887ff3 Apalache SeqTail Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
35b91ea61e90d23359c5a865de1fc4224fbe6355 Apalache SeqTail Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
6fd63733b9187fbfb7afa85372918ee1e1f82063 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
98ed5606ad44620d96b8424ff86ce3407ce49938 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqTail LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
a355a1c9608e8301f8e8872d508ebdf822c053c8 Apalache SeqTail Extends True Passed
  • Model Under Test
  • Equivalent Model
5a178e8825307b268484a32f18dbe285502b2abf Apalache SeqTail Extends False Passed
  • Model Under Test
  • Equivalent Model
1e9448cb14e0f3b3470840d4bbff45bd7642a65d Apalache SeqTail ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a89e7e9bacb6cb05eaec674bef17d45c0f3f55c1 Apalache SeqTail ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
aea3b4372891795ec2cc3c4c5431f6d3d6d3d2ba Apalache SeqTail Variable True Passed
  • Model Under Test
  • Equivalent Model
10b8b38d68263a9dc7e26497545738a49d73d063 Apalache SeqTail Variable False Passed
  • Model Under Test
  • Equivalent Model
fc06736535bbbf861f78a1d78ae4a5a5c53155e0 Apalache SeqTail Constant True Passed
  • Model Under Test
  • Equivalent Model
079a5ad267659b13b41561b4c67391530fd594d5 Apalache SeqTail Constant False Passed
  • Model Under Test
  • Equivalent Model
cb9823860af88cd0027548e51f951bb902adee0a Apalache SeqTail ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
7fc6e199618306db5ff47a17f833e27cec5c11b8 Apalache SeqTail ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
4c6b9059ffa94ded3c40f1fcbef6359ca1de214a Apalache SeqTail Instance True Passed
  • Model Under Test
  • Equivalent Model
d64718ece31acac88b00e4f5820f2a4edff2235b Apalache SeqTail Instance False Passed
  • Model Under Test
  • Equivalent Model
e67cb92b8e0f032a8b791a543e480c8ab38e15fe Apalache SeqTail InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
f778b48a0824e06eaabfded05f911d6c984ab624 Apalache SeqTail InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
a81d7abff3cc9e02174e949efc33710c7261953c Apalache SeqTail InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
fcfb3e74a30ab8f31cfeb0c0dd893b820ca4ddc6 Apalache SeqTail InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
48f38e3084d918e172a6a2186bf04b7e173414b7 Apalache SeqTail InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
736d0e6f79b2352121c1cb0021556e2932c13fce Apalache SeqTail InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
be784eed210f3534bc51c015ca71474c1a9d8609 Apalache SeqTail InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
a0688bb595b5ce8b7d6539f060c9f9a1bcfee79f Apalache SeqTail InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
39177e1f1084afcbf1e1051cae7e45e4fc9233fe Apalache SeqTail InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
57c735d367a6973d9de267c6693d179dc4df4e58 Apalache SeqTail InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
a97abab267bfbca4fb60097e0a979265b752d083 Apalache SeqTail InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
60e3819a5055596c9822cc6379924d9bf5df62d1 Apalache SeqTail InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
c9bfd2d32e3f424ee9d7176b48e0c7344992cc66 Apalache SeqTail InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
d6149cadcbf94c90f8a9fd8823332eb54c94f0fb Apalache SeqTail InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
5186219e588a9a8c9d0deedf7c6c398f340c7bdd Apalache SeqTail IfCond True Passed
  • Model Under Test
  • Equivalent Model
2dc041c9bb2fac4f182182e7b3fedecf060108b2 Apalache SeqTail IfCond False Passed
  • Model Under Test
  • Equivalent Model
6ba066cbf06f8135eca3592485b9a9813932b796 Apalache SeqTail IfThen True Passed
  • Model Under Test
  • Equivalent Model
ed4371afc118d57db855bb7052a2ef11b177420f Apalache SeqTail IfThen False Passed
  • Model Under Test
  • Equivalent Model
ad67ba558b6741b391b8a93f41ec9325d2437b01 Apalache SeqTail IfElse True Passed
  • Model Under Test
  • Equivalent Model
bd6834e9c819edc78ceb1a98521966c9d271f207 Apalache SeqTail IfElse 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
395d1c9ecfe3d128db6494c255600a72be21546d Apalache SeqTail SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
37c072d0ed2772e18571bb9ea87f0ba943c6acb9 Apalache SeqTail SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
436c906bb8929a33a1cb833999bac6c941cbc123 Apalache SeqTail SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
f25716c67c0a6e342b7b7b7aa79de633830cc2f9 Apalache SeqTail SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
f31c06fc5cf7ec97754ea5e704174ac6aaed4fac TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqTail TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
6dfb02366e9a4f5886365229bb3d2d64e285c5b8 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqTail TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
b26e9858028a62c87835e03ecdcf8e6c4ad74d6d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqTail TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f34df48ea918a9faaefae42307802abbf7065d26 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqTail TlcEval False Passed
  • Model Under Test
  • Equivalent Model
d0ad9f56ab4969f82cc33bec4cc4d756c3814ffc Apalache SeqTail SeqHead True Passed
  • Model Under Test
  • Equivalent Model
96fe0c106ec086809aa69305152c64469b51bbe0 Apalache SeqTail SeqHead False Passed
  • 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
6f845a544faca4bede9ccbca51640c667f0f6fcd Apalache SeqTail SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
d4f39ca71d422cb072688d4a4c40999406d7c79e Apalache SeqTail SeqAppend False Passed
  • Model Under Test
  • Equivalent Model