Index

Tests by plug feature Prime; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b8fd3a9394214400d2e581905731de88264a501c Apalache And Prime True Passed
15682286b5323d157b3fb35656e604c40c39abda Apalache And Prime False Passed
a57e7fe5d0db9460f264941881bd3a570d39a5ed TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Prime True Passed
60d4299d5907a548a2a4b2f0185de9792c9fe3fd TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Prime False Passed
5c201d5768c4ae3cdcec1c8a9fe9f8a53a2af70d Apalache Imply Prime True Passed
0caa844e21455bb9a1aa1b63a48dc6b55a822ee4 Apalache Imply Prime False Passed
3dfed61c451f9c4ed1b62cc7ddcfec7d83fa62f1 Apalache Not Prime True Passed
8dbcebc70d0963cb6ad56aebeb49dff454fa12ac Apalache Not Prime False Passed
a1ed3bd37f329de61ecdc2bde84a143c79a074ba TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Prime True Passed
5b6eeb69c0b2c293230082e9dd54ebac6a2e3637 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Prime False Passed
ca25533eeb4b38baa53643ac8668a0c87eebd509 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Prime True Passed
bec6bb483bbe3c2a535d67e5b94d64d384303240 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Prime False Passed
ad42606209e55850cf2b9a2aa99ccd818f109dba Apalache Boxed Prime True Passed
4ce214492980ee32823fee5af6a49349cb527302 Apalache Boxed Prime False Passed
63600974cbb5cd4e06289882572808f550a2690a Apalache Eq Prime True Passed
91af409318633e11c1baa55490cb79005226ffa6 Apalache Eq Prime False Passed
129f150b3232c70b700710f8a12f4aa64d0bfcb6 Apalache Ne Prime True Passed
e785733c086bc4c483c8a13ca948ae52884f7a90 Apalache Ne Prime False Passed
fecb1c8c5bbfcf5e455f8bd2941bf294787427bd Apalache Let Prime True Passed
f4d648a5920cd0e3cec194dced5ccb1bba3d9e85 Apalache Let Prime False Passed
744d62474fa1aea30d06e0571f94efd9451b7158 Apalache Set0 Prime True Passed
484602886fdab596252b41868959306da6e4ca4f Apalache Set0 Prime False Passed
5a09d0b44db5d286b677ae5bba9a7def5d743f4b Apalache Set1 Prime True Passed
b2efff8c391c6679f4d86c2febabd7802e1ff000 Apalache Set1 Prime False Passed
c3a25c35562c83e2f8efcf3e8be3d04f92eeee35 Apalache Set2 Prime True Passed
3b754917419b81b751bcc7d93022bf0691c88ee7 Apalache Set2 Prime False Passed
1f5614d98017ee26a118bc0a5141b214e2d626e8 Apalache Fun Prime True Passed
2d4a67aed76df0da169abeaeca9cff5213373106 Apalache Fun Prime False Passed
5a47849f4665291b8be141a3b71afb37ccc637eb Apalache In Prime True Passed
075f8199098f8e80c7549a387fddf65d0da0ae15 Apalache In Prime False Passed
8b972ee0299d28fd90aea57e3ea256cc76e6e5e0 Apalache NotIn Prime True Passed
e5c620977e04152fed7ca0b13860483b3a065098 Apalache NotIn Prime False Passed
253234aab29f13790e177e8572cb9593093c253d Apalache Exists Prime True Passed
7fbdcd7abf96ffb5ae7fb46f96aa25a958b9296e Apalache Exists Prime False Passed
f67ce6be250fee94102b71540e92987991fe8e1a Apalache Forall Prime True Passed
e2bd8f315a52ebe8bd03ab860e99cd18c3234770 Apalache Forall Prime False Passed
b9f3d8e711282828d92e27c533085dae5d539420 Apalache Choose Prime True Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
b97daa0d0f86ec9dcc7a7729ac2289f9802425f7 Apalache Choose Prime False Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.
4913276bf159fafc2ba6936db5fd30d1f2044cc8 Apalache Record Prime True Passed
4443ebba1b0d803978c4ed227521016168ed0b51 Apalache Record Prime False Passed
ffa5ab3dc9caa70a581b7893f64c5cf958243ba4 Apalache Tuple Prime True Passed
6cd42de79928deaf5ba9d67c2d8840029e9d33db Apalache Tuple Prime False Passed
cb00cc7a3e02a8b28b27c68815f069c687843cd5 Apalache FunApp Prime True Passed
b13d460e80061c3558dbdd2248960255a04cb6e4 Apalache FunApp Prime False Passed
1f3461ba36d17c925343c566828f1eb2ca63d961 Apalache Except0 Prime True Passed
54785af79d1e84b281bd23dc876d1c01f0bf09c8 Apalache Except0 Prime False Passed
31e956943743cbfae444713338580e09050a87ff Apalache Except1Fun Prime True Passed
361b4726c24116a2a545d4e81a3b9f78872a4b54 Apalache Except1Fun Prime False Passed
9a436690019f39514b485a5555f61ee62f788afe TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Prime True Passed
12484122bc1f6c40a30ce14efeb9f3941c662b19 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Prime False Passed
64143ff95512cae9349337eb6c3de45f40506fa7 Apalache Except1Rec Prime True Passed
a9857992f3475995821b8defc7b17d9dc259189b Apalache Except1Rec Prime False Passed
2d97199f40c32dc8625deccd991974c51257d2b4 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Prime True Passed
71687290f4887808e1d7fe220f3480808381f0d8 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Prime False Passed
0b5baef17c1c54d6fdd454a0ef765664d714699b Apalache Except2Fun Prime True Passed
2a486c2ba07b019026d0bcc24e1a870dab617dfd Apalache Except2Fun Prime False Passed
5b4a3e9f4385b775b98b660c7a4564784ea2baa3 Apalache Except2FunTuple Prime True Passed
159faca663b41530ed092f7c4a390ad9ec9ece79 Apalache Except2FunTuple Prime False Passed
c17b9c6bfefa25acf7bc7bf8880dd288afe08382 Apalache NumUnaryMinus Prime True Passed
0faa8dcd4017aff22a6f7331fb6814950c30415d Apalache NumUnaryMinus Prime False Passed
5ca54822877656eff9de7db57abf723acf5d06f6 Apalache NumPlus Prime True Passed
c978dffc72af8a04fc58b67b22092a2516c3665c Apalache NumPlus Prime False Passed
53b734034c5fdd4f14c64fbc1768f4f4d017bd3c Apalache NumMinus Prime True Passed
5fa6b10e6576167615bdf53640ee272347aecfe1 Apalache NumMinus Prime False Passed
c6ac31d0ced4a5450f7ffe390072b95da074fc50 Apalache NumMul Prime True Passed
c4722c6df71e2e8a62d38f7414ee16b66446e36f Apalache NumMul Prime False Passed
63e56b3fbd052171060bc65bd37726c1bc51a6d2 Apalache NumDiv Prime True Passed
dd050389ac69c22f1479c579f958dc9f6a98390a Apalache NumDiv Prime False Passed
e1dd69e7cf0b5aa59f636689484a74abc3c5a34e Apalache NumMod Prime True Passed
77de0618573cf4eb83198fd6f0fe7e3b9a9bedca Apalache NumMod Prime False Passed
c5cb3999eb2f612f0f1c3024b1aa7dcb35277956 Apalache NumPow Prime True Passed
d7cadd6e078375690e39500d5c2884a2dba6c84c Apalache NumPow Prime False Passed
214e9c2fb5e24a15f26cd58eecb846a104bf1076 Apalache NumGt Prime True Passed
10eb9dc463c3cfceecc254af4da2248d37f5b96c Apalache NumGt Prime False Passed
08b87dccd5be19df515a0a3d59d57359e90f3d1f Apalache NumGe Prime True Passed
0d65b8aa705e7a301829f9519c79a2317a71947d Apalache NumGe Prime False Passed
c03e7ec7b5f3b7a775e688a4041ac17ca6bbf7b8 Apalache NumLt Prime True Passed
53357f89202d6a10c977d590020b970e13ef1510 Apalache NumLt Prime False Passed
ba7330926280feac79eeba289c3f956a504bc674 Apalache NumLe Prime True Passed
219b2179fa14318750968039ba136ba81e881b64 Apalache NumLe Prime False Passed
6a29a041aa0a3b80a672ddb24b9958a3d1fa17ba Apalache DefFun Prime True Passed
f15058c86ea98faa2ef00f4e3d1dbe8c104008de Apalache DefFun Prime False Passed
5a7bf6e4f3bce3084b9df7e2f94988e869ebd5cb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Prime True Passed
461592241f4e3d4d712c4a75626c6a45da3e6924 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Prime False Passed
02d4d784289402a891e96f252ff6369bab6b9574 Apalache DefFunRecursive Prime True Passed
133ec67e7467a31b767850c0290471c1dc3d3ab3 Apalache DefFunRecursive Prime False Passed
dd06a1f777fec3fff02cf257a154ca72f2b33002 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Prime True Passed
9203b5ffb93499d6bcf5e80f4b184133986f2d79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Prime False Passed
2d23269c32be7d8c37783e53cb2f770dda845bef Apalache Def0 Prime True Passed
1e80c491abbe788a3516db08574ff77783e561d2 Apalache Def0 Prime False Passed
184c335f538091b8680465d20fe199e30b2300ac TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Prime True Passed
2d8e09c9dbfc82db275096b6f123cbf3ce4f759d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Prime False Passed
ca6b95fc307ed909030494d452081ad2f2697b24 Apalache Def1 Prime True Passed
bdf315726129a0a178264a4aeb030a6079435947 Apalache Def1 Prime False Passed
f7132d280c46e3db8eb9dcff91504d17354eb8f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Prime True Passed
e8142ff980648af20d971858a870279713a15a4c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Prime False Passed
c4ad70bd08f3224499d444cd370e9fee04c61d1c Apalache Def2 Prime True Passed
913bb88e0dabc5801f4d27c54856c82b52180004 Apalache Def2 Prime False Passed
c068418e1ae21b7734a9034a9539c55e42f7390b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Prime True Passed
fb1c6729357902ddb257b1ac04fed419f974b281 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Prime False Passed
ce7d8a2eeb506a85fd5e5cf024569fd41bff85f7 Apalache Def1Recursive Prime True Passed
633c99ecd42f38e58a7dec16d47b96ab75110cc1 Apalache Def1Recursive Prime False Passed
995b80b0c0e44397fc5237a5f3a119262e5f2217 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Prime True Passed
e3c582dfc01f60a19fa710b1ec871eb60125ea44 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Prime False Passed
7efd268c753744c702e379df0b3c767008a70a38 Apalache Extends Prime True Passed
34fe9e0017efe7813239a698b2b006f500da800e Apalache Extends Prime False Passed
2bafe1e31d63680a5f8e38bedc8bcfe66959092e Apalache ExtendsInDifferentFolder Prime True Passed
2cc695f10165951f7f0cc5a058461ec9802840fe Apalache ExtendsInDifferentFolder Prime False Passed
5a2f5137de28cd777694c8be8b02b4586c1ebccc Apalache Variable Prime True Passed
07510a1cdb125aa4d52ed5152df7c7c7812fb35c Apalache Variable Prime False Passed
bed5e89d4d971f29ed469ed06faed79ef3187975 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Prime True Passed
13ccb77b855d4527b0801041f0fe5f06a57222e2 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Prime False Passed
a1d9a610999004e017744cedf1c9988c024d6dc7 Apalache Instance Prime True Passed
9a0b3ce8f6b4e5ef0e1ef3f46d6a2009d74515b1 Apalache Instance Prime False Passed
710a4ae21b9704cc24ff1ce8c200eb9388b3e2e4 Apalache InstanceWith Prime True Passed
9f40f6e88e31470d72e066b74ad773949a1d29c6 Apalache InstanceWith Prime False Passed
2642cdecba01c6a37595287bd68b2d405555f712 Apalache InstanceNamed Prime True Passed
bb65238c9253914800bcd46596ca9a73677db591 Apalache InstanceNamed Prime False Passed
f7ff1f8e21396f7a0f2074d94ca24df9d3600d81 Apalache InstanceNamedWith Prime True Passed
86f5bba37a03621c89697c871cc7b6bece598405 Apalache InstanceNamedWith Prime False Passed
ffac7bec91bdb29c27c89ebea4007a885951c63a Apalache InstanceInFolder Prime True Passed
ccec58ec6ff2b6943011327dae8fb5cbb4515912 Apalache InstanceInFolder Prime False Passed
8ac5c67e0cdc3b45c0f0985ac38e0b45ff4d18b6 Apalache InstanceWithInFolder Prime True Passed
118a8474bc18f05251cac016df2552be3f50e4c3 Apalache InstanceWithInFolder Prime False Passed
0bd016754e4dc36ac4cf92139049734777e8dfc2 Apalache InstanceNamedInFolder Prime True Passed
0f162b80637bdbefc0d52e2d63ec7e276462059f Apalache InstanceNamedInFolder Prime False Passed
13b71f5c7948c6de6ab1f42bd85db98e2043bde1 Apalache InstanceNamedWithInFolder Prime True Passed
ddc45b373c5f61a37ff8ec4e90239144750ddb06 Apalache InstanceNamedWithInFolder Prime False Passed
3f3001acd9119182626f3574409308511d49d62e Apalache Enabled Prime True Failed: TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form
c7f97baecf90cb807d26ee99123473a6f8b317f7 Apalache Enabled Prime False Failed: TLC model check results are correct. Apalache does not support ENABLED operator and if used with prime operator it is irreducible to equivalent ENABLED-free form
4f6d34b2623b6b74fd6b9a72113b95da12a6dad8 Apalache Lambda Prime True Passed
2bf67c952db7a50a385bd35e229daefd3e34023e Apalache Lambda Prime False Passed
c529d9531b1df4e102ee7ee207e9ce93395d30a2 Apalache Cross2 Prime True Passed
b28765ca1b7b57fd1635c13c3fcb1f8c355bb92f Apalache Cross2 Prime False Passed
ce7eed1e617470a52064690170277e6310f0131e Apalache Cross3 Prime True Passed
f2f28edcecb3d6724625fa5e57f666ed77ada0cb Apalache Cross3 Prime False Passed
6a3aeea0c7ac7575c75a954822d665981a1ddc2b TLC with reduction strategy:
  • Case 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))
