Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
32e2cf8fb8d64ce0844bc9a6863f9c45cdd59ef4 Apalache And Ne True Passed
0cf12e8bb5a359341061638cd4c32596ff60c663 Apalache And Ne False Passed
8c00add5ed3440c3120041f6027ca4be3e082b24 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Ne True Passed
fa375fcfb03641250218965713ede1315347ed65 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Ne False Passed
051cd0cd9d07bc1a809dd655f3254779c880d55c Apalache Imply Ne True Passed
4aeec08cfa87c34a49ace438026782215172f865 Apalache Imply Ne False Passed
bb05ddb0ca1c01028cc1a3cccab6057a8b8e9933 Apalache Not Ne True Passed
557702caaa4588a99b7d2d1e3cea721336f42636 Apalache Not Ne False Passed
774e2fdae959345c2773d4779d7e9c34c1c79d50 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Ne True Passed
bab89e8db0070eed5292017d9688a7dd9ea67057 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Ne False Passed
eb2592d0e0382aaf13a8cd98555a832546b7e3ac TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Ne True Passed
a8ea7d51ce3d5f731cdb285ee0fe8a2e68a44bbd TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Ne False Passed
5e86c02fd4dfc4cae8a6985c3c3b6142d181097e Apalache AndProp Ne True Passed
88a063e88524449d6e7fc0643b3e1f963119839c Apalache AndProp Ne False Passed
e6da0caf30ef69f0771e3aba043842f4ee1ccbf2 Apalache Boxed Ne True Passed
b14409249d126a97263422863370eeae25106306 Apalache Boxed Ne False Passed
159616899eea774ec145e8e412b7fbef1676e9d2 Apalache Eq Ne True Passed
fa1047c610c5e9ec868407b40b0ba34fa062dd38 Apalache Eq Ne False Passed
522f16adb8cb89a1ac6db4609c0d26145bc2cd7e Apalache Ne Ne True Passed
07733a7477313a9cf7a494eb5ded5d270f141290 Apalache Ne Ne False Passed
914b71041b9c93dac4afed8c5a0baf0e90c07f1a Apalache Let Ne True Passed
5c63c3c6dc4d45de7c2d164b600e9273c50a7fa5 Apalache Let Ne False Passed
cf790474d72d04bb7023fb2c40f2ef8a87b7d219 Apalache Set0 Ne True Passed
9106e59ba344d28e8858708b4ba20257a1dcb9c6 Apalache Set0 Ne False Passed
054fc96a7567507c4cbd77834606a0c926714f8e Apalache Set1 Ne True Passed
5a9af5e5eac88d01da8dd55680b671b4889c787f Apalache Set1 Ne False Passed
1d0573d69a874b42ccda3b82c19369b1543fdb9e Apalache Set2 Ne True Passed
73aefcd248061c250ec5389b99568b0d97b93a84 Apalache Set2 Ne False Passed
f3e4d7ac09abbe3e4e4dca6147b82f1e66fb92e9 Apalache Fun Ne True Passed
4b383ba3c4a5076cbcb4c804a8297e4177614a02 Apalache Fun Ne False Passed
e75be4e0caaa60dc00b662d3aa723da4cac51f34 Apalache In Ne True Passed
f8e2359e693b218ce915a552628f4db5c4aba8e8 Apalache In Ne False Passed
7c0d241bab1187307b4f8c0a28d53acee6fb64d9 Apalache NotIn Ne True Passed
767e893946676a3e382292878c48d71de8fda52b Apalache NotIn Ne False Passed
a7860d94284a772f1757fd879d00da9e005be967 Apalache Exists Ne True Passed
9a50172b37b783885e1562931b97c021bf55678e Apalache Exists Ne False Passed
659e00c31f8a685696a3a91cfae343810bb6567f Apalache Forall Ne True Passed
e1918432e1b7fbf31a942c05492d76509e6a3469 Apalache Forall Ne False Passed
34ae665676973327b27a581ad0eaa89dab85247a Apalache Choose Ne 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.
fef49c794ebed4050d2c975d336b40177678bffb Apalache Choose Ne 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.
549f0c88be79aa5b93f30413998d6de8a4f0e3ea Apalache Record Ne True Passed
c51920f4b836f505fbede4a5b71d4df791ef18f8 Apalache Record Ne False Passed
b71aae35d3b7496923b3f418b97c5f064dd3b762 Apalache Tuple Ne True Passed
d6c2fdc837aa23619fc3136cb3913e5f36d82a75 Apalache Tuple Ne False Passed
164448b2a4918c74ca0d5d9432ff111af8cbecc2 Apalache FunApp Ne True Passed
dafa9e12119fdff9860c25b84c7cb92c238568e7 Apalache FunApp Ne False Passed
c4b6a3d7c0b7a335f4112a6e15f716eb048593ee Apalache Except1Fun Ne True Passed
80ee70f30544c1b711105d9223f5c4bbebaa58f8 Apalache Except1Fun Ne False Passed
b5e0c674ba8ac5cd972635ef0f20384d264986fd TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Ne True Passed
a0d6e585d332b897e377e51a1e968f81f5cb974c TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Ne False Passed
44f5ac7c2cd7d3a25430a86956c1e22e9f5c944d Apalache Except1Rec Ne True Passed
3decdfb4b44154f2daf92672bc46009f0022dced Apalache Except1Rec Ne False Passed
b7dbcac6c9529cd4563457fdbcbdec2b3445272e TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Ne True Passed
471893aeee11b1272b66e02862f86789e567dd1a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Ne False Passed
bbf46aaf0772f67a75bbc192d0021ca77aebf9a3 Apalache Except2Fun Ne True Passed
78c1667453613671657e348add7286c1d281c5d0 Apalache Except2Fun Ne False Passed
cdc91a8b00cef6afa16ad6a004a673fbdef984c3 Apalache Prime Ne True Passed
b3238436806e684ae39a4bc89c203a4e8db1edde Apalache Prime Ne False Passed
c89550f85063552a66e4c7878b482ed71ea9c26b Apalache DefFun Ne True Passed
bf0e8ec1ea6f9c88dd2f5b4a01c3d1d0dc2eaa02 Apalache DefFun Ne False Passed
4db608c5a50d269b4f8f49886a1a2e37adfc93c4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Ne True Passed
2429a0e0119b5ccc1d00a6e66763fbf10f017d13 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Ne False Passed
5ad12480f64b4b86050b84bb53b4760cc0a024ff Apalache DefFunRecursive Ne True Passed
65323a11b51ff83512ef175ce2a870cc905f81fd Apalache DefFunRecursive Ne False Passed
a3cc69cd868469ea98dbc61d84b42d180d8d6f5c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Ne True Passed
d12b0fea7ab77feebf5cbd436791c13c27d5f3f6 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Ne False Passed
864653529079172a6c6c676464fb7405f6e64e2b Apalache Def0 Ne True Passed
06d487dfa7de95a82a1c24bf91e0154ca7e7851f Apalache Def0 Ne False Passed
1eca6826ec01f2ee6e9b4dcc312298ccdd1772f1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Ne True Passed
5c739aeb1c631c6aa084954dda8f3eb00b721f1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Ne False Passed
97f238e69ee350bb864c9d9938e2cc602f0ff5ef Apalache Def1 Ne True Passed
aacfecdac09094444831a9e9de82c74527cb0196 Apalache Def1 Ne False Passed
ea7ebc1a3f70fb86d2507f37117c9326e60d6d41 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Ne True Passed
4d0c0572eeb7d41a186334029d41c01c7b3e4adf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Ne False Passed
6f2d23249bcc7cc8488eaecd22e598a38acb60e1 Apalache Def2 Ne True Passed
aa2af6fcfa4b9a29417b7c0610d9dd40ffdfe587 Apalache Def2 Ne False Passed
81fa06a7d6574045fd0ffba7fd27e4421abf1818 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Ne True Passed
8c4dcf55d89b4d43e86a1494274fab20f9c14220 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Ne False Passed
7e2999f3a8afdacabfa967587d36ca6054f3eb53 Apalache Def1Recursive Ne True Passed
6364753ad08d2c30a0a407391e59a4eaf026ce16 Apalache Def1Recursive Ne False Passed
8bf0bd2368a706195650d41587bb9c1c08ae1282 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Ne True Passed
da7a8f88918852b7096ef1e1a853e68eef105c40 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Ne False Passed
9890d52aa2d5ba55eab5dffd32f266713a4242b6 Apalache Extends Ne True Passed
e6ad78a6e54360696eb09e82d93e6da0e8d638d6 Apalache Extends Ne False Passed
500b9907a175ea1deff8d814e21f1879d62202a4 Apalache ExtendsInDifferentFolder Ne True Passed
524a10f21ad9a9b6ed3d6026997abeed44d22434 Apalache ExtendsInDifferentFolder Ne False Passed
0671d1de782522a7a8089566e97d175f1639d2ee Apalache Variable Ne True Passed
77b972c2a5c537e12f917aa112fe0dfd1048045c Apalache Variable Ne False Passed
2b92f79b4a58b4d990797199fe149d5c1acd5d5f TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Ne True Passed
531fcc4ab0ee8156a5730a666b6d3bbd0ca810bc TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Ne False Passed
4525be6078e66fea88d0daefdf2242dc8b12b79f Apalache Constant Ne True Passed
bd9c9d9cd403c62ec0dd1d1c76f23c94e61bccd1 Apalache Constant Ne False Passed
beb054b4de9325f8dee2a10b632da5ef447c8e65 Apalache ConstantRank1 Ne True Passed
c5a7d183ca7aba1f93d3e4746de6787fdf7e3412 Apalache ConstantRank1 Ne False Passed
260f9ee108867d0227e81687f77718219678fc7d Apalache Instance Ne True Passed
7c177032643250d2eaf3429ebcba0d456e74fe76 Apalache Instance Ne False Passed
276e6e7106d2f5188026c686b2239023f9645a2a Apalache InstanceWith Ne True Passed
e969c490e01dad77474f04170498ebcb9c8f73ba Apalache InstanceWith Ne False Passed
f1237a0e105d92379557dd2350e5944fc3a88b8f Apalache InstanceNamed Ne True Passed
cc0a07b3a9c48d433142ee0f20208cad10d8b6fe Apalache InstanceNamed Ne False Passed
0cc9237d0a747170131a2dd3e0e2dfcd310c789d Apalache InstanceNamedWith Ne True Passed
06b6239912a4d2c199b269de6f6119eadb58b163 Apalache InstanceNamedWith Ne False Passed
cc8a621e10ce660ec5e5af5964aeed6907e98d33 Apalache InstanceInFolder Ne True Passed
a2a9a38e5692922f8bf5768626af8cf1ba8a94bd Apalache InstanceInFolder Ne False Passed
af947531995c16e9604915e6534b7ee9af5ae250 Apalache InstanceWithInFolder Ne True Passed
04ffa0545a59222008fd2a277aed4c28c4991ef4 Apalache InstanceWithInFolder Ne False Passed
724e7fe4bbcae53c2e3754e9907b4e4b481c74d9 Apalache InstanceNamedInFolder Ne True Passed
7af56126bcce52b0fe6d063ca4b2ebc301e956fb Apalache InstanceNamedInFolder Ne False Passed
2096b546db226cad9f01747bc0eb401f3eb815d8 Apalache InstanceNamedWithInFolder Ne True Passed
1f80480dd7d9da14f9c4289c1ee33c8c174f13f4 Apalache InstanceNamedWithInFolder Ne False Passed
aa9957d1ec73697dba5e1b700a3dab555e17b44e Apalache Enabled Ne True Passed
5528e99a55a7e3ebe47560d9d660ff60b7f677ae Apalache Enabled Ne False Passed
5ec61836126644c77de60ce3a1944fc822465812 Apalache Assume Ne True Passed
33bc8bbed4d5ca9e878a70052223e0cc132c4631 Apalache Assume Ne False Passed
fb6ab188c956c30e533b993c0c95dcf437e27ab3 Apalache AssumeNamed Ne True Passed
25e9ecd27500754f5f888146011c3887fa8c0025 Apalache AssumeNamed Ne False Passed
cf1048a911bac5be62eefc006ac411ef8209a8ea Apalache Lambda Ne True Passed
006c59cdc786749b10209a9d48ba1f4362787c5f Apalache Lambda Ne False Passed
fdd110c48a6ae0d9d43cf67f8a8238e5e0d8698a Apalache IfCond Ne True Passed
42204b898547ff8df3db3f4269b7d8994c6aa19b Apalache IfCond Ne False Passed
172927294ba97cd756fa6954830a30ad1e69cc88 Apalache IfThen Ne True Passed
6c6e89c4bf23a22347a275b4965472696a2ae468 Apalache IfThen Ne False Passed
5deff266d37fab9586e80cdc6ecdb92db940e9c0 Apalache IfElse Ne True Passed
be97ee264181623d2d8e069903d3bbb5e4b8121f Apalache IfElse Ne False Passed
7f5c36348d5a1d63d43d4ddfefaf3723a21ff36a Apalache Unchanged Ne True Passed
0f3e43bfee46e311f1839542826c7332c3c60653 Apalache Unchanged Ne False Passed
48bd4a8429b7658ce7b09f456a6a10d67ed0c29e Apalache Equivalence Ne True Passed
acca261028a27e11d9d82fe389989835af7430c6 Apalache Equivalence Ne False Passed
50ec20e190d2fd7b97a8acdff777da5665531213 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Ne True Passed
eb61246e86c6ccb73ef2de19e3b46c3b28588e19 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Ne False Passed
3a9c1a49de6670db9cf670df3fd2f94471617c2d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Ne True Passed
9bdc3d29f39368a3c3e3e56aa60441e7110e21e2 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Ne False Passed
c46e9e905e69f77b17f91e58d2778e6e6fc3a2d1 Apalache BagBagIn Ne True Passed
0c4c103371a00c28957a591d840a05581d194cbc Apalache BagBagIn Ne False Passed
b6866b7df81bec51ad134cc3cd4a960722f6b650 Apalache BagCopiesIn Ne True Passed
c875e6b543b2007073695a0421d60f88ebc892cf Apalache BagCopiesIn Ne False Passed
1be8b83ee8105b0fa54626c5f947ad8265f8c25b Apalache SeqAppend Ne True Passed
5d1f632604f40d07a6e21a55fc70ed71f0fc706a Apalache SeqAppend Ne False Passed