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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
3231ad2afc09b3722a423023e0431198d71ab3be Apalache And ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
31effcd0fa642aa46e30fd5b38157c6da51feac8 Apalache And ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
fd778bb0029d4ccf1b88318a26f5fca0d8808cf1 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
3113f710c346730e825ef53409ae8c0db727ba83 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
bfa8be86b02376bea68dc5ad6b948bdafc9007b0 Apalache Imply ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
34d984f5c13db2329df820684741d4a4e561ce4f Apalache Imply ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
75a38b6ee73c21a109d286c0d491532d23280b90 Apalache Not ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
104109ca0379f178e46cee4a878fa9abb4ba3a28 Apalache Not ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
1c64a448aad6acd9b89836504cbb62aad65e99cb TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
9fe0fe1f6c218b528a515ec10bb2e3f84523183f TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
fb86b646f57cc8c29aeb19bfff82083702516592 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ae50b32e3a27dc6683a28c202515c37e9964b61f TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
505c1b9a11ed4b846e55dc0b8cc74630901c54ce Apalache Boxed ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
eb64378a777339054d56c3738555bce24607f832 Apalache Boxed ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
68534a5d56ab699737204fc5f8b0929cb3fe2055 Apalache Eq ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
449b590ae2331729a8e948de9a08396c29d3920d Apalache Eq ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
157d637f923b54b41d9d4bc6bcf45103543e9ba2 Apalache Ne ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
b561b1b899128f490611c0a465bc9e82e28d0751 Apalache Ne ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
dce00ecb69a24037e69982e1f954582a826a964a Apalache Let ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
17db1e59351f20a5c36433bd8f91edf3ebae3e85 Apalache Let ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
dbc861e1e3dd71a2945f9cd4c940741110810d51 Apalache Set0 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
0d74f7c5c26b51f1e9bad6d8a52de6a337f5fc8d Apalache Set0 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
0ba96423fa072eb702ad1817f55174efb7fe5d56 Apalache Set1 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
a75edd0e190fd08d5f06004e9fd1602eaee168ec Apalache Set1 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
aa52804299fa0901d8286ee4d52f297a598c47e7 Apalache Set2 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f3e1078d502edf6aa52418a550c6080df8f2578e Apalache Set2 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
44dd31d0e57a1dd42807254ca9993bdf1fd8c703 Apalache Fun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
6a851d1ea01bd5eebba7be6fb59719ab64b921b0 Apalache Fun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
9d7433eeb66bdadf90e54af6e4ac346c7cbc0a1b Apalache In ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f912d0d3e6254c97da41e0d60aca17fee05cb7f1 Apalache In ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
3f5ee8a027335a73ea5b9401941e605ed3e792ec Apalache NotIn ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
19f1709798ecc0347dc62e7d7bd7e393627afb45 Apalache NotIn ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
d4c0e3d0f6cb5bc488111f25fa16607e88b54e88 Apalache Exists ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
2da2951fa4e7196827aeea4494f5b3e00e58b317 Apalache Exists ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
d593590aea3743c81f5e058313906c64694f4c4a Apalache Forall ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
fdd1e4f9e161e4bc03b49e12366e5f2fd1a4ca63 Apalache Forall ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
aae12e511b8a937f651e97e3c625efdaf2b03693 Apalache Choose ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f76fc5758e6214f4288a34f048a233291d12f933 Apalache Choose ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
2685a854371d63881a4ca0bc7715750135e3b5bc Apalache Record ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
35ff38dfcf598e85451221d56e84aa483137cd89 Apalache Record ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
707225cecdc27d6006c7797de09670acefbf0b1a Apalache Tuple ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
93fe9d3a8d62b1fbe8f6a137ae4481e08c1075d0 Apalache Tuple ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
b993d28cf283ab1f94475dc287b3dec57c69ae4f Apalache FunApp ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
e0e0e142cf9d32aa85f72612999a27f3106c05e2 Apalache FunApp ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c4c245352cfc7dba33845b5e8ac60928998ac8d8 Apalache Except0 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ca39a25d008f217453ba0239b8e571284d4d6bbd Apalache Except0 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
4ca3238aa4ad7ecb343c3b9dbdef6a57cb4a2b5b Apalache Except1Fun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
65265f0b39f1c909626de1c80560e364f1b48286 Apalache Except1Fun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
58f463294fc83b3f49be953ecd14163d70c6bb72 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
163ea0382f8c70cca5058ea8e59e8101dfd7f2ff TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
589112f4a0317a41a1023a936d9c38077fd1d707 Apalache Except1Rec ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
549d41ac6eb7ca954d5884e6c00fdd7c624693f6 Apalache Except1Rec ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
af79c12240bd21c520c889b4a933a36ff1ba3a8c TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f89a11650d91c57e240d7d13705cbe85c12fcad9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c73ab9b1ff74db60cfe179d531a35f17673882e5 Apalache Except2Fun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
37d71a712725188d07866ff6a6348184bc45ef10 Apalache Except2Fun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
b257d96f2065dfbf975635ef8d8c181b38bb3a05 Apalache Except2FunTuple ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f8a87faa4a1c965a4f0e5bcd9032c2a18144ef57 Apalache Except2FunTuple ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e7b805ee68422172316e9f876708443ae0b0d23d Apalache Prime ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
e17576b8f0ab16c7d87041e1e037360449d06326 Apalache Prime ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
de16ca2634a1f91670d9ef64097debba119004b7 Apalache NumUnaryMinus ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
6ed6e59d1ce50e5db1b5e9bc1763f0ec94f6a394 Apalache NumUnaryMinus ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
f51b24522476fc0401c2cb5ec64cf8c31c20414a Apalache NumPlus ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
62337c4079b844b6b140e0913291de08a661c164 Apalache NumPlus ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
98f863751c45ebab690fae17364307c1a749f3b7 Apalache NumMinus ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
eae58c60e09307b0ef151bf5db92c798cf223fde Apalache NumMinus ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
95b76802fc4a3ab9625eda590930545a58734816 Apalache NumMul ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
24bbfaa02b3a3b4cb7b2838344c1d0587c565167 Apalache NumMul ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
435fff60c5f52d6638ad93b08b29dd9cb6a745a5 Apalache NumDiv ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
6d54df0276fa8fcb9a34df544f4f185003b5660e Apalache NumDiv ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
471be2068d9b1238ffa4eb41a15c8273cb872498 Apalache NumMod ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
114fe751455c2f477fcb2d5f4ec13739452255f6 Apalache NumMod ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
530931a088af289fc2f578e937e683ae820f15d2 Apalache NumPow ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ad7e9e06329da5dd0c7322b9d1bb33484bc219f8 Apalache NumPow ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e9adbb23c429e7effb3c5bd9cd39053a9d1155aa Apalache NumGt ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
cad38f9315abce6a8e7af9cce1cddf6cfa1bdb4e Apalache NumGt ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
3b3043b806130ec4c71ca78b418d2c4ea8fd431c Apalache NumGe ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
5063748a93ada52325e2fb42510f11f862fdfa02 Apalache NumGe ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
0e8f73c597b5bed3e5fef79f2266af5f42641133 Apalache NumLt ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
bc3611c5d9295e520c58ea2c332a67b66b235db6 Apalache NumLt ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
0772ce55e2b6eaf7836fea37571b1ebe331bb88b Apalache NumLe ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
3c7efe2a92f6443d6e331e1118505dee0dce5d54 Apalache NumLe ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
28c4351c65b090353d8119226f7643764164292d Apalache DefFun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
5276954c8a6deba4546580bbfc606ca6104c3663 Apalache DefFun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
1c0293c1b76463ee2dc9d8570a2d1c003f827906 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
a90511896f92dfda876cfe55e9bdfa1a7a4f6272 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
9952d43287b67b3c7da32cdc9fd60732013d2242 Apalache DefFunRecursive ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
76d88883356026da40eef97c79716dc20db2efe2 Apalache DefFunRecursive ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
ea3e1d9b1d4c6e612083a9148bc2a34287534bf4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
66142f6879248950669978c9f726617c55e0537f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
ca61a4d415b64e078fb8e7f039b382e464873a03 Apalache Def0 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
135f9866e9f7592ece8eb70ecf5c9ff16f639ab2 Apalache Def0 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c0bbb48bb07b6567ac50b3b4de2759b75d820f4c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
91b2183e978a9312bd726869850c404b89334a9d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
02640d4cebd3814e5eb0c6da60c07ec17a75dc89 Apalache Def1 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
95698b2ffb904d7f6f9a1d046cb8ced281d1e893 Apalache Def1 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
f8789d0acee781b6d19f971714c8c3520d0117f5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f3ff79e9fcb329c551f3d59dbb8d72d9de4fb31c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
4cec99b460a522eaa437a76659511157105b5e87 Apalache Def2 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
61fa30f69767e6de44c58411acfa0e2607637348 Apalache Def2 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
cfd5e4a34bbda2a0deda790a430887c968d2cc72 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
b75ab081f5267b4897857a8545e90c247a757e70 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
045202c75ecda7ecc6c54110937d0be3596357aa Apalache Def1Recursive ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
e9c2ac4457d1f029b9c9b3d2aac6fbe07e7fe7b0 Apalache Def1Recursive ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
709d35b6464a209e966586b6bb5c86fc58c18eb1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
bd0c3a2bf69b32f5109819f6ec6289ac35a26a66 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
161eb8e7b9a295a940a1ef7dc53569b3e469e123 Apalache Extends ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
41752ce9a53801934478a858ef85513e5f0ad5b9 Apalache Extends ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
27358d9780170f973dc7db97f747145e7cd18cdb Apalache ExtendsInDifferentFolder ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
fad6d146ff5b54fd80185386104f6c2f274bd78e Apalache ExtendsInDifferentFolder ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
b7817f5a80e07c45580f5f57a53e156c356251f1 Apalache Constant ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
1a4a08ef829385b1c50813881464b2287c20825a Apalache Constant ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
2f0bb8c183b4afc95546b875ffc45beb24e13230 Apalache ConstantRank1 ConstantRank1 True Failed: TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point
  • Model Under Test
  • Equivalent Model
