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 case feature Let; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c83339c65fad9b504e0b7f456154a0ea5b0078b2 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
8ec2827f396bb39605d184fdf389035147bca8cc TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
ad802033f2fb567d0f9d75e5d071c21da95a4846 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
f0c8ac077dcdd067b41b03a12c9d7d487ed6f399 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Let MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
06cb41f6d429e5df49e3648fa0c09fcd9dd41244 Apalache Let BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
afb5a158cc0289c80fb1a9285d646ce5c9483562 Apalache Let BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
3870929418abe4114f36583a9a4d04798480ce4f Apalache Let BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
db34a439da0a07814aeb80e65ca4fdb76d980551 Apalache Let BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
0f3f1c02e21c33dfb676a9059e4dbd0073a1cb65 Apalache Let BoolSet True Passed
  • Model Under Test
  • Equivalent Model
0639a174117014c70222431a97ed3122a43363af Apalache Let BoolSet False Passed
  • Model Under Test
  • Equivalent Model
4590c0d29ca74d0f554a4612ae59ec9b70b8ac90 Apalache Let And True Passed
  • Model Under Test
  • Equivalent Model
3452634f7ed56b53b96306eeb7f5b4d876187680 Apalache Let And False Passed
  • Model Under Test
  • Equivalent Model
040790120d4c3ab24af47ab00381776b60b8a6b4 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Let AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
ccea67a010bc7fb12ded5345dbb137aece52527a TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Let AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
173a5569eb4eff7c700953b6242e427b296691f4 Apalache Let Imply True Passed
  • Model Under Test
  • Equivalent Model
4f76102ea96a539955227bbff77d4efd52596efa Apalache Let Imply False Passed
  • Model Under Test
  • Equivalent Model
c85781eb0f6d5a54314ee18d24c81854477a4c70 Apalache Let Not True Passed
  • Model Under Test
  • Equivalent Model
bf21403654892c5050acbeedd8bc42af1f006d37 Apalache Let Not False Passed
  • Model Under Test
  • Equivalent Model
ee67b6597be8da458c6fb184d86fd9657e022b98 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Let Or True Passed
  • Model Under Test
  • Equivalent Model
474a3294934c58238f30940655e379e5a8fb9345 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Let Or False Passed
  • Model Under Test
  • Equivalent Model
03190783de6897d460f05fb0ffbe5befd203cf2c TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Let OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
cf216d66495ab7f1191f405ef79e6c972821cecf TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Let OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2ed391362fa8262b533c40a83e4958c16ff8d7ee Apalache Let Eq True Passed
  • Model Under Test
  • Equivalent Model
af8417db8fb598f2645f064a5e891adf4bfeadce Apalache Let Eq False Passed
  • Model Under Test
  • Equivalent Model
914b71041b9c93dac4afed8c5a0baf0e90c07f1a Apalache Let Ne True Passed
  • Model Under Test
  • Equivalent Model
5c63c3c6dc4d45de7c2d164b600e9273c50a7fa5 Apalache Let Ne False Passed
  • Model Under Test
  • Equivalent Model
fd5bba37f7dcb973d109eba71e90d9b374214ac7 Apalache Let Let True Passed
  • Model Under Test
  • Equivalent Model
3824cad01a99a912935462b68af6984838e52835 Apalache Let Let False Passed
  • Model Under Test
  • Equivalent Model
67130891bccc937c05d79e9b669aa0369a3b5ada Apalache Let SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
634a4485f6e784c5e5e1453fb3b0f08e150f3e83 Apalache Let SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
36e11df36d388fa59151f8a030f1007a58342517 Apalache Let Set0 True Passed
  • Model Under Test
  • Equivalent Model
8323236f5fb44f69c7a667c9203d492dcfe665ce Apalache Let Set0 False Passed
  • Model Under Test
  • Equivalent Model
fbc15e4dd73d8ef1f136a9af5b4ff222d9be9922 Apalache Let Set1 True Passed
  • Model Under Test
  • Equivalent Model
04931032ba178e883eddfa429b5b251e0388948f Apalache Let Set1 False Passed
  • Model Under Test
  • Equivalent Model
