Id | Type | Case Feature | Plug Feature | Check Deadlock | Test Results | Test Models |
---|---|---|---|---|---|---|
bde3dd56526d8c05fcb2533d5604a3971e9b5f9e | Apalache | And | Not | True | Passed | |
b356d2503f38f9bd3ab7d0f5534425ba6f1063c4 | Apalache | And | Not | False | Passed | |
f32be84bcb25b678147d2bbe2fa33ab5e139e0f1 |
TLC with reduction strategy:
|
AndMultiLine | Not | True | Passed | |
fe0d36f35fa3a18fdaf969c095d824ca0d1a790d |
TLC with reduction strategy:
|
AndMultiLine | Not | False | Passed | |
90f1e67440dc17e354c7f85b66117bdd834f3fab | Apalache | Imply | Not | True | Passed | |
5c4dae6909fe3a7df20b32cbb785953be4a79162 | Apalache | Imply | Not | False | Passed | |
306456070cb441c51b54dee95f9e338da4befac8 | Apalache | Not | Not | True | Passed | |
067efe3c3b5e6bdf7d0dd9f0c7ca026846a999f4 | Apalache | Not | Not | False | Passed | |
72343bdf1061d442c715969692a4a49b39b482f7 |
TLC with reduction strategy:
|
Or | Not | True | Passed | |
f34111f8e99d4837785a0424248967de04251179 |
TLC with reduction strategy:
|
Or | Not | False | Passed | |
a5aaa01ef26ef717e4e040efaab4474dba560b80 |
TLC with reduction strategy:
|
OrMultiLine | Not | True | Passed | |
a23eccccd6e3104967cd1f5abe594f3f9111bfcc |
TLC with reduction strategy:
|
OrMultiLine | Not | False | Passed | |
b3b9095f903ac03be858ca24df566ed7032db9d0 | Apalache | AndProp | Not | True | Passed | |
d399c3ca9ec6c9b75aa5fe4eee8959f029c26548 | Apalache | AndProp | Not | False | Passed | |
8e712d990298a151ad1f71678cb02e37794cbbc0 | Apalache | Boxed | Not | True | Passed | |
c9de56110cfd3efb6e8ebb4c809d52589c981530 | Apalache | Boxed | Not | False | Passed | |
9ef3a20352e38aeb37af37ad4360a385eac25d23 | Apalache | Eq | Not | True | Passed | |
0d0029507005791253d40c91b936f9e9d409c19c | Apalache | Eq | Not | False | Passed | |
9e66e99317be5d9ae88e96ec4f22696c7b784d3e | Apalache | Ne | Not | True | Passed | |
95f55f66cff664863595b3e3bb3ebd26c499685d | Apalache | Ne | Not | False | Passed | |
c85781eb0f6d5a54314ee18d24c81854477a4c70 | Apalache | Let | Not | True | Passed | |
bf21403654892c5050acbeedd8bc42af1f006d37 | Apalache | Let | Not | False | Passed | |
f9b6889d0f93c692c862a0aa471253c712f911dc | Apalache | Set0 | Not | True | Passed | |
61989fb6ae65577da5e525df4fd044abe5eb53e5 | Apalache | Set0 | Not | False | Passed | |
3b16f950f51ad09bedabb74617d0ca1e92dd29a8 | Apalache | Set1 | Not | True | Passed | |
ca0013887556fe0cea75e793b6bd83141a98afdf | Apalache | Set1 | Not | False | Passed | |
32ced51d7bad6caf609a4c50261bf822dbc2851f | Apalache | Set2 | Not | True | Passed | |
e90de7743fb232f037e638ecd064f1865fd68085 | Apalache | Set2 | Not | False | Passed | |
724817d16dfeb1c71eb7e2e8f0ea743f61693f3c | Apalache | Fun | Not | True | Passed | |
582eaa9b5cd42999fb528e0c49bd603e7db2e5a2 | Apalache | Fun | Not | False | Passed | |
c01faef2df5deeee02540c37ff0324097a453d56 | Apalache | In | Not | True | Passed | |
808f570465a6ac23e5ae888d79ab1f3a809e2174 | Apalache | In | Not | False | Passed | |
1d3bed688f7da90a785f805c0c2433abcc4f0e06 | Apalache | NotIn | Not | True | Passed | |
b6b8d714da92b5e48de717609688a8dc6caaad13 | Apalache | NotIn | Not | False | Passed | |
328de057e68d8059306b85730850a298641410c1 | Apalache | Exists | Not | True | Passed | |
6b9f597b80bd75c11a3077126df645393e3d51b9 | Apalache | Exists | Not | False | Passed | |
79715d99ec5ab4d68cb805fdef68335d9bf1e31d | Apalache | Forall | Not | True | Passed | |
559c1fd79ee55a143503d5ea00d5d90bce05f520 | Apalache | Forall | Not | False | Passed | |
6f4b6450456ea77d11909cabd20cdee0a7323965 | Apalache | Choose | Not | 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. | |
f2f82f385106fcf3529bcb41555fcf0e475d4ab8 | Apalache | Choose | Not | 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. | |
3fa73ca397661e5e35bdd4d53c6064db2bd6f57b | Apalache | Record | Not | True | Passed | |
725db4bdbcd3568800d0757616d00e2edca19aa9 | Apalache | Record | Not | False | Passed | |
7fe9cc35ff2736f1900a1d59ffec7fac2f00d4bc | Apalache | Tuple | Not | True | Passed | |
a629994cc4319d21ce547199934c3a8faabff995 | Apalache | Tuple | Not | False | Passed | |
3976d45ff757e3f0ee83cce760661b367bfd44af | Apalache | FunApp | Not | True | Passed | |
bb4a571886b0fedc04e67f468956e1de5b2a85b8 | Apalache | FunApp | Not | False | Passed | |
f0d887f774e10c62e02b8b9b54d5cfbf0c3956e2 | Apalache | Except1Fun | Not | True | Passed | |
591e98ed958b2b6ec167764f6f9c978a93f8a62e | Apalache | Except1Fun | Not | False | Passed | |
aabb28f4a91a27cee1bf8a4fe2e8d4b0c92ec46b |
TLC with reduction strategy:
|
Except1FunWithAt | Not | True | Passed | |
6ef250972d19fcef5184a2549aee94e07bfe0b75 |
TLC with reduction strategy:
|
Except1FunWithAt | Not | False | Passed | |
141d59aba9bdc82afd2b9ae0c731c91547115eb6 | Apalache | Except1Rec | Not | True | Passed | |
758178f118a885c453c33cf35e5af0137ecb42ac | Apalache | Except1Rec | Not | False | Passed | |
3229fdb09a23b2df7d810559894a7563e672e845 |
TLC with reduction strategy:
|
Except1RecWithAt | Not | True | Passed | |
77be4eef3f4dc78f24a69244aa40274d456be958 |
TLC with reduction strategy:
|
Except1RecWithAt | Not | False | Passed | |
d15ba9c7f0130f3bcdb322ec6f3ed173213393e3 | Apalache | Except2Fun | Not | True | Passed | |
8214e1e03135f71d993eaf1f9f96e1b91c62dfda | Apalache | Except2Fun | Not | False | Passed | |
443ca44ac58fac6bc25f093f7c38e8492fe7c495 | Apalache | Prime | Not | True | Passed | |
194f8f56fd4fdfedf7e0b4f4a06bfd32c1ad792d | Apalache | Prime | Not | False | Passed | |
951781c18032422457c42dc250fc53a8a85acd60 | Apalache | DefFun | Not | True | Passed | |
0c78a63878af135d2ea0894c884f7229ca9885ff | Apalache | DefFun | Not | False | Passed | |
942807f3d88d407f7e9e53ba5e97e194625b23e0 |
TLC with reduction strategy:
|
LetDefFun | Not | True | Passed | |
5d581b66b9dbddcad75fb46f823c21101ef11aed |
TLC with reduction strategy:
|
LetDefFun | Not | False | Passed | |
e3b10ba64b0a3b0b1794bd5411a0ba8e330d787c | Apalache | DefFunRecursive | Not | True | Passed | |
db8684c8df227b7669c94220a58eb4114bd6b664 | Apalache | DefFunRecursive | Not | False | Passed | |
51f027a43c1eca3ee281727ed363cd522be9103d |
TLC with reduction strategy:
|
LetDefFunRecursive | Not | True | Passed | |
b0c0c4251db18faf033e01df75fd521b2ff46c0b |
TLC with reduction strategy:
|
LetDefFunRecursive | Not | False | Passed | |
e25e3726fa999da58593f4ae2056fa571dc97dda | Apalache | Def0 | Not | True | Passed | |
6e8c043ff9c7bc5e701297be2529e26b40389f8b | Apalache | Def0 | Not | False | Passed | |
8654e294bc5e5f214c5fc5791ac4734f13474c7f |
TLC with reduction strategy:
|
LetDef0 | Not | True | Passed | |
29bb1d48f2d9da0c87bc3e06ddc2d5198ca984da |
TLC with reduction strategy:
|
LetDef0 | Not | False | Passed | |
b8eb1a420db359a882b2edb725aa38e1d50dbb17 | Apalache | Def1 | Not | True | Passed | |
9254870bf23a7263621c1dd2527f210512e54673 | Apalache | Def1 | Not | False | Passed | |
abee8024c5fa8b5411d45c242effe4916475a9f7 |
TLC with reduction strategy:
|
LetDef1 | Not | True | Passed | |
326d0298ef24da0b5d7cab35372fb89b2b5e34ea |
TLC with reduction strategy:
|
LetDef1 | Not | False | Passed | |
0d734bbc05c0a98d7d5ddd677f9abce9df24d4bc | Apalache | Def2 | Not | True | Passed | |
49d4f3584348c6739018c020548a9287d258958f | Apalache | Def2 | Not | False | Passed | |
1723780b0dd96417494df067a13034d4288f0572 |
TLC with reduction strategy:
|
LetDef2 | Not | True | Passed | |
ce27716b5a1ed370b28d56684016c92fc61031da |
TLC with reduction strategy:
|
LetDef2 | Not | False | Passed | |
f76acc7f791b910d516d32df3d75eae199426317 | Apalache | Def1Recursive | Not | True | Passed | |
c5b5eab4ef1cbe2ac0e61d2a809767679c320b5c | Apalache | Def1Recursive | Not | False | Passed | |
3885c60a8893f4465b40f3560fe20a607078de8c |
TLC with reduction strategy:
|
LetDef1Recursive | Not | True | Passed | |
3ed3a088d637883546414ab9556d0e67cfd9dc47 |
TLC with reduction strategy:
|
LetDef1Recursive | Not | False | Passed | |
f01d366758a3b1f9a433129099f1e6856f749ab3 | Apalache | Extends | Not | True | Passed | |
f68c8a06103223a2253b68cf4fca5f626efe425d | Apalache | Extends | Not | False | Passed | |
36795d84082b110d2d5ef5e31052c5b015f83001 | Apalache | ExtendsInDifferentFolder | Not | True | Passed | |
f8620fd3e104761dca0c388693a4007d03e2ed52 | Apalache | ExtendsInDifferentFolder | Not | False | Passed | |
74b0eb20af7a3683f4d419d0ef7e446440f7c00a | Apalache | Variable | Not | True | Passed | |
a3c9baea421b54da7506b64ac43ee5fd608e5f55 | Apalache | Variable | Not | False | Passed | |
ba394567a098b0aecf6fb385c730e395639858a2 |
TLC with reduction strategy:
|
VariableViewExclude | Not | True | Passed | |
eefd347c7097b1c84bd57fa86ef17894cc232fec |
TLC with reduction strategy:
|
VariableViewExclude | Not | False | Passed | |
d53641767d904b3303b9383508e4f61901dec04d | Apalache | Constant | Not | True | Passed | |
ec052f170e4de95f1a12a720bf4be86003dd9a50 | Apalache | Constant | Not | False | Passed | |
009c74d7c74476a0c3f5671e997d7916ccd6cccb | Apalache | ConstantRank1 | Not | True | Passed | |
9316b4c2b916b37b5c75be6e3c9660c4bf56a12d | Apalache | ConstantRank1 | Not | False | Passed | |
95c0ef9a622fc4a90526158599fcbac5e42ddabd | Apalache | Instance | Not | True | Passed | |
7d8a8127df7ce8339ca8648190985cec1314a095 | Apalache | Instance | Not | False | Passed | |
b02dac24c226ef3234d1dbece6e40a69ef250b48 | Apalache | InstanceWith | Not | True | Passed | |
f204c067f5e8c595943d5945e701b6d3de229f52 | Apalache | InstanceWith | Not | False | Passed | |
0a1fefd3cd05cc7a134366f9a35a80072a9e31a5 | Apalache | InstanceNamed | Not | True | Passed | |
502bfe6324a9e7d54946434406f2b4e8dc4df716 | Apalache | InstanceNamed | Not | False | Passed | |
15cb67f320745cb2e12f265a278c2240075bdaa7 | Apalache | InstanceNamedWith | Not | True | Passed | |
c08e9332bad9631a39d7eb597c1009acf6709e4b | Apalache | InstanceNamedWith | Not | False | Passed | |
ef78c6d965452504ac9256dc36d5099507539abb | Apalache | InstanceInFolder | Not | True | Passed | |
3682c3592928e700f3a1c2e9f6a03fb91407fa35 | Apalache | InstanceInFolder | Not | False | Passed | |
30e999fc4ac4c361ca9bcd8f9c32ca1ea88f5199 | Apalache | InstanceWithInFolder | Not | True | Passed | |
12ca80172623e499ef080e0c847a6b7233c1fcaf | Apalache | InstanceWithInFolder | Not | False | Passed | |
4409246e885448a3d0bea10c0b1b2c1f11e59e75 | Apalache | InstanceNamedInFolder | Not | True | Passed | |
9b17098bb39173925b22fced82bc1a7b0e70e59a | Apalache | InstanceNamedInFolder | Not | False | Passed | |
486536447f0e26c3e46442617755cbfbd9a8b9d6 | Apalache | InstanceNamedWithInFolder | Not | True | Passed | |
cdf6de2ea742c1bc18917101e09b2703e5fca252 | Apalache | InstanceNamedWithInFolder | Not | False | Passed | |
89c236159a0cbea584b1c43cc58659ca793b66d9 | Apalache | Enabled | Not | True | Passed | |
37e0a8995dbf39dc7b9d9ebccd61406092d03c0d | Apalache | Enabled | Not | False | Passed | |
c6993462344521884eee0827d1eb34890bac66ea | Apalache | Assume | Not | True | Passed | |
ab1ed1527c6e1d15d04eff06e048d59c2dad1506 | Apalache | Assume | Not | False | Passed | |
4de9f86db8ac23f64ca038a596243105e3fb5033 | Apalache | AssumeNamed | Not | True | Passed | |
a333320177240021c257d3b3572be5b9fc9ba974 | Apalache | AssumeNamed | Not | False | Passed | |
5ad8f1468be36eb0fd6b3108fed35827132cf032 | Apalache | Lambda | Not | True | Passed | |
f7b76d27b6954261b997535d72efcbe60aa6d13e | Apalache | Lambda | Not | False | Passed | |
5a0769ca50983e0f0b3002735033c351d6666c8c | Apalache | IfCond | Not | True | Passed | |
d2c6a7f946ab4fc03d90e1e611d902c634f57133 | Apalache | IfCond | Not | False | Passed | |
f9120c3685048682711edb5d8b05d141dea0821d | Apalache | IfThen | Not | True | Passed | |
fa32b0575038e4d2a7dabe1e0e98f8da64ac83f8 | Apalache | IfThen | Not | False | Passed | |
0d5408fc42709c930937894a009171dab3acef10 | Apalache | IfElse | Not | True | Passed | |
db2153d34158d93b4d032ca0af6663184d7f5976 | Apalache | IfElse | Not | False | Passed | |
f4a5fc7eca8c1027815dc7867e0364e46b827e2c | Apalache | Unchanged | Not | True | Passed | |
320a7eb5a4eee1bbf9f3ae33ba578b5d563630cb | Apalache | Unchanged | Not | False | Passed | |
93f4e71e3e81f963325458316d0e8a0850225742 | Apalache | Equivalence | Not | True | Passed | |
596359e670c0d2603bef29d5347eb42501a282e1 | Apalache | Equivalence | Not | False | Passed | |
6f82028fd2765f9d4201a0a215b26ae2d631f43e |
TLC with reduction strategy:
|
TlcSingletonFun | Not | True | Passed | |
28e09122612cf3c3d109441843f8870b4637e443 |
TLC with reduction strategy:
|
TlcSingletonFun | Not | False | Passed | |
8379b3b86568127fad0ea572e0d90f0cd2ad1c83 |
TLC with reduction strategy:
|
TlcEval | Not | True | Passed | |
6042d287e7317d62b771df43a2850a9b25f40a98 |
TLC with reduction strategy:
|
TlcEval | Not | False | Passed | |
8ed77716c188ce2af48d077cb084042449538ff5 | Apalache | BagBagIn | Not | True | Passed | |
ede531bd35dba1539850a0c8144fc576e45f0900 | Apalache | BagBagIn | Not | False | Passed | |
1169e03b27b98bbecdf0c7c942fe590ca1718650 | Apalache | BagCopiesIn | Not | True | Passed | |
db90cea1225a3790afd75c30373d263bbd84d21e | Apalache | BagCopiesIn | Not | False | Passed | |
98a41c14095285515cab89e526fc2222d5ed48cb | Apalache | SeqAppend | Not | True | Passed | |
d58248553bd09c8311a795b6dd061ab544f97d8a | Apalache | SeqAppend | Not | False | Passed |