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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
44b3836e6891473f8affb6794daefc5fae72111b TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Not OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
74954692f5e5d31df6babcb90b410d08b33f0d47 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Not OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
8dd98dd01d7142f5b864059e69951101e7585655 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Not MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
e131dbf1a317c39975270b98a3ff24dc75de0d72 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Not MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
ef6ae3291fd48908358702412d85777b39c97386 Apalache Not BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
4e676aef8a0f64d90130ba264875c998fc73b55b Apalache Not BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
55220aeed17a1df57f7c1252539082684702bb7b Apalache Not BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
925f33a35f5b564db7c32d77d5d534663ca819fe Apalache Not BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
1eef4085ef3dd9dd4764d72bc092b06258cfc0fb Apalache Not And True Passed
  • Model Under Test
  • Equivalent Model
b3ad7d811b6ceeb78da8ca69dc5ce436397bca7e Apalache Not And False Passed
  • Model Under Test
  • Equivalent Model
716ba9a108d71bd104d4f0ee2ec51fe99a053d11 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Not AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
4a79bb923b62e11a5c720dd25e8e826e65cae582 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Not AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
7f05e5814083dd650aab02b56c5174e8a3a98fe7 Apalache Not Imply True Passed
  • Model Under Test
  • Equivalent Model
5a3af6565cf45f0e016d0c28f17018f168fb77bc Apalache Not Imply False Passed
  • Model Under Test
  • Equivalent Model
306456070cb441c51b54dee95f9e338da4befac8 Apalache Not Not True Passed
  • Model Under Test
  • Equivalent Model
067efe3c3b5e6bdf7d0dd9f0c7ca026846a999f4 Apalache Not Not False Passed
  • Model Under Test
  • Equivalent Model
f8ece3fc347745f7ada3729642bfa883a51da770 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Not Or True Passed
  • Model Under Test
  • Equivalent Model
e84d48fa783fbd46b6e6e8292942d30ddf58520b TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Not Or False Passed
  • Model Under Test
  • Equivalent Model
9a63ea7610d0176ec69c45397893b06f51adf056 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Not OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
43e86082409990c484cb3ac96e19491d92545755 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Not OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
e8754ffc8b6aa5ea08cf6bfc9c7bac7f56b5f320 Apalache Not Eq True Passed
  • Model Under Test
  • Equivalent Model
4e6ac30ea701146d704af57a3d8dc7be7bbc0952 Apalache Not Eq False Passed
  • Model Under Test
  • Equivalent Model
bb05ddb0ca1c01028cc1a3cccab6057a8b8e9933 Apalache Not Ne True Passed
  • Model Under Test
  • Equivalent Model
557702caaa4588a99b7d2d1e3cea721336f42636 Apalache Not Ne False Passed
  • Model Under Test
  • Equivalent Model
ad93bda5d89e18cc26be89f61f46fe743c8ead35 Apalache Not Let True Passed
  • Model Under Test
  • Equivalent Model
4ab8f0a1fc5c254a61f4c0dbafbe84061a538c0c Apalache Not Let False Passed
  • Model Under Test
  • Equivalent Model
bab431f0527ec6403e9e58eda301114f7ce55a19 Apalache Not In True Passed
  • Model Under Test
  • Equivalent Model
74848245c7e45b65eb9e251b121981efd4032bbc Apalache Not In False Passed
  • Model Under Test
  • Equivalent Model
1f5a5cb2293754d9015a23b81103f9145e79befa Apalache Not NotIn True Passed
  • Model Under Test
  • Equivalent Model
72573c4f07ac2bb995ebc9699a505bbaaa1aa856 Apalache Not NotIn False Passed
  • Model Under Test
  • Equivalent Model
c0dcae3eeb35be4ced3ecfbc03015357e56be819 Apalache Not Exists True Passed
  • Model Under Test
  • Equivalent Model
590f69222f3f626b034735d408ab5fc0f116e64e Apalache Not Exists False Passed
  • Model Under Test
  • Equivalent Model
7ce982038794efebb5f3d7f3250db4400de99871 Apalache Not Forall True Passed
  • Model Under Test
  • Equivalent Model
53e030882c99c0728bf252dcb5fb0d8cc61f20b4 Apalache Not Forall False Passed
  • Model Under Test
  • Equivalent Model
ac93ba2b50754a0fae0bbdeb852a79e43ffab502 Apalache Not Choose True Passed
  • Model Under Test
  • Equivalent Model
92952727543bd92ecb93c1922fe032d6689f8c78 Apalache Not Choose False Passed
  • Model Under Test
  • Equivalent Model
c6e6ba9cc8b45e000f2bcef68b8963fa71ecb6bb Apalache Not FunApp True Passed
  • Model Under Test
  • Equivalent Model
