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

Id	Type	Case Feature	Plug Feature	Check Deadlock	Test Results	Test Models
af41682ebf577ba8fd4dd0e68cde6e4bf301d694	Apalache	Except0	Let	True	Passed	Model Under Test Equivalent Model
043c0823202ce3fcc30d7c0e05f2ff16491e49f9	Apalache	Except0	Let	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
08cc473b80be7530a5fe24edfd0b9b979df2bbcd	Apalache	Except0	Choose	True	Passed	Model Under Test Equivalent Model
9bfa0fdf97b1d29409c70e7e4d541180059ac141	Apalache	Except0	Choose	False	Passed	Model Under Test Equivalent Model
6d14c43cbb99c3700fa16988875cabaa3f76e642	Apalache	Except0	Record	True	Passed	Model Under Test Equivalent Model
bc7f19984a2b98205edf1cdc7cc696f1efc0086b	Apalache	Except0	Record	False	Passed	Model Under Test Equivalent Model
85106667401a5a3b66632141fe39fceb70fd130d	Apalache	Except0	Tuple	True	Passed	Model Under Test Equivalent Model
6eb5763fdcce9e695432da3f315d5e404ddb85ad	Apalache	Except0	Tuple	False	Passed	Model Under Test Equivalent Model
1b80418d75c0f0644d7909116df20d2ce863a964	Apalache	Except0	TupleEmpty	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
ea53af8dd5d5e1b94168ffe2b33a00e5becc32a0	Apalache	Except0	TupleEmpty	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
86fe0ed35a238c5bfbf25555ffee23ba61b41614	Apalache	Except0	FunApp	True	Passed	Model Under Test Equivalent Model
edca9210011f2eabc4038615724698115b515db4	Apalache	Except0	FunApp	False	Passed	Model Under Test Equivalent Model
1f3461ba36d17c925343c566828f1eb2ca63d961	Apalache	Except0	Prime	True	Passed	Model Under Test Equivalent Model
54785af79d1e84b281bd23dc876d1c01f0bf09c8	Apalache	Except0	Prime	False	Passed	Model Under Test Equivalent Model
48cc251ea541814471a163c7cb8f3bc77c07d438	Apalache	Except0	DefFun	True	Passed	Model Under Test Equivalent Model
869fe856886620a59fb4bc3183c7ec18aeed6ed4	Apalache	Except0	DefFun	False	Passed	Model Under Test Equivalent Model
8829d3b91252f582d294c0e878707ae3f70a4f2a	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDefFun	True	Passed	Model Under Test Equivalent Model
c17c3e884a9619cbc4665c64cd2ac228e381ecf0	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDefFun	False	Passed	Model Under Test Equivalent Model
aa5392bc0869e89bde5088be9e82ae04069e3c73	Apalache	Except0	DefFunRecursive	True	Failed: TLC result is correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. Moreover, in this case, Apalache produces result, which violates TLA+ CHOOSE semantics	Model Under Test Equivalent Model
fd438e654d87e6c621db9cc8ef25d6b1e6c7a8d1	Apalache	Except0	DefFunRecursive	False	Failed: TLC result is correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. Moreover, in this case, Apalache produces result, which violates TLA+ CHOOSE semantics	Model Under Test Equivalent Model
e21b752ce8f0039e9b01c3b0164bdd7f19876914	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDefFunRecursive	True	Passed	Model Under Test Equivalent Model
e58a259b02d279cb9d96e9ac96f270e066705d68	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDefFunRecursive	False	Passed	Model Under Test Equivalent Model
2b619cdc86b110502af010e07236edb1067cd515	Apalache	Except0	Def0	True	Passed	Model Under Test Equivalent Model
731022db13ae16c5477916a54511f8ec547b0f64	Apalache	Except0	Def0	False	Passed	Model Under Test Equivalent Model
158f85b7278fa76eedb6c7e08d9bb6cf2839cb88	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef0	True	Passed	Model Under Test Equivalent Model
89265aa11d8fd6432d29cd3c8bd50af6165302e9	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef0	False	Passed	Model Under Test Equivalent Model
b7cea052623ee1c0876f28c6bdde18c912e6a198	Apalache	Except0	Def1	True	Passed	Model Under Test Equivalent Model
6de6590ed819ecd4ca0c5bfb0e02014290d7bd4c	Apalache	Except0	Def1	False	Passed	Model Under Test Equivalent Model
e0292360d4963cb696f053973d547bf59a07faae	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef1	True	Passed	Model Under Test Equivalent Model
7adf5a99dcad19d01465ff3e55ecf9d4386d2d7d	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef1	False	Passed	Model Under Test Equivalent Model
06f837501c9227f0c648381e9c5f8c4d7af0aa95	Apalache	Except0	Def2	True	Passed	Model Under Test Equivalent Model
ad5a41ae7698c30f5b3acc2767e628dac9311d60	Apalache	Except0	Def2	False	Passed	Model Under Test Equivalent Model
088868779c87bcc01f7568560593d6a703b680f1	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef2	True	Passed	Model Under Test Equivalent Model
ac57aff7c8c53e12d1c5457338bed7f19afae921	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef2	False	Passed	Model Under Test Equivalent Model
3a9625ed3b88c1ad9799c49b149c627218da719a	Apalache	Except0	Def1Recursive	True	Passed	Model Under Test Equivalent Model
ca9bed1dcb44753f2ba9e40efcfd65ebb3cae658	Apalache	Except0	Def1Recursive	False	Passed	Model Under Test Equivalent Model
fbc6f512b0f5e4faeb428728a2b28a8b6a5f09e6	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef1Recursive	True	Passed	Model Under Test Equivalent Model
701e77b46d4abef0e65114a70148d6e99b4570bc	TLC with reduction strategy: Plug Feature: LET definitions are reduced to global definitions	Except0	LetDef1Recursive	False	Passed	Model Under Test Equivalent Model
7b222313bff3c3bdb4d2a61130f16991e4b475bb	Apalache	Except0	Extends	True	Passed	Model Under Test Equivalent Model
1a6f85747bd6ec7f52bf86789154d5d947ba0522	Apalache	Except0	Extends	False	Passed	Model Under Test Equivalent Model
f48a4a660318a4da5e00b1666873714f595df495	Apalache	Except0	ExtendsInDifferentFolder	True	Passed	Model Under Test Equivalent Model
c1d84275c740998f4cac39a714e3a5f821382b21	Apalache	Except0	ExtendsInDifferentFolder	False	Passed	Model Under Test Equivalent Model
baa3df4b7aa6e5ada0f3c2315efecd46df4a701b	Apalache	Except0	Variable	True	Passed	Model Under Test Equivalent Model
482c8cd86c9ee11c44c24f33266d59b72471ac05	Apalache	Except0	Variable	False	Passed	Model Under Test Equivalent Model
cd19bae2b8f597702e4fc04cff55f97e29774e58	Apalache	Except0	Constant	True	Passed	Model Under Test Equivalent Model
b2d94019fa4044624126734261bd171726ec46be	Apalache	Except0	Constant	False	Passed	Model Under Test Equivalent Model
c4c245352cfc7dba33845b5e8ac60928998ac8d8	Apalache	Except0	ConstantRank1	True	Passed	Model Under Test Equivalent Model
ca39a25d008f217453ba0239b8e571284d4d6bbd	Apalache	Except0	ConstantRank1	False	Passed	Model Under Test Equivalent Model
01cb6eb6502233b15282efe11abe05577deec2d4	Apalache	Except0	Instance	True	Passed	Model Under Test Equivalent Model
e82a1794c8c58652d736bc56f226cebe52132161	Apalache	Except0	Instance	False	Passed	Model Under Test Equivalent Model
b31f45199881f461f9caea78969dd843968ce286	Apalache	Except0	InstanceWith	True	Passed	Model Under Test Equivalent Model
bb717d0e72558439e291bf84f5ad30d1b972b260	Apalache	Except0	InstanceWith	False	Passed	Model Under Test Equivalent Model
930ff86231c5a48cd5097361ce482072625ffea4	Apalache	Except0	InstanceNamed	True	Passed	Model Under Test Equivalent Model
6022cfa4c415cb61f86f14c746e2d2bfab311360	Apalache	Except0	InstanceNamed	False	Passed	Model Under Test Equivalent Model
8bd4dd1ee6f024f7d000a76f95fbeb325934a193	Apalache	Except0	InstanceNamedWith	True	Passed	Model Under Test Equivalent Model
e711ba7d41b60f3596622f14b936b4f6532d3763	Apalache	Except0	InstanceNamedWith	False	Passed	Model Under Test Equivalent Model
6fdb02e94cf17f356bd58e94ebc85df49b7c58f3	Apalache	Except0	InstanceInFolder	True	Passed	Model Under Test Equivalent Model
37e1d9597d931f8edb80a679db31693371b6d175	Apalache	Except0	InstanceInFolder	False	Passed	Model Under Test Equivalent Model
734bc806926ca9766c4f0c8452a7a1f3e0dddb38	Apalache	Except0	InstanceWithInFolder	True	Passed	Model Under Test Equivalent Model
eef5213ac414e9fe85aacb86b28355df69aa5fe3	Apalache	Except0	InstanceWithInFolder	False	Passed	Model Under Test Equivalent Model
8c1cbe16603124f885d52c2342d1031fe74ccc64	Apalache	Except0	InstanceNamedInFolder	True	Passed	Model Under Test Equivalent Model
b6f693cc45cf4144ebd72498d78a730e0cd69878	Apalache	Except0	InstanceNamedInFolder	False	Passed	Model Under Test Equivalent Model
a90ebc4b05d6400a56280fac4411f8b83d4c5626	Apalache	Except0	InstanceNamedWithInFolder	True	Passed	Model Under Test Equivalent Model
a8176914d7c8fe3b23aaa43d979bc11f63969f36	Apalache	Except0	InstanceNamedWithInFolder	False	Passed	Model Under Test Equivalent Model
708cf034e05d6e4d690f0391a029716adafe19fe	Apalache	Except0	IfCond	True	Passed	Model Under Test Equivalent Model
fce4e78ea18a361ea4a592980da932400e8299ce	Apalache	Except0	IfCond	False	Passed	Model Under Test Equivalent Model
847edacf73724f48511d8918e8a696281c250b25	Apalache	Except0	IfThen	True	Passed	Model Under Test Equivalent Model
93b1561b2c6cba2bb659f2f88465bd7066a25a79	Apalache	Except0	IfThen	False	Passed	Model Under Test Equivalent Model
c961f126d86ccc27d06a9420dc2adf01ae8a6185	Apalache	Except0	IfElse	True	Passed	Model Under Test Equivalent Model
b870ce88c47fdd7aaf98593e91ee44c3faa051e9	Apalache	Except0	IfElse	False	Passed	Model Under Test Equivalent Model
1388c118def13e467811caae1e2c5aa49f9d1e13	Apalache	Except0	SeqConcat	True	Failed: Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, SeqConcat function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
9d9e6f88b9f6d5ce7ea072d881d513f0f97ccb57	Apalache	Except0	SeqConcat	False	Failed: Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, SeqConcat function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
b442dd12a710bd97d202a80ba096b922714e3c54	Apalache	Except0	SeqSelectSeq	True	Passed	Model Under Test Equivalent Model
cd006e55d4cb3f2c85f57d649eb9280bfc3fa397	Apalache	Except0	SeqSelectSeq	False	Passed	Model Under Test Equivalent Model
c852c72f3645a4d5615c7576bb7760768a383526	Apalache	Except0	SeqSubSeq	True	Passed	Model Under Test Equivalent Model
d5350c526969170449d35c56dffef03543b72186	Apalache	Except0	SeqSubSeq	False	Passed	Model Under Test Equivalent Model
27ad1b6e861e46270be8ed2d65d207d49235b7fa	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except0	TlcSingletonFun	True	Passed	Model Under Test Equivalent Model
7f0b7fdbfc251d120770059797b568538df166ff	TLC with reduction strategy: Plug Feature: x :> y is replaced with equivalent [u \in {x} \|-> y]	Except0	TlcSingletonFun	False	Passed	Model Under Test Equivalent Model
2989e5c4db8446011d726ddcfd1b1dbd0713ca30	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]]	Except0	TlcExtendFun	True	Passed	Model Under Test Equivalent Model
f8be92adde07f25689097b299aeb6e5248c541bb	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]]	Except0	TlcExtendFun	False	Passed	Model Under Test Equivalent Model
8a727f4db0a30a6e675743dd9022a4944a3c3158	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except0	TlcSortSeq	True	Passed	Model Under Test Equivalent Model
8f815350d2e76fdaffdf292fcb8c71de9b8d6779	TLC with reduction strategy: Plug Feature: SortSeq(S) is reduced to equivalent sort implementation	Except0	TlcSortSeq	False	Passed	Model Under Test Equivalent Model
52a3f252560d673d985e50a8572204e9a02834a8	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except0	TlcEval	True	Passed	Model Under Test Equivalent Model
076fe602c19d770d6b7b47fa13a2bc79d1d59801	TLC with reduction strategy: Plug Feature: TLCEval(expr) is reduced to just expr	Except0	TlcEval	False	Passed	Model Under Test Equivalent Model
343b1f3370aeb1b321256fe34ac84dc471355a11	Apalache	Except0	SeqHead	True	Passed	Model Under Test Equivalent Model
2b28b5a1686ba56e3a5dc317bc94c3dad53ae950	Apalache	Except0	SeqHead	False	Passed	Model Under Test Equivalent Model
e12db5064497d0de3d9b20ce5bd6ff71169cd11b	Apalache	Except0	SeqTail	True	Failed: Except0 uses CHOOSE to select an argument. 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
8a70e1ffbdd262912cbcd8e82292579147ec57a7	Apalache	Except0	SeqTail	False	Failed: Except0 uses CHOOSE to select an argument. 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
cdb1ba69f63bc435b34e165b27031eac3bbd21eb	Apalache	Except0	SeqAppend	True	Failed: Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, Append function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model
6b0fa28307d11363d42c7c9bcc0c47f188897158	Apalache	Except0	SeqAppend	False	Failed: Both results are correct. The reason they are different is CHOOSE operator, which is allowed to return different values for TLC and Apalache if applied to a set with more than one element. In this case, Append function from Sequences standard module is used to add one more element into non empty sequence	Model Under Test Equivalent Model

Index

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