bb60025931e9e5e07634bd3983d02ef77dc1dea0 Apalache Let Set2 True Passed
  • Model Under Test
  • Equivalent Model
016b357f030cc6dd41907c8023313e0318c50955 Apalache Let Set2 False Passed
  • Model Under Test
  • Equivalent Model
2e7fed07380564b1444046b8b28430de4b73ea80 Apalache Let Fun True Passed
  • Model Under Test
  • Equivalent Model
907f7569697850a7b34ec996ec71e6243866f5ad Apalache Let Fun False Passed
  • Model Under Test
  • Equivalent Model
7b381ca36d140705ea9dc070980d745f1ba39463 Apalache Let In True Passed
  • Model Under Test
  • Equivalent Model
f0741947d3e4de05021b66e226547ca656a15efd Apalache Let In False Passed
  • Model Under Test
  • Equivalent Model
98e3356685f785c882aaa53fa4ad3246c0bee7f1 Apalache Let NotIn True Passed
  • Model Under Test
  • Equivalent Model
f50a5badbefd638945edc5b71b0739c7175ac673 Apalache Let NotIn False Passed
  • Model Under Test
  • Equivalent Model
a5da83a5ff27fdf544d45e52184f5273d41f7931 Apalache Let Exists True Passed
  • Model Under Test
  • Equivalent Model
aea5feec63a83011e2b7d60efd981fe0f0876f1d Apalache Let Exists False Passed
  • Model Under Test
  • Equivalent Model
7cead322b6dfec7148998104d4cbea07e716b2e6 Apalache Let Forall True Passed
  • Model Under Test
  • Equivalent Model
d7dd33e61eed14cbc1fa39470263a3d3d5973568 Apalache Let Forall False Passed
  • Model Under Test
  • Equivalent Model
a798420ab75707e589d4a511f3335b8be062a03c Apalache Let Choose True Passed
  • Model Under Test
  • Equivalent Model
dbbd6d9fb610ac8656945bd56dece9cff949c89f Apalache Let Choose False Passed
  • Model Under Test
  • Equivalent Model
9dfac4bcbe9c3449d35c9b168980126fce1e6d1c Apalache Let Record True Passed
  • Model Under Test
  • Equivalent Model
96a9b20fbe058325144acdefab4da3796cb4456a Apalache Let Record False Passed
  • Model Under Test
  • Equivalent Model
758743c466e14370651525121b0366067792d9ca Apalache Let Tuple True Passed
  • Model Under Test
  • Equivalent Model
eb471cc3abf2996e582249bfecce1206fc780ed0 Apalache Let Tuple False Passed
  • Model Under Test
  • Equivalent Model
74340ccc150151054ac448024f270aac209e1866 Apalache Let TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
065cfac74aea21d7813618399a487289721f761f Apalache Let TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
d75d4f484312da2e4d3d65d88c2af3cba1b323a7 Apalache Let FunApp True Passed
  • Model Under Test
  • Equivalent Model
f7a56637239b89afe0a7b7b28a294aca64f620ac Apalache Let FunApp False Passed
  • Model Under Test
  • Equivalent Model
fecb1c8c5bbfcf5e455f8bd2941bf294787427bd Apalache Let Prime True Passed
  • Model Under Test
  • Equivalent Model
f4d648a5920cd0e3cec194dced5ccb1bba3d9e85 Apalache Let Prime False Passed
  • Model Under Test
  • Equivalent Model
2b037cb7c85641e3b76ab1c57fccaf1bbbe5d83c Apalache Let NumZero True Passed
  • Model Under Test
  • Equivalent Model
76734c5c8a2b05ea60b3b6bdce59d8b2051f3809 Apalache Let NumZero False Passed
  • Model Under Test
  • Equivalent Model
c8df92b0f82ebd59a675b6460bc21e3d8e1427c6 Apalache Let NumOne True Passed
  • Model Under Test
  • Equivalent Model
4c263f9841f2913152e82e709cb55cffce6f6e40 Apalache Let NumOne False Passed
  • Model Under Test
  • Equivalent Model
