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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
41e760008890a8c1d097c0b8d3be8ed0b899c62e TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumDiv OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
63da80130fb92a7aad392aab8fdd016c0fef837e TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumDiv OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
6c173b2544c42ceed56725d7f56827c27ad43ec3 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumDiv MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
5ad22d1d92be0aa10ff8d06f51fb0ebaeabd2aae TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumDiv MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
141d24dfd5b99d9b08e5fe9604e9180d8b83506a Apalache NumDiv Let True Passed
  • Model Under Test
  • Equivalent Model
13ff87a457b221e778ea2d0694f866c48c0192e5 Apalache NumDiv Let False Passed
  • Model Under Test
  • Equivalent Model
514977d34d2d5d8c5e77a6c12e1a9471e2ed2057 Apalache NumDiv Choose True Passed
  • Model Under Test
  • Equivalent Model
7a5c8da4e20fb9b5e5399d5660fc8c550418cb73 Apalache NumDiv Choose False Passed
  • Model Under Test
  • Equivalent Model
9f6d048e5bceb75acc0e4d97b141de194ac763c5 Apalache NumDiv FunApp True Passed
  • Model Under Test
  • Equivalent Model
1cfda8c959a81902cbee921d6722767aa688ff09 Apalache NumDiv FunApp False Passed
  • Model Under Test
  • Equivalent Model
63e56b3fbd052171060bc65bd37726c1bc51a6d2 Apalache NumDiv Prime True Passed
  • Model Under Test
  • Equivalent Model
dd050389ac69c22f1479c579f958dc9f6a98390a Apalache NumDiv Prime False Passed
  • Model Under Test
  • Equivalent Model
f038b07f3bbefed3f8035fdfbe0eda40fed586cf Apalache NumDiv NumZero True Passed
  • Model Under Test
  • Equivalent Model
731e63204398d6b5a132d1c928d2559572c0b2b3 Apalache NumDiv NumZero False Passed
  • Model Under Test
  • Equivalent Model
6daa383763db51ac63b542178e54cdcee94d50ec Apalache NumDiv NumOne True Passed
  • Model Under Test
  • Equivalent Model
b3b3fe03c1c6bc05c9758b2527a4ffc53c2c7631 Apalache NumDiv NumOne False Passed
  • Model Under Test
  • Equivalent Model
88aa182c3d9ddffea593eaf85473a94cfbc20722 Apalache NumDiv NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
3e01cbea26ff65309139a93f5e6e49bdee3fa1eb Apalache NumDiv NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
9f14414ef9760a610429042534c5cd449663c53c Apalache NumDiv NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
2ba198dca12a9eb5454fc83c196ba485bf657ad4 Apalache NumDiv NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
bb73c5bc7634056770f7a459e8f1b926cc37dcb2 Apalache NumDiv NumPlus True Passed
  • Model Under Test
  • Equivalent Model
ac805ce3e370a768e424f65adceabbe925942ab6 Apalache NumDiv NumPlus False Passed
  • Model Under Test
  • Equivalent Model
1bd59be9744def68a5e7fc853b20a70c6ee273e3 Apalache NumDiv NumMinus True Passed
  • Model Under Test
  • Equivalent Model
aee3ce09fa97d6dd41a3cedec71f57f30233dc6a Apalache NumDiv NumMinus False Passed
  • Model Under Test
  • Equivalent Model
7a46cf7f67e8cb20954f50ab55d149abaf71f8a4 Apalache NumDiv NumMul True Passed
  • Model Under Test
  • Equivalent Model
1e4ea436d5543550811270a67ced7bd76fad2d3a Apalache NumDiv NumMul False Passed
  • Model Under Test
  • Equivalent Model
2ab3c5213521b28cc0c62642aaebb94f5c62e1d7 Apalache NumDiv NumDiv True Passed
  • Model Under Test
  • Equivalent Model
ba2692ebe60424545aaa5e9c886e3c1497c287dc Apalache NumDiv NumDiv False Passed
  • Model Under Test
  • Equivalent Model
2179eecb49a6a65a5e0532d1db65da362c1bc9e7 Apalache NumDiv NumMod True Passed
  • Model Under Test
  • Equivalent Model
4f3df857e988abc59e0bc0cf2319f2e514943676 Apalache NumDiv NumMod False Passed
  • Model Under Test
  • Equivalent Model
4d31962e0d290a0e5e3192d9c92469d3a27ded82 Apalache NumDiv NumPow True Passed
  • Model Under Test
  • Equivalent Model
7039d5f435380b7d0d55334607e3b74ff7255b25 Apalache NumDiv NumPow False Passed
  • Model Under Test
  • Equivalent Model
ca2fd40b4bb513ffb5c833207df4c2826e0db841 Apalache NumDiv Def0 True Passed
  • Model Under Test
  • Equivalent Model
39b95c4b628a4230fa1e122fd5d728eb03f79995 Apalache NumDiv Def0 False Passed
  • Model Under Test
  • Equivalent Model
20dbde3afca9f166215c9f406a8c43e328c04df6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
551fedb5faf41c0702e7e1112dda6fcf076d0746 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
7b0cccd08ae6c6f6e37e9a42b0039a8e60fb3989 Apalache NumDiv Def1 True Passed
  • Model Under Test
  • Equivalent Model
62723af3c119b0ea62953f7e17619e0b1975df07 Apalache NumDiv Def1 False Passed
  • Model Under Test
  • Equivalent Model
388e1596d1ab58b56f2cc3627c3ec661bb524db2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
4260fdd33dfb7a8e726d71fbfb6a3c57cdd641f7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
0d1b6f1ecda216f921a069ed6efc287e8e6af3d7 Apalache NumDiv Def2 True Passed
  • Model Under Test
  • Equivalent Model
