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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
37c60fedb6251c307ca19c0f978e899f1819ec44 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
InstanceNamedWithInFolder OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
66c11570899f15bdd9da6deee8877ca944a84340 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
InstanceNamedWithInFolder OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
900cd892e3795f6ff56f350e14a6a03b1baa46a9 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
InstanceNamedWithInFolder MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
96596de6ec41ef89bce3494e52693abfce614cbe TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
InstanceNamedWithInFolder MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
38be08329c565aeaec1f2b60dc66bb4db27d1da8 Apalache InstanceNamedWithInFolder BoolTrue True Passed
  • Model Under Test
  • Equivalent Model
896defee2259a14e541db1ba0ff31ada335813e9 Apalache InstanceNamedWithInFolder BoolTrue False Passed
  • Model Under Test
  • Equivalent Model
768a805373df47d68afffb1905a8f83961cc83c7 Apalache InstanceNamedWithInFolder BoolFalse True Passed
  • Model Under Test
  • Equivalent Model
5bbdce123db6963611d6e0741f7ae4ba06a7e871 Apalache InstanceNamedWithInFolder BoolFalse False Passed
  • Model Under Test
  • Equivalent Model
c3db8d986042aa0dbc5d971f16142f8aaa20a514 Apalache InstanceNamedWithInFolder BoolSet True Passed
  • Model Under Test
  • Equivalent Model
1c969b0b6b0d01fec6536946da29ec7d987971ab Apalache InstanceNamedWithInFolder BoolSet False Passed
  • Model Under Test
  • Equivalent Model
8d73f79d81ed5d930eab4554ce212b014bdda45f Apalache InstanceNamedWithInFolder And True Passed
  • Model Under Test
  • Equivalent Model
5a97138821d3ea8faa62893100d0586c61c7ba0a Apalache InstanceNamedWithInFolder And False Passed
  • Model Under Test
  • Equivalent Model
8c08e3b2ec449f6dbf03c7dbaa5f0c3f1be19b35 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedWithInFolder AndMultiLine True Passed
  • Model Under Test
  • Equivalent Model
00689f02984de5e4e77a018e564f9efa05e5b0cb TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
InstanceNamedWithInFolder AndMultiLine False Passed
  • Model Under Test
  • Equivalent Model
2076a61daf1448f3bab7cffb021e1aadbd767f26 Apalache InstanceNamedWithInFolder Imply True Passed
  • Model Under Test
  • Equivalent Model
078dd6c8a3caec208cc221ccb1ff3f8fc8884da8 Apalache InstanceNamedWithInFolder Imply False Passed
  • Model Under Test
  • Equivalent Model
486536447f0e26c3e46442617755cbfbd9a8b9d6 Apalache InstanceNamedWithInFolder Not True Passed
  • Model Under Test
  • Equivalent Model
cdf6de2ea742c1bc18917101e09b2703e5fca252 Apalache InstanceNamedWithInFolder Not False Passed
  • Model Under Test
  • Equivalent Model
532a47f513f605ad307cbdb3b122cf75392c30f4 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedWithInFolder Or True Passed
  • Model Under Test
  • Equivalent Model
5602698e722e59a2dde6c42b4893d4fa803ff769 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
InstanceNamedWithInFolder Or False Passed
  • Model Under Test
  • Equivalent Model
fed7dae33296b23a6495a7e4bd6896d52057f113 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedWithInFolder OrMultiLine True Passed
  • Model Under Test
  • Equivalent Model
5064009770321e000f8499eabe84ccf6ce74f7a4 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
InstanceNamedWithInFolder OrMultiLine False Passed
  • Model Under Test
  • Equivalent Model
a13ab54de55c0a78afabce121fd5d9075b1795ba Apalache InstanceNamedWithInFolder AndProp True Passed
  • Model Under Test
  • Equivalent Model
c52200d425146ae067a8899d5deb3edf24414189 Apalache InstanceNamedWithInFolder AndProp False Passed
  • Model Under Test
  • Equivalent Model
df8a8afaccb442ccb643cee241d9ac8daa2aa4d9 Apalache InstanceNamedWithInFolder Boxed True Passed
  • Model Under Test
  • Equivalent Model
2ebf13488a0d8422d34fc28af9466daae170dd65 Apalache InstanceNamedWithInFolder Boxed False Passed
  • Model Under Test
  • Equivalent Model
41ba97f96a477a196beb36c4e5abaa0ec1c009a8 Apalache InstanceNamedWithInFolder Eq True Passed
  • Model Under Test
  • Equivalent Model
540d0c089679b730b32d470ed4a34a007974f585 Apalache InstanceNamedWithInFolder Eq False Passed
  • Model Under Test
  • Equivalent Model
2096b546db226cad9f01747bc0eb401f3eb815d8 Apalache InstanceNamedWithInFolder Ne True Passed
  • Model Under Test
  • Equivalent Model
