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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
fdff057f98886f9b29c9737397715f23ccedbbfe TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMod OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
e70c7a7f44f5326dbe5e7adb4b1673f1057117ff TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMod OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
18f257c63081ffacd9c810b017297034c9801748 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMod MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
40901899622faf284fe1196701f68dd60e8f0620 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMod MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
095b74a3d98759a6e523a55b4bb63bae6641cd39 Apalache NumMod Let True Passed
  • Model Under Test
  • Equivalent Model
4db00a8e7af1fc25c7bb7b77ccb47a722d63b1da Apalache NumMod Let False Passed
  • Model Under Test
  • Equivalent Model
06782b4273b6dab38be15b58feb8e935386cd163 Apalache NumMod Choose True Passed
  • Model Under Test
  • Equivalent Model
548909587b11aba52ce5707f5aa5f40a4af75c78 Apalache NumMod Choose False Passed
  • Model Under Test
  • Equivalent Model
4601ab57aacd7c6614a8dccb2f5f2c6ce3a5aabe Apalache NumMod FunApp True Passed
  • Model Under Test
  • Equivalent Model
bc345174118b6d8f5226ccd7e1458d546e8595dc Apalache NumMod FunApp False Passed
  • Model Under Test
  • Equivalent Model
e1dd69e7cf0b5aa59f636689484a74abc3c5a34e Apalache NumMod Prime True Passed
  • Model Under Test
  • Equivalent Model
77de0618573cf4eb83198fd6f0fe7e3b9a9bedca Apalache NumMod Prime False Passed
  • Model Under Test
  • Equivalent Model
212bd0286394d4cc94895933c5393b22a97a3fc1 Apalache NumMod NumZero True Passed
  • Model Under Test
  • Equivalent Model
8c995354e7f319fd187a0f559af169764f89eb32 Apalache NumMod NumZero False Passed
  • Model Under Test
  • Equivalent Model
b571d82d615067a3787de7c7aa71512b5b5ffc75 Apalache NumMod NumOne True Passed
  • Model Under Test
  • Equivalent Model
a5a36a564184449225b7ad811e500086fd8aeaca Apalache NumMod NumOne False Passed
  • Model Under Test
  • Equivalent Model
3fcb6b44cbd8a5f28806cdc3a24d83d0754323a5 Apalache NumMod NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
0b89c400ef8f0712e374d547a782a17e5ee6c73d Apalache NumMod NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
7f36d4b5bb574248bc684748862e21dedc89f045 Apalache NumMod NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
658c0636ab0740f543db24c40814c21b640968db Apalache NumMod NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
fcae8c653bace3ef21d9f5946d891f7aaa653631 Apalache NumMod NumPlus True Passed
  • Model Under Test
  • Equivalent Model
faf8ffac617060f6c703ed22effe42bbe0c7db7e Apalache NumMod NumPlus False Passed
  • Model Under Test
  • Equivalent Model
bb81417638c3742d7d624b045e734ead2d8fdf66 Apalache NumMod NumMinus True Passed
  • Model Under Test
  • Equivalent Model
41212285b57240391d51f09c3a9e38c6971e7a0d Apalache NumMod NumMinus False Passed
  • Model Under Test
  • Equivalent Model
b6819b1e2dbf1646ff60152ab5b607930ee13a2f Apalache NumMod NumMul True Passed
  • Model Under Test
  • Equivalent Model
fcdfe168d6e331250cd9e61ede496b6e0ae18fb4 Apalache NumMod NumMul False Passed
  • Model Under Test
  • Equivalent Model
45202268e1d344109964cf2b4e2a8bcea1c39f6c Apalache NumMod NumDiv True Passed
  • Model Under Test
  • Equivalent Model
9bdf1a0a7b7f4ee46e1247ac8606ba3b9e71996d Apalache NumMod NumDiv False Passed
  • Model Under Test
  • Equivalent Model
30e8f9164c05577cf38e667043d894fada5d762f Apalache NumMod NumMod True Passed
  • Model Under Test
  • Equivalent Model
d7b7ff84e2ecdaecefb6d39384b3ca99f2989f2a Apalache NumMod NumMod False Passed
  • Model Under Test
  • Equivalent Model
3b037f79464f2eba794061e8dd21a75e778054b4 Apalache NumMod NumPow True Passed
  • Model Under Test
  • Equivalent Model
c7a9faf894c32f74473f21c92512c278bcb2c26a Apalache NumMod NumPow False Passed
  • Model Under Test
  • Equivalent Model
aa035c2c663fdc4716b334eaf3484010ef6f2942 Apalache NumMod Def0 True Passed
  • Model Under Test
  • Equivalent Model
3f03d512c46c728a76d0111901cdf6af8f46bc1a Apalache NumMod Def0 False Passed
  • Model Under Test
  • Equivalent Model
b2b8e2a3faa35c730e0d9af2e7a4579640202215 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
8b2535a4ba27f4c42badfb7d329695bfd3208f1a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
46b0749080c1151f5b0831f61b15fb3e62a43487 Apalache NumMod Def1 True Passed
  • Model Under Test
  • Equivalent Model
0971b961300483f3935a76043ffc561e604a31cc Apalache NumMod Def1 False Passed
  • Model Under Test
  • Equivalent Model
b34603ec4ef441addb25414363e2c53aed3fcc89 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
3e657d662b79655ac5f154edf63e72c7ec0d1517 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
677d5821fcfad107bf60150ff505c2b9b686bdda Apalache NumMod Def2 True Passed
  • Model Under Test
  • Equivalent Model
