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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
84fd79cb5d2c9c8cabf46164501bd81a22a6265a Apalache And InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
2314f1b11127cbae7142737d43db5bb9b13cec87 Apalache And InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
5cfd8e1024773fd0f159f3f94ad57ab1df93e4d4 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
794868b1f9bf640d1defef599627cf777b7e707d TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
5a4992ba4f56d1f23b8a0f94a387e4b0474cd40e Apalache Imply InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
b231c5191d67615750c4be71882b7b01eb4efa0c Apalache Imply InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
e4270e413ce5ec66ba5ea41f1a570745799bb02e Apalache Not InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f3131638869f25af878573436326ffe73bdf6946 Apalache Not InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
21f26e0588f13b00d940eaa178113359c7b7a375 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e89a4574f6a79452dd289cf2b1dcfae043a61504 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
d545605166f9ae2d82b724cd7ecb4f50fb9f1bf0 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
c3a25e2909b68681299f1edb115c787556608f83 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
a6db2baee279bbc6735321e405156a44a023e912 Apalache AndProp InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
fb69af4cac7248b86bd94bf1996df1df7d130048 Apalache AndProp InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
23a1e48936162fbf7f03da783377e8171ca812f3 Apalache Boxed InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
c00db02bd250e2775f379d8828dc693cd9e2bfda Apalache Boxed InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
13e81d88d84063c2b4e44d9a41fc456a1b9148c1 Apalache Eq InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5399228d71bf254cb838949c959f12754571cc0d Apalache Eq InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
74285f84fdc14b1443e2c0a34c1b8efb9d596617 Apalache Ne InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
dbad4313c09fe43686b025183abd3f8ac5d07910 Apalache Ne InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
01184f48bb8fd128bbad86f60d2da02d331996ef Apalache Let InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
8dd1690c9e60c7de15c8aabf4a2dc2dd5256c7bc Apalache Let InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1c97f35a59f4489dacdb384597c69bc9dad68695 Apalache Set0 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
983695a3fdab57fbbb4e59daa6e27e629f8b93e0 Apalache Set0 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
cae62e74626af06db00e04c078daa6bafa717088 Apalache Set1 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
332efddf527ec827778583d4a51b935df49f29c2 Apalache Set1 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
f4d0c572c229bc8af2edd5c1c4741a4a2d017d17 Apalache Set2 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
0839231220f9d2f3328a54e9d47ba12fc3f0b862 Apalache Set2 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
bf8705a8125b4925dd1f4423a76bf78c43440d95 Apalache Fun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
523c4a6584c6aaf07c4443dda92dda34bd36d472 Apalache Fun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
049bff06d6a9d7ac84524861d91cabad94a0674f Apalache In InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
3ddad21c5812773ea46e85dd92a936a858784442 Apalache In InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
81e9ae363ada3a04eb37a52e9a2536f121245c6b Apalache NotIn InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
26b00f2f5d5baae1393cd6c3d97d55498655940a Apalache NotIn InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
4c749db7c56bac76445be1770a8216a695f8db40 Apalache Exists InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
fa41514bf04a8fc38ef1e86524cfcf7625b37a33 Apalache Exists InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
30811d65ceb2cd4790f6a464e01f01a7aab27569 Apalache Forall InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
4f41db3f67b589428cb736d891163045dca2a6d1 Apalache Forall InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
79d57173391a409318e91a89c7ee4e2450303215 Apalache Choose InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
3d9c54bc307c5f55f41a014710e9126798a199dd Apalache Choose InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
55bd623d226885db57350d02c7ee8bc159057973 Apalache Record InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
527d057a580f1521b317a3aad7be6920199faf19 Apalache Record InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
c7401a45a520b4aeec216d64a63dc8be8dde3166 Apalache Tuple InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
b5b109cbac6b1d9a2b9acb47725bd3508808febc Apalache Tuple InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
7ea5e3d4ecf41dfdf367ab07336a41e444680643 Apalache FunApp InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5c75d14a627399f6444c580f643a466dfbec6d08 Apalache FunApp InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
6fdb02e94cf17f356bd58e94ebc85df49b7c58f3 Apalache Except0 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
37e1d9597d931f8edb80a679db31693371b6d175 Apalache Except0 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
457c4c62043fb8e103a208a00ff0a6f5608a22e5 Apalache Except1Fun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
99a21ddf1bd0b94413885938254c8252b15963f5 Apalache Except1Fun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
fcdae3ed72a9af9a5fc15fba8369cdc13edc7e93 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
768b21a697c2c3d63af4b945521d9378c200c352 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
fce049c32e2d5596c214477bf2daf777ed7487f1 Apalache Except1Rec InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
159a73370d132f9c341149abb1ca504644aca161 Apalache Except1Rec InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1da9a178c80817be9f723a46d988aeb882611fbb TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f0abe957eeebb792e3df7e504eb598370bbc7270 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
b7c799973f4410f9d1a127d01797ee6c0c0786d7 Apalache Except2Fun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
533a3c681660bfceb86b7c994d18aa9fa56bd5b3 Apalache Except2Fun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
2b601b32f244eed1b46ac03b2d6f7402109643c5 Apalache Except2FunTuple InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
c49dd30ecf9760bc0ee6b5ad655ff3c2f33e768e Apalache Except2FunTuple InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
a5b4f36c3cd62967746f7081496dc14b0fe19164 Apalache Prime InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
4e2e76f2e097eb31fde07c1ea5458f831be366f1 Apalache Prime InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
71557d88ade96adb1295289d6882a29c3ac7f0b2 Apalache NumUnaryMinus InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
3752294f68e79920da4631eafc5d48f8de67251d Apalache NumUnaryMinus InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
3497857d4e2b1cd7b3675a962bb2ebda4e38436b Apalache NumPlus InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
4b9a7477ac2abdaf6e760d6c39a7a2cb5132cf2a Apalache NumPlus InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
13836d995f7da44d0dc3cc0245099cca09bcc790 Apalache NumMinus InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
604be757e73ce07a7f33c328ea1237b56f5898c7 Apalache NumMinus InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
a4e7ce775ac7a6496bb0314680df48e0e5be974a Apalache NumMul InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
70ea8268355d26ea9931c2f645dada2f6cb81eb1 Apalache NumMul InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
80472baca623054597741da9dace43180db2a4a2 Apalache NumDiv InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
8e5de43388eb5759c64957c6bb186a704e2bcbbe Apalache NumDiv InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
270adfed95af3f217fe4eaebcc37f1791bed59f6 Apalache NumMod InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
12867835aa2f98103ca4841f05e22e44e06b56fc Apalache NumMod InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
6d9b4c88b66cd7d1a6a5181d4f8e4bfba1247fb9 Apalache NumPow InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
d8ebb4ca04181ac6bf525aa1d66e486e2461e810 Apalache NumPow InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1696d17d8c85b84d41fdc80867a93e8043db6ec9 Apalache NumGt InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
4a206451dc937ccaffd5d003c93f77c672f8e1ff Apalache NumGt InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
76f64f6eca193b7b3d6dd88d8dd8f80e0dd506cf Apalache NumGe InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
70993923652ec5683923236805cbffa54259c231 Apalache NumGe InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
f24dc6c113b674eaf807fd6ecb7e5449fccb3b85 Apalache NumLt InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
cf067647d36451e6dbe01d8f6b454efff9c81455 Apalache NumLt InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
f6f7eb57d5fefe285228774349e2df11689a7f92 Apalache NumLe InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
616b65b9149f517c0d8bb481d8f2b2e33e07b9ae Apalache NumLe InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
d697df3b125b41b0aa6b0b923d835dfc736caf41 Apalache DefFun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
aaa3835d0e12a4a749147f966659dd00e0affcaf Apalache DefFun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
a001d0a144e9148e21f584f45d35d18b4038dbff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5e75123a73e780b91c6700de9c7c4855a6653a5a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
327e6b437c4baf5979eef9af8f5f8e547e68c957 Apalache DefFunRecursive InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
621704ecae045678e1bcf83c3939105ed4cb5607 Apalache DefFunRecursive InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
0377d73f5c36f73418dee46cf1824ed7bdd90f53 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
811b7c4c596e1ea3851dcee445d7c557c4f0ad6e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
ba796252672dda62d1aeb3a7b06135a8f87e0838 Apalache Def0 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
cde7e7691b7ae7b84b4934ff054a89ee237cbbec Apalache Def0 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
8e328870cbf94813b147baa3d7e31f318e4651fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
46c753c3e709dd81698b656953c8e128aa140c83 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
9bd5c37e5be3df06014efd9a41e27269e72e650e Apalache Def1 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
a765aede3510372b63dfb2ed7e920a50b991d9f8 Apalache Def1 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
76cd2e7ca7d9560885ed35af51f793afd44912a2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
d60932465786f2aa833d521909eaba30270b9c94 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
f9b6fe0166cfff174e65050a478551b1380874e5 Apalache Def2 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
c0703757ca11b4e4a75c9718f836e9f825e967bd Apalache Def2 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
831082975f207bb144043febf333a5861d1171fb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
140c3366fee0c388ef3bb9d6d71fbeaa5b35cd98 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
00a1d44f1d614f6f3ba3251c7372066d55ec554a Apalache Def1Recursive InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
eb8053bc41226d1c29c80fef710d2d2aa11d1460 Apalache Def1Recursive InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
c659ccb9f1843cee91cb020ef7fa00105fe4e1c0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
d3a81407792dd11e3915e4128e3472636cfb7040 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
d9ddcaccec233c092259739d809fb7b1f5109a3b Apalache Extends InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
7db4e3ba5fca3b1ff8199d2c3c11ddd1bbec59e1 Apalache Extends InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
2bfc0972cdada79046d19a91936531f086c00636 Apalache ExtendsInDifferentFolder InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
2b404732eb4376664c4b44b93dff27f04e6ae4f1 Apalache ExtendsInDifferentFolder InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
d9e85090b15f6bfe3796c3ed188347a8ce85d972 Apalache Variable InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
8a40c16f08575484f82b57a23fe397a8ec6f2a56 Apalache Variable InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
0bc705120dfe0475551c0c44c435f7ef85d8ca81 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
2124db818b387f0615d2ac10c166bef3f3016ea7 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
03886f0012832242035880e5849e2101728384bc Apalache Constant InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
64169b8c11814e7bc0eff3ecb4870cf46688b566 Apalache Constant InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
07cb4275bf8330dfeb87e33d3e313dbd5a577c83 Apalache ConstantRank1 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
a7441c39542c8bdefa73494ac06996d1b53f7009 Apalache ConstantRank1 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
6696a7fd38faf14fc6650ce75078adeb37b23639 Apalache Instance InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
a3ea98f64464e28dc8b1e67ec764a866a4a832ee Apalache Instance InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
0b9777aab1ee1d5bdaf5e078812585234575aa03 Apalache InstanceWith InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
8635cba93eb0e198dff916d517b5c5c32dec8a69 Apalache InstanceWith InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
b0d027d7c376e58ad45bbc2f2127f5734846bc89 Apalache InstanceNamed InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e1a3a4c19ba09d956f77960a2bf8f7907e10299d Apalache InstanceNamed InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
943b53ca306ca753970e2660243b51c645c326b2 Apalache InstanceNamedWith InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
279cb42e503ddafd6bc4271cb726b296f48be430 Apalache InstanceNamedWith InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
a84f5a6a1752668502518a0a72f171844132faa4 Apalache InstanceInFolder InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
070d784963341829ad532c570971ce1aa39281fe Apalache InstanceInFolder InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
b31fb73199ab7b134d8a6be5b8c868c7e3edb5f1 Apalache InstanceWithInFolder InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
9071c47e366d4829bb7b48cd9640a828cf592479 Apalache InstanceWithInFolder InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
6ce3360aeb00abb722f7af74b49e8ea27ef9f713 Apalache InstanceNamedInFolder InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5f726e3630442176506717fa4a04991e60a4e424 Apalache InstanceNamedInFolder InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
dcd54b18881875bffc2a344aa21dda5652cd78c6 Apalache InstanceNamedWithInFolder InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
b863290fc92e58149f894be5d903b5a4a0f009aa Apalache InstanceNamedWithInFolder InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
02837c33988de99a34531811f038bb15e2b03885 Apalache Enabled InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
596b7bd245b3df0f5be2cf3168c5c280bc996432 Apalache Enabled InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
61d7ac904a416b3aef63155b08e9fce6c5b04de5 Apalache Assume InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
b2a14f5233d3baf53cf8c2d98b72df2fa89176b4 Apalache Assume InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
dea01e8ffafcafd3b37738670d701583f74affa0 Apalache AssumeNamed InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
de5c1257e664598d33cf549dedb1ae9109a75e33 Apalache AssumeNamed InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
0b59c51b50e4a12864b87acc13b8b922bfb10d8d Apalache Lambda InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
c58f648f764357c8c836e7374d85feeb8e15a980 Apalache Lambda InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
8bbfc0029be83bd8cc26fc713782699fb36721f4 Apalache Cross2 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
c78605d9e56e837968b5edad00058a9071f223c0 Apalache Cross2 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
49e9ac503ac1f648a999d202c2422d2dfb5d08fb Apalache Cross3 InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
09f3438e44112a19a87960a075650586d44f7d26 Apalache Cross3 InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
249e11cc2bfa3d2885c0c8eefeff7d5a667e1f2f TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
b08579acfa0cffeee90c2683276aa1797a34a779 TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
7c1e872f299b810915af2c206d48e0b3b8b3d1a0 TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5f9a1c87d539516d041ac3e23bb291d4ca35038a TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
41aafa18eaa9c32a9c77dde1b38730647505a456 Apalache SetDiff InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
38e879a0b86ea26477913de3a5938785be28ecac Apalache SetDiff InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
38d2af1e2641336fc5f781708df15146abac171c Apalache SetUnion InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e7f411f2a02d3e5720f2c2271639425db64f2d9b Apalache SetUnion InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
eb6773daba45888250f922476004193aa21939e9 Apalache SetIntersect InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
ce471dd3cdf6cb4bd3dfb01d6510e2d38928de30 Apalache SetIntersect InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
e3b82560a6890976a9b5ca5d92eaf71cd22de810 Apalache SubsetEq InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e4581b6afd36400db6430aa794968c8180fb6ca0 Apalache SubsetEq InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1dd42248093731f4b75ff98e18ce70cd3e8fe824 Apalache IfCond InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
6d7505c965d9e0a6bf8e79b3f3b92b3135280bcd Apalache IfCond InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
9c22be4e49bb1bcb4a63ee0faa8c211530a9fda1 Apalache IfThen InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
aeef8a769cbaaa38b8eb3d546a9a61cc1532ee44 Apalache IfThen InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1acaeb91c86e9f2bd7bd60615290713ae18bd5e7 Apalache IfElse InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
0c3169b28c202510fecaf1f3c1199b9b55966636 Apalache IfElse InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
18e022c464d5d75d1363c65943afaf06aa4fbbe3 Apalache Subset InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e9a4fef40af8c6b67b3d1b99b1b8e1e9c253dc36 Apalache Subset InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
49dd052bb419d2f67523261e0613f2175c77d7e5 Apalache Domain InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
741b4c7c134cdd61d7e067ca5ee96f1994d99d81 Apalache Domain InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
d6468f6e19b0fca19210fde24a7d5f596d71182b Apalache Union InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f6950808272ede0b297be85984d45c5d4dfd6aaf Apalache Union InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
594ce72e4cbfea4c0fe53b00cc79bfaad1840b87 Apalache Unchanged InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
10f348700faf3907563dd6dd81cb4c2c93285f4e Apalache Unchanged InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
68fa67e77564996c29ef40c758db7c2aa689145b Apalache Equivalence InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5acfb3bda2efbde08eae9738daab627152298239 Apalache Equivalence InstanceInFolder 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
2741e1d9f04253c9df632c7ea6a1e38b56e7645a Apalache SeqConcat InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
449cbdbbda79538b17821726dd5af38a15190507 Apalache SeqConcat InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
3e23d9b183fcaa62a395a714768a5b967a936422 Apalache SeqSeq InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
8eab66e89435e17c17238599c4d05d5feac8aed8 Apalache SeqSeq InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
7393ce0590380bd5e598f6e11bcd311c6d119e51 Apalache SeqSelectSeq InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
92747afa0f7ea6dce186deddc7680819dfb49e5d Apalache SeqSelectSeq InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
d28a4ba8e0feb864e428f113f0eb4f1cb7fb746a Apalache SeqSubSeq InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e730254c3b488e04653784b0bdf46c1972ec9e6d Apalache SeqSubSeq InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
704141392015d62469eebe117aba794d0950161c TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
a95b604914753d80c88ae14fea231334f8c4f130 TLC with reduction strategy:
  • Case Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
