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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
7b558e8a455c5b2466d6f37afe61331dfc44701f Apalache And NumGe True Passed
  • Model Under Test
  • Equivalent Model
ecb6e78812175a081cef063ddd1a69e5e8c8f422 Apalache And NumGe False Passed
  • Model Under Test
  • Equivalent Model
1d75fc45be9c0965f11801be6f9d6904f5f8dde4 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGe True Passed
  • Model Under Test
  • Equivalent Model
19c7f0b79c44ae2deb959841ad429fdb551a00da TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine NumGe False Passed
  • Model Under Test
  • Equivalent Model
9c61ed96cb28d4c25732b32752517133b32c719a Apalache Imply NumGe True Passed
  • Model Under Test
  • Equivalent Model
a053d7f51756ec8805ecd252ccab31048ba756e1 Apalache Imply NumGe False Passed
  • Model Under Test
  • Equivalent Model
151c5578b1530c9a56c5f682cd8148797c24b36a Apalache Not NumGe True Passed
  • Model Under Test
  • Equivalent Model
06566d8abbb9b0237b0ce3dbf80cd431c6ccfa55 Apalache Not NumGe False Passed
  • Model Under Test
  • Equivalent Model
c29d18d6596d10cd3a5351b619f3adcfafd07e44 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or NumGe True Passed
  • Model Under Test
  • Equivalent Model
4506d05dbc8881127cf864fd4e491941f0fe098a TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or NumGe False Passed
  • Model Under Test
  • Equivalent Model
4baa5c992a74aaca5c0e08a446f3e83db5ff9c42 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine NumGe True Passed
  • Model Under Test
  • Equivalent Model
9170f699e677a5b6ed68d3f20e18f9018aac1fe7 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine NumGe False Passed
  • Model Under Test
  • Equivalent Model
6a48cd57005372eb9e30fc63ebe738fa7630ebb5 Apalache AndProp NumGe True Passed
  • Model Under Test
  • Equivalent Model
74957808889d63c06a8f86b937ff524d54662bab Apalache AndProp NumGe False Passed
  • Model Under Test
  • Equivalent Model
580cc5054162ac762ca187b6d2be7f71ade7dc46 Apalache Boxed NumGe True Passed
  • Model Under Test
  • Equivalent Model
9882f5be469bdce7a83b5c3c06d01d4efb115574 Apalache Boxed NumGe False Passed
  • Model Under Test
  • Equivalent Model
5db78246c3945d4e5fddacf0fef7e48bd181379c Apalache Eq NumGe True Passed
  • Model Under Test
  • Equivalent Model
5466518c8ca9787dd72dbeee9553e2de1833582a Apalache Eq NumGe False Passed
  • Model Under Test
  • Equivalent Model
07c085dec75e167d78318ddfe1b7bb285fd35c24 Apalache Ne NumGe True Passed
  • Model Under Test
  • Equivalent Model
904ae4355b6538d880d7ce75817b13036f2da01f Apalache Ne NumGe False Passed
  • Model Under Test
  • Equivalent Model
1bb34d51d0781a550d4edd33f2c9d2093f86a1b8 Apalache Let NumGe True Passed
  • Model Under Test
  • Equivalent Model
7c9b9ad7bd41500db7b5dde69ba0aab5fa90d9d4 Apalache Let NumGe False Passed
  • Model Under Test
  • Equivalent Model
3a31565e0cf1e27b566a8963995c86b97db8ee96 Apalache Set0 NumGe True Passed
  • Model Under Test
  • Equivalent Model
bf3ced58835a81cf2be84cf601c5e938db6c5a16 Apalache Set0 NumGe False Passed
  • Model Under Test
  • Equivalent Model
7cfb28b54773b963a85b3d01f7e221f986e18f15 Apalache Set1 NumGe True Passed
  • Model Under Test
  • Equivalent Model
daaa62fba356f5cd53d9601c0da185c751a0f530 Apalache Set1 NumGe False Passed
  • Model Under Test
  • Equivalent Model
cecccb33c07f680426f44fb93bcd8726a43a2c5d Apalache Set2 NumGe True Passed
  • Model Under Test
  • Equivalent Model
c2f411ddeb3b9e561a2a12c7d13842c37d761775 Apalache Set2 NumGe False Passed
  • Model Under Test
  • Equivalent Model
