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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
1e7b1776740577b7b27d45f7181279c97b876f4d TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMinus OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
34a2b273887a07b47c4d1f3b7ee0ed5e50b82896 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMinus OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
2ab5bc22f1704a42e9b1f997cd72c1cdca816b09 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMinus MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
927b18e0c79d17f9268ee0887306e25ad26a2fc1 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
NumMinus MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
8fb7553c246bf8e3e70985e5ff5d29d597f29a7d Apalache NumMinus Let True Passed
  • Model Under Test
  • Equivalent Model
4568555ca676e3e284e84ea2da28f0ef28006ae5 Apalache NumMinus Let False Passed
  • Model Under Test
  • Equivalent Model
54098ee44f5e72c14366cd4007d7b6cbfdf31fff Apalache NumMinus Choose True Passed
  • Model Under Test
  • Equivalent Model
7ca0d5a8a24c2736e5f96379b93e7fcaaf4b4cbc Apalache NumMinus Choose False Passed
  • Model Under Test
  • Equivalent Model
ff633f99178f89f73bae17fa93dbb0b0c5ce6887 Apalache NumMinus FunApp True Passed
  • Model Under Test
  • Equivalent Model
f8d3fc4edfb2c4c811d1fe490c3ab6d21ad0e73c Apalache NumMinus FunApp False Passed
  • Model Under Test
  • Equivalent Model
53b734034c5fdd4f14c64fbc1768f4f4d017bd3c Apalache NumMinus Prime True Passed
  • Model Under Test
  • Equivalent Model
5fa6b10e6576167615bdf53640ee272347aecfe1 Apalache NumMinus Prime False Passed
  • Model Under Test
  • Equivalent Model
98bc4bd38cc099aacc0a3740e9ea896926baa579 Apalache NumMinus NumZero True Passed
  • Model Under Test
  • Equivalent Model
71ff20a747c0233ac7543317a55f5387cdc18145 Apalache NumMinus NumZero False Passed
  • Model Under Test
  • Equivalent Model
5d3f16c7d16cec96527f3b6f8f12ea38e4903fe1 Apalache NumMinus NumOne True Passed
  • Model Under Test
  • Equivalent Model
108245b360d0e30bb5a4ef3cb5f5ef4093c96276 Apalache NumMinus NumOne False Passed
  • Model Under Test
  • Equivalent Model
8e065bc75cba6088068647e4312ff994cda10fcd Apalache NumMinus NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
0333f5ac9e0f7fd9f74654b1ad1a958a756cd279 Apalache NumMinus NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
5daa50534055faa9778b1f1bffd507937cf92f0a Apalache NumMinus NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
e45e6cef1fddeb3b779d9ca97ed90dffdfae6868 Apalache NumMinus NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
9c99fc5bc817447607d3de4fc71eafc35408adf3 Apalache NumMinus NumPlus True Passed
  • Model Under Test
  • Equivalent Model
69658586b0c52595348f393e7305e79e98f036ca Apalache NumMinus NumPlus False Passed
  • Model Under Test
  • Equivalent Model
455ab83e76acdaa242d9f3f34b2365cdb6693d07 Apalache NumMinus NumMinus True Passed
  • Model Under Test
  • Equivalent Model
ff4afdf1f35fbbb1b904765aeafeef943e1db27b Apalache NumMinus NumMinus False Passed
  • Model Under Test
  • Equivalent Model
ecf4feb77d8aeb939f4bef84ae6626146d1088a9 Apalache NumMinus NumMul True Passed
  • Model Under Test
  • Equivalent Model
39c80742ce3711cc92cdfbb321c4a145cd0efabf Apalache NumMinus NumMul False Passed
  • Model Under Test
  • Equivalent Model
f52e2be645bb297d950b6da7a6ad4281e1bc9a6d Apalache NumMinus NumDiv True Passed
  • Model Under Test
  • Equivalent Model
