Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b4b0ff4dcea4477660fdd96ffb94bb615e6fb577 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Replace spec with the same without comments
TlcEval OneLineComment True Passed
6800c81c75c860212c0f427e922664ea0b420cfe TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Replace spec with the same without comments
TlcEval OneLineComment False Passed
580d57cd47a86b60f4fa0b78fad210e2328c2348 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Replace spec with the same without comments
TlcEval MultiLineComment True Passed
a9e8e1f7e72f30d1a1537da98f51ded25c0c815e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Replace spec with the same without comments
TlcEval MultiLineComment False Passed
590f14181374d45bdf6035dff8c2fcb990651664 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolTrue True Passed
2dc0a4d66854fd97ba2f8f1d9b8b7301e7b93a51 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolTrue False Passed
99859ccbe0a85f6b0a1e403e702c83aee3335151 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolFalse True Passed
ef5dc9f851b9ded0c21e3403eb6cca3e64baa69e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolFalse False Passed
0ad458dc0a660695aebba3af57c4608ccb86e860 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolSet True Passed
91021823b9eebfce650f3cd9c7480cc77c43bd27 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BoolSet False Passed
238357c05cdd1baddac0c2203a237f43c0f47353 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval And True Passed
c64ca0ce7dbfd6ada086bd0cb1b517e04b607cae TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval And False Passed
2337288fb60b027bc2b8b2fc4b6ca9d874ee089b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcEval AndMultiLine True Passed
a09a45b2a2c5ac11e35dc23868d33e9f3804ae20 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcEval AndMultiLine False Passed
6173117978726a914edb9c05c685a4a4a3993e3a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Imply True Passed
dd56eb7fd88bac0e2d9c7a108f87fa64bd934f50 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Imply False Passed
8379b3b86568127fad0ea572e0d90f0cd2ad1c83 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Not True Passed
6042d287e7317d62b771df43a2850a9b25f40a98 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Not False Passed
f2be1b679f497b89258b35ece61b5e31453a32bc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcEval Or True Passed
88ba92ae36fd1a468921c93ee0a6d01ab96cc025 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcEval Or False Passed
aff1fbadf438a5722ee0534a58332c49193e31ae TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcEval OrMultiLine True Passed
060c4614afbb24d6f6e60b8c724491ff11de03fc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcEval OrMultiLine False Passed
1cbd2b0944f5448f04a3a245c0708092ad5f1c1f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Eq True Passed
18be04031106b0feaa49c6958aca1b594b8d004e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Eq False Passed
3a9c1a49de6670db9cf670df3fd2f94471617c2d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Ne True Passed
9bdc3d29f39368a3c3e3e56aa60441e7110e21e2 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Ne False Passed
0066fe48f7c9cd549262ea1487353628101b7a95 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Let True Passed
2fc25103b839389d551bf788ff7abf1a9f44d221 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Let False Passed
edb82c1105efc07e263284c6fdbee962f67ca4a5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetEmpty True Passed
ef777d9cea30563049c9def07ccbf31fdb2f29c0 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetEmpty False Passed
de4c4534207d2012501613fb65919f61bd81be9e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set0 True Passed
49af65d821d972d55d954e3600e02036580bf1b3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set0 False Passed
178c457c55e1dd69c1c96a01e9547ceebd30ac9e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set1 True Passed
2dc34db7120caabe497de80b6d53bc8209a83432 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set1 False Passed
f4bcb7b3acd4754cf4b8b87397ac2dd86c778866 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set2 True Passed
6ad601a110bf85c61148f0640a21ba1be94e08fb TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set2 False Passed
f87cf948e84b1e2da903f3c4caf115ad41efcd75 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Fun True Passed
1f94ca3ad7d61e0b46c73960b7441a7e1d821a11 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Fun False Passed
8fc650f5986df8b8ca0b35c9afff46ffbfe4e2af TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval In True Passed
fae292342b0a93dd6f8378fee1a544aea0b78a3b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval In False Passed
170c209d32ee0e62f04677356e16c27251f31080 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NotIn True Passed
8b31f01d78eb25d77b0db305254d168e1d9b9d13 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NotIn False Passed
bc8f8555b111ac116d64ecec262ffe983e700d6b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Exists True Passed
f5a1b4a1bf7cca773e0cd6e6ef2f45d83515960a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Exists False Passed
161d3b01ed4c59942ba7e6ef464ca6a7df41d345 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Forall True Passed
9fe552f823db8aac3e6452dfb105e52d4fbf032e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Forall False Passed
906c0afbf9fb6dfeee89c2ca43821d112e6eef74 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Choose True Passed
5c6e67278cbfd2927579ee5be36ebf4f482c691e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Choose False Passed
59530bca615fc7e22e2e90cd44c1ad5e99f34fa4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Record True Passed
9414575a6b4b61b97a38a628cb68da817d23293b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Record False Passed
ee331d65871b1b54bb1034f2f2b137a54657b8c5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Tuple True Passed
612498eec8ee01b1a5cccb4bd90700635c3d00d7 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Tuple False Passed
4277d9a1dc0ec7d7672508f04d60df470613409d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval TupleEmpty True Passed
3408691c0aa395996e323bd7c9f0cb303c35aae9 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval TupleEmpty False Passed
825209bb144690adf846e9ce2206cb9b59329e38 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval FunApp True Passed
52f4d985da8ad334d8cb3f59e0d96d0f662e39f4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval FunApp False Passed
53f744bdc0da241a6cabb5f7be854607d8b041d8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Prime True Passed
46c12091363e7c56d9ffbacd4de2290787353c83 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Prime False Passed
814458335367b0ae569bb2cdf73648e0cb074a44 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumZero True Passed
251485109dcc48170b91eef6bbf51d73ac1b91d4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumZero False Passed
69c2558ba70dae67629c74111d2a87c362c11383 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumOne True Passed
2730a29235071918c01696cee7aca63de5d10be8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumOne False Passed
8eba09ae6c89a891535684b0ad8cabcfc677b821 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMaxInt True Passed
b0cca46d087f0ef80209d676bd62dcda40950270 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMaxInt False Passed
c8b00755c1cb55145eb60c1c1a4bafc6666a2bab TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumUnaryMinus True Passed
8417a79c0b5ebf3f8cdefcd24789baadfc2600dc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumUnaryMinus False Passed
62356cc495be509e7747e6c582117eed868030e5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumPlus True Passed
9d2e53c213410534282cafb1ce2ad307a436a0c8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumPlus False Passed
fa19944bed9315e0e0153734bf2a209e3b9d5b17 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMinus True Passed
1603baa382256471ce6af3e3be52aea70e39abf3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMinus False Passed
d50f85bce725a377b90e1dc8d6d2c58bd6acc58f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMul True Passed
17b1b6fb4cf9225908d8fa16dd5bb1530c1db286 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMul False Passed
cd364ab17492e0adf020494d8627c25992a89828 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumDiv True Passed
827a02f4eb181d31cbf39f9290187c44754d54dd TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumDiv False Passed
3f0ca684d1b173594a175af6cfc152eefb31ccb0 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMod True Passed
d6a2ae5361579283eef1c75e3fc85d483d2929cd TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumMod False Passed
3eccb2877f79ed85c4125a89ffc96d2bd4c30c48 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumPow True Passed
0d1d5c3937fc8b1d1db69040bf927e7fd845fc1c TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumPow False Passed
69d3eff51e8ef6011369a8cd6d3b479069bc8ed0 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGt True Passed
3fabf8b50ae6731a4925a8c9cb626892915515af TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGt False Passed
7ccff27968dae0c85e745e0b7a1c550be94fefd9 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGe True Passed
0e6c885f58f48310901dc55dbd31351ef3a38471 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumGe False Passed
e825ec4464a7936d7c4ae5c9558828e2a89de929 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumLt True Passed
c31ae8642f7acd9ace282abd60319f579d913900 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumLt False Passed
5a2ffce9f93084d073e94f0c436d8cdb339dc7e9 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumLe True Passed
a466e25dca2d6aaf1578eacd143bcf9345cd757e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval NumLe False Passed
4647264e4fae96c9724f33047d1d57945eecd1af TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval DefFun True Passed
38c8c3004bba7ba85ba127a99ba6a8a560225f7b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval DefFun False Passed
b2ce24bb72451118c651559f486d02d70185a3ef TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDefFun True Passed
40325cef33061efa83ee2ff43ed7825adc5ce069 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDefFun False Passed
2386eb299bc770a6b7ae2919cbecb8a7fc9fa098 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval DefFunRecursive True Passed
c3e52dcd96bcedb3abd40484b20e8a9483bec403 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval DefFunRecursive False Passed
de8b76fb289b9c0e0fc63078e0692e66091367dc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDefFunRecursive True Passed
8f149541dbcd524311e8254ba813ce36a2386abd TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDefFunRecursive False Passed
65cf7ab010d81d455638e06d16c25fcf0d7a1bd8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def0 True Passed
2bc6b58d506321941fb69ae59ccdb24ec45894fc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def0 False Passed
8a063ba0f15c347573e871efec8cf3ae43eeaca8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef0 True Passed
8926a21adc570c61365050605e36f963deac172e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef0 False Passed
981e2656c3da961cddfa73f2c387a5d71bb43934 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def1 True Passed
d55b1561bafc8752526f462d03096fbcb6efca37 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def1 False Passed
5a47b9df83e80e00b26453d3bc2e20698d7daf5a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef1 True Passed
f23bb62df2b1dbe284eebe91f2217e4a8b198db6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef1 False Passed
b542f5e901a416bc6029511480f9423e7cab1a82 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def2 True Passed
7ecac8cbf17fc5af00967d7fc8864cd548b3ab2e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def2 False Passed
f3925e125b803ab599e43b56c5f0ee948c71be4f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef2 True Passed
6711318cb3e95d255643d8b2a357b65630eb9b4f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef2 False Passed
e3d571e14e2fc1aca866b1bff5ee4c67ab8f791d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def1Recursive True Passed
14fb969f4fdfa4cd18600ab7ae725813973a8bd1 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Def1Recursive False Passed
a3f69eefff4704cbe8e62f73d3bc0814a225ff66 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef1Recursive True Passed
e3f03b2d601e50f3249d41d1c8076a08e297e61d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: LET definitions are reduced to global definitions
TlcEval LetDef1Recursive False Passed
a37cc50090020204b66541da975409e1679600b8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Extends True Passed
fc2200fe3ebf038d03c648c2dee5468d62938d94 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Extends False Passed
e66b64c8f2196f0b5dbe98e1eaaa025d74364599 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ExtendsInDifferentFolder True Passed
fbaafc57f4df0a0da8a5b056497a90d2b2666448 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ExtendsInDifferentFolder 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
66afb7288bd2e11a4a7e924f772eec019989373b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Constant True Passed
e3d66ad28a39ccf79fd7240d1705a43a3c8699e7 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Constant False Passed
c0e84e2f701c09dfc9094d2e965398186f35599e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ConstantRank1 True Passed
c8f2d2cbed13422fdd0239a4c28db39d552055bf TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval ConstantRank1 False Passed
20d538933249ae49f9ff28729f7596ddcfedb742 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Instance True Passed
99f68b306227034f0a8785821808c6475c4fb5cc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Instance False Passed
5f6e6906b7428b176efa6a90e040e32dc30fe722 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceWith True Passed
48012815fff2c2032d21c5bd67740a77e3d73cb9 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceWith False Passed
f4318cb94735aa37a6f32af582812fe4ab540a95 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamed True Passed
78c1e69f67fef1a4a450ada95f6aa77259e559bc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamed False Passed
c6da8dcc81c1eb72a4c2d23c5cf516fa19fc5d83 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamedWith True Passed
86392c24a6bf1ddd30ad673d89374220f54d63b4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamedWith False Passed
c7cccc83aac02b2dd4898e1541fd95a7828614f5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceInFolder True Passed
ab7f2d8dafba24691436a375edc10e9f00d28ea5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceInFolder False Passed
7744d63b203404b1b6510d930d5789b36bb95f52 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceWithInFolder True Passed
b09dae27529cf84e17a23639ceea1d6d862ca1a4 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceWithInFolder False Passed
76f598e4b9711954435f427838b7f3aa0a7424d7 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamedInFolder True Passed
14acf19fedce64a1dd9f2a5c07cdb33cf3a096c1 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamedInFolder False Passed
087c97aa7b3a0c8acd5f9e6bdc42b6d04d74d5b2 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamedWithInFolder True Passed
2bed4b02ed69eccc14491a9eb98c2c8589be3718 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval InstanceNamedWithInFolder False Passed
6970b36b6948dc812ce0421aa90e04eeac296090 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Enabled True Passed
78f0e09e726ccedd0cf0bd3fce796ec1eb5d164a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Enabled False Passed
793802826d937495e8b8f784a127e3badeb17124 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Cross2 True Passed
06be4169e967304abb4b51499b52b9bfcccfbc2e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Cross2 False Passed
47db8c2bbb11182309f525e7cb92e88ae8a33bcf TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Cross3 True Passed
b686a0555d3ceb352d9c993918ccc9aef6722978 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Cross3 False Passed
6e289c56df78a64e7dde7ff59da58b5b9e75dd97 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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))
TlcEval FunSet True Passed
7338878c7e53b9bb6acb2df7f197be89d18d3626 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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))
TlcEval FunSet False Passed
db87c79454cda4d4e46326ec752c066bd8f13b11 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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)
TlcEval RecordSet True Passed
17d1e467cd4cd8c68926f474da21027bbcb403fe TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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)
TlcEval RecordSet False Passed
87c7ea0e8649ef9b11cb74ac839f8e132a4a97a5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetDiff True Passed
9298aeffaa3b57e7dc89b598b578986083d65363 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetDiff False Passed
ce0256ce69429849c23526f8e063a45226b3b86c TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetUnion True Passed
fd31256cfe65b6e88532dba66609f6a307a83483 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetUnion False Passed
4fa553d87888e78c18580642b3c9776a5a9b97a6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetIntersect True Passed
9e355741a2f81dee3e707b6d21951c0ed2c00e43 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SetIntersect False Passed
2e5e3229ee1e7c01e181264b9586442885d62d9d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SubsetEq True Passed
3ca5b623a2db08e305e2269f2452d71dcc97f4d6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SubsetEq False Passed
241a6c887ce8cb181cba95846fb8fc3054f3192b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfCond True Passed
2235b88e31172dc68339b9f0ccc31973e8a780a3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfCond False Passed
8f8f379084ebd9203ff4c7e3acd4bd4b2001d779 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfThen True Passed
c11c1ccbb612bf41ac6e5df6c06f80498bfe49db TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfThen False Passed
c24361afdb68728ccc327ba4c6aa5671de1ffcb3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfElse True Passed
d5e514e0173ea3c90a4449bdb21c81dde1d2b8fb TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval IfElse False Passed
115c075e140397aa5569eb1766254731c81c6117 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Subset True Passed
7db96ec1ee44ac9d9e8549344264111854379d37 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Subset False Passed
62edd618da1becc4819246d9ff6a982da2a2a4f8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Domain True Passed
c081d2c8a5a4daf0a5ff793ae2c267e047726f34 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Domain False Passed
cecf1b1d345f21ad038e30ffa0247db86516eb92 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Union True Passed
1acdf143795809f513445b3290745018e092ceff TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Union False Passed
3e3db6ba77940bfdaeb396423afd6957fc489d0d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Unchanged True Passed
8883a35ffcc28e403405bd156f08af57ba6ce004 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Unchanged False Passed
4d8c4f6460f5fee462bbbb83cb1c45f59ccc362c TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Equivalence True Passed
f61c5f439d662b0b754c178273a646321bccd5cf TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Equivalence False Passed
a3f465b48c24dbe5e0fa6c10195fa15d8d32cc47 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval StringEmpty True Passed
18686f6d011399b425d3edbc80c6eb7a06913556 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval StringEmpty False Passed
90f7376eb95adb30e9fca23a4043fdfb204bbd38 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval String True Passed
9e37aa63e976720e9990aa99916a4a857e0cd9cc TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval String False Passed
ffde67212a90450a4411967fad7790f5945adcd8 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqLen True Passed
8a439ca6a11fb062feabe028416ad635ed7d3d21 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqLen False Passed
77458b1e3840c881c0e881d2b4fa147c1ae86c67 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqConcat True Passed
8d1f7fed665dcc64f62a17c1b86afcdf7746d5db TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqConcat False Passed
b7e3bac6740131f826ebf9cf735977a5647e6e4e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqSelectSeq True Passed
2e72033788f05aff3bc909e25f8cfdb4733a571f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqSelectSeq False Passed
4f96ec3d9ca1d3ad0eace6e50d6ef8a40bf212f3 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqSubSeq True Passed
829a5945ff38b96987b943f9115c9bee9b9a7457 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqSubSeq False Passed
f502aee272972d4fdca6a981717e43e265c6e893 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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
TlcEval NumRange True Passed
e2dfc1a37146de3389f20dc4bd111b448d79dc97 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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
TlcEval NumRange False Passed
5a61561c25108035071ad94e5a77f9361a00b04d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcEval TlcSingletonFun True Passed
97c626a835e1834f2005b2cd9dac16e90de69d70 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcEval TlcSingletonFun False Passed
6931eb1f55ace7c9e1b25d74b3997a30a502e503 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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]]
TlcEval TlcExtendFun True Passed
ccd9f84ce74cc67f90539778de00bdb4bf7ed5f6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • 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]]
TlcEval TlcExtendFun False Passed
d056dac3711cc2c5686558c67a18b4e7745ba5d5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcEval TlcPermuteFun True Passed
22d853b5c0d0121a02cde213df39ffe80ea50f91 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcEval TlcPermuteFun False Passed
fdd3b0e5a2003d5d7a5cfea7c72e1943bdee152a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcEval TlcSortSeq True Passed
3cbcfd3487ee55044daa2f0fa60ad9eedab03e1d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcEval TlcSortSeq False Passed
bb30911c94fcba2e5953a72f23062a4dd832d962 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcEval TlcEval True Passed
2923b9df5763d9cc48f675caef161744f1a2b9cb TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcEval TlcEval False Passed
be447bfb66628e0440817257da51036e1dfd1ed7 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagToSet True Passed
a23fe5c9bc78e86d20609ae9fb35c3cf48c5deec TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagToSet False Passed
1834e186a0ffcd11bea5f351b7043d3788fedf13 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagSetToBag True Passed
9698c33556f900ef345075b666c8dd1517d80a96 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagSetToBag False Passed
4f7847880a7bef8cbf0896aa15a8bafcd15b3242 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagIn True Passed
8a5d761ea722fb586f85f40ba5d07fa167a5d67b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagIn False Passed
88ff0a1080f1ebfa00baddb61fd25c7b5f791141 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagEmptyBag True Passed
f1a11d7d5adcd6edecdb8c5aed5f60896bd00ad2 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagEmptyBag False Passed
d67911051c9c651e433e70a30837fff383397329 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagAddBag True Passed
ceff100202cec479c28aa6a03620a12f3a7462aa TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagAddBag False Passed
d2c18668dc7974502653de3fe65bab6d5d37b31d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagSub True Passed
6af294bbde43597451b7c44fce84b03d63de52d2 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagSub False Passed
d453895b60081fc31df46e4ef7768ae7c3aaddd9 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagCopiesIn True Passed
6bc1b7538c2327cce6a917695d3757a034b34c3f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagCopiesIn False Passed
4f7ba4969097a7934cf2055cde3826b113c6422b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagSubsetEqBag True Passed
60270c822c6a6f61e46e9c3b8c538d0bcc99dda7 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagSubsetEqBag False Passed
e8e15466f13ba8dbe69f5ccf355bf39bffeb898b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagUnion True Passed
ac6533761865ec19939312660708cd20e61070df TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagUnion False Passed
50e08a870a5599aec22fa77894463937883cec30 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagCardinality True Passed
2c5299c6337ea609c5e608eb4a16b85f9fea6e8c TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagCardinality False Passed
2d627408d6d35245b2eb546c35df330181837844 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagOfAll True Passed
9b805f95f1ec71b7109e1563e1bc9eecd2e5d8d2 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval BagBagOfAll False Passed
b277bbfa6b61cc2970b48729016c16f5e2cdb360 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcEval BagSubBag True Passed
8734f1740605f5ca0a2742008c994c0da8321872 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcEval BagSubBag False Passed
3cd1e6588ec114e494c72a010fc723b038c39152 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcEval FiniteSetsIsFiniteSet True Passed
fff84e45bed951a3221991201cd0f6f9a0c89e13 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcEval FiniteSetsIsFiniteSet False Passed
e60752ba4bfbe780c9cdd4ec171e4f65bdc87d00 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval FiniteSetsCardinality True Passed
0ad8aeb6fbfe15facb016423e2d36fe6a207faf6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval FiniteSetsCardinality False Passed
a6efaa222dc1fa1af95fc5ced8f9f6d017bb7247 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqHead True Passed
612841233f12a71c41abec502e83e4671983e665 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqHead False Passed
780cb464dab30b09011f33a4acb0066ffc34d338 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqTail True Passed
ddd237336b810daee519cec67fb5875c8ba0b028 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqTail False Passed
8790e82a5549b14c8ced4070411f0837f321217f TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqAppend True Passed
5d9a0a75bb5bbdf82b2e1e3285e45646fed902b5 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SeqAppend False Passed