c1da7d046c2f9227b53961700cdcaf4e2610fd74 Apalache Fun NumGe True Passed
  • Model Under Test
  • Equivalent Model
128fb15e41c66e000b0d17a461b0746e1581a64f Apalache Fun NumGe False Passed
  • Model Under Test
  • Equivalent Model
59e8f6dbd139573b3b20cc8280757bcec0e5262d Apalache In NumGe True Passed
  • Model Under Test
  • Equivalent Model
f1be5415e67af99a9340457f8926071343aa873a Apalache In NumGe False Passed
  • Model Under Test
  • Equivalent Model
e98f501cd1850458407f01357d846f41014f817b Apalache NotIn NumGe True Passed
  • Model Under Test
  • Equivalent Model
6a3fc7a1b97025e87144e1ae34f33af62c566427 Apalache NotIn NumGe False Passed
  • Model Under Test
  • Equivalent Model
e35e6a60ea2e92e4d4bf3ed68816e773d37865c7 Apalache Exists NumGe True Passed
  • Model Under Test
  • Equivalent Model
159f0a3318be44990ba1c97da08984e95ee2f687 Apalache Exists NumGe False Passed
  • Model Under Test
  • Equivalent Model
16635fd5adf70953fc9bc753cbb7e6f29eb9d988 Apalache Forall NumGe True Passed
  • Model Under Test
  • Equivalent Model
025439bb6e6a4611861400c2b476da791e8b56d2 Apalache Forall NumGe False Passed
  • Model Under Test
  • Equivalent Model
89105e9f6e710afa6ced594c86c2a96e08d7ee7b Apalache Choose NumGe True Passed
  • Model Under Test
  • Equivalent Model
e944529958bee449b08e21dac93fb763d1b4ec9a Apalache Choose NumGe False Passed
  • Model Under Test
  • Equivalent Model
361b3f2e4c269fa5693f8debd27a5e9dd0637cb6 Apalache Record NumGe True Passed
  • Model Under Test
  • Equivalent Model
5668b23c522e3167ab5ef53f3bcf4d15ba3757e4 Apalache Record NumGe False Passed
  • Model Under Test
  • Equivalent Model
8475af864ef7a1f9e7d542d4014f431e294ba422 Apalache Tuple NumGe True Passed
  • Model Under Test
  • Equivalent Model
502b0b3e13b0487be24a3a69bb1c7ea1b2da32c4 Apalache Tuple NumGe False Passed
  • Model Under Test
  • Equivalent Model
4682732aeb12e51931ad6d2193caeb7595cfcc48 Apalache FunApp NumGe True Passed
  • Model Under Test
  • Equivalent Model
82af2d52ed8f6124e712c1094a134d3378cca368 Apalache FunApp NumGe False Passed
  • Model Under Test
  • Equivalent Model
41c03947041946a879391c28a845a391a67dfe22 Apalache Except1Fun NumGe True Passed
  • Model Under Test
  • Equivalent Model
c43bcaa0a98f41ede9aabb4636c9d99507412beb Apalache Except1Fun NumGe False Passed
  • Model Under Test
  • Equivalent Model
99fc6ca8bcd0d9311b607c85dccf2d735e396aab TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt NumGe True Passed
  • Model Under Test
  • Equivalent Model
d90bb4ed21b1ca42ed7bec9808a60e8052052580 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt NumGe False Passed
  • Model Under Test
  • Equivalent Model
f66138abac0ec73e13f75beb2c4d25e2e116c61d Apalache Except1Rec NumGe True Passed
  • Model Under Test
  • Equivalent Model
0ea9cf552df9dd87d6544028337bc24de8bc88cc Apalache Except1Rec NumGe False Passed
  • Model Under Test
  • Equivalent Model
7953e2cf24cf388a68232c9ca5e1495d28c9dda6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGe True Passed
  • Model Under Test
  • Equivalent Model
e9bee7413e846d421dd5ced419f9778f6d41cf3c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt NumGe False Passed
  • Model Under Test
  • Equivalent Model
7a1ed246b0cf10d041550a31791b9c24befeab39 Apalache Except2Fun NumGe True Passed
  • Model Under Test
  • Equivalent Model
7e62939b75a3b0e5ab6389d5691d9d3be97e8212 Apalache Except2Fun NumGe False Passed
  • Model Under Test
  • Equivalent Model
