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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
aa5924b2eaecad3a8c92173f9614ac9141901277	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Domain	OneLineComment	True	Passed	Model Under Test Equivalent Model
6520d88f3c3920aff11f5c2b4433439b2b1d63a3	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Domain	OneLineComment	False	Passed	Model Under Test Equivalent Model
527c0414f2aa0697508e00d3792f2850c9dfc44b	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Domain	MultiLineComment	True	Passed	Model Under Test Equivalent Model
412b3703e681f7996a74fdd461e146bc85700626	TLC with reduction strategy: Plug Feature: Replace spec with the same without comments	Domain	MultiLineComment	False	Passed	Model Under Test Equivalent Model
498b34db27febf443af0bdea731f6108d761ecd0	Apalache	Domain	Let	True	Passed	Model Under Test Equivalent Model
499bf05fae91fda8b6ce3516aa85c42abfc865ea	Apalache	Domain	Let	False	Passed	Model Under Test Equivalent Model
f3d28f0741057fea14b87e060b6b574d828d86cf	Apalache	Domain	Fun	True	Passed	Model Under Test Equivalent Model
f10815f53fe40abb79b700fd9f3fc68cbefd545d	Apalache	Domain	Fun	False	Passed	Model Under Test Equivalent Model
eafa16fbccc0d81cbdc1e2837492f734f768f6d6	Apalache	Domain	Choose	True	Passed	Model Under Test Equivalent Model
0d5d567ffe9752c11f26310fef6fdb59329e5e7e	Apalache	Domain	Choose	False	Passed	Model Under Test Equivalent Model
2b78423e2bfe6f581cda515f9951cfec1ef565db	Apalache	Domain	FunApp	True	Passed	Model Under Test Equivalent Model
5086daa513c9bef3509fb6e6f389aa4ee9a60d98	Apalache	Domain	FunApp	False	Passed	Model Under Test Equivalent Model
92304b23b22c82ec6703e23c430c06eb07e444d5	Apalache	Domain	Prime	True	Passed	Model Under Test Equivalent Model
c7c11f755b261eb964fa70560d627c89ecba817c	Apalache	Domain	Prime	False	Passed	Model Under Test Equivalent Model
5bcf9fafe9a93b4105d0a13936113ea4e1d36e1d	Apalache	Domain	DefFun	True	Passed	Model Under Test Equivalent Model
b2210e178018be3a01dc8f634d269ae97ba3da8a	Apalache	Domain	DefFun	False	Passed	Model Under Test Equivalent Model
e649b1acae504205e7a5225ea079d30bc73231f4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDefFun	True	Passed	Model Under Test Equivalent Model
b0646dc33158582d5bab2115a4c4f373635fe325	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDefFun	False	Passed	Model Under Test Equivalent Model
32238dc277d8ef11fa08b5cfcb6cf0ca5e2e6f89	Apalache	Domain	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
c200f0dbc3836824ee7d5ad79df7ced88740354b	Apalache	Domain	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
7f3180de1e46d4ba3c44eb006ffbef10a1eda92f	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
d3543c46ef5f2fdf70d1d98a2fc5d46691077d8e	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
9b35ea3219296bb4091c5c5411035ca01f81e642	Apalache	Domain	Def0	True	Passed	Model Under Test Equivalent Model
774db65943744cd60ab084b8f83522ae843a685e	Apalache	Domain	Def0	False	Passed	Model Under Test Equivalent Model
69dc0045e5cb063274ab0af61993117f4f9a4627	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef0	True	Passed	Model Under Test Equivalent Model
49040e40ee967f4f32675368146b632e4f26aeb4	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef0	False	Passed	Model Under Test Equivalent Model
a251da9021f0f21b97f2423b108d307e8a23312f	Apalache	Domain	Def1	True	Passed	Model Under Test Equivalent Model
b1c8f21cac1b86663aa19fc35303ae4c8c41ca3e	Apalache	Domain	Def1	False	Passed	Model Under Test Equivalent Model
0fdafb56605289dafa4a68475c4a50593bd7756a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef1	True	Passed	Model Under Test Equivalent Model
c083126530f268ea9079e9e754c38ab17c3cc935	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef1	False	Passed	Model Under Test Equivalent Model
fff4468113eae0559c5a792ca78355367ed33425	Apalache	Domain	Def2	True	Passed	Model Under Test Equivalent Model
4c5ca1368833b812036911d0f564a76a11eee105	Apalache	Domain	Def2	False	Passed	Model Under Test Equivalent Model
52c38468b0b326ef4fdea013067d5d6332f880a2	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef2	True	Passed	Model Under Test Equivalent Model
b617f78dd91a5c33d1d19c1f63d5254498749857	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef2	False	Passed	Model Under Test Equivalent Model
426bf08b90b3c87607ed3fe4407be85a77c3bf5b	Apalache	Domain	Def1Recursive	True	Passed	Model Under Test Equivalent Model
16011e3dfe9c233f49cf7dfbf2ee6e41aa20a91c	Apalache	Domain	Def1Recursive	False	Passed	Model Under Test Equivalent Model
bcaec5de117716367cf00f5e9b3d340d1c46673c	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
bb1f88d9f188a7d654a1cf86d4374e96867ed022	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Domain	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
ee6600a9430a8c44da73a966ab031bbcc3b80951	Apalache	Domain	Extends	True	Passed	Model Under Test Equivalent Model
1dd07f515015b1b5a13faadd5021f29c6f0fb729	Apalache	Domain	Extends	False	Passed	Model Under Test Equivalent Model
ad7c2467320c488cf16d3102dab4a8a9d1ca4534	Apalache	Domain	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
ea9ccd789d977857703fba49e6385478e98ce6b9	Apalache	Domain	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
4b0b8947f3610fc06cf98b497d034ba8117b8d9b	Apalache	Domain	Variable	True	Passed	Model Under Test Equivalent Model
6ecf89d28d55d9f3e354e1ddd8d1994200ef1e73	Apalache	Domain	Variable	False	Passed	Model Under Test Equivalent Model
39ee78787bf8ef298d12c573aeaceeb499e0539d	Apalache	Domain	Constant	True	Passed	Model Under Test Equivalent Model
5c58e70d0b84a7bc85d38170a208e07548e4d176	Apalache	Domain	Constant	False	Passed	Model Under Test Equivalent Model
e20f92bb3074ed09fa3ecec11fb6724a5b8549c6	Apalache	Domain	ConstantRank1	True	Passed	Model Under Test Equivalent Model
f08fb8c741cec77f1c12a9f6ebefb1129c74f707	Apalache	Domain	ConstantRank1	False	Passed	Model Under Test Equivalent Model
842bd011cb878dac2b3d85d1a84c9dcf3e6eb55f	Apalache	Domain	Instance	True	Passed	Model Under Test Equivalent Model
16bf96ae0fa0e8e85b2628dd36c67866e5a805f2	Apalache	Domain	Instance	False	Passed	Model Under Test Equivalent Model
ea794cbf75f587eeeed46e6dade4182224b5ff28	Apalache	Domain	InstanceWith	True	Passed	Model Under Test Equivalent Model
f6b60637fa3359682833944d591a3ac8a5e73d27	Apalache	Domain	InstanceWith	False	Passed	Model Under Test Equivalent Model
8b0d5c9398139be6ae0c2dba4f9582239944578d	Apalache	Domain	InstanceNamed	True	Passed	Model Under Test Equivalent Model
542167f2d367254777bde288f3d50b186765eae9	Apalache	Domain	InstanceNamed	False	Passed	Model Under Test Equivalent Model
09c9de832d8e66c7f9bc1908d3671fed2071efc4	Apalache	Domain	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
008951f1c9701bbc8eacc89e756d3a8ca5963b09	Apalache	Domain	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
49dd052bb419d2f67523261e0613f2175c77d7e5	Apalache	Domain	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
741b4c7c134cdd61d7e067ca5ee96f1994d99d81	Apalache	Domain	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
4836934049d7441262d004ec7f441612f8524ac2	Apalache	Domain	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
3deff240ba8712fdac205609bd3d98369f6b1f88	Apalache	Domain	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
1810493b7d3a2f519fd1c33c182d12b2d6cfa9d5	Apalache	Domain	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
0482a43d65009d80ddffac7336520a95771012d0	Apalache	Domain	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
c179b4325969d9f56406306c31da64a50f1a6d25	Apalache	Domain	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
4b02842e7b7a28c8256f55c405e5c8920f2a22bd	Apalache	Domain	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
96be80444072c588e07c7dc20081b2287b47bd05	Apalache	Domain	IfCond	True	Passed	Model Under Test Equivalent Model
9344488fb2e4159089936702a586716d12328e57	Apalache	Domain	IfCond	False	Passed	Model Under Test Equivalent Model
6b4b7f392852c2d5b2b9d47a4048197597084e54	Apalache	Domain	IfThen	True	Passed	Model Under Test Equivalent Model
0f11d49e7bef588fb07fd125a711d23750ebaacc	Apalache	Domain	IfThen	False	Passed	Model Under Test Equivalent Model
df6bbedd5ce2207e1c31531cceb0934cc179ce6b	Apalache	Domain	IfElse	True	Passed	Model Under Test Equivalent Model
3bd901037df53eb0dd4d257304ac12fe71c9cce8	Apalache	Domain	IfElse	False	Passed	Model Under Test Equivalent Model
6e6d7d1d46e3baca9bc0eea5d738275e31efe697	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Domain	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
bf6a3abde7d7cf6b172a8664e3c4e23ea924e1d4	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Domain	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
c373fe34f0249be404ebfdd4ebfe338f72911d3e	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Domain	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
412d2f11722a9dbe1a6086bc8fba52ea7ba8832d	TLC with reduction strategy: Plug Feature: f @@ g is replaced with equivalent: LET DomF == DOMAIN f IN [u \in DomF \union DOMAIN g \|-> IF u \in DomF THEN f[u] ELSE g[x]]	Domain	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
473ef9590017e60e1fe84f85b95488ea38c0c4f2	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Domain	TlcEval	True	Passed	Model Under Test Equivalent Model
d376d89e9483f3b7995f05b8c16bbbafe41cb80a	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Domain	TlcEval	False	Passed	Model Under Test Equivalent Model
3e3be0578ea3643ef27e90aa9fdffcf3405a08c6	Apalache	Domain	SeqHead	True	Passed	Model Under Test Equivalent Model
53ef9984666deb57f97ae5ce6a993f09ccf09b0d	Apalache	Domain	SeqHead	False	Passed	Model Under Test Equivalent Model

Index

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