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 plug feature BagBagUnion; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
3e7adadcaf9a4e2af5e8b511a9fb219868f90159 Apalache Eq BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
0cced50e6052405e0ff65b81c61f052659259e4f Apalache Eq BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
9698220d5f1fb99526ed81a6d38acc5e3281e517 Apalache Ne BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
811ea012e96dc6b73e2fb1fbccf4067aeacc96fd Apalache Ne BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
24c0d556ba634efa0faaa6a1404abbfc49182980 Apalache Let BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
23aea2b29a99e01f895397c296c135efeb1f65a4 Apalache Let BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
da31de903ca2ace4b6cac8d275393f284bb7624a Apalache Set0 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
3a586c38b220c3d8483b6660377434fc3ff8728b Apalache Set0 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
e7ff54ccab9b3e0282fd8da5a07c89453a9e2551 Apalache Set1 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
c6bd50156027d291e3e515960c3e752013889641 Apalache Set1 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
ea63dbb269ba21b0ee1dadfdf39f7f01002b4167 Apalache Set2 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
a4f63f8caa338f17c89f6e766e3252df83c39a03 Apalache Set2 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
17edcd64973c395f9d50ac1f9d877a686438471c Apalache Fun BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
ed751897ca557ac1be6ef30527446ee32b7064ab Apalache Fun BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
4d7d567d46fe77ac36a499d199d48b4072cf6930 Apalache In BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
23b4fae496ee96db87772223780bf2dcb3b85818 Apalache In BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
feb49a590a1907b507c9f4a27bf1f780ebcc1a12 Apalache NotIn BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
0fd94f589d2cb0aa694db448ae9ebfef713ba9ab Apalache NotIn BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
0459517802ea5a3add21c728c90e3cf50c17eb8f Apalache Record BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
12cb1a69306c2ce7e1c4564901150efafad76f9c Apalache Record BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
a5cd5f06f964f426f668ec8a517a2b3324a1819d Apalache Tuple BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
c3a491ec845099f963e188332f3061de6cb87295 Apalache Tuple BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
cd5a8e7ffeec96d776f655037b92b23f63e60947 Apalache FunApp BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
3ee83fd3e25d12a1812837579e8a59720843e2c5 Apalache FunApp BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
c129a0be954ddd87237db4821152941312bc5b1f Apalache Except1Fun BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
50dcb89961d61d83c68603a6104ae834341c39e8 Apalache Except1Fun BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
3ebf77281bd10cf6f185846a81f8476a4ba36433 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
f64a25351512644a47021b39387d602d9b656f29 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
2e25a6e5af6f6cfb9b41d6363c0dd5c1fb4e40ae Apalache Except1Rec BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
d4328d17e337bce6b5b02b96d7b1d9e3af103c18 Apalache Except1Rec BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
745d84370292fb182f7d2fcc849045fb66d04eb7 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
5ec2062275efb51d964f2bf57561e0b4a0c8f768 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
e835306dcf9195a290b767c4acca2b013b8b3b4c Apalache Except2Fun BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
bd7a6e463234d09309d915de18e02951a57934f3 Apalache Except2Fun BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
fa27784bf29e51c5f452444a52c2051381c05c2d Apalache Prime BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
6c5ddb645eea96da673e338f1e2a303c7124b5ca Apalache Prime BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
c7fe0f86277d3c219d977ee43eb7a0d28b6e16a4 Apalache DefFun BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
a3d01f1b1d31fd72deb1d6b3d93def9322496a2b Apalache DefFun BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
f9e8b132d2dbe748158dfcc1a649bacebdc6bb41 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
285d35a3d65085d0822292d1ab0948c70ebcc67d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
e8b9a81642e999105368096acef510d2d4a16594 Apalache DefFunRecursive BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
5d867656d1ff53fd45fd7f91f7906daef7482403 Apalache DefFunRecursive BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
9ea01c0fc2e540fd38e30194fa6a0fe9477c5088 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
a4f9aac4ae8f6f0c30424ae7195883edbe06eab7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
2be703f794e5453ab58afdda1b25842a4b4e4854 Apalache Def0 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
c4b2880242f6235de412eff8d40e7fdff2615fbd Apalache Def0 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
fca62a2cd3f484b1ededc6740b62392f11587893 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
4c7efaa859f3d7a9de967018c3befc48a08b3f88 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
471b536e6f21a40a8b0249a285aaa2383e3398c2 Apalache Def1 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
6ed6c2a156a592f3fa6e65b03a694af699734938 Apalache Def1 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
471ef9e3d0f98a7c2c8ca9091e4f6f74bf32c6ce TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
b4f758cefae2a382723847526cb3479662c0638d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
8f3cf1a04409842750b15b0ba6f0bbcde4ff2aa0 Apalache Def2 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
889fcf52483cd9b31f1aab78b34a240975a82c14 Apalache Def2 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
ad47f0a63bd6cb03c8d970c6c10efed46e5ab821 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
379b2509cfac85de5bf80faf7c9537ef8b74e09d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
db64182d14a08568215935110e60a08bb75b328f Apalache Def1Recursive BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
7595766e1c6f3059a7b994da463d3ceb92f7e943 Apalache Def1Recursive BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
f973e4ae57f3f78f7a27c3ef9c9b886e64a77768 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
b0a93882cc6e29c5d0c131dd7df6c4b087e4f44c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
16c9e2ecf63d945ec527004990179c2f79dd0cdb Apalache Extends BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
79872fde454c1b86ff81843c00852d4393c36042 Apalache Extends BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
0d45fc707f7b78d7324ed671d96f9c4e48ba68ca Apalache ExtendsInDifferentFolder BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
68b6c71ad9a36d6e596688c4eb07652b3ae78b75 Apalache ExtendsInDifferentFolder BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
cb2fd141034e7d106d423ffbdfe11fc492715a79 Apalache Variable BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
18a3a6416e7cf23d8e0690eafb814626aa224154 Apalache Variable BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
15d5d6f6d388cebb2c40dac509148743ff077b86 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
17e4af37480d515436f0623159a35203f3eb4b83 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
67d5dfb8eb7f190867386cfcadeccb66556fd325 Apalache Constant BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
adba8dd8bf1f334919822b3087a6de3d0cb6b921 Apalache Constant BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
f5c80d09f80e372338e60374f50eb470f3af0af5 Apalache ConstantRank1 BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
02f1e320b11bbafcb3275737049681171dffae4a Apalache ConstantRank1 BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
6f667938038e6ec84c163432e024cdb2dca4ab8e Apalache Instance BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
6de84ee0918d2b90f43017263ad9bc2545ffcd87 Apalache Instance BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
78b138cd8cdecabd828fb100798613288eecb193 Apalache InstanceWith BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
b96222a250e2c910219d8558fa7f8bb7890d604c Apalache InstanceWith BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
ac26abf3b93062dda35e3b9bfae7cbfe1e103b00 Apalache InstanceNamed BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
09babfd766f5fd2c455407644344eae3dff91569 Apalache InstanceNamed BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
54f6c1254a38b61c5ad71e9ee15691f16435c3e0 Apalache InstanceNamedWith BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
db9a057e06f505c1a12ede36a40204a3e1f51cd5 Apalache InstanceNamedWith BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
b828c514262af2cd2fcd56f06c9716cd62935071 Apalache InstanceInFolder BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
9f10910a31657321b0ca2591b61e1cc9f1404aae Apalache InstanceInFolder BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
b1cafd6767ac43d64fe99147dfd23f4e4eabf0d6 Apalache InstanceWithInFolder BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
24e148e7e507d301df883a1b706c936fda71655d Apalache InstanceWithInFolder BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
86ebe6fe5d786f401484b2d2617322c3d3fbaea8 Apalache InstanceNamedInFolder BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
79fa0d11653536ab306278c84d94253e01d2d797 Apalache InstanceNamedInFolder BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
b5c6768b30d35377bd08695db0f4f6b612f1c8b6 Apalache InstanceNamedWithInFolder BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
cc2852332e69dce9630a717e45bb03dec56d8ea8 Apalache InstanceNamedWithInFolder BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
5b728aac08f5a3b58deb68f7ec1cf12b1f4faff1 Apalache Lambda BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
e4fb27e48a68ee231b8d6caf31bd8335d91356c5 Apalache Lambda BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
4a8fd92e7e0a99f7a5d075b411fe6595ab786dba Apalache IfThen BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
03f7e8a651886ec8cdf1dcb1df5ef3e7fb2d14b8 Apalache IfThen BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
4eea4da431132bc91b45acec631565ae4b6b1d24 Apalache IfElse BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
b01a9f13af19e9ea2a72b740e78d134e97892954 Apalache IfElse BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
4fbcd1893d012e11b3776e105ac391a20699dfec Apalache Unchanged BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
cee437dc20c8f874cb9772580f1070672f6b900f Apalache Unchanged BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
62366dff444779d4a2e7bc4953b58730cb1c8d7e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
81b70a8f693f47abec9b0472cad85fe4f7b10263 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
e8e15466f13ba8dbe69f5ccf355bf39bffeb898b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
ac6533761865ec19939312660708cd20e61070df TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
af41a9e8a814c7abd8ecb81c792a32623e98d778 Apalache BagBagToSet BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
233015371427978a1c9bd99449d64f9941ef43ba Apalache BagBagToSet BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
8e6c7abf6278b47cf352ceccf18c8a00c056cb0c Apalache BagBagIn BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
a08d6f899de4549907eb14d810832404a306de53 Apalache BagBagIn BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
2c810e4a9d32b55694de9f57acb02c7ca16302a7 Apalache BagAddBag BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
4d979515229e4c9dd01ee9c3037631eecaf04300 Apalache BagAddBag BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
c278dd4970eeac928a3b4298b29ad286ce3f5d3e Apalache BagBagSub BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
9878345c3df0e1b0a8fd6df812219819183aec97 Apalache BagBagSub BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
de68b5a14e19f4552667cd6b001abb684b0c1b8a Apalache BagCopiesIn BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
0504b0e2c7c2c1a28053fa199307bd509b8d0600 Apalache BagCopiesIn BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
9bdd0c37bc49d0797a8f6d7ee430a2b7d5514796 Apalache BagSubsetEqBag BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
619b45b0ead0064f3c225097e51697c0f9227554 Apalache BagSubsetEqBag BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
06b2c5c1d31aa894d94189ea0a0a4b7414745219 Apalache BagBagCardinality BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
022fda6cad91fc27638f4bfed7af5f911c7e5bcb Apalache BagBagCardinality BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
5f5475c35ec8b7f99614714d5356569ea22a91db Apalache BagBagOfAll BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
ac6321009c8ecf38dde5400e19d8d1c7564838a7 Apalache BagBagOfAll BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
073747c3d8c9241ec81cfe3284c59efece2ad1c6 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
be933bb3accf7a1dc7d0f356ea7aba3d8433d198 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model
c9af470c124f21ec7b8323df718e63b078cd3c81 Apalache SeqAppend BagBagUnion True Passed
  • Model Under Test
  • Equivalent Model
03a6dc51e0ccfe28fe43db67239ba318aab66ec0 Apalache SeqAppend BagBagUnion False Passed
  • Model Under Test
  • Equivalent Model