NumRange InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
b966856cbfb603b0520e6b860ba7fe3c3f263a49 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
1b57f3a98390c6eca8093c7947858f48264f7b30 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
9bde8e80f26ab37bee2bdf8e14c405d2eb06848e TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e954236b328cedb485ada1fa141c1ec660348f55 TLC with reduction strategy:
  • Case Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
TlcExtendFun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1bd9ede7984ceb819291d2aeb3d328aad963b538 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
32de3be4b90c748f30af0cc1ed9a19b8a58cbced TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
cb0991e84321b503227b2e8d2436efa18418fb87 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5094790181db102437f9c4d929b7e289019fc57b TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
c7cccc83aac02b2dd4898e1541fd95a7828614f5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
ab7f2d8dafba24691436a375edc10e9f00d28ea5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
7ff4f4c5ab5fe19c6e1674007671543404db12da Apalache BagBagToSet InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
63803b851268ccb4f5cb37f68af01e2042320092 Apalache BagBagToSet InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
8b1d0442379ab4d1f8b55fccfbf30048f58dea5a Apalache BagSetToBag InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
5f5256d6c640f3e954fde62252c2d21c4b8f5bc6 Apalache BagSetToBag InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
75952b0d41cfe06947685ac9e83ac75e9b0ea290 Apalache BagBagIn InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
92424e7c0b4f415a236dfc921c7dd383453db990 Apalache BagBagIn InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
ff2fc104701ece1426c172a3531511a567a16417 Apalache BagAddBag InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
ac4c4d93df621be7b5b97b8263dc8dd04bbb6614 Apalache BagAddBag InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
1a98969576b61e01d5f1698de377091b22241e04 Apalache BagBagSub InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f970f0d86ddd36cfdea4e781a3697b7fb90154db Apalache BagBagSub InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
9e9f378ae7eca07990804401e983dc49c386a7da Apalache BagCopiesIn InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f5be4877d76947989e1bc3eedd49b6a345a95871 Apalache BagCopiesIn InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
fe36d4e2fbefa2337116e7cb406a96f258428124 Apalache BagSubsetEqBag InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
220a92b937606a927cb54020e049040ff10f2b6c Apalache BagSubsetEqBag InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
6a3e246653e07a225232c6aa31974dd09bad32c8 Apalache BagBagUnion InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
4a02fa77e7c0649bb7b1d1549dfb9c42204abb0d Apalache BagBagUnion InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
efe488f941b32d639b8bdc71738e41b4c57776ac Apalache BagBagCardinality InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
896c3b412ebf66d986f79fa8964bce81d320b0f0 Apalache BagBagCardinality InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
154ff1005150337c020f0f4b5655a8f594e25c67 Apalache BagBagOfAll InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
69af128f554a137f87130d538e887d92a087fd34 Apalache BagBagOfAll InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
5baa905d3fca031a2a05033e6baa5f220bfaf835 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
cd571e576d1286763abab2a32819320679d8bca6 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
323bbb798ba96bb3643b84eff56e453956fbc7c5 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
387033c955e55aaf6e828e53745a84139375eaa4 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
769d02bf73e12fbef72d28813d83f85500a0e18d Apalache FiniteSetsCardinality InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
412fbe564a83b26282b85c62287eca522f38c70e Apalache FiniteSetsCardinality InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
9f2a9b61306ca7bc9194125bf280252456d7b416 Apalache SeqHead InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
e1a11a631a30d15d50c8f1c2ddae1eced115a428 Apalache SeqHead InstanceInFolder 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
04c5abc9152993163815302e1bad30984bb794a9 Apalache SeqAppend InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
12497bc2437989b9edb361763121ba46d6b7df4c Apalache SeqAppend InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model