1452ed5c8c5922bedf6c018a77e549c71d8d4af4 Apalache NumDiv Def2 False Passed
  • Model Under Test
  • Equivalent Model
d1ea25466413046cee937a2888451d2c6d297d80 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
69805a519321f65146abd0af07bfd76e35bac901 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
e7ea8c576677f6987a72819d0303d009a6d217f1 Apalache NumDiv Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
43ba074e79de1639d890e9950aa69bfe753e6ff9 Apalache NumDiv Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
fc6c76a4f1932d5c383d89a3a36df6674bcc9c25 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
2992d53b31eeb9d3d2271bc981e1baab72a53ec8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumDiv LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ca6a3f9a0da445ec7a3f8d903264518a1f7998ac Apalache NumDiv Extends True Passed
  • Model Under Test
  • Equivalent Model
e94e5c7c93f3cce7f76d3abe0b9995cf0d8ca0d2 Apalache NumDiv Extends False Passed
  • Model Under Test
  • Equivalent Model
2e664c18c948468cb6c86d67b9e1764900b5b45f Apalache NumDiv ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
edac7cd50f6a00d7f8347d8ded173ca489edf1f7 Apalache NumDiv ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
9602d0024c08b01322a76c5963d36a0edd6514b9 Apalache NumDiv Variable True Passed
  • Model Under Test
  • Equivalent Model
0772a0ce94c6be56348907da8d74e021c900057b Apalache NumDiv Variable False Passed
  • Model Under Test
  • Equivalent Model
95fad5c9595b84bcee41af78a94e697a4139cb47 Apalache NumDiv Constant True Passed
  • Model Under Test
  • Equivalent Model
4b9953991c1dc3c6dfd81c5c816a9ff479483baa Apalache NumDiv Constant 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
818c9219523d03e2b3b2261e2a8edd54508fe020 Apalache NumDiv Instance True Passed
  • Model Under Test
  • Equivalent Model
8150f69a422783a58e3d51c7e6a7b8b47229731a Apalache NumDiv Instance False Passed
  • Model Under Test
  • Equivalent Model
4d83fa1b3942af2d5e23ef3095057c4e5a7acf40 Apalache NumDiv InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
a538cafb697a0c10076eff38bbd111839fdba5be Apalache NumDiv InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
6a6747b17a3256ca92bf9b37155a4fe7bdf6f971 Apalache NumDiv InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
270620726fdd3242b1833f7473120809429c17dc Apalache NumDiv InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
aa353cc48266054323fe06d3c9734552cf4ce179 Apalache NumDiv InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
bda11be87461adf28958e29cb06e3920347805dd Apalache NumDiv InstanceNamedWith 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
e9c0fcc40c53d275e9c6639d86703009b6713021 Apalache NumDiv InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
06a1473bb6f06243b10b64f4654a89f8086936e9 Apalache NumDiv InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
abbaa55f5e1bbd240d3a0c50e02d94ab4de73836 Apalache NumDiv InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
122c2f014651805dc75b69594d9d088e92d34e62 Apalache NumDiv InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
cc8a5234a722aacbd7882ac0965dd439e1dab526 Apalache NumDiv InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
3d445a61bcdb55ef97e089f9486cd992e90b0155 Apalache NumDiv InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
3dc8abf664fecafdbfca67cdda08f846994fdce4 Apalache NumDiv IfCond True Passed
  • Model Under Test
  • Equivalent Model
a2dff2ac9fad78bc9aff995b8050370b891bc3e4 Apalache NumDiv IfCond False Passed
  • Model Under Test
  • Equivalent Model
b27b28834d901fa027586af060cef2727c35e27c Apalache NumDiv IfThen True Passed
  • Model Under Test
  • Equivalent Model
c794f7ca5d266fbe16f168721bbbea67aaf6094c Apalache NumDiv IfThen False Passed
  • Model Under Test
  • Equivalent Model
05ab36e11ae9398809c5f63aef5a2e38e0441021 Apalache NumDiv IfElse True Passed
  • Model Under Test
  • Equivalent Model
50efb77fa7874ac4f79d16d615f02a9f2b48d5b9 Apalache NumDiv IfElse False Passed
  • Model Under Test
  • Equivalent Model
0e8b83db0bd8c3e609d47ff323f4b4b0a680ddf2 Apalache NumDiv SeqLen True Passed
  • Model Under Test
  • Equivalent Model
54fb88d1b4c086334123587740bf9d16d2d18b8b Apalache NumDiv SeqLen False Passed
  • Model Under Test
  • Equivalent Model
16b5497a41f192e7eabc2160734b15da5f105e71 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumDiv TlcEval True Passed
  • Model Under Test
  • Equivalent Model
dfbb361a823e5c46617b5c6a98f0fdfdfb1d839f TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumDiv TlcEval False Passed
  • Model Under Test
  • Equivalent Model
7e770f59485440c62f0e5ce0b940a3f20fcafa02 Apalache NumDiv BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
53601410354685e301650c76efb93f6e867c16ef Apalache NumDiv BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
79f6900fbdb9154d2f46b9f4619ff87011249a76 Apalache NumDiv BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
8c6c056ea21a0cc0aca42d8655a77bbf5015056b Apalache NumDiv BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
f3b9c4e6a795c12567658de4ef7b3fc9bbb6903b Apalache NumDiv FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
cf6e858fc2b20d0eaa4358a3fda8c042339d2595 Apalache NumDiv FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
6fe077472aa24659bad7e3ffd7f905455d3a490e Apalache NumDiv SeqHead True Passed
  • Model Under Test
  • Equivalent Model
c98ff60199fe10f0adb7529f9095bb2f20394330 Apalache NumDiv SeqHead False Passed
  • Model Under Test
  • Equivalent Model