51e3eba388510a7fc13e867910f78c42f69eeb87 Apalache Let NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
f1c9ac5d012045620d2a74e43309da1177773303 Apalache Let NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
383b13ec460045744dd5e9262cd7a36cf407c334 Apalache Let NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
42466a59d054323253cf4cfb1740c9372224837e Apalache Let NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
cd9d58b53fdf6eadbb842e865a69def8890396f9 Apalache Let NumPlus True Passed
  • Model Under Test
  • Equivalent Model
3d9cfbce17f322b8ba1f3c2c1628949b9352375a Apalache Let NumPlus False Passed
  • Model Under Test
  • Equivalent Model
0f48895547aaddf330d1f0f2e8ad57880f9dd6a9 Apalache Let NumMinus True Passed
  • Model Under Test
  • Equivalent Model
016ffa323fdb78bce685fc198637e57189e01ac8 Apalache Let NumMinus False Passed
  • Model Under Test
  • Equivalent Model
c1af3efdbc8f3f8b13abff52e9c41fd781840650 Apalache Let NumMul True Passed
  • Model Under Test
  • Equivalent Model
f3f132305293e0d6b5d37ef4aab927e2fe520929 Apalache Let NumMul False Passed
  • Model Under Test
  • Equivalent Model
c56f9709af7d639b852c45c766f572433a6b1e81 Apalache Let NumDiv True Passed
  • Model Under Test
  • Equivalent Model
d6666a37b541a3be27bbe34878551c099a73fc7d Apalache Let NumDiv False Passed
  • Model Under Test
  • Equivalent Model
2abdb626b5324ea278c80541f0da7d6d3b799fc1 Apalache Let NumMod True Passed
  • Model Under Test
  • Equivalent Model
c3b59277785b3b7ec46f2b77f23088904326c04e Apalache Let NumMod False Passed
  • Model Under Test
  • Equivalent Model
95b17ff0cc7ea84c652874023ffe4227befcc77b Apalache Let NumPow True Passed
  • Model Under Test
  • Equivalent Model
42263614bd6e86ec1849dea3ec16802da67b7abc Apalache Let NumPow False Passed
  • Model Under Test
  • Equivalent Model
5d3257779203f72b31c9175ccf9ac6b53c48d636 Apalache Let NumGt True Passed
  • Model Under Test
  • Equivalent Model
348d674b1d51b558416b1a5e5e562c760be60eb0 Apalache Let NumGt 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
cc54e75bca07f9d7874c527e00ed7d307d6b4a10 Apalache Let NumLt True Passed
  • Model Under Test
  • Equivalent Model
4bdaa0e6e14f7fc1a06adaf4c81a286e89ab0fe5 Apalache Let NumLt False Passed
  • Model Under Test
  • Equivalent Model
28068509151cfb9839a60b4481adf17667159abb Apalache Let NumLe True Passed
  • Model Under Test
  • Equivalent Model
560173feb1b63c4fd9acccbcd24b1ee185750e21 Apalache Let NumLe False Passed
  • Model Under Test
  • Equivalent Model
36dfd9b662283c3f4f0d53020a6c0c0a37488922 Apalache Let DefFun True Passed
  • Model Under Test
  • Equivalent Model
dc7b623fc85abf1b81ff6dcc6f1a22968e5d0827 Apalache Let DefFun False Passed
  • Model Under Test
  • Equivalent Model
c7208accf7193fdfcd1e3afb9c05bde5e395dfea TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
23464eff7fad3bfeab1516c24515194cbee9dfae TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
bf6053f24ebf0c6227d7cf5b30943032deb0f86a Apalache Let DefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
f807f627d8c2b85b64609a65e06dc44190a1a42f Apalache Let DefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
0e389d39d61fa1f90b3b71103ac179c35e6922e3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
c952898242464708fd7e79e950920b960f77b549 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
68ec03057badb4c04781e87e8f3580962e508a17 Apalache Let Def0 True Passed
  • Model Under Test
  • Equivalent Model
