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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
f580cc3b06705bd4642da650f2c5d40bb65439a0 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
And OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
bbaf2108ac35f1f82817c5189307323084295b2d TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
And OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
6caaaecc57ad921d70b6bffa63fcee007d8b9c9a TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
And MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
5835eae97994ab84cef7b27719f2db940b0f1b85 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
And MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
934f1d94d3075ce2b93e8133211746cfe3118a87 Apalache And BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
a384cfe51a3f8eed5e48f12d999762513e4ab7e9 Apalache And BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
0856bc21023b45ce56b3d3c01cf38abd1851bc59 Apalache And BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
52a7f03b0e5f6ae081816856a6bad900ac6a7440 Apalache And BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
23025fbcd8936222f9ecd5d962e96c1c6a2e0bdb Apalache And And True Passed
  • Model Under Test
  • Equivalent Model
2e0b8a91610c08545b3c504344ed8b6804140875 Apalache And And False Passed
  • Model Under Test
  • Equivalent Model
28ebbde43ea69ba9ff3fbe5434f073356583b36e TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
And AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5bf6b0e52cbfc93805a74870e26bdb10fc20e262 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
And AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
4c6d31167702f82dff46089666ffc9f30db6e17d Apalache And Imply True Passed
  • Model Under Test
  • Equivalent Model
9d2bee499ecb429e8362fad71520bf1a35a22739 Apalache And Imply False Passed
  • Model Under Test
  • Equivalent Model
bde3dd56526d8c05fcb2533d5604a3971e9b5f9e Apalache And Not True Passed
  • Model Under Test
  • Equivalent Model
b356d2503f38f9bd3ab7d0f5534425ba6f1063c4 Apalache And Not False Passed
  • Model Under Test
  • Equivalent Model
49d681a75bb5769a1583342ce2f11940e37ee0eb TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
And Or True Passed
  • Model Under Test
  • Equivalent Model
723641895431b9b43ff120e3371541f70f22f6bb TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
And Or False Passed
  • Model Under Test
  • Equivalent Model
b648f8aa924fb179b37240884592c4c96da949f4 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
And OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
9a46870522b9ebedbf984d864042c93dd3f07fd3 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
And OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e193a250d1d84a1c35d4470aa1a026417afb9150 Apalache And Eq True Passed
  • Model Under Test
  • Equivalent Model
9b2c0571ea4d727eae26fa9011ed98ae5ac35839 Apalache And Eq False Passed
  • Model Under Test
  • Equivalent Model
32e2cf8fb8d64ce0844bc9a6863f9c45cdd59ef4 Apalache And Ne True Passed
  • Model Under Test
  • Equivalent Model
0cf12e8bb5a359341061638cd4c32596ff60c663 Apalache And Ne False Passed
  • Model Under Test
  • Equivalent Model
9a5e3863bdbc237c337f081c9e7fe4cf4453725c Apalache And Let True Passed
  • Model Under Test
  • Equivalent Model
f14fb5ed8ba02349ac0fca1e49adf786525979b0 Apalache And Let False Passed
  • Model Under Test
  • Equivalent Model
2e89a8e866b2efdaf2a4ffd5b82b0b1f7763980f Apalache And In True Passed
  • Model Under Test
  • Equivalent Model
5fc6ed7a397571c4f92cb75a88d66a04cb279098 Apalache And In False Passed
  • Model Under Test
  • Equivalent Model
eee1ba85df7022277c9e55ce9b1bae461e314742 Apalache And NotIn True Passed
  • Model Under Test
  • Equivalent Model
66d160461a63d7905b9613901c3c9b4f6d923372 Apalache And NotIn False Passed
  • Model Under Test
  • Equivalent Model
b51a0e507fdc4195fddd68e1da0346fd227c2037 Apalache And Exists True Passed
  • Model Under Test
  • Equivalent Model
6104c8efaea0866af691c0128ed03de675df84ef Apalache And Exists False Passed
  • Model Under Test
  • Equivalent Model
cca0bbfeddc2efdd95173a50adda581d6f9612d2 Apalache And Forall True Passed
  • Model Under Test
  • Equivalent Model
41b2c07c482f3beb3ea0e0677b92d83aa1d3cc62 Apalache And Forall False Passed
  • Model Under Test
  • Equivalent Model
b37906ac4e70e5680c1fb63457e9e611fe19c07e Apalache And Choose True Passed
  • Model Under Test
  • Equivalent Model
3d539580b6e80bfdcd03189ac77a8330feaff301 Apalache And Choose False Passed
  • Model Under Test
  • Equivalent Model