1f80480dd7d9da14f9c4289c1ee33c8c174f13f4 Apalache InstanceNamedWithInFolder Ne False Passed
  • Model Under Test
  • Equivalent Model
c125e747229df03dddbe9b01ee29749d00ad5a8c Apalache InstanceNamedWithInFolder Let True Passed
  • Model Under Test
  • Equivalent Model
be1d28ee067b873c5408588687ac221778818cf2 Apalache InstanceNamedWithInFolder Let False Passed
  • Model Under Test
  • Equivalent Model
7c6698e168bed6cc0827877efa4568a0838b0075 Apalache InstanceNamedWithInFolder SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
e952dcbbdd1297ecbf52f83226b8907259823d24 Apalache InstanceNamedWithInFolder SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
7f6553d0c12d4851ae6ba2fdf73b44989c176be5 Apalache InstanceNamedWithInFolder Set0 True Passed
  • Model Under Test
  • Equivalent Model
aa11e0544d2048dc4c657c82e64a2de90a18ecb6 Apalache InstanceNamedWithInFolder Set0 False Passed
  • Model Under Test
  • Equivalent Model
c95ad536714a6df2d7e5f0a69f230b8da59b1a5f Apalache InstanceNamedWithInFolder Set1 True Passed
  • Model Under Test
  • Equivalent Model
ed81fd3f797eac096d94483ad1a1933f12843c7e Apalache InstanceNamedWithInFolder Set1 False Passed
  • Model Under Test
  • Equivalent Model
fe71850937e6e692358f1a46ab4205f1bbc52d0a Apalache InstanceNamedWithInFolder Set2 True Passed
  • Model Under Test
  • Equivalent Model
b7303ea0f093b5e32754cd5a1aa7568dd46936e4 Apalache InstanceNamedWithInFolder Set2 False Passed
  • Model Under Test
  • Equivalent Model
73aba66052f77e3eebeb134cb85313b2f8390ce7 Apalache InstanceNamedWithInFolder Fun True Passed
  • Model Under Test
  • Equivalent Model
d72e5959f6807aae54a62d22df8695e998f646e6 Apalache InstanceNamedWithInFolder Fun False Passed
  • Model Under Test
  • Equivalent Model
79a558b72a90f7c5879d4e4cdbdf813b5794b33a Apalache InstanceNamedWithInFolder In True Passed
  • Model Under Test
  • Equivalent Model
3a31ed015eff9aadb607520b5aee39cc7d3e0415 Apalache InstanceNamedWithInFolder In False Passed
  • Model Under Test
  • Equivalent Model
c11d7accc8e74a0fee2d53e3b1e8c7209c9fce65 Apalache InstanceNamedWithInFolder NotIn True Passed
  • Model Under Test
  • Equivalent Model
95c9b01eb2abc6d293a7dd8b73308919be240f4d Apalache InstanceNamedWithInFolder NotIn False Passed
  • Model Under Test
  • Equivalent Model
2f0dcc7e967480e5e17c0e7d10f8896f758b4081 Apalache InstanceNamedWithInFolder Exists True Passed
  • Model Under Test
  • Equivalent Model
ca77ec52133494836aaf3fcf4fa8f765cbdf414e Apalache InstanceNamedWithInFolder Exists False Passed
  • Model Under Test
  • Equivalent Model
403d5e3f1de97ff2dece75a56c4404854ff77226 Apalache InstanceNamedWithInFolder Forall True Passed
  • Model Under Test
  • Equivalent Model
b28ae973b5de90cb66fa648903ba3ef9fb870bdd Apalache InstanceNamedWithInFolder Forall False Passed
  • Model Under Test
  • Equivalent Model
6790ad306442febc54a7890a168c5d4ba5261ea4 Apalache InstanceNamedWithInFolder Choose True Passed
  • Model Under Test
  • Equivalent Model
9c1bba5003574438870964532fbef6bc8bc90cd6 Apalache InstanceNamedWithInFolder Choose False Passed
  • Model Under Test
  • Equivalent Model
47b045e3f84096687d200641d5582df65211c30c Apalache InstanceNamedWithInFolder Record True Passed
  • Model Under Test
  • Equivalent Model
d2701f55d9c016cd2200333f8b2bd549cb3c996d Apalache InstanceNamedWithInFolder Record False Passed
  • Model Under Test
  • Equivalent Model
f848444c04853c804dab91feac443ec13085e398 Apalache InstanceNamedWithInFolder Tuple True Passed
  • Model Under Test
  • Equivalent Model
2f73780cfe562f0a0a8f7f20ca2c1d2b2eb36b7a Apalache InstanceNamedWithInFolder Tuple False Passed
  • Model Under Test
  • Equivalent Model
6780860c707a3edf1cf9f186ee02b00f3d7fd634 Apalache InstanceNamedWithInFolder TupleEmpty True Passed
  • Model Under Test
  • Equivalent Model
