Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
9123579e43dcc6c6a708feb69e4b75b7359bcd7c TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Replace spec with the same without comments
TlcPermuteFun OneLineComment True Passed
054d68a7107021a536f14ffe472ab0bbd2237869 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Replace spec with the same without comments
TlcPermuteFun OneLineComment False Passed
2ec9138347a4406cb08e8895129530f96099b1f1 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Replace spec with the same without comments
TlcPermuteFun MultiLineComment True Passed
e82257eccebf784d3710aabe5ad3a4a8a789a90e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Replace spec with the same without comments
TlcPermuteFun MultiLineComment False Passed
a7608a583667b7a24badc1a9b961b50e758d00f8 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun BoolSet True Passed
aaadf43b063a19498afe10922080d6c88d36ab27 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun BoolSet False Passed
086f17286213ac6e00b1419519273b6e0a6cc32b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Let True Passed
b75d5b5863d79fb8a5620f5fe8b4689886b33f26 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Let False Passed
197001680529a23f81f538165c93c36df82b4e96 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetEmpty True Passed
aa94100730caae26f12f3dbe63bf57dbfb558506 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetEmpty False Passed
ba99548442a8cb03a738f94e280ca709b7f5201e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set0 True Passed
eab7eb8d73b3f48fc0e18f64279603385880ac87 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set0 False Passed
f97ce67b3b9ea98b71f566074bcd0bead9e04cde TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set1 True Passed
3905ee6ccfd4006ea8acae80be1b937af4fd6c63 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set1 False Passed
2b64300a43962ecf1f927a65760c67a5a1771d58 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set2 True Passed
ece313d99b47d268ad0fc9958744f392d9ea117d TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set2 False Passed
8c48a668f714fe8267a80367d808f31135112af2 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Choose True Passed
54ad3d1bada91f01c5df9501ccf0c5f0dbce5d6e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Choose False Passed
c577d052dc08e84aff43fe6741f212bdf3c60447 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun FunApp True Passed
e18f3384c1014c2fc4f1c9950001300c8a070861 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun FunApp 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
15cc42783c2ae862ae49e49daddaff6218d7e34c TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def0 True Passed
19036903735ef0c025afdd60316e1eee6d9d0661 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def0 False Passed
8286112fa5cb033a55aea17520b429b4a013c9c1 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef0 True Passed
a5a6bb6546ddb57ee4320482f02bd2f88989ffbd TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef0 False Passed
8b9d248f06527c60d131d33acef18b77b49ccd7e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def1 True Passed
eff1caf06bba3b01df771af4f26d6f718629fb07 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def1 False Passed
99f960e99c625a84d50a09210f40736b3e3fab35 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef1 True Passed
919746ab78b100984ca5caebb6337ecc0591454f TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef1 False Passed
4b9f4c8277ebb93052eb4a4e2da693a3fb942ae3 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def2 True Passed
ccb0183917efde3adf5dbf9c78792d88aacfe60d TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def2 False Passed
295bb75a8b74e3782a916701077c2e23669af378 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef2 True Passed
ead54ae998624ec096bb30948423a9ed6001e0b4 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef2 False Passed
35111e9dad0ef29d6185427b87fa5496e441d825 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def1Recursive True Passed
1a48ae6071c3412536852befac8711af46d5fc99 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Def1Recursive False Passed
779ec65dd63d78ed1a5bfd6d400f01f10de919d8 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef1Recursive True Passed
9101e5d7cc4bb7a96b7d99b5d4384dc36ff60d20 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: LET definitions are reduced to global definitions
TlcPermuteFun LetDef1Recursive False Passed
5741b3274c3ef0a573e7d061c66772ad71946086 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Extends True Passed
5ed145ce14d7dafe35d150a6d1308cf9342079d7 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Extends False Passed
4166d9da1f79e61172b87cade705a95f2c21c6f5 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ExtendsInDifferentFolder True Passed
1da6a479f8c5a174b5a6a613c9a63dad7d68292a TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ExtendsInDifferentFolder 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
965930c2b44bc60bcdd58f193dd32bf7d066eb90 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Constant True Passed
25d7db20b9ca06c572086471131bfe5568001394 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Constant False Passed
fe5d70f9989255d3a7932aa2ac781937b2c3723b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ConstantRank1 True Passed
1c3b56b68ac5fc968027abc9765cabd119045730 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun ConstantRank1 False Passed
b77881c29cf1f8a5cf66e43cea74de6de739041e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Instance True Passed
a3faf681ff6bbdb47ce0c82761c309a2de2c35ab TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Instance False Passed
a59aa32ff026654bc12104e12ffd79595d9b1f02 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceWith True Passed
e07e376722c872272db8b42492cec799b24e6908 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceWith False Passed
87e7a7a6ad7899d2f943351ae1a2abf528c6adec TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamed True Passed
ef7a7d29a165882be973afe34ff4d65d140f78b1 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamed False Passed
878a7f22fa3e12d025fe5cf98bfc87c0ced4d06e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamedWith True Passed
5ef6d249ae92fa89b45c002ad6eb373e131013e4 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamedWith False Passed
1bd9ede7984ceb819291d2aeb3d328aad963b538 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceInFolder True Passed
32de3be4b90c748f30af0cc1ed9a19b8a58cbced TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceInFolder False Passed
9e7bb06fe8924d4f66bac71da122551adaa14e24 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceWithInFolder True Passed
bc554efff5e0b79ab22290f8890a19275d93a689 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceWithInFolder False Passed
676b95351a3ba8ce5efce9e7d6f1578e72ae91bd TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamedInFolder True Passed
f247b6866cbbcddcb1febdfe3562f527a19ca8f6 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamedInFolder False Passed
8faddf1a8a389e2d34b25d5b871b34a154fb5882 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamedWithInFolder True Passed
d58e56b01e8a555703195db4d7af62498ef7065c TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun InstanceNamedWithInFolder False Passed
b5cfe56d9b10614b465391dfd6e1ffe34d687b13 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Cross2 True Passed
1fd49406e892ebf24ae846d66f64ee95a517f253 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Cross2 False Passed
13e92d5c59deb365f1fd3a335ddfadbb81804f3a TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Cross3 True Passed
b937c9d2117c4001aa8fb97756d17727b2f17520 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Cross3 False Passed
67a6f3f6d030ed7389e74d94bacfd765aadfed70 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • 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))
TlcPermuteFun FunSet True Passed
f3cb1317500d9d520f4a55f3bc06b3fec72544b8 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • 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))
TlcPermuteFun FunSet False Passed
d28200128de2bd7db503215f710bec4d474d9ae3 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • 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)
TlcPermuteFun RecordSet True Passed
ee3dd35083d9486734d3ad3d2bf86f3205349d10 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • 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)
TlcPermuteFun RecordSet False Passed
07b212f9a4453704c03c3e00f28ddd4279bf6791 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetDiff True Passed
993ce246d3708eaacdf04f1a0592d323dae1b733 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetDiff False Passed
409205b6cecf09efb85a4b3bf80c4142c76aaef6 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetUnion True Passed
210aec81b32e23640871e36c3ac1a47fe72ecf2b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetUnion False Passed
772525ea7204ca2240834c52f5e4837881b3c717 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetIntersect True Passed
8a7bda1bfa88d7e0108c0127e35266d054758949 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SetIntersect False Passed
2dc1f72e403c29f881fadb229d696d6e32d3979e TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfCond True Passed
15cf594d51d1c10d05727115925048dd96106518 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfCond False Passed
aba620854905b63133e9dd8633a830d3cb19b94a TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfThen True Passed
99a30ec01dde29f5b9a8507185984cb5360c14c2 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfThen False Passed
5c977e111d27a8f1011735e34341f3c18b87a1bf TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfElse True Passed
b581d694194f95ec2830503759571dfc4b5cb094 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun IfElse False Passed
bf9f3d0f5935aa2e7c00258e691f3c1bccd99e18 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Subset True Passed
3f0bbb47538d6896beed3df1cc87dd9c78eaa54b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Subset False Passed
6322c0562b8dc31a5b00c550ba9c775d65668949 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Domain True Passed
b9bda0f0fd8d8c5df85a028253b21f4b42fc41ce TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Domain False Passed
1c3c18c8319e0a171d965b24353de2f7728491e7 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Union True Passed
fc99661f370368d6b56d44782d6e6466512b6325 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Union False Passed
8bfbb45d9fc630a4aec03dfc58105669b32e36f1 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • 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
TlcPermuteFun NumRange True Passed
4b785f0addf2a1699d7967635514b2d839a5a6b4 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • 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
TlcPermuteFun NumRange False Passed
81e22650cb38a4bc83515e7876de193f3b641ca3 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun TlcPermuteFun True Passed
b2434f93a6fde990156aff4238b3230ca2665eed TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun TlcPermuteFun False Passed
8b271be15df2aa19459fff7cdca2c3f207a3cf6f TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcPermuteFun TlcEval True Passed
fb0808c8f39a811e3fc466baec7724cc183d2d3b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcPermuteFun TlcEval False Passed
fcc91c01b7fb0c52d701758b52449049228192a6 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun BagBagToSet True Passed
42da04f6eb76d04bb7b05f23ac67f0225290c86c TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun BagBagToSet False Passed
c9f7b64adf75eb9622c6c9022739f2f0edcfcfcd TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcPermuteFun BagSubBag True Passed
f3f737c8008814227b1b8692b16ff9bb905a10af TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcPermuteFun BagSubBag False Passed
1d1030093473d323ebc1c401358a652cb9e0a884 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SeqHead True Passed
293a418a2b50cb78485ee6b8239d96f068368be2 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun SeqHead False Passed