FunSet Prime True Passed
7c448e43256aa0557534c0e6978f726fbeade1d2 TLC with reduction strategy:
  • Case 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))
FunSet Prime False Passed
8294aaa9fa245fea1c0a991ca33873a1ba488d39 TLC with reduction strategy:
  • Case 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)
RecordSet Prime True Passed
327f19642068d4740009398b57d2f124198d3a08 TLC with reduction strategy:
  • Case 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)
RecordSet Prime False Passed
9254992bcfbf659d7b21d737ad7957750ddfd2f3 Apalache SetDiff Prime True Passed
d449fd3ad2727aeadb5d02b4a00bcda78495b47b Apalache SetDiff Prime False Passed
391e0b725cba9f8ff10dc127834f17a6f56922a2 Apalache SetUnion Prime True Passed
230bb7d8da2aae1966617efbc7c79630c7a6c650 Apalache SetUnion Prime False Passed
2ecbec2642fbadf7f3e339fa118bf6571499be21 Apalache SetIntersect Prime True Passed
53ab05cfe4c6719549d2154dedafdb50fb360316 Apalache SetIntersect Prime False Passed
62a14a85805b8bbad45d7662f508d10bb0bafda7 Apalache SubsetEq Prime True Passed
559fd77953a515ad68488554733ec7cb51618e36 Apalache SubsetEq Prime False Passed
5541bd1232289c8241b615955bffa5eb5dbbf027 Apalache IfCond Prime True Passed
ef76214524a4af1a6be5dbdb8d0b00c52f753162 Apalache IfCond Prime False Passed
a3d5ed39f814923334df841a0931500b2138303d Apalache IfThen Prime True Passed
2faf483918c4f92f009a6d7a740cef01154c4641 Apalache IfThen Prime False Passed
1f816d2c009cc706e9a795d4d188803cf84144fc Apalache IfElse Prime True Passed
eb6186604a51c317c0c50cc8df60f7d701f7e274 Apalache IfElse Prime False Passed
9645120f8debcf0d1c656e5b7cb6fdeb2cc60397 Apalache Subset Prime True Passed
20d661e75d4405a4961c30b08ee825b43582a3ee Apalache Subset Prime False Passed
92304b23b22c82ec6703e23c430c06eb07e444d5 Apalache Domain Prime True Passed
c7c11f755b261eb964fa70560d627c89ecba817c Apalache Domain Prime False Passed
32fa408404e86168d3eeb84e738ba9d11e169bf1 Apalache Union Prime True Passed
98f631837631216047060f49ddf24db6372a8331 Apalache Union Prime False Passed
6f8165beae91f4a90f6ca18f490e41690682a85f Apalache Equivalence Prime True Passed
9926e38b82f247386ff4653b27fb334da007f2da Apalache Equivalence Prime False Passed
23593e7e01ca9c3386888aae17c904fe7a16eceb Apalache SeqLen Prime True Passed
3e0cf30db1e2daa2517db5949d73264f394da5c1 Apalache SeqLen Prime False Passed
2094e300a13b057694f448ce89aefb9cc8d93e7f Apalache SeqConcat Prime True Passed
c88304f9e00eeca31ff5d64e9c3da7911a0167ec Apalache SeqConcat Prime False Passed
13e590c6f19b4b93b743e1fa1c9eea37cc133015 Apalache SeqSeq Prime True Passed
9047603c3e5be7fa78aa956d8471d748a4ddb0a4 Apalache SeqSeq Prime False Passed
1db799412c616648cd5ee5c58392d7935dd0781a Apalache SeqSelectSeq Prime True Passed
06f0384c0728743f216324c0a065a24b29706e7e Apalache SeqSelectSeq Prime False Passed
94feca230080b5db33510cc25ff24c51b9db97d5 Apalache SeqSubSeq Prime True Passed
18ff2e878980780658e2866e3bb32ae6dafbd2c7 Apalache SeqSubSeq Prime False Passed
8dce0153123e51fcba173b0d7bf790d7428e1d84 TLC with reduction strategy:
  • Case 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
