Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
28834479bb0baf06dced074027b2c3d8e90ba8de TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Replace spec with the same without comments
TlcSingletonFun OneLineComment True Passed
6717d3cb6feeac7f82a8191d9026bcfdafc2d3bb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Replace spec with the same without comments
TlcSingletonFun OneLineComment False Passed
3513a995735d53adc202bb031e0f3fb86213ad83 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Replace spec with the same without comments
TlcSingletonFun MultiLineComment True Passed
f69b769b99494823b3c776a1c6d59c7132dd275b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Replace spec with the same without comments
TlcSingletonFun MultiLineComment False Passed
5ce2bf74252fac06a8f2535b305865733de548ef TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolTrue True Passed
8a0b86a4e210bedf951b4cbe544ba0d5fe3719dd TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolTrue False Passed
0d8c501100d53ad9df6fbc5ad9c7ef4634a05b39 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolFalse True Passed
b5061aed8bdaa77bb01b4c0ffa9dd645bc196f4e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolFalse False Passed
7d822ae7d8cdbe615314f4eeb5460e3d5754e05e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolSet True Passed
db0e77d8cff90452d6818198bb0be6a9dcf87aef TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BoolSet False Passed
e1df42b4dbd1eadb9657d2d532111e0686fe93b1 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun And True Passed
755874a1745bcc47247bfb5ffb1be40c3eceaf0d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun And False Passed
619a2aef1c693bb624cd41d078b07970e91c876a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcSingletonFun AndMultiLine True Passed
9ac6c9ecac3913770a3bfde26ebad9a5f630ec14 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    /\ A
    /\ B
    == (A /\ B)
TlcSingletonFun AndMultiLine False Passed
873f9511dea9947ba6f90693b39c8437f4ebf457 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Imply True Passed
bdabd293d6ca87d65063310238876a28c3cf590f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Imply False Passed
6f82028fd2765f9d4201a0a215b26ae2d631f43e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Not True Passed
28e09122612cf3c3d109441843f8870b4637e443 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Not False Passed
73bdc2d0da8179f6cd34d921915bf500e74cee49 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcSingletonFun Or True Passed
7984a19022d1484bc13a0663763e638d117dfe6e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: A \/ B == ~(~A /\ ~B)
TlcSingletonFun Or False Passed
08ecfa6f33c4f7331c0f59e1282478e95cfbb0dc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcSingletonFun OrMultiLine True Passed
a1e3c5795677ed9bb7967c31e5642f6086d31427 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature:
    \/ A
    \/ B
    == (A \/ B)
