Id | Type | Case Feature | Plug Feature | Check Deadlock | Test Results | Test Models |
---|---|---|---|---|---|---|
d4064e66fc69c93202ce3cb94d725e295f39a84d | Apalache | And | BagSubsetEqBag | True | Passed | |
1dd94d4979a5b9d7a50f37e677730e788bfc4279 | Apalache | And | BagSubsetEqBag | False | Passed | |
d9eddf370a2cf7d27d9d62b9a352c49d28c20861 |
TLC with reduction strategy:
|
AndMultiLine | BagSubsetEqBag | True | Passed | |
ad13e4967849b22c5de21548e09dab431c37d580 |
TLC with reduction strategy:
|
AndMultiLine | BagSubsetEqBag | False | Passed | |
de0d0a1e48639c017e4b5eacfaf07acf7860ac6e | Apalache | Imply | BagSubsetEqBag | True | Passed | |
cacd53f993220b11c11f02acbbedd2f94810c749 | Apalache | Imply | BagSubsetEqBag | False | Passed | |
340e39e31c8b913cc759cae9fb6f0f7a3bd577c3 | Apalache | Not | BagSubsetEqBag | True | Passed | |
007f7c50786a8b42cae0e1be2b73f3f798fe0e08 | Apalache | Not | BagSubsetEqBag | False | Passed | |
41fe47e89f789b50fed0b29bacd18763fe1c62ac |
TLC with reduction strategy:
|
Or | BagSubsetEqBag | True | Passed | |
06318d10e54f37f7ac0bd1f9326ce01ddad22bc1 |
TLC with reduction strategy:
|
Or | BagSubsetEqBag | False | Passed | |
015518e8d8f3ecf0c5d4694d6b9c24300409185b |
TLC with reduction strategy:
|
OrMultiLine | BagSubsetEqBag | True | Passed | |
c59997a88e04978539189dacb2219eca89c6615c |
TLC with reduction strategy:
|
OrMultiLine | BagSubsetEqBag | False | Passed | |
68ced92e52c5a24210e5ce4c21c10df088f5fdf2 | Apalache | AndProp | BagSubsetEqBag | True | Passed | |
2ee3d93b5695153d5be0ea929d841addb7cd4ac2 | Apalache | AndProp | BagSubsetEqBag | False | Passed | |
68fdceca048e91228295d0ae5fbc9c7d4a3a908c | Apalache | Boxed | BagSubsetEqBag | True | Passed | |
4d51a649f02d42d07ed97a6a48da5903dce91cca | Apalache | Boxed | BagSubsetEqBag | False | Passed | |
513b7ed6ce6891bad180df53ca7208b3896dd0e0 | Apalache | Eq | BagSubsetEqBag | True | Passed | |
698cf305ef0d3cbd2b1b21f6968be203995046ed | Apalache | Eq | BagSubsetEqBag | False | Passed | |
f142a75557363ea0b11774cbe7a570e7bbe0a193 | Apalache | Ne | BagSubsetEqBag | True | Passed | |
217aba63029199e99e83d56f975a987d2643bb5d | Apalache | Ne | BagSubsetEqBag | False | Passed | |
d6512937b39d463ac4f2ed52ef626d0f873cdfa6 | Apalache | Let | BagSubsetEqBag | True | Passed | |
8fd900bda06b5b937a1f3bde13998d69ad802e04 | Apalache | Let | BagSubsetEqBag | False | Passed | |
4360e0d08c4fcd1b637afbd722edde6286ad67b1 | Apalache | Set0 | BagSubsetEqBag | True | Passed | |
ae170741a3cadc61cb5b98862af4f8dcac926828 | Apalache | Set0 | BagSubsetEqBag | False | Passed | |
9e2ba70e24531e02574139f58061bc361582f210 | Apalache | Set1 | BagSubsetEqBag | True | Passed | |
2124efe01cc45e70cf2cbe675ca7eb7d46c70029 | Apalache | Set1 | BagSubsetEqBag | False | Passed | |
d21274d685795c958eba5cdef9602aadf3e6da73 | Apalache | Set2 | BagSubsetEqBag | True | Passed | |
9a5908e58d9c80243fb699c49dea3410d24015c5 | Apalache | Set2 | BagSubsetEqBag | False | Passed | |
efda27595fca6d8dde41014d57a4b7f1c83eba04 | Apalache | Fun | BagSubsetEqBag | True | Passed | |
0944cbb3a8c03604d20570a56b0b4f368a07459c | Apalache | Fun | BagSubsetEqBag | False | Passed | |
4ab2d41b97e68cc4effd64d6b74852d3d7843541 | Apalache | In | BagSubsetEqBag | True | Passed | |
9b7cb3b6fbab2c55bae7ffae9ac09627d29232bd | Apalache | In | BagSubsetEqBag | False | Passed | |
e676266635b03f54c5058be922a1dad8ce40f374 | Apalache | NotIn | BagSubsetEqBag | True | Passed | |
e811105aeb9040cac802f5a76f7218166dfa384b | Apalache | NotIn | BagSubsetEqBag | False | Passed | |
4e851d9d4136f6e254a0ad7403a12a8be7e96fcd | Apalache | Exists | BagSubsetEqBag | True | Passed | |
22f3f8ecd0efc2f32ad3c43f061da2cfb4fab75d | Apalache | Exists | BagSubsetEqBag | False | Passed | |
1c38127cf9e689bcb673700fefe0050ee155ad51 | Apalache | Forall | BagSubsetEqBag | True | Passed | |
071638dc2df97bada7e5943095d908ae501083e7 | Apalache | Forall | BagSubsetEqBag | False | Passed | |
60c7365b4ab7bd2051d5d3a1e2bdd53e417a28d4 | Apalache | Choose | BagSubsetEqBag | 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. | |
79f8bff2282b53f2375f9055f6f0d44e921b2f5d | Apalache | Choose | BagSubsetEqBag | 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. | |
a2de2467e5abe2dc3dc4d32d9000ebcfd9a6fbdf | Apalache | Record | BagSubsetEqBag | True | Passed | |
38b676019f1ac676f51ca85f5f184c088335ef25 | Apalache | Record | BagSubsetEqBag | False | Passed | |
878edb6bd8b789b7451a8686eb6b86908e9f1afb | Apalache | Tuple | BagSubsetEqBag | True | Passed | |
106b6926e5ac7957fec9fd938328bd8fc234b2bf | Apalache | Tuple | BagSubsetEqBag | False | Passed | |
488081a59be9fc7b93a6fa6195a484d566a13b57 | Apalache | FunApp | BagSubsetEqBag | True | Passed | |
66da7f7ba0597768378bd1c90053a451808494bb | Apalache | FunApp | BagSubsetEqBag | False | Passed | |
252270cfc3c2f4cf239f914df1b4e54cf1fe924c | Apalache | Except1Fun | BagSubsetEqBag | True | Passed | |
1ae8fceaf4bf3c839b72d29dd3beb527b18c32cd | Apalache | Except1Fun | BagSubsetEqBag | False | Passed | |
4f3c01a5a7334f1d9aadf1d0ed4f79a470020dda |
TLC with reduction strategy:
|
Except1FunWithAt | BagSubsetEqBag | True | Passed | |
408af4b5643ff7d502ea8e6796dce22cc723c279 |
TLC with reduction strategy:
|
Except1FunWithAt | BagSubsetEqBag | False | Passed | |
42e330a06c9e3328fa90b617a6246c18af95c8fe | Apalache | Except1Rec | BagSubsetEqBag | True | Passed | |
4508f82bf1352616016255eddea77a31067fd309 | Apalache | Except1Rec | BagSubsetEqBag | False | Passed | |
d28d4ce336e5d7715d74bd73d0c8a9e268632376 |
TLC with reduction strategy:
|
Except1RecWithAt | BagSubsetEqBag | True | Passed | |
7e174916e39bffe1b74faa6c29af52d95060adb9 |
TLC with reduction strategy:
|
Except1RecWithAt | BagSubsetEqBag | False | Passed | |
c2f786f1c69396cd6161e82d61d55c946556ba9d | Apalache | Except2Fun | BagSubsetEqBag | True | Passed | |
58c7726987b24819594eaf77a5c29041dac044d3 | Apalache | Except2Fun | BagSubsetEqBag | False | Passed | |
6956cca1ab274e1c2d67e327af3c8b8270ff9c98 | Apalache | Prime | BagSubsetEqBag | True | Passed | |
b621278ee0d06f14a0192feef84acb24e5c26a41 | Apalache | Prime | BagSubsetEqBag | False | Passed | |
fc70cd1e0d8b92c8cdd15032d5fe2202548888ae | Apalache | DefFun | BagSubsetEqBag | True | Passed | |
2270e801c5926f51c3163d0e20070e2bbd69b6d2 | Apalache | DefFun | BagSubsetEqBag | False | Passed | |
02149e5f86266d3b4ff835f707af2bafdec6d142 |
TLC with reduction strategy:
|
LetDefFun | BagSubsetEqBag | True | Passed | |
98fdea14c2baae0607154856dc83cb137209050b |
TLC with reduction strategy:
|
LetDefFun | BagSubsetEqBag | False | Passed | |
aafa0d5e7e42322188d101f67aa711a40aa1f166 | Apalache | DefFunRecursive | BagSubsetEqBag | True | Passed | |
f907723dd8b7b789e4f2ff7210e0b1d1160d69ab | Apalache | DefFunRecursive | BagSubsetEqBag | False | Passed | |
184d8afdb643014e9019d52c3680f668cb424dfb |
TLC with reduction strategy:
|
LetDefFunRecursive | BagSubsetEqBag | True | Passed | |
bce2e29c1aa85ce83a4297667f20c6c3df2f2984 |
TLC with reduction strategy:
|
LetDefFunRecursive | BagSubsetEqBag | False | Passed | |
96ce495c285577ce595330c6b503f7c64be299f8 | Apalache | Def0 | BagSubsetEqBag | True | Passed | |
db40f0751f0e2621298b541b89faee725c285676 | Apalache | Def0 | BagSubsetEqBag | False | Passed | |
a3cbe2cc10c5052f19fa913ebb302e5e6efe906f |
TLC with reduction strategy:
|
LetDef0 | BagSubsetEqBag | True | Passed | |
76bf5654285dc337496329d4296092e8d6c1a55b |
TLC with reduction strategy:
|
LetDef0 | BagSubsetEqBag | False | Passed | |
2d7b49195e2c26216a096e21e559173a6815172e | Apalache | Def1 | BagSubsetEqBag | True | Passed | |
a6ab4d59c22ddc907013b22d89454123d2c5a229 | Apalache | Def1 | BagSubsetEqBag | False | Passed | |
79ccde906d8f45828b4843e4a7249e5a2756d822 |
TLC with reduction strategy:
|
LetDef1 | BagSubsetEqBag | True | Passed | |
3c4404d81236492c987ff30ebab98387e8790016 |
TLC with reduction strategy:
|
LetDef1 | BagSubsetEqBag | False | Passed | |
0b8956f133536f400823b14df172c3e214f3606c | Apalache | Def2 | BagSubsetEqBag | True | Passed | |
bb9a8c693571b84d294a89f2b2c9efcd06e4213c | Apalache | Def2 | BagSubsetEqBag | False | Passed | |
fdd64b6131d862e1e3d943c333fa7c6807a77bf0 |
TLC with reduction strategy:
|
LetDef2 | BagSubsetEqBag | True | Passed | |
81ebccc624e56cac2a804c3061244449917a0c77 |
TLC with reduction strategy:
|
LetDef2 | BagSubsetEqBag | False | Passed | |
44b43a0a9b370c9569c9d6356ce7fe31a195dfe6 | Apalache | Def1Recursive | BagSubsetEqBag | True | Passed | |
d69a55bcd39808b434b7ac956276322a8705be71 | Apalache | Def1Recursive | BagSubsetEqBag | False | Passed | |
82971dcab5344f2d953f751c180a86323ea05bf2 |
TLC with reduction strategy:
|
LetDef1Recursive | BagSubsetEqBag | True | Passed | |
d11c40304edf807e3da857f0292ef0614a0d3a26 |
TLC with reduction strategy:
|
LetDef1Recursive | BagSubsetEqBag | False | Passed | |
70db327844b371cc77954067a813e034da5efeac | Apalache | Extends | BagSubsetEqBag | True | Passed | |
ac2c3d0aede589bd568a98e66b23e70f260d2239 | Apalache | Extends | BagSubsetEqBag | False | Passed | |
5e0c1807c8bca86151125bdbdbbd7f2ed2a7124e | Apalache | ExtendsInDifferentFolder | BagSubsetEqBag | True | Passed | |
ef9d858269c9a7af1ed4fd95fcc8032b813aa9a4 | Apalache | ExtendsInDifferentFolder | BagSubsetEqBag | False | Passed | |
27a2baeb29735ade089c05cbf9423a238179fe97 | Apalache | Variable | BagSubsetEqBag | True | Passed | |
53c88fbd79e88e872596d8b063c87335697d9137 | Apalache | Variable | BagSubsetEqBag | False | Passed | |
69e83f7ea6e1d3012d51cd9306a33f10d2d73adb |
TLC with reduction strategy:
|
VariableViewExclude | BagSubsetEqBag | True | Passed | |
adcd0da47be2bb9d6eb93d1d0dc03a3fc54b8c17 |
TLC with reduction strategy:
|
VariableViewExclude | BagSubsetEqBag | False | Passed | |
52864ab0a252c94ca9dfb56a5348fe952fd8caad | Apalache | Constant | BagSubsetEqBag | True | Passed | |
4ea72fe228ee8c62e51d5fba6583b9372dbacd75 | Apalache | Constant | BagSubsetEqBag | False | Passed | |
30a3f4b50045ae81e1cb9c317946ae963734256f | Apalache | ConstantRank1 | BagSubsetEqBag | True | Passed | |
6823e1398fdb14dbcef9fb44a04ae151159b6bcb | Apalache | ConstantRank1 | BagSubsetEqBag | False | Passed | |
f7f81158627dc6fcd03bdffd2f3b6b4bbdaeb691 | Apalache | Instance | BagSubsetEqBag | True | Passed | |
b94d92c40ddbc1ddbc9661ca777c7bc313395a90 | Apalache | Instance | BagSubsetEqBag | False | Passed | |
b962e3f831e838f0a6f48bdc3115ce44484a45d3 | Apalache | InstanceWith | BagSubsetEqBag | True | Passed | |
5390ee408e3322d7937648bb30acd86ecd4a1678 | Apalache | InstanceWith | BagSubsetEqBag | False | Passed | |
825107858a2f294c21e368ee5325dc4bcef6ea74 | Apalache | InstanceNamed | BagSubsetEqBag | True | Passed | |
bcb2d38e5c5ee71f7cf045521e6ac118fbe100ee | Apalache | InstanceNamed | BagSubsetEqBag | False | Passed | |
488e2dc79b2662774ece2f263915499236783394 | Apalache | InstanceNamedWith | BagSubsetEqBag | True | Passed | |
98fc0a660b575b268fe4e697e96932293d42d678 | Apalache | InstanceNamedWith | BagSubsetEqBag | False | Passed | |
8d10128bd52c4232add9803d145ccaadbec1cbc9 | Apalache | InstanceInFolder | BagSubsetEqBag | True | Passed | |
f374b23b66b3c26068d2e56c195d55a29c6cce24 | Apalache | InstanceInFolder | BagSubsetEqBag | False | Passed | |
df87dbf2baa409fd544a443dd258278448374873 | Apalache | InstanceWithInFolder | BagSubsetEqBag | True | Passed | |
834d569d11754cedf254d60cabe7a3a4ec0fded3 | Apalache | InstanceWithInFolder | BagSubsetEqBag | False | Passed | |
36c611df80ca982c1ba5e469cdfb82ce0f9e4eec | Apalache | InstanceNamedInFolder | BagSubsetEqBag | True | Passed | |
45478c796466826a67a71a2d17797bd8765e829c | Apalache | InstanceNamedInFolder | BagSubsetEqBag | False | Passed | |
b24f79d268760cf2d0ad618425a2f7ed629ba8c0 | Apalache | InstanceNamedWithInFolder | BagSubsetEqBag | True | Passed | |
0c0008ec143b95eeb77333bcac21e1f15e150bee | Apalache | InstanceNamedWithInFolder | BagSubsetEqBag | False | Passed | |
64b8098acc329c87fed23a0f8b0bef671200d47a | Apalache | Enabled | BagSubsetEqBag | True | Passed | |
5b66a22b372780017fe8a1eb6cf8efe48631ed95 | Apalache | Enabled | BagSubsetEqBag | False | Passed | |
a862e5ceb09586301621e9618dbc89da2d3cbdb8 | Apalache | Assume | BagSubsetEqBag | True | Passed | |
d4bf314cb195558de5b903ff1ed97f05a4411109 | Apalache | Assume | BagSubsetEqBag | False | Passed | |
df03a56917fb3b50d452063b7e9741b9543f78ed | Apalache | AssumeNamed | BagSubsetEqBag | True | Passed | |
d531dc8b84c3e219ede24329a0cad5f3141d52c4 | Apalache | AssumeNamed | BagSubsetEqBag | False | Passed | |
af17cdf2f0c846829cba4c72278a60820b579ae4 | Apalache | Lambda | BagSubsetEqBag | True | Passed | |
99e3bc8c325c181aa5118180988ff7f19993ce97 | Apalache | Lambda | BagSubsetEqBag | False | Passed | |
8355b23b2536721f0bd07d7755b169897b60f22c | Apalache | IfCond | BagSubsetEqBag | True | Passed | |
bb33b539005ba23c2545156e7c9288636992315b | Apalache | IfCond | BagSubsetEqBag | False | Passed | |
4380932ff944b79a00edd30439d80ecde02c0963 | Apalache | IfThen | BagSubsetEqBag | True | Passed | |
e27bdb6d417779a7b7f76438b94fbf14349dbc6d | Apalache | IfThen | BagSubsetEqBag | False | Passed | |
4e5e43a5bda6d542dea7329a865d6a7f321a7b39 | Apalache | IfElse | BagSubsetEqBag | True | Passed | |
359667035343955c47ba3efe375ca14bd2235dc9 | Apalache | IfElse | BagSubsetEqBag | False | Passed | |
399fc70f3e43c2fe54ffc8b3ddd099ce4b59c895 | Apalache | Unchanged | BagSubsetEqBag | True | Passed | |
1b86764624ea111c6e35e8b89269ddc0505f67b5 | Apalache | Unchanged | BagSubsetEqBag | False | Passed | |
4f22f77cdbabd3ad4ab85a8dc1cca5db1752795e | Apalache | Equivalence | BagSubsetEqBag | True | Passed | |
2bd44cbdd34711b5af65f82b1377fe3ccd80f78b | Apalache | Equivalence | BagSubsetEqBag | False | Passed | |
42c2298cc03facef64d3b54cced821ad184babf3 |
TLC with reduction strategy:
|
TlcSingletonFun | BagSubsetEqBag | True | Passed | |
4c34634b60d20c1f418e455ce4b1eb6ef1b0fc3b |
TLC with reduction strategy:
|
TlcSingletonFun | BagSubsetEqBag | False | Passed | |
4f7ba4969097a7934cf2055cde3826b113c6422b |
TLC with reduction strategy:
|
TlcEval | BagSubsetEqBag | True | Passed | |
60270c822c6a6f61e46e9c3b8c538d0bcc99dda7 |
TLC with reduction strategy:
|
TlcEval | BagSubsetEqBag | False | Passed | |
d084e0e755ed8ec63690c95d3cbe8c84a3f2c1ae | Apalache | BagBagIn | BagSubsetEqBag | True | Passed | |
7b9518ace3082a876085762fe23d79312e951cb6 | Apalache | BagBagIn | BagSubsetEqBag | False | Passed | |
39096a4a891dba562befea5f63bd9317f5de5249 | Apalache | BagCopiesIn | BagSubsetEqBag | True | Passed | |
955f1168b418a6c6d52f3875e627430f22ac3a38 | Apalache | BagCopiesIn | BagSubsetEqBag | False | Passed | |
ff70427904d767adf81146e351ea73b713fbfa6f | Apalache | SeqAppend | BagSubsetEqBag | True | Passed | |
98f2c6a7ee4c75de30a6fff854202d33583171d7 | Apalache | SeqAppend | BagSubsetEqBag | False | Passed |