Index

Tests by case feature Instance; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
530b41c043c951c79b570512097a812b9fc2c875 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Instance OneLineComment True Passed
c4565c3263b67f2c0af00b6a5895ac0eccc32663 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Instance OneLineComment False Passed
a6e7b7ef3839acb6d778f8c6f38c05ebdf161bff TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Instance MultiLineComment True Passed
16b09fcb3b578ea65d6e302c143a66f7c06296f2 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Instance MultiLineComment False Passed
2295337e3de31845468f2741ad64c9c81c91e146 Apalache Instance BoolTrue True Passed
d59f8b30fb983751c628e2e3118bacee5a772d51 Apalache Instance BoolTrue False Passed
48c407c33c7a677b163bf0ef174bdc28bb9ce3d3 Apalache Instance BoolFalse True Passed
a81a54f4d3e2beeccf35eb66dbe2b0bc65f28788 Apalache Instance BoolFalse False Passed
9efe56ce06377f558af1e0500ad92c93c96954be Apalache Instance BoolSet True Passed
902e95763162bf8dfa6c3112f55883e352371c23 Apalache Instance BoolSet False Passed
9364f95ea8bfee7b6711cd36e08f395465ae2f15 Apalache Instance And True Passed
27ee7659e2015386230a9d05b2a3325e9b11dc51 Apalache Instance And False Passed
8aa6a92ff19c2fca8f1bc9fc7b4b87691f4688a9 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Instance AndMultiLine True Passed
bf5e20338f46cfd46ee77a31413fef32b1f25edc TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Instance AndMultiLine False Passed
b78919fe92c258d903c1b5dea124fc9e519cf919 Apalache Instance Imply True Passed
822936ee097ee22d777a7ca13b6946bf5b211c1c Apalache Instance Imply False Passed
95c0ef9a622fc4a90526158599fcbac5e42ddabd Apalache Instance Not True Passed
7d8a8127df7ce8339ca8648190985cec1314a095 Apalache Instance Not False Passed
d06b570cc13c914145560b53135b68721f68a480 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Instance Or True Passed
24fab264efb9a4ee2a4ce0a2c4451c58932b6b50 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Instance Or False Passed
ee66ac75d25134b8da1591e933c44aa9a10fde88 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Instance OrMultiLine True Passed
16e9cb74777c3da9ab037c7fec82ddf3c6015d26 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Instance OrMultiLine False Passed
beb7d55386ff6e9ac9f5952a9a46c671af4df63d Apalache Instance AndProp True Passed
203eaa47b920ee05a7ed11dbeaf1f6468ac7b97b Apalache Instance AndProp False Passed
fd627611942b61adefde3cecbcacc97cd9d4d1a7 Apalache Instance Boxed True Passed
1c5fa0b2541edd2c1b3ec001fb3e5331340d4e1b Apalache Instance Boxed False Passed
bceff5f7140e68afbd43ea0e874a555edc7a10f4 Apalache Instance Eq True Passed
cdda85df6c7e7f3db11c0c46cec6fb37ded0da42 Apalache Instance Eq False Passed
260f9ee108867d0227e81687f77718219678fc7d Apalache Instance Ne True Passed
7c177032643250d2eaf3429ebcba0d456e74fe76 Apalache Instance Ne False Passed
451436f1b15cd72ed0b3e9289ed9f50d461d6d87 Apalache Instance Let True Passed
c029294473543fddb2bebd271ac89db54f19620f Apalache Instance Let False Passed
122388c35d3e08453b4905bd970f92b0593014c6 Apalache Instance SetEmpty True Passed
67b2914504a928f43a6db02806e97fa40e036fe1 Apalache Instance SetEmpty False Passed
6a3467296e07e13d29ef9babb265919c2b7fe42f Apalache Instance Set0 True Passed
6ddde844cff30cee7dad1ffbc2f6d42435aaa148 Apalache Instance Set0 False Passed
d38bcc86d842c347c92060c9709fb4a2f78e5e00 Apalache Instance Set1 True Passed
0dd0d9f4cb949ce4bd44117f1c993a3e313737a7 Apalache Instance Set1 False Passed
275eafa860654ab4cf8e44eec2126f3965cd6d0d Apalache Instance Set2 True Passed
c4924d71d3c1073598ee780584896f913bca6b1c Apalache Instance Set2 False Passed
0a0c86ae435fbf0ef6ee95ec5024112a6c45f47d Apalache Instance Fun True Passed
422a80899440b31f66770973e7b5b8402a006605 Apalache Instance Fun False Passed
d9630b8fbec2e412972b6f77874857725307d242 Apalache Instance In True Passed
c146271feea511d59c106c6a9a1c4902bf7ddf7b Apalache Instance In False Passed
b58aeb69b496faaf5c1970574660b0f4a433af88 Apalache Instance NotIn True Passed
773cbd220d8e716764bc21e9749990de33412a41 Apalache Instance NotIn False Passed
04f159752747c08d7e0727c822f63a3265c8f01c Apalache Instance Exists True Passed
0f23a4d3bba8f3003d962c8c376ff4a64cd70d6e Apalache Instance Exists False Passed
e8384d36c0674b00167132f50ab90907a6ae79bf Apalache Instance Forall True Passed
88936f0b2ace481b6221b9952a9624c46f1efd20 Apalache Instance Forall False Passed
b3fb9cac7824a23bc52b88ab14a5d4a61c9c8c61 Apalache Instance Choose True Passed
03fe765d9c7eac17dcf7483dc7a42a6701ca63b9 Apalache Instance Choose False Passed
64e6ee7bf6c31016d00f64d7c4b30299541a6e7b Apalache Instance Record True Passed
ae6cea83d60d19132e4397b8349304c6ce211e22 Apalache Instance Record False Passed
e54e40059bf1949c6e2f86983110199b6ed8c313 Apalache Instance Tuple True Passed
022e2891c8ed0f11d8fccc3e201e3a85be4caa88 Apalache Instance Tuple False Passed
ca955c468330e0ed59e12c7b67b71a05858b1b09 Apalache Instance TupleEmpty True Passed
4e6893f1e1616be8d79a6029b47d06ccd707490a Apalache Instance TupleEmpty False Passed
eaff91da5e11b5c8de104da3b4880b66d481f226 Apalache Instance FunApp True Passed
ffcde4ecaf0d200e0e6650490ad8b9d7438b04af Apalache Instance FunApp False Passed
a1d9a610999004e017744cedf1c9988c024d6dc7 Apalache Instance Prime True Passed
9a0b3ce8f6b4e5ef0e1ef3f46d6a2009d74515b1 Apalache Instance Prime False Passed
4d96b3c69db5fa951ebbfc5801713df6f8c84e9b Apalache Instance NumZero True Passed
58d5eaa9c81eec56e02ae653c6beef5a5dbfa6e0 Apalache Instance NumZero False Passed
48c6c40bbd496d5fd95654e06be112c6635fe526 Apalache Instance NumOne True Passed
32e70e6d0e4a776ff016292ebea803f8281c3da2 Apalache Instance NumOne False Passed
4f84f78e106d4086f6eca9fbdff5161b6e624936 Apalache Instance NumMaxInt True Passed
1aa168883e7ff0db285eb5b0d2db8d7b01ef4a3d Apalache Instance NumMaxInt False Passed
ffa0cc1d7bc355db957b511ca475d2c29839141d Apalache Instance NumUnaryMinus True Passed
e34dd684869a8d539eda62ac9cf6853d08e62d8a Apalache Instance NumUnaryMinus False Passed
031473bb4131678a8bbe8e55780ff57d2732afd5 Apalache Instance NumPlus True Passed
cc1c3832042d70a9ffc1f7f60194d1a358809dd7 Apalache Instance NumPlus False Passed
142d1d45d1abb17c2a813773fbf5d9a7d249bad3 Apalache Instance NumMinus True Passed
f7f136c8c6ed7fca1a7e2ae75e8de7eea65731f8 Apalache Instance NumMinus False Passed
091284e198b1684436a5fbb00386db6ca2dba09a Apalache Instance NumMul True Passed
f45198d61b6c2cab3a3ffeb3ef629a483158e782 Apalache Instance NumMul False Passed
aeb3645743a394012dcc814c1879a8e54d5d6d82 Apalache Instance NumDiv True Passed
0ad24805fd7ba91757059733517f394b3e62a1c6 Apalache Instance NumDiv False Passed
083c5944592858a7f22ab8790da670070ea8607a Apalache Instance NumMod True Passed
edb7a251cbe88eb88a9ac0a6c887ec12d59546da Apalache Instance NumMod False Passed
7f06ae550bddb54400302f126d78e74b5067a86d Apalache Instance NumPow True Passed
72f10c0623017e4a02e710a48931bf844e5ca148 Apalache Instance NumPow False Passed
61102584fc18f8e867b194a997ee19452fd76781 Apalache Instance NumGt True Passed
f62ca666fc515f37c47a2f40224fb17599ad66ca Apalache Instance NumGt False Passed
fe34d5af9050ba82ee0eaf0ca59480ba74849771 Apalache Instance NumGe True Passed
f14f1977b8abb4739001d328da60af96baf72704 Apalache Instance NumGe False Passed
a680ea2612742fc6cc0de8f250849126b2289efb Apalache Instance NumLt True Passed
f646957b4e2df2e61cc123564aa2493e9cda33a8 Apalache Instance NumLt False Passed
f256ad67cf46ad7d9e8a74f742004981a190e9ef Apalache Instance NumLe True Passed
b57a4f039fb474fe2610c38b1e507b6e104d3931 Apalache Instance NumLe False Passed
02aa548dee7398affc5ff682b2f1c3bdaee5bc65 Apalache Instance DefFun True Passed
35c426480a9d884fb4a8041b6babc6cc84ea8180 Apalache Instance DefFun False Passed
1146bba2cb8f25cece20b6b0af0854ff32aefc94 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDefFun True Passed
164021d81a4e24baa1ce46ff4992516938ba2787 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDefFun False Passed
84a85c6123da11c1c989d246e94c22da29e6fcfc Apalache Instance DefFunRecursive True Passed
86f1824bbf2d31f530a4306a79187ad27c7c7e3d Apalache Instance DefFunRecursive False Passed
47f7c62861a150598e692760f4d32485be1ee628 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDefFunRecursive True Passed
6aa25838148b98b8f13c3b386b9341e80e2c9ba1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDefFunRecursive False Passed
884fe48fd23345eb3bae28d457a1e7414af4a87e Apalache Instance Def0 True Passed
18b6b46071b0a9d2dafab572c1af0d5352789783 Apalache Instance Def0 False Passed
cde00abb4446a66f16e12f2d102294744d99baae TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef0 True Passed
b12154522d052bf8787f41005f9d63688c4dfe9a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef0 False Passed
70c4533f8aea963e6cfa1621e74934edcaf2dc3f Apalache Instance Def1 True Passed
aedae4aab3696e805b4731fd811cd6a7ebcb6028 Apalache Instance Def1 False Passed
baf93e275fdcd9444fa6aefd2901ce312f9c0c9a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef1 True Passed
7b66a14838b1cc3d7572ed1bc4a274d3cbbd00a1 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef1 False Passed
5b12f80cda7d4aa88062d59f10e9645db959641c Apalache Instance Def2 True Passed
307ba445f804d7cd7d824622c6fa6a8aeea8cbcf Apalache Instance Def2 False Passed
f87d582cd829fb27856ab750ef286b4239772d53 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef2 True Passed
c800cc358e23fc4c983efe9cb5914dcb2b978943 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef2 False Passed
57e2c800c95177d7f3933fc9a3d5fe8a50dfdee3 Apalache Instance Def1Recursive True Passed
a76c313f7a4b54b2592400092997d061597d62e0 Apalache Instance Def1Recursive False Passed
d7fc4e1a6717cc438c49cd81e4a7dda7a90fd737 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef1Recursive True Passed
1d9976ae37d4dfa78d4f0bb01cb708c941662da5 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Instance LetDef1Recursive False Passed
73af86021860395c8f96cbd6fc881bc24a0531d1 Apalache Instance Extends True Passed
2b8a0c85baf99878cab1de17842bac877be092c6 Apalache Instance Extends False Passed
3ae41fd48228b11701815c5e56d9cde4fe92841d Apalache Instance ExtendsInDifferentFolder True Passed
19318ed6d761357925fa71ee49c79852fe3f620b Apalache Instance ExtendsInDifferentFolder False Passed
dbad5d07839ec88a0c3ce8188fbcc45d9a027ef8 Apalache Instance Variable True Passed
9a0cf27348b3e4d2c23bc62e0743c53a9bb1fd4a Apalache Instance Variable False Passed
5e643b52979b09d877d48de998d4b193c256ebfd Apalache Instance Constant True Passed
0a89aca417cc1c918d3785ab6eb0e384f8cbf9ca Apalache Instance Constant False Passed
50d7578199c28ac4b62993935d5525e47f094c15 Apalache Instance ConstantModelValue True Passed
b9cb7fe65f5b96a1c781c71bbd57aca6004b3dda Apalache Instance ConstantModelValue False Passed
4357caa0d5ee29a7a2c02fa36f7b42fc2ce10479 Apalache Instance ConstantRank1 True Passed
e9cc3a09fbbf3e92ddadf3d661ac89ee33de8dfb Apalache Instance ConstantRank1 False Passed
af3cbb9c1babc120f62f9ba85b07ba7730cb2065 Apalache Instance Instance True Passed
cf9ed8d703c7d6ee8b11329a21c697470974ee81 Apalache Instance Instance False Passed
2fbd31f97c9dbce7f5278e0e143478ee6523a5d2 Apalache Instance InstanceWith True Passed
6d63d377fa09d4453c0aefe1cffbde99e5820bb1 Apalache Instance InstanceWith False Passed
f5255dec7834d85ce7f1acc03c4adbede190c1ed Apalache Instance InstanceNamed True Passed
833a99785a2b7b814eea7800bbe7c8d9c55faec0 Apalache Instance InstanceNamed False Passed
7ac7fba669bbf90bf6e094c4ad664092a9e42071 Apalache Instance InstanceNamedWith True Passed
91ecd9f9943069818924e453c493280a18f97256 Apalache Instance InstanceNamedWith False Passed
6696a7fd38faf14fc6650ce75078adeb37b23639 Apalache Instance InstanceInFolder True Passed
a3ea98f64464e28dc8b1e67ec764a866a4a832ee Apalache Instance InstanceInFolder False Passed
727c5ff8be3bd2cf826df4ac88e80fe61d5cf7d6 Apalache Instance InstanceWithInFolder True Passed
7109912cfe5535619d55d15ad6b7695ef7ef227b Apalache Instance InstanceWithInFolder False Passed
13b933f7727cff585074b9d2d7ec81874f679fa0 Apalache Instance InstanceNamedInFolder True Passed
96057f008686ceb89f9171b6a071c1c0893ca6f8 Apalache Instance InstanceNamedInFolder False Passed
7015d96abe28b4e7366273da278def5aa92c5d4f Apalache Instance InstanceNamedWithInFolder True Passed
c6fb8daa095eb3153f63b0b068069e2b6291d674 Apalache Instance InstanceNamedWithInFolder False Passed
e2a3765897607f0a868be8e9745fcddaecd99ad8 Apalache Instance Enabled True Passed
e2fe61f11a149ce79d52a24823f3c14637332c70 Apalache Instance Enabled False Passed
24bb52eb2ac92ad02e758f209a9ed94d0cb8a8e6 Apalache Instance Cross2 True Passed
34bd82046c6bc6b01ca4d3955ba9046416d3a353 Apalache Instance Cross2 False Passed
30f6cc897ee95f47c644bf44d7d3009b325fd271 Apalache Instance Cross3 True Passed
2d04aa9b79170389e73afb026634960b5a5f1174 Apalache Instance Cross3 False Passed
ad2aec6bcde1f1c289d2b5d86a40e1d28123abf4 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))
Instance FunSet True Passed
3f0fd760ec7fd377ebca5c8f73e8bd0d4958d2d0 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))
Instance FunSet False Passed
86e24979ae30001643bf29584c8a10803a20d27a 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)
Instance RecordSet True Passed
7a20bf3ba9ab56e0fafb046c5efe7ab7aa11fe90 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)
Instance RecordSet False Passed
73260a66c8a2f5dc4d64d499ebb6cb47665f1d1a Apalache Instance SetDiff True Passed
e47106dea9a680e0aa5084d49129dd8940aade93 Apalache Instance SetDiff False Passed
97f356e211dc0b38dfba6009a2923ca9994f9e91 Apalache Instance SetUnion True Passed
b658d4a6f2224c8f631f49a6fecd3aabffd6ea25 Apalache Instance SetUnion False Passed
67f89387d8310c0a15478f72c3d1a3c956eb3ae5 Apalache Instance SetIntersect True Passed
00152f6ece78e09b0784a42b8c1820e77570230b Apalache Instance SetIntersect False Passed
75b7069cd90f4544db24467992cc3dfe7d758dae Apalache Instance SubsetEq True Passed
5a8c25e223a6d56ca9f3245379136cd97f1b54d6 Apalache Instance SubsetEq False Passed
d572869da01421c0a541e368a04e1251e17ce102 Apalache Instance IfCond True Passed
3e28eccccaa33e6dc29a52a3c75a80cb3d231ee3 Apalache Instance IfCond False Passed
27c1a8532a051417a72f993617136c31117ac9fe Apalache Instance IfThen True Passed
64bc6ac23bce0bf87b50b0035f07f29a73cf92c5 Apalache Instance IfThen False Passed
3432c0f3527f635b06fddb92c7292fb3df74b08a Apalache Instance IfElse True Passed
5d85410a215cb15495beeed97761c3ef4943dfd5 Apalache Instance IfElse False Passed
28b8e15c811fb8a53ccc827975130cde933f15e0 Apalache Instance Subset True Passed
7ca71106bbbbaf830b2183ffaf2a1557b6912ab5 Apalache Instance Subset False Passed
3f08e7977b1579a5e0aee3cd175fdbba3ed6153f Apalache Instance Domain True Passed
4dcb6a149f82e77f4a595644c187310f141ebc3c Apalache Instance Domain False Passed
f14206e9f9ab218af774006a71eb94b2781fbc35 Apalache Instance Union True Passed
800057138936817bb00f642ae126d07ede4328ce Apalache Instance Union False Passed
6c1fd42952e9f68abc14a3ee1088f0f91e65262c Apalache Instance Unchanged True Passed
a8ae9fad19aac24b46665ee8870136c5542c20f6 Apalache Instance Unchanged False Passed
72ad127fe94b8937a1b096712d290831d5650edc Apalache Instance Equivalence True Passed
c3ac457425e32a2e537ef3d65b02fe7c2867d48b Apalache Instance Equivalence False Passed
95048f6df5ed05b8ae41cb40f08d3ed6fb7bc5ef Apalache Instance StringEmpty True Passed
daea41845090e176c6d4137cc899c0d9601ea0f7 Apalache Instance StringEmpty False Passed
1dd9aebeac241e965ee6d0ff80b99e3cffb54e8a Apalache Instance String True Passed
ec6d08c769f69bc30dda0224fe94c371d50da227 Apalache Instance String False Passed
9d3e64badf2574dd79d7c911e86267067c90ef35 Apalache Instance SeqLen True Passed
82477bfc218d05a72c1ab8d0033e1ce61f36df12 Apalache Instance SeqLen False Passed
02b2bc2653aac5053b490280b39146765593058e Apalache Instance SeqConcat True Passed
90e4a75d024b79559c98f77f5dbab2d2d72c2b15 Apalache Instance SeqConcat False Passed
9d4e871d764c1a17572a1e227a005d33c8040a2b Apalache Instance SeqSelectSeq True Passed
34767839c9846db997f675ad6a299612d2dd9984 Apalache Instance SeqSelectSeq False Passed
6c34c952959fc23b564edc921d28243687372428 Apalache Instance SeqSubSeq True Passed
dcb0d6a218100e86b7d5c6e26fad322d9ee7f011 Apalache Instance SeqSubSeq False Passed
192f8ec31453ebf46fbbe7b0264f8209ad9e83a8 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
Instance NumRange True Passed
c7456eb0716cc21db78663a8af41e60b96db7242 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
Instance NumRange False Passed
ebc3ccdd5d0b2db992eca50eabf6de51355f3afe TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Instance TlcSingletonFun True Passed
c254e824f9dd99f13bd0e6b66ba232c94f6048f5 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Instance TlcSingletonFun False Passed
8223e5d9e5a8135824a7a3b7d623cdb578b454f2 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]]
Instance TlcExtendFun True Passed
ffbb6c66ebfb8b96ed4e6b59cf21986d5a11ffd8 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]]
Instance TlcExtendFun False Passed
4ff10b349ba3338f48f634ccda09ea5c48b27b52 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Instance TlcPermuteFun True Passed
0e80fa173ad975cbe7fb56988ddf55150dc080dd TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Instance TlcPermuteFun False Passed
dbdb33cbd3f953c0a2e2b867d1638c4196a3433c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Instance TlcSortSeq True Passed
9bdbee331362ebce31ca919ba9ac6466162e0188 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Instance TlcSortSeq False Passed
d4638f8c99b573c4e3e4e7a00dd94e9b194f9c18 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Instance TlcEval True Passed
ddc4d8d3e612fca061c651b77f2985255223be9a TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Instance TlcEval False Passed
5d7d53156524931ab57c8036fb023da29951ca34 Apalache Instance BagBagToSet True Passed
975ee89c81bcb34ab36b47204d3a5f1102bfb810 Apalache Instance BagBagToSet False Passed
edf79a3a996f58b1c0cfbb175802408861215cbf Apalache Instance BagSetToBag True Passed
16a8bdbec960db45d11b6eda035885c92299f5d2 Apalache Instance BagSetToBag False Passed
b61a588bad8663578362385935015b4db3aa55fc Apalache Instance BagBagIn True Passed
1cd9b41f454f679343cc07851a990c6b1b19e134 Apalache Instance BagBagIn False Passed
892429a87cf5e4b3d67536a241b09cc9d897697b Apalache Instance BagEmptyBag True Passed
6be8110eb3a3089c559d6ecd35899f8ec99b7517 Apalache Instance BagEmptyBag False Passed
bbe135c47abca2e7381323d3194075be56669e6a Apalache Instance BagAddBag True Passed
a29533b018b98f2b9ebfd8a767392974b5682d43 Apalache Instance BagAddBag False Passed
912651bf39212dc32cb87009f70a543f139ed486 Apalache Instance BagBagSub True Passed
8c499572b6a93b6166243aa488e0d6a5f25450ac Apalache Instance BagBagSub False Passed
fb53116d3a28d1b2146222fb65bfa0291812cfd9 Apalache Instance BagCopiesIn True Passed
665a20750e116452ad854746a925c147307ff099 Apalache Instance BagCopiesIn False Passed
f7f81158627dc6fcd03bdffd2f3b6b4bbdaeb691 Apalache Instance BagSubsetEqBag True Passed
b94d92c40ddbc1ddbc9661ca777c7bc313395a90 Apalache Instance BagSubsetEqBag False Passed
6f667938038e6ec84c163432e024cdb2dca4ab8e Apalache Instance BagBagUnion True Passed
6de84ee0918d2b90f43017263ad9bc2545ffcd87 Apalache Instance BagBagUnion False Passed
e93368e62a1778829b8017d234b617eeff492728 Apalache Instance BagBagCardinality True Passed
32a0714aa05f2bd10ed6073a1ee58443ee4d4266 Apalache Instance BagBagCardinality False Passed
96e001da500c83b8ffdc99a9656822303548548b Apalache Instance BagBagOfAll True Passed
8e7f8c565f3efa48c035025e9d146b5f71b62290 Apalache Instance BagBagOfAll False Passed
2a8306bec543f096e74cd8d60d23ec7f54b69256 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Instance BagSubBag True Passed
109d6c4be8d12412941da434d9a5c0fd7f0b64c8 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Instance BagSubBag False Passed
e5ef6dbdafd858f76a27f8e77b81b5cb8a2e7c3f 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)
Instance FiniteSetsIsFiniteSet True Passed
340ddd92aaa8a691508c5bd10277ec5f0956456a 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)
Instance FiniteSetsIsFiniteSet False Passed
2a2cc6c1cd8e830560a44777c01080433ecbc6c5 Apalache Instance FiniteSetsCardinality True Passed
19c1590b837b14fea11e51b37410e7dcbac0fe60 Apalache Instance FiniteSetsCardinality False Passed
049cbbecd732041d17fde3ed435ab1f993c50d69 Apalache Instance SeqHead True Passed
e463447df1eb16357fc4d196ba646fe273c72149 Apalache Instance SeqHead False Passed
ef311779ec41593eab15064ee3a7fd2929b88660 Apalache Instance SeqTail True Passed
d2fd1cc0ca2b2768b907394b943258d9bb5974cb Apalache Instance SeqTail False Passed
3e5c8ba397f74a09d80567ab7a44fe466c215526 Apalache Instance SeqAppend True Passed
e7250b7a03989e3696a3040c3bac5b465169eb0f Apalache Instance SeqAppend False Passed