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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c9159678594ed939c68d2e8d3dc5e6d674b1baf9 Apalache And Unchanged True Passed
  • Model Under Test
  • Equivalent Model
240e80dc15efabaafc82045ef1b9bfb40c66944f Apalache And Unchanged False Passed
  • Model Under Test
  • Equivalent Model
56e9bb0e5da832b2707fc98d20352a31b3fe686b TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Unchanged True Passed
  • Model Under Test
  • Equivalent Model
e380fbe9c82c8530d911c34a5a81ca4b2ddfaa10 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Unchanged False Passed
  • Model Under Test
  • Equivalent Model
8574810f0a422761d80b440ea7b20225272beea6 Apalache Imply Unchanged True Passed
  • Model Under Test
  • Equivalent Model
8a3e899f52f0b438fc791e21f1618ef15d51c232 Apalache Imply Unchanged False Passed
  • Model Under Test
  • Equivalent Model
ef70d74dc75afc5faae440cee6de2905a8f3e618 Apalache Not Unchanged True Passed
  • Model Under Test
  • Equivalent Model
74d3c9dee5c8b22faca222f343cec46ab4d1b30a Apalache Not Unchanged False Passed
  • Model Under Test
  • Equivalent Model
5c8f9dc579c9a95a263ab2bd15c5b4e6ce0f6555 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Unchanged True Passed
  • Model Under Test
  • Equivalent Model
648a27e63ec57c8aeb8b7eb07358fd0f6efd7f47 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Unchanged False Passed
  • Model Under Test
  • Equivalent Model
3fa8f956012887cdbccd05489f954fbb675b2560 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Unchanged True Passed
  • Model Under Test
  • Equivalent Model
9608f9399099770659f3424e3469a9aa22eefbe7 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Unchanged False Passed
  • Model Under Test
  • Equivalent Model
7c2ed4461da22534f7594451f65f5c682484d3dd Apalache Boxed Unchanged True Passed
  • Model Under Test
  • Equivalent Model
615a11ccec6fd5633d9f5c6d512e31c7d10284ee Apalache Boxed Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d7299d457d2fe786d4d11083f22ee50a107243af Apalache Eq Unchanged True Passed
  • Model Under Test
  • Equivalent Model
9f4b4cdfd50b572803f52300f1af2e4bf46170d2 Apalache Eq Unchanged False Passed
  • Model Under Test
  • Equivalent Model
7a64b03db95c0d311fed1c46fead9166f6f83c68 Apalache Ne Unchanged True Passed
  • Model Under Test
  • Equivalent Model
ac3890d72c2fd1f02ffddff581e70028e32be358 Apalache Ne Unchanged False Passed
  • Model Under Test
  • Equivalent Model
72135ef59caf0753d8a44eb3b307b58980b6f1db Apalache Let Unchanged True Passed
  • Model Under Test
  • Equivalent Model
47ac9f66298cfd3924b7044b4abbc882c5a69036 Apalache Let Unchanged False Passed
  • Model Under Test
  • Equivalent Model
cea96c30d6a302ebea4a12be0d4181ced7573a05 Apalache Set0 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
84d08675b51acfedc14f5916dbaf8e9ab7b6ca2f Apalache Set0 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
853a49eaeb80074c81b20d922b56a059c2b987e1 Apalache Set1 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
3c26770d8e2008eb0d1fb71c20f370a35b4ded2c Apalache Set1 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
9a1798308a46d09409656d3afe65eeaf45759638 Apalache Set2 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
2636bdc05f744665738366b4d01061b3a5f3c56c Apalache Set2 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
c0f27558a5fa6df89f1f1a46e1395db179b40547 Apalache Fun Unchanged True Passed
  • Model Under Test
  • Equivalent Model
666c5fb4e4f12a5a923489f2cfdca80a3bdd1de0 Apalache Fun Unchanged False Passed
  • Model Under Test
  • Equivalent Model
9143c191a43897a0d9e5d30770d615371b0e5e4c Apalache In Unchanged True Passed
  • Model Under Test
  • Equivalent Model
5f54a581d4ab64f833520d949e63afd950167504 Apalache In Unchanged False Passed
  • Model Under Test
  • Equivalent Model
f3ab4d8b603af03c143f19fb13eef97f4c094632 Apalache NotIn Unchanged True Passed
  • Model Under Test
  • Equivalent Model
2d6815be13cc1b368b6653c88e5978b1ee30b7b0 Apalache NotIn Unchanged False Passed
  • Model Under Test
  • Equivalent Model