17b802026ef628c00fc70fa61922186f152d9b45 Apalache Not FunApp False Passed
  • Model Under Test
  • Equivalent Model
3dfed61c451f9c4ed1b62cc7ddcfec7d83fa62f1 Apalache Not Prime True Passed
  • Model Under Test
  • Equivalent Model
8dbcebc70d0963cb6ad56aebeb49dff454fa12ac Apalache Not Prime False Passed
  • Model Under Test
  • Equivalent Model
0430eb8551f91c9f086e750425f93ed65947cca6 Apalache Not NumGt True Passed
  • Model Under Test
  • Equivalent Model
d116421942e60c7d6ea7426803da885eef2cfa3f Apalache Not NumGt False Passed
  • Model Under Test
  • Equivalent Model
151c5578b1530c9a56c5f682cd8148797c24b36a Apalache Not NumGe True Passed
  • Model Under Test
  • Equivalent Model
06566d8abbb9b0237b0ce3dbf80cd431c6ccfa55 Apalache Not NumGe False Passed
  • Model Under Test
  • Equivalent Model
8aa6d9c1353b13fc0c71f0fcc7dc7d23dc3a24be Apalache Not NumLt True Passed
  • Model Under Test
  • Equivalent Model
6b00e17b7c1121738bcdb3ddb31e55a7a2285086 Apalache Not NumLt False Passed
  • Model Under Test
  • Equivalent Model
5a90ada9f018d443a31d290d014f93a04bbed9d6 Apalache Not NumLe True Passed
  • Model Under Test
  • Equivalent Model
c5f788cce1507cecac84317e0fe0a22899cd4eda Apalache Not NumLe False Passed
  • Model Under Test
  • Equivalent Model
18d2b6f5a286cf5235fbfb5efc3ca80898588160 Apalache Not Def0 True Passed
  • Model Under Test
  • Equivalent Model
66cbdbd7a3ae66df309ac8365dea79b150b7d9e7 Apalache Not Def0 False Passed
  • Model Under Test
  • Equivalent Model
d42e22894b4538046f84d64ee841c11ad43aab04 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
9fbd8698755ce75ae30d3a75948b3af2c70bdf3c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
8aac44bc278a43688f036e43f3a0f0f91ad2cefd Apalache Not Def1 True Passed
  • Model Under Test
  • Equivalent Model
c81f9abf51be8f6b5a6227d8a95d3726c97b4774 Apalache Not Def1 False Passed
  • Model Under Test
  • Equivalent Model
e36a830f4a480765c17bd1622b0193613a026e25 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
0ad72c74d4d91457766cce4b7ac7904dc13095b2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
982f8bbdac0120ddae993c091069ffc79db12c8c Apalache Not Def2 True Passed
  • Model Under Test
  • Equivalent Model
f4c60e78bc32b29757682e4fb664cb53e8f147b0 Apalache Not Def2 False Passed
  • Model Under Test
  • Equivalent Model
6d2e6f4d91ba8afd4a5da2fc04f9c42cc34a8f64 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
51e3679f930609e16a145084707a180c9e1c834b TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
4896231436275e3e2bb94a5ad56148ef2db09736 Apalache Not Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
21e8f84e69d1a65113e6763863ac64a94b949b9a Apalache Not Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
e91b4df138def45e10596847755fc55c36a18851 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
ce26be14274d2dfe1c6a83911893482426372bd4 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Not LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
ad7e4718e2e516396910ec9f8ff6d26dc4765ba5 Apalache Not Extends True Passed
  • Model Under Test
  • Equivalent Model
dcd11026ccd432bdc0c38f541e014d2abe67244a Apalache Not Extends False Passed
  • Model Under Test
  • Equivalent Model
bad3a091b771009c00f8453d89f825be7cbabcb7 Apalache Not ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
500dd0207a3ecd5c86821bc0db4d8da40b3c1b53 Apalache Not ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
854ddc017b2819c8be7cc8db0cd811a34d11e546 Apalache Not Variable True Passed
  • Model Under Test
  • Equivalent Model
85b481dc0a4ef2e4fc16dac5bc5f10bd076d3d57 Apalache Not Variable False Passed
  • Model Under Test
  • Equivalent Model
cae863783d1eb7a2467d87a957f5902d2ef4439b Apalache Not Constant True Passed
  • Model Under Test
  • Equivalent Model
7ef82559de8da974331ccc17ac483a62b0b87752 Apalache Not Constant False Passed
  • Model Under Test
  • Equivalent Model
75a38b6ee73c21a109d286c0d491532d23280b90 Apalache Not ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
104109ca0379f178e46cee4a878fa9abb4ba3a28 Apalache Not ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
a50a0fb3927b7705b99ea64e7a96b465742973d5 Apalache Not Instance True Passed
  • Model Under Test
  • Equivalent Model