5409acadd520c495f33ea074e8a19e8a10608ff1 Apalache Let Def0 False Passed
  • Model Under Test
  • Equivalent Model
e3d3210278e3cabf3378f074cf17e506539ab120 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
3043cd522b14362d6482121d66d5463d8b265a5a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
282ae46252aa369e97af588199f41d0a258a97d0 Apalache Let Def1 True Passed
  • Model Under Test
  • Equivalent Model
d68dba880710cf727935f65d9def6c095243e78f Apalache Let Def1 False Passed
  • Model Under Test
  • Equivalent Model
a1b4ea3f6997feffa65d5d11640a232f2e35cad3 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
d4ce37d06c93cf88545692e9c613c88eec6b39b1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
2bfa6d0efb91e4e2988c58991e90e7e94e25dce7 Apalache Let Def2 True Passed
  • Model Under Test
  • Equivalent Model
6642b7ef676e4fce8c79a71f721d97821c4f203f Apalache Let Def2 False Passed
  • Model Under Test
  • Equivalent Model
40c2798d052465adbf3889ca87c468613ae98d0f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
1d91b440081b49997783ff7fbbae4394d033e127 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
34ad5a557cc07357fcdeb21e388c1cdff45925b2 Apalache Let Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
941c0efef5183bd02182ad365ae658b9b2157168 Apalache Let Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
94c76226b33f151c592ccedee097e75a132f9ae7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cd3d2278b223f8f0af72eb151b6eb0e2c300fd8f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Let LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
d358fd1ad91071d1109faae3b95bf5e94441c78c Apalache Let Extends True Passed
  • Model Under Test
  • Equivalent Model
b2ec72c2170b904cc1cdd40f917bcffd88f6fe6f Apalache Let Extends False Passed
  • Model Under Test
  • Equivalent Model
eb1b51e99a3fc91dba9474edaf4d54c88ac90995 Apalache Let ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
7e34b889b060a50d868207eaefa9b93798d26ccb Apalache Let ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
2ae0e9e6726b4218c8083246b3f2943db9367fa6 Apalache Let Variable True Passed
  • Model Under Test
  • Equivalent Model
acf116d245f359e6f81913dc17cd215e526d907b Apalache Let Variable False Passed
  • Model Under Test
  • Equivalent Model
4c21cf0ea14ba06e45141b146e321e9b06b9e7d3 Apalache Let Constant True Passed
  • Model Under Test
  • Equivalent Model
bdcdcd7da54f2be6cc057c628371ba19b72a823d Apalache Let Constant False Passed
  • Model Under Test
  • Equivalent Model
45911ff45fdb44587ad3268228e37be1fc8760a7 Apalache Let ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
cf587dc75800a7de0fa6e0594898732df9a9af32 Apalache Let ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
dce00ecb69a24037e69982e1f954582a826a964a Apalache Let ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
17db1e59351f20a5c36433bd8f91edf3ebae3e85 Apalache Let ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
a78f33bfb1881e1b55f1647c98cb22a50cdba44b Apalache Let Instance True Passed
  • Model Under Test
  • Equivalent Model
3cc797661d38f6af98d846ea6ac65dd01b8516a4 Apalache Let Instance False Passed
  • Model Under Test
  • Equivalent Model
6b49036f1700aaf6e07fdd31b49eb3ad3eb84a9f Apalache Let InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
41aff8e558ef0bbd5f694e4564099d233ffaf2ea Apalache Let InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
905c8ec97dae649f5945a47a71a650f8f82d927f Apalache Let InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
d469016fbaf54f7e41491cc6abe78659ce67a74f Apalache Let InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
57bd81198ac39a0c5391c7266980b8c7566a4f5a Apalache Let InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
2e2df8211d8f37f7867d73d10019e06abec87c47 Apalache Let InstanceNamedWith 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
01fa4943cf5bb59279b536035a68ae1ed92466ce Apalache Let InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
2b4007bc0f6632bb0940d49914ed52670b08c087 Apalache Let InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
7da0785415a64b079154fcaa81dba41c72dd7dd6 Apalache Let InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
e0a8f20d84f463e058f2ba69e11d36f3d275759f Apalache Let InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
214f3996be096f0dda0ca0212849da496504af88 Apalache Let InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ae8a3cc2ceadd2d07567787649edba23bfdddfa3 Apalache Let InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
9b7eecbff91185fc4be51b620f933f7d71a7eff6 Apalache Let Enabled True Passed
  • Model Under Test
  • Equivalent Model
