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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
782ee242fb43f28ad9d56c313949649532c5d04f TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumPow OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
62263cbf826831ca8235096db95aa9c1a7f83db1 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumPow OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
740366d9c92bea3b3f3ef72f635d5651106802e2 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumPow MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
c39c4cf1539439b9dc4dfa1b395ac0766e014676 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumPow MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
69b49d4d371f9bf9634c4f4a1423973066c2c13b Apalache NumPow Let True Passed
  • Model Under Test
  • Equivalent Model
50ead2819b482124b1dabfbe42b4dc1b62cc42aa Apalache NumPow Let False Passed
  • Model Under Test
  • Equivalent Model
6e7878cdc990f7bb7bfb39f678a66d8fce1bfd2f Apalache NumPow Choose True Passed
  • Model Under Test
  • Equivalent Model
69452cd98357ee5a056069d18a14866b1258c1fb Apalache NumPow Choose False Passed
  • Model Under Test
  • Equivalent Model
4a8c62c338abb2fd4634ba8404d0330aad37df7b Apalache NumPow FunApp True Passed
  • Model Under Test
  • Equivalent Model
ff80e41e5e05f9bb9056ed6bef0c21051859db0c Apalache NumPow FunApp False Passed
  • Model Under Test
  • Equivalent Model
c5cb3999eb2f612f0f1c3024b1aa7dcb35277956 Apalache NumPow Prime True Passed
  • Model Under Test
  • Equivalent Model
d7cadd6e078375690e39500d5c2884a2dba6c84c Apalache NumPow Prime False Passed
  • Model Under Test
  • Equivalent Model
bb537fb4e59fad75791e4157ba3853200272d43f Apalache NumPow NumZero True Passed
  • Model Under Test
  • Equivalent Model
67e7b5a1d5eab95b17ae77678234f273ac66d382 Apalache NumPow NumZero False Passed
  • Model Under Test
  • Equivalent Model
00f1fad4713227b7050bf879ac0eae2f6a39fde8 Apalache NumPow NumOne True Passed
  • Model Under Test
  • Equivalent Model
cbe9260bcdabff05d608f4c630d3bf21fd5c430f Apalache NumPow NumOne False Passed
  • Model Under Test
  • Equivalent Model
43aff303ad3271d7c79c418775cbe1b2f2bfe549 Apalache NumPow NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
81480fb85d718e5ccab76dd99e73315fe9ff5f1b Apalache NumPow NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
0f410c3bcfad73a47419a54d9c33057055f574a3 Apalache NumPow NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
e557682e965b881ab3cb165f9738e933ceb2f3e0 Apalache NumPow NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
3d058bd90baf69a446c8af0937eab57fcaaf7fe4 Apalache NumPow NumPlus True Passed
  • Model Under Test
  • Equivalent Model
485b763c11a66d67dc5b9a67b7425b789586fe44 Apalache NumPow NumPlus False Passed
  • Model Under Test
  • Equivalent Model
e2a4a78b19c4b1b8c829854eb63e4cf6284952bc Apalache NumPow NumMinus True Passed
  • Model Under Test
  • Equivalent Model
cd5b2e23b40c26f57d27823a50a634fead20f560 Apalache NumPow NumMinus False Passed
  • Model Under Test
  • Equivalent Model
a65065f7289a45b44942a0b6a532d3c0c02b84cf Apalache NumPow NumMul True Passed
  • Model Under Test
  • Equivalent Model
95fcccd9819415e049253cdab3389610acfa890c Apalache NumPow NumMul False Passed
  • Model Under Test
  • Equivalent Model
76776d99e7cffd4127b629889a1b199baf00f6c2 Apalache NumPow NumDiv True Passed
  • Model Under Test
  • Equivalent Model
fbcf5765bfe436d9b805a20c9ed3d1c32c6195ed Apalache NumPow NumDiv False Passed
  • Model Under Test
  • Equivalent Model
d6ea8ad92179dc99310e0a882a1b98a0e7a7318a Apalache NumPow NumMod True Passed
  • Model Under Test
  • Equivalent Model
3e8d4f7a83addf47614666197d0d0a42fed7072d Apalache NumPow NumMod False Passed
  • Model Under Test
  • Equivalent Model
16aa70f891d99d99af2b1d77fd8b39f19c3328e0 Apalache NumPow NumPow True Passed
  • Model Under Test
  • Equivalent Model
fae51e1aefc9db7549f925fd8ab70cc5eb4d8377 Apalache NumPow NumPow False Passed
  • Model Under Test
  • Equivalent Model
075060063646a75813cfb1bd023ab866b5e97a86 Apalache NumPow Def0 True Passed
  • Model Under Test
  • Equivalent Model
f0067d186f1041f4100a4f578ee0d9840ae4968a Apalache NumPow Def0 False Passed
  • Model Under Test
  • Equivalent Model
5cb322f34b5ef0119d5056a8693277e479388879 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
59f24b5eee2cbad24bc040b60e54032c2326aa03 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
49e70b0766b50ed63b89b195e445381f28b669da Apalache NumPow Def1 True Passed
  • Model Under Test
  • Equivalent Model
578e7b329528106c6c472d7bf3bb785039bda2de Apalache NumPow Def1 False Passed
  • Model Under Test
  • Equivalent Model
fc555082c8d881edab4dc3105792df16c4dc2ed2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
6f2290d0a446dc700e43fd9e6193c907d4832c2c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
d2e9d251deaa8de45237ebaf54ff54eae05d3d86 Apalache NumPow Def2 True Passed
  • Model Under Test
  • Equivalent Model