0659312890300a44ca36e4835956884bf7ca77c1 Apalache Exists Unchanged True Passed
  • Model Under Test
  • Equivalent Model
5221ac322273caea196c8760d043c0e48f7d5497 Apalache Exists Unchanged False Passed
  • Model Under Test
  • Equivalent Model
e6faaaf83d1ef06bef1cf62d355d597bf98d86df Apalache Forall Unchanged True Passed
  • Model Under Test
  • Equivalent Model
0d62bdfea0fc3a0e7c5a14b82ab6d4808a0f420a Apalache Forall Unchanged False Passed
  • Model Under Test
  • Equivalent Model
454ef4523aa109624a7a3e01692258e2ffa446fd Apalache Choose Unchanged True Passed
  • Model Under Test
  • Equivalent Model
c091458edcc28b4add51b953b27332daf365eed3 Apalache Choose Unchanged False Passed
  • Model Under Test
  • Equivalent Model
55cbd84b509d87ee037b90058bf907f7b2102cc8 Apalache Record Unchanged True Passed
  • Model Under Test
  • Equivalent Model
3a5489ae8db0b34caeebad5f05780059bd3b1b50 Apalache Record Unchanged False Passed
  • Model Under Test
  • Equivalent Model
ae5b375526ef1492f56fa635a1e1a7a394ff60f5 Apalache Tuple Unchanged True Passed
  • Model Under Test
  • Equivalent Model
62d706aa5812961532957cbe4352568b2cd5d1dd Apalache Tuple Unchanged False Passed
  • Model Under Test
  • Equivalent Model
88f60a3488ea87e4cf6969cc2dc5cc23aba981ef Apalache FunApp Unchanged True Passed
  • Model Under Test
  • Equivalent Model
1f5386e57cdc8528b1197b878dc8316f50d472f9 Apalache FunApp Unchanged False Passed
  • Model Under Test
  • Equivalent Model
2b2e80104ea3d0bdde0a8fdc512e0ca3afff8f21 Apalache Except1Fun Unchanged True Passed
  • Model Under Test
  • Equivalent Model
914c76c287b410aaeccc9f044ef4dab3c15da7cd Apalache Except1Fun Unchanged False Passed
  • Model Under Test
  • Equivalent Model
73bb9c458f2ffbb69da3790a1824fdd41947612b TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Unchanged True Passed
  • Model Under Test
  • Equivalent Model
40d0ccc3f7eefd950d189fbaa76e7be2a3fc2d9e TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Unchanged False Passed
  • Model Under Test
  • Equivalent Model
4fd81201b48fb61c800f3720b08dd761e08f0a32 Apalache Except1Rec Unchanged True Passed
  • Model Under Test
  • Equivalent Model
c67a7760db8a5c2dc2d51e43b57b95d323d9f3fa Apalache Except1Rec Unchanged False Passed
  • Model Under Test
  • Equivalent Model
395669ebcb92fef4a08c5e6a1a50424b30281218 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Unchanged True Passed
  • Model Under Test
  • Equivalent Model
392eec0e47be6727b4b24630a8ac6f410033204e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Unchanged False Passed
  • Model Under Test
  • Equivalent Model
b8c2153b1266a635b7d4eb2c35f04cc66f5cae67 Apalache Except2Fun Unchanged True Passed
  • Model Under Test
  • Equivalent Model
2d9398f9ddc8c0dd2053c41ee41ae9d6bd708933 Apalache Except2Fun Unchanged False Passed
  • Model Under Test
  • Equivalent Model
8138183f4bfb47c916156333fe82d496dc0e6a12 Apalache DefFun Unchanged True Passed
  • Model Under Test
  • Equivalent Model
ae53f137c6fc6fb892a7261d9ce0ea53f7d317d5 Apalache DefFun Unchanged False Passed
  • Model Under Test
  • Equivalent Model
9440b5dd8149f894adaba563cd16b05703c7f5de TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Unchanged True Passed
  • Model Under Test
  • Equivalent Model
aeceed33926cab4ec9b8ff07e55800001f31bb80 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Unchanged False Passed
  • Model Under Test
  • Equivalent Model
39e5e7b25dd37f4e16b31df488ba55b42bfb796e Apalache DefFunRecursive Unchanged True Passed
  • Model Under Test
  • Equivalent Model
3916461d707e0a0ccbe80c9abe96e0f84d7c40d9 Apalache DefFunRecursive Unchanged False Passed
  • Model Under Test
  • Equivalent Model
f387690ca3f73ef2bb6d6f211b5c1228d7c06004 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Unchanged True Passed
  • Model Under Test
  • Equivalent Model