b355a2a324ef62377da62023dd4ca4367b9d8396 Apalache Let Enabled False Passed
  • Model Under Test
  • Equivalent Model
3cad38ed1cbd5ebbce148223c437de95dc2a8c7e Apalache Let Cross2 True Passed
  • Model Under Test
  • Equivalent Model
9540c274709eef93d2abceee3210486c3ad0440a Apalache Let Cross2 False Passed
  • Model Under Test
  • Equivalent Model
d5e451fa0edaeeada91799c31a11ad65c5b26e94 Apalache Let Cross3 True Passed
  • Model Under Test
  • Equivalent Model
6a0c4e2edc1002d392e68f84bab279e1569c7515 Apalache Let Cross3 False Passed
  • Model Under Test
  • Equivalent Model
7208bf20593c7a627e0f3aed3797d803e412dbda TLC with reduction strategy:
  • Plug 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))
Let FunSet True Passed
  • Model Under Test
  • Equivalent Model
2406b977891363b427ff170bdf0a4ceb8a256811 TLC with reduction strategy:
  • Plug 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))
Let FunSet False Passed
  • Model Under Test
  • Equivalent Model
322b21d2a3fb0e99c8fc3e4793c7a8a98cf75239 TLC with reduction strategy:
  • Plug 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)
Let RecordSet True Passed
  • Model Under Test
  • Equivalent Model
df5a0b923cb7a1bf20dd134df23c4859fd9dfffb TLC with reduction strategy:
  • Plug 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)
Let RecordSet False Passed
  • Model Under Test
  • Equivalent Model
587e9c2addfdda9a63def638d79020902156efc1 Apalache Let SetDiff True Passed
  • Model Under Test
  • Equivalent Model
87bb30445d6c5d8b90a22f65680598686c232cd8 Apalache Let SetDiff False Passed
  • Model Under Test
  • Equivalent Model
7424f24f83e7b3dbfefd52892f59d0b775efa5a7 Apalache Let SetUnion True Passed
  • Model Under Test
  • Equivalent Model
27456c38179d0f4d767e9298a4a24c72370e9b5d Apalache Let SetUnion False Passed
  • Model Under Test
  • Equivalent Model
28d1c4162783c360e91f48f20aee7d0ce018307f Apalache Let SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
b4934d844e731b2f23a01fceb7f1368732ea83f6 Apalache Let SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
daa68428b7b23a665da6bb6342fb194b7a092ccc Apalache Let SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
8e46b29ec711e83a6edbf6dfa04ab71a3a4a3bc3 Apalache Let SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
21cc17eaaa6d50307ffb77a0c9baa380bd98f411 Apalache Let IfCond True Passed
  • Model Under Test
  • Equivalent Model
cc11b8cc68fbfd572a320b902332bb039e8459b9 Apalache Let IfCond False Passed
  • Model Under Test
  • Equivalent Model
6eb47e4baf39bdfcb8366217c9fef57e4de7a70c Apalache Let IfThen True Passed
  • Model Under Test
  • Equivalent Model
20c363dab8b8426d996609b98986b27c092276c3 Apalache Let IfThen False Passed
  • Model Under Test
  • Equivalent Model
1223b4ead3300de738379a33313a969072323bba Apalache Let IfElse True Passed
  • Model Under Test
  • Equivalent Model
e0fa5fbd5e6ad70b06ac3810cb290bf9aa5fc75b Apalache Let IfElse False Passed
  • Model Under Test
  • Equivalent Model
b183581e0692fbddc2cf0c7ac68fbdf8a60ba522 Apalache Let Subset True Passed
  • Model Under Test
  • Equivalent Model
