Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
94a52a27aac370548ed0b21a5789cb96ff459ba9 Apalache And Equivalence True Passed
0a71254a715433d2523852c2b1a491f49ad9a701 Apalache And Equivalence False Passed
d3c813fabd7097faa8e7f8c70ba54c044f0d6324 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Equivalence True Passed
dd6b933683a274a6b3981d548b02539e2d45dfd9 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Equivalence False Passed
e6a1aff8545cfab3e7e3f6fab341b37920f040a8 Apalache Imply Equivalence True Passed
86e8bdd3c527d922764ff1e0858935df29ff64b3 Apalache Imply Equivalence False Passed
5edc6a31c5ab2c32beb8c46861518087a74e94c6 Apalache Not Equivalence True Passed
54eaa65d8c5b1446ef8a10444e4f76562caf436b Apalache Not Equivalence False Passed
137b4065f6e3767f9670cb36e9f5acef8d8e5b86 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Equivalence True Passed
b5ea1ac67d70e89561a3a8e6c3ca269b89fb1b16 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Equivalence False Passed
b84f417edd0475071c63f4a71ee7950773fefd5f TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Equivalence True Passed
a4bcad62dfa55195b5aa6fa0dc1bcbe89d7eeca7 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Equivalence False Passed
424b7a3952ff96e18fde23e5d8ce025992d62cfd Apalache AndProp Equivalence True Passed
86e60331786db986bf6a2f43387b354566614115 Apalache AndProp Equivalence False Passed
dfa0b127d89373c12c5ac44f80bec467a6ba1d9c Apalache Boxed Equivalence True Passed
11218e5d82908d48d893c1b1fb3009029e1bfb23 Apalache Boxed Equivalence False Passed
97ba1e97f818a8b175dad45972c094488c3ba872 Apalache Eq Equivalence True Passed
e273b13dad17bed1aa5705707640126be4d8ceab Apalache Eq Equivalence False Passed
461c4d6c3903d0910a751d6aab3c023dd124f22d Apalache Ne Equivalence True Passed
a36aa00347bf387e3ad0ba0c61b07008e0dec6f2 Apalache Ne Equivalence False Passed
77f3ad6c299d6b891a724a1c95613da866fd27cd Apalache Let Equivalence True Passed
788e27c552c3c3fd03623686a08e83ca8a839e1c Apalache Let Equivalence False Passed
665fcd55daadaecf66dd2511ae59b2cb64648c99 Apalache Set0 Equivalence True Passed
c8662f3ddfddd82f4c34288e65e15157fc7fc45f Apalache Set0 Equivalence False Passed
c3f72d474d92e7ce4d387a40be57fddb201be7e6 Apalache Set1 Equivalence True Passed
e6936ed2d8123d152e462535486d0162041ab875 Apalache Set1 Equivalence False Passed
1b2d3be5e6c37dd8c2644849c6f81b93e2217bf2 Apalache Set2 Equivalence True Passed
ea060b7c375b49f92641623bc29e47f60fef3019 Apalache Set2 Equivalence False Passed
318a1da37bb8b400edea0de8d48f81c1e7453255 Apalache Fun Equivalence True Passed
29950990f26bc553269d9e2cc6ee35fa0baff61e Apalache Fun Equivalence False Passed
9a4f2c5ec0fe2bcf44f54c07bb303fbb5bdca5a9 Apalache In Equivalence True Passed
27c6cb08a99d2e4db9524b71590da38d275ec463 Apalache In Equivalence False Passed
e79923b0a4062622bedd2efd1e053f818459be5f Apalache NotIn Equivalence True Passed
c1b86044aa5fb8f9f8e3ef08c291299d01eeff66 Apalache NotIn Equivalence False Passed
c680a9cf2a7390c138d71a776011496986d9ccb2 Apalache Exists Equivalence True Passed
345141e00fa3e8e258678086771a009f691006b3 Apalache Exists Equivalence False Passed
669946725e7165580e738252068394f5cfa50d73 Apalache Forall Equivalence True Passed
71ee72546d51f743faf0cb805ba352cd00fe0dc4 Apalache Forall Equivalence False Passed
6c65754b60c324fac1386bc062d7a257290df344 Apalache Choose Equivalence 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.
9580c4c94498621cae1061cf1b62dbd20530e314 Apalache Choose Equivalence 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.
5a5f408c0923470bb66b5a2402ad8c62fb0ca45a Apalache Record Equivalence True Passed
b9ef92711e61f97c403fdd0f69c8301b889ba255 Apalache Record Equivalence False Passed
59f4124d3f83f791b68a76168266bbef58877845 Apalache Tuple Equivalence True Passed
03d6ec41cca99ac11812e297ffe0739943f08085 Apalache Tuple Equivalence False Passed
5f85a14a36c7aa8a193027362e4fdf5c6275448a Apalache FunApp Equivalence True Passed
38d8eab84ea70c0176b477ecfb52ec79ef39e80c Apalache FunApp Equivalence False Passed
e9488527d2565c20919aa817253e705e57eb69ce Apalache Except1Fun Equivalence True Passed
78fc1df0f22062fd99086f72ee53dcb803aa753d Apalache Except1Fun Equivalence False Passed
7535840cbc629a5fe96ce8e0db064b0374c3153e TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Equivalence True Passed
2548ae84bad6f6562bd746362095c7f9a43c7924 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Equivalence False Passed
f89097d284804118ba5e8dbe6606c20df59c4472 Apalache Except1Rec Equivalence True Passed
9e8625ab105098fe676fbf22723c3851823a2005 Apalache Except1Rec Equivalence False Passed
33a5b68db3940fde58fbfa76228e5160b3f5e901 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Equivalence True Passed
964e8190235de416aa08d8f5f6eb1e4aadd67b9f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Equivalence False Passed
d4623085e9cb8d3de69e9aa355999be1b6026411 Apalache Except2Fun Equivalence True Passed
bf52fbbb97a70c30b187e7d19ddb23cf35ff4ffc Apalache Except2Fun Equivalence False Passed
765d528889dbc769940095fa1e786fb97e8df016 Apalache Prime Equivalence True Passed
be47085c344587f4cfc27cf8eed9ef8316ea1470 Apalache Prime Equivalence False Passed
ac2cfba44260060722cc9330f938043c761a9760 Apalache DefFun Equivalence True Passed
90dc83808ed02c75042dbdb0b366d1f49436b5c5 Apalache DefFun Equivalence False Passed
7422eb62cfff19829b5c8116dcf22f48a656d3d3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Equivalence True Passed
b73abdac1fbbca67c8e77e8f62412f754ce1de2a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Equivalence False Passed
4cd4843a8d908e55931bdbef5dc692f0ed23aef6 Apalache DefFunRecursive Equivalence True Passed
19182e8a3dac8c69de1992ee4e19f621666913ef Apalache DefFunRecursive Equivalence False Passed
e582103006f9e9d7ab642902bf8d1b5f2aa83291 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Equivalence True Passed
5f7091de24c9076d29df55f3021e23e443e9e759 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Equivalence False Passed
c32454af3cb22f9f0f22e6bfba48e256b7802e51 Apalache Def0 Equivalence True Passed
ede88663ef16b722cc6030fac97a0e4717a9fa88 Apalache Def0 Equivalence False Passed
7c189626fa78da584e5a72d031073aa3a258d3a5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Equivalence True Passed
acc0404dcae61cca816824fbb47dde815f8872da TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Equivalence False Passed
b4938e4d7d38442fe7f295f26cdc6009df687e0b Apalache Def1 Equivalence True Passed
19c40587b5c30e8e67ac2a8f346665bb6f109f11 Apalache Def1 Equivalence False Passed
984f406c0f713d7c343ebea8875070f197d39dfb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Equivalence True Passed
06e7c75dc450d1d5e285fef8fa650727cd76e905 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Equivalence False Passed
e9e0dad6062c57ceed970aa1d75dc3cc0e685db9 Apalache Def2 Equivalence True Passed
05f464b5c8e365ce8fc370c92ad3df7b769707e9 Apalache Def2 Equivalence False Passed
2350f2cdb5214e8db9cd5e8f54940be617b289c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Equivalence True Passed
b283bef96ddfd6192dfede6532708f916155ba18 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Equivalence False Passed
f3510acd94a463ff0af76c9cd00c8f877c33ab1e Apalache Def1Recursive Equivalence True Passed
9eb5c1f78288b77c4e3e86cbafa574769189aab4 Apalache Def1Recursive Equivalence False Passed
2d3f5c7dbcd0305b978ad717cd54d492cc160ded TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Equivalence True Passed
bf39d7ced6b4b262e7aacf02255c59eade9de420 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Equivalence False Passed
ad62ea61f2b7e73a7186df2688e2de4a280bf5c4 Apalache Extends Equivalence True Passed
dab843f18af465dcd34abfbcac5adeead85b320a Apalache Extends Equivalence False Passed
758bdfa648e0ada1258024fc5aaec6e7855785b0 Apalache ExtendsInDifferentFolder Equivalence True Passed
0c34f18748010a49fe5798c57c3764cb152bc1f3 Apalache ExtendsInDifferentFolder Equivalence False Passed
de053681a61daed488b06cdec04cd9f3b654a115 Apalache Variable Equivalence True Passed
6147dcdabbe3c9643cf706bae765201b8adcb532 Apalache Variable Equivalence False Passed
f4164cde51d583217e27aab83ad87255df036fd2 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Equivalence True Passed
685daf01d34ffcdd8f6fb0a220d4b7b66dc13e1f TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Equivalence False Passed
c7cd4b28c0098f65f12ebd1c0fd5d1a96909ab75 Apalache Constant Equivalence True Passed
8ff753205d8fdcfe24efbd25ee58f09d6d0b25a6 Apalache Constant Equivalence False Passed
c4313981955be6d7d3921175e996cf465dd7721c Apalache ConstantRank1 Equivalence True Passed
d0956c54d49213ddbe00970bff9ffcd3659ff069 Apalache ConstantRank1 Equivalence False Passed
72ad127fe94b8937a1b096712d290831d5650edc Apalache Instance Equivalence True Passed
c3ac457425e32a2e537ef3d65b02fe7c2867d48b Apalache Instance Equivalence False Passed
00e62949e77ab5841c1b768a718bf39eb1702d23 Apalache InstanceWith Equivalence True Passed
76cc17d02600a0228d8fefcf135b7d52a1572573 Apalache InstanceWith Equivalence False Passed
295071f295a6dc6387572d316cdaa35e02bb2bfa Apalache InstanceNamed Equivalence True Passed
096e5827d590c2546f66a5c285d03f0216273829 Apalache InstanceNamed Equivalence False Passed
65f51ec134e90cde23a9ca0133c7f3f14e7e3fb9 Apalache InstanceNamedWith Equivalence True Passed
819fdac304a35d88b89b622c36d9af1f981e443c Apalache InstanceNamedWith Equivalence False Passed
1e952599eaa594f91ea896f70275c57f996d27c7 Apalache InstanceInFolder Equivalence True Passed
155a158ea79cee41f674f6bb80ace1547b44f82d Apalache InstanceInFolder Equivalence False Passed
e062d891e3c0ad030e94e6ccffb763851db79212 Apalache InstanceWithInFolder Equivalence True Passed
a7433cf689a7fe2c3d85035720fea0337b9cf145 Apalache InstanceWithInFolder Equivalence False Passed
f966e87381866b5335520c2e1024af75d3ef499b Apalache InstanceNamedInFolder Equivalence True Passed
3e0b632034ad8c6da082c7393186b0918f93e023 Apalache InstanceNamedInFolder Equivalence False Passed
8592c75280957eacc6b729b98d788698c7dfd55b Apalache InstanceNamedWithInFolder Equivalence True Passed
e3b6e4764bd3c60c2579e36cee04c98c9eff3b73 Apalache InstanceNamedWithInFolder Equivalence False Passed
7bd4c9936a24b376682a19a4da638daabbc9af1d Apalache Enabled Equivalence True Passed
00c946bef0a50fff85da141729495765dd28d733 Apalache Enabled Equivalence False Passed
7b653616ebc284cd2c57db5be8cb83a8acf34de1 Apalache Assume Equivalence True Passed
4512cc5ac3953cf381cda2ef930772e112090c80 Apalache Assume Equivalence False Passed
d1edae011aae2f1a651fcbea163e945e9a1dafbf Apalache AssumeNamed Equivalence True Passed
c044ae63dcc042b13cb74825f07beaff36e3c52b Apalache AssumeNamed Equivalence False Passed
f1243afefb39647974c6a0262cf630f0ae92b029 Apalache Lambda Equivalence True Passed
86bbf869e3f3e207d05aac038a876df17ca43a7a Apalache Lambda Equivalence False Passed
28993c91864402d39ca59927806a0916368b0d09 Apalache IfCond Equivalence True Passed
7994d25ea99f7ad562319c0c3cf6d7ab2fe12b95 Apalache IfCond Equivalence False Passed
004ff7bbacd598f59daf65ed5b3fe5ad2c78044b Apalache IfThen Equivalence True Passed
4bfe0d09592bfcf05097f0dbddb910e4fcc5eafd Apalache IfThen Equivalence False Passed
b5422a978b6f57fd05927b830fa71d449aadde07 Apalache IfElse Equivalence True Passed
d54dd51bc275bb1620a60355668cde9a27c33d19 Apalache IfElse Equivalence False Passed
69e950190d7be5019960506170fa39f4b016425b Apalache Unchanged Equivalence True Passed
ab2282ee5e8acaea6bcf347420e51efef564a2dd Apalache Unchanged Equivalence False Passed
6356f9a8cda9155773e9d86dc126f6caa406f854 Apalache Equivalence Equivalence True Passed
2a93779ed53f5e1f1c9a4a82b73498b5a21a2b7a Apalache Equivalence Equivalence False Passed
5744e8f565f866cf37bd3c49aaa10bbc5ca0dd29 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Equivalence True Passed
faef683d22b33aa4736d5eff367a89848dd5009c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Equivalence False Passed
4d8c4f6460f5fee462bbbb83cb1c45f59ccc362c TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Equivalence True Passed
f61c5f439d662b0b754c178273a646321bccd5cf TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Equivalence False Passed
f85564e659a0036992eee2a5ef0859bf910e9609 Apalache BagBagIn Equivalence True Passed
61c39b516633337fdc891223f30bfc830a89d2f0 Apalache BagBagIn Equivalence False Passed
c47b2e63586af1e6c821e326aa3d5d614108be74 Apalache BagCopiesIn Equivalence True Passed
60d600d20efd8aa8499fbf7b5f9e5f5fcc66b829 Apalache BagCopiesIn Equivalence False Passed
52504ead642a38c06ac078422bcf8156663a642a Apalache SeqAppend Equivalence True Passed
47238f18f2ca6f188cdf23e4209c922e4f8e21d5 Apalache SeqAppend Equivalence False Passed