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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
72de2bde056cb070c7a21970143538deeddc43b5	Apalache	Eq	Fun	True	Passed	Model Under Test Equivalent Model
e76e8a3e8c69568ed8111c82e921fe4b4820fdfe	Apalache	Eq	Fun	False	Passed	Model Under Test Equivalent Model
77d35058e256d3e856b2d4ed9cfeb38a260a1976	Apalache	Ne	Fun	True	Passed	Model Under Test Equivalent Model
520569c45e2fa865eb07fd484140954db87896eb	Apalache	Ne	Fun	False	Passed	Model Under Test Equivalent Model
2e7fed07380564b1444046b8b28430de4b73ea80	Apalache	Let	Fun	True	Passed	Model Under Test Equivalent Model
907f7569697850a7b34ec996ec71e6243866f5ad	Apalache	Let	Fun	False	Passed	Model Under Test Equivalent Model
dd6101838d1e5d1c6fb8100bf5baa5ac3ef7a7ad	Apalache	Set0	Fun	True	Passed	Model Under Test Equivalent Model
95d295ffd651922c26a1ee7d81366afd48425819	Apalache	Set0	Fun	False	Passed	Model Under Test Equivalent Model
068a5bf745f5643234bc23c1cb114b87ec7c5215	Apalache	Set1	Fun	True	Passed	Model Under Test Equivalent Model
953cf800e333872994499560b64db4f29a77b56a	Apalache	Set1	Fun	False	Passed	Model Under Test Equivalent Model
471c3474904f97a59f9a7fc23a4d3d3c0694fbb7	Apalache	Set2	Fun	True	Passed	Model Under Test Equivalent Model
ca5247593b533e0b75bc27692922ed845e20046d	Apalache	Set2	Fun	False	Passed	Model Under Test Equivalent Model
84f42b52b795966a7fe13a1107d581dc280f5c92	Apalache	Fun	Fun	True	Passed	Model Under Test Equivalent Model
c384cec2ecefc7cc52da11182be142fe5bf27f13	Apalache	Fun	Fun	False	Passed	Model Under Test Equivalent Model
7c531193f77250f261767de9cfd715dcc639e373	Apalache	In	Fun	True	Passed	Model Under Test Equivalent Model
f6efff75a8c07b7b876eb94f01fd9f9d616d1201	Apalache	In	Fun	False	Passed	Model Under Test Equivalent Model
a008c7ded082d08c89a5bf3f592d8ab304824ec7	Apalache	NotIn	Fun	True	Passed	Model Under Test Equivalent Model
ba843e08d4f1d5f32e7d3f6487476854bc9b396a	Apalache	NotIn	Fun	False	Passed	Model Under Test Equivalent Model
9e56f0ad389b7c4b68e2cc6d40fe0b14bd0b3632	Apalache	Record	Fun	True	Passed	Model Under Test Equivalent Model
40aaee352319893e83a2585849bc66ac34a2ac0c	Apalache	Record	Fun	False	Passed	Model Under Test Equivalent Model
9667ab6bef041f381f420746e498324129347d65	Apalache	Tuple	Fun	True	Passed	Model Under Test Equivalent Model
ad1a4a6496a70c9d978f097a5e816addaa55020f	Apalache	Tuple	Fun	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
0564fdbc7f1598a7d08335be67a8e3053dfd9ae8	Apalache	Except0	Fun	True	Passed	Model Under Test Equivalent Model
c6aaf1c408e65d7ea19cd93aeed43d187c95ee5d	Apalache	Except0	Fun	False	Passed	Model Under Test Equivalent Model
e322b7df9f2f8fe24bf5ee60f1268df1b31fad5d	Apalache	Except1Fun	Fun	True	Passed	Model Under Test Equivalent Model
32d41e363f590102915d92475f04d489eceea742	Apalache	Except1Fun	Fun	False	Passed	Model Under Test Equivalent Model
d37fcbd8cad887ff2f6deb46c3dae16b7df19df8	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Fun	True	Passed	Model Under Test Equivalent Model
b28ea4437874039706370d76d09571c41d0a4b65	TLC with reduction strategy: Case Feature: @ is reduced to F[arg]	Except1FunWithAt	Fun	False	Passed	Model Under Test Equivalent Model
d0123ebad18988b0055d211babd8fcfa77ae48a5	Apalache	Except1Rec	Fun	True	Passed	Model Under Test Equivalent Model
9046f27dca006771f1eb58ad348ce82350224ab3	Apalache	Except1Rec	Fun	False	Passed	Model Under Test Equivalent Model
db1ec0aaed3e8a3a63cd61d24159dcb22137132c	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Fun	True	Passed	Model Under Test Equivalent Model
408aa902977b99c0df9287a9f60abb2948af7885	TLC with reduction strategy: Case Feature: @ is reduced to F.arg	Except1RecWithAt	Fun	False	Passed	Model Under Test Equivalent Model
96c2043aef17277ee4f03115d0f2952511e9a8f8	Apalache	Except2Fun	Fun	True	Passed	Model Under Test Equivalent Model
117db562640098399b193cb22c9f5078bdcc238b	Apalache	Except2Fun	Fun	False	Passed	Model Under Test Equivalent Model
7f13979c3f4105d400c4b73f15c4375421d17d7a	Apalache	Prime	Fun	True	Passed	Model Under Test Equivalent Model
b7f19a14a6842d9585a06edcd96deb8248e2291d	Apalache	Prime	Fun	False	Passed	Model Under Test Equivalent Model
5476f1cbbf90cbd079f862859d3bd7849eaddfb6	Apalache	DefFun	Fun	True	Passed	Model Under Test Equivalent Model
585cfd3726ffa19ef188e4329c5a672c925220b2	Apalache	DefFun	Fun	False	Passed	Model Under Test Equivalent Model
a5f196f8fd60029ef30f313fd323973c8ba9ca0e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Fun	True	Passed	Model Under Test Equivalent Model
227fab258e673224cc7e6b7b02b05a3abf5786c1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFun	Fun	False	Passed	Model Under Test Equivalent Model
92de4c69c8bb4f10fbdbab32e76d446e7180452e	Apalache	DefFunRecursive	Fun	True	Passed	Model Under Test Equivalent Model
4ac741d6b56ec2167bf34cd5fc6f7562b3d8697c	Apalache	DefFunRecursive	Fun	False	Passed	Model Under Test Equivalent Model
d8f69589e0865c6c0dc020c9afde745a3b06346e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Fun	True	Passed	Model Under Test Equivalent Model
9bbb960bc531357601c4679c5741c2a5507f4b04	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDefFunRecursive	Fun	False	Passed	Model Under Test Equivalent Model
28bb6b493fa84a384eec6fbc71b8951be288e56c	Apalache	Def0	Fun	True	Passed	Model Under Test Equivalent Model
f57863153ae99a272b20f4632e2414c6e3418d6c	Apalache	Def0	Fun	False	Passed	Model Under Test Equivalent Model
4be665db0f76de4d89309e52ffef51d063825ece	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Fun	True	Passed	Model Under Test Equivalent Model
e85d76370b4d4b16e618a00e4ab92030719ea538	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef0	Fun	False	Passed	Model Under Test Equivalent Model
a5b7b505753066060433563c4662ba92459413f1	Apalache	Def1	Fun	True	Passed	Model Under Test Equivalent Model
f2b032d7f36eea9b381df60c17cd71a6c8487c0f	Apalache	Def1	Fun	False	Passed	Model Under Test Equivalent Model
3b89fd242124155cb31c06881071f2fd88c151d5	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Fun	True	Passed	Model Under Test Equivalent Model
357b3c91ae17a4b51975ce69d4bde61b547e86a1	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1	Fun	False	Passed	Model Under Test Equivalent Model
6c676e2ec96cc21249b7f577e09cab1e4a18cf79	Apalache	Def2	Fun	True	Passed	Model Under Test Equivalent Model
81c769a82304e9d560a9267dcf7e35151f4c70ae	Apalache	Def2	Fun	False	Passed	Model Under Test Equivalent Model
e66f8a356f5eee48d9b88d0c5b931d8ceda055eb	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Fun	True	Passed	Model Under Test Equivalent Model
8c09a9e76366323ec02bc04d1b1f0355559d840e	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef2	Fun	False	Passed	Model Under Test Equivalent Model
f62e5863c0e3866cf4c503af86b61f72a18c6389	Apalache	Def1Recursive	Fun	True	Passed	Model Under Test Equivalent Model
881dfc2698485c4dc73b1090045ebf5281b8e08b	Apalache	Def1Recursive	Fun	False	Passed	Model Under Test Equivalent Model
4457b72f5ad648e8ee53df9ec43e74013cd6dfaa	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Fun	True	Passed	Model Under Test Equivalent Model
646e80a1d55dc2b0d8e138fb9ea54d469623e07b	TLC with reduction strategy: Case Feature: LET definitions are reduced to global definitions	LetDef1Recursive	Fun	False	Passed	Model Under Test Equivalent Model
5be6f9f3cf932cbec81ff17e0a26868d3dc11465	Apalache	Extends	Fun	True	Passed	Model Under Test Equivalent Model
1d99c917cff8e08467d85e1f9308aec4c35cabc3	Apalache	Extends	Fun	False	Passed	Model Under Test Equivalent Model
79b0e36326e478c68a8ee22a6699839586f187f5	Apalache	ExtendsInDifferentFolder	Fun	True	Passed	Model Under Test Equivalent Model
78d109de7398f6c5f72458b965f6b7456ba15cc6	Apalache	ExtendsInDifferentFolder	Fun	False	Passed	Model Under Test Equivalent Model
ff752ce9f33347d2bc843dc534051606a0f0ea72	Apalache	Variable	Fun	True	Passed	Model Under Test Equivalent Model
6a763449a6d224d7f64e29e9c3a5d5171fa860f7	Apalache	Variable	Fun	False	Passed	Model Under Test Equivalent Model
e158ab8de42c06f212bc0306b991d012bae71610	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Fun	True	Passed	Model Under Test Equivalent Model
231a8aab28aebc475ced9eef08d1827a3f819ebb	TLC with reduction strategy: Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior	VariableViewExclude	Fun	False	Passed	Model Under Test Equivalent Model
f5fe19425afdb9283d9b31718869f6fd618918cd	Apalache	Constant	Fun	True	Passed	Model Under Test Equivalent Model
ee457b185c60158e1676d34ff57b9acc6edd0042	Apalache	Constant	Fun	False	Passed	Model Under Test Equivalent Model
01a27a53f9569f5424031e1bc033532ee4a57241	Apalache	ConstantRank1	Fun	True	Passed	Model Under Test Equivalent Model
0bc53621141d0374c72daca0c3ed782e5030de92	Apalache	ConstantRank1	Fun	False	Passed	Model Under Test Equivalent Model
0a0c86ae435fbf0ef6ee95ec5024112a6c45f47d	Apalache	Instance	Fun	True	Passed	Model Under Test Equivalent Model
422a80899440b31f66770973e7b5b8402a006605	Apalache	Instance	Fun	False	Passed	Model Under Test Equivalent Model
1d4d2bb1492d3d70dfdf88e1de923aca1b802fab	Apalache	InstanceWith	Fun	True	Passed	Model Under Test Equivalent Model
2876befa54cba3863ce65782ee43489626479527	Apalache	InstanceWith	Fun	False	Passed	Model Under Test Equivalent Model
11034736cb5b1e02753933d8cf387cfeaa3886c7	Apalache	InstanceNamed	Fun	True	Passed	Model Under Test Equivalent Model
4859c58076710f7d6b2c033c02c47c06424a0058	Apalache	InstanceNamed	Fun	False	Passed	Model Under Test Equivalent Model
770f35e0cab390f9d961aeeebe830813265372e8	Apalache	InstanceNamedWith	Fun	True	Passed	Model Under Test Equivalent Model
d8fd86eece7e91559ccd572a5b9adadd18e1fc0e	Apalache	InstanceNamedWith	Fun	False	Passed	Model Under Test Equivalent Model
b43525574f31feffedc7ac6f4acb9184119caa4b	Apalache	InstanceInFolder	Fun	True	Passed	Model Under Test Equivalent Model
e80f0cdc255b90cfa31a4a914efb5d821d944124	Apalache	InstanceInFolder	Fun	False	Passed	Model Under Test Equivalent Model
ca5506103024406d16ff3d46b591aa60875b08da	Apalache	InstanceWithInFolder	Fun	True	Passed	Model Under Test Equivalent Model
7633d3af6ccaa50f6275a3fc9dfe74fc8b79ebe6	Apalache	InstanceWithInFolder	Fun	False	Passed	Model Under Test Equivalent Model
28e54ec6074a7b58cceb17eb99eedc87b65b6d88	Apalache	InstanceNamedInFolder	Fun	True	Passed	Model Under Test Equivalent Model
8f158f17c02aa37f33cb7fcd4d78bed35b5269d9	Apalache	InstanceNamedInFolder	Fun	False	Passed	Model Under Test Equivalent Model
73aba66052f77e3eebeb134cb85313b2f8390ce7	Apalache	InstanceNamedWithInFolder	Fun	True	Passed	Model Under Test Equivalent Model
d72e5959f6807aae54a62d22df8695e998f646e6	Apalache	InstanceNamedWithInFolder	Fun	False	Passed	Model Under Test Equivalent Model
bced6d61a750336a1bb1800ef7b9ff39b4a4eb3e	Apalache	Lambda	Fun	True	Passed	Model Under Test Equivalent Model
b20f547cd73d14029dd8a25497d15dc57b58bf0c	Apalache	Lambda	Fun	False	Passed	Model Under Test Equivalent Model
42c157a889a9f3db2908f1d614676892be666aa7	Apalache	IfThen	Fun	True	Passed	Model Under Test Equivalent Model
6c11ac0ca817acccb22d91893ad6e664fb3ce91d	Apalache	IfThen	Fun	False	Passed	Model Under Test Equivalent Model
e2260da99156650ab65c9854b22418663c5587ca	Apalache	IfElse	Fun	True	Passed	Model Under Test Equivalent Model
49555ca8d86eeca066c5ddf6721e44e491f6d776	Apalache	IfElse	Fun	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
88f4c1921665a28d318278e9c0fd395b5f32ef19	Apalache	Unchanged	Fun	True	Passed	Model Under Test Equivalent Model
36393cb1cc83a9a2addedf9e0975305ab0698bf7	Apalache	Unchanged	Fun	False	Passed	Model Under Test Equivalent Model
ebbfc5c961386d8477bb2e8653393c6b34a26c09	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Fun	True	Passed	Model Under Test Equivalent Model
41bccdcd7456b9aecf6272150a3b08ba7bb8b496	TLC with reduction strategy: Case Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	TlcSingletonFun	Fun	False	Passed	Model Under Test Equivalent Model
b4291bd8b1ede56125a02ae5850220b6c512ec23	TLC with reduction strategy: Case 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]]	TlcExtendFun	Fun	True	Passed	Model Under Test Equivalent Model
6f53eeb31c4af8a018040545beb931dff81d8f3f	TLC with reduction strategy: Case 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]]	TlcExtendFun	Fun	False	Passed	Model Under Test Equivalent Model
f87cf948e84b1e2da903f3c4caf115ad41efcd75	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Fun	True	Passed	Model Under Test Equivalent Model
1f94ca3ad7d61e0b46c73960b7441a7e1d821a11	TLC with reduction strategy: Case Feature: TLCEval(expr) is reduced to just expr	TlcEval	Fun	False	Passed	Model Under Test Equivalent Model
e7cfb5ab1b34ac2eb8d0d121366129f95b907848	Apalache	BagBagIn	Fun	True	Passed	Model Under Test Equivalent Model
8889435974bc14c0031643203913f6478644bafd	Apalache	BagBagIn	Fun	False	Passed	Model Under Test Equivalent Model
d160b61ef5542c04d281a122a7497ace9684b5b5	Apalache	BagCopiesIn	Fun	True	Passed	Model Under Test Equivalent Model
fc2dcfed35857d166ed5909733f9eb9e65440fce	Apalache	BagCopiesIn	Fun	False	Passed	Model Under Test Equivalent Model
eca5f88abba6e2ccc90eb2eff7f9d013afe572f3	Apalache	SeqAppend	Fun	True	Passed	Model Under Test Equivalent Model
9c9c20ef464ee62b845889b691c7a044e05b991d	Apalache	SeqAppend	Fun	False	Passed	Model Under Test Equivalent Model

Index

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