5e9c10fd09d4bffad98cff453d0c48f0b12dda34 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d4d54e27fc470a6ff4f2066709931a1acb9349e0 Apalache Def0 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
4cf248d03915eb16b3c7c429ccad6939e8683460 Apalache Def0 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
ee19198331c030d2531dfac52ae97108783b52b3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
5d80b29fe0b90e964c62436f3970fbca78d5a3f9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
ab17cf2f98df7844660d8706512f020a5c41e1b5 Apalache Def1 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
95b6677e6499d7ef1a6651ed177c3b32a01231a3 Apalache Def1 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
4a77b0cc736fc70bbbbbb18fe8df86c9318c033b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
9c85931c6d618633e6e8619e1e0d6c2b2d15533c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
92246f4f5486d446b81e91b2b598c1749986a715 Apalache Def2 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
35b2d2907c19ed4f70d69ab800469bbe9ba57bcd Apalache Def2 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
67a1ad6d0c7d483d1019a16abf21ce8682c4551a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Unchanged True Passed
  • Model Under Test
  • Equivalent Model
3b0f1e57213db9b76eec1639b4601eccca753e48 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Unchanged False Passed
  • Model Under Test
  • Equivalent Model
6902edbd8b2fe372ca580316541ec47dce199fe7 Apalache Def1Recursive Unchanged True Passed
  • Model Under Test
  • Equivalent Model
22293de36917c31c810aa5422c57c8d9e051915d Apalache Def1Recursive Unchanged False Passed
  • Model Under Test
  • Equivalent Model
04f4c9102c930ba6d65c3043e3af24eed88e1f92 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Unchanged True Passed
  • Model Under Test
  • Equivalent Model
058225963d808c1bd7e6b29571f36560740bd042 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Unchanged False Passed
  • Model Under Test
  • Equivalent Model
015fdf54556b508beb16eb4d526e2924ea072539 Apalache Extends Unchanged True Passed
  • Model Under Test
  • Equivalent Model
439c7efde190d6c04c11f4d3217f68cfa0e59322 Apalache Extends Unchanged False Passed
  • Model Under Test
  • Equivalent Model
f6cee01f84d06193eac9d993c97d663c5b8ff0ab Apalache ExtendsInDifferentFolder Unchanged True Passed
  • Model Under Test
  • Equivalent Model
bb96f492348ec0b11863ce8b62d8821c33d49902 Apalache ExtendsInDifferentFolder Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d7e47a9a65da7582e4474b6ab50953987c4bbf24 Apalache Variable Unchanged True Passed
  • Model Under Test
  • Equivalent Model
0a778f723b0aab9bb385d07c223a5f56e6a90c41 Apalache Variable Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d7e6ec37847c14a3596ec15b3f292ef281afec13 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Unchanged True Passed
  • Model Under Test
  • Equivalent Model
ccb7d11af4ed4c467e8f66f78f5e331477ac162d TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Unchanged False Passed
  • Model Under Test
  • Equivalent Model
6c1fd42952e9f68abc14a3ee1088f0f91e65262c Apalache Instance Unchanged True Passed
  • Model Under Test
  • Equivalent Model
a8ae9fad19aac24b46665ee8870136c5542c20f6 Apalache Instance Unchanged False Passed
  • Model Under Test
  • Equivalent Model
3874b65d9457907fab7dd3351d96a38f773bf22b Apalache InstanceWith Unchanged True Passed
  • Model Under Test
  • Equivalent Model
dff0640cbc54651efc1ad6863d4c4d21ecda9310 Apalache InstanceWith Unchanged False Passed
  • Model Under Test
  • Equivalent Model
c3eed7fc4f088807147d4ea1e1afc2f5a382910f Apalache InstanceNamed Unchanged True Passed
  • Model Under Test
  • Equivalent Model
64caafc8bb0af9c268b326cdf42d68bce670ad4e Apalache InstanceNamed Unchanged False Passed
  • Model Under Test
  • Equivalent Model
c6c9abd6c8db709fcf6041c99139f42c03648066 Apalache InstanceNamedWith Unchanged True Passed
  • Model Under Test
  • Equivalent Model
dd8caee81b8ae98040c7f3e3bfd7d742379b83d6 Apalache InstanceNamedWith Unchanged False Passed
  • Model Under Test
  • Equivalent Model
f62f8417f3767375779066958a716e90cc1d0faa Apalache InstanceInFolder Unchanged True Passed
  • Model Under Test
  • Equivalent Model