NumRange Prime True Passed
b5776e9f44f5044f43e50381e131c89e851af7a7 TLC with reduction strategy:
  • Case 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
NumRange Prime False Passed
6f2cd44d0ff4213abb61e1b205233e93f6904a18 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Prime True Passed
d00b1ec1f9ba76bdde285b33d264c37430e9e694 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Prime False Passed
f82baf83c1121d975d8a2b5c29901c3b9b5542c8 TLC with reduction strategy:
  • Case 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]]
TlcExtendFun Prime True Passed
8a3f4c8b8438d096ee2eca023de42faac2372fa6 TLC with reduction strategy:
  • Case 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]]
TlcExtendFun Prime False Passed
bc345542f26c5a075d0d66d974c98333d9cdd8d4 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Prime True Passed
8f298dd21aa72cdb4ec9962a249b94ddb4dca976 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Prime False Passed
8e41c822a79abf79f292cbdf16d9bebead39f279 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Prime True Passed
dbca4a2e9931c86e730208e65a63868608f63a23 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Prime False Passed
53f744bdc0da241a6cabb5f7be854607d8b041d8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Prime True Passed
46c12091363e7c56d9ffbacd4de2290787353c83 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Prime False Passed
cb242e1f7e1e9d09ada80fd5ba823ecd7d7954cc Apalache BagBagToSet Prime True Passed
bc134dc1af44637148997625a5705d385725521e Apalache BagBagToSet Prime False Passed
3c96ec19eb18efabcf6d41a1128049ce467ad4d7 Apalache BagSetToBag Prime True Passed
2a3d75c3680ec8cccaa7aa18635bea86331a773a Apalache BagSetToBag Prime False Passed
ed012e88b17687f77e2e7105a87a8fb378dd9222 Apalache BagBagIn Prime True Passed
184f7134205893377bfabbe7e6b37029c54d60bf Apalache BagBagIn Prime False Passed
a8e1451b45f7b6726e78ac6054b99e0ead0d9a64 Apalache BagAddBag Prime True Passed
68258b309ed9db0f1a48c6904b4e05797335d190 Apalache BagAddBag Prime False Passed
9918b5cfc55607839595e3b520dcf144f4035552 Apalache BagBagSub Prime True Passed
c47f66f87c74780d69823594a700c7fb15fe2d8f Apalache BagBagSub Prime False Passed
8fd41b6e52b97610e4b1e3d4fb671cfdf04d7828 Apalache BagCopiesIn Prime True Passed
3d93e0c452ba5649d8923ea5d76c9e19bc307451 Apalache BagCopiesIn Prime False Passed
c5c64bb46fa7b7b0ae147cb0995236d6692641ac Apalache BagSubsetEqBag Prime True Passed
edc6cbf73a16b48b5273140cbe65136a56576e45 Apalache BagSubsetEqBag Prime False Passed
845a5887c5f8154b0abe0551d7fa8e2fc60cc691 Apalache BagBagUnion Prime True Passed
6b42a1772a2596d262639193d2250cf23847ea39 Apalache BagBagUnion Prime False Passed
09b80fd98a6608a6ace07dd12dfd4893e70da6a9 Apalache BagBagCardinality Prime True Passed
d77f3c4278769f31dcad536f4156c40203223196 Apalache BagBagCardinality Prime False Passed
9e096ef361205ff186a3a5e299963ff725ce281a Apalache BagBagOfAll Prime True Passed
5eada67e3b49d7c47e74b169018786c5e8c90462 Apalache BagBagOfAll Prime False Passed
9e5db5dbe03b241b3fc2b38fdcf2ec6b92dd7a3b TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Prime True Passed
e7e497e3fd5a0cbfbbcf25992af5fe638d613af8 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Prime False Passed
da1d7d9e454d49298325d05229db6e263dd18673 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Prime True Passed
2633cb4eee6b54cfd3858f7dcd061c14faa8a02f TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Prime False Passed
a2335d94f64d86b93c269dd8303100433705c7ff Apalache FiniteSetsCardinality Prime True Passed
4fd5c7eaa56988d4fa7dafb4571ffd3eeff52365 Apalache FiniteSetsCardinality Prime False Passed
727e030fd21e34b95d57925a9191c6015bfe23f2 Apalache SeqHead Prime True Passed
eadde176d4fe38ecd37226791d63a7a37d78c800 Apalache SeqHead Prime False Passed
55aa45430186f3e4e466ad4a020213b04f77f290 Apalache SeqTail Prime True Passed
016e6a26d887a17cf667bc7625cba442a38b669a Apalache SeqTail Prime False Passed
bfc40f78f510ddeee00631190f10ac576d4f59a9 Apalache SeqAppend Prime True Passed
b3e3725733af50a0b86245c90caefb509b1562c5 Apalache SeqAppend Prime False Passed