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 SeqLen; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
1af1afe1855356e42bda1c8563dd09295d8a7c31 Apalache SeqLen Let True Passed
  • Model Under Test
  • Equivalent Model
473547cb759a719860d5b458441169c51969b48d Apalache SeqLen Let False Passed
  • Model Under Test
  • Equivalent Model
2d4de8e1ba0936ee5cb0ffdc17253a0254c5ba17 Apalache SeqLen Choose True Passed
  • Model Under Test
  • Equivalent Model
4c09309cc84934abdcf96a6c79c0591a35b5baf9 Apalache SeqLen Choose False Passed
  • Model Under Test
  • Equivalent Model
6f5ae1a62d6274b31aa2222cafb4910917ff910f Apalache SeqLen Tuple True Passed
  • Model Under Test
  • Equivalent Model
2e5b1f08edac9564f8048a780b20f744ba93b15a Apalache SeqLen Tuple False Passed
  • Model Under Test
  • Equivalent Model
fb172ada74afa0f04cc114ea6b7b1e937b9dbfd7 Apalache SeqLen TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
c2c4e8ad95f86d3553bf58b73ec3cf24f6b77e3b Apalache SeqLen TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
0121151b97e7d8fdbad378e76411ea05af876205 Apalache SeqLen FunApp True Passed
  • Model Under Test
  • Equivalent Model
b45fabb14491b1ce522272dab28b8b16078a2eab Apalache SeqLen FunApp False Passed
  • Model Under Test
  • Equivalent Model
23593e7e01ca9c3386888aae17c904fe7a16eceb Apalache SeqLen Prime True Passed
  • Model Under Test
  • Equivalent Model
3e0cf30db1e2daa2517db5949d73264f394da5c1 Apalache SeqLen Prime False Passed
  • Model Under Test
  • Equivalent Model
e887d1609923d169f0c9ea9c9eee5eddb6e9c0c6 Apalache SeqLen Def0 True Passed
  • Model Under Test
  • Equivalent Model
5bea690250775df2093c07d8a76453de77b17364 Apalache SeqLen Def0 False Passed
  • Model Under Test
  • Equivalent Model
183c4f8d8ea4e771b454fee0bdd6107e4c6beee0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
23e0b63acd2c920e6552dc427ff7441ad98d9071 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
bd52b4cd6653d64f8e12ffb7b0ad0a547ffe6bf3 Apalache SeqLen Def1 True Passed
  • Model Under Test
  • Equivalent Model
b66563678e4a65eb1778e3d9a85621d8c96594d1 Apalache SeqLen Def1 False Passed
  • Model Under Test
  • Equivalent Model
7a69be9a14d8c5495a3affac6319a5364d429136 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
0cecefb77189b59c5fb1f74b95e5e725e8b2fd54 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
b3ed065c786cb83a62f8a2bd5d4d82d04c781467 Apalache SeqLen Def2 True Passed
  • Model Under Test
  • Equivalent Model
b1b996b0c2162ff4413f1ab403c739f13581bcda Apalache SeqLen Def2 False Passed
  • Model Under Test
  • Equivalent Model
0b585364ea756851d07fd5477bc754515e7eaefb TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
e63e682a81d492f22a4dff0ccbe355b90e6da4f1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
13d35000ac38ea7228777ea600a64641dbdb1789 Apalache SeqLen Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6c4cfb79a866f1b86c8b347cf4859e48b446d1e4 Apalache SeqLen Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
4d165d942c96f52c17002f0aa671d09fef045598 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
dbbea8ad6f7862ec63357d153854d9cbbd5c45c0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SeqLen LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
928d965ea2821b84db04353eac82d668534954d3 Apalache SeqLen Extends True Passed
  • Model Under Test
  • Equivalent Model
696c7f76457f4188aeeb64be638e8ce90005bc07 Apalache SeqLen Extends False Passed
  • Model Under Test
  • Equivalent Model
11ad7ac5bb32c561393f99cecc70f21390bbd3d9 Apalache SeqLen ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
09f09fda467ab498012935b514c9c6ab7c4147b4 Apalache SeqLen ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
fa7d1fcb75213cb7eff4e2c9686c2dae21bd3998 Apalache SeqLen Variable True Passed
  • Model Under Test
  • Equivalent Model
a6c31e1d3636823077658abdbf2075cc77a4e5aa Apalache SeqLen Variable False Passed
  • Model Under Test
  • Equivalent Model
236f807959fdb3628a6b81f87552ec64d6740550 Apalache SeqLen Constant True Passed
  • Model Under Test
  • Equivalent Model
816981eeabbbe6c0b67568a700d76bcce0ac5bc8 Apalache SeqLen Constant False Passed
  • Model Under Test
  • Equivalent Model