fddb90daec356c4b98a52883ae4cff1fb9b6875e Apalache ConstantRank1 ConstantRank1 False Failed: TLC doesn't allow to use constant as a replacement value for another constant in CFG, even though the former constant is fully defined at this point
  • Model Under Test
  • Equivalent Model
4357caa0d5ee29a7a2c02fa36f7b42fc2ce10479 Apalache Instance ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
e9cc3a09fbbf3e92ddadf3d661ac89ee33de8dfb Apalache Instance ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e6dc50404282317a692d0204a60d0de5f6f03605 Apalache InstanceWith ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
552328426bd9defeb729a13d70b2dd62f93cccca Apalache InstanceWith ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
d6a65681c2282b472c6962a4267433154b333a86 Apalache InstanceNamed ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ea0dea27de63500cbd6d02e68e16633135b4b982 Apalache InstanceNamed ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
70d428c652e52bc2e3f7671ec2d24ed1795c2533 Apalache InstanceNamedWith ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
b446ec0e40a7c9c2ac503e6661d5a3a0bb241c36 Apalache InstanceNamedWith ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
6b91705ef0c93b655d4e95ad5679757ccc0bc061 Apalache InstanceInFolder ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
8a583d1737abeaac5d330f9eb39b09fe452d7035 Apalache InstanceInFolder ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c81a07108d00dcf72c4b0ada9232aece1191e9f7 Apalache InstanceWithInFolder ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
6512aec031c7d955441e969387eea9f1fb7bf91f Apalache InstanceWithInFolder ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e02369d89e9804f1db464ef3c60ceff415b2b352 Apalache InstanceNamedInFolder ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
af1c4ea50693289827e9f786491d52d0db0d6cc0 Apalache InstanceNamedInFolder ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
a2f56b2b9a234dbc193b00eb92d31e3480f78eb0 Apalache InstanceNamedWithInFolder ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
2f7f4c38ba8144a563df474dd1f654ab466b72ac Apalache InstanceNamedWithInFolder ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
8e4b53cfc246696c75b2ced2c983d87c25e140e6 Apalache Enabled ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
acfccac88ea1418444694c7c67b1d7764bf6d756 Apalache Enabled ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
f0ef9fc1a561d95b941efc3372a20bd184ac92dd Apalache Assume ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
1e23a52d63459f10c3ce338256e9959884348313 Apalache Assume ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
576768a0c81e57138e551a1b43bb581452514b39 Apalache AssumeNamed ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
c2b7547ec7f032a3ad404bf88f685c22e67139c5 Apalache AssumeNamed ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c6ba49d5151b7cbcd08913b38dff4d4463e9b7a0 Apalache Lambda ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
10c7023c1764d1225b9ce4e7607cba5d23b2a7b9 Apalache Lambda ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
426ec8df2f3291a35e2800f084325489a0a16313 Apalache Cross2 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
16ba6561695a5c3a0be3441f5607fefa91d623eb Apalache Cross2 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
f5912d2ab28fad87223afde195baf93fa3a1fbb7 Apalache Cross3 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
7f5d33eda4ceaeaca9c5678122984d8fe0c579ef Apalache Cross3 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e6647354c591d85f2c3d27bd09fc54b780871420 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 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
50ec8ce4db74154ce1c645a00e36fb32ee20c09c 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 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
eb3f569bd74d63bdc12c79298fc9746bd5de1cc2 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 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
31e942e405f2dd125facda86364b8cf83cfacdcb 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 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
9917d4610b835ba3c8a66257d5200a8e1824281f Apalache SetDiff ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
4848fe673ee12b63a6a63750bdf064572a9b8a9d Apalache SetDiff ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
66ada128343813c98b3682f218b5bb4eced24c87 Apalache SetUnion ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ebf5c60a1fa2548a66208c723681651f28e32ddb Apalache SetUnion ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
1d55a4696a9b14b89dd4dc5d91bc953741df4c40 Apalache SetIntersect ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
b579306c0405a5861befd896af2f780353c955e4 Apalache SetIntersect ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
4f3f115b7e191fff4d383f739521241ecb93b20b Apalache SubsetEq ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
46b38f55f3892bdee50e0c3e83d1f86b9a25f428 Apalache SubsetEq ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
2f77d4be7050474cbc95791d0cd0d8e4f2765b5b Apalache IfCond ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
7075187047528f63e9d37ba870763791fa20fbbf Apalache IfCond ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c915e75da2d887cab3a50e422d8b3cceb9352e62 Apalache IfThen ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
d64d6c8925a5681740971be6ba969885e151f375 Apalache IfThen ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
0d4972f58689683fdb3e768525e10fc2eadb659e Apalache IfElse ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
76b51c2ea74fd971faff2a3eeee2a085ff66a7f2 Apalache IfElse ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
9030748409e14cbeecfe73a5eca9fee67f479c83 Apalache Subset ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
5d8386d32a502b456256faa280912f49fa4d644c Apalache Subset ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e20f92bb3074ed09fa3ecec11fb6724a5b8549c6 Apalache Domain ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f08fb8c741cec77f1c12a9f6ebefb1129c74f707 Apalache Domain ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
88df97e16507577a30f057ee6f21f03648c2de91 Apalache Union ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
5ceb6ff9110f6c62fbace991d63fdcb2c528c1a1 Apalache Union ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
d2a117eaf1ff274903c5405299f1860fbe74a38c Apalache Equivalence ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
c475e4e78c8735a3db4af71a0437f48cf94fe097 Apalache Equivalence ConstantRank1 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
bf24383be16776f49e88952b304f96f09da4a754 Apalache SeqConcat ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
81523d777bf197bfa56e4786b54f534c0475ac07 Apalache SeqConcat ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
ef4fc1847bda9a95f8d116b4abbf4f33aadb4041 Apalache SeqSeq ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ba759383cfe2e9ac7a27d5b5ff299bd0da770679 Apalache SeqSeq ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
4aee1e4fc04606ac86c1381ad1d33babb9a111f1 Apalache SeqSelectSeq ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
07c01c28d0a0c198fbac50ba659d468192a5b421 Apalache SeqSelectSeq ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
742ea498c1140cb1115f9b0cf39d5c9e94d72759 Apalache SeqSubSeq ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
37ec52b864e13fe693dd6bb3d01db0a0a9c98ba1 Apalache SeqSubSeq ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
ddea6a60307bedfeef92fe3a2a05de4468727ad7 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 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
d3fb3c55c925f1b000f8c3c5810e2e2a4cdba253 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 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
373f8e58a87e7b25cb68b3c6ad16a9f65fed152d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
3c890897cf76ce29b9b49547adf55c10d631abe4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
b9ed4f964dcedbbd2daebc0627bc99e62ad52d98 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 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
56798a72cb8df5b53570a24b60b4928573c27a12 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 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
fe5d70f9989255d3a7932aa2ac781937b2c3723b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
1c3b56b68ac5fc968027abc9765cabd119045730 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
0d99b5034f11bacf165b15f29c57f8e39c04c7ba TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
fc27e96385ecaa72116d262ac67dbafd80908242 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
c0e84e2f701c09dfc9094d2e965398186f35599e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
c8f2d2cbed13422fdd0239a4c28db39d552055bf TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
92391c97df39fe264f6eff68da2dd33e86cec5a4 Apalache BagBagToSet ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
8ea4b58783303b2a86b3bfc1a037c53bbaa72497 Apalache BagBagToSet ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
86540ae656e84f30fc8575aa85a7a41dd0243ab1 Apalache BagSetToBag ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
f073e4d80676dff6110897fb55e25215af08fdde Apalache BagSetToBag ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
2ef7b2b81f4d42fc575c1f26b283d99da8896a81 Apalache BagBagIn ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
090288f6f666b42ba5b2965cb24966be0944d25c Apalache BagBagIn ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
f004e36164414112bfcc5ab8bdcfa9b90cf05003 Apalache BagAddBag ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
9d80187eecc0f01b1ac65a52c46af2c85529d5fa Apalache BagAddBag ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
3fece4a0ace37b4eb3193b2e93f7539d7ec2d07e Apalache BagBagSub ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
925c68a0633b94a299cf691de8d74b4e1fe192e7 Apalache BagBagSub ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
f34adaa74819d3488d298413ef823ad5e8c25bf2 Apalache BagCopiesIn ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
6bc2d828549a21ad2f510cc8f8a43634f43baf73 Apalache BagCopiesIn ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
5c1f96b51a5d97532127d70ad1dde9df853ec5c6 Apalache BagSubsetEqBag ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
0f32d90c32659aa3582615350c9c529309b88d8e Apalache BagSubsetEqBag ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
6a7476b208205241083369cbf8c1784ac683de24 Apalache BagBagUnion ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
4a0de05d1eb5e9045aea4ddd18ae9a877bfd6f98 Apalache BagBagUnion ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
e7bf89ec680ff044d3bc81bd58a7cc6622a6db5a Apalache BagBagCardinality ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
e05612c8e0bf6e0539008f67fd48a19679dd17b8 Apalache BagBagCardinality ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
2bb3769ec540c5760aa521e8cefd1e7deee5d72f Apalache BagBagOfAll ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
af2dd815ef9c859883679a574376b8706f7bc7de Apalache BagBagOfAll ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
37a2f36ae494b96c25f6184cca454e65c12d69ad TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
ad60489f1a2097a15b633665d79950731f3a96a4 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
147e294cef7b7413c3665132b5073f9857355f61 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 ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
3cf7ff7e2015b3a87b3ef50a8781e00abfe213be 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 ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
afb9703ab9937044f16eb1089d5e0832230a75b8 Apalache FiniteSetsCardinality ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
2fdd0cfda9c5e9b60b2d581586fa5db9b629b64a Apalache FiniteSetsCardinality ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
ddce54f39124250621b1b6e6cebb35b47d0b8c5b Apalache SeqHead ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
26dd5f9817be25dbde29d358ef2c2fd48491217d Apalache SeqHead ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
cb9823860af88cd0027548e51f951bb902adee0a Apalache SeqTail ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
7fc6e199618306db5ff47a17f833e27cec5c11b8 Apalache SeqTail ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
2d2bfd294f2b45d8c47f071cc341dc124569489f Apalache SeqAppend ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
2c3197b8ad0ff146732aebbabe0f0a66ad938001 Apalache SeqAppend ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model