e3698e3a43aada7755a28cefda0c26eb4badbe03 Apalache Prime NumGe True Passed
  • Model Under Test
  • Equivalent Model
3235781fef640776cbda13a42098279d01ced5a2 Apalache Prime NumGe False Passed
  • Model Under Test
  • Equivalent Model
f4e051edc5c1c0708ed69f7a6d6b3f5f8699539a Apalache DefFun NumGe True Passed
  • Model Under Test
  • Equivalent Model
d52e838a567029cf98d839afdd7a786fd7a8ea6e Apalache DefFun NumGe False Passed
  • Model Under Test
  • Equivalent Model
2319f20e3430dcca196b1422f27723d2508731bf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGe True Passed
  • Model Under Test
  • Equivalent Model
5b4e857d710481bb97ea8cc375452e79d2ed78da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun NumGe False Passed
  • Model Under Test
  • Equivalent Model
d0fa8910700c07d7ec7aef1d7dad70c214339808 Apalache DefFunRecursive NumGe True Passed
  • Model Under Test
  • Equivalent Model
21671f28fcab2750e8c9018ae383f57bdc025c8f Apalache DefFunRecursive NumGe False Passed
  • Model Under Test
  • Equivalent Model
4a5f09f7410ece3cae2e4e950a5b5e11b81c88b5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGe True Passed
  • Model Under Test
  • Equivalent Model
00417c2cf8b66228a58b430921259b32727a9c44 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive NumGe False Passed
  • Model Under Test
  • Equivalent Model
f6d428a67ec4c30418cffa8fe6ab62463461cf91 Apalache Def0 NumGe True Passed
  • Model Under Test
  • Equivalent Model
a0f95ad1fcbbff06e8765970ea998eb8c6c235a4 Apalache Def0 NumGe False Passed
  • Model Under Test
  • Equivalent Model
f7a9a04da8f51e8385bb76b3e09f6bb7bf2f1315 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGe True Passed
  • Model Under Test
  • Equivalent Model
f15e1806631f0628c26840095e369f6c7c177f86 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 NumGe False Passed
  • Model Under Test
  • Equivalent Model
ba33ba2acabed7abe45165df2a7a084742bb5154 Apalache Def1 NumGe True Passed
  • Model Under Test
  • Equivalent Model
7cf0470a59ea5e3ce99cb95c3791adcde38eceb8 Apalache Def1 NumGe False Passed
  • Model Under Test
  • Equivalent Model
bcecedd60843204f9b26cee96df0a3bc689a643b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGe True Passed
  • Model Under Test
  • Equivalent Model
0492c0ede8553bc9ec25fbe6feb7759a69af5c91 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 NumGe False Passed
  • Model Under Test
  • Equivalent Model
a41a411a1451abac9eef6a87e9319a6c9e71fcf1 Apalache Def2 NumGe True Passed
  • Model Under Test
  • Equivalent Model
d7524c0aef0d29dab1d97d4387712709b3cfaded Apalache Def2 NumGe False Passed
  • Model Under Test
  • Equivalent Model
095c8d6ddf6bd95094e855b2b3704f0bca105bb2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGe True Passed
  • Model Under Test
  • Equivalent Model
571433af2f70c8add46effa949a4029737a3c573 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 NumGe False Passed
  • Model Under Test
  • Equivalent Model
36f7a1137b330172072e62a3190472a9fe651ff8 Apalache Def1Recursive NumGe True Passed
  • Model Under Test
  • Equivalent Model
3a737475a74b44d12fffaa6cb7ff720eb8e23257 Apalache Def1Recursive NumGe False Passed
  • Model Under Test
  • Equivalent Model
b3e807548f5666a765cea5fa2439730b14992763 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGe True Passed
  • Model Under Test
  • Equivalent Model
c302fc49cca0cbaa3dedda800ba56951806e0479 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive NumGe False Passed
  • Model Under Test
  • Equivalent Model
13a8a6f1def2a46a87b2c6155ece0953ebdb3c02 Apalache Extends NumGe True Passed
  • Model Under Test
  • Equivalent Model
eb6a5a3f284b744898bf85a3cff6bea0df3bde75 Apalache Extends NumGe False Passed
  • Model Under Test
  • Equivalent Model
