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 BagSubBag; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
68a53ec436bfc1123f438d843a5b6eb9e8f3f02b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Eq BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
9144cff674efdc7cc04d68c5d62293364fae646d TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Eq BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
5aed793a75d4f5942fd389f5c3b610b4d6e4e5b8 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Ne BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
a5ed8fdbbbff8caab02a3fcd0aba11ecaa104c81 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Ne BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
2e5845ce70d7d1bf7363bb199d7c1f0483982037 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Let BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
08324b9e1cd370be6158462910355b9144c23735 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Let BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7714428ec67e594065d2787a787cc2df8c15136f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set0 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
00b66de7a3472cf13cc58e50bcb7a68b1d349734 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set0 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
f08025fe17a651ef0044ef3ff4ca80714e188193 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set1 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
0b09eb5d1f99f0b75d44f420d49a109b50849a07 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set1 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
3fe5449abc3e51e056c0127dab92c7ca5cadab74 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set2 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
e37e75f71a80af30811e9cafa77a4ae2f1262c3d TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Set2 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
b38ee7085cbd08b157d8e81802b5ba1b4f0d0876 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Fun BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
83bffc079528998187d0283180a0de648bc12d6e TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Fun BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
d2530c0ce8b1d5c120e6acc752a8b935de6d3867 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
In BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
9181b1abf2998fe5e13a16cb5a5d1605c3f0c432 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
In BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
d2eae288974c2a0baa96d11a93fd8899530f6488 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
NotIn BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
771708b597ab4260d8283319ff0f1c952e96185b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
NotIn BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
8bfc85707e1ddb0090468a2a857b1fb9f2cc5a7f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Record BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
76c2dae1c45f66544e59cc0c8f2c7ea9999b998d TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Record BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
f8ec13c6990cd452a166c65afc51b21e9ff0cffd TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Tuple BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
ae8710e2ef3f88fbbd2efda17fc34b004dc1982f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Tuple BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
ab01c1f181c69f89474f5a245b2d96ea483c6068 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FunApp BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
910858b5d8025b70aa8d3f253b458a9705c87b2a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FunApp BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
899d3a33dd37a3b6a8f26171f14c66c77031d7ca TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1Fun BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
0a3a986a18c845713ca2c15f952dc5ac99b99c52 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1Fun BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
408d509c74e243546a9247527c78e7b20a4d38d9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1FunWithAt BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
05887580e70be331db7b91b92a1ef2f4bed1536c TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1FunWithAt BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
9a954aa94550491671b877afd0583a5974087b32 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1Rec BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
63977fcb0ac64a632be7ea6075841ecc2004aa4a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1Rec BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
60b74805d2bb78095d2b898e5e794bdfee629282 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1RecWithAt BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
84dd46c991f19ec17a9bbb972b8c2780bc29bf96 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except1RecWithAt BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
61a2632b7f4792c495a8bb3c8c464ba759dcdc78 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except2Fun BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
bd3d6293511cc35ca3f06f5091e2b4669300cf3a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Except2Fun BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
3b92d8d3ced0179ea0ef9cbfe883bee9a8184cf0 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Prime BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
3984d106717ac52fc55365e6fa3b26484d476c61 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Prime BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
496e5eb8884c6d19059670384c270505432dcc26 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
DefFun BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
3bbb70eaabac13b7862cc943d768a00533e4336d TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
DefFun BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
c606132d195d5ec687e396e262d2a531b9246c8a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFun BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
42e9066e753d92766bc13c7d71583a163ab678d6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFun BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
fdd60cc56404c5ef5627a40ebd16c513bafd82a5 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
DefFunRecursive BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
f319811f98c0992462a07e5aaaed152b17b5be27 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
DefFunRecursive BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
53435144d8f31bf43eb60ea34ccd761b5b76c526 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFunRecursive BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
8d3a78fe512601a56829c4b10605f43540194672 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDefFunRecursive BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
74b9460c569e92215f22f421a69651217f2e0432 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def0 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
1fac4bb9e0904f74f1180ed13da5c42da1843c0f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def0 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
4c1ebe4305a22ee668e834b110013a621431c92c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef0 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
62ef01e5a9a4c06e938337c4883bc39be14dd209 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef0 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
41486844dfe15d55ff783473ff0b1cb22b24fffb TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def1 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
7555c65b8beb14abdf3d40a72193e98f9682681b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def1 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
e915c592f4d5360a36c06fbf7b1ba4cb1fc4d018 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
808bf460a4e5ccf8577cbaf3c2ad0de298b279e2 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
180e679660f905f76a72e02cf940738a9bb2757a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def2 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
34ba1569b059241b1ab7a9ce19eb7ff630d9431f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def2 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
92825c400223f3a8225857d85fe1ea3cdce57e51 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef2 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
701912fe40c82080471de25f3dbc2a89c17362da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef2 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7999ea96d14d50aaf222ee26c423b91a0de017d9 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def1Recursive BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
f94d6e1c009392129e03105ea6010979c0ed99e1 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Def1Recursive BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
2408092993c01d3e8ebfe7b59814675521c3096c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1Recursive BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
fcabf2a336d57ea4da87f94926d23f2fedb8594d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
LetDef1Recursive BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
c40f606b1c15852c51f511c6f8d3fb36c7c11aa5 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Extends BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
dd8a1c196637cab6224f146f7739f18e88fabc24 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Extends BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7b0d881225e62c0cba18f0a247acd2031bb88981 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
ExtendsInDifferentFolder BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
fa0784721787b4f99641a7c5d73c61ecf4d8b498 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
ExtendsInDifferentFolder BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
e1920c174aab3ca2346eefbc3e1309b3e86a74da TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Variable BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
ee9e54d3a1a0f881fe6e2b9804a8c9d7552d1979 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Variable BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
66d1afea721a2e206414bf8c4acfb210d2086312 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: SubBag(B) is reduced to equivalent SubBagR implementation
VariableViewExclude BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
b66f5bbd733f7661b876f6f39cf826de1370e7c9 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: SubBag(B) is reduced to equivalent SubBagR implementation
VariableViewExclude BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
5c13e0d942038ccbde957509b2fae1d9605a3fcb TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Constant BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
1e19ad6fb6c9daad009828dac5cbbb587041e69f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Constant BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
8958f2c45477d7be3718bd67952ecad6cf9699c8 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
ConstantRank1 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
3eacfb20493472ab048dfffb4af8ffb3d6db9e0c TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
ConstantRank1 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
2a8306bec543f096e74cd8d60d23ec7f54b69256 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Instance BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
109d6c4be8d12412941da434d9a5c0fd7f0b64c8 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Instance BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
f93c84faf95d56891a03b5653d4f2c05dc3a8456 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceWith BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
da2a153891e1375cbdaabc0761ba68f0c517f7fe TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceWith BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
65f8da20faaa8e6288ce725d0e52078f12730b39 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamed BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
26173f92f91df54253f77a8aa97328b1d381cebc TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamed BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
b5dcb3524ec87ac979b19d5ffc6b90de089c5f1a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedWith BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
d9d3b1a116e9f7c58f76bb06034682fdc2e8033c TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedWith BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
e89c0ba5b937744f355d169d8856c7a2789a43ee TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceInFolder BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
dd0d08a70c1e35217c5c8903976a23606ecf158b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceInFolder BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
3ec723f343392285ba3adb344b185f1e6d2fab97 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceWithInFolder BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
6395ed423052be4b865915bb5fdd4072768b6f16 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceWithInFolder BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
2baf790dbe68ebb1ff03abfd2c9cf46161c8ba9b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedInFolder BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
86b30073ceb9dc3429813ae66faa22ae1793f40f TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedInFolder BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
caf102dc1e6962effc4795ffbd380c3b0e8cdfef TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedWithInFolder BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
2fb7c2f7a78f2fa2ac895998c1528f39794b8a6c TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
InstanceNamedWithInFolder BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
e4f49c13a9b0c5d9987001929c86cad03de2373b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Lambda BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
c07ada86138f8c99e807958f7d70d4b1593a2fb1 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Lambda BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
871c51f7c47fcfba992f7164d15565f65b445f63 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Cross2 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
a8a584c8bc6a1b6a61d5bbf5e1f0a19acca1761d TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Cross2 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
fd81451d45f66332724091d2ee82fbf782c44cad TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Cross3 BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
1e7641a458418484990d727970d9e80c15544165 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Cross3 BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
cb99b092f9bfea0df1e1d7b790c3e9f2fbb58430 TLC with reduction strategy:
  • Case 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))
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FunSet BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
51b25774a6521f4a4edb28a70a13d079213fd974 TLC with reduction strategy:
  • Case 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))
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FunSet BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
039a02fb0ff15c209e0e2e6119a5bac4f40f3b66 TLC with reduction strategy:
  • Case 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)
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
RecordSet BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
dbc3b3fda35183d1847d5f814cbffa263c8382a5 TLC with reduction strategy:
  • Case 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)
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
RecordSet BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
dd1f04641a22f7aa7750d72c3468a0f1b7dec0f2 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetDiff BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
029c9cf567206e22d904532543bf81d11fd19c8c TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetDiff BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
4aae2948f25e4e914981ef2a7c51d038448b5177 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetUnion BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
2e7495fc4d610f98c008fcde5ef7b832568b646e TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetUnion BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7e8480c1df5e4951c6c2ac9c3eb1729f6a96032b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetIntersect BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
ee70ad10bf37fb558d3f55e82bacc8762e0ec079 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetIntersect BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
036057fab3f2ac3113aa671946cf4366566fc462 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SubsetEq BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
124100261710fd29b544e54c3d8a48e61bff3b85 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SubsetEq BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
45f5344fd3468e468952c699b27a9dfe2f481dc2 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
IfThen BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
b3fe96e4eb836168272641c90d5b121fef287c06 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
IfThen BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7db0e0e6f4524b58e27dcb8fb9d5fe64f6c6e461 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
IfElse BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
f4b660122ca8bb344af4667789fe7d524123b382 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
IfElse BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
3712ce370d712f717cabe95bf0cd9984a9c332de TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Subset BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
44d74f513e9f48d235f898b00ec9fc59536cd519 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Subset BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
92ba00b9a467fb4a25ba73d8c52876ea93e3dd74 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Unchanged BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
1ecb02748154e0da60e6cd32b8665426ab58e6bf TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
Unchanged BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
b903606e22f52fcb36e3b9670019bc11fa23c5b3 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SeqSeq BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
a337f2f1bef4192bd9cecd63dc77c15f88d52a04 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SeqSeq BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
c9f7b64adf75eb9622c6c9022739f2f0edcfcfcd TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcPermuteFun BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
f3f737c8008814227b1b8692b16ff9bb905a10af TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
TlcPermuteFun BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
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
  • Model Under Test
  • Equivalent Model
2e1dbc82fda724c73d7b485f5131938adc04afd4 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSetToBag BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
d5744be9c095b4029b8245aa5736451705a42d6a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagSetToBag BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
e8e68ce717547fea2d3cfc27b1ac7bcefb3997e5 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagBagIn BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
9ef39de64b6f1dbc521221a1dba1f8fea04b6c1a TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagBagIn BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
7ee189e2808d7b4c8b5019bc2eaaea6ddc21a924 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagCopiesIn BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
8e01f5bf3a8e5081fd4978a5bb44a784b2c6efce TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagCopiesIn BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
dcedfaad8e6e519ff511837aa4d630bdaf42830b TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagBagUnion BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
e8816cdf6082e9fb49128fde338d9229af55ae91 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
BagBagUnion BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
ab4dfa6398209f24514b72d463bcc19b903c2c70 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FiniteSetsIsFiniteSet BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
71d9dca7bb4371113d89657b48b193f104e5a323 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FiniteSetsIsFiniteSet BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
72cd902ac2ed5f8eb64f74705c41ae5dac5e2a50 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FiniteSetsCardinality BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
8880666897944bea4499891c7f843073d2c97601 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
FiniteSetsCardinality BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
6679cfc720b104b9e8a9d2c13e4ff9dcc6083209 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SeqAppend BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
5201939700c59346d4c6a0ad0fa464eafd3f1b81 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SeqAppend BagSubBag False Passed
  • Model Under Test
  • Equivalent Model