TlcSingletonFun OrMultiLine False Passed
ee8e911d5572178718c8c94b33649edfbc7ea3c8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Eq True Passed
0fde6dc525cb2a80c42344a0a9f13ba90db0491e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Eq False Passed
50ec20e190d2fd7b97a8acdff777da5665531213 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Ne True Passed
eb61246e86c6ccb73ef2de19e3b46c3b28588e19 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Ne False Passed
4cbea1160b877bbc64e2e5be77cb65fb62df0986 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Let True Passed
de41710e9a98d3da215cd24b9da210fa04a80926 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Let False Passed
8b1eeb19883a9026284a40d27176c42647ec8a41 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetEmpty True Passed
5e4499d2407b33be80f24c7e80ae68a0e589aea4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetEmpty False Passed
3cb2de7433d36ae76d2145d270c968e083b87496 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set0 True Passed
b2b107980030e30bdba65df4f4cb96a067df1011 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set0 False Passed
b801084a27c312a39e6501f002e4bdc5d686a0c2 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set1 True Passed
dca9df2c930bcc6547a16db7c2849997cdcde1ef TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set1 False Passed
a9473a8e93eba52d8452315b1173c6aa620e0b7b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set2 True Passed
64adecbc09e71d882e35afaaecf9cf8675f1961c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set2 False Passed
ebbfc5c961386d8477bb2e8653393c6b34a26c09 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Fun True Passed
41bccdcd7456b9aecf6272150a3b08ba7bb8b496 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Fun False Passed
7f5f68f8fc05a57bbf326c85ce0c41305984e8ba TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun In True Passed
f7bcd11eba114332e43ac64863566c56b0171223 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun In False Passed
b12417e1a57e1dfac6cb0ddf10287142ca6c812b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NotIn True Passed
5da4017a811f5b35ee0c09199ae2271430f93825 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NotIn False Passed
630f0b23f8ee31060c382b77b1bdf121c7d170eb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Exists True Passed
60225ed731f52901b9cbd7e6875ab0994e6715ff TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Exists False Passed
d8c561952aa0127ac77a98622b29c2593bd170bf TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Forall True Passed
08ad44babb69dc7598d4ca85ec70085ba9922aec TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Forall False Passed
68d1d10badecb31f828887b46b7a4b80b51f335c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Choose True Passed
fcd1a06aa387c70af5d80d4198e6860309fb46a8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Choose False Passed
50db38cacd3205c5a1b72072a7163bc2314eb10e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Record True Passed
27af4338bce2dae759774c79bd701826456e0dae TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Record False Passed
161cb8db9524de6b9e9c1b025940870a59187730 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Tuple True Passed
5657b8417b8c43ad5f0070e48a713cadf9f521e7 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Tuple False Passed
88aadf19af2a0e12207bab28432286b686070bbf TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun TupleEmpty True Passed
5ed3242a3333a410e46f1aad715e766df023863e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun TupleEmpty False Passed
37035be2293f5a3e47d48d221a2a40f24fd77609 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun FunApp True Passed
bbb168686f7273460df767f7c67a4484e374b452 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun FunApp False Passed
6f2cd44d0ff4213abb61e1b205233e93f6904a18 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Prime True Passed
d00b1ec1f9ba76bdde285b33d264c37430e9e694 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Prime False Passed
bc07107b406c9747f56f331a004eec1ff085940c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumZero True Passed
33c673ada05527a2ccb7da9711377cc3c285b078 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumZero False Passed
79156316718bacfc91a3d28af8076b0dfddf1fdd TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumOne True Passed
11f0573735af0c144ef7c81563fabb9363c4487b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumOne False Passed
bd31bb0214b8ede54a4d9ab6b93afe8b4c7fdf50 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMaxInt True Passed
d0fc5858b4c5c8b8c0e5f677f36a1482202160da TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMaxInt False Passed
058eebd2775c16db87bb12d50b273915ee66fdfc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumUnaryMinus True Passed
5caaf1ecaed78d6937c2a3c7658f8b01cdb5268f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumUnaryMinus False Passed
5fc9666eeeec69df80fda3f4ea7285c20fee6820 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumPlus True Passed
0ceb916f36098b5b15e8445c49294f5766e37fe6 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumPlus False Passed
1154ddfdc2a5ea86f5db13305d7b74b2feff977f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMinus True Passed
84b0366f09b40cd2582c3a1b51027fd7f1c9673e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMinus False Passed
22cce2294dcabac0718ac41a9e006759afd70a39 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMul True Passed
5d92a04560d5498f2964c260fc6ea63d586e6def TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMul False Passed
c1451bdf218935acea24bb95526ce8a2cc4a2d26 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumDiv True Passed
efc2d9340593db27c4be6ea376a5a5444d3641fe TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumDiv False Passed
1fd339a218ad09128b18094a5377b536f0788e0a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMod True Passed
27a470c19f9952f1d143201badaa19e653a1fe16 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumMod False Passed
07bd9d677fa254ba9b0c7ad6e6c9acc04d658cf6 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumPow True Passed
f419930d76314f385727126981018bd5d61d71fc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumPow False Passed
7080e4b55722a627c0bdf09497eed7690e719fdb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGt True Passed
4bb1fd5f4eee8a40629ea601b172e5d613be74a6 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGt False Passed
28d950f41706c89c3e4dc791b91cd551a61b70ef TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGe True Passed
f7955778556391c7a64a9dc82cbc4ce6b6a79c17 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumGe False Passed
87a2e75f06888e342c8ffa31cfe24f1eb93e5c73 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumLt True Passed
eacc8d80d54538d4a31e4faec67f77bc382555b9 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumLt False Passed
bacfb217ed6ae88abedfab55adce0bfacb4d33b3 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumLe True Passed
7e708c474bc9568e207a6d9c9d16168605dc8b33 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun NumLe False Passed
f2a4b97db6cb993dfe7bc0d9d0638079cf2b53d4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun DefFun True Passed
d3eda6f8391d82386a62007e1425ea3ae08e4d9a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun DefFun False Passed
b33df3dea58f42e98a21a6b4f3b72609c9298a8d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDefFun True Passed
9bcfc15b527c5a268e9b623cfd907383f448982a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDefFun False Passed
46afaa02174e3c23301920c941195cf39bd7a4d3 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun DefFunRecursive True Passed
aa9ec4ca55866f9c29428a452db86a3bbd4e56cf TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun DefFunRecursive False Passed
510f769881e670c200a1bd054b5132754a492673 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDefFunRecursive True Passed
d65a5db15d4ac29edc1d2c4ed648a4d70aa0ea67 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDefFunRecursive False Passed
aa80e1a148a704bb0c9ee82da750ef860e641d9d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def0 True Passed
04158e7409e03db1ee294f2e2c3d6036f69256c5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def0 False Passed
7126b5f34183bdcbeb98805f15a3f4fe579dec09 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef0 True Passed
dc97071356a6ee4dca52130d5e557f4ebb6911cc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef0 False Passed
fcd0526573ebd9c529c29b93fba35efaebf97eb8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def1 True Passed
e4a014f086a79a6f7e2bae2746a01d9ec15c0ceb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def1 False Passed
82be8a05672c277f36d728649703f47c434cc52b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef1 True Passed
8a41d1aa643a11cf2437abc9d470970c5c08d4ac TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef1 False Passed
65539af9c5c3bf57d4a2cce2491019e85dab0815 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def2 True Passed
4d7882b2fa713badeb19539c19b1ce559699b579 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def2 False Passed
c8dab2d39e4bc3600467fa4f1b128048ae2272b0 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef2 True Passed
2e294b8dadcbf077c1548945ad09c2bbfc18a4b1 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef2 False Passed
33390c559c07550ebdecb65f8ee4d150e102cfdc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def1Recursive True Passed
d54797112b1245af1761ab0a9597a382fff2f4cd TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Def1Recursive False Passed
e6ae4ac0e8e1376ca33ab212048168178119f384 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef1Recursive True Passed
94539d9a718fa3c527d37c76521e8e0dbf7357e0 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: LET definitions are reduced to global definitions
TlcSingletonFun LetDef1Recursive False Passed
4b33431f9b4e1db68af11accbce627f1b1b174e5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Extends True Passed
9175e9f24cc269609be6d51bffcf9377bd87b082 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Extends False Passed
88520bc3b22ba4fabb49986b6eb9e2559865d252 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ExtendsInDifferentFolder True Passed
04b36442037435e774f0fa3a274507f73dcedaf4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ExtendsInDifferentFolder False Passed
bb40014fe1530cc319f0b1b04b280c153ff85b99 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Variable True Passed
c76ca105eacf0399af2d2d39ff9470642bdc2821 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Variable False Passed
c3758783101a59985b944aead01d04f93bc93b29 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Constant True Passed
62235f434a2a5f837b0aa01a9958475fa6eaa805 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Constant False Passed
373f8e58a87e7b25cb68b3c6ad16a9f65fed152d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ConstantRank1 True Passed
3c890897cf76ce29b9b49547adf55c10d631abe4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun ConstantRank1 False Passed
a99ad677ea429d2f52993cef235759709d1cca40 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Instance True Passed
bbf32d0ad0506f64468357edf57aef64d9af74bb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Instance False Passed
5b7b11a0032d5459be3d1139744bb0d3760a48f7 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceWith True Passed
85004fada3df35e6f0f2a392a8dbf3a12c01c488 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceWith False Passed
78e0fd9afa5c262f197890259e6d6f5bb0e6487a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamed True Passed
79aecbf9bb6229b9757b1e454604c8760d41c869 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamed False Passed
68450499ad4ec583a8f008025b48b8bd9961751f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamedWith True Passed
c2303bde107871a87dd1eae61601bbdafe054413 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamedWith False Passed
b966856cbfb603b0520e6b860ba7fe3c3f263a49 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceInFolder True Passed
1b57f3a98390c6eca8093c7947858f48264f7b30 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceInFolder False Passed
437e189654a7692f8ac1abb97c52c1a9c9f251e9 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceWithInFolder True Passed
7f9f0a53834a36d5f93256569eb588e5464d2acc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceWithInFolder False Passed
06670321afe5d41decd9999e1e095692981e67dd TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamedInFolder True Passed
446484dabb639e6d0fd858e8037435d6d58bc945 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamedInFolder False Passed
f7248deb81fe2a93468470966e7dc46cbf0d84a6 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamedWithInFolder True Passed
223f647a310f6d5277d60e0952a0ff48d2567b62 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun InstanceNamedWithInFolder False Passed
26d930dc65d4b20ad67cb3746b167448cab15406 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Enabled True Passed
ea17097df405ddfae96e082f00e1cf3bc41345d8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Enabled False Passed
b869f2e0c10ffc0eee088c134a233754d28edc51 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Cross2 True Passed
c8757a40bed5287be80be978141e8035be7c2e3a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Cross2 False Passed
106239261bfa6ea4370b1392042a072a8041c7bc TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Cross3 True Passed
249cd502124bbdc1625a55ed0c5c430220376795 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Cross3 False Passed
809e20f2b886d521980a3eb85669e6070dbe86c5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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))
TlcSingletonFun FunSet True Passed
66c593a4d4c37ffd03ff0a753b0cc10a1088b094 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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))
TlcSingletonFun FunSet False Passed
ab46bfabe8b62f190ca11b0023c0fbcf00f3301b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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)
TlcSingletonFun RecordSet True Passed
84002f6e4e39c45aba841567c336339f3070878a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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)
TlcSingletonFun RecordSet False Passed
c01027129018945a440cf429f9eca7f6e75ff7b8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetDiff True Passed
2353dbc9dbaf68f8b1f3b43be3655ed4d97d9a98 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetDiff False Passed
82b2fb369c77c8958ae6e9baf125d2f9ce1a6d3d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetUnion True Passed
f685f840d03124d16f4622332513683eecb7741d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetUnion False Passed
6dbd3862073d98f4addd348b6c73339219607d4e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetIntersect True Passed
80e58a0c2d00c75eb1ce6a5fa3480f64a8cb107f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SetIntersect False Passed
7d5c444841bb6093a6561a8cb4df11cebf56170d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SubsetEq True Passed
526f4e0649e7679957807b9f28e759d21e4b4629 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SubsetEq False Passed
43d0f7d5b086add62d5b900f63ca69271c7bd2d0 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfCond True Passed
594c83de82b1d40db18ecb63cd69acf30103f8ce TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfCond False Passed
974c1f3db283ae371eafb533326d60b9a4c8f13c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfThen True Passed
74424c60171bece101939e8b880409920a4702db TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfThen False Passed
eae1eef7361ea3bcfa35a7e5c39a7a05a862bd15 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfElse True Passed
98b05d8f39a81089b34a761e1061d5611d9ee6ea TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun IfElse False Passed
f9558ceb65aa1465c39c0c040ce8c0a2bf7f1514 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Subset True Passed
d2120fdbb33821a27b5c7e4464094454c34194f5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Subset False Passed
2848add887442d497f249cceedf3b33b26535fcb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Domain True Passed
0a352e865a2944591b6b57c781027dafb65f0910 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Domain False Passed
c9cab046eb3ee36ee56da90440e9535ab67b169c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Union True Passed
e791e9ba362d9db38d4496f103334d7aeafb238a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Union False Passed
e15099bdb69349c17bbe73098dfd646a91d831ba TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Unchanged True Passed
ed5b36fd4be44d4d311aa22d5058f684111a3b07 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Unchanged False Passed
5744e8f565f866cf37bd3c49aaa10bbc5ca0dd29 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Equivalence True Passed
faef683d22b33aa4736d5eff367a89848dd5009c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Equivalence False Passed
805a3e15db62b30d8362b6c09abae55240abe94f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun StringEmpty True Passed
4ec4cc3eea9970392d087ed8ef909d9e52950f34 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun StringEmpty False Passed
ff377c4c92e2243b3b5519ae7b919407dbcdc94a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun String True Passed
79a1a82d74af3e05e84e76936b8c6d4f97052d03 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun String False Passed
c3ccf9c69adb6555537fd6a43ca164c2db8f2c66 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqLen True Passed
50ec207fc4d6804ab6e4143d63b46c4624d9da85 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqLen False Passed
d99e52674e4b0b8685684bf88b1029e12e982570 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqConcat True Passed
a65d94fd71ea6443c6642052627c11ed43967cca TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqConcat False Passed
4a67e2058979f9b391e17ddd47e90c8a258b13ba TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqSelectSeq True Passed
3bc637de7714bcc3b4cd030f98c78027d802299a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqSelectSeq False Passed
b8ff613352338ded148a1c27965b83e7a2b4c8c8 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqSubSeq True Passed
02d16719a38489158fc87b6ca47196afd34b92b7 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqSubSeq False Passed
40adf3a1cf593329453f2a90f720030f6a37f736 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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
TlcSingletonFun NumRange True Passed
4de5379a313cdd420a6e9c6b7fa0aa559a15d9a4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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
TlcSingletonFun NumRange False Passed
d8cf5554b566b916814a4e48ae44069d9aea8c90 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun TlcSingletonFun True Passed
b5c7b007a049e24e000bf3eacd100bab3937ff2f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun TlcSingletonFun False Passed
8ce7e62b5da2deef59b4be60c1a4306523765d38 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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]]
TlcSingletonFun TlcExtendFun True Passed
9caf35544817f14a1f69f6b4b8291e6a0f243b8d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • 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]]
TlcSingletonFun TlcExtendFun False Passed
386390a0ff8e09311c4ffbfdd50f85a1b2218076 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcSingletonFun TlcPermuteFun True Passed
76a167da929ad4a3e36a3892bbaed7d95cec5600 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcSingletonFun TlcPermuteFun False Passed
6e35f6241906f8f9ae8cc3f265192f9b05a06349 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSingletonFun TlcSortSeq True Passed
abce4f3a34ab4b1f9150ea8a83538886723009a3 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSingletonFun TlcSortSeq False Passed
374c3462f59ba155b098477b88cdd38849b3c295 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcSingletonFun TlcEval True Passed
a478651420f7e036325f6db622315c2eac02ea42 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: TLCEval(expr) is reduced to just expr
TlcSingletonFun TlcEval False Passed
f3c00713b56e9465274e6e1b7c6efa440c82dba9 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagToSet True Passed
8405ff94e2713eddf6102507725259c41d56f338 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagToSet False Passed
7643252f9b892141427f323f3227b669c667e89a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagSetToBag True Passed
e0cf60176cf68c973f0ea15bb7a73ee096dd5d6e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagSetToBag False Passed
21f7ad24e1da031ab354d089f478a8504f51d103 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagIn True Passed
7c4b5b559d24d3b31b5ec8c4e6be542d5138de46 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagIn False Passed
1b82fd7a03e5740e80b16618f055baec17477b6e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagEmptyBag True Passed
8878b745d26171ac4036509122e86a8e939e85a5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagEmptyBag False Passed
f25fb87ed65c2a1f1ff97542450b95ece87572aa TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagAddBag True Passed
5723973cc784f316a191e42dec755e4ed0193c73 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagAddBag False Passed
e07e395d7ca527b11f98d7eedb868a512ae666f0 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagSub True Passed
b005280f625632ae29a373479432b403b52c6e8a TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagSub False Passed
d782b0534496b00eec09cf76d302aa09dd2a8940 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagCopiesIn True Passed
77cf6eb6b1481e73b81c525166104c6e0243a66d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagCopiesIn False Passed
42c2298cc03facef64d3b54cced821ad184babf3 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagSubsetEqBag True Passed
4c34634b60d20c1f418e455ce4b1eb6ef1b0fc3b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagSubsetEqBag False Passed
62366dff444779d4a2e7bc4953b58730cb1c8d7e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagUnion True Passed
81b70a8f693f47abec9b0472cad85fe4f7b10263 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagUnion False Passed
8a7d051096531b11e8a748048dc53b33013693cd TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagCardinality True Passed
65d9d63f69d9378ab2a5ee5edaba71043cd18352 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagCardinality False Passed
ebd1b463210f86033171392511643b2cd57bd8c4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagOfAll True Passed
f8eaac6a6337456690d89d104b249df5dbad3869 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun BagBagOfAll False Passed
009df8d915395b9df069093006b1655dd5a62b9b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcSingletonFun BagSubBag True Passed
b241b458b76c3ba5f0881c04c2f2eabd3f1baa54 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcSingletonFun BagSubBag False Passed
236383e2647e8e063f55bc4abc371bfebc7c3240 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcSingletonFun FiniteSetsIsFiniteSet True Passed
e9296e641cd13aa33cae1a8fbfe5c3d99e81397f TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
  • Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
TlcSingletonFun FiniteSetsIsFiniteSet False Passed
a520caae0874a9cd0ed703d965a33de17f0ced1e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun FiniteSetsCardinality True Passed
2a3d88bc4fc2a45772218072503332624b383f29 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun FiniteSetsCardinality False Passed
de7a8f10a0cd873449cee8ca6f2c31cdaf87e64b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqHead True Passed
94e3a82bee27db9ba8b2a87a61d3a988cfdfce24 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqHead False Passed
470e916f99b63e964e411608b19cc2a0d71f96db TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqTail True Passed
8bf887803ea67e0d4fe3284ffdc7556cb6ccd4e4 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqTail False Passed
1067d048089f430bd7b6a2183ca269a1b565d5e9 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqAppend True Passed
cae0add6200d1fcfe49748eabf4c5cd622e2fb5e TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SeqAppend False Passed