5e8d90f2b8c51027409410f72aca978444ea30c3 Apalache Not Instance False Passed
  • Model Under Test
  • Equivalent Model
f065634db37a298899a34a512c69a460f9b2ba09 Apalache Not InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
9ac066ec91767ad380414f18a3a49fcf8904ce34 Apalache Not InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
19a08da53d1e909a65a031f9de55662d85abe9e9 Apalache Not InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
951442cdf08367ffa67b344743289167d2bc28bb Apalache Not InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
d9f40d89306f0b401c7dfb073614c768d84736b2 Apalache Not InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
25bed91170bb8e22d14503671762d2210788d52c Apalache Not InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
e4270e413ce5ec66ba5ea41f1a570745799bb02e Apalache Not InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
f3131638869f25af878573436326ffe73bdf6946 Apalache Not InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
cf3ef4446dd5c109a363795824bb22d2d07434de Apalache Not InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
1b36f09e34b21a8a37ac19bff458b899994f52c5 Apalache Not InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
cb54af746045b1ac0de7d690cd70b017a00ee4ad Apalache Not InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
d731fd65279bdee79c5e5be7ae5ddc7a7f704092 Apalache Not InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
afb631b6f4cb4d7ece57b8851670d3d95aaffaf8 Apalache Not InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
4d6b020537dc8708774495fa228e2f3d5bc1ab0d Apalache Not InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
787a4c9535ca7a7482c0756af13595a06f32fda4 Apalache Not Enabled True Passed
  • Model Under Test
  • Equivalent Model
3fea92155647da726e56e6d1a196dfe2bc9a2cd1 Apalache Not Enabled False Passed
  • Model Under Test
  • Equivalent Model
03a640d76c7722ef979ed4499846722132aaf550 Apalache Not SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
962eaf3f81ad12faaf9e3b760ba90e7964e2af77 Apalache Not SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
944a31b263af64efc5c82fd5d9f737efa0c0da81 Apalache Not IfCond True Passed
  • Model Under Test
  • Equivalent Model
125769fe2f70c8efdf61659ac4dc89d24d31cc7b Apalache Not IfCond False Passed
  • Model Under Test
  • Equivalent Model
51bdd4f1aad50d556a846b9dae29630e4c68a79f Apalache Not IfThen True Passed
  • Model Under Test
  • Equivalent Model
d4521746d8ab84aab0bec60f7a77f8ac2c9a5a7e Apalache Not IfThen False Passed
  • Model Under Test
  • Equivalent Model
22dda7daf5a0a323933edff0d63d0ddbc992e037 Apalache Not IfElse True Passed
  • Model Under Test
  • Equivalent Model
fa0ad76c47850ccff4b984317b5d543f6f8e11fc Apalache Not IfElse False Passed
  • Model Under Test
  • Equivalent Model
ef70d74dc75afc5faae440cee6de2905a8f3e618 Apalache Not Unchanged True Passed
  • Model Under Test
  • Equivalent Model
74d3c9dee5c8b22faca222f343cec46ab4d1b30a Apalache Not Unchanged False Passed
  • Model Under Test
  • Equivalent Model
5edc6a31c5ab2c32beb8c46861518087a74e94c6 Apalache Not Equivalence True Passed
  • Model Under Test
  • Equivalent Model
54eaa65d8c5b1446ef8a10444e4f76562caf436b Apalache Not Equivalence False Passed
  • Model Under Test
  • Equivalent Model
46d341f198a078d376f09babe49386c5429b3a3b TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Not TlcEval True Passed
  • Model Under Test
  • Equivalent Model
183fc80552eeba56ce7d8dcb75bef58d6ea97a4a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Not TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b700e6f3d9f1b62a91a4b64682498fa56f4999e6 Apalache Not BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
84aaa221832734a338785a2cb8a1f73c4dffdbc8 Apalache Not BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
340e39e31c8b913cc759cae9fb6f0f7a3bd577c3 Apalache Not BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
007f7c50786a8b42cae0e1be2b73f3f798fe0e08 Apalache Not BagSubsetEqBag False Passed
  • Model Under Test
  • Equivalent Model
bc37527d552f3e7a88bf2e4b5c0b36ae789ce9e0 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)
Not FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
f8583b3e8d953445dde1aa0c8a2336bddf98e926 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)
Not FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
295cee2f26dbf4f56610b92afda6c057679aebc4 Apalache Not SeqHead True Passed
  • Model Under Test
  • Equivalent Model
f4c53ab4ba441083595d5e8af1934a5d7d5bddc3 Apalache Not SeqHead False Passed
  • Model Under Test
  • Equivalent Model