936c288407d898217a48823d193d5dcdd582efde Apalache NumMod Def2 False Passed
  • Model Under Test
  • Equivalent Model
644f6262f60684303ebfe552c274c5572430677a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
954b060df240851bc3270f1614d544edd5798ac7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
6bd319eb196b034efce9ded67086dfb5e3472c1e Apalache NumMod Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
f7445d00c5df2721813cdf3b93f2ee26c69ae581 Apalache NumMod Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
280363734fa9f0f64638ce13578513c1d22390db TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
6e06407f6e4771288034d66ac4b7f3ba6951b7a5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMod LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
d5fac2c1c67d3b5a839b62e5082021e09485a039 Apalache NumMod Extends True Passed
  • Model Under Test
  • Equivalent Model
8cd7c2d2fa220cb4fa032ef4da25d26e9dd8e5b3 Apalache NumMod Extends False Passed
  • Model Under Test
  • Equivalent Model
8f43db7b973dec0a1b390256de919509fe6c1a52 Apalache NumMod ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
3d1078419bb1ce0e193b80f4ae6eece020fd4d35 Apalache NumMod ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
ccf9da2df47faafe3f79884e934e6850fc27cdcb Apalache NumMod Variable True Passed
  • Model Under Test
  • Equivalent Model
01cd55a0af5f2378fdec8969197080f5a6c2d1db Apalache NumMod Variable False Passed
  • Model Under Test
  • Equivalent Model
76f6c9e4a43cb3a4ebb37874108ad30246dcbdc1 Apalache NumMod Constant True Passed
  • Model Under Test
  • Equivalent Model
5842adadf1d72d205167bd32815ac0172c87050e Apalache NumMod Constant 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
c95c750f6274d48645ae68b8552cc42a84eddffb Apalache NumMod Instance True Passed
  • Model Under Test
  • Equivalent Model
d885139a2b09298c9ff872c5e021ef0916beeeaa Apalache NumMod Instance False Passed
  • Model Under Test
  • Equivalent Model
cc376664f18098fdd552a0b5e2eb68eb1e30e950 Apalache NumMod InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
cccc0d2d0b8a26699eb9a7c584343ea7f77f2adf Apalache NumMod InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
3df6f6c646d20fd2b50a4238740966ecb1e1b907 Apalache NumMod InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
823f3438f35f51191fb0101fc9aa62ca67ffc3c3 Apalache NumMod InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
9b6d157a6d0d95d34eb94436c42bcd6cf64a9c24 Apalache NumMod InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
63f61d12530d37ef20572918861a88d599a59a78 Apalache NumMod InstanceNamedWith 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
c574b03d2a219b92d5002cc21b32f3b697a37ca7 Apalache NumMod InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
754afe765d4303163b6b77c9ee14d90e63ac6b2c Apalache NumMod InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b41a4388687a8f080f9d58ebbea67d60e49a19da Apalache NumMod InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
a268dfcc39c073c75fe1edafc8206027a313c870 Apalache NumMod InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
bf56cb660dcebad7a31f3fe97f6432cf67c42e92 Apalache NumMod InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
f0a82b702c7acee514958317a730b594bdf516d1 Apalache NumMod InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
d71f13529609e7f03ca2cdb83040cf0c82995913 Apalache NumMod IfCond True Passed
  • Model Under Test
  • Equivalent Model
bae8613fb70c009489dfbbe2b86f88df57c4234b Apalache NumMod IfCond False Passed
  • Model Under Test
  • Equivalent Model
69bb7ca96ef28bbc2067c4ef96ddbc7a79f63d18 Apalache NumMod IfThen True Passed
  • Model Under Test
  • Equivalent Model
d5ce54211da0baae983aa00f3401cb85e3f8b3f6 Apalache NumMod IfThen False Passed
  • Model Under Test
  • Equivalent Model
c6ed065ff0ee3c2aed5b5c7f30fedcafa16ee0a6 Apalache NumMod IfElse True Passed
  • Model Under Test
  • Equivalent Model
2e3665f83ead3dc038c0eec99bf9e2cb1eb461f8 Apalache NumMod IfElse False Passed
  • Model Under Test
  • Equivalent Model
186fb7d31d49712becba5beb76f0d2f37033a684 Apalache NumMod SeqLen True Passed
  • Model Under Test
  • Equivalent Model
af1a3c859717490b13c087529479fb478a13eb63 Apalache NumMod SeqLen False Passed
  • Model Under Test
  • Equivalent Model
1295f8e107247425ebfe0ca36d72f371485c53cd TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMod TlcEval True Passed
  • Model Under Test
  • Equivalent Model
7e705d1cb29c95feefa2d46a06cb637b4621db6d TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMod TlcEval False Passed
  • Model Under Test
  • Equivalent Model
3ba3eeabab839c2523a95a2952107d49e439816b Apalache NumMod BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
5ac176185505d32570e1eab0b716239304dc2eee Apalache NumMod BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
e3e90c6a94f754bfc493774e22bdaaab067e9637 Apalache NumMod BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
7d24f8b4285cd5ef016c484abc35029fe8c40932 Apalache NumMod BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
d1be0522025eb62871332344d9d31719b43c75eb Apalache NumMod FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
490d0017b0cced86754aacdb10e6582cdda0f910 Apalache NumMod FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
9faed85e8f83c6bcf2f4c41c11a17d38e23cac0d Apalache NumMod SeqHead True Passed
  • Model Under Test
  • Equivalent Model
85c759c2606906e9c2b5f7407afa8313b0610d18 Apalache NumMod SeqHead False Passed
  • Model Under Test
  • Equivalent Model