c8eb4b6a4ae416728b2c31cf6fffdf5b6c73930c Apalache And FunApp True Passed
  • Model Under Test
  • Equivalent Model
cc14e5033924706b44e2fc209680c59b1362ad9a Apalache And FunApp False Passed
  • Model Under Test
  • Equivalent Model
b8fd3a9394214400d2e581905731de88264a501c Apalache And Prime True Passed
  • Model Under Test
  • Equivalent Model
15682286b5323d157b3fb35656e604c40c39abda Apalache And Prime False Passed
  • Model Under Test
  • Equivalent Model
b62019e401c3a4acfe0f56e6d5e46860ed4250d9 Apalache And NumGt True Passed
  • Model Under Test
  • Equivalent Model
64c8d287ddf77c539e25597dec505cefbf2bb791 Apalache And NumGt False Passed
  • Model Under Test
  • Equivalent Model
7b558e8a455c5b2466d6f37afe61331dfc44701f Apalache And NumGe True Passed
  • Model Under Test
  • Equivalent Model
ecb6e78812175a081cef063ddd1a69e5e8c8f422 Apalache And NumGe False Passed
  • Model Under Test
  • Equivalent Model
dbfcc200b7b5d5d897666f508e01198ef89799a4 Apalache And NumLt True Passed
  • Model Under Test
  • Equivalent Model
b544b2a2610aea053f9ebc112e5817c5ac54e1c0 Apalache And NumLt False Passed
  • Model Under Test
  • Equivalent Model
706da1b468c81f5853ce350634a4fb6425bd9244 Apalache And NumLe True Passed
  • Model Under Test
  • Equivalent Model
cc2c8a0ce9c6a9be308921ad328236958351e8b9 Apalache And NumLe False Passed
  • Model Under Test
  • Equivalent Model
b7d76362b86d36ca3543471b8028c1c3b1aa1d38 Apalache And Def0 True Passed
  • Model Under Test
  • Equivalent Model
6a6d327ea007e4ed8fdee09901546951f7c11f9c Apalache And Def0 False Passed
  • Model Under Test
  • Equivalent Model
4f7ca26c505f244a121f61d8e78c58158cca531b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
f987a74cc4c995c1885872cda735527645ce625b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
44bf54955398767fc7cfc64839e1b9ec207ce71d Apalache And Def1 True Passed
  • Model Under Test
  • Equivalent Model
52984650b5621b880542b7b92c29bab28df7b2b7 Apalache And Def1 False Passed
  • Model Under Test
  • Equivalent Model
319359e440920ffed360072356c758cbfb9f98f1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
b966d05c3bda35df438fc1b108621d4e36e5343d TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
aa4ef39b749874988479c96a1324c7871b5d2c5d Apalache And Def2 True Passed
  • Model Under Test
  • Equivalent Model
6dcc60029d0cea4c5c45304f60734cfb15f549cb Apalache And Def2 False Passed
  • Model Under Test
  • Equivalent Model
08ffcaa9d0af83f5faafae8332fd3bf2c92fdd7f TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
70889423d7188b852a135ec5b8ceb91331807cb0 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
15edfd7a85b3fbea3c5be61294ace4510e83bd45 Apalache And Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
713fb2f4f12aa304412b24715430f1852f4722b5 Apalache And Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
70f6c7c8aa1c81fef986a3670d3c04f6af50f868 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
1f0815609350a80afa7ec102ad281122de788a7a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
And LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
0375443e581246ce5b03020203726e935c3a8201 Apalache And Extends True Passed
  • Model Under Test
  • Equivalent Model
3377aa75cfaf8b0ca8990530f0ac8873d23950d0 Apalache And Extends False Passed
  • Model Under Test
  • Equivalent Model
c712508f80fd7bbde4c149a73cc801c0f49886a2 Apalache And ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
ae1e597ab9e05a25f6c5921003fcbc64f0d4d23c Apalache And ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e5e60336daff343ecfaca7aa16756ced2246701b Apalache And Variable True Passed
  • Model Under Test
  • Equivalent Model
3e9bc6d3ceb3959d63f5de5aa39ff67619a0cf6e Apalache And Variable False Passed
  • Model Under Test
  • Equivalent Model
0d45b04d124b14716a01d7069e6c55fe40fa1e6d Apalache And Constant True Passed
  • Model Under Test
  • Equivalent Model
f51b6b3f7a51b7fe9d53a8de51510277df8248ec Apalache And Constant False Passed
  • Model Under Test
  • Equivalent Model