b4b6c1b18737bd0a8b73115abd1954c0c4b6741a Apalache NumMinus NumDiv False Passed
  • Model Under Test
  • Equivalent Model
fe59afb13e4c09b08ffd22ea5ac8b792d8ed09ec Apalache NumMinus NumMod True Passed
  • Model Under Test
  • Equivalent Model
a1e943cc0fa46072d90bebcc40d831eb9e639ddb Apalache NumMinus NumMod False Passed
  • Model Under Test
  • Equivalent Model
2f736df5d3bd693c6ab911da2a6591cb230b1d39 Apalache NumMinus NumPow True Passed
  • Model Under Test
  • Equivalent Model
aa6ec01a3cd6ff4f9f26910b85cf9152e65e7a1c Apalache NumMinus NumPow False Passed
  • Model Under Test
  • Equivalent Model
a3ce983665f60ff854988df0005bd3e3b83ce65c Apalache NumMinus Def0 True Passed
  • Model Under Test
  • Equivalent Model
975b274edbb1c5a7f99ba117812f87ee2dc772dc Apalache NumMinus Def0 False Passed
  • Model Under Test
  • Equivalent Model
b44507507f9ad3865a9a88e3d7e708f02082dda8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
fd30e4c9770d30f0fcbd49319a60fde77fa5b45a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
1ca177f827c35679c1571018d7f833be65feacb4 Apalache NumMinus Def1 True Passed
  • Model Under Test
  • Equivalent Model
54a3ec919e174166d0bd6dc90a7900dd1949092f Apalache NumMinus Def1 False Passed
  • Model Under Test
  • Equivalent Model
9b61cf2650b27dc2d314e81143ff890d03850bc1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
edfe00cf6d5e32aff5eac576c7834cb6f7370816 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
69741fcf4fd38bdb979925cd3fccece7deb8087b Apalache NumMinus Def2 True Passed
  • Model Under Test
  • Equivalent Model
013f0806fca5e0d090c74006944f0deb9c52bb01 Apalache NumMinus Def2 False Passed
  • Model Under Test
  • Equivalent Model
cbb162da85a2b3713fc5a0a05c204ad518833a63 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
6c9d3cd915e631fc3dfb9013bf83fdde5232114e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
44083c3675623b6e8cf3760972e235f7213c2614 Apalache NumMinus Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
990212ac33fb45b7ac530b7c49ca94b8eadd229b Apalache NumMinus Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
eb7d77755f20be319684ecb8be5022ba9a0031aa TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
cc68d31a1ff99b0bb9c4345794f4539895d6b105 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
NumMinus LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
5fcb9087f403f4fee21045f36ac9365ae1de460d Apalache NumMinus Extends True Passed
  • Model Under Test
  • Equivalent Model
a40f3176a18a4bba1e8ca34da4c4a6f45e243615 Apalache NumMinus Extends False Passed
  • Model Under Test
  • Equivalent Model
5f48d5fe59ccb1215a7a95d814649fb9169a86ef Apalache NumMinus ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
94684a7b8b9a84a4d6f93f7910c63d16ca13780e Apalache NumMinus ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
50717cc6a95187b411672280f858d000f44e1749 Apalache NumMinus Variable True Passed
  • Model Under Test
  • Equivalent Model
781ddf36a63390303ad6fd993a1373c3050b519a Apalache NumMinus Variable False Passed
  • Model Under Test
  • Equivalent Model
3fd97338ab9276ee9049d7ac55a8082090a431d3 Apalache NumMinus Constant True Passed
  • Model Under Test
  • Equivalent Model
fbfb2e5bbc1cdb0355551c9c1c4b1afa7b0b1619 Apalache NumMinus Constant 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
4c21c2f73dc563fccd074b481443517694ef1272 Apalache NumMinus Instance True Passed
  • Model Under Test
  • Equivalent Model
ea26ec47c962991ef605aacb995cfb785bfe9194 Apalache NumMinus Instance False Passed
  • Model Under Test
  • Equivalent Model