e3bd57ca9292cccc9f643f92a949cca7100001d7 Apalache NumPow Def2 False Passed
  • Model Under Test
  • Equivalent Model
0b98ae80ff61c7a9a9aba4193687b661c1c4c07c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
97cf06ae42d1ac9f924a786278a900e716688877 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
a077a8779c4d40cafbf437d2cd724d2e96a68ab2 Apalache NumPow Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
0b584e552b94e451533350a9b80a5060214b6d9d Apalache NumPow Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
51df4359b6d85cbf5d03b0a71421fa2aac025243 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
c611bf00e06136e738834c6b991c7497adec3b4c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumPow LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
f938e2df4c2e08336793c757fc1e21ac18d6c5d3 Apalache NumPow Extends True Passed
  • Model Under Test
  • Equivalent Model
e71f9214b11a79b676f4025e80c61ec4752d977b Apalache NumPow Extends False Passed
  • Model Under Test
  • Equivalent Model
fc9889b81d7370417725bf2028ce264383c0d273 Apalache NumPow ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
970b9a637f799f5923e4fecba3534dbb2466dacd Apalache NumPow ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
cb72a1c4e8d05fd97ba24288b7ce803cafa746fb Apalache NumPow Variable True Passed
  • Model Under Test
  • Equivalent Model
99885f08aec35a1271ab24e759e52cf0e54e0202 Apalache NumPow Variable False Passed
  • Model Under Test
  • Equivalent Model
487fe31b651aad3581eb021cf699002dbb886721 Apalache NumPow Constant True Passed
  • Model Under Test
  • Equivalent Model
b76e1c17dc6648c1a02e17c324ad5d39da1d4595 Apalache NumPow Constant 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
51ac529914a793a06575c8da4b025f0e6b515339 Apalache NumPow Instance True Passed
  • Model Under Test
  • Equivalent Model
a9cc1b367a4278eb9f8d7e0f182ccc5edfde17b9 Apalache NumPow Instance False Passed
  • Model Under Test
  • Equivalent Model
ad964669add18d44f5d85573c6b1ba9c58658f2c Apalache NumPow InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
a949455af673f2991aac23a9be31a7efc41dfc61 Apalache NumPow InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
dd8eab80f3a8f5c2c97ffd4b938417a2502e68e3 Apalache NumPow InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
161d28011fba98bb7192537d8aa8aa96701cfab5 Apalache NumPow InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
22019640ff8010c5a0ad8702d01bf7bcbbec4d9e Apalache NumPow InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
2cb210cdf18727abbd127a74db1b16e4ef1f6684 Apalache NumPow InstanceNamedWith 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
9419cf663657d65dd1fc45085d392bd8ae468796 Apalache NumPow InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
337fe26e5ec30e48bd902d7d7cb96565e30ba763 Apalache NumPow InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
00f85b42447c448e1c11c06c9cd331fe9fcb0f99 Apalache NumPow InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
82f6ef5009009ffb8216c74d9a89b838859fc0d9 Apalache NumPow InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
b275651657430582c7a8f7d51a117778606d17ba Apalache NumPow InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
ccbcff1b29f22b174e62c7a2d4cbc57a42151970 Apalache NumPow InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
eb7796812c02f684d9cd9512ff68f08320109323 Apalache NumPow IfCond True Passed
  • Model Under Test
  • Equivalent Model
7287678f29467b1734d36084ea60867d262e7b83 Apalache NumPow IfCond False Passed
  • Model Under Test
  • Equivalent Model
5d32367afaba4123e2efbf01f5a2e1494c9d814b Apalache NumPow IfThen True Passed
  • Model Under Test
  • Equivalent Model
6e7b63a04a8f618fec920b98bfcff14f42cb9b2d Apalache NumPow IfThen False Passed
  • Model Under Test
  • Equivalent Model
b478556e98f0e4cfaf16d538d38f4385990738f3 Apalache NumPow IfElse True Passed
  • Model Under Test
  • Equivalent Model
ca576e8a351f7e75437a1e87a27634b0ba87b1ca Apalache NumPow IfElse False Passed
  • Model Under Test
  • Equivalent Model
84b52cbf599aa55d5977f1fd2ebbfbd9b3a4adcb Apalache NumPow SeqLen True Passed
  • Model Under Test
  • Equivalent Model
bf934c0b8bc5dab1a14e0ce1e2c3559427b8aed0 Apalache NumPow SeqLen False Passed
  • Model Under Test
  • Equivalent Model
016e17ffd626759d201a7a839fafe2a28629c73c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumPow TlcEval True Passed
  • Model Under Test
  • Equivalent Model
eea33c0e5f9b1842394582e29246b647af1571f3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumPow TlcEval False Passed
  • Model Under Test
  • Equivalent Model
995032f8a18a15e696d50d5717f53181634eba53 Apalache NumPow BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
d196ea4aea1d1ce5ca83cccabe55184a583dda10 Apalache NumPow BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
a50dfd276946f18e195cb41456ee58705f74974b Apalache NumPow BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
aa1189f0a213a57dc032c5271acfc275be3a2989 Apalache NumPow BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
4b4a2e66f08546a3ed56979800fea6b6125b8092 Apalache NumPow FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
224d3580f1a95127eed8c58896a48b59e90a0c5c Apalache NumPow FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
13e190307245c44a818451416278c016e9dfe34e Apalache NumPow SeqHead True Passed
  • Model Under Test
  • Equivalent Model
b58aa8ee0f7b7a7d3b8da49daf830b81aa7e48c8 Apalache NumPow SeqHead False Passed
  • Model Under Test
  • Equivalent Model