6fdcd5cfa4abc859be5758bef01c8f0550b1a4ea Apalache Let Subset False Passed
  • Model Under Test
  • Equivalent Model
30158e1b34b749cb2984eea202c10e8a9d2a3285 Apalache Let Domain True Passed
  • Model Under Test
  • Equivalent Model
32aa710f43cbb68cf8c4d4b801a3cd871188a2ca Apalache Let Domain False Passed
  • Model Under Test
  • Equivalent Model
353ca0090b880ef9d289598d8726980ab9f3b777 Apalache Let Union True Passed
  • Model Under Test
  • Equivalent Model
3e92ee09979dbd9469cb7722bd8739a8810fa501 Apalache Let Union 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
77f3ad6c299d6b891a724a1c95613da866fd27cd Apalache Let Equivalence True Passed
  • Model Under Test
  • Equivalent Model
788e27c552c3c3fd03623686a08e83ca8a839e1c Apalache Let Equivalence False Passed
  • Model Under Test
  • Equivalent Model
02c0a9ccdf77f987fcd2f90c3c6306b83da3b6b6 Apalache Let StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
af65d341f4d3a4f94fe61d1ce81b8ab867c7998e Apalache Let StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
5e8dc2fd86c1d44311ca97b42c247f01ba06edbc Apalache Let String True Passed
  • Model Under Test
  • Equivalent Model
01ea371bc4395544a124e7513048dd1a8a8c97ef Apalache Let String False Passed
  • Model Under Test
  • Equivalent Model
0427a1d7a77a11d2151c606a1e626ef0f6ab0fd8 Apalache Let SeqLen True Passed
  • Model Under Test
  • Equivalent Model
a95541ec83ae43e3e8fae8cfe24aa1a0eb1433d2 Apalache Let SeqLen False Passed
  • Model Under Test
  • Equivalent Model
cd500fbde7d4221191e0399329a28fb2cbc5331f Apalache Let SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
4c37adaef03b332589bac03d5b12d6d06c355958 Apalache Let SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
b25a4c8bb58e4e677155665542395ffbc924abfd Apalache Let SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
4d59222795212edde98c3b0c160b744dbaba3efa Apalache Let SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
0ac54ff005396a6396945f0b8f1e561bb3ebc84f Apalache Let SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
b9dd7c05be6c428d7a638c480a66eddd6f139848 Apalache Let SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
6b4d386b2ed21550ef74261fb5d57ef626512bfc TLC with reduction strategy:
  • Plug 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
Let NumRange True Passed
  • Model Under Test
  • Equivalent Model
efd1c9d27cc8e8e36cce7770cbceaf3e4044080c TLC with reduction strategy:
  • Plug 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
Let NumRange False Passed
  • Model Under Test
  • Equivalent Model
a6b577531c74e95e0018c5c50d74d8603ceceac4 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Let TlcSingletonFun True Passed
  • Model Under Test
  • Equivalent Model
af7d1d44027366bd44b76d8a81cfc8b5df20a7ec TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Let TlcSingletonFun False Passed
  • Model Under Test
  • Equivalent Model
da72186db927fdcac2ccd1db22592239d8ed6f7a TLC with reduction strategy:
  • Plug 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]]
Let TlcExtendFun True Passed
  • Model Under Test
  • Equivalent Model
c6eb0f281de72c4e99ca4ff5aa668ee542f9166b TLC with reduction strategy:
  • Plug 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]]
Let TlcExtendFun False Passed
  • Model Under Test
  • Equivalent Model
ba87d89e64399593674afb676df3bae293ac6aaf TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Let TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
c5576fbad91e5c43ee63a63144dc1adae6002026 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Let TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
761a7c68b590aa08311dd3f1e069844c4295676f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Let TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
57670d48df740c3ddf7ecf895bcb96db3307e970 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Let TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
a8fd05265f1752a6b1be235dacbf1c854428fae8 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Let TlcEval True Passed
  • Model Under Test
  • Equivalent Model
f69af7561d7b8ffccc368d43740eba1f159ab37a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Let TlcEval False Passed
  • Model Under Test
  • Equivalent Model