bb9d5042992f1f6de559d405e92a077454918b84 Apalache NumMinus InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
0f59f72e945b71b29cc10ab7b700b72eddf2f371 Apalache NumMinus InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
a8295fa2f2e9f2e7e9530b6671aaa360ed401c0e Apalache NumMinus InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
7ecb39287ecf66ede52d41dc57df126696ae80b2 Apalache NumMinus InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
80c4d6d98a288ea5822bf6398e74c5c7b205e36b Apalache NumMinus InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
bebeb9177f1d9b563c1abb970814ffd053f18f23 Apalache NumMinus InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
13836d995f7da44d0dc3cc0245099cca09bcc790 Apalache NumMinus InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
604be757e73ce07a7f33c328ea1237b56f5898c7 Apalache NumMinus InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
415816eaf7f7f01edc535a98ac57121c44513f08 Apalache NumMinus InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
2f5d5fb03cbf3ddad8f9451598a629b35a37326f Apalache NumMinus InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
5b83f4ffe90fc4841908bd41610269e86309bd16 Apalache NumMinus InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
79d0f6b6b3c96ec5e0a9f116abdc8086a0072a20 Apalache NumMinus InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
347fa86a6d74b0471e17a3f40cab60ef1d41627c Apalache NumMinus InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
44b389205460063f726fc0eb5a38ffe4c634bd5b Apalache NumMinus InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
b868b50b748970cd37aaec094bc12bbc96c8994a Apalache NumMinus IfCond True Passed
  • Model Under Test
  • Equivalent Model
0486d76bcd94dd30790fa6b5ffb244993dce4b6c Apalache NumMinus IfCond False Passed
  • Model Under Test
  • Equivalent Model
0860811137b089d064e691a2cfcc535c889b6c25 Apalache NumMinus IfThen True Passed
  • Model Under Test
  • Equivalent Model
a65cd5a589dcc4d3bc4ee8a4769f087a3616950a Apalache NumMinus IfThen False Passed
  • Model Under Test
  • Equivalent Model
1b2a70bec97d69c58115e0b491b969aaeae8423a Apalache NumMinus IfElse True Passed
  • Model Under Test
  • Equivalent Model
5a6db31be5faaf6f34b38530b04476f9c4d4a4fe Apalache NumMinus IfElse False Passed
  • Model Under Test
  • Equivalent Model
91917c92f3137a09d58c0eb91c455f1451a2f79a Apalache NumMinus SeqLen True Passed
  • Model Under Test
  • Equivalent Model
2790f9cf4e3006afac3f8bd9d3efc550755d6044 Apalache NumMinus SeqLen False Passed
  • Model Under Test
  • Equivalent Model
f4010360316374d9f210b12360a45bb9083c7c72 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMinus TlcEval True Passed
  • Model Under Test
  • Equivalent Model
e30a54b9ede0bc1553ae1ae2a8b4c660f57b21e3 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
NumMinus TlcEval False Passed
  • Model Under Test
  • Equivalent Model
c9011a765ce6b68bacf673e7f5ea00d77134fa7a Apalache NumMinus BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
5dadfdb3df29d9110e63c6e6f71857af781063ed Apalache NumMinus BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
5d1fdd6aa3bd5c29be8aa6a6c4ed31b7850db614 Apalache NumMinus BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
678e68828e038e6baa7ffd9c29d43e52c2351fa3 Apalache NumMinus BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
25ea04f712bbf71cc55b63222dbe620e991851f9 Apalache NumMinus FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
fd27201b0c276679d1b0dfb4a84bebff7b802dc1 Apalache NumMinus FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
bc62c8687c638d9a42d0c9658a06070b4e1935f1 Apalache NumMinus SeqHead True Passed
  • Model Under Test
  • Equivalent Model
09b9b99ca28e303bd55bd0b7bcd7c8d4456d30f0 Apalache NumMinus SeqHead False Passed
  • Model Under Test
  • Equivalent Model