c4ee4f8bbb9a8e2ea6c2aacc9f7404e3ccae1a74 Apalache InstanceNamedWithInFolder TupleEmpty False Passed
  • Model Under Test
  • Equivalent Model
a5029fd9355272b0931f650568c5050022576eef Apalache InstanceNamedWithInFolder FunApp True Passed
  • Model Under Test
  • Equivalent Model
cc147fa56c0d290f2cfe8e343732f8c396cbc653 Apalache InstanceNamedWithInFolder FunApp False Passed
  • Model Under Test
  • Equivalent Model
13b71f5c7948c6de6ab1f42bd85db98e2043bde1 Apalache InstanceNamedWithInFolder Prime True Passed
  • Model Under Test
  • Equivalent Model
ddc45b373c5f61a37ff8ec4e90239144750ddb06 Apalache InstanceNamedWithInFolder Prime False Passed
  • Model Under Test
  • Equivalent Model
d8c2f4d6bc3d3f767731e7dec795384b978011ad Apalache InstanceNamedWithInFolder NumZero True Passed
  • Model Under Test
  • Equivalent Model
99264b402b51d4eb8937603aa4c8ef02c7ea38f5 Apalache InstanceNamedWithInFolder NumZero False Passed
  • Model Under Test
  • Equivalent Model
4a77a2e9d16592efef83989dac4aa739fd105293 Apalache InstanceNamedWithInFolder NumOne True Passed
  • Model Under Test
  • Equivalent Model
3cd4724cec1f9bc81cc0b25a44f4df812b47af44 Apalache InstanceNamedWithInFolder NumOne False Passed
  • Model Under Test
  • Equivalent Model
8a40da5b428e5635113be8d47658dd7f03abba12 Apalache InstanceNamedWithInFolder NumMaxInt True Passed
  • Model Under Test
  • Equivalent Model
90e07c44ee90996d4952c09ea9418094f4dcd982 Apalache InstanceNamedWithInFolder NumMaxInt False Passed
  • Model Under Test
  • Equivalent Model
16a1c277e618320c4f1b0060cadbc559dbc438d4 Apalache InstanceNamedWithInFolder NumUnaryMinus True Passed
  • Model Under Test
  • Equivalent Model
5fc3400088b38197736e869dd4c0556795d4ba9b Apalache InstanceNamedWithInFolder NumUnaryMinus False Passed
  • Model Under Test
  • Equivalent Model
bd5c2c42ef743580c29de56924b401812b9dfb36 Apalache InstanceNamedWithInFolder NumPlus True Passed
  • Model Under Test
  • Equivalent Model
73e582da6004dce69b25c2e8f04fb76f17ffd405 Apalache InstanceNamedWithInFolder NumPlus False Passed
  • Model Under Test
  • Equivalent Model
d2163c5d12e9c50727546c47a9d0aad5e8876f62 Apalache InstanceNamedWithInFolder NumMinus True Passed
  • Model Under Test
  • Equivalent Model
bd2bb5f47b64472aabbaa3b2cb462784ff8c1ed9 Apalache InstanceNamedWithInFolder NumMinus False Passed
  • Model Under Test
  • Equivalent Model
c66689edd32ea2e0836edc6fe3e76a544c7fd317 Apalache InstanceNamedWithInFolder NumMul True Passed
  • Model Under Test
  • Equivalent Model
dc3942743cc1d21461afeb6532f82ab977ce5b4a Apalache InstanceNamedWithInFolder NumMul False Passed
  • Model Under Test
  • Equivalent Model
741b37a71eac2e22cf1b365f107ce8e258198d51 Apalache InstanceNamedWithInFolder NumDiv True Passed
  • Model Under Test
  • Equivalent Model
228c8412e4e75df5d81c9218d295aecf2aea2b8b Apalache InstanceNamedWithInFolder NumDiv False Passed
  • Model Under Test
  • Equivalent Model
90be98f9107b7bd90e44707cce92cfac51616eaf Apalache InstanceNamedWithInFolder NumMod True Passed
  • Model Under Test
  • Equivalent Model
702faeeb207b91f665f0f709054f88bee71d0e44 Apalache InstanceNamedWithInFolder NumMod False Passed
  • Model Under Test
  • Equivalent Model
c64884b274ff85815473593406fd72fea8c8164f Apalache InstanceNamedWithInFolder NumPow True Passed
  • Model Under Test
  • Equivalent Model
030beb51d3db538e94d56ad5c3f8c91a9784d659 Apalache InstanceNamedWithInFolder NumPow False Passed
  • Model Under Test
  • Equivalent Model
3a44ea0d5b6b75bf3c04669b467dd6cd7ff99152 Apalache InstanceNamedWithInFolder NumGt True Passed
  • Model Under Test
  • Equivalent Model