3cb2d14e4bae1f656ac55eea22a28bbca45a477d Apalache InstanceInFolder Unchanged False Passed
  • Model Under Test
  • Equivalent Model
42b946785b50672d4a345e47d5c25421b3282a16 Apalache InstanceWithInFolder Unchanged True Passed
  • Model Under Test
  • Equivalent Model
ca81bc09593e4f505a0102309191b948437ae9c4 Apalache InstanceWithInFolder Unchanged False Passed
  • Model Under Test
  • Equivalent Model
c1c487b137f83368e35ebf4fb6c25ed4245a9695 Apalache InstanceNamedInFolder Unchanged True Passed
  • Model Under Test
  • Equivalent Model
5a9de09d1749492e067fbe9653cc18de470a74ca Apalache InstanceNamedInFolder Unchanged False Passed
  • Model Under Test
  • Equivalent Model
6325a9b5321e70aafa984fbae08282e20358ce10 Apalache InstanceNamedWithInFolder Unchanged True Passed
  • Model Under Test
  • Equivalent Model
84cd102d013e2f72acc0de416ce15af5b811c29a Apalache InstanceNamedWithInFolder Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d856805729fc05540be362eff9a4f8038326eea4 Apalache Enabled Unchanged True Passed
  • Model Under Test
  • Equivalent Model
de85c596c6cef02259946d412754818c3d692d65 Apalache Enabled Unchanged False Passed
  • Model Under Test
  • Equivalent Model
c71b3aad5adf026cc0a3cf684c3a5070f75034f7 Apalache Lambda Unchanged True Passed
  • Model Under Test
  • Equivalent Model
7d6727edfcb332796350e9c10d51c2aea06fac23 Apalache Lambda Unchanged False Passed
  • Model Under Test
  • Equivalent Model
4d68141e5a6286708280324f28db661109017583 Apalache IfCond Unchanged True Passed
  • Model Under Test
  • Equivalent Model
00ace853e47ecd5d3a4127554de916a1d0999a17 Apalache IfCond Unchanged False Passed
  • Model Under Test
  • Equivalent Model
0aa0cdca90ceb3d2123cb623856f938780ce0a5a Apalache IfThen Unchanged True Passed
  • Model Under Test
  • Equivalent Model
17aedf256a7e207c8a00b713180f0ac7c0a20025 Apalache IfThen Unchanged False Passed
  • Model Under Test
  • Equivalent Model
1154b08ebc885dbd827ffd265a402d48472f62c2 Apalache IfElse Unchanged True Passed
  • Model Under Test
  • Equivalent Model
27292d5de07b5e02158d328e02ab81e57754f02b Apalache IfElse Unchanged False Passed
  • Model Under Test
  • Equivalent Model
80f4236c53566e4a2e727ef73df3ddc1b0de765e Apalache Equivalence Unchanged True Passed
  • Model Under Test
  • Equivalent Model
65dbb870255a4baf3393d781ecc4f64e63760f1c Apalache Equivalence Unchanged False Passed
  • Model Under Test
  • Equivalent Model
e15099bdb69349c17bbe73098dfd646a91d831ba TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Unchanged True Passed
  • Model Under Test
  • Equivalent Model
ed5b36fd4be44d4d311aa22d5058f684111a3b07 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Unchanged False Passed
  • Model Under Test
  • Equivalent Model
3e3db6ba77940bfdaeb396423afd6957fc489d0d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Unchanged True Passed
  • Model Under Test
  • Equivalent Model
8883a35ffcc28e403405bd156f08af57ba6ce004 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Unchanged False Passed
  • Model Under Test
  • Equivalent Model
6cf7bf5d3d5e595ab3c27963de9ca8d39185bc34 Apalache BagBagIn Unchanged True Passed
  • Model Under Test
  • Equivalent Model
d39175f7310a774b6e14ab62bda6bd5f924c024e Apalache BagBagIn Unchanged False Passed
  • Model Under Test
  • Equivalent Model
6dd5f2e81d606fafb5c19547fe8835c2fc8857ed Apalache BagCopiesIn Unchanged True Passed
  • Model Under Test
  • Equivalent Model
aecf496aa551d07b8a1a4cfdb6ec839113362d9a Apalache BagCopiesIn Unchanged False Passed
  • Model Under Test
  • Equivalent Model
d8b684b84cdcdd2821c5050bd0c72264be841542 Apalache SeqAppend Unchanged True Passed
  • Model Under Test
  • Equivalent Model
107eada58d72f9d19dda5a11e0487809a18d3e6c Apalache SeqAppend Unchanged False Passed
  • Model Under Test
  • Equivalent Model