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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
0856bc21023b45ce56b3d3c01cf38abd1851bc59	Apalache	And	BoolFalse	True	Passed	Model Under Test Equivalent Model
52a7f03b0e5f6ae081816856a6bad900ac6a7440	Apalache	And	BoolFalse	False	Passed	Model Under Test Equivalent Model
9fb8920de1e19037d8891e9d7cf4186acfb2ebd2	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	BoolFalse	True	Passed	Model Under Test Equivalent Model
0bd45bd0a3e024a6eb9e3671033ea741ed632a7b	TLC with reduction strategy: Case Feature: /\ A /\ B == (A /\ B)	AndMultiLine	BoolFalse	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
55220aeed17a1df57f7c1252539082684702bb7b	Apalache	Not	BoolFalse	True	Passed	Model Under Test Equivalent Model
925f33a35f5b564db7c32d77d5d534663ca819fe	Apalache	Not	BoolFalse	False	Passed	Model Under Test Equivalent Model
1e98021b5e0897ca3087f314c0470d7e8f32e721	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	BoolFalse	True	Passed	Model Under Test Equivalent Model
bf57281e7131775bc3b08eb9a9ca9123dae625cb	TLC with reduction strategy: Case Feature: A \/ B == ~(~A /\ ~B)	Or	BoolFalse	False	Passed	Model Under Test Equivalent Model
42e0ca4efe72f99e6afc1b3b9cb699ebd1b90b69	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	BoolFalse	True	Passed	Model Under Test Equivalent Model
3ee67d16cccef34bdc4094a040f9391c31f695b6	TLC with reduction strategy: Case Feature: \/ A \/ B == (A \/ B)	OrMultiLine	BoolFalse	False	Passed	Model Under Test Equivalent Model
ab78aa39fe9beb288acc2b0858d326c89c384394	Apalache	AndProp	BoolFalse	True	Failed: TLC reports an error if it sees trivially false property. Whereas Apalache returns violation	Model Under Test Equivalent Model
5f286ab4bd180ba58d337bae341c7399907d0125	Apalache	AndProp	BoolFalse	False	Failed: TLC reports an error if it sees trivially false property. Whereas Apalache returns violation	Model Under Test Equivalent Model
18ddd500ad3cdf75c329f317c645e11736267539	Apalache	Boxed	BoolFalse	True	Passed	Model Under Test Equivalent Model
400e779330355fb4567b4013e6d1cbb419ef41a8	Apalache	Boxed	BoolFalse	False	Passed	Model Under Test Equivalent Model
1433cf727e0e566bdfdca64b1b72b30a32716461	Apalache	Eq	BoolFalse	True	Passed	Model Under Test Equivalent Model
24f15a44b2df798de8c821d6fe3f677722ac1808	Apalache	Eq	BoolFalse	False	Passed	Model Under Test Equivalent Model
0f9f2a311ddaecf436a57b8e5747d41a0acd832b	Apalache	Ne	BoolFalse	True	Passed	Model Under Test Equivalent Model
6204ea6f74f4e5cc00990985df20f5b74d986fd2	Apalache	Ne	BoolFalse	False	Passed	Model Under Test Equivalent Model
3870929418abe4114f36583a9a4d04798480ce4f	Apalache	Let	BoolFalse	True	Passed	Model Under Test Equivalent Model
db34a439da0a07814aeb80e65ca4fdb76d980551	Apalache	Let	BoolFalse	False	Passed	Model Under Test Equivalent Model
6a8a731387a90c014efbbc0f72cd0c9dc485d7fb	Apalache	Set0	BoolFalse	True	Passed	Model Under Test Equivalent Model
223582b991e35721bbd09df58c58cfcceebfcfe9	Apalache	Set0	BoolFalse	False	Passed	Model Under Test Equivalent Model
5b6fd8afd8ff41f2841186afa74698078f137622	Apalache	Set1	BoolFalse	True	Passed	Model Under Test Equivalent Model
83d8c8fadfeb797a87a848c2be14ed5c32d71a47	Apalache	Set1	BoolFalse	False	Passed	Model Under Test Equivalent Model
f928a6d04712d14d5ac0ec7296fa98fadf2470af	Apalache	Set2	BoolFalse	True	Passed	Model Under Test Equivalent Model
a3ad33ede5fca116c67b64440e406c4bb98108f3	Apalache	Set2	BoolFalse	False	Passed	Model Under Test Equivalent Model
735c8312749f6271bf0986f0687d4e709bb64cc7	Apalache	Fun	BoolFalse	True	Passed	Model Under Test Equivalent Model
7e02605666bd9d62deb1f94764a38b8e03f24f0f	Apalache	Fun	BoolFalse	False	Passed	Model Under Test Equivalent Model
a4541ea0c0616ffe6efb40a5c2333b461cad22bf	Apalache	In	BoolFalse	True	Passed	Model Under Test Equivalent Model
162d432a160919241ae93996ad57d842d149fc1b	Apalache	In	BoolFalse	False	Passed	Model Under Test Equivalent Model
15d916aaf4e68f10884f641a1dd54a57758f65e6	Apalache	NotIn	BoolFalse	True	Passed	Model Under Test Equivalent Model
7ba1ea5c3b971cbfe10165867c4ad1c2e92083dd	Apalache	NotIn	BoolFalse	False	Passed	Model Under Test Equivalent Model
935d74d83c98c4d11211c89f0203b8ded3cbc310	Apalache	Exists	BoolFalse	True	Passed	Model Under Test Equivalent Model
156c890d66f192fa1b2ec431b1514dba876741b3	Apalache	Exists	BoolFalse	False	Passed	Model Under Test Equivalent Model
07338e830629cab6ed32919cd1672e37dd4a6edd	Apalache	Forall	BoolFalse	True	Passed	Model Under Test Equivalent Model
e98a7038eca3f88850f3ad804646ff9616b07dab	Apalache	Forall	BoolFalse	False	Passed	Model Under Test Equivalent Model
85de1265e6ddc5777839a5372c6cb145958cec88	Apalache	Choose	BoolFalse	True	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
e9af4b5dda8a82ec1c6e9d135089645fb4fded7d	Apalache	Choose	BoolFalse	False	Failed: CHOOSE has different semantics in TLC and Apalache if there is no element in the set, which satisfies the criterion. TLC reports an error and Apalache returns arbitrary value.	Model Under Test Equivalent Model
234b830e0329c6922930656f0f25e4a5ab4bf4eb	Apalache	Record	BoolFalse	True	Passed	Model Under Test Equivalent Model
9f3581360a6c6b0ab7aa585b1ace93b4c9048cb7	Apalache	Record	BoolFalse	False	Passed	Model Under Test Equivalent Model
af71b617f6c925b7b358c75d9f35b54372448725	Apalache	Tuple	BoolFalse	True	Passed	Model Under Test Equivalent Model
74da46e71fd9a4a94b7eb4ed132fdff8b6f15cfb	Apalache	Tuple	BoolFalse	False	Passed	Model Under Test Equivalent Model
20e3efa068ddc747802179871a5b3465f1d603c3	Apalache	FunApp	BoolFalse	True	Passed	Model Under Test Equivalent Model
5497444ca2b778f78a382c6cc535638923735dd5	Apalache	FunApp	BoolFalse	False	Passed	Model Under Test Equivalent Model
5fe36f301b5c68b14c5fbfda7868a58680b4cd51	Apalache	Except1Fun	BoolFalse	True	Passed	Model Under Test Equivalent Model
bb38fb00b68364db31a172800c8f3c0c1da52b2c	Apalache	Except1Fun	BoolFalse	False	Passed	Model Under Test Equivalent Model
799d5e705c66a81039f95be1030b34f3f47f8465	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BoolFalse	True	Passed	Model Under Test Equivalent Model
2232553e9b587721a51fa0a5c06480ceee0534f1	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	BoolFalse	False	Passed	Model Under Test Equivalent Model
0bbb99bff32f0c519f117e8640791ae2c825ca3e	Apalache	Except1Rec	BoolFalse	True	Passed	Model Under Test Equivalent Model
06b896fe0c875f43def73ab54c422f6bb5afed94	Apalache	Except1Rec	BoolFalse	False	Passed	Model Under Test Equivalent Model
1e56b9f5deef7fa4aa8e2fbd0b372e38fb5b4172	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BoolFalse	True	Passed	Model Under Test Equivalent Model
eca583272a4e933322f1db5e3158b7bdb660cb21	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	BoolFalse	False	Passed	Model Under Test Equivalent Model
ac8a25242a2b2a19fdcc769aaeb7f056f4fefe3b	Apalache	Except2Fun	BoolFalse	True	Passed	Model Under Test Equivalent Model
bca68203bf3dfb077e68ce29b4ba875dbf2c994d	Apalache	Except2Fun	BoolFalse	False	Passed	Model Under Test Equivalent Model
3e8d1719329d99212c42e65c339cb41faac80cb4	Apalache	Prime	BoolFalse	True	Passed	Model Under Test Equivalent Model
f9014c53213517944c6e654253c28fc68739ed83	Apalache	Prime	BoolFalse	False	Passed	Model Under Test Equivalent Model
9a5bd8fc221cab88ffc9ff48a3eded87a2a8fca9	Apalache	DefFun	BoolFalse	True	Passed	Model Under Test Equivalent Model
efdca00234252421c0a41f8b6e551b4256371d1d	Apalache	DefFun	BoolFalse	False	Passed	Model Under Test Equivalent Model
97f90e2b51b238aa985f21dc4fa02d3cf20d688b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BoolFalse	True	Passed	Model Under Test Equivalent Model
1440e6784c506a7f48eabcf6ef623ce24ba43a10	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	BoolFalse	False	Passed	Model Under Test Equivalent Model
67f24b292f61c0712f740aa1c9d745d59db25f9a	Apalache	DefFunRecursive	BoolFalse	True	Passed	Model Under Test Equivalent Model
e497e648eb76675220f5a5ea0b064cf9ff89c663	Apalache	DefFunRecursive	BoolFalse	False	Passed	Model Under Test Equivalent Model
6b34cdab45220875e07bf62d9a5f22ead3d5d389	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BoolFalse	True	Passed	Model Under Test Equivalent Model
94e4308a2a9c687d599f45613c9488db7eafaccf	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	BoolFalse	False	Passed	Model Under Test Equivalent Model
0769cf6df8b0111e3ea68cf5680cf6570de1a25c	Apalache	Def0	BoolFalse	True	Passed	Model Under Test Equivalent Model
e550c24cf4ee42bf1a2be7e68d7870b9415f4118	Apalache	Def0	BoolFalse	False	Passed	Model Under Test Equivalent Model
8e77fd0535e1ec0fea9ab609eb8da2a7f87ecd57	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BoolFalse	True	Passed	Model Under Test Equivalent Model
db28d00d3f8bff9e2891591f2b6efe6541c2aa17	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	BoolFalse	False	Passed	Model Under Test Equivalent Model
63a6965e320c77c34094ca144b902cf9d07b79c8	Apalache	Def1	BoolFalse	True	Passed	Model Under Test Equivalent Model
8e3dceac7856ac3f42895d2f3963744da2e50bc8	Apalache	Def1	BoolFalse	False	Passed	Model Under Test Equivalent Model
55df86dbf80ada2ceb8cdda249fa224600299ed8	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BoolFalse	True	Passed	Model Under Test Equivalent Model
1ca0794a32c0edb2a94d52e8580e9bb2afd10993	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	BoolFalse	False	Passed	Model Under Test Equivalent Model
8862f9830bbacf04a9866d0aee72915d3629e29b	Apalache	Def2	BoolFalse	True	Passed	Model Under Test Equivalent Model
70e04f1e4295738e4346770d9c775cba57e2da9e	Apalache	Def2	BoolFalse	False	Passed	Model Under Test Equivalent Model
f3b142e80a5ee54cb33258112ac50dab2b1c11f3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BoolFalse	True	Passed	Model Under Test Equivalent Model
f55c7c5a92a024f2f9a38c42f495a9603953e012	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	BoolFalse	False	Passed	Model Under Test Equivalent Model
210328ac8de01513df49f2342922519fca997c0f	Apalache	Def1Recursive	BoolFalse	True	Passed	Model Under Test Equivalent Model
02aa6d744ba3aaeb7a441ba5574862e940ad3a38	Apalache	Def1Recursive	BoolFalse	False	Passed	Model Under Test Equivalent Model
4013ae863ca032ece376e70359a4f4f592230971	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BoolFalse	True	Passed	Model Under Test Equivalent Model
2ca4ed7d3caa9dd3d123a41c83156d9b21cf1ca3	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	BoolFalse	False	Passed	Model Under Test Equivalent Model
88c476bb25fc0ef88528f3ca2d1310e62ba4f0f8	Apalache	Extends	BoolFalse	True	Passed	Model Under Test Equivalent Model
cb5fb8a47995de121669249b25eff0f08b7d00bd	Apalache	Extends	BoolFalse	False	Passed	Model Under Test Equivalent Model
04bb17a875692fcd1a81dab68a2b7c3fc7e4c2ee	Apalache	ExtendsInDifferentFolder	BoolFalse	True	Passed	Model Under Test Equivalent Model
7465240dacf24a456795ca5262eafc86fbe1b6a8	Apalache	ExtendsInDifferentFolder	BoolFalse	False	Passed	Model Under Test Equivalent Model
d416b36d1af6ab925e99be5bed44bb70b599d3c8	Apalache	Variable	BoolFalse	True	Passed	Model Under Test Equivalent Model
06efdd4e789cee241b922d2887db0fa0ad345c07	Apalache	Variable	BoolFalse	False	Passed	Model Under Test Equivalent Model
700339b84caac4340ef12f9bed643dd6c5fe3440	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BoolFalse	True	Passed	Model Under Test Equivalent Model
7aae012214aff6d739dffcedfb2e2316b962692c	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	BoolFalse	False	Passed	Model Under Test Equivalent Model
90a31cfe2351c3877a9c990aff476bd6f9d98ede	Apalache	Constant	BoolFalse	True	Passed	Model Under Test Equivalent Model
290925cb1855d34e656eb10e0a817d00c36969fc	Apalache	Constant	BoolFalse	False	Passed	Model Under Test Equivalent Model
8a53be181bfc52e45d54259ff9e32ef1259ab05a	Apalache	ConstantRank1	BoolFalse	True	Passed	Model Under Test Equivalent Model
abe6cbd06db1ab6bfbe4f223540ef66cee7158a6	Apalache	ConstantRank1	BoolFalse	False	Passed	Model Under Test Equivalent Model
48c407c33c7a677b163bf0ef174bdc28bb9ce3d3	Apalache	Instance	BoolFalse	True	Passed	Model Under Test Equivalent Model
a81a54f4d3e2beeccf35eb66dbe2b0bc65f28788	Apalache	Instance	BoolFalse	False	Passed	Model Under Test Equivalent Model
74ec2655b480b66ef073c48a7950e597d23124bc	Apalache	InstanceWith	BoolFalse	True	Passed	Model Under Test Equivalent Model
bf3c0aa3e4701be2f31f90b41d79dd49b69626da	Apalache	InstanceWith	BoolFalse	False	Passed	Model Under Test Equivalent Model
5c47f156eb22b069fce473dcb0946489449d542f	Apalache	InstanceNamed	BoolFalse	True	Passed	Model Under Test Equivalent Model
c77d109e2737d71cf9091f6b96cd8cab9085ec16	Apalache	InstanceNamed	BoolFalse	False	Passed	Model Under Test Equivalent Model
90fd9daab81221afee6ce88c42448621ec9afb45	Apalache	InstanceNamedWith	BoolFalse	True	Passed	Model Under Test Equivalent Model
4e97856939057fc81a11c6e4e811523e016df94c	Apalache	InstanceNamedWith	BoolFalse	False	Passed	Model Under Test Equivalent Model
abb641246dd96583ee4b1b8e1554acb8b4e0a0f7	Apalache	InstanceInFolder	BoolFalse	True	Passed	Model Under Test Equivalent Model
79bb0f956be1aa700db7cb4f6ff93d4f6e7c2d85	Apalache	InstanceInFolder	BoolFalse	False	Passed	Model Under Test Equivalent Model
b405e4fc2afdeb43f3b73a58f8439400df47cc0c	Apalache	InstanceWithInFolder	BoolFalse	True	Passed	Model Under Test Equivalent Model
28136f720547b9d50e55f88ab6e08277eac30df9	Apalache	InstanceWithInFolder	BoolFalse	False	Passed	Model Under Test Equivalent Model
c5275974220bdc4e9752377c68d5c565f5cf1bec	Apalache	InstanceNamedInFolder	BoolFalse	True	Passed	Model Under Test Equivalent Model
89d5f6f355d2b1c180affbc2c8f8c07f0bc7ef6f	Apalache	InstanceNamedInFolder	BoolFalse	False	Passed	Model Under Test Equivalent Model
768a805373df47d68afffb1905a8f83961cc83c7	Apalache	InstanceNamedWithInFolder	BoolFalse	True	Passed	Model Under Test Equivalent Model
5bbdce123db6963611d6e0741f7ae4ba06a7e871	Apalache	InstanceNamedWithInFolder	BoolFalse	False	Passed	Model Under Test Equivalent Model
5d9425415c79d7fd9b6407f9eb3d100716e6bc2a	Apalache	Enabled	BoolFalse	True	Passed	Model Under Test Equivalent Model
e5d7e351f1d2a4c04a6827d0297b2a90db5011ce	Apalache	Enabled	BoolFalse	False	Passed	Model Under Test Equivalent Model
2a4eddf14b8b28638c031964f594239d9d39d869	Apalache	Assume	BoolFalse	True	Passed	Model Under Test Equivalent Model
be4148cfbd9a57f8456c1235c223377ee61b5f4a	Apalache	Assume	BoolFalse	False	Passed	Model Under Test Equivalent Model
d8a4c533cccde5070c0ee43590a0990325794eff	Apalache	AssumeNamed	BoolFalse	True	Passed	Model Under Test Equivalent Model
15e7076be3334e2508f6d0540a8d13fe40f8b1bf	Apalache	AssumeNamed	BoolFalse	False	Passed	Model Under Test Equivalent Model
98f6a57bd6736530c61a3d28468e53305c2e1ba7	Apalache	Lambda	BoolFalse	True	Passed	Model Under Test Equivalent Model
50ea1e9f54ff3874c4e28ef3cab6e925a226ea5e	Apalache	Lambda	BoolFalse	False	Passed	Model Under Test Equivalent Model
6a47840bf71e797beb768a736e7419628b9cf53d	Apalache	IfCond	BoolFalse	True	Passed	Model Under Test Equivalent Model
73d3ae1724f1eb279bfb173413e0c232e49707a5	Apalache	IfCond	BoolFalse	False	Passed	Model Under Test Equivalent Model
73338903b4f9f82e4164e6677dc2613dac15fcdc	Apalache	IfThen	BoolFalse	True	Passed	Model Under Test Equivalent Model
5426724b9437cca0127cbf17ec7894c21df5478f	Apalache	IfThen	BoolFalse	False	Passed	Model Under Test Equivalent Model
370f155ee014637f19b3c076cb107552383bb529	Apalache	IfElse	BoolFalse	True	Passed	Model Under Test Equivalent Model
2bff9282cc35e24ddc669d722433b29895731252	Apalache	IfElse	BoolFalse	False	Passed	Model Under Test Equivalent Model
7137701d9d4f237c49e230393f1cf631a97e3acf	Apalache	Unchanged	BoolFalse	True	Passed	Model Under Test Equivalent Model
275975f93f366be21edb0ec793efb487a51cf8d1	Apalache	Unchanged	BoolFalse	False	Passed	Model Under Test Equivalent Model
557626860ef46ec7a7076a354d09b25fabecfe30	Apalache	Equivalence	BoolFalse	True	Passed	Model Under Test Equivalent Model
90cbc98d1426fdab82d2a8ba594d4a7255344e83	Apalache	Equivalence	BoolFalse	False	Passed	Model Under Test Equivalent Model
0d8c501100d53ad9df6fbc5ad9c7ef4634a05b39	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BoolFalse	True	Passed	Model Under Test Equivalent Model
b5061aed8bdaa77bb01b4c0ffa9dd645bc196f4e	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	BoolFalse	False	Passed	Model Under Test Equivalent Model
99859ccbe0a85f6b0a1e403e702c83aee3335151	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BoolFalse	True	Passed	Model Under Test Equivalent Model
ef5dc9f851b9ded0c21e3403eb6cca3e64baa69e	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	BoolFalse	False	Passed	Model Under Test Equivalent Model
7091f83aebd93858fba2eccbf6b11ae10dbaa6b7	Apalache	BagBagIn	BoolFalse	True	Passed	Model Under Test Equivalent Model
7018a9a746b635fdcf0fa69bfabbca22c08c8e1d	Apalache	BagBagIn	BoolFalse	False	Passed	Model Under Test Equivalent Model
8d7bcb754c0e6494f62b59dfa1b42b451268d5de	Apalache	BagCopiesIn	BoolFalse	True	Passed	Model Under Test Equivalent Model
8d03ceffb86f40cfcac4d718acd3a80e5a00e92b	Apalache	BagCopiesIn	BoolFalse	False	Passed	Model Under Test Equivalent Model
a1ae4630261a6a4493e3f00e6516c7c56333ebc2	Apalache	SeqAppend	BoolFalse	True	Passed	Model Under Test Equivalent Model
efc523748bdf037cb5f3d4c2de2a0fb0112dd716	Apalache	SeqAppend	BoolFalse	False	Passed	Model Under Test Equivalent Model

Index

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