5b383a19340ffdff4d562e7928afc9b3f0188f17 Apalache InstanceNamedWithInFolder NumGt False Passed
  • Model Under Test
  • Equivalent Model
2fb6a6db4981cddfef0ee0b27d588060b2bb9e85 Apalache InstanceNamedWithInFolder NumGe True Passed
  • Model Under Test
  • Equivalent Model
14524d0ec3b98f606aeec47134a054df0abb1b12 Apalache InstanceNamedWithInFolder NumGe False Passed
  • Model Under Test
  • Equivalent Model
84aa84f8be39686640c98e766e0c26e6b8485cfc Apalache InstanceNamedWithInFolder NumLt True Passed
  • Model Under Test
  • Equivalent Model
f30b86f932f9a8671d70e089bea093396ee44358 Apalache InstanceNamedWithInFolder NumLt False Passed
  • Model Under Test
  • Equivalent Model
a1828a0a4242a3412321fc98e29eb2ca75b2c855 Apalache InstanceNamedWithInFolder NumLe True Passed
  • Model Under Test
  • Equivalent Model
cc3c8f15fc0afcae196cbbbb56b85e286f3935b2 Apalache InstanceNamedWithInFolder NumLe False Passed
  • Model Under Test
  • Equivalent Model
7a74a712f7a4bf3919813604a484ce87ba3cf4d1 Apalache InstanceNamedWithInFolder DefFun True Passed
  • Model Under Test
  • Equivalent Model
114d7c6a63b864ea70091893fe0626345ac21691 Apalache InstanceNamedWithInFolder DefFun False Passed
  • Model Under Test
  • Equivalent Model
9b5eeda26137fcb00c67fee0d5e766595f6c238e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDefFun True Passed
  • Model Under Test
  • Equivalent Model
fd57c9914323077b0224357e9087930f2edc0395 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDefFun False Passed
  • Model Under Test
  • Equivalent Model
ba321dac148f75167d57fac269c0731f25073aeb Apalache InstanceNamedWithInFolder DefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
19464527ad7b85fe45eb7d5e56d38bf8e30cb3ae Apalache InstanceNamedWithInFolder DefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
131d8172f308614fbe753d7ae7851abc0e490112 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDefFunRecursive True Passed
  • Model Under Test
  • Equivalent Model
859b6cd35ac648976ea7e42c288361a283dd589c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDefFunRecursive False Passed
  • Model Under Test
  • Equivalent Model
c1cd9e8d2931d29109068cf8ceaa43a379d86418 Apalache InstanceNamedWithInFolder Def0 True Passed
  • Model Under Test
  • Equivalent Model
b0edb551380338a9971130a553a916bbd1723000 Apalache InstanceNamedWithInFolder Def0 False Passed
  • Model Under Test
  • Equivalent Model
0ea164dfc6ec94d31d1dcadb0c6c9741377b37b5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
05f76cb89ff613ff0a161a38658723798af6d842 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
2b5c2c6c1b24bc4f97df3d94064fc45504092f8a Apalache InstanceNamedWithInFolder Def1 True Passed
  • Model Under Test
  • Equivalent Model
308131e76fc7faaaae35b33e53a1c1b2f6b9f8c2 Apalache InstanceNamedWithInFolder Def1 False Passed
  • Model Under Test
  • Equivalent Model
556d3e7c3d97df1766511fef5e718e2913727bd9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
886d1c8a321eaaf918ff03f8fb342448567093d9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
709b00c4deccd45b53ec19ab5d120f7194288f9f Apalache InstanceNamedWithInFolder Def2 True Passed
  • Model Under Test
  • Equivalent Model
1e94e55e9eecb60f40e1f1c8232b617ab70fb2e6 Apalache InstanceNamedWithInFolder Def2 False Passed
  • Model Under Test
  • Equivalent Model
75a971de47e45e0832f277653375b9783505cd9a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
bd649bf6cfd78fd61c45a6a1538726a512078bf8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
0352bd344ed5314c7674806134a499f572281982 Apalache InstanceNamedWithInFolder Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
501c48dfe004a38007b0ead3cbbee5de36e1497c Apalache InstanceNamedWithInFolder Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
99fdab9f0100964696e32eea7ba9b93f746ed4c5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
43986c4d852f081bbfcb638ae64f41942ed7f372 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
InstanceNamedWithInFolder LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
c7150976d93031246a3117c66b11e0d2804ff605 Apalache InstanceNamedWithInFolder Extends True Passed
  • Model Under Test
  • Equivalent Model
c7e6548d127723a5f278c2b684abe49cc86a55e3 Apalache InstanceNamedWithInFolder Extends False Passed
  • Model Under Test
  • Equivalent Model
519618c515c707e00c5b13b42d904d8db1ed7d06 Apalache InstanceNamedWithInFolder ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
f9d6baaf3624909fb5194df123101b8014a2ef6b Apalache InstanceNamedWithInFolder ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
8e513c03b5c4139e5d99b224bdcd6d895f331420 Apalache InstanceNamedWithInFolder Variable True Passed
  • Model Under Test
  • Equivalent Model