fd05cb04bea487348e130f4b4163afb36e6eefb6 Apalache Let BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
f38735307a11f553857b97e7d18083111e06abe5 Apalache Let BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
39ba3934ec648b51e02f75ba61d5e63b4300ca2e Apalache Let BagSetToBag True Passed
  • Model Under Test
  • Equivalent Model
86cb16b16571c8a5af575272a6e1808d58e039a1 Apalache Let BagSetToBag False Passed
  • Model Under Test
  • Equivalent Model
d492346b4558f2c0d0875e50e4ed13b7bd8e40a9 Apalache Let BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
b4147996b5263ed9c22f79372135999f3df647a5 Apalache Let BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
86ea72a9c9a07f9b21462476e880a6522d6f7d3a Apalache Let BagEmptyBag True Passed
  • Model Under Test
  • Equivalent Model
4b4c1a90f6ef1f9e887958fe30bde84dc18351c6 Apalache Let BagEmptyBag False Passed
  • Model Under Test
  • Equivalent Model
f0f402d524c72d2a7358609147c1786c12a28e94 Apalache Let BagAddBag True Passed
  • Model Under Test
  • Equivalent Model
0bae3fa75bece1818bbf711094d21015064b9c18 Apalache Let BagAddBag False Passed
  • Model Under Test
  • Equivalent Model
25caf1c7ed489bb3b6fa60fd370e47f5f9bb6bd4 Apalache Let BagBagSub True Passed
  • Model Under Test
  • Equivalent Model
82f6d680ce095cb724bc905ebf31d315e0cb3e8c Apalache Let BagBagSub False Passed
  • Model Under Test
  • Equivalent Model
c3830ff7be1cb535755aa840c37a65d5472ecc13 Apalache Let BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
2ee1fefefb74a4ec3d14ac1e498344d2a9642626 Apalache Let BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
d6512937b39d463ac4f2ed52ef626d0f873cdfa6 Apalache Let BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
8fd900bda06b5b937a1f3bde13998d69ad802e04 Apalache Let BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
24c0d556ba634efa0faaa6a1404abbfc49182980 Apalache Let BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
23aea2b29a99e01f895397c296c135efeb1f65a4 Apalache Let BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
1e39c54b38f1c210bc3101339d64b314c5d18f49 Apalache Let BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
51d70c1739dd3421d454d9114f48fe62c8cd2a97 Apalache Let BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
e2c5a6b07d0944e3bfd39caf281556ecae6e4bd1 Apalache Let BagBagOfAll True Passed
  • Model Under Test
  • Equivalent Model
25389eee8747c2dc13ba81df46b8b8a7bde2e6ed Apalache Let BagBagOfAll False Passed
  • Model Under Test
  • Equivalent Model
2e5845ce70d7d1bf7363bb199d7c1f0483982037 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Let BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
08324b9e1cd370be6158462910355b9144c23735 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Let BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7c3d45eab1e94c2d036c16db930595e85d70511b TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Let FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
30fdfb178b0379347bcde61197b9a857973f452b TLC with reduction strategy:
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
Let FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
ec48d973c687946a1edb38041ceb21cdcc1c19ec Apalache Let FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
a47c972f65faa012fe3e8e1f782347af3313af13 Apalache Let FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
b2b471d147a98c7c6c4192bad1e0dff94a250d25 Apalache Let SeqHead True Passed
  • Model Under Test
  • Equivalent Model
b7473182780da65ad1067325217ec909e3892cf5 Apalache Let SeqHead False Passed
  • Model Under Test
  • Equivalent Model
d8c2c95ba67036fdeb382f3cf292fb2d1dcd535a Apalache Let SeqTail True Passed
  • Model Under Test
  • Equivalent Model
999175260707bd9d1a518606385e1098e3100c31 Apalache Let SeqTail False Passed
  • Model Under Test
  • Equivalent Model
f94782943e93881e37e996b0b2ba77c90abc2068 Apalache Let SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
73c3462e1a3d848552b95b0ef26a625e2e3a880e Apalache Let SeqAppend False Passed
  • Model Under Test
  • Equivalent Model