3231ad2afc09b3722a423023e0431198d71ab3be Apalache And ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
31effcd0fa642aa46e30fd5b38157c6da51feac8 Apalache And ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
627894965dcd7d112a807812d64c2450c428b18d Apalache And Instance True Passed
  • Model Under Test
  • Equivalent Model
fd359cc68b9b9e58a27a13b77a6b35b9408ddaaa Apalache And Instance False Passed
  • Model Under Test
  • Equivalent Model
033d00f6284e6518992eb6ddab55fe4155839557 Apalache And InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
e934f896c2f773869a3ff7dbca67552574510339 Apalache And InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
b311ccfb6ffaa46d31b710028f8257d80dca7f46 Apalache And InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
4b8946aafaa516d92a37c960241913fb979f8c88 Apalache And InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
63d235d9596878d6a664965222af25970b5f0797 Apalache And InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
a5e33b2af42ae573ee872ad67611aa223645eb5c Apalache And InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
84fd79cb5d2c9c8cabf46164501bd81a22a6265a Apalache And InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
2314f1b11127cbae7142737d43db5bb9b13cec87 Apalache And InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
e977357801c613c33c2260c0031104e82231b0ee Apalache And InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
44d422cbcaf42adb91217e4f833b46222170a9dd Apalache And InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
a2fa1f9dee7a095768580b6657dbff49a4fa4eb4 Apalache And InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
00f088d0c34a92cff6ff47cf05d960c4a5aab0d9 Apalache And InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
d968c08e71857f8be7339efc36cbbe6033844c5e Apalache And InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
8832c213404995a98a9989ccd37e26da8540d4d0 Apalache And InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
96b842ecc4a364698078eab6d225365383003597 Apalache And Enabled True Passed
  • Model Under Test
  • Equivalent Model
18c091666b4d57070c922490c38012fdb7fe7c24 Apalache And Enabled False Passed
  • Model Under Test
  • Equivalent Model
c2b07476f88b5d91b985b93efb74059f1514fc64 Apalache And SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
d7e0b3939d20b41a19ecd2fd95740d3f51fddb1d Apalache And SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
93260058bb7ea1f75e63204a3cdbf811136aba4f Apalache And IfCond True Passed
  • Model Under Test
  • Equivalent Model
cc30efb1bcad44905f03b3b7a858eb6dd98d8fc9 Apalache And IfCond False Passed
  • Model Under Test
  • Equivalent Model
191edcca1760ef8804004f0eb30b340244d3ae46 Apalache And IfThen True Passed
  • Model Under Test
  • Equivalent Model
1ff89852084c936aa8d3e7f3cde7a86dd3044d38 Apalache And IfThen False Passed
  • Model Under Test
  • Equivalent Model
8dd211ed95b33fb777d3192790ff0123ca00839d Apalache And IfElse True Passed
  • Model Under Test
  • Equivalent Model
f24455401af1829c4895d2e47f20cb08f2dfb3f9 Apalache And IfElse False Passed
  • Model Under Test
  • Equivalent Model
c9159678594ed939c68d2e8d3dc5e6d674b1baf9 Apalache And Unchanged True Passed
  • Model Under Test
  • Equivalent Model
240e80dc15efabaafc82045ef1b9bfb40c66944f Apalache And Unchanged False Passed
  • Model Under Test
  • Equivalent Model
94a52a27aac370548ed0b21a5789cb96ff459ba9 Apalache And Equivalence True Passed
  • Model Under Test
  • Equivalent Model
0a71254a715433d2523852c2b1a491f49ad9a701 Apalache And Equivalence False Passed
  • Model Under Test
  • Equivalent Model
b6123830170a3a151fb060bacd43e2f7a76ce53c TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
And TlcEval True Passed
  • Model Under Test
  • Equivalent Model
ba63e80c0bbde8f95a0504a9999bdbba475ccb40 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
And TlcEval False Passed
  • Model Under Test
  • Equivalent Model
075b5284839238612156df4bd45a20700f3e706b Apalache And BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
b259291ace3761bef9957ecb04c6b3286b36757b Apalache And BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
d4064e66fc69c93202ce3cb94d725e295f39a84d Apalache And BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
1dd94d4979a5b9d7a50f37e677730e788bfc4279 Apalache And BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
a69d61b93971989cf5a29292c49a20652b5cf8e1 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)
And FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
69d004576353c9ade94f3286c51266628e3f1f4d 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)
And FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
c512219a3563b9511c6a702f69aa738b33d81d5f Apalache And SeqHead True Passed
  • Model Under Test
  • Equivalent Model
65c0bb6c20e70cbcc699c639c9ac82b3feed45e6 Apalache And SeqHead False Passed
  • Model Under Test
  • Equivalent Model