Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
583bdc6b68b3fc503748593d9b79829b84ffdc93 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Set2 OneLineComment True Passed
a67d797c218cdd40ee2fc45fd6faaa7c61936b35 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Set2 OneLineComment False Passed
00f1a1d4dee6aef83b39e15bb06c30fa38257d3c TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Set2 MultiLineComment True Passed
06c565f260ece63643682f8219633e4ec0199618 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
Set2 MultiLineComment False Passed
85e8af4d0eabec6001850abe5c089c405f55f236 Apalache Set2 BoolTrue True Passed
54504b579f568f7bb7e72f3e2c71e0ab764bb984 Apalache Set2 BoolTrue False Passed
f928a6d04712d14d5ac0ec7296fa98fadf2470af Apalache Set2 BoolFalse True Passed
a3ad33ede5fca116c67b64440e406c4bb98108f3 Apalache Set2 BoolFalse False Passed
a55bca863bee2a9caf6dec1803ed94b54b40d802 Apalache Set2 BoolSet True Passed
a0f6464645a0f6e27840c127e374734aea18c705 Apalache Set2 BoolSet False Passed
53580c96fca888df598dbe2a03a5c786e123711c Apalache Set2 And True Passed
2bdff88b939a033ccc0b39545c45d86a78290f18 Apalache Set2 And False Passed
be452db73c83632fba375cfba2bc0613d44768a7 TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set2 AndMultiLine True Passed
7ad18c88cf14cc1a73a6de58dc769c8ca37c64ce TLC with reduction strategy:
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
Set2 AndMultiLine False Passed
33e7db235133b1cb755bbccd621842f1b13a58f2 Apalache Set2 Imply True Passed
6f5482c1f4eed94b7a5de7c14217a28a6afe8a1c Apalache Set2 Imply False Passed
32ced51d7bad6caf609a4c50261bf822dbc2851f Apalache Set2 Not True Passed
e90de7743fb232f037e638ecd064f1865fd68085 Apalache Set2 Not False Passed
7214d1ba981c6c64725a14690393f673d5dcd837 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set2 Or True Passed
cedef707e29d29fc1f2d5a8d12a13ac993e2d8e1 TLC with reduction strategy:
  • Plug Feature: A \/ B == ~(~A /\ ~B)