10ac6798b0d19f94e39b2fbac873cebdd2164292 Apalache ExtendsInDifferentFolder NumGe True Passed
  • Model Under Test
  • Equivalent Model
44823ac32e8b481415b435172c23836d4e3e7b41 Apalache ExtendsInDifferentFolder NumGe False Passed
  • Model Under Test
  • Equivalent Model
b510461c6013481f881b205551d22b29057fefda Apalache Variable NumGe True Passed
  • Model Under Test
  • Equivalent Model
2665c82e450072ba812e7cb6284faa9cc46827cd Apalache Variable NumGe False Passed
  • Model Under Test
  • Equivalent Model
00db2df66194808a44e7152c694f8c895e5e3c7e TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude NumGe True Passed
  • Model Under Test
  • Equivalent Model
114a1976853a4b5dc39ef4ffad629ffb691e4be0 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude NumGe False Passed
  • Model Under Test
  • Equivalent Model
92e8fd9ba963fba4365763709dc446b2dee2db68 Apalache Constant NumGe True Passed
  • Model Under Test
  • Equivalent Model
010c79d17d23c88e47fba48763b0d754adb591d2 Apalache Constant NumGe False Passed
  • Model Under Test
  • Equivalent Model
d8fe5d064787bbaf66f3e2281832d1dc8d146d19 Apalache ConstantRank1 NumGe True Passed
  • Model Under Test
  • Equivalent Model
06099c50e51b55fc04053173940d3a39d3381a75 Apalache ConstantRank1 NumGe False Passed
  • Model Under Test
  • Equivalent Model
fe34d5af9050ba82ee0eaf0ca59480ba74849771 Apalache Instance NumGe True Passed
  • Model Under Test
  • Equivalent Model
f14f1977b8abb4739001d328da60af96baf72704 Apalache Instance NumGe False Passed
  • Model Under Test
  • Equivalent Model
bc3912e1ed2142d29a5811e13f68d5280ed56177 Apalache InstanceWith NumGe True Passed
  • Model Under Test
  • Equivalent Model
59fe0d56b97fa3e6e2e1dbed8fbf1de84f7d9a58 Apalache InstanceWith NumGe False Passed
  • Model Under Test
  • Equivalent Model
2dc0c258071affae4321a9b6dbdf4a43b82cff6c Apalache InstanceNamed NumGe True Passed
  • Model Under Test
  • Equivalent Model
5139c50e9c01ead850c9125dea9dead82553498c Apalache InstanceNamed NumGe False Passed
  • Model Under Test
  • Equivalent Model
2d59359875b54ab5b011751291ad51a84cd9df71 Apalache InstanceNamedWith NumGe True Passed
  • Model Under Test
  • Equivalent Model
40bda6d44932330341d7d406d52e718538bc6e83 Apalache InstanceNamedWith NumGe False Passed
  • Model Under Test
  • Equivalent Model
33976043ddefc3d1569647682eea0d0e21029b5e Apalache InstanceInFolder NumGe True Passed
  • Model Under Test
  • Equivalent Model
aadc2cafea357ccf7509bf16144872bda66886ca Apalache InstanceInFolder NumGe False Passed
  • Model Under Test
  • Equivalent Model
086a15188091e8535a4e1fc9bb3231366b2b8eb0 Apalache InstanceWithInFolder NumGe True Passed
  • Model Under Test
  • Equivalent Model
96cb079d80829eb3b887a4d8d1b82f53cc97bfc4 Apalache InstanceWithInFolder NumGe False Passed
  • Model Under Test
  • Equivalent Model
39051fbbef09b81b7be52f0d878c88de6940223a Apalache InstanceNamedInFolder NumGe True Passed
  • Model Under Test
  • Equivalent Model
96bef38c9f02eb9bf2f5a444b3adbe102590694f Apalache InstanceNamedInFolder NumGe False Passed
  • Model Under Test
  • Equivalent Model
2fb6a6db4981cddfef0ee0b27d588060b2bb9e85 Apalache InstanceNamedWithInFolder NumGe True Passed
  • Model Under Test
  • Equivalent Model
14524d0ec3b98f606aeec47134a054df0abb1b12 Apalache InstanceNamedWithInFolder NumGe False Passed
  • Model Under Test
  • Equivalent Model
71a591cc6dcd2fb77836d8878ad0781d5c08e2d7 Apalache Enabled NumGe True Passed
  • Model Under Test
  • Equivalent Model
