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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
cca0bbfeddc2efdd95173a50adda581d6f9612d2	Apalache	And	Forall	True	Passed	Model Under Test Equivalent Model
41b2c07c482f3beb3ea0e0677b92d83aa1d3cc62	Apalache	And	Forall	False	Passed	Model Under Test Equivalent Model
d075a52aa7f7e912e183fa0311eff6b09f44c7a2	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Forall	True	Passed	Model Under Test Equivalent Model
9d2d7665ab38a31176307c17790b96b2b9ebdc6c	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	Forall	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
7ce982038794efebb5f3d7f3250db4400de99871	Apalache	Not	Forall	True	Passed	Model Under Test Equivalent Model
53e030882c99c0728bf252dcb5fb0d8cc61f20b4	Apalache	Not	Forall	False	Passed	Model Under Test Equivalent Model
2a52584bb27ade065a644f5dcff2a4aba55aea50	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Forall	True	Passed	Model Under Test Equivalent Model
098f0c7e748b9e1384f2eb80a2b247113ca27d25	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	Forall	False	Passed	Model Under Test Equivalent Model
df56caf92eaa75c35f256e7e534e6403fc47f46a	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Forall	True	Passed	Model Under Test Equivalent Model
f5da9eb3b5d868363b50bd89243b90622debbad9	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	Forall	False	Passed	Model Under Test Equivalent Model
1c7dc89a9f17204c86023fbb896a77971a8af744	Apalache	AndProp	Forall	True	Passed	Model Under Test Equivalent Model
f2f7190fe3cdc39de4535d491276f6a1dd110b54	Apalache	AndProp	Forall	False	Passed	Model Under Test Equivalent Model
52c1177686336382ca015e68a7733848c96dcff4	Apalache	Boxed	Forall	True	Passed	Model Under Test Equivalent Model
838b0f401f8a7e52bd76661440681648d9efd3ba	Apalache	Boxed	Forall	False	Passed	Model Under Test Equivalent Model
2c07af2ca8c5cb29424c37d33931b55e731d1431	Apalache	Eq	Forall	True	Passed	Model Under Test Equivalent Model
d2fe0d6b02bab357ad65326cdfccc5e29d524e32	Apalache	Eq	Forall	False	Passed	Model Under Test Equivalent Model
f081c6f2f05b1365cdd382122f779c2ee1d25a61	Apalache	Ne	Forall	True	Passed	Model Under Test Equivalent Model
fb1cf6abd5375323a1459ea01ac8ddf158ddffc4	Apalache	Ne	Forall	False	Passed	Model Under Test Equivalent Model
7cead322b6dfec7148998104d4cbea07e716b2e6	Apalache	Let	Forall	True	Passed	Model Under Test Equivalent Model
d7dd33e61eed14cbc1fa39470263a3d3d5973568	Apalache	Let	Forall	False	Passed	Model Under Test Equivalent Model
81e76652a4bef1155986b8bfdb51e77a0f5c477a	Apalache	Set0	Forall	True	Passed	Model Under Test Equivalent Model
5e696be424ee288558976865443cc1b27367d1b3	Apalache	Set0	Forall	False	Passed	Model Under Test Equivalent Model
ec5a24e115bb7913d1e02e8cb4e066cc56ef2ba9	Apalache	Set1	Forall	True	Passed	Model Under Test Equivalent Model
9cea1440fe06d23db8774f7b2959df81c057b4f9	Apalache	Set1	Forall	False	Passed	Model Under Test Equivalent Model
6ae14c726d224fb7f3ca53c93439c1d2bd420812	Apalache	Set2	Forall	True	Passed	Model Under Test Equivalent Model
25d8db4c6808f8f79c18cc4ca1781fbfab777893	Apalache	Set2	Forall	False	Passed	Model Under Test Equivalent Model
58abd9deb3e121487b4b1da13050636f8dcc5e30	Apalache	Fun	Forall	True	Passed	Model Under Test Equivalent Model
fd181e6621b9a2b70a8d10d33c0fbe1f0ce563ed	Apalache	Fun	Forall	False	Passed	Model Under Test Equivalent Model
83eced1aa8e1778c919a4e5f4ebe9799442a52f2	Apalache	In	Forall	True	Passed	Model Under Test Equivalent Model
67731f8a799b37b239abda8db527fa22de4a829c	Apalache	In	Forall	False	Passed	Model Under Test Equivalent Model
cb85b0b18d850eb83529f084098d3b63ede1770c	Apalache	NotIn	Forall	True	Passed	Model Under Test Equivalent Model
e41ff464906633cdc5124cb4704c6e79ddd0e45d	Apalache	NotIn	Forall	False	Passed	Model Under Test Equivalent Model
d6df8c6837cc711146c2d6d7c2e24ff2a94d0a97	Apalache	Exists	Forall	True	Passed	Model Under Test Equivalent Model
4c7aea0c82e48014ace4c36e7d1e1162727caa27	Apalache	Exists	Forall	False	Passed	Model Under Test Equivalent Model
6b79f87d81d02a9c7c4cad00dccf91287a14c3b8	Apalache	Forall	Forall	True	Passed	Model Under Test Equivalent Model
00e63e97ea93b69c1f27ed4a65dd7fbc106c49b9	Apalache	Forall	Forall	False	Passed	Model Under Test Equivalent Model
04e29056043d520ed82db3386d0f148177bebe72	Apalache	Choose	Forall	True	Passed	Model Under Test Equivalent Model
2c2f0be1eae207e67cb3fbbfbb8d953f4d065634	Apalache	Choose	Forall	False	Passed	Model Under Test Equivalent Model
a1725a9cc92d33bb5fd9a6b9e692da80b532c759	Apalache	Record	Forall	True	Passed	Model Under Test Equivalent Model
55fc3e98a33299dec9b519dfccaee62f33ecd807	Apalache	Record	Forall	False	Passed	Model Under Test Equivalent Model
80dd892f23ac0f4b3c46a7f5fc6a8f64d7493d09	Apalache	Tuple	Forall	True	Passed	Model Under Test Equivalent Model
fc628c3060b282665e1a3bf8fb6cf641046af8a5	Apalache	Tuple	Forall	False	Passed	Model Under Test Equivalent Model
5bb28f9e8707b7d23e39301ffe6fd52d5d37defe	Apalache	FunApp	Forall	True	Passed	Model Under Test Equivalent Model
700696982c16611eaa6e1c9fa07310dda6a5d019	Apalache	FunApp	Forall	False	Passed	Model Under Test Equivalent Model
b9ad83f962b21b5c22c0f9f29ffb206ab0285062	Apalache	Except1Fun	Forall	True	Passed	Model Under Test Equivalent Model
c18a2df18df7bcb94584de759bd7a4069f5564c9	Apalache	Except1Fun	Forall	False	Passed	Model Under Test Equivalent Model
8ac9b1154e68a52934765610230565aabd882484	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Forall	True	Passed	Model Under Test Equivalent Model
55f133555037abd86f7054fb8298efe1b31afba3	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Forall	False	Passed	Model Under Test Equivalent Model
7d26a3d013604f931dcaf338fd63607cfe386f77	Apalache	Except1Rec	Forall	True	Passed	Model Under Test Equivalent Model
bce381f587fa89742c21e4898f849aeaa54b0e2f	Apalache	Except1Rec	Forall	False	Passed	Model Under Test Equivalent Model
a942a0e1e2fae9c9e1756a63e4d20b1721a090f8	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Forall	True	Passed	Model Under Test Equivalent Model
98ebd3f69a8cb960ba00e680a1cb7dd6fdd06ee6	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Forall	False	Passed	Model Under Test Equivalent Model
4ef63918a3beb56eb8d2244e354194993aa48a6f	Apalache	Except2Fun	Forall	True	Passed	Model Under Test Equivalent Model
bf414449c2da4816a2341142e566812fb14848c9	Apalache	Except2Fun	Forall	False	Passed	Model Under Test Equivalent Model
f5f9c0630f45cfc79526bc144ba3f6cc27c6c2b9	Apalache	Prime	Forall	True	Passed	Model Under Test Equivalent Model
b9f69440b39a321126809e136c0ce5308504ceca	Apalache	Prime	Forall	False	Passed	Model Under Test Equivalent Model
2a480c618ac3c1aad75296844cd0da33fe2db9d6	Apalache	DefFun	Forall	True	Passed	Model Under Test Equivalent Model
4a1761cef757b9ad4bb6ba98ec89992c3fda7d03	Apalache	DefFun	Forall	False	Passed	Model Under Test Equivalent Model
6484db4623585ca6a5fd62844e264009f4df2d09	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Forall	True	Passed	Model Under Test Equivalent Model
646e0276932db3f7b67cde41ee674697e806d253	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Forall	False	Passed	Model Under Test Equivalent Model
1a025312e2cb1d3474d8bd418c6e503d0b15892d	Apalache	DefFunRecursive	Forall	True	Passed	Model Under Test Equivalent Model
84cbc1c8a6fdc5c49d7446cc068229668dbd38eb	Apalache	DefFunRecursive	Forall	False	Passed	Model Under Test Equivalent Model
cc9e6ed8175b38a20a60894cc1044220031255ab	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Forall	True	Passed	Model Under Test Equivalent Model
3c3b00a5739661b208e47d5854071de439b9818b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Forall	False	Passed	Model Under Test Equivalent Model
ef8018ee282230738713d78d67285bcdb8bba6b5	Apalache	Def0	Forall	True	Passed	Model Under Test Equivalent Model
e48d1f9961322fca747ae8969022bb22efdccb13	Apalache	Def0	Forall	False	Passed	Model Under Test Equivalent Model
198a555126d7940481dee7d3dbf5f513f9d33f44	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Forall	True	Passed	Model Under Test Equivalent Model
8fd4c1ad9ad122c53dad4abd736a62adc5a8d673	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Forall	False	Passed	Model Under Test Equivalent Model
312ab1038e9a6b09e7f413aa0a657d723e29363f	Apalache	Def1	Forall	True	Passed	Model Under Test Equivalent Model
fb872562f201dd26bc7c583e45ca71d29e0f0131	Apalache	Def1	Forall	False	Passed	Model Under Test Equivalent Model
afcec437da7c0bb1e0adee3f927db76b9db909e8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Forall	True	Passed	Model Under Test Equivalent Model
57dd3171665ebe8841d398b67d649263980997f9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Forall	False	Passed	Model Under Test Equivalent Model
14641efef82e056ba06df86afd00b7612db2fb33	Apalache	Def2	Forall	True	Passed	Model Under Test Equivalent Model
0099bdd96bd0adcf79d195afec6e2c1a28dfe820	Apalache	Def2	Forall	False	Passed	Model Under Test Equivalent Model
f36fbcc85ef11b4520758033db43fa23795783a3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Forall	True	Passed	Model Under Test Equivalent Model
0353715276e71112c93d2188ab8ce4ae4a64abd7	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Forall	False	Passed	Model Under Test Equivalent Model
c039ab74d4659c127d90b5b8d3fa8d188df9e01d	Apalache	Def1Recursive	Forall	True	Passed	Model Under Test Equivalent Model
6fce7ce8bb78979ffb5a29007cec33d6218f1359	Apalache	Def1Recursive	Forall	False	Passed	Model Under Test Equivalent Model
5585483ff41295925ffbbd3e91170eaaccad2ce9	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Forall	True	Passed	Model Under Test Equivalent Model
e886ad9b76a0592f33038b010ef5677d2efab775	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Forall	False	Passed	Model Under Test Equivalent Model
30117a181956a04b1f762281d888d2f1c8a2938b	Apalache	Extends	Forall	True	Passed	Model Under Test Equivalent Model
0ee4517f2df7d247b28ff3f9bdd64ffd5a5946a3	Apalache	Extends	Forall	False	Passed	Model Under Test Equivalent Model
359331bb8cda5daff760647c02079609f2544780	Apalache	ExtendsInDifferentFolder	Forall	True	Passed	Model Under Test Equivalent Model
8f185d70b6bfcbed01e03f63795967b17e62d911	Apalache	ExtendsInDifferentFolder	Forall	False	Passed	Model Under Test Equivalent Model
85d52afd980ac26563442675b8155eeb6214998d	Apalache	Variable	Forall	True	Passed	Model Under Test Equivalent Model
115e91a5dbd9c8401fc794003d7f9cd861a486df	Apalache	Variable	Forall	False	Passed	Model Under Test Equivalent Model
62e0f6137b3a1ff41321be2010b6a1db79360c6b	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Forall	True	Passed	Model Under Test Equivalent Model
f832a2f530f3bf02a5d4acc5f02e49fa73290277	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Forall	False	Passed	Model Under Test Equivalent Model
47016140ab8e03d48748468aa6ecca8f5d50d34b	Apalache	Constant	Forall	True	Passed	Model Under Test Equivalent Model
78ef43eac78a922ff92ed460b0d10f9c49f755a8	Apalache	Constant	Forall	False	Passed	Model Under Test Equivalent Model
4591f6d132751ba8e1aa09a2e7dade308024dd33	Apalache	ConstantRank1	Forall	True	Passed	Model Under Test Equivalent Model
464a4cbafad05d3db29f4aa3983d0837242df721	Apalache	ConstantRank1	Forall	False	Passed	Model Under Test Equivalent Model
e8384d36c0674b00167132f50ab90907a6ae79bf	Apalache	Instance	Forall	True	Passed	Model Under Test Equivalent Model
88936f0b2ace481b6221b9952a9624c46f1efd20	Apalache	Instance	Forall	False	Passed	Model Under Test Equivalent Model
dda9f7c416d12a0c7adf86d4ebd932d7b9314eca	Apalache	InstanceWith	Forall	True	Passed	Model Under Test Equivalent Model
d9f4c6e245340c788291651d580f8fe281f30399	Apalache	InstanceWith	Forall	False	Passed	Model Under Test Equivalent Model
96fa48a4832b389a190e4cebd0a4e5b6bb0d6f1c	Apalache	InstanceNamed	Forall	True	Passed	Model Under Test Equivalent Model
ca4b4ed3ba25aa2827b17110316188a67d591fe1	Apalache	InstanceNamed	Forall	False	Passed	Model Under Test Equivalent Model
4798756c2c1f2103bc857aca1e20f29bfbef7409	Apalache	InstanceNamedWith	Forall	True	Passed	Model Under Test Equivalent Model
d3a56be2ab304976e57eb2d3a62e453b31ccc895	Apalache	InstanceNamedWith	Forall	False	Passed	Model Under Test Equivalent Model
e53ebca5d7070c9b0f7f666da0e812580e916d89	Apalache	InstanceInFolder	Forall	True	Passed	Model Under Test Equivalent Model
a6351ecbb06e2e8020b827e06ab070d9725fbc10	Apalache	InstanceInFolder	Forall	False	Passed	Model Under Test Equivalent Model
44a104a27fe2c389e641aedaa6f02cbd82fd4d37	Apalache	InstanceWithInFolder	Forall	True	Passed	Model Under Test Equivalent Model
d5c61d9a038505317fbbbd48d01b99276a83a918	Apalache	InstanceWithInFolder	Forall	False	Passed	Model Under Test Equivalent Model
054c6e885acb5427519c21e873a3e71bab247873	Apalache	InstanceNamedInFolder	Forall	True	Passed	Model Under Test Equivalent Model
9fe6ec87088bbafd6fbb2600fd8c609ccb5697b8	Apalache	InstanceNamedInFolder	Forall	False	Passed	Model Under Test Equivalent Model
403d5e3f1de97ff2dece75a56c4404854ff77226	Apalache	InstanceNamedWithInFolder	Forall	True	Passed	Model Under Test Equivalent Model
b28ae973b5de90cb66fa648903ba3ef9fb870bdd	Apalache	InstanceNamedWithInFolder	Forall	False	Passed	Model Under Test Equivalent Model
30e6256d472fb78d644c00733928a11201137f88	Apalache	Enabled	Forall	True	Passed	Model Under Test Equivalent Model
443920f3f17364fe46550f08b4946c536439e9a9	Apalache	Enabled	Forall	False	Passed	Model Under Test Equivalent Model
8f610c4763fb86c80715558a062d8c33f018d3ef	Apalache	Assume	Forall	True	Passed	Model Under Test Equivalent Model
a230c8f3c63aed509630d5dd0905c4b3f3fd2b03	Apalache	Assume	Forall	False	Passed	Model Under Test Equivalent Model
dfd2e6cd3ebac91a1cf9aa2177085d5abdd414ca	Apalache	AssumeNamed	Forall	True	Passed	Model Under Test Equivalent Model
c59211aeb904cf79e9d877d8dad227d4dfdbf6bb	Apalache	AssumeNamed	Forall	False	Passed	Model Under Test Equivalent Model
949fcede39d65c8eef26c1ffbe56060063ee5200	Apalache	Lambda	Forall	True	Passed	Model Under Test Equivalent Model
7253c14011ca84f19048909b1d9df5b96d19db5d	Apalache	Lambda	Forall	False	Passed	Model Under Test Equivalent Model
0823bbcf75e298e094320566ea3aa438c7706f5d	Apalache	IfCond	Forall	True	Passed	Model Under Test Equivalent Model
18cb9692e220e43b59cb21ace6e24afd00935a34	Apalache	IfCond	Forall	False	Passed	Model Under Test Equivalent Model
ffaffb31738962b888826aecaf1d37e0a3401d8c	Apalache	IfThen	Forall	True	Passed	Model Under Test Equivalent Model
0ffa69c0b8bd99ea88919fe1d3c8d9dfe9958954	Apalache	IfThen	Forall	False	Passed	Model Under Test Equivalent Model
27c2fb4513f41d093ffacafc6ee17ce53bb92187	Apalache	IfElse	Forall	True	Passed	Model Under Test Equivalent Model
e64becb235b46da117356421d24eee99275ac70f	Apalache	IfElse	Forall	False	Passed	Model Under Test Equivalent Model
16b703f30baeb30e753aa7bcffa428886a12e292	Apalache	Unchanged	Forall	True	Passed	Model Under Test Equivalent Model
dd53a7c885f258dc26597aabb2bf62a5cbe7d8d5	Apalache	Unchanged	Forall	False	Passed	Model Under Test Equivalent Model
f1e23e54e17629e36015cf72ad9daae877527a6b	Apalache	Equivalence	Forall	True	Passed	Model Under Test Equivalent Model
9d9992416cdb757610aabc8da674d1caa3e8ffc3	Apalache	Equivalence	Forall	False	Passed	Model Under Test Equivalent Model
d8c561952aa0127ac77a98622b29c2593bd170bf	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Forall	True	Passed	Model Under Test Equivalent Model
08ad44babb69dc7598d4ca85ec70085ba9922aec	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Forall	False	Passed	Model Under Test Equivalent Model
161d3b01ed4c59942ba7e6ef464ca6a7df41d345	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Forall	True	Passed	Model Under Test Equivalent Model
9fe552f823db8aac3e6452dfb105e52d4fbf032e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Forall	False	Passed	Model Under Test Equivalent Model
e134c33198f6ac694a442fc3707de5def482a564	Apalache	BagBagIn	Forall	True	Passed	Model Under Test Equivalent Model
5515e226bb870115e9beceb072020c73283ca1ad	Apalache	BagBagIn	Forall	False	Passed	Model Under Test Equivalent Model
4b53c3ab2d6357e699cf8e6e162cd6e2980e7b23	Apalache	BagCopiesIn	Forall	True	Passed	Model Under Test Equivalent Model
b4169eaa2a7e00cf51202eaa16571d1e0b893688	Apalache	BagCopiesIn	Forall	False	Passed	Model Under Test Equivalent Model
f9aab2f41dc3be4baacac53e91b1133ccd919c12	Apalache	SeqAppend	Forall	True	Passed	Model Under Test Equivalent Model
5860b4311c023aa2a2a167f090048d9ceaca408b	Apalache	SeqAppend	Forall	False	Passed	Model Under Test Equivalent Model

Index

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