53ff769093cb29fd220055a2f44e1787734d3a4b Apalache InstanceNamedWithInFolder Variable False Passed
  • Model Under Test
  • Equivalent Model
f034acb7ad00341f2591d02cd9a312545f5d1e4d Apalache InstanceNamedWithInFolder Constant True Passed
  • Model Under Test
  • Equivalent Model
0510e9e02889c7dc4ffb4ac470276b665412ce63 Apalache InstanceNamedWithInFolder Constant False Passed
  • Model Under Test
  • Equivalent Model
c6ab66d82c4e1008698f261b982db659a5ef89c9 Apalache InstanceNamedWithInFolder ConstantModelValue True Passed
  • Model Under Test
  • Equivalent Model
3d1b81bb73c6414605cc86fe812091ba9aa9066a Apalache InstanceNamedWithInFolder ConstantModelValue False Passed
  • Model Under Test
  • Equivalent Model
a2f56b2b9a234dbc193b00eb92d31e3480f78eb0 Apalache InstanceNamedWithInFolder ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
2f7f4c38ba8144a563df474dd1f654ab466b72ac Apalache InstanceNamedWithInFolder ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
3d3c11c6f0cc8e0444c28bff875abde55e7510f7 Apalache InstanceNamedWithInFolder Instance True Passed
  • Model Under Test
  • Equivalent Model
c520f5e1466eadf6cf117a8299ffa1045c96c421 Apalache InstanceNamedWithInFolder Instance False Passed
  • Model Under Test
  • Equivalent Model
bca3ba95a974348c7c0f7fefc8a921c43fadbc39 Apalache InstanceNamedWithInFolder InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
e26aba6af7531e57884c4a067d4f68da6266ffae Apalache InstanceNamedWithInFolder InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
810936f8572b2faa8de5181b712a9067db0d7010 Apalache InstanceNamedWithInFolder InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
a3e8559714171f0267ebeb2b6fb3e22988d1165f Apalache InstanceNamedWithInFolder InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
c9bc752ca3d1974bdc33dece5408cb6477d18a76 Apalache InstanceNamedWithInFolder InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
a604f4c1346de3438d132df1e69c82353f2b2df1 Apalache InstanceNamedWithInFolder InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
dcd54b18881875bffc2a344aa21dda5652cd78c6 Apalache InstanceNamedWithInFolder InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
b863290fc92e58149f894be5d903b5a4a0f009aa Apalache InstanceNamedWithInFolder InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
5dfec5edeb753f82edebf673c2c0941ae063da07 Apalache InstanceNamedWithInFolder InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e0892b18cf2fa1c2ed74d2ab1180cb02ad753f71 Apalache InstanceNamedWithInFolder InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
722abf6583e89eae31911edc5f4d33ec9f7449bf Apalache InstanceNamedWithInFolder InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
d9c402aafab23248fb7576080538d1c7e860ea05 Apalache InstanceNamedWithInFolder InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
4bc8412a36fe196fb270cc56fd19b664eadb7922 Apalache InstanceNamedWithInFolder InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
4b120dbacb6ea66a3f576179eea1d21af07a3d3d Apalache InstanceNamedWithInFolder InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
659c4b75cd31d3fb769b4343914729302ec94c94 Apalache InstanceNamedWithInFolder Enabled True Passed
  • Model Under Test
  • Equivalent Model
e962da61340a864fcdf9b2ec3ae620e97fd8e7fb Apalache InstanceNamedWithInFolder Enabled False Passed
  • Model Under Test
  • Equivalent Model
18f659a24fb591457acf0352c1ee7e441a1f0743 Apalache InstanceNamedWithInFolder Cross2 True Passed
  • Model Under Test
  • Equivalent Model
3767fc15ecf75061580407a3643691bd39eec501 Apalache InstanceNamedWithInFolder Cross2 False Passed
  • Model Under Test
  • Equivalent Model
d327ed56c41d0c066e3ef78f0bac5a7cf28a1d64 Apalache InstanceNamedWithInFolder Cross3 True Passed
  • Model Under Test
  • Equivalent Model
855807b0e199cfef1758334f2dae95126d42b55a Apalache InstanceNamedWithInFolder Cross3 False Passed
  • Model Under Test
  • Equivalent Model
8271fff688d4c495bd6af436fce868b5897f0111 TLC with reduction strategy:
  • Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
InstanceNamedWithInFolder FunSet True Passed
  • Model Under Test
  • Equivalent Model
4aeb579f60151d95791080f28e3495daea93c8d7 TLC with reduction strategy:
  • Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
InstanceNamedWithInFolder FunSet False Passed
  • Model Under Test
  • Equivalent Model