837bb2f23109050933d190542ad1cfa32adc637f Apalache Enabled NumGe False Passed
  • Model Under Test
  • Equivalent Model
4a9e811a77a149043c69245ef0bc107d8a9e4248 Apalache Assume NumGe True Passed
  • Model Under Test
  • Equivalent Model
e20c72b428a59fa8f9b802c40a8ce7994da1f00d Apalache Assume NumGe False Passed
  • Model Under Test
  • Equivalent Model
715a853cff3d6e0f7f56712ea7ccc89c1b1d0fb8 Apalache AssumeNamed NumGe True Passed
  • Model Under Test
  • Equivalent Model
b441d28dd2a2b0b5e99ca8c70d8742ef14397877 Apalache AssumeNamed NumGe False Passed
  • Model Under Test
  • Equivalent Model
3dc1cb0f989d7336a9a089e9530987fb8e245fd9 Apalache Lambda NumGe True Passed
  • Model Under Test
  • Equivalent Model
ce1d352d570b31f00f85d6a1a3660a9e47051065 Apalache Lambda NumGe False Passed
  • Model Under Test
  • Equivalent Model
e6a0d0fc7ea21159cf93d8ca565ae35cc353bb3e Apalache IfCond NumGe True Passed
  • Model Under Test
  • Equivalent Model
39131f23645a6f03bd0f84c4c9739fac7f1d797a Apalache IfCond NumGe False Passed
  • Model Under Test
  • Equivalent Model
14d605d4ae3d68556a60436433ccc06617111ac6 Apalache IfThen NumGe True Passed
  • Model Under Test
  • Equivalent Model
772a43d23e54a1d8f28facccb1065fd456b4ce73 Apalache IfThen NumGe False Passed
  • Model Under Test
  • Equivalent Model
f3c080388e78624fad72878a08f9935cd25f8fbe Apalache IfElse NumGe True Passed
  • Model Under Test
  • Equivalent Model
c9484fa1f02da6625c2c66c6a4f06d19d2c78f9d Apalache IfElse NumGe False Passed
  • Model Under Test
  • Equivalent Model
4e2da392d4f230021a719d3bd09cfe8c3ca814db Apalache Unchanged NumGe True Passed
  • Model Under Test
  • Equivalent Model
1eb4f6ccb1c8c2149c6dab09e55cb59840a532ce Apalache Unchanged NumGe False Passed
  • Model Under Test
  • Equivalent Model
f2494a9d39310f81bb4358f23db28e4fe79d7ddd Apalache Equivalence NumGe True Passed
  • Model Under Test
  • Equivalent Model
eef832b66d31b3a3fd5133ed440a5fd1e61d0f2f Apalache Equivalence NumGe False Passed
  • Model Under Test
  • Equivalent Model
28d950f41706c89c3e4dc791b91cd551a61b70ef TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGe True Passed
  • Model Under Test
  • Equivalent Model
f7955778556391c7a64a9dc82cbc4ce6b6a79c17 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGe False Passed
  • Model Under Test
  • Equivalent Model
7ccff27968dae0c85e745e0b7a1c550be94fefd9 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGe True Passed
  • Model Under Test
  • Equivalent Model
0e6c885f58f48310901dc55dbd31351ef3a38471 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGe False Passed
  • Model Under Test
  • Equivalent Model
211894e25d86e8636243941596656c818d3c371e Apalache BagBagIn NumGe True Passed
  • Model Under Test
  • Equivalent Model
c39d7ce45e0f6c62514d3014ca4dcc28d9e953e0 Apalache BagBagIn NumGe False Passed
  • Model Under Test
  • Equivalent Model
db8997d8fca980e10f1519028ef96c1b910416f6 Apalache BagCopiesIn NumGe True Passed
  • Model Under Test
  • Equivalent Model
2b2dc5b1512f53ac8218182c0d76856a8aa32931 Apalache BagCopiesIn NumGe False Passed
  • Model Under Test
  • Equivalent Model
21976a7f94d1a43d758635d8e0737ead5a4cd3d6 Apalache SeqAppend NumGe True Passed
  • Model Under Test
  • Equivalent Model
4d4bade0969c76a6ad681b3a7c65813ae00cd4df Apalache SeqAppend NumGe False Passed
  • Model Under Test
  • Equivalent Model