Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
e5e60336daff343ecfaca7aa16756ced2246701b Apalache And Variable True Passed
3e9bc6d3ceb3959d63f5de5aa39ff67619a0cf6e Apalache And Variable False Passed
00cfd3ab74590028ee482731fda3fb272b2a7a95 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Variable True Passed
2b529315f2ce79733386a3dd7034b37f30bec50a TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Variable False Passed
da1a635d418232d8804bca7a6e542ac62d007a95 Apalache Imply Variable True Passed
61ac48c0543a5bf24c00458ceee5480c4219c803 Apalache Imply Variable False Passed
854ddc017b2819c8be7cc8db0cd811a34d11e546 Apalache Not Variable True Passed
85b481dc0a4ef2e4fc16dac5bc5f10bd076d3d57 Apalache Not Variable False Passed
402251d65beee857135a7c54e829b8e73937b4ec TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Variable True Passed
ce8cfee34c714f661ff8a2dfd396b6fe78fd7919 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Variable False Passed
00a6631623995adb7790bd61ae7f24ba15c2249f TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Variable True Passed
7b797796d1229775dac1de3fcf152e24437d133d TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Variable False Passed
3eb0adb89f6f11b762b9d63fa7df4a9baa9b012a Apalache Boxed Variable True Passed
14f01ad00bc7f600dd277a0cbb6c9e9bc2319d20 Apalache Boxed Variable False Passed
f304f06946f7929a3c784400f9f2aa5f78a961b5 Apalache Eq Variable True Passed
17ee2442cc93692931bfc1d836f1aa6920707310 Apalache Eq Variable False Passed
bd029079b616d835b0f1c71e62cd56d3ce6d3ad8 Apalache Ne Variable True Passed
48007f4402aa3e822f0257cc909bfd3bba8687a6 Apalache Ne Variable False Passed
2ae0e9e6726b4218c8083246b3f2943db9367fa6 Apalache Let Variable True Passed
acf116d245f359e6f81913dc17cd215e526d907b Apalache Let Variable False Passed
464e80f4ee99c08f00abb9f377561f8fc54fec75 Apalache Set0 Variable True Passed
44f63926131902138838a9bee46f87a992a9caa7 Apalache Set0 Variable False Passed
ec9668936fd2c71d4d487230f61343fea70cd36f Apalache Set1 Variable True Passed
f62bd6501c3fbf64849f3a87eb4a0b2a828f8ccc Apalache Set1 Variable False Passed
8d9290fefb66826f9ed20e7986810904c37b2657 Apalache Set2 Variable True Passed
a11c291b06bb6b8b597a60399d96fc86361fb5f5 Apalache Set2 Variable False Passed
a66f70b36548dc410778ac91bef290ecf33fbf5a Apalache Fun Variable True Passed
d9c8eebf4bf0445842398110468e52a9d28949d2 Apalache Fun Variable False Passed
dda3ae70adc9357cd6dc2e914032bbab64a77b19 Apalache In Variable True Passed
1b39d96129ff99596fddc891462fe9ad2b1c16d6 Apalache In Variable False Passed
937efccc46684a79ab7d6cb9bdb1913c6bfa05c4 Apalache NotIn Variable True Passed
e823b3f8a72b18623913f3620d47ceeeb15c6e6c Apalache NotIn Variable False Passed
efd45114c1f72007e3f78226825fef24daef53eb Apalache Exists Variable True Passed
7f0a9dc36d66113bbfb23a2ea743b5d26bb42315 Apalache Exists Variable False Passed
51528949fecc6ecd3443e3ce65b5e36128820d55 Apalache Forall Variable True Passed
16f189f9f84a2ce070cefc6285bfb04d8be688f2 Apalache Forall Variable False Passed
f6eeb2a15e9e61e36ff879bed25395dbf0dcb8a2 Apalache Choose Variable True Passed
57137c67126cf9425143a4a89a1a4cead80a414b Apalache Choose Variable False Passed
47c643a5054c6754ec5ae6c0afbaa0b9e6de4a49 Apalache Record Variable True Passed
bbb26f1eda787685d3b7ce9380d41106cba7b9c2 Apalache Record Variable False Passed
4d5ada87a9459a3ef877ec250a89ca43dbd4cc0c Apalache Tuple Variable True Passed
258fdd3a9e4f72ada553a3a4f167e2d577a22627 Apalache Tuple Variable False Passed
144786a7f8f906f2f109dc2cdd6b2fde806eace3 Apalache FunApp Variable True Passed
0d19b13e9254bf5446840a52251b7e9d07febfa1 Apalache FunApp Variable False Passed
baa3df4b7aa6e5ada0f3c2315efecd46df4a701b Apalache Except0 Variable True Passed
482c8cd86c9ee11c44c24f33266d59b72471ac05 Apalache Except0 Variable False Passed
8c00702f66259010cb14bed905c97ffa40254d28 Apalache Except1Fun Variable True Passed
4860a6f010088501853eea3eeb8a8821281e69f3 Apalache Except1Fun Variable False Passed
01b22f0b9c41ce0de7e6ccc540166b950eab955a TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Variable True Passed
73253cc6237215473c34cb746ab3792a30194e98 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Variable False Passed
528ca3e98cdcd17036d19e3e2910908a754bed5a Apalache Except1Rec Variable True Passed
2cc74eb605b3e778c6a7c3898d23f30cd02ab692 Apalache Except1Rec Variable False Passed
603cd135f4249d6ca68c8cc73770c5dc369d96a2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Variable True Passed
0bd88ae1918ea7a2f192e7527da79a355aacccf6 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Variable False Passed
74e819edabfd2cfe075ca44241769eae8ada173c Apalache Except2Fun Variable True Passed
408f3108b3899176809b394e37310031d19cf0ee Apalache Except2Fun Variable False Passed
1a148c6ac3a7a08f008df7bce4ea6a3bff143dfe Apalache Except2FunTuple Variable True Passed
58476eea039caa22af6d46532307d8beb41fb370 Apalache Except2FunTuple Variable False Passed
56b01d6b1e6cc8b22d8d87f3812815c6c6f274f5 Apalache Prime Variable True Passed
383390720ff861a4d59712842528d6bb14c34766 Apalache Prime Variable False Passed
5442b0222d9989eb7b4e597471c3c367b02cbdd4 Apalache NumUnaryMinus Variable True Passed
b68ba890b07d80f27759fa6c05d4b6fb042cd0a4 Apalache NumUnaryMinus Variable False Passed
76462ab639594076c07092e855eceed3ea4f9341 Apalache NumPlus Variable True Passed
98876abd9cf12da7d734c50dc4e5be7b2c9ef1ff Apalache NumPlus Variable False Passed
50717cc6a95187b411672280f858d000f44e1749 Apalache NumMinus Variable True Passed
781ddf36a63390303ad6fd993a1373c3050b519a Apalache NumMinus Variable False Passed
122f52a2f44da4c6236c2ad5cb25ce51bec4dfea Apalache NumMul Variable True Passed
9024b65290c2353447f74c51a7a9d8c9028894d8 Apalache NumMul Variable False Passed
9602d0024c08b01322a76c5963d36a0edd6514b9 Apalache NumDiv Variable True Passed
0772a0ce94c6be56348907da8d74e021c900057b Apalache NumDiv Variable False Passed
ccf9da2df47faafe3f79884e934e6850fc27cdcb Apalache NumMod Variable True Passed
01cd55a0af5f2378fdec8969197080f5a6c2d1db Apalache NumMod Variable False Passed
cb72a1c4e8d05fd97ba24288b7ce803cafa746fb Apalache NumPow Variable True Passed
99885f08aec35a1271ab24e759e52cf0e54e0202 Apalache NumPow Variable False Passed
3fb7ba3faeccb44804ad9bf538d2b1d9cc260947 Apalache NumGt Variable True Passed
9dd9a8d50af8c8032e7b2ab57e1f68d73ff61f44 Apalache NumGt Variable False Passed
f9733204024a15706bcf72c47b00f9eafd3d2119 Apalache NumGe Variable True Passed
4c51bb4c47b7cbf06bf2cdd652a5d10797fd9d37 Apalache NumGe Variable False Passed
9480377fcaeb4774903b6bc2252f13d741815f86 Apalache NumLt Variable True Passed
09f944216246c6f9d93ae45ce07c033da16ade17 Apalache NumLt Variable False Passed
8d313ccbeee34c5b17e140ca3cfb139ac408e460 Apalache NumLe Variable True Passed
5fbd6091b95d7f0203d4b5bfbd77fb5f2370f4d2 Apalache NumLe Variable False Passed
3042ec0e53403780249d2f61479b044eb41c235c Apalache DefFun Variable True Passed
957408cadee0226c39a31f0f3221d682885fedc2 Apalache DefFun Variable False Passed
177f5ec3c578dd61eb2f0fb10dd1591b0181b40e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Variable True Passed
1311b937140ae1ee5ae8c2f903e17c906b6a50f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Variable False Passed
35cb992812dfa574307b623bbf0975ad3e70767a Apalache DefFunRecursive Variable True Passed
8f337a47e591a1698d93aecdfc07efc060dfd35f Apalache DefFunRecursive Variable False Passed
d7680b1ef0f372319eac4394a745197c786b0374 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Variable True Passed
8813b9f4b5fc345e606e0c6dec0357cf83cee3f4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Variable False Passed
1220ceb8e4c0c1936f9ecd151dede528c18ce8ef Apalache Def0 Variable True Passed
30150da8715891656b7ac2265bb7f828a050d056 Apalache Def0 Variable False Passed
71dccf6cc7a9dd4a3b192c01effc0866e352e01f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Variable True Passed
59dfa0efb7f35ea96833d773093bfc6edced2b2b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Variable False Passed
d6edc0482dc0fe51f657c7ff07ec5d070fe9b8d0 Apalache Def1 Variable True Passed
ddda8fa643cc059d0539b5f7587d201b598dd474 Apalache Def1 Variable False Passed
4b47dfdc77ad8ccbc18e55c386718a33d7a554fa TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Variable True Passed
b2220381aba4e6c6e90211bab1511ffc7ba26add TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Variable False Passed
f5ffdcc192b654c511dfe1547cea6b3c43b263e4 Apalache Def2 Variable True Passed
aae4189fe4a6c3c92b2ea089334884cdb6b43836 Apalache Def2 Variable False Passed
4f3b8cc7d7ff7a5633a71153b8804ea187ae321b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Variable True Passed
be7bfc4efb1d99520f79e3a8e8c9df64368aa532 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Variable False Passed
8630152294c422865ec47f4a10c52cb45c7e942d Apalache Def1Recursive Variable True Passed
49ba40a05e63339c434b7be4b41176ce6fc84b3a Apalache Def1Recursive Variable False Passed
18c1d2adca6b1e0362ab439ba4bc17d8b5553b91 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Variable True Passed
8f0e2a44f9358407a07b18b91a502cdd1192efe3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Variable False Passed
d2d1586262dc84fabea6709f77e99e6ab3793a8f Apalache Extends Variable True Passed
6b5a2c468b8eef15b74a6f933c562e9c853f5622 Apalache Extends Variable False Passed
e82ab8735331939c161afd11a67a10da21c218ad Apalache ExtendsInDifferentFolder Variable True Passed
d5b7c54479f81bdaea8dda63335abac3871918f0 Apalache ExtendsInDifferentFolder Variable False Passed
c16eabd8afdbcdcebe22346d6018391367037a8d Apalache Variable Variable True Passed
42335999f496d50501956fc71912bacd871007ab Apalache Variable Variable False Passed
7ea6321f83a6a7041a58aa936ffe76955da48ba6 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Variable True Passed
c2d7d4a7fb3680bdf4b626ecec8bdcf1defdf432 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Variable False Passed
dbad5d07839ec88a0c3ce8188fbcc45d9a027ef8 Apalache Instance Variable True Passed
9a0cf27348b3e4d2c23bc62e0743c53a9bb1fd4a Apalache Instance Variable False Passed
a4912964f5e9e26ea2bb5538450d1a46693dc85f Apalache InstanceWith Variable True Passed
23cb1bc4e226bdba56d0d6725d23ef3e81204f0e Apalache InstanceWith Variable False Passed
964a3ec2f209d09ad4295ca0df6fc59b80f40048 Apalache InstanceNamed Variable True Passed
c6a16a50f7f679a87b09ddeee993eefb76944696 Apalache InstanceNamed Variable False Passed
339011018c1ec95554fdfe30f93dc81362ab2acc Apalache InstanceNamedWith Variable True Passed
c5cdd066933d6305c8a651f9c33510e4c21b9651 Apalache InstanceNamedWith Variable False Passed
6330bb7b92c87d4b56f8aa407fa3f7119b28a215 Apalache InstanceInFolder Variable True Passed
d254195fada4e02fab97a81584f57ba3b1b55773 Apalache InstanceInFolder Variable False Passed
54f07302b55b58106bfdecb0a39b4c49218d9e10 Apalache InstanceWithInFolder Variable True Passed
946e7babca7445beab891982d1ff304f1b049239 Apalache InstanceWithInFolder Variable False Passed
a566270ef6a2b30eeae4287fb0601effd6c57a71 Apalache InstanceNamedInFolder Variable True Passed
d957f27e68c5ae4aa98515e43b6669b7d53c9c7e Apalache InstanceNamedInFolder Variable False Passed
8e513c03b5c4139e5d99b224bdcd6d895f331420 Apalache InstanceNamedWithInFolder Variable True Passed
53ff769093cb29fd220055a2f44e1787734d3a4b Apalache InstanceNamedWithInFolder Variable False Passed
009de57ca1b4595a55cf98245635fe0f6e80d5ed Apalache Enabled Variable True Passed
d882ec607eb88804cef4c35e84861a8fdfd27579 Apalache Enabled Variable False Passed
357ea49b57aae256b86ec2af0baba61b4f0f4370 Apalache Lambda Variable True Passed
2ad7365971ed588f0e8f3aca69f2ad7c52df153e Apalache Lambda Variable False Passed
2b141afc1818e0a064790e948945172a42835c07 Apalache Cross2 Variable True Passed
4948d17093087b7a5923b3c99d651eaa7303ebe3 Apalache Cross2 Variable False Passed
4ad758376907af56e72c7a1c6f5c4911bf5ec9b4 Apalache Cross3 Variable True Passed
4124bcad2ee9b196b130d41ab73c0a9d7d28dd6e Apalache Cross3 Variable False Passed
76a9fe20cc6e517c0c34af8c351db7b229710f2f 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 Variable True Passed
43db056e14f00df100a7b4c1cba93eade53c8e9c 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 Variable False Passed
50a1fb8953ed369a65098d4546b65dc1e2afcf2c 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 Variable True Passed
b180993b7eacb8793c4fba4a3cc68defefa23049 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 Variable False Passed
e520ec93be4d1ec24a42fd01fa64dcdd76bfda79 Apalache SetDiff Variable True Passed
9e909d7a98b6a1ef212b05b5d1a36b293cd3b2b6 Apalache SetDiff Variable False Passed
2849af095158fb26b2ee04eec61e0f72f5e82458 Apalache SetUnion Variable True Passed
c3cdaa037fa895d579bbfd0ea89fe67f7de6f2ea Apalache SetUnion Variable False Passed
628a2dca21ca4ee7a1cee792ee3ba1d68b2fa9af Apalache SetIntersect Variable True Passed
4b6e943f67bab0f21cb03ff383e74ee86c487e1f Apalache SetIntersect Variable False Passed
b8756ba92a9643fba5e7f9869f1136d34b14e0cb Apalache SubsetEq Variable True Passed
42b7372043c3c12107d839c297df6a7c68841076 Apalache SubsetEq Variable False Passed
5af841eda6c3a0024873232b923913770c0e054d Apalache IfCond Variable True Passed
27ef54909e5bc0298d60a9425da84991220165bc Apalache IfCond Variable False Passed
6d8a1dfb70a5e72f4980f7e24a901c8d30ddd284 Apalache IfThen Variable True Passed
a78687d8ecc611143411a1c510dd1f578ee85062 Apalache IfThen Variable False Passed
06d8b9fbcb9bcfa46167038a34560992e51933fc Apalache IfElse Variable True Passed
eeaff06690c560d40912b64ece47c75b494fb0c7 Apalache IfElse Variable False Passed
9d38a256aeb670189981d8914600655239651276 Apalache Subset Variable True Passed
892d79707f31b71f4013dde9799a9293ea3bdd0b Apalache Subset Variable False Passed
4b0b8947f3610fc06cf98b497d034ba8117b8d9b Apalache Domain Variable True Passed
6ecf89d28d55d9f3e354e1ddd8d1994200ef1e73 Apalache Domain Variable False Passed
b87bcf52564383fc41b1f3afd19e2bf4ee33748a Apalache Union Variable True Passed
9fd1c1d48592f0ab145929a2661fd1b5874d2b16 Apalache Union Variable False Passed
a110750136d046336d0a5077f28cefa7d7a38605 Apalache Unchanged Variable True Failed: TLC model check results are correct. Specification uses UNCHANGED twice in the same action and Apalache complains about spurious manual assignment, because it is unable to detect that the second usage is just no-op
d621f2ef4ad3be8f4e084ccd91d1730804f2a9c8 Apalache Unchanged Variable False Failed: TLC model check results are correct. Specification uses UNCHANGED twice in the same action and Apalache complains about spurious manual assignment, because it is unable to detect that the second usage is just no-op
afb94c2bb43149db19ffc51a527ae4fa61137e1d Apalache Equivalence Variable True Passed
ca0cb0857ba3f71dd8dd14fb361094a6390593a5 Apalache Equivalence Variable False Passed
fa7d1fcb75213cb7eff4e2c9686c2dae21bd3998 Apalache SeqLen Variable True Passed
a6c31e1d3636823077658abdbf2075cc77a4e5aa Apalache SeqLen Variable False Passed
82045f9c1c0a830acfdfa7310421ead6f0c0bcda Apalache SeqConcat Variable True Passed
31f041f96c956993cd465941b542dcdec7495d38 Apalache SeqConcat Variable False Passed
10f9407d3048cd9bc465c5a2aa39c8a243ce585d Apalache SeqSeq Variable True Passed
cfea068b8431cb74cd7f7b58ad5c0aa66b6ec47e Apalache SeqSeq Variable False Passed
dc6c8543f7da7cab080d65c5d33ed53a9b8be84d Apalache SeqSelectSeq Variable True Passed
8b6492a839d019a5668ae55f0b8bafab3ad5c07f Apalache SeqSelectSeq Variable False Passed
29b6e713779e7cc2b21d11c44038e9a085e5f19b Apalache SeqSubSeq Variable True Passed
2aeb4a55225d71e7e9f206946beb8149750e334d Apalache SeqSubSeq Variable False Passed
7f7565d23fd5ec4e4081383d27d8675d878bb06a 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 Variable True Passed
c14fdfdadd9726797bd90a64ca39317dfa2a843f 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 Variable False Passed
bb40014fe1530cc319f0b1b04b280c153ff85b99 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Variable True Passed
c76ca105eacf0399af2d2d39ff9470642bdc2821 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Variable False Passed
ffdfbcb94877f2f48a792dd3f1dc1ea5159f805d 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 Variable True Passed
6b30c1d6c22f67212219ff3cf97e97de5c32cc68 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 Variable False Passed
7912bab4c198753467da3c6924163a53291b1ea2 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Variable True Passed
028efdfe6e7c82d9f83f0e52b096d9335a74ec17 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Variable False Passed
61e62630bdf4f6005c3f58d86da4486b6a8cea51 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Variable True Passed
f4b168b90dc7e4f72565a9e232042fd5b6cdf3a0 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq Variable False Passed
fd0a2f6a51adde6f773d104ef51f7153ca423c0a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Variable True Passed
d0fa9a35bfa7d93a5b91ef1445ad6dddf8482076 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Variable False Passed
55867688f5425daaf4f633b260f939b01d2c311b Apalache BagBagToSet Variable True Passed
0d98bf1139e9c915ccc3ddc9ef31614547d11f59 Apalache BagBagToSet Variable False Passed
1d64af67d73182ee2d82d8152019bfdf9ebd75c4 Apalache BagSetToBag Variable True Passed
af865b21434cac7f9e0f08f3c04cb2f8e81bc115 Apalache BagSetToBag Variable False Passed
8cb973ba615fb00c667f8346d4fd31a0037507ec Apalache BagBagIn Variable True Passed
627f2f8433cb61e988d30bac0faf937e7c590966 Apalache BagBagIn Variable False Passed
bd764b536456ea6bc3e3851171e39fede7ced850 Apalache BagAddBag Variable True Passed
4ce76758d410cc9af3509105fa675ab783065a37 Apalache BagAddBag Variable False Passed
443a623171843832de85bbc34c48d78bd767e2a9 Apalache BagBagSub Variable True Passed
978ae4b60a561d9ee44b377c21cc4e41e5299476 Apalache BagBagSub Variable False Passed
19982dd3f3bbe49e6f9997da8583553f53532dbb Apalache BagCopiesIn Variable True Passed
c34461ef9eba35b2971803560038cf625bb7bdcc Apalache BagCopiesIn Variable False Passed
5340629b38531a1e512e2b15a9dbc707f2d4c909 Apalache BagSubsetEqBag Variable True Passed
104d746238c0950238e8e144879d9007a6c4c48e Apalache BagSubsetEqBag Variable False Passed
7ecb84ca58b2e32a251ef5ef6ce9c791c568317a Apalache BagBagUnion Variable True Passed
111aee858a9de41d94d0bcf4b99f5116e70b11e5 Apalache BagBagUnion Variable False Passed
83e0af13d0ff7c25b998b3d93407b92a2c2c707d Apalache BagBagCardinality Variable True Passed
747a3dd3158dac34890b03138034b92a8df04cc7 Apalache BagBagCardinality Variable False Passed
7c0fbb347a933149247bad39b59940b0aed00154 Apalache BagBagOfAll Variable True Passed
8c5d82596739230e190a387c8bf22569730acb44 Apalache BagBagOfAll Variable False Passed
13b3411bab500cbda03f068408b364364ef48926 TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Variable True Passed
03cd439d1612bc52a638501638e81bd53949ed8b TLC with reduction strategy:
  • Case Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSubBag Variable False Passed
d8e89f95a990df8b1f748e0efe96c37a990eac7b 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 Variable True Passed
ff26fb1d468ea799151723029b96e7bdd632b2dd 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 Variable False Passed
3c5e59ba9c0ecf46c3996c5d1ad3e897769f532f Apalache FiniteSetsCardinality Variable True Passed
dea8f780f7c748d51b07f89fe08ca80477655c11 Apalache FiniteSetsCardinality Variable False Passed
571649dfe7518a8814620fc4aeb4b1f38f3dcf11 Apalache SeqHead Variable True Passed
4346779e0f7256277fd01ebab9c347cb6654023d Apalache SeqHead Variable False Passed
aea3b4372891795ec2cc3c4c5431f6d3d6d3d2ba Apalache SeqTail Variable True Passed
10b8b38d68263a9dc7e26497545738a49d73d063 Apalache SeqTail Variable False Passed
a4010c147670a24b7184c8ccf180ec2799ca64f0 Apalache SeqAppend Variable True Passed
b24eace9f38bd2759e269db541adca8f8b66806d Apalache SeqAppend Variable False Passed