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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
6426ab6cd9468968a3f3df18d7c8d2f809da5b23	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Imply	OneLineComment	True	Passed	Model Under Test Equivalent Model
97f1ad59fb8480cba697ea2b56ddf4cd41b37690	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Imply	OneLineComment	False	Passed	Model Under Test Equivalent Model
e7944dd0dba4f1607dc924769d23ff2e44abd8cd	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Imply	MultiLineComment	True	Passed	Model Under Test Equivalent Model
ecea57ae3580106393b7cc61be8cceedbdeeda29	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Imply	MultiLineComment	False	Passed	Model Under Test Equivalent Model
fe414cb109cbed79877d56afffc0fdacb8d2adbb	Apalache	Imply	BoolTrue	True	Passed	Model Under Test Equivalent Model
f804c6ac64af1ff6918ac892c16b7fd3c63bc90a	Apalache	Imply	BoolTrue	False	Passed	Model Under Test Equivalent Model
c042df99e6ae6e017ac100060bd2ad5b56e3d3a6	Apalache	Imply	BoolFalse	True	Passed	Model Under Test Equivalent Model
ae992f03b75fbb6d52bb5cc70f256971997599b8	Apalache	Imply	BoolFalse	False	Passed	Model Under Test Equivalent Model
30e0bc9cd7d72c14a253f8fef6e3a72dbdeb356d	Apalache	Imply	And	True	Passed	Model Under Test Equivalent Model
8a10eda0546c96ae209d1b2788f8f2c7b927d29e	Apalache	Imply	And	False	Passed	Model Under Test Equivalent Model
2166af4e30e556090f245f2e84ac087f0764ab6a	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Imply	AndMultiLine	True	Passed	Model Under Test Equivalent Model
e7cfc59dffa81587459fab6f5d8d2c54cdd3bf73	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	Imply	AndMultiLine	False	Passed	Model Under Test Equivalent Model
9ab3e0d5fefbc9befa5708c98d6446d8120f6b9b	Apalache	Imply	Imply	True	Passed	Model Under Test Equivalent Model
5422d4368115b879edc2e4c5f393569979cb5a01	Apalache	Imply	Imply	False	Passed	Model Under Test Equivalent Model
90f1e67440dc17e354c7f85b66117bdd834f3fab	Apalache	Imply	Not	True	Passed	Model Under Test Equivalent Model
5c4dae6909fe3a7df20b32cbb785953be4a79162	Apalache	Imply	Not	False	Passed	Model Under Test Equivalent Model
cc7bd8f76451efdf97f43519587bec9ddc67622c	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Imply	Or	True	Passed	Model Under Test Equivalent Model
87d486172bdfb787112df45b217f883f55d514d0	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	Imply	Or	False	Passed	Model Under Test Equivalent Model
b479cc1b0b2d1bdb0f3acc6b5be233ecd67d6513	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Imply	OrMultiLine	True	Passed	Model Under Test Equivalent Model
3a1d23e1995b934664c7d866efada1e1f1f9f26a	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	Imply	OrMultiLine	False	Passed	Model Under Test Equivalent Model
c0d4209212022b0c0a7b1fe96c293c2eb5b39ba5	Apalache	Imply	Eq	True	Passed	Model Under Test Equivalent Model
d374e8c6fda910f814aac2e538496ebd5f07b4a3	Apalache	Imply	Eq	False	Passed	Model Under Test Equivalent Model
051cd0cd9d07bc1a809dd655f3254779c880d55c	Apalache	Imply	Ne	True	Passed	Model Under Test Equivalent Model
4aeec08cfa87c34a49ace438026782215172f865	Apalache	Imply	Ne	False	Passed	Model Under Test Equivalent Model
05e2c017f740cb149aa1057fc5b8f398d6ce79d8	Apalache	Imply	Let	True	Passed	Model Under Test Equivalent Model
2aa02ab8be2109af112cc0a60557af2ad6dacd17	Apalache	Imply	Let	False	Passed	Model Under Test Equivalent Model
5514ca0c928c8c4656d8b3fc1c4a61ec934aa5cf	Apalache	Imply	In	True	Passed	Model Under Test Equivalent Model
aa8aff67a4537dae1cf8a94add4097b419c40f76	Apalache	Imply	In	False	Passed	Model Under Test Equivalent Model
1ed7ca65a3445defef6a676a8b3133acaef81962	Apalache	Imply	NotIn	True	Passed	Model Under Test Equivalent Model
5d2b6e5bded3630d5b423914e63ead931c9951b3	Apalache	Imply	NotIn	False	Passed	Model Under Test Equivalent Model
f5aa585d9c4b687503d49ac6634ce891520d16bd	Apalache	Imply	Exists	True	Passed	Model Under Test Equivalent Model
bdd91d8e8142b3d40d5c3f4e74131d3ab0022223	Apalache	Imply	Exists	False	Passed	Model Under Test Equivalent Model
1d56feb30f01b4e529221a231777beed1c36c6b9	Apalache	Imply	Forall	True	Passed	Model Under Test Equivalent Model
0643830aa2cc67891932bd4c47a2a2b4c8fee2c0	Apalache	Imply	Forall	False	Passed	Model Under Test Equivalent Model
469aacb3833657a369ecec4de92caa2acbc7a29c	Apalache	Imply	Choose	True	Passed	Model Under Test Equivalent Model
44383b5816f1252f0579b4845e6ebc6ff32cdada	Apalache	Imply	Choose	False	Passed	Model Under Test Equivalent Model
2beac356ab1631cbebf69a5e374b661f37d01eff	Apalache	Imply	FunApp	True	Passed	Model Under Test Equivalent Model
d928ef064cc04996938fed8308f827f32f64efca	Apalache	Imply	FunApp	False	Passed	Model Under Test Equivalent Model
5c201d5768c4ae3cdcec1c8a9fe9f8a53a2af70d	Apalache	Imply	Prime	True	Passed	Model Under Test Equivalent Model
0caa844e21455bb9a1aa1b63a48dc6b55a822ee4	Apalache	Imply	Prime	False	Passed	Model Under Test Equivalent Model
107718c668a2bf18f5875eff62821b788f894bb1	Apalache	Imply	NumGt	True	Passed	Model Under Test Equivalent Model
a1e91f6132e0c04040a85a4c03b144e56d9082b4	Apalache	Imply	NumGt	False	Passed	Model Under Test Equivalent Model
9c61ed96cb28d4c25732b32752517133b32c719a	Apalache	Imply	NumGe	True	Passed	Model Under Test Equivalent Model
a053d7f51756ec8805ecd252ccab31048ba756e1	Apalache	Imply	NumGe	False	Passed	Model Under Test Equivalent Model
186b2094302b35566614e03b91aaf32250326f30	Apalache	Imply	NumLt	True	Passed	Model Under Test Equivalent Model
b8b6b16410dcd82d374d531ae9b1e88a189c0c69	Apalache	Imply	NumLt	False	Passed	Model Under Test Equivalent Model
4c9792ad912f869d4064a347a67fd72078e726d5	Apalache	Imply	NumLe	True	Passed	Model Under Test Equivalent Model
4d60859dfb52064c21cf35793c6638070f6b2bcd	Apalache	Imply	NumLe	False	Passed	Model Under Test Equivalent Model
ed220a5de70e24104dcc7c3b08bee97fb0acaf96	Apalache	Imply	Def0	True	Passed	Model Under Test Equivalent Model
eabc480755ab50bf02411b509483df9b95d587a1	Apalache	Imply	Def0	False	Passed	Model Under Test Equivalent Model
2c71034e132c870b1103eee631dbbabab7aa6df4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef0	True	Passed	Model Under Test Equivalent Model
3dc06e9ef7100c4686b1cb038dbf659d9ed3040a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef0	False	Passed	Model Under Test Equivalent Model
1ef80585e15bc8fe3f60e54f56a876a645af0e64	Apalache	Imply	Def1	True	Passed	Model Under Test Equivalent Model
33ff1638639ea7e8feabc7ebdb269e059435f1c4	Apalache	Imply	Def1	False	Passed	Model Under Test Equivalent Model
3ddd944ba1ee738a481e115c73f7b72fabfc25f0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef1	True	Passed	Model Under Test Equivalent Model
c6208e68d13ee715f2d9dde91f71862739a85542	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef1	False	Passed	Model Under Test Equivalent Model
31311ac47f01c6494d39d37fab81d4acfd0de839	Apalache	Imply	Def2	True	Passed	Model Under Test Equivalent Model
f63e3f15c0d423af8444f26064af79693b1ba363	Apalache	Imply	Def2	False	Passed	Model Under Test Equivalent Model
9e1933b969225f1836650c8d7404ecf3bed091fe	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef2	True	Passed	Model Under Test Equivalent Model
49acbb54959aa555cb70532ce58811b5e2054b97	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef2	False	Passed	Model Under Test Equivalent Model
e07b31a2d4dbd75b431b968b7849c5a8c373adb5	Apalache	Imply	Def1Recursive	True	Passed	Model Under Test Equivalent Model
9783eb09bfcf6e4357d92c315340422962659d4a	Apalache	Imply	Def1Recursive	False	Passed	Model Under Test Equivalent Model
45b5fae61e4db52caeaa1ea6d1566b3dc6649210	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
0603158049a4dc7d2c8cc059c717f96f51fab8cc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Imply	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
7149d8928d3555187726ad9694fb836e648a7c44	Apalache	Imply	Extends	True	Passed	Model Under Test Equivalent Model
e3897ec1734a84ba681802b94c068e1f5a59c357	Apalache	Imply	Extends	False	Passed	Model Under Test Equivalent Model
2ea2e1d46d5f423b8c41185058bc0f2334369274	Apalache	Imply	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
cd2a7cb60eb11839e2955f0cb9b2c4a5c3d781ea	Apalache	Imply	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
da1a635d418232d8804bca7a6e542ac62d007a95	Apalache	Imply	Variable	True	Passed	Model Under Test Equivalent Model
61ac48c0543a5bf24c00458ceee5480c4219c803	Apalache	Imply	Variable	False	Passed	Model Under Test Equivalent Model
c95eb0c06b20753525261fc7569b83c6acf12d71	Apalache	Imply	Constant	True	Passed	Model Under Test Equivalent Model
a06105ab3d2a02c80a13f780a6a2382a1da6c512	Apalache	Imply	Constant	False	Passed	Model Under Test Equivalent Model
bfa8be86b02376bea68dc5ad6b948bdafc9007b0	Apalache	Imply	ConstantRank1	True	Passed	Model Under Test Equivalent Model
34d984f5c13db2329df820684741d4a4e561ce4f	Apalache	Imply	ConstantRank1	False	Passed	Model Under Test Equivalent Model
ad8c5567dbde28787a8ef844df33d69a279b7e60	Apalache	Imply	Instance	True	Passed	Model Under Test Equivalent Model
a233b38594cd8d9e0f82828edba69a60fe3fc244	Apalache	Imply	Instance	False	Passed	Model Under Test Equivalent Model
dad5964a1579dfd020b6866127f69aaea55da046	Apalache	Imply	InstanceWith	True	Passed	Model Under Test Equivalent Model
d24e02005338c668c25b47fd6dda3f255d2c2ffd	Apalache	Imply	InstanceWith	False	Passed	Model Under Test Equivalent Model
bceae87d312230daa757d9fc08700f029104aa00	Apalache	Imply	InstanceNamed	True	Passed	Model Under Test Equivalent Model
694363262f38af54ed8a30d59866ec86f48f6d35	Apalache	Imply	InstanceNamed	False	Passed	Model Under Test Equivalent Model
2017c5b27f351420d445264cd7340f0342db884f	Apalache	Imply	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
649ff2715af43c7b73865f15ebe83ad616fc0d09	Apalache	Imply	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
5a4992ba4f56d1f23b8a0f94a387e4b0474cd40e	Apalache	Imply	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
b231c5191d67615750c4be71882b7b01eb4efa0c	Apalache	Imply	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
2a689859877ab0fd831df9747d21e28f6daaae64	Apalache	Imply	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
a1d1b3b7cd308c04fa5c425005bacc6fbcb51580	Apalache	Imply	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
d62ca68eaaaf555f4657f757c2f3f2fd3f0ec9ef	Apalache	Imply	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
89c3a48d934426710bc1653dc920f5a14c4a915c	Apalache	Imply	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
13742a3850c1198806101d6fa2d46474cea59ee1	Apalache	Imply	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
07de0713799db83152827857f5ae62e8d2fc8384	Apalache	Imply	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
8a0f063fb517a05679feb71b4242b319849599fa	Apalache	Imply	Enabled	True	Passed	Model Under Test Equivalent Model
42dd73b7a301798e773027e286caa59423c4573b	Apalache	Imply	Enabled	False	Passed	Model Under Test Equivalent Model
6258dfe4a8755b592e95df1533819bb148b8c4e4	Apalache	Imply	SubsetEq	True	Passed	Model Under Test Equivalent Model
30b8d27d5ae889357caf16af577e2639a1d3ffb1	Apalache	Imply	SubsetEq	False	Passed	Model Under Test Equivalent Model
8fe30239537ef1da41240c2b687236ab8f900d8b	Apalache	Imply	IfCond	True	Passed	Model Under Test Equivalent Model
f3313d2be80cf47c9430e02a64d5503f236c47dd	Apalache	Imply	IfCond	False	Passed	Model Under Test Equivalent Model
8f74f4374a30c2e33b2f44dff216370ed0a0a929	Apalache	Imply	IfThen	True	Passed	Model Under Test Equivalent Model
50533942d60f01db240ab50d805673dc59ec2f32	Apalache	Imply	IfThen	False	Passed	Model Under Test Equivalent Model
b271c898b63029311bc60df88f37ca63e96d71e1	Apalache	Imply	IfElse	True	Passed	Model Under Test Equivalent Model
59773df1edf02b015e646833d78a55d4534bba83	Apalache	Imply	IfElse	False	Passed	Model Under Test Equivalent Model
8574810f0a422761d80b440ea7b20225272beea6	Apalache	Imply	Unchanged	True	Passed	Model Under Test Equivalent Model
8a3e899f52f0b438fc791e21f1618ef15d51c232	Apalache	Imply	Unchanged	False	Passed	Model Under Test Equivalent Model
e6a1aff8545cfab3e7e3f6fab341b37920f040a8	Apalache	Imply	Equivalence	True	Passed	Model Under Test Equivalent Model
86e8bdd3c527d922764ff1e0858935df29ff64b3	Apalache	Imply	Equivalence	False	Passed	Model Under Test Equivalent Model
538d0a11de68256521c98734bd55124f5a3bf92d	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Imply	TlcEval	True	Passed	Model Under Test Equivalent Model
2818b40e58fafe144a5bbac4b10beefa31dfee33	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Imply	TlcEval	False	Passed	Model Under Test Equivalent Model
fb7574bd72fea35618dc117779fba5e267e6e7e9	Apalache	Imply	BagBagIn	True	Passed	Model Under Test Equivalent Model
21a0ae69196f3e12df69bff8dc8900de1b183818	Apalache	Imply	BagBagIn	False	Passed	Model Under Test Equivalent Model
de0d0a1e48639c017e4b5eacfaf07acf7860ac6e	Apalache	Imply	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
cacd53f993220b11c11f02acbbedd2f94810c749	Apalache	Imply	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
3ff483a15352e5eaf4dbce31bd0766f4d5ed00eb	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Imply	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
5ac04196bc1310cdc07fda0dd97d7db35167edf2	TLC with reduction strategy: Plug Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)	Imply	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
781649b73558e63d26bed988f6891f43972442f5	Apalache	Imply	SeqHead	True	Passed	Model Under Test Equivalent Model
b04271bf5ec5a04fb2d8c002caff1370c6389abe	Apalache	Imply	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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