522df6a97af2e892480810e536fda5fc39bc614b Apalache SeqLen ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
064f5e85116b7c8588fbd68791e1a8ec6af79c73 Apalache SeqLen ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e688083bdca55ee16c92d1ca47078f984e50b104 Apalache SeqLen Instance True Passed
  • Model Under Test
  • Equivalent Model
882eaa083a1042ce13cd72084b752f028a135c7c Apalache SeqLen Instance False Passed
  • Model Under Test
  • Equivalent Model
30557f8b764d055c109f3c58828684ee2d08edd9 Apalache SeqLen InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
023e69a29cd81f9cf42683c4c065945b6b667908 Apalache SeqLen InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
942476e525a72b29cb3945e1bb7ed7b77c89289b Apalache SeqLen InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
bf8825cddac27ab7f59a93c17b1cf8d3faea0f4d Apalache SeqLen InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
162567b7045e637eac0be80b9e47f51de013b01c Apalache SeqLen InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
612cd371054bb5ac0ab6c89b2728b225c03c20cf Apalache SeqLen InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
be183d74d4983514a334d2e43080f439f9da151f Apalache SeqLen InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
97389f8b0016d1c0d8dd9794910c2cf77119b631 Apalache SeqLen InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
094c3542a66826c1fd7562156d94267e7521f87d Apalache SeqLen InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
6131115e7eee92fd7ebd82339372d0ba2a1d4fc3 Apalache SeqLen InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
388c6d5e4c01d51b0d654b91227a1b29e87a1e75 Apalache SeqLen InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
7debfba02aa477d227ccea4fadb018272cb131a3 Apalache SeqLen InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
2e01cc0793da1fb560440470ddf9b012f62e2e78 Apalache SeqLen InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
a6c4cdadfc5569c6ef0826eb68fde12df6f30f5d Apalache SeqLen InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
d62d3b7550baa32831087a8f0dd5b34b8cbb3d58 Apalache SeqLen IfCond True Passed
  • Model Under Test
  • Equivalent Model
1b748d25ac9057236f537f20295ada9b449df0bd Apalache SeqLen IfCond False Passed
  • Model Under Test
  • Equivalent Model
aafce8f75272524f6d1cde21a4b34ee711382b3f Apalache SeqLen IfThen True Passed
  • Model Under Test
  • Equivalent Model
2d8426e5a230ecb029231b560e5e7ee820b4560d Apalache SeqLen IfThen False Passed
  • Model Under Test
  • Equivalent Model
e393674dd64ade67eb55e852ab1d2bb5c4ac4785 Apalache SeqLen IfElse True Passed
  • Model Under Test
  • Equivalent Model
2cc06c7c60c375f4c00e348a8e9c62a8cda32171 Apalache SeqLen IfElse False Passed
  • Model Under Test
  • Equivalent Model
c9f71e36fae7bdf832e1de9616adf3bb8d99938b Apalache SeqLen StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
ab0a944f76a0fcee3c7f1347f051ec859ed0a7e4 Apalache SeqLen StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
b589fde34c9f085b6707da13986d265c34125678 Apalache SeqLen String True Passed
  • Model Under Test
  • Equivalent Model
dd41abb7113b86a4b5ca4e5bf6e6294455b44f03 Apalache SeqLen String 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
a44d9c1c62bc2b30dd71572730e32891c5517769 Apalache SeqLen SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
fe6960ac5a5d9e752defd281c54f66a235606f39 Apalache SeqLen SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
98af65116937abffd370b1e4b8820c32f4a5dc49 Apalache SeqLen SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
f6b07dba1a9f9960b2fcd162f4d73109b2b72d21 Apalache SeqLen SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
db4ed971215b735beb08c740728dd1f76947cb6c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqLen TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
e7d00e5d5e7a7e0a28b620e88d386b72c0c9a312 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqLen TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
a4d6b9bca1609113226737f0213b5016cc60e31a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqLen TlcEval True Passed
  • Model Under Test
  • Equivalent Model
74eeb5eff07603d6bc8413681633a4f7c5f645b6 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SeqLen TlcEval False Passed
  • Model Under Test
  • Equivalent Model
6aa577f812a2690fd0e2701fd2b5190600f79360 Apalache SeqLen SeqHead True Passed
  • Model Under Test
  • Equivalent Model
fc55b06a88301bcde2dc4e49c4b64e765a754b3b Apalache SeqLen SeqHead 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
2ba366bdcc1947b9aa2ffb963e69155b102b0646 Apalache SeqLen SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
8cc3bfc3a99ac8916992498386c1b3b63226448a Apalache SeqLen SeqAppend False Passed
  • Model Under Test
  • Equivalent Model