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 plug feature ConstantModelValue; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
26db2b4023bbf3ccf69b2db3b2f5ab9dc2b5114a Apalache Eq ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
534257e3fbe90320aa0e8092e98adfa4158eb81b Apalache Eq ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
4d076d88a5568aef6ca438066528223143e9e095 Apalache Ne ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
f4afe220544b0798990491de87a3564424b38775 Apalache Ne ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
45911ff45fdb44587ad3268228e37be1fc8760a7 Apalache Let ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
cf587dc75800a7de0fa6e0594898732df9a9af32 Apalache Let ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
f23a080b0ee169f7b905ea5b0dd4475fed479d95 Apalache Set0 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
d9846276c6586430edbeba1d5f706cda046c07b2 Apalache Set0 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
bc8b80cf97ec4ddf4e32bd47bfb71125c9f9fb6a Apalache Set1 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
755aa84321536cc971a5ca1b0a1f64df7e481b0f Apalache Set1 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
a8337ea5bbbc303f88a9b13a4a9250ba61b07f42 Apalache Set2 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
230de7a47aacd7f995662a2341dac17d69f31825 Apalache Set2 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
0a075ea8b400c86f9cff2e178a7fd3e57c6b87ec Apalache Fun ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
14b7d82ce99b39d6ec5fc3e840639a85a410b86c Apalache Fun ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
056e5518d99b58c23a6a2f0fe8658d83e82b1735 Apalache In ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
71d3cb0bd6f17ca0c87469338d06d6d932059fcf Apalache In ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
d17c77111e411176c75e591992dba47b47552170 Apalache NotIn ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
60b53341cfe931d6d0b5eb1e0968baff07bb409b Apalache NotIn ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
aa0a7f104ab6e61ca52480ff769a41c8591b714c Apalache Record ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
a5cf0fdf9650f0c0b2cc78956e25658431bfe8eb Apalache Record ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
d7003b02508198f5e58991c2479b40d473ab2970 Apalache Tuple ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
caefe49b56158967039add377b56e4fa4f8230cd Apalache Tuple ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
44c41f34535d83f86a0b2279ca4defbdf3adbfc2 Apalache FunApp ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
09012b36c8dcc22a842ea5ea5b70f76b8fc88261 Apalache FunApp ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
44b68a33c8efe4dd44e72eaa8597f75aef6bc61a Apalache Prime ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
a1ee2055ae77c21e0a34246173a9f1ff040de41c Apalache Prime ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
848000cd7a918814ea503ebd539736ad8e69d174 Apalache DefFun ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
5a25b2712dd41040644450c83c3f974cc2615c78 Apalache DefFun ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
959719f2e9fa022659067892c4c647e1822177e6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
4cacbac8facdb5951de08d56a9c3b0f199624bf9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
86ed9552ae6a26b1bbe7ec6d6b9d8e828fda4b06 Apalache DefFunRecursive ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
6e03b7a57fd0eee774b3e36739d591ffeb599143 Apalache DefFunRecursive ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
be74da9984dae1663adeaa7be7bdce8040f4707d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
17a63fd6e6ff5ed8507d45c6a723855c6427b74f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
b1022a0568314cfaaff1f4e159c5f466b8d1b420 Apalache Def0 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
9fb56a78b153ef43ee4838dbbad92a821b709909 Apalache Def0 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
a850ebb25ddb878e194ae0230ef484b02459ade5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
ce65a90dfc860f2576e4e1263b8bac119fbd581b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
ab4653feb8e086e869ca4fa3d879a1f7536b37c0 Apalache Def1 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
9e0451f6c522ca7068c2ec9494d34110a03ddabb Apalache Def1 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
9ac14504e2ec9430d9b649a392e045dd970a8c26 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
c96994c68b952c43ff61673e3596c59805e07734 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
9abe9da6d0107f2b7836fba04629ca560074008c Apalache Def2 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
e4a3ea94f0d9a014448565b7a5b46f334bd1dca2 Apalache Def2 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
4918f157c50f3b7e10a6891c18801235fe04a214 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
64669e6cc4452e42d90921e2636b2c1613bfa852 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
9ce8966b7bc8d72d8033698ab4d3827d448508a2 Apalache Def1Recursive ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
c8e21d1a308c29d09334d472cbc581d6a1dc835f Apalache Def1Recursive ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
3f69a4187db2bd8c662cc23297d1ba723f33b48f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
824f0196de385fe651e42d54087d49f574c0eea9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
99b29fb34566965e20fc2501b0c8eb1735f3bc92 Apalache Extends ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
e010d841b4c42de25e834080c6eaf8c9b85a40ed Apalache Extends ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
409bac117052339daa984fc39bb93cf829d3e407 Apalache ExtendsInDifferentFolder ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
a8ea86833bd2366fd1acff736d1baa97e2425724 Apalache ExtendsInDifferentFolder ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
4c3a5a66fdf4956b1a64c2cd7107f19d5b513748 Apalache Constant ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
33e7d75749a54e458135bf359b115fdda6eb9574 Apalache Constant ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
60033f061357b206874f647b7bfdfe77b7ed32f4 Apalache ConstantRank1 ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
c3fcbbb9c63a3178297ee28abb4cba8bb7f3138f Apalache ConstantRank1 ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
50d7578199c28ac4b62993935d5525e47f094c15 Apalache Instance ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
b9cb7fe65f5b96a1c781c71bbd57aca6004b3dda Apalache Instance ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
03914d4f371f10c6a95d4f41db81f38cc6f442fa Apalache InstanceWith ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
ec98765cbb44394f469b022e480064f5dbd2241f Apalache InstanceWith ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
29a94a78e931027e8b01c2ea141bbc6268ffda08 Apalache InstanceNamed ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
eadb83e83d07ae2a36571403531ecee133788ef0 Apalache InstanceNamed ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
5939873c1f112b267150485f3ced324f61575cb2 Apalache InstanceNamedWith ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
db01ca10a8c087c6fcbf0506f4054972b7491109 Apalache InstanceNamedWith ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
387966100fefdb5bf4006d867c622e03f383bf88 Apalache InstanceInFolder ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
5c1835f028b9fa941e33feacdeef49dc53455c98 Apalache InstanceInFolder ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
8f352165da7d44c346f893aeaa8985398aca8848 Apalache InstanceWithInFolder ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
69b1f60dcf3d4842820e6343a36cd170e60dcb66 Apalache InstanceWithInFolder ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
15e63e87f5acaaf685977f80baaf56cef449a49d Apalache InstanceNamedInFolder ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
fb9a27951f4aa46c854fc2b7ffc1f7353f88c0d6 Apalache InstanceNamedInFolder ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
c6ab66d82c4e1008698f261b982db659a5ef89c9 Apalache InstanceNamedWithInFolder ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
3d1b81bb73c6414605cc86fe812091ba9aa9066a Apalache InstanceNamedWithInFolder ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
3b5001dde714b93021887b1d766d2ffec63ee68b Apalache Lambda ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
da709d3f87e246d84fd2f1771a8076f518f7d9de Apalache Lambda ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model