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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
3bff317541c2a2276b2c51a6022c9bcbd0dff797	Apalache	FunApp	BoolTrue	True	Passed	Model Under Test Equivalent Model
9a5d16f29c2529042018a32f2e9c0f5c4fe2e27f	Apalache	FunApp	BoolTrue	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
de68dd4c3d45671e717fce375d8da8863a4791ff	Apalache	FunApp	BoolSet	True	Passed	Model Under Test Equivalent Model
a2c68b08e0a96d54277e92023f3e11d0a596c7ef	Apalache	FunApp	BoolSet	False	Passed	Model Under Test Equivalent Model
7888fe3891a88c2ebc2d8b2456728ae30e2b8476	Apalache	FunApp	And	True	Passed	Model Under Test Equivalent Model
1a51acb4d4ecfb8ffb4d9b0f002269d19817e300	Apalache	FunApp	And	False	Passed	Model Under Test Equivalent Model
6e8545802c4355608e0c5b84644db0a19bad66fe	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	FunApp	AndMultiLine	True	Passed	Model Under Test Equivalent Model
66348926e10cea2841d82cf669a2c90d8f961ea1	TLC with reduction strategy: Plug Feature: /\ A /\ B == (A /\ B)	FunApp	AndMultiLine	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
3976d45ff757e3f0ee83cce760661b367bfd44af	Apalache	FunApp	Not	True	Passed	Model Under Test Equivalent Model
bb4a571886b0fedc04e67f468956e1de5b2a85b8	Apalache	FunApp	Not	False	Passed	Model Under Test Equivalent Model
117f7260d32e527630770f19d3ecd71fea66a6cc	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	FunApp	Or	True	Passed	Model Under Test Equivalent Model
7f9e192f3c67601009bdd397c3606b3e92ca5e79	TLC with reduction strategy: Plug Feature: A \/ B == ~(~A /\ ~B)	FunApp	Or	False	Passed	Model Under Test Equivalent Model
0f1635a4c2419d19ee167efd785d710120b3cee9	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	FunApp	OrMultiLine	True	Passed	Model Under Test Equivalent Model
9b86833630eb7c6fb010d9f7dad195969aee045d	TLC with reduction strategy: Plug Feature: \/ A \/ B == (A \/ B)	FunApp	OrMultiLine	False	Passed	Model Under Test Equivalent Model
15faf7a7809b1a9da565998da2e87ec3d8d31677	Apalache	FunApp	Eq	True	Passed	Model Under Test Equivalent Model
8fd3d412b11409854be6e399dadcfbc0383bdb9f	Apalache	FunApp	Eq	False	Passed	Model Under Test Equivalent Model
164448b2a4918c74ca0d5d9432ff111af8cbecc2	Apalache	FunApp	Ne	True	Passed	Model Under Test Equivalent Model
dafa9e12119fdff9860c25b84c7cb92c238568e7	Apalache	FunApp	Ne	False	Passed	Model Under Test Equivalent Model
e779f6477b2718781087209699e7a8f06e2e9725	Apalache	FunApp	Let	True	Passed	Model Under Test Equivalent Model
c46c5e066b167212d1c83fd47a3eae78c29c2435	Apalache	FunApp	Let	False	Passed	Model Under Test Equivalent Model
04f490b5ce4456c9e5558e5e5bc171b19c51da5d	Apalache	FunApp	SetEmpty	True	Passed	Model Under Test Equivalent Model
220911ba87fb47f88c59367369f1e60fc3d9c0a8	Apalache	FunApp	SetEmpty	False	Passed	Model Under Test Equivalent Model
b0ce8dfd3f3cec0ae3691beb4906940e2f9a4a70	Apalache	FunApp	Set0	True	Passed	Model Under Test Equivalent Model
db7f49afb903b4fe40c339f60dc48885694c8023	Apalache	FunApp	Set0	False	Passed	Model Under Test Equivalent Model
e02bdb8a3ba6eadb306381ae3319bb111387dc8b	Apalache	FunApp	Set1	True	Passed	Model Under Test Equivalent Model
bcac5fc0c2b805a74714dc4863c9d1b46b4a427b	Apalache	FunApp	Set1	False	Passed	Model Under Test Equivalent Model
55a16b965fa57846985aa2e4d1fe31f8d34f58b8	Apalache	FunApp	Set2	True	Passed	Model Under Test Equivalent Model
a4453836f6f4b080cd87b17e75bb85676684ffa6	Apalache	FunApp	Set2	False	Passed	Model Under Test Equivalent Model
1e9929725fe522ddd1a6bed2c88e8262127270b0	Apalache	FunApp	Fun	True	Passed	Model Under Test Equivalent Model
080182f5b3a1c49f5d516ecd6c08d275bd8b0643	Apalache	FunApp	Fun	False	Passed	Model Under Test Equivalent Model
7c2f0eea16f0a3767241e0672894b1f14d00929f	Apalache	FunApp	In	True	Passed	Model Under Test Equivalent Model
e7c9545ed582dacb8b30a60267c81fc1fa82e9d3	Apalache	FunApp	In	False	Passed	Model Under Test Equivalent Model
69517f5a04a46f437bc10b64b919ab49316206ec	Apalache	FunApp	NotIn	True	Passed	Model Under Test Equivalent Model
f708613bf0af7918792d0a093acde6bd4040fe83	Apalache	FunApp	NotIn	False	Passed	Model Under Test Equivalent Model
3367010539b900ab6c3b83982f31c691c0ffacdb	Apalache	FunApp	Exists	True	Passed	Model Under Test Equivalent Model
4b7c7843fdeaee1618938e4165020e573a836996	Apalache	FunApp	Exists	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
590e54bad482488ea9aa6e33cf3833b3eb33e59e	Apalache	FunApp	Choose	True	Passed	Model Under Test Equivalent Model
6fd51fe932d8b8852acb7d3d863a9bc7630b972b	Apalache	FunApp	Choose	False	Passed	Model Under Test Equivalent Model
f583f2866b57e54bb7f4da1590f7322a0622b17b	Apalache	FunApp	Record	True	Passed	Model Under Test Equivalent Model
737de45efafaf1e23261154b6e51e7c79377e1a5	Apalache	FunApp	Record	False	Passed	Model Under Test Equivalent Model
f491c1f144f0810ace9e3e2d97888201498ce020	Apalache	FunApp	Tuple	True	Passed	Model Under Test Equivalent Model
5b47844d117f1d5a5429547aef1c33af553985d1	Apalache	FunApp	Tuple	False	Passed	Model Under Test Equivalent Model
cdf78ceed0b53146c6672f9140c27fd4bb68da5b	Apalache	FunApp	TupleEmpty	True	Failed: TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
a4604139020fc219015253d4a621cfdf1a4c7cef	Apalache	FunApp	TupleEmpty	False	Failed: TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
59601f7b08f17e976629808295cd70a7f75a0502	Apalache	FunApp	FunApp	True	Passed	Model Under Test Equivalent Model
24c5e73972831495bea5a070456a0373496d6e0f	Apalache	FunApp	FunApp	False	Passed	Model Under Test Equivalent Model
cb00cc7a3e02a8b28b27c68815f069c687843cd5	Apalache	FunApp	Prime	True	Passed	Model Under Test Equivalent Model
b13d460e80061c3558dbdd2248960255a04cb6e4	Apalache	FunApp	Prime	False	Passed	Model Under Test Equivalent Model
736f98e047db9970be2efbbda5b28537dc1a6a18	Apalache	FunApp	NumZero	True	Passed	Model Under Test Equivalent Model
671ff60a83132a0bbba961ead37b8a5e63d84b60	Apalache	FunApp	NumZero	False	Passed	Model Under Test Equivalent Model
6f6ccbbefa57702a44b7d8621176e4820a669b77	Apalache	FunApp	NumOne	True	Passed	Model Under Test Equivalent Model
4fa3e79daf36ac528eb8ca396b38dfdc2d6f3c9d	Apalache	FunApp	NumOne	False	Passed	Model Under Test Equivalent Model
f3717938369e21f71b53af3b0e9d565bf6aa9dba	Apalache	FunApp	NumMaxInt	True	Passed	Model Under Test Equivalent Model
4010b10fc635c68c332553049fe1d2ff258976ca	Apalache	FunApp	NumMaxInt	False	Passed	Model Under Test Equivalent Model
402bd9ed798f6e102651ffe0e4932a6b4c573f96	Apalache	FunApp	NumUnaryMinus	True	Passed	Model Under Test Equivalent Model
4e22949e02573bba14e667dcdd16b962b52d2c30	Apalache	FunApp	NumUnaryMinus	False	Passed	Model Under Test Equivalent Model
9fa9058f7693d149ec6d2c787afd5e3cea5ed27a	Apalache	FunApp	NumPlus	True	Passed	Model Under Test Equivalent Model
2c97657efa7bc7ac6e2276f85494960df8c8bcf6	Apalache	FunApp	NumPlus	False	Passed	Model Under Test Equivalent Model
a31f9bcd399333c0decb2ce898ae4fd104fc2785	Apalache	FunApp	NumMinus	True	Passed	Model Under Test Equivalent Model
90b4cc25e9eb76d984d71b9def47ee0c853cb7e4	Apalache	FunApp	NumMinus	False	Passed	Model Under Test Equivalent Model
73d194eaa291cfc62b3d055685b27fcdfe2dad85	Apalache	FunApp	NumMul	True	Passed	Model Under Test Equivalent Model
9b77a13cc0d404f08e678fedcd68069f2f75b9de	Apalache	FunApp	NumMul	False	Passed	Model Under Test Equivalent Model
c3cb86fb6a39c5efd2c5979b1826f917ff425589	Apalache	FunApp	NumDiv	True	Passed	Model Under Test Equivalent Model
b2d274f112bca1681ecde16c2e4616cafd98add8	Apalache	FunApp	NumDiv	False	Passed	Model Under Test Equivalent Model
c62f83c3c0ce3a9628fb7856dbaa565947514213	Apalache	FunApp	NumMod	True	Passed	Model Under Test Equivalent Model
7d6798068a73feb099f7b3d3d1af296d78dca3c1	Apalache	FunApp	NumMod	False	Passed	Model Under Test Equivalent Model
34754c75aac6bb08b49ca9d93584e7bb20ea92c4	Apalache	FunApp	NumPow	True	Passed	Model Under Test Equivalent Model
1a79a9185d5f0ccf5bc5c066d8a0c2a76122cdc6	Apalache	FunApp	NumPow	False	Passed	Model Under Test Equivalent Model
48f1ee85219782297459468a382d2fa8c03bd4f2	Apalache	FunApp	NumGt	True	Passed	Model Under Test Equivalent Model
b2abd64f3625068e53aacc792d74a45b250193fb	Apalache	FunApp	NumGt	False	Passed	Model Under Test Equivalent Model
4682732aeb12e51931ad6d2193caeb7595cfcc48	Apalache	FunApp	NumGe	True	Passed	Model Under Test Equivalent Model
82af2d52ed8f6124e712c1094a134d3378cca368	Apalache	FunApp	NumGe	False	Passed	Model Under Test Equivalent Model
cc309cfc6dc96e88c5e0eaa2019910f52801bcb6	Apalache	FunApp	NumLt	True	Passed	Model Under Test Equivalent Model
dac95254c399a40dfbc8920dd951e93424a4338d	Apalache	FunApp	NumLt	False	Passed	Model Under Test Equivalent Model
15495a746306d9f212a0a8f5bd02d17c98ef77e6	Apalache	FunApp	NumLe	True	Passed	Model Under Test Equivalent Model
b3d7afbc4a5ce0e5386ee5951b9ed00534fa73d6	Apalache	FunApp	NumLe	False	Passed	Model Under Test Equivalent Model
05ef20e73a72ac5ea7646c466226789dbb28c7f6	Apalache	FunApp	DefFun	True	Passed	Model Under Test Equivalent Model
b6d968d0280ea494d94e8fcdad304224ed4eeca5	Apalache	FunApp	DefFun	False	Passed	Model Under Test Equivalent Model
80f87a39372e13666bcbc2412abe8524b105cc65	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDefFun	True	Passed	Model Under Test Equivalent Model
5bba05752c9c6aca297aa95fe9937ffc2170a5d1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDefFun	False	Passed	Model Under Test Equivalent Model
991080016df7b4a87ff350f16ece7553bdbcd4d5	Apalache	FunApp	DefFunRecursive	True	Passed	Model Under Test Equivalent Model
4b51e4ce0c65d8a9047e6803bcfa27665964beca	Apalache	FunApp	DefFunRecursive	False	Passed	Model Under Test Equivalent Model
ec4a05864265775be2b7e5feff4c66e48ac69cf3	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
f1117b378a683ac1c8b0777b71c2f20f3dfe121d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
b0cb2f76fd006f4ef8ad7e68e09e97b48607adc3	Apalache	FunApp	Def0	True	Passed	Model Under Test Equivalent Model
2379556892eaec43d2288e0c6924d704a65fe63f	Apalache	FunApp	Def0	False	Passed	Model Under Test Equivalent Model
d398d33751cbea07cb84f3eb275f9f0db9a5c190	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef0	True	Passed	Model Under Test Equivalent Model
f6b3656b47ce3d6d578cabda36e463466c543f12	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef0	False	Passed	Model Under Test Equivalent Model
74db2085bf55e1adf2595ef8b61f8d1a97f65d2f	Apalache	FunApp	Def1	True	Passed	Model Under Test Equivalent Model
1b069fd0c4d3976d3e59271a2182f6e6c94a14c5	Apalache	FunApp	Def1	False	Passed	Model Under Test Equivalent Model
d74f5d067babee1d51ae438f72498b63cab42045	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef1	True	Passed	Model Under Test Equivalent Model
ff26aa35219e2ed6d88c99efa49216d9a6f62018	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef1	False	Passed	Model Under Test Equivalent Model
e64b2c2d8d53445c217da31db104755109233305	Apalache	FunApp	Def2	True	Passed	Model Under Test Equivalent Model
578c3c391d87cd6f567ac3457e15ccbfc8115656	Apalache	FunApp	Def2	False	Passed	Model Under Test Equivalent Model
2445b0206d353fd6f4571df7dacc55c208410626	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef2	True	Passed	Model Under Test Equivalent Model
a5ee8321b587d2ff9e9cb57d53c6f8d2bcbd6971	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef2	False	Passed	Model Under Test Equivalent Model
0c78036e5449af6f093b61f4b07c6ad3ac695f58	Apalache	FunApp	Def1Recursive	True	Passed	Model Under Test Equivalent Model
adb0269c991e2239b8c01977dc5b40ac1f8cdbab	Apalache	FunApp	Def1Recursive	False	Passed	Model Under Test Equivalent Model
ca5e7a2af9911cbc29fda2fcc4276f2d591fdec1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
a3aa265e0cda70780545544ee8923f2482616deb	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	FunApp	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
09789a68e2d11a49f4af83c64cb8e660d386bf2f	Apalache	FunApp	Extends	True	Passed	Model Under Test Equivalent Model
253fad0dfd5c3b12b9e0c6a2eccbce1cb296995b	Apalache	FunApp	Extends	False	Passed	Model Under Test Equivalent Model
6dbc7ffe8b19246e434dacdbc46f3ce97e818f65	Apalache	FunApp	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
3e484aa0bc2cbdbc0f64e286b3b0bebc957b9568	Apalache	FunApp	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
144786a7f8f906f2f109dc2cdd6b2fde806eace3	Apalache	FunApp	Variable	True	Passed	Model Under Test Equivalent Model
0d19b13e9254bf5446840a52251b7e9d07febfa1	Apalache	FunApp	Variable	False	Passed	Model Under Test Equivalent Model
e02f94f25e26882bad51a8eea3886822df2e56fb	Apalache	FunApp	Constant	True	Passed	Model Under Test Equivalent Model
07b8bdadf8d9d748e67c4237b62583fe3ba4fa76	Apalache	FunApp	Constant	False	Passed	Model Under Test Equivalent Model
44c41f34535d83f86a0b2279ca4defbdf3adbfc2	Apalache	FunApp	ConstantModelValue	True	Passed	Model Under Test Equivalent Model
09012b36c8dcc22a842ea5ea5b70f76b8fc88261	Apalache	FunApp	ConstantModelValue	False	Passed	Model Under Test Equivalent Model
b993d28cf283ab1f94475dc287b3dec57c69ae4f	Apalache	FunApp	ConstantRank1	True	Passed	Model Under Test Equivalent Model
e0e0e142cf9d32aa85f72612999a27f3106c05e2	Apalache	FunApp	ConstantRank1	False	Passed	Model Under Test Equivalent Model
1879578d93f35f9bbb7c9d61a00c76e04cbdb84c	Apalache	FunApp	Instance	True	Passed	Model Under Test Equivalent Model
4607d9f05e3eb39f2aedcfeaf49b684f58b22542	Apalache	FunApp	Instance	False	Passed	Model Under Test Equivalent Model
18baae4b069e5585a99a6a26c55c7e073c179bc5	Apalache	FunApp	InstanceWith	True	Passed	Model Under Test Equivalent Model
bd2faf68c1ce916fc8f43ca3e9dec5d5ceceb6d7	Apalache	FunApp	InstanceWith	False	Passed	Model Under Test Equivalent Model
9d80a06d7ed8e27ad8c23100fbd1a14668f74490	Apalache	FunApp	InstanceNamed	True	Passed	Model Under Test Equivalent Model
23b1fd438ceb1d5063908e20f3380ff6a4ee6c87	Apalache	FunApp	InstanceNamed	False	Passed	Model Under Test Equivalent Model
66abd7a73566bab758fe1f5dc90c9563f4bd0886	Apalache	FunApp	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
f717adf41897f78dfac56f8fa50499ec418e057e	Apalache	FunApp	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
7ea5e3d4ecf41dfdf367ab07336a41e444680643	Apalache	FunApp	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
5c75d14a627399f6444c580f643a466dfbec6d08	Apalache	FunApp	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
faaf35f248dcd55c4c0d86557e0f95c8cbaa7e4b	Apalache	FunApp	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
9e2c204ba779075ab76b068363735b5e6e571a8b	Apalache	FunApp	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
16970c3193a8d97db22c54fbd1090fbcbcf22e84	Apalache	FunApp	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
5c00c97791ab4babf8b337fbc2c2179a9d67604d	Apalache	FunApp	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
15521c437ffd67983a723eab82604e767a1f7399	Apalache	FunApp	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
ae31652aa3f2b75af9b1e54919a0f0b0bfccdaf6	Apalache	FunApp	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
d96489168c995807f457b4e92ff156e8080009aa	Apalache	FunApp	Enabled	True	Passed	Model Under Test Equivalent Model
92980fef8568cea05e465240de2bfc70dd6b8f71	Apalache	FunApp	Enabled	False	Passed	Model Under Test Equivalent Model
0d173ee986fd20474565425305c51fa46b6e4590	Apalache	FunApp	Cross2	True	Passed	Model Under Test Equivalent Model
38a3922457e7dbb24c2fc8b9de1e48152c62f7b6	Apalache	FunApp	Cross2	False	Passed	Model Under Test Equivalent Model
5158f5d6a1895dadb03a49a0199329813f6372f7	Apalache	FunApp	Cross3	True	Passed	Model Under Test Equivalent Model
521972b0ddc953bd066a9b8182adb898036361bf	Apalache	FunApp	Cross3	False	Passed	Model Under Test Equivalent Model
0a40390b40d71ca76217252cc9e442b748c5efb3	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	FunApp	FunSet	True	Passed	Model Under Test Equivalent Model
f0bcfd32a1e6cf0ffbc6b493018b0c58a186d393	TLC with reduction strategy: Plug Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))	FunApp	FunSet	False	Passed	Model Under Test Equivalent Model
8767ced8a08a45ba8c9a44322f420216d2791bae	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	FunApp	RecordSet	True	Passed	Model Under Test Equivalent Model
2009f007c92efce69fbdaac5a4031e6355136aae	TLC with reduction strategy: Plug Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)	FunApp	RecordSet	False	Passed	Model Under Test Equivalent Model
1c639ef7deca21ab9310ac431642230166b696d9	Apalache	FunApp	SetDiff	True	Passed	Model Under Test Equivalent Model
367cc7328dd0b1b2b29ee9382ce5b1e120a9ef0e	Apalache	FunApp	SetDiff	False	Passed	Model Under Test Equivalent Model
253e7c7b31440ca4cd6e7e3b4bf1b72be693c297	Apalache	FunApp	SetUnion	True	Passed	Model Under Test Equivalent Model
93313d759fa3110a506b45eb9a0a6617b6d20ed6	Apalache	FunApp	SetUnion	False	Passed	Model Under Test Equivalent Model
c83b74bd83c1e9e3f0a9e19f48cb84dd032a80a5	Apalache	FunApp	SetIntersect	True	Passed	Model Under Test Equivalent Model
b01f1feb8ec91c9fdb7a77ae11637abe43d98965	Apalache	FunApp	SetIntersect	False	Passed	Model Under Test Equivalent Model
6d4df3c15d6f16bc9338a83da8d5b116cf7f1a36	Apalache	FunApp	SubsetEq	True	Passed	Model Under Test Equivalent Model
5017a5f4cb15b1062303bce83f8d1a607b4c4d8a	Apalache	FunApp	SubsetEq	False	Passed	Model Under Test Equivalent Model
5cd7f0ce64754ecbb70caffd1744a2caafb678f7	Apalache	FunApp	IfCond	True	Passed	Model Under Test Equivalent Model
ad95b77709069e2b39cfa84bd0fa2a49168cf72f	Apalache	FunApp	IfCond	False	Passed	Model Under Test Equivalent Model
5c434a376989301b58f0dede3ba2332a473b4069	Apalache	FunApp	IfThen	True	Passed	Model Under Test Equivalent Model
02a29d2832c01b57a58a19d04c35b334c2d3302c	Apalache	FunApp	IfThen	False	Passed	Model Under Test Equivalent Model
a5e810207342613d85616a596095555c1ba1951e	Apalache	FunApp	IfElse	True	Passed	Model Under Test Equivalent Model
e96762ce5528f1d9946226a9a331c81171dbe094	Apalache	FunApp	IfElse	False	Passed	Model Under Test Equivalent Model
81c71bd37ee26c22cd13dd8fae8dcfbed975b913	Apalache	FunApp	Subset	True	Passed	Model Under Test Equivalent Model
50d522e97c9bccf438acb419e9e45289b1a1a31b	Apalache	FunApp	Subset	False	Passed	Model Under Test Equivalent Model
cef96115cc95c6afa28a6418da0f5e25e875937e	Apalache	FunApp	Domain	True	Passed	Model Under Test Equivalent Model
20c4cf703d5a31233eecf2fc8f09d81a5fb393fa	Apalache	FunApp	Domain	False	Passed	Model Under Test Equivalent Model
7e42949ba5bf3e834af212a766c849805aa6a0d3	Apalache	FunApp	Union	True	Passed	Model Under Test Equivalent Model
ed73c9f7776ffcda2100b25212182b2ecc1b5ec7	Apalache	FunApp	Union	False	Passed	Model Under Test Equivalent Model
88f60a3488ea87e4cf6969cc2dc5cc23aba981ef	Apalache	FunApp	Unchanged	True	Passed	Model Under Test Equivalent Model
1f5386e57cdc8528b1197b878dc8316f50d472f9	Apalache	FunApp	Unchanged	False	Passed	Model Under Test Equivalent Model
5f85a14a36c7aa8a193027362e4fdf5c6275448a	Apalache	FunApp	Equivalence	True	Passed	Model Under Test Equivalent Model
38d8eab84ea70c0176b477ecfb52ec79ef39e80c	Apalache	FunApp	Equivalence	False	Passed	Model Under Test Equivalent Model
bdcfbe873a6b33b01a450cc0c391a4c14f353ec4	Apalache	FunApp	StringEmpty	True	Passed	Model Under Test Equivalent Model
e411e9cc8bfc04f835564bf3ad0b66a2a9f54318	Apalache	FunApp	StringEmpty	False	Passed	Model Under Test Equivalent Model
881b35a78b1e431ce2456417b71b8257ce0a96ed	Apalache	FunApp	String	True	Passed	Model Under Test Equivalent Model
41db0a2a80494f925128440fd2f6aeeaf9d6fe3a	Apalache	FunApp	String	False	Passed	Model Under Test Equivalent Model
83d789a6ec0a2a37f2c2db34d01288bb1a20a283	Apalache	FunApp	SeqLen	True	Passed	Model Under Test Equivalent Model
fde6032c852dbcec04a04c8362a64785817145bb	Apalache	FunApp	SeqLen	False	Passed	Model Under Test Equivalent Model
efab1f87ff3037f32b12688918c72c1b26663db7	Apalache	FunApp	SeqConcat	True	Passed	Model Under Test Equivalent Model
b04ed020ebc93141a5f5d3ea96d9f64ad413ddb9	Apalache	FunApp	SeqConcat	False	Passed	Model Under Test Equivalent Model
5b1c24f643cd7c8adb5efb999276e12386d5d2fb	Apalache	FunApp	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
dddaca85247635af0faa78b6aade46c8d676271d	Apalache	FunApp	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
4c5e69b49cca62f0d3074f5c71a5606d8fb2d40a	Apalache	FunApp	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
92b9e627c2f3a5e82b9664862cc941738b8fecc0	Apalache	FunApp	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
795be87bf2c4193f0a05a080f8ce948f967efa89	TLC with reduction strategy: Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	FunApp	NumRange	True	Passed	Model Under Test Equivalent Model
e27e66293b188931f9aef7dd6adcd77e1c220ff3	TLC with reduction strategy: Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review	FunApp	NumRange	False	Passed	Model Under Test Equivalent Model
f1f7bbc2f380a37151da9d348fa70f5cd5b38659	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	FunApp	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
ac05c8155eb067947e1269fff3855e235a324b1c	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	FunApp	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
34934d8a30cd0a146df158815efe6014d80e6eb8	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]]	FunApp	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
a2963d158b541f4bb8686856735d5f7bd1749800	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]]	FunApp	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
cd0d073f58b81857bc1116e347c96106f97a079b	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	FunApp	TlcPermuteFun	True	Passed	Model Under Test Equivalent Model
206c61b3dc093d0feab5ebcdd84366128a910ed0	TLC with reduction strategy: Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }	FunApp	TlcPermuteFun	False	Passed	Model Under Test Equivalent Model
8b2ae66b435303ddc9faf7de7a77edc5530c3cca	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	FunApp	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
88035c1886dbd865465f2e9a9d10cd7984e24a2f	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	FunApp	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
260adfcc9650e8ef1c3809f8a0e63e6352fd67a5	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	FunApp	TlcEval	True	Passed	Model Under Test Equivalent Model
c1f5580c0bb13fead2b5d70e8573c90ee6b48c92	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	FunApp	TlcEval	False	Passed	Model Under Test Equivalent Model
344c5a9a8c4fed087a97a7dfe0e55c904b2422ef	Apalache	FunApp	BagBagToSet	True	Passed	Model Under Test Equivalent Model
61fbbac5bb17f7aa4af1d0cbccbded4c21abc5d0	Apalache	FunApp	BagBagToSet	False	Passed	Model Under Test Equivalent Model
88e5618ecc6d1927e489cf37cddc8b6cf6850999	Apalache	FunApp	BagSetToBag	True	Passed	Model Under Test Equivalent Model
19c51baccf3c086aaa7700cfc169a2c15a0ab4a5	Apalache	FunApp	BagSetToBag	False	Passed	Model Under Test Equivalent Model
699ee502e45f1a6e35e05483551294b68b2a223b	Apalache	FunApp	BagBagIn	True	Passed	Model Under Test Equivalent Model
6a95b91aa7431a0f337043289d53e0f345beeecf	Apalache	FunApp	BagBagIn	False	Passed	Model Under Test Equivalent Model
2a570ec35ac67ff5dd2611dff94aeba19a6bb22e	Apalache	FunApp	BagEmptyBag	True	Passed	Model Under Test Equivalent Model
f5b56953796e48405f1e3a63c8828d6f980e241d	Apalache	FunApp	BagEmptyBag	False	Passed	Model Under Test Equivalent Model
f0d24236e85213de58209150c9a2b7026054b067	Apalache	FunApp	BagAddBag	True	Passed	Model Under Test Equivalent Model
4647a19da70966815dfab16ae201b783b4e5edfb	Apalache	FunApp	BagAddBag	False	Passed	Model Under Test Equivalent Model
d8bb01b3668b9895b1294825bd7e2fcaefac2711	Apalache	FunApp	BagBagSub	True	Passed	Model Under Test Equivalent Model
3bedc09291e31f10e797079aecd130a413c9130b	Apalache	FunApp	BagBagSub	False	Passed	Model Under Test Equivalent Model
1b06560ffe26f6cdf10c2b31451ec9d0cf474e0f	Apalache	FunApp	BagCopiesIn	True	Passed	Model Under Test Equivalent Model
8a29f3886efafa76d70822293f32964f07b2eb4f	Apalache	FunApp	BagCopiesIn	False	Passed	Model Under Test Equivalent Model
488081a59be9fc7b93a6fa6195a484d566a13b57	Apalache	FunApp	BagSubsetEqBag	True	Passed	Model Under Test Equivalent Model
66da7f7ba0597768378bd1c90053a451808494bb	Apalache	FunApp	BagSubsetEqBag	False	Passed	Model Under Test Equivalent Model
cd5a8e7ffeec96d776f655037b92b23f63e60947	Apalache	FunApp	BagBagUnion	True	Passed	Model Under Test Equivalent Model
3ee83fd3e25d12a1812837579e8a59720843e2c5	Apalache	FunApp	BagBagUnion	False	Passed	Model Under Test Equivalent Model
5b4da5bef082c27e97fb078d516873e7925563d7	Apalache	FunApp	BagBagCardinality	True	Passed	Model Under Test Equivalent Model
01f1ea86fd7813ffcda2d8bf6acdfdd40a58730c	Apalache	FunApp	BagBagCardinality	False	Passed	Model Under Test Equivalent Model
3068142bba536c7e26b09d4598ae91ccc1484b78	Apalache	FunApp	BagBagOfAll	True	Passed	Model Under Test Equivalent Model
b85505941a6ce3a98933ec70e6f4bc4db4f9317c	Apalache	FunApp	BagBagOfAll	False	Passed	Model Under Test Equivalent Model
ab01c1f181c69f89474f5a245b2d96ea483c6068	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	FunApp	BagSubBag	True	Passed	Model Under Test Equivalent Model
910858b5d8025b70aa8d3f253b458a9705c87b2a	TLC with reduction strategy: Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation	FunApp	BagSubBag	False	Passed	Model Under Test Equivalent Model
b44f74e1a4ec97d9578d3383e6a19faa98d09062	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)	FunApp	FiniteSetsIsFiniteSet	True	Passed	Model Under Test Equivalent Model
c8ec5e0dba0090f97ce99ffd588fa5d884fa9b73	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)	FunApp	FiniteSetsIsFiniteSet	False	Passed	Model Under Test Equivalent Model
b4c0103993b7a355e2150341ee35010bd9ad2cc1	Apalache	FunApp	FiniteSetsCardinality	True	Passed	Model Under Test Equivalent Model
0002b9f40c1d7a99d8acf4fa458600d50938534c	Apalache	FunApp	FiniteSetsCardinality	False	Passed	Model Under Test Equivalent Model
1e2580effe2b7f7d9945f333b2b272b64b1aaed1	Apalache	FunApp	SeqHead	True	Passed	Model Under Test Equivalent Model
3dbdb3eea2156ff1b04e720a68be6b2c41e43da9	Apalache	FunApp	SeqHead	False	Passed	Model Under Test Equivalent Model
b180a5b4624bd8aea0a581e8da5e3aacda085a61	Apalache	FunApp	SeqTail	True	Failed: SeqTail produces empty sequence and TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
b340fe3b08248a58461c6d0e26d654c6462d3059	Apalache	FunApp	SeqTail	False	Failed: SeqTail produces empty sequence and TLC reports an error if there is an attempt to apply a function with value not from its domain. Apalache is unable to detect such situation and returns arbitrary value.	Model Under Test Equivalent Model
e5cac48fc5250c540ed8ec191837737ce2b60909	Apalache	FunApp	SeqAppend	True	Passed	Model Under Test Equivalent Model
2e272c2bc44d6ce9aa008e09572cfeb30deacf15	Apalache	FunApp	SeqAppend	False	Passed	Model Under Test Equivalent Model

Index

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