Set2 Or False Passed
c5906e353e0c095011eee7ecbf7451089dbfab9d TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set2 OrMultiLine True Passed
f3eddac0f10530b47104a50af69d42b2ecf35de6 TLC with reduction strategy:
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
Set2 OrMultiLine False Passed
6d804f73c3a5f911f982bac2b069f0ab9edf68b7 Apalache Set2 Eq True Passed
95b347204986f996bd4e769d9c12e433460ec212 Apalache Set2 Eq False Passed
1d0573d69a874b42ccda3b82c19369b1543fdb9e Apalache Set2 Ne True Passed
73aefcd248061c250ec5389b99568b0d97b93a84 Apalache Set2 Ne False Passed
df1a355a5b933cb9ebdec21e06ed2388d2506016 Apalache Set2 Let True Passed
98bed916b5e1461502faeabe0e956910365b21ae Apalache Set2 Let False Passed
99f69e968f378d777007b7e8a1f8c06759a108af Apalache Set2 SetEmpty True Passed
8350d6b68338817685dadc9177339a7262189fd6 Apalache Set2 SetEmpty False Passed
4920420437000010f862ca566172e38a39a201c2 Apalache Set2 Set0 True Passed
50218a0e287364d2df68b3780add12ba39d1af0e Apalache Set2 Set0 False Passed
89bb8ebb57a1bce8760c2d6bc5662a20a926dee5 Apalache Set2 Set1 True Passed
c66659e3e601ad7fb675bd0d7c03ee108150cf60 Apalache Set2 Set1 False Passed
424ab54c3792f3dbb573a3e0f86bdc07b0263ce6 Apalache Set2 Set2 True Passed
89ffcc238b6073552d6bba98dd76f2a8235b1fa1 Apalache Set2 Set2 False Passed
471c3474904f97a59f9a7fc23a4d3d3c0694fbb7 Apalache Set2 Fun True Passed
ca5247593b533e0b75bc27692922ed845e20046d Apalache Set2 Fun False Passed
58cefc6e1e01dea6bba6d673d5fa242f8bc107e7 Apalache Set2 In True Passed
4789a949d0fd33ce514cb1505af0a78ed8311ace Apalache Set2 In False Passed
1c1b514c7db1636e816586b00099a05fae6f7bdd Apalache Set2 NotIn True Passed
fdb75b3b4f724d6222a0d2cead5fda5aaaed85f1 Apalache Set2 NotIn False Passed
b32dfa3fdbe2faa1e49a8f8f7951d17ecb1ef290 Apalache Set2 Exists True Passed
b3ff89cf279ae41aa9aaad855ac953e88976efbf Apalache Set2 Exists False Passed
6ae14c726d224fb7f3ca53c93439c1d2bd420812 Apalache Set2 Forall True Passed
25d8db4c6808f8f79c18cc4ca1781fbfab777893 Apalache Set2 Forall False Passed
c7bab1fadea3ed99b428f2c1f30d55a3234b7b39 Apalache Set2 Choose True Passed
7e590ebff5cbcb4b956d86cd0b969161b78f3240 Apalache Set2 Choose False Passed
d2d67a4e64b55f7583aca9ea2992bf39d1f9f1bc Apalache Set2 Record True Passed
8a1e81eab8e52191dda7097c97d8ee79e081c1f8 Apalache Set2 Record False Passed
61c99906e16b36ed6a9b80dee08291c23f3de330 Apalache Set2 Tuple True Passed
5722e003a5f851eebdaac51efcf211355d35ccf4 Apalache Set2 Tuple False Passed
2f3c2a45d5c517d708597199587dbd7adeafcd4c Apalache Set2 TupleEmpty True Passed
4336372eae4ce5073eff1b008b1526ca1b94642a Apalache Set2 TupleEmpty False Passed
7b4ff9a807b6edf739146496479f1d28edab96ab Apalache Set2 FunApp True Passed
931b7f830096ccd52670e5b89dbb1d3124420e09 Apalache Set2 FunApp False Passed
c3a25c35562c83e2f8efcf3e8be3d04f92eeee35 Apalache Set2 Prime True Passed
3b754917419b81b751bcc7d93022bf0691c88ee7 Apalache Set2 Prime False Passed
0787a1e9df22d4756a7613c6f916372fd3a8f9f1 Apalache Set2 NumZero True Passed
22020b954a5bc196d7ec5cb59f9a1fe81526f461 Apalache Set2 NumZero False Passed
3070d856f592455c1e2f46fba1fb37a0438810f1 Apalache Set2 NumOne True Passed
52124197cd92d8b1988fb184b05867e9799d0892 Apalache Set2 NumOne False Passed
19ecd84495ab8c599fd4aaa5efed5e442dc1b73e Apalache Set2 NumMaxInt True Passed
34e7b535ee83dd4f099d4dd3f741147d0f819717 Apalache Set2 NumMaxInt False Passed
05bdb2c7e72853e52371a506cf0a30cfd019e2fd Apalache Set2 NumUnaryMinus True Passed
d2ae253a1e76d6b1f7601a69152cdc37a7eae8d4 Apalache Set2 NumUnaryMinus False Passed
5d5b0e7a28ad5d9ca87464bb90086a5af14c8800 Apalache Set2 NumPlus True Passed
bfa70f4e4cf690ed1e3916f848c305c20670d5db Apalache Set2 NumPlus False Passed
fbb2429a42e7c5dc7eb774dac9a3cf721d53c2a1 Apalache Set2 NumMinus True Passed
9560d180d50fe40ec3b0c8a07296f711b147754e Apalache Set2 NumMinus False Passed
f67614374742574bac20508d489f0339da82d16a Apalache Set2 NumMul True Passed
aab1eda73e7ec04eeb5aa4a19d670d202c1e68f2 Apalache Set2 NumMul False Passed
d1e02ca1a81684621627c7f3bde18c888812ea8b Apalache Set2 NumDiv True Passed
207071138e9aa398999b77576cad79e080bf5fa1 Apalache Set2 NumDiv False Passed
70505a99daafbedb99c4d4dc6343c6eb65f8d82b Apalache Set2 NumMod True Passed
e4e216f6dee7f1b4adb12e9cb60c839ac967ef7c Apalache Set2 NumMod False Passed
e9a9ea63c54a49d33216f699cd8bb85c425ac19e Apalache Set2 NumPow True Passed
65021d86cc505a3de7a81f38848545d59d401a13 Apalache Set2 NumPow False Passed
091c6404135616917e0450296e9803e75b9ac57d Apalache Set2 NumGt True Passed
2f408964cf3ae51b98cd141f46aba214cd19594f Apalache Set2 NumGt False Passed
cecccb33c07f680426f44fb93bcd8726a43a2c5d Apalache Set2 NumGe True Passed
c2f411ddeb3b9e561a2a12c7d13842c37d761775 Apalache Set2 NumGe False Passed
579671e26c1e711e2fd12017f4b6b45289c20cb0 Apalache Set2 NumLt True Passed
b0344fa00be8fef63fe709200fc8742b0473cbdb Apalache Set2 NumLt False Passed
3ee63be0b2c185b352908f7abe96a716854f1621 Apalache Set2 NumLe True Passed
7dc1612d82e36d3f4003fa7944fbaee6bd87658a Apalache Set2 NumLe False Passed
27562ed9b6c4c318425578d52b7f6e77a765a4c4 Apalache Set2 DefFun True Passed
6570b3db39156d87685bcce50fb98df19d97b024 Apalache Set2 DefFun False Passed
185faeed65c64ac1d872aab93b45a5d62c1328ee TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDefFun True Passed
8538f647a5444e29ceb8d7280fc1bbd4a1d1e4e7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDefFun False Passed
55cfe46c56e240a45314442b898669ad6f4c3d13 Apalache Set2 DefFunRecursive True Passed
6a6f775358911d81cd64ce4d518cf7f46d8355db Apalache Set2 DefFunRecursive False Passed
3bc0497f76da97fa825f6e6ed00cdf1433bd01d9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDefFunRecursive True Passed
b72770877acac4bdfdbf414d87cf114f2aa2efc8 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDefFunRecursive False Passed
8004ecbdd406a3ecfaf85f183b07ce1f156e22e9 Apalache Set2 Def0 True Passed
1e9e9703208ac2bdbd580b7b332d070a3e6ccc11 Apalache Set2 Def0 False Passed
4284dad668f13557a993e36d14e7c0d4ac65926e TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef0 True Passed
ba007b696ed1161d9ddffeb373053df9b63de7f2 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef0 False Passed
763d88dd9f18955c8e2810025de09a6e96d6ea8f Apalache Set2 Def1 True Passed
e3b6703ba1071e04df0e2e8f4b4df477eef09bd2 Apalache Set2 Def1 False Passed
7bed4d5db4ba24a4063f1bbb38bb2ea8463149a6 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef1 True Passed
621e82f887dfca3f83a928c1105a53a4a33f8154 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef1 False Passed
e96926c72504148b336a55bd0b72879b45e7b958 Apalache Set2 Def2 True Passed
2562f5dfdabc0247d0dde1209ecfeca775be2c82 Apalache Set2 Def2 False Passed
2aece2a2df029d2e8022572522f474a8f3787bbe TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef2 True Passed
d574051a34559c809d2e9344d8b21566a9fb7ad7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef2 False Passed
e07a22a65197b47e65fca02f938d232d66c1b0c6 Apalache Set2 Def1Recursive True Passed
1ad62d3d61ff313c934aaba486da85a6712fd211 Apalache Set2 Def1Recursive False Passed
595733b34f9c440a2e6975b85bee5781b9eeb70a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef1Recursive True Passed
99900a26c556054f4168ff727ec01afe8a39fcdf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
Set2 LetDef1Recursive False Passed
9aa67a13fbead96b39d1975b93a60034502136a7 Apalache Set2 Extends True Passed
ae4f4e33b43000485db3b2fd01538448d0e5f1c3 Apalache Set2 Extends False Passed
d3e1c1f67dd93dfb2ca8236605f7aaf1956edc57 Apalache Set2 ExtendsInDifferentFolder True Passed
ebe1bf22b3a5e1a0a7a02b26fb6a1f56af549797 Apalache Set2 ExtendsInDifferentFolder False Passed
8d9290fefb66826f9ed20e7986810904c37b2657 Apalache Set2 Variable True Passed
a11c291b06bb6b8b597a60399d96fc86361fb5f5 Apalache Set2 Variable False Passed
35858d9c6257ff800b95abd64492c2eec2abbbbc Apalache Set2 Constant True Passed
d6cc032c0ca0161c9d88943b920baf84dc75a4b6 Apalache Set2 Constant False Passed
a8337ea5bbbc303f88a9b13a4a9250ba61b07f42 Apalache Set2 ConstantModelValue True Passed
230de7a47aacd7f995662a2341dac17d69f31825 Apalache Set2 ConstantModelValue False Passed
aa52804299fa0901d8286ee4d52f297a598c47e7 Apalache Set2 ConstantRank1 True Passed
f3e1078d502edf6aa52418a550c6080df8f2578e Apalache Set2 ConstantRank1 False Passed
7e6f881dc51ef9a26e52990cbee0a4fbd8638175 Apalache Set2 Instance True Passed
8a841cd71b6d44a581a21bda996b814b1b0e8abe Apalache Set2 Instance False Passed
c42521330c7e0098f09c6b3694c0158c2994fbde Apalache Set2 InstanceWith True Passed
cec6926a13ad09d84cac0c29328ece2cdd66998f Apalache Set2 InstanceWith False Passed
b4167ab7958052458e3cecfe1b4c674e2848cf67 Apalache Set2 InstanceNamed True Passed
8e0173ecec5cea72457085a8e4130352c62a8f9c Apalache Set2 InstanceNamed False Passed
fef76ae84dc336b8aa312a6a8f9d39e435ccdaa5 Apalache Set2 InstanceNamedWith True Passed
c669b4f3771be9a1364d754733970021d50a613b Apalache Set2 InstanceNamedWith False Passed
f4d0c572c229bc8af2edd5c1c4741a4a2d017d17 Apalache Set2 InstanceInFolder True Passed
0839231220f9d2f3328a54e9d47ba12fc3f0b862 Apalache Set2 InstanceInFolder False Passed
22f936e441d86b9ba0466a01d65023de46d1de61 Apalache Set2 InstanceWithInFolder True Passed
ff3d83591206124570435bd44685880edcad5a54 Apalache Set2 InstanceWithInFolder False Passed
69cf15acd277db2d252c734c54b78aca1223f56a Apalache Set2 InstanceNamedInFolder True Passed
f301d7318174bb1af21e7d39a652700bba59a4c8 Apalache Set2 InstanceNamedInFolder False Passed
1866cc8069401f9f6cee854bbad97c490cb1c0cd Apalache Set2 InstanceNamedWithInFolder True Passed
7843c28d532559c531cb544bf5491b6197d8e202 Apalache Set2 InstanceNamedWithInFolder False Passed
660906175528ff330bd8c72769a9c16cc60280fa Apalache Set2 Enabled True Passed
d2daf911ad42ff9c4c57db9711a22092cdfaae68 Apalache Set2 Enabled False Passed
f321686d1da654ca6f349e9a1830623a645db0b8 Apalache Set2 Cross2 True Passed
22bcf1cc94bac734dd03d55651c43db919922f42 Apalache Set2 Cross2 False Passed
d8b4003c69c724ad42cc27f5f27964703aac04ad Apalache Set2 Cross3 True Passed
e7a3acd4cd89bfecd46b5872faf3b4d9146b40a1 Apalache Set2 Cross3 False Passed
d652803f884d575228f18d65b8441a391c9dbd9e 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))
Set2 FunSet True Passed
189635d11c777db0c48f5e012b0212a5386ec5ac 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))
Set2 FunSet False Passed
000f1e04728cc8b41a44f3c74162b467339b9c60 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)
Set2 RecordSet True Passed
2ec7dfdfe49e37e80291b90a2c5caf8ef3561373 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)
Set2 RecordSet False Passed
cda1dd7d55a54877e701690f7b90286b002fe46c Apalache Set2 SetDiff True Passed
0e8f1d840ad7a6133eb0798a5dbb0e8968a72a3f Apalache Set2 SetDiff False Passed
4f8032e8e4a3cb3aecabc603feb44951313dc987 Apalache Set2 SetUnion True Passed
cc7f91e14a7b6c366d0f7ce5627c5af9276588dd Apalache Set2 SetUnion False Passed
6bdd483831240eea328fb6525ebb08944e473753 Apalache Set2 SetIntersect True Passed
59295e8f4c3f775d3068ece1dc81d4ba6497cda5 Apalache Set2 SetIntersect False Passed
a0e9bb7750a9bfc392d95abbc94f5052a2ab023d Apalache Set2 SubsetEq True Passed
ead598d05059d5bab6068558f66c2b7692fa1d67 Apalache Set2 SubsetEq False Passed
db0c23931f3c875f037a4520d29576818d4a5070 Apalache Set2 IfCond True Passed
afca60299f8938eed123f09613ae8d020c9d245d Apalache Set2 IfCond False Passed
9a0d1c94dcd4a3e99487ed3ca007793c40095fa0 Apalache Set2 IfThen True Passed
053ae7c59342028321822a838c4ddacc649a172c Apalache Set2 IfThen False Passed
ae1e6c184a04b0d373a390173982556f1cb66373 Apalache Set2 IfElse True Passed
814c8ef95d9df274e9ebe54214a9965a519ac146 Apalache Set2 IfElse False Passed
da9589de3d5948945714e59e6e481f6a23a95f1e Apalache Set2 Subset True Passed
4925273512a688985182a4e5f841607df1cf6489 Apalache Set2 Subset False Passed
7e64a3fc9c96b3f6863b20ba9ea5faa4c9378d4e Apalache Set2 Domain True Passed
fefc391a8c1618ca551cbcda975d50715e51cd41 Apalache Set2 Domain False Passed
62dd8ea4384b1f60277fe5f9ec69ab4303aa8cb7 Apalache Set2 Union True Passed
b0af1feafcbf5e3b2120cea961e886dca7a13f3a Apalache Set2 Union False Passed
9a1798308a46d09409656d3afe65eeaf45759638 Apalache Set2 Unchanged True Passed
2636bdc05f744665738366b4d01061b3a5f3c56c Apalache Set2 Unchanged False Passed
1b2d3be5e6c37dd8c2644849c6f81b93e2217bf2 Apalache Set2 Equivalence True Passed
ea060b7c375b49f92641623bc29e47f60fef3019 Apalache Set2 Equivalence False Passed
11fae848cf6c6aa8d7da17610a492cb35fe2b983 Apalache Set2 StringEmpty True Passed
b39b02b6a407c1b3ee2ecea1eedf8be0fb12973d Apalache Set2 StringEmpty False Passed
1a8db90ed031ce7b3deef917daeea2fef0ab848e Apalache Set2 String True Passed
7f648feb7af1d793526ab81bb0245bd6c8264c7b Apalache Set2 String False Passed
6ce2802ed1093f0c54cc91d8e9ab345f88f35b8d Apalache Set2 SeqLen True Passed
e1d3ebc588d0cc76601ad0bc0b9acbd9b192ecbf Apalache Set2 SeqLen False Passed
dd89a57df30226c25d1df12d0c102ff5e6dba67d Apalache Set2 SeqConcat True Passed
ac10bf9a2be781eba7e99141fa9bae1aeb049f6a Apalache Set2 SeqConcat False Passed
bd29f794563a4148726da6bb1f7f0f056496f24f Apalache Set2 SeqSelectSeq True Passed
340812dcf5e72a8c14bdd3c1cf3a12d104553271 Apalache Set2 SeqSelectSeq False Passed
ae095567b714baf3be6a20f3286437bf55eeae15 Apalache Set2 SeqSubSeq True Passed
3de6bb1d66e5dcf0d932ddeac7f79bd2d219427c Apalache Set2 SeqSubSeq False Passed
d14f348ca87e398b7b72d2b914801c14d97b7701 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
Set2 NumRange True Passed
95f6740c3e0e85ca9bae3fb8128689a3150dad15 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
Set2 NumRange False Passed
7e4fe2f3630f5d870c3c1ddb55f9a1380a3c4335 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set2 TlcSingletonFun True Passed
702ca35b1996dc27818c7c718b159130f0f44ea6 TLC with reduction strategy:
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
Set2 TlcSingletonFun False Passed
2eede76c11ace992e7dbcf2b38db7d92ee934e60 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]]
Set2 TlcExtendFun True Passed
7aeb4f81cda6de6213f0dda96d616d0a4c1298fb 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]]
Set2 TlcExtendFun False Passed
b97f5648ca688bd4a9dbfd10ade47cee413ea959 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set2 TlcPermuteFun True Passed
a4b935f1b42c6914e5709549a4a87f1864bd6238 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
Set2 TlcPermuteFun False Passed
50b2711f0999abbd071f98bf0258bc48d7421506 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set2 TlcSortSeq True Passed
486c4921f11862c627c4aa437d5edc861eced92b TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set2 TlcSortSeq False Passed
ceaa8eed41e731d6c2218a0be5c7eda32fb89e28 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set2 TlcEval True Passed
731414a6df0dc6d0bda727c24f81507d53e87ac4 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
Set2 TlcEval False Passed
8ba806ccd19599d7a45d00df1ec584c3dbd4319e Apalache Set2 BagBagToSet True Passed
b90177e6a9b68c0e1e33de2685097bf246a58d71 Apalache Set2 BagBagToSet False Passed
aa81ff2961505081cfba61e5c8d1ee56876719db Apalache Set2 BagSetToBag True Passed
c64aebebfce3fb9fc3d360edb6fe28f6b8bd2179 Apalache Set2 BagSetToBag False Passed
981655d9b5f67db81716ef6cb38ab260ee0f3fcc Apalache Set2 BagBagIn True Passed
57ba2804b8d63f42e3e9ec897e2e393936539363 Apalache Set2 BagBagIn False Passed
f3d6c6f3f57ad1f99b792b74934b774f525717be Apalache Set2 BagEmptyBag True Passed
34377d24b8c035c8710262f90d07a15999857230 Apalache Set2 BagEmptyBag False Passed
1d1aee41449d508ddd6057fe467e27b1a503b727 Apalache Set2 BagAddBag True Passed
2f25031558d677a488f75df75cb6376e35343c88 Apalache Set2 BagAddBag False Passed
bf11da463bb437cadbea0497576c20e7c6ed38db Apalache Set2 BagBagSub True Passed
49390e19e232e5742e72ab9b1c1dae93336d23b0 Apalache Set2 BagBagSub False Passed
5043f4bf5fc3a13074e6db0ea8d53c712cefb818 Apalache Set2 BagCopiesIn True Passed
f6b48973e8c215b2cc665ac9afe961a7c14655dc Apalache Set2 BagCopiesIn False Passed
d21274d685795c958eba5cdef9602aadf3e6da73 Apalache Set2 BagSubsetEqBag True Passed
9a5908e58d9c80243fb699c49dea3410d24015c5 Apalache Set2 BagSubsetEqBag False Passed
ea63dbb269ba21b0ee1dadfdf39f7f01002b4167 Apalache Set2 BagBagUnion True Passed
a4f63f8caa338f17c89f6e766e3252df83c39a03 Apalache Set2 BagBagUnion False Passed
abbdb2942fc76771f13103e96ffc295cf59a5012 Apalache Set2 BagBagCardinality True Passed
8954901a667a886fa710ae0ce2f0091dc965e3a5 Apalache Set2 BagBagCardinality False Passed
d913f005eb8a4c7fd7b1bada28a5c489313e82d0 Apalache Set2 BagBagOfAll True Passed
bea2949d053a6f684df68242e6ba2a15433279ba Apalache Set2 BagBagOfAll False Passed
3fe5449abc3e51e056c0127dab92c7ca5cadab74 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set2 BagSubBag True Passed
e37e75f71a80af30811e9cafa77a4ae2f1262c3d TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set2 BagSubBag False Passed
82ab2eb536554b3ef70f118280a2285c77aeee8d 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)
Set2 FiniteSetsIsFiniteSet True Passed
3198c7726636c52cff5556e35681de6b508117b6 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)
Set2 FiniteSetsIsFiniteSet False Passed
1a47dec0cfe0eaa7a376d9e3972bc92d72c96d32 Apalache Set2 FiniteSetsCardinality True Passed
ad049fc2619db34c763e08bcc65cfd72fd474ad4 Apalache Set2 FiniteSetsCardinality False Passed
87b5e92476659a86c26ffd537a3802bd7a55b6b0 Apalache Set2 SeqHead True Passed
ac689ef737af0a51ec72d4f842d00be475383be7 Apalache Set2 SeqHead False Passed
d385bd8696cf2f10b334c5fc79fd96b154de902d Apalache Set2 SeqTail True Passed
4485ba7f507901a033abd921e20cb8e2c570387a Apalache Set2 SeqTail False Passed
15e8485859419f9c4099fef4a19b6c07847edb14 Apalache Set2 SeqAppend True Passed
7d4b1ba53b793e635fd3091430caef27ca475df8 Apalache Set2 SeqAppend False Passed