Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

Tests by plug feature TlcSortSeq; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
08071da95ac6b7094f601b95481bb8f9a2cd1227 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Eq TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
981212db543634f51de8d5dfe8cc32889373a2e8 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Eq TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
e7b69af17e79e0ed105101f719572e48b631fe3d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Ne TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
ccab69710a5b23ce3b55bf7c7cf9f05d489693a5 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Ne TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
761a7c68b590aa08311dd3f1e069844c4295676f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Let TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
57670d48df740c3ddf7ecf895bcb96db3307e970 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Let TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
460c6181575433a5e71e7edffbe269a0b4763884 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set0 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
ca702a74ddff802c30f4f524762b805c9c4ed6b6 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set0 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
ac718f46ef3e52a94b900e4861853ac24e515891 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set1 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
42268939beb2a4a29732bdc97d42534ce6cc6798 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set1 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
50b2711f0999abbd071f98bf0258bc48d7421506 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set2 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
486c4921f11862c627c4aa437d5edc861eced92b TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Set2 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
38a8f0fb2859714edd0647476b08e65d29187192 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Fun TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
af3ed8862c1bb966a8ee1da7da36e60ec9614035 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Fun TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
676e2336f89b2ce33ff52310a1682d3493d637d9 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
In TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
593c6e47b6e4181a13e273a4e302e3b49e01120c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
In TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
463c4eb866da7b6981e699b57630c1485c1f06fe TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
NotIn TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
11a3ab5d570f2133c063de73b153039b79712dd7 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
NotIn TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
d0bd402d0661b2ff771e50a4a0aacdc305cf2a6f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Record TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
47b89b2ef8d2b3cb29a04837171b7e2c279bbc3c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Record TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
7b78152ff34d8328e78830c7543ac2884abb77d9 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Tuple TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
95232a7fe8838fda3466c2a10673aa9987dfa897 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Tuple TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
8b2ae66b435303ddc9faf7de7a77edc5530c3cca TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
FunApp TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
88035c1886dbd865465f2e9a9d10cd7984e24a2f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
FunApp TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
8a727f4db0a30a6e675743dd9022a4944a3c3158 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except0 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
8f815350d2e76fdaffdf292fcb8c71de9b8d6779 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except0 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
1e3e1b183989384166f38fd7af2338243ec0a8e4 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1Fun TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
8c8386e006fb12a3f97978ba94f5a18b72897559 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1Fun TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
47a4d4685a8cad728c518537b2c4f470108dfd9a TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1FunWithAt TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
10a73b6eeb7e344aec5b2ae4306bb80eade1f1cd TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1FunWithAt TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
bde9aab0ff1fcac0160f3194fb6989bbfc97fa9c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1Rec TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
b1cf9ea8305c37eec4f338582243e6c3e2fc0da2 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1Rec TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
0250b34b0baa6a5780c15989d054f2a8c39595b2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1RecWithAt TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
130af58758d8c27570881e5c2548f84dccab3031 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except1RecWithAt TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
85e1e7bd913eef3b48b358a836719e418c21fceb TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except2Fun TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
f63f60dd88d1e21cb85e4887541b9318a7e9d921 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Except2Fun TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
e047af7f5770a71a3ad81b21c32b13354047241d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Prime TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
6aa802ccb1a16316c5a6298b0d118bc03fbec94a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Prime TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
c30a7bd9f90125e8f6a26d783503dca27e3b0d6a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
DefFun TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
7bdab4cf17ba8c587284d103b48cad70a0624b5f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
DefFun TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
3fb98a8025697a31d2346cdeb7362d26f1990e1e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFun TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
7647ccac77297478e04793af48f821f17c04279c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFun TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
7778c635ad3bde1c921b9e5407f807cb72903e5e TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
DefFunRecursive TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
9351a62ed6cac45c99855bcb8e09303d7e0df221 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
DefFunRecursive TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
d578807a491ab58547ea86c892f3e0d778691b31 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFunRecursive TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
d120424d04a6cafbfa74e4dd9aac90d70f077ec2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDefFunRecursive TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
b89485a8026f6c69298d6bf8a9b6969a76d70aa8 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def0 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
46d3558df42d7bb58bdf189f56ea3454d15b7416 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def0 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
43777adf5c78aa28ea3d61a3e7f484109fe45ec0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef0 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
f81bccf8db2b7794d11906baccc2b3afb6c36640 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef0 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
c88e57fd86a06c0051851319580ecd0d250a2b3a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def1 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
e407aba7dd3270d1d726ba789eb7493e7fd7bfe2 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def1 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
3816397713537ea2d3074ba69821549d68eb2ab2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
08ea9a20a6965f46d0aeff434d10542052bd99a3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
f073767a0be044aaee212991b2682b7ca4c77d70 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def2 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
cc4b9ddf044194d0bde8f43e46bd2585fca3394a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def2 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
a657c7c36ca25cc2792e3e6c4d39a1e0ae9a35e4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef2 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
3e3a10f09000589e659202285c79cf71d04d8591 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef2 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
3d40efc753dc3a4e28fdcd923a14e189bc1f92c1 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def1Recursive TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
35b336ff3c168643c3dcac8a84a26a82c13e9ea2 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Def1Recursive TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
4288d0e795c7b6274204e70dee53fa781a6e1964 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1Recursive TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
5f90f48e1cbbe75ce3d4af7a78b2e569699f4130 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
LetDef1Recursive TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
86ea0b23bde2bdfad4a74b80677b47feab9212d2 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Extends TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
faf8409945a08edda67359e10e7de12baba8d17a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Extends TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
f0ca7f3906ade6cd54f5c2490ef70949ff56d4ed TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
ExtendsInDifferentFolder TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
9034970ef90bbe19394c3dba47289f95b5daca68 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
ExtendsInDifferentFolder TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
8198b238a6068cae2196ffb339923fe9456d9255 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Variable TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
dd247ce1253c07764516304f07d53b15f5fababe TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Variable TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
144f222a2d20ba141f4060299d249413b837fea3 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
VariableViewExclude TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
372c849eaedc1a6469f663eaae99085be1164217 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
VariableViewExclude TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
d63a9cdacb9bec2a6cb9066ff1e1d7c04662cbef TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Constant TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
eaf7802795731aa84a136499e59fe376d6e22723 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Constant TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
862904681e50269c15fb19cb2c3d71b6dc18400b TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
ConstantRank1 TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
2132a8b8e709d76b9403582e1152973696f422e7 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
ConstantRank1 TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
dbdb33cbd3f953c0a2e2b867d1638c4196a3433c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Instance TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
9bdbee331362ebce31ca919ba9ac6466162e0188 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Instance TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
d5ad7399471acad7aa0c31c2aea647863df45ca4 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceWith TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
ddfdaf35f43aaa4d0dcb5a67f593f1ab80e295e0 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceWith TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
10bf272b1161257d95441a35866b08eb29218c49 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamed TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
c4e24b785c7e25b55f51fa9f56de93f72fa033b6 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamed TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
ab5e62bbd0721f329f11e914d4f21d50e6ca2bcc TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedWith TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
625d1209296f9e08a861af44069d7967bae2bc81 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedWith TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
dca82e8571e7c9a5576598454db3ab0c1e0e4085 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceInFolder TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
cdb429ec2af5cbf2b7c7d8bd2c666b03345831a1 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceInFolder TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
69f75b269cbaae63c8ea3ad45045906f3c76aecc TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceWithInFolder TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
3f8f4f0f0ffe9fa3aa45e357b36082bbfb92837a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceWithInFolder TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
c0a20115e2ff1e39fa8f933377b87d5d9d0c897f TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedInFolder TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
86deb410633afe4f6c218a19548961ba31cef5ce TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedInFolder TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
72a16bf6f6f61db0fa86d09951e3243f6780f44a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedWithInFolder TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
28e52312bd6ccf4ecd80e2b68ad0b91a0ce5316d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
InstanceNamedWithInFolder TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
bdcda349ffecfde46ee45938e3712d87cf7d4988 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Lambda TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
73a09f1779c15d27394617e988ccd472769d9e55 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Lambda TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
33d5947194f6a5ed283c9dc06e9cd89c4cd53f96 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
IfThen TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
82799a91bc0ebf9b39840b0884d8fd5e011f8d45 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
IfThen TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
722250c0cd34958c6ba9f7a89210cdd9b4d69389 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
IfElse TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
f66c92e500ea5280f5c53ef8531de18129dc5316 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
IfElse TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
b97ce502da3b27a62ff3c4364a5bf89cd438eb1a TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Unchanged TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
cf9a047b8c29f18917809b7ba028b1ede46362f8 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
Unchanged TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
db4ed971215b735beb08c740728dd1f76947cb6c TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqLen TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
e7d00e5d5e7a7e0a28b620e88d386b72c0c9a312 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqLen TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
f05a0a5d38b446afd1c6eba6e6b27f5974a849f3 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqConcat TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
1c55a0dae676e1a5cacce5bbb19a2719dec36122 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqConcat TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
e45ff4e1479fb17f0144b43d87d827e324268cbc TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqSelectSeq TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
e9f237b2790f10181e8bcc5ac1454bbcdc0bac78 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqSelectSeq TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
886f69c526ea5e3362b7ea3f78a58a52a25f6dbb TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqSubSeq TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
36b4c5cf69806ea7d8f4eedfd514f1ac8396f4c5 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqSubSeq TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
cf118a906edcae6bb9ba1c978e7887822a7c8945 TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
e01819714e31c00141297f579933b47faf8b5e4e TLC with reduction strategy:
  • Case Feature: SortSeq(S) is reduced to equivalent sort implementation
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
TlcSortSeq TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
c384cdacfab5a840cff06baf22e7296dcd0fd406 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
BagBagIn TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
689f501cfac53c2b023c97d8c3608ca5f230e845 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
BagBagIn TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
487116da511b79b4df6daa7bdfd068c7d6701c11 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
BagCopiesIn TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
142a0b0370cb1f1fe4bd0e4147062181f5aa7a2d TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
BagCopiesIn TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
a217bfa10d359412d0476f9434e769664af4b762 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqHead TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
9e334b8e4735d1822a5393bc7bcd17669d4791e6 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqHead TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
f31c06fc5cf7ec97754ea5e704174ac6aaed4fac TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqTail TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
6dfb02366e9a4f5886365229bb3d2d64e285c5b8 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqTail TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model
28075a2677a076dce35ec4ad7c61b8d68cc615dd TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqAppend TlcSortSeq True Passed
  • Model Under Test
  • Equivalent Model
b31a944cef21ef074959e6b8d33dabfff3ae1849 TLC with reduction strategy:
  • Plug Feature: SortSeq(S) is reduced to equivalent sort implementation
SeqAppend TlcSortSeq False Passed
  • Model Under Test
  • Equivalent Model