70a1138dccb35f02069b72aff44f84ab97570c42 TLC with reduction strategy:
  • Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
InstanceNamedWithInFolder RecordSet True Passed
  • Model Under Test
  • Equivalent Model
bea8580fa52e533510ffbd3394d3690e742ac563 TLC with reduction strategy:
  • Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
InstanceNamedWithInFolder RecordSet False Passed
  • Model Under Test
  • Equivalent Model
6c94e23024d22cffcb37bbc21ef96257a2c1fb14 Apalache InstanceNamedWithInFolder SetDiff True Passed
  • Model Under Test
  • Equivalent Model
834e280ff935c78c11d50a451f80ca3446c0baef Apalache InstanceNamedWithInFolder SetDiff False Passed
  • Model Under Test
  • Equivalent Model
70284b4eac9ad3d59109fb17687a963d69c6ee6d Apalache InstanceNamedWithInFolder SetUnion True Passed
  • Model Under Test
  • Equivalent Model
bce98ba21aae95740c1b61897d29ed5116dbf362 Apalache InstanceNamedWithInFolder SetUnion False Passed
  • Model Under Test
  • Equivalent Model
4d9af4193bf00778014c18576b2d4c62cae26c36 Apalache InstanceNamedWithInFolder SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
20c17ff5e1b0694168b9d27e2197a14f93eef9e3 Apalache InstanceNamedWithInFolder SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
d06877a58cc350d4969a417b648ec00362b86b70 Apalache InstanceNamedWithInFolder SubsetEq True Passed
  • Model Under Test
  • Equivalent Model
fc2d667859f60fcff7f1a33cae1b66081e7b9fb1 Apalache InstanceNamedWithInFolder SubsetEq False Passed
  • Model Under Test
  • Equivalent Model
57dbb30a8830a74ab81a91cfef09a7cb600770c9 Apalache InstanceNamedWithInFolder IfCond True Passed
  • Model Under Test
  • Equivalent Model
8cb1eb259d03cb66d72c10a048cc1aa93e3e0244 Apalache InstanceNamedWithInFolder IfCond False Passed
  • Model Under Test
  • Equivalent Model
a053d1893039c1e6da188758bceaf51125a3f76e Apalache InstanceNamedWithInFolder IfThen True Passed
  • Model Under Test
  • Equivalent Model
f10369d63da8a38d80dca3b3a20c05767edff73f Apalache InstanceNamedWithInFolder IfThen False Passed
  • Model Under Test
  • Equivalent Model
da3e2d09eda69739dda329e8c75b08544576c762 Apalache InstanceNamedWithInFolder IfElse True Passed
  • Model Under Test
  • Equivalent Model
fa210d81aa06076419d803d708c2149cfaed1781 Apalache InstanceNamedWithInFolder IfElse False Passed
  • Model Under Test
  • Equivalent Model
9bf8af9e7ba23ccc0c84f2931ce35451044f8321 Apalache InstanceNamedWithInFolder Subset True Passed
  • Model Under Test
  • Equivalent Model
1c7cbd16e6476bf48e70ad590dac645cd49acb53 Apalache InstanceNamedWithInFolder Subset False Passed
  • Model Under Test
  • Equivalent Model
c7e881bb198ef0a5c204a17d2bad5d52c0d3d5c1 Apalache InstanceNamedWithInFolder Domain True Passed
  • Model Under Test
  • Equivalent Model
bf89382248bc8e06d617561c9100987f83f09c50 Apalache InstanceNamedWithInFolder Domain False Passed
  • Model Under Test
  • Equivalent Model
1bbdeb0e4bf8b77fe961a82190ed25c6fdc7414e Apalache InstanceNamedWithInFolder Union True Passed
  • Model Under Test
  • Equivalent Model
71da149f58a97d4cfa89c47be5bd3d3a96c7366c Apalache InstanceNamedWithInFolder Union False Passed
  • Model Under Test
  • Equivalent Model
6325a9b5321e70aafa984fbae08282e20358ce10 Apalache InstanceNamedWithInFolder Unchanged True Passed
  • Model Under Test
  • Equivalent Model
84cd102d013e2f72acc0de416ce15af5b811c29a Apalache InstanceNamedWithInFolder Unchanged False Passed
  • Model Under Test
  • Equivalent Model
8592c75280957eacc6b729b98d788698c7dfd55b Apalache InstanceNamedWithInFolder Equivalence True Passed
  • Model Under Test
  • Equivalent Model
e3b6e4764bd3c60c2579e36cee04c98c9eff3b73 Apalache InstanceNamedWithInFolder Equivalence False Passed
  • Model Under Test
  • Equivalent Model
58affb382e1f7d45ed307e72cbf7136d9b627f64 Apalache InstanceNamedWithInFolder StringEmpty True Passed
  • Model Under Test
  • Equivalent Model
665d34d6e15b9ac64b1de714c18a0b033bcfda86 Apalache InstanceNamedWithInFolder StringEmpty False Passed
  • Model Under Test
  • Equivalent Model
4c79abc2a738bbef7ec0c8c16098fa0ae7799e88 Apalache InstanceNamedWithInFolder String True Passed
  • Model Under Test
  • Equivalent Model
23b09164146186fef04c31459bb312d923e6ff30 Apalache InstanceNamedWithInFolder String False Passed
  • Model Under Test
  • Equivalent Model
a6d6277f3ea1e94169f104ad80330b5fa32da1d9 Apalache InstanceNamedWithInFolder SeqLen True Passed
  • Model Under Test
  • Equivalent Model
4b7e1e670839b39d3d7fca75f219e4391765ecb8 Apalache InstanceNamedWithInFolder SeqLen False Passed
  • Model Under Test
  • Equivalent Model
c4b5447047949773977d04fa0720b4d24ea65ee6 Apalache InstanceNamedWithInFolder SeqConcat True Passed
  • Model Under Test
  • Equivalent Model
faf5c002fd72c36af71dc640b2d48f0da8bf3fa9 Apalache InstanceNamedWithInFolder SeqConcat False Passed
  • Model Under Test
  • Equivalent Model
32164d0e93dc9b01428f174dade7f9492c62e3f1 Apalache InstanceNamedWithInFolder SeqSelectSeq True Passed
  • Model Under Test
  • Equivalent Model
17de8a2578cbf949d845d6b71310b6881eca0088 Apalache InstanceNamedWithInFolder SeqSelectSeq False Passed
  • Model Under Test
  • Equivalent Model
325e2d98f0ab3d9d6e7c5320e519552c6c0ee77e Apalache InstanceNamedWithInFolder SeqSubSeq True Passed
  • Model Under Test
  • Equivalent Model
5e134335242ba1dc8454db24076bdd94cf6ec02a Apalache InstanceNamedWithInFolder SeqSubSeq False Passed
  • Model Under Test
  • Equivalent Model
1db2b2b2303c60d225901bb54e45e49d5bdef1b6 TLC with reduction strategy:
  • Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
InstanceNamedWithInFolder NumRange True Passed
  • Model Under Test
  • Equivalent Model
3a2ca3b18aafe52e0d4abccf270c5b2ac8e50830 TLC with reduction strategy:
  • Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
InstanceNamedWithInFolder NumRange False Passed
  • Model Under Test
  • Equivalent Model
8725d9c1a697f3204940733e9e63e28a1db1122a TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedWithInFolder TlcSingletonFun True Passed
  • Model Under Test
  • Equivalent Model
473b79ad8740b0910d5f503afa45fad442cc4337 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
InstanceNamedWithInFolder TlcSingletonFun False Passed
  • Model Under Test
  • Equivalent Model
8b01f9c3e1ec42b6799c365a0e1e0b2829c8f765 TLC with reduction strategy:
  • Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
InstanceNamedWithInFolder TlcExtendFun True Passed
  • Model Under Test
  • Equivalent Model
b4542c7ce705bdd559536202f1cf7dea24d6ca18 TLC with reduction strategy:
  • Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g |-> IF u \in DomF THEN f[u] ELSE g[x]]
InstanceNamedWithInFolder TlcExtendFun False Passed
  • Model Under Test
  • Equivalent Model
af9af71d1b9b7a705ee0051471a99f2d720bfe20 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedWithInFolder TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
8d13913dbffd983e979bc826926a498148a12a1a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
InstanceNamedWithInFolder TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
72a16bf6f6f61db0fa86d09951e3243f6780f44a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedWithInFolder TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
28e52312bd6ccf4ecd80e2b68ad0b91a0ce5316d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedWithInFolder TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
88309d0cd53ecb23518b52781205c865443cfdc1 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedWithInFolder TlcEval True Passed
  • Model Under Test
  • Equivalent Model
5dc1e63ff30fe11f34b5d8eae0a199d077209f87 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
InstanceNamedWithInFolder TlcEval False Passed
  • Model Under Test
  • Equivalent Model
aaca363cce4eb116a34e4ba4ed7e25f69622b1b4 Apalache InstanceNamedWithInFolder BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
9db2bd221dfecbbabb228e03228cc5bd73d96ff7 Apalache InstanceNamedWithInFolder BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
32b5d8c9264ffb6fa412c2cdef4315f9d0a60320 Apalache InstanceNamedWithInFolder BagSetToBag True Passed
  • Model Under Test
  • Equivalent Model
da6f20e3fd7c5ad837b22da11837c8ace405b42f Apalache InstanceNamedWithInFolder BagSetToBag False Passed
  • Model Under Test
  • Equivalent Model
268f24e1ddffb119e010ba7ad2ed4dd06870421e Apalache InstanceNamedWithInFolder BagBagIn True Passed
  • Model Under Test
  • Equivalent Model
5ee710c0f8ce705b398cbee97d1e7c69a2fdcaf1 Apalache InstanceNamedWithInFolder BagBagIn False Passed
  • Model Under Test
  • Equivalent Model
de79d77dd7096eb5c2927712861eb8d510a67f1a Apalache InstanceNamedWithInFolder BagEmptyBag True Passed
  • Model Under Test
  • Equivalent Model
09f01f27d1430f93eebaaf2f6d7e6005f8b5a89b Apalache InstanceNamedWithInFolder BagEmptyBag False Passed
  • Model Under Test
  • Equivalent Model
c1b9621cc5db95862ab6c15d190168ce8c6a8256 Apalache InstanceNamedWithInFolder BagAddBag True Passed
  • Model Under Test
  • Equivalent Model
b4b092288fad02635ba7aa1ef58c138dc1ad4927 Apalache InstanceNamedWithInFolder BagAddBag False Passed
  • Model Under Test
  • Equivalent Model
18c22880e30199a91739089b824928f9128d2735 Apalache InstanceNamedWithInFolder BagBagSub True Passed
  • Model Under Test
  • Equivalent Model
8da64cd1838c8ad3b2fd144b9208466e25419ed9 Apalache InstanceNamedWithInFolder BagBagSub False Passed
  • Model Under Test
  • Equivalent Model
691762633f4aa070a9e2408160e61080a427a6d0 Apalache InstanceNamedWithInFolder BagCopiesIn True Passed
  • Model Under Test
  • Equivalent Model
22418e4a1a875502c5e0040718701a3e741a4eea Apalache InstanceNamedWithInFolder BagCopiesIn False Passed
  • Model Under Test
  • Equivalent Model
b24f79d268760cf2d0ad618425a2f7ed629ba8c0 Apalache InstanceNamedWithInFolder BagSubsetEqBag True Passed
  • Model Under Test
  • Equivalent Model
0c0008ec143b95eeb77333bcac21e1f15e150bee Apalache InstanceNamedWithInFolder BagSubsetEqBag 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
4cf186baa6e2c4d28fd6f71799c78d8a04d18f6a Apalache InstanceNamedWithInFolder BagBagCardinality True Passed
  • Model Under Test
  • Equivalent Model
680829a1c592f37cef10a3f535fc12f607d5ff9d Apalache InstanceNamedWithInFolder BagBagCardinality False Passed
  • Model Under Test
  • Equivalent Model
c4d23432941d694a97a1a206e94dd4ea11df6581 Apalache InstanceNamedWithInFolder BagBagOfAll True Passed
  • Model Under Test
  • Equivalent Model
912e55e2d8383e9039a8519b556976cfa850f3be Apalache InstanceNamedWithInFolder BagBagOfAll False Passed
  • Model Under Test
  • Equivalent Model
caf102dc1e6962effc4795ffbd380c3b0e8cdfef TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedWithInFolder BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
2fb7c2f7a78f2fa2ac895998c1528f39794b8a6c TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedWithInFolder BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
bc280fb41206e6009441dbe95783947c66910035 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)
InstanceNamedWithInFolder FiniteSetsIsFiniteSet True Passed
  • Model Under Test
  • Equivalent Model
4f21433339461686d86ac170757e01ce5ac72ebd 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)
InstanceNamedWithInFolder FiniteSetsIsFiniteSet False Passed
  • Model Under Test
  • Equivalent Model
7d4686a1a8b2b96514151f9a0ab51d54af6c85b4 Apalache InstanceNamedWithInFolder FiniteSetsCardinality True Passed
  • Model Under Test
  • Equivalent Model
dada92ebfca79379c9c100013054e14265de1d02 Apalache InstanceNamedWithInFolder FiniteSetsCardinality False Passed
  • Model Under Test
  • Equivalent Model
17c4dab18b4f21fca5dd8c059536026394528fef Apalache InstanceNamedWithInFolder SeqHead True Passed
  • Model Under Test
  • Equivalent Model
6a74b29a5ea61170c213b0e08cc61e1937fcfc7d Apalache InstanceNamedWithInFolder SeqHead False Passed
  • Model Under Test
  • Equivalent Model
1e31130c489790c069a62f885ad58be99810f766 Apalache InstanceNamedWithInFolder SeqTail True Passed
  • Model Under Test
  • Equivalent Model
c767c5b7038780363dc3dcf2d5a6aea55619ab60 Apalache InstanceNamedWithInFolder SeqTail False Passed
  • Model Under Test
  • Equivalent Model
d551939ea081809e97d50a5d9ac1f56ee3df7a07 Apalache InstanceNamedWithInFolder SeqAppend True Passed
  • Model Under Test
  • Equivalent Model
697568aea1eed7ac05d9906344eb59029d8457a3 Apalache InstanceNamedWithInFolder SeqAppend False Passed
  • Model Under Test
  • Equivalent Model