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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
4c6d31167702f82dff46089666ffc9f30db6e17d	Apalache	And	Imply	True	Passed	Model Under Test Equivalent Model
9d2bee499ecb429e8362fad71520bf1a35a22739	Apalache	And	Imply	False	Passed	Model Under Test Equivalent Model
2ac4f878797c10c839fe3169411f7832a44c1793	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Imply	True	Passed	Model Under Test Equivalent Model
f59354b3e43d014117ca992ebd865fb9be254673	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Imply	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
7f05e5814083dd650aab02b56c5174e8a3a98fe7	Apalache	Not	Imply	True	Passed	Model Under Test Equivalent Model
5a3af6565cf45f0e016d0c28f17018f168fb77bc	Apalache	Not	Imply	False	Passed	Model Under Test Equivalent Model
3c4b20adea599e7e82fcbfebcfd3aef390f85cd7	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Imply	True	Passed	Model Under Test Equivalent Model
f60686cbb137bbc807b28e41e2446c0298e72299	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Imply	False	Passed	Model Under Test Equivalent Model
00c37b2495e1e5a5c6f1111f39bbcc68041e9298	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Imply	True	Passed	Model Under Test Equivalent Model
209273e308fa20e115a196713a07047a8e074d59	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Imply	False	Passed	Model Under Test Equivalent Model
bfe86f3b86de574f9783c168f86f7804d968095c	Apalache	AndProp	Imply	True	Passed	Model Under Test Equivalent Model
6d4c19883182cbbc38e886fb8915bdbbcc71f255	Apalache	AndProp	Imply	False	Passed	Model Under Test Equivalent Model
41dc2bb0967d518d99b39ec0d6f46e96e0abb077	Apalache	Boxed	Imply	True	Passed	Model Under Test Equivalent Model
a062804b2defdc1b79aa11b15bf4ae56d447daa5	Apalache	Boxed	Imply	False	Passed	Model Under Test Equivalent Model
0ed43111accabcef96f31cbed105f8b6384be0cd	Apalache	Eq	Imply	True	Passed	Model Under Test Equivalent Model
e16f2fbff8773467f147c11badb6ca05814c26a7	Apalache	Eq	Imply	False	Passed	Model Under Test Equivalent Model
1f60104deb6ce7e40bc2d9c884423fbe864a1e31	Apalache	Ne	Imply	True	Passed	Model Under Test Equivalent Model
f7cd3466b3c7cea325630804b1feed703ab213f5	Apalache	Ne	Imply	False	Passed	Model Under Test Equivalent Model
173a5569eb4eff7c700953b6242e427b296691f4	Apalache	Let	Imply	True	Passed	Model Under Test Equivalent Model
4f76102ea96a539955227bbff77d4efd52596efa	Apalache	Let	Imply	False	Passed	Model Under Test Equivalent Model
974726411a029c85628d232bdf66e4050d383f5f	Apalache	Set0	Imply	True	Passed	Model Under Test Equivalent Model
4a9cdb852577c041e8989ad6f2846d10707de65d	Apalache	Set0	Imply	False	Passed	Model Under Test Equivalent Model
ec24ffab6828b4f15ea908be854299d8285dab34	Apalache	Set1	Imply	True	Passed	Model Under Test Equivalent Model
97db7005f4c4e713ae401f9ea64ef6171775dcb8	Apalache	Set1	Imply	False	Passed	Model Under Test Equivalent Model
33e7db235133b1cb755bbccd621842f1b13a58f2	Apalache	Set2	Imply	True	Passed	Model Under Test Equivalent Model
6f5482c1f4eed94b7a5de7c14217a28a6afe8a1c	Apalache	Set2	Imply	False	Passed	Model Under Test Equivalent Model
e54dd8102e119354cca7c4986a65993268dcace5	Apalache	Fun	Imply	True	Passed	Model Under Test Equivalent Model
670e101cf085179a32ae6ec88689e9630aa30c6f	Apalache	Fun	Imply	False	Passed	Model Under Test Equivalent Model
dd73558a98f2e6f4ed10475ff1e6bcdc5361a361	Apalache	In	Imply	True	Passed	Model Under Test Equivalent Model
08a6d7c9ed0ad396e4e8c75b0d180a363493a948	Apalache	In	Imply	False	Passed	Model Under Test Equivalent Model
d313e30d9b0c30ea46717c9cfbdaa622d008fe9e	Apalache	NotIn	Imply	True	Passed	Model Under Test Equivalent Model
053b7e9d18e031baec3458db1b6a31cf9e527dd2	Apalache	NotIn	Imply	False	Passed	Model Under Test Equivalent Model
f86c676b49b6daceb3590912de2d68de7beba028	Apalache	Exists	Imply	True	Passed	Model Under Test Equivalent Model
3447f92bd9737cdc1755511b8808994e0d05af43	Apalache	Exists	Imply	False	Passed	Model Under Test Equivalent Model
49fa40a870e1aefcb0e22b22ad0eef8c4117d8a1	Apalache	Forall	Imply	True	Passed	Model Under Test Equivalent Model
74a0b9dcfb9f710b2fe1412277963d1371ea06fe	Apalache	Forall	Imply	False	Passed	Model Under Test Equivalent Model
5337f17a1dffeab9aadb37fd3f5d2ebb928e6ce1	Apalache	Choose	Imply	True	Passed	Model Under Test Equivalent Model
588b74646247ed0be3097b8693a797c1d9bd294a	Apalache	Choose	Imply	False	Passed	Model Under Test Equivalent Model
c60217e1d77b9059652d2e842d7663ed5ad088b5	Apalache	Record	Imply	True	Passed	Model Under Test Equivalent Model
556b932b43b03a9570ac5bcc7955312dae438463	Apalache	Record	Imply	False	Passed	Model Under Test Equivalent Model
5842377af310f168ee08b9d3cee74a8650d9253d	Apalache	Tuple	Imply	True	Passed	Model Under Test Equivalent Model
31a79485dbf0934884f59d842cd2587111e3b1cf	Apalache	Tuple	Imply	False	Passed	Model Under Test Equivalent Model
d2146135d98a00831c90cf5c84e6bbcbdbcbdbb4	Apalache	FunApp	Imply	True	Passed	Model Under Test Equivalent Model
40f03209d85470c0241a9e72d56e37c897ef35c5	Apalache	FunApp	Imply	False	Passed	Model Under Test Equivalent Model
f5c35e381f22a9dde66adaa734faf2afff5f376d	Apalache	Except1Fun	Imply	True	Passed	Model Under Test Equivalent Model
792a0444181b53ac5d1a06590974e344329b1c29	Apalache	Except1Fun	Imply	False	Passed	Model Under Test Equivalent Model
208f8aadf42587f37ec26338aab48ecd0e3ef965	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Imply	True	Passed	Model Under Test Equivalent Model
0252090225c811de904c8b0858fa9a9c5c9683d9	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Imply	False	Passed	Model Under Test Equivalent Model
9fe9c654546c214234ff939c7c5a2f43840261d4	Apalache	Except1Rec	Imply	True	Passed	Model Under Test Equivalent Model
12aa58cae5c3f220f991736cd3877ee5ba3a6b0f	Apalache	Except1Rec	Imply	False	Passed	Model Under Test Equivalent Model
cec07143875a0aadd2d977c00aca65973dae7c4a	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Imply	True	Passed	Model Under Test Equivalent Model
7414e03bd4f94ae697b2f920ddb7b8b28617bc1a	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Imply	False	Passed	Model Under Test Equivalent Model
5746e5f8bec59a11b46f1001d0316d745c80c798	Apalache	Except2Fun	Imply	True	Passed	Model Under Test Equivalent Model
397ab9bd406371023214b3cf6a5323672463b97d	Apalache	Except2Fun	Imply	False	Passed	Model Under Test Equivalent Model
678bc9a800b1be91bd2e5404a2cfd85db4570701	Apalache	Prime	Imply	True	Passed	Model Under Test Equivalent Model
75948ef3d28c63ae3b9a14d8989bed957fd5a428	Apalache	Prime	Imply	False	Passed	Model Under Test Equivalent Model
aa50994199909ca887136f4a8aea328ad73eebe8	Apalache	DefFun	Imply	True	Passed	Model Under Test Equivalent Model
840e13a0b2688e2e02d4007bf7e58a5123baa44e	Apalache	DefFun	Imply	False	Passed	Model Under Test Equivalent Model
59baedc4a969284b29481dcb51fb5657cee74973	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Imply	True	Passed	Model Under Test Equivalent Model
2388d984ddc24bf2001faea441d95f285a5ad728	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Imply	False	Passed	Model Under Test Equivalent Model
bc5a1ecfe9a21190a946cc5e12049485e447f0f4	Apalache	DefFunRecursive	Imply	True	Passed	Model Under Test Equivalent Model
8ead7844beb4e824d402c5baca99c51f3e0e789b	Apalache	DefFunRecursive	Imply	False	Passed	Model Under Test Equivalent Model
4627427b276a201906bff467b87b722224f3270b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Imply	True	Passed	Model Under Test Equivalent Model
86b04cbe0f60fe59d7a47d1dee7c004192ee4065	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Imply	False	Passed	Model Under Test Equivalent Model
3da13f41dc3db59bc92291ffb7a812f1c0319960	Apalache	Def0	Imply	True	Passed	Model Under Test Equivalent Model
c36bd19bc490b20474d85dbd398e4d67ee87f7a4	Apalache	Def0	Imply	False	Passed	Model Under Test Equivalent Model
47a496a6716fbff269ae93978de0a8d04d479902	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Imply	True	Passed	Model Under Test Equivalent Model
112a0e5ae950f5c443acaccd94495e6e47eefb37	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Imply	False	Passed	Model Under Test Equivalent Model
ad4e92dce466deb320745897c28efa9ecd1c671b	Apalache	Def1	Imply	True	Passed	Model Under Test Equivalent Model
9817360065de5fa02e4999ddacc84cd51fb4dcde	Apalache	Def1	Imply	False	Passed	Model Under Test Equivalent Model
6310145efe8acaa0692cac29c9b1411f053b5cef	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Imply	True	Passed	Model Under Test Equivalent Model
ca454aaeb4b18aaa282fddb02c42d09879d6e968	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Imply	False	Passed	Model Under Test Equivalent Model
f87b8ed937f11bc7ade14275d8b2c3037d0d1a74	Apalache	Def2	Imply	True	Passed	Model Under Test Equivalent Model
1fe93a337ba6fcd333cbf4074119da433a16dc43	Apalache	Def2	Imply	False	Passed	Model Under Test Equivalent Model
7cd094aa5389af4cf2fb40fe0e831f42bd4103de	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Imply	True	Passed	Model Under Test Equivalent Model
cf2c709c8d3997642c829bd7b1b86cb8bcde5ad3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Imply	False	Passed	Model Under Test Equivalent Model
dfe6fedef438b13056d1e27db406aeef1da57780	Apalache	Def1Recursive	Imply	True	Passed	Model Under Test Equivalent Model
dff62cc1c9a4767b176563e6adce20b221c648a7	Apalache	Def1Recursive	Imply	False	Passed	Model Under Test Equivalent Model
f36409ac0bba10cdddb5619228ffe17fdcf077d4	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Imply	True	Passed	Model Under Test Equivalent Model
c06bb656722a5110644ece8acd806995b84223f2	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Imply	False	Passed	Model Under Test Equivalent Model
62fdddffadb373726853a76a4bc304b282a61ca1	Apalache	Extends	Imply	True	Passed	Model Under Test Equivalent Model
bd5c2875439e8855e5e5dfe8508cc7ca5b570d25	Apalache	Extends	Imply	False	Passed	Model Under Test Equivalent Model
334d5780be64727294c40de9296d5bf97b8d9025	Apalache	ExtendsInDifferentFolder	Imply	True	Passed	Model Under Test Equivalent Model
18f11109e3e7d09647164234eb3cf83cf8603eec	Apalache	ExtendsInDifferentFolder	Imply	False	Passed	Model Under Test Equivalent Model
a2511070d32db117418e3a642f28b1902b7a26e0	Apalache	Variable	Imply	True	Passed	Model Under Test Equivalent Model
484e44f9a42ac6f1d10374053e240616b4e41a73	Apalache	Variable	Imply	False	Passed	Model Under Test Equivalent Model
0f5f4cf094c2fd03db10641b8b6dd9ef99ca7715	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Imply	True	Passed	Model Under Test Equivalent Model
34eac49c05337a0c0b0ca3c58f7fe2c523a14703	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Imply	False	Passed	Model Under Test Equivalent Model
48f14580b43534862031078f9f3d42a1b322155d	Apalache	Constant	Imply	True	Passed	Model Under Test Equivalent Model
e2b11558c1251810bd90dd460d6f0522c055636e	Apalache	Constant	Imply	False	Passed	Model Under Test Equivalent Model
c5ce94d5353f8560e585542ebbcf2ada17770264	Apalache	ConstantRank1	Imply	True	Passed	Model Under Test Equivalent Model
5acb6e06ef10ab725d8d22a91303499730526305	Apalache	ConstantRank1	Imply	False	Passed	Model Under Test Equivalent Model
b78919fe92c258d903c1b5dea124fc9e519cf919	Apalache	Instance	Imply	True	Passed	Model Under Test Equivalent Model
822936ee097ee22d777a7ca13b6946bf5b211c1c	Apalache	Instance	Imply	False	Passed	Model Under Test Equivalent Model
901f2dd11e5458e3c37de0637bf22dd66e1a582d	Apalache	InstanceWith	Imply	True	Passed	Model Under Test Equivalent Model
278df3358cf4aa85dc6210778b97ada2a6fe45d8	Apalache	InstanceWith	Imply	False	Passed	Model Under Test Equivalent Model
9c56d3c32b697b986e149626d800164ef27ea910	Apalache	InstanceNamed	Imply	True	Passed	Model Under Test Equivalent Model
666d437b7b480629b24dc26ed3c962a6565c3ebe	Apalache	InstanceNamed	Imply	False	Passed	Model Under Test Equivalent Model
2cba73f192c872a612f74513a91a2294c9ecd92a	Apalache	InstanceNamedWith	Imply	True	Passed	Model Under Test Equivalent Model
d40be38bef8b8555eb8c56628f077e051073286b	Apalache	InstanceNamedWith	Imply	False	Passed	Model Under Test Equivalent Model
b58328f7badbec6c59c552f75c41b8e85e5a4f9f	Apalache	InstanceInFolder	Imply	True	Passed	Model Under Test Equivalent Model
147626c86be024716b2ace38208a6b8e36395a23	Apalache	InstanceInFolder	Imply	False	Passed	Model Under Test Equivalent Model
9331e89fe06774151ab80d4ac80dbdbacdc23ec1	Apalache	InstanceWithInFolder	Imply	True	Passed	Model Under Test Equivalent Model
e9013fcbe2a16a9ca9f9fea14686581ce74b367b	Apalache	InstanceWithInFolder	Imply	False	Passed	Model Under Test Equivalent Model
76844a114bf51fc5b8ef436b846dcd611b974def	Apalache	InstanceNamedInFolder	Imply	True	Passed	Model Under Test Equivalent Model
d4e0084cfa3e51831d3c3bca69ca11692ea90484	Apalache	InstanceNamedInFolder	Imply	False	Passed	Model Under Test Equivalent Model
2076a61daf1448f3bab7cffb021e1aadbd767f26	Apalache	InstanceNamedWithInFolder	Imply	True	Passed	Model Under Test Equivalent Model
078dd6c8a3caec208cc221ccb1ff3f8fc8884da8	Apalache	InstanceNamedWithInFolder	Imply	False	Passed	Model Under Test Equivalent Model
a9fe40438fb217276a7bd536330d7fe3f8ead9c1	Apalache	Enabled	Imply	True	Passed	Model Under Test Equivalent Model
c5996b3bf82ef51af8153188648262311bb5caff	Apalache	Enabled	Imply	False	Passed	Model Under Test Equivalent Model
598cc46b2e06f2eb2ff9f4660f2a5290c9a0d3b9	Apalache	Assume	Imply	True	Passed	Model Under Test Equivalent Model
7372b7042f867bb368b2467b26c688b404519251	Apalache	Assume	Imply	False	Passed	Model Under Test Equivalent Model
d7d0f06c2646c8a47b4a7f6ef780c178162e5ae5	Apalache	AssumeNamed	Imply	True	Passed	Model Under Test Equivalent Model
c1d28085c616b38b3b2f80f453be7f684d86b543	Apalache	AssumeNamed	Imply	False	Passed	Model Under Test Equivalent Model
010406c9841522b35a1f7b4d04e15e8718786064	Apalache	Lambda	Imply	True	Passed	Model Under Test Equivalent Model
f57a3015ea236f861ce0316d18b6b19909279d14	Apalache	Lambda	Imply	False	Passed	Model Under Test Equivalent Model
2f36c929933b7e3ecc79dc0cee76ea0b6d71c958	Apalache	IfCond	Imply	True	Passed	Model Under Test Equivalent Model
af53452c806278083050e3f22b5120233a78395f	Apalache	IfCond	Imply	False	Passed	Model Under Test Equivalent Model
f8b66d7b31c76b6b43bf541d19f4cc5dc6037e74	Apalache	IfThen	Imply	True	Passed	Model Under Test Equivalent Model
0b19b459c47a55dfe26e65826da606958e0aa73f	Apalache	IfThen	Imply	False	Passed	Model Under Test Equivalent Model
a84a48e9a8606f100e8ece8011f39e6c9354a571	Apalache	IfElse	Imply	True	Passed	Model Under Test Equivalent Model
4035443a07ea8f78b805a798a9fca1f926104b4b	Apalache	IfElse	Imply	False	Passed	Model Under Test Equivalent Model
ae5f0c660fd08a74d59b76bd479452e58938378d	Apalache	Unchanged	Imply	True	Passed	Model Under Test Equivalent Model
4c840fd127d3c80f18266dc5a8dda943747578d4	Apalache	Unchanged	Imply	False	Passed	Model Under Test Equivalent Model
b2f0e65d9d05d0b864d1b2801d5c4a22de561872	Apalache	Equivalence	Imply	True	Passed	Model Under Test Equivalent Model
a589942a0a2a7fe052b5b3221af37820b498ff50	Apalache	Equivalence	Imply	False	Passed	Model Under Test Equivalent Model
873f9511dea9947ba6f90693b39c8437f4ebf457	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Imply	True	Passed	Model Under Test Equivalent Model
bdabd293d6ca87d65063310238876a28c3cf590f	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Imply	False	Passed	Model Under Test Equivalent Model
6173117978726a914edb9c05c685a4a4a3993e3a	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Imply	True	Passed	Model Under Test Equivalent Model
dd56eb7fd88bac0e2d9c7a108f87fa64bd934f50	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Imply	False	Passed	Model Under Test Equivalent Model
a363bfa1e4f8464fc6098ff2d7c03e7bfd0f2c27	Apalache	BagBagIn	Imply	True	Passed	Model Under Test Equivalent Model
d3277213067e39c9b4dbbce7c10a8c0884601ba2	Apalache	BagBagIn	Imply	False	Passed	Model Under Test Equivalent Model
af182b08ccc1b113045e813baf5bb3237071bb95	Apalache	BagCopiesIn	Imply	True	Passed	Model Under Test Equivalent Model
965816fe065f63e753c10924daf1eee9a53b0a28	Apalache	BagCopiesIn	Imply	False	Passed	Model Under Test Equivalent Model
62996240545b8c16474eb2ae0912f76227db9658	Apalache	SeqAppend	Imply	True	Passed	Model Under Test Equivalent Model
6692df160cc3bdeec80ed6a6caee9b18ea5a2064	Apalache	SeqAppend	Imply	False	Passed	Model Under Test Equivalent Model

Index

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