Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
1875ad1352b9a2952d6d3064428c0f020644a006 Apalache Eq Subset True Passed
3a103bd0d016c22a5358f6c62dfd4b7c5caf3589 Apalache Eq Subset False Passed
6b03695874c807d91684fce7267cddbae62685be Apalache Ne Subset True Passed
0b54be0a6940661e25e8e2be9fbed21e446dfdb3 Apalache Ne Subset False Passed
b183581e0692fbddc2cf0c7ac68fbdf8a60ba522 Apalache Let Subset True Passed
6fdcd5cfa4abc859be5758bef01c8f0550b1a4ea Apalache Let Subset False Passed
2e819c6ebd512f4459776e7015f81372eb04a2ac Apalache Set0 Subset True Passed
aef2e0fafdddd096941b430c154d9f7315f5f12e Apalache Set0 Subset False Passed
34474d6a3db2446d8da4e6783b58ec57f24a356e Apalache Set1 Subset True Passed
fa67775ca9fa29a1fa7e66a0ec1fa1460e784bdd Apalache Set1 Subset False Passed
da9589de3d5948945714e59e6e481f6a23a95f1e Apalache Set2 Subset True Passed
4925273512a688985182a4e5f841607df1cf6489 Apalache Set2 Subset False Passed
75b512e87d212c737996c5a010b18fdb7bcd7ae1 Apalache Fun Subset True Passed
b4cc86f510d6a8410f85525b80006fdebb4f3cda Apalache Fun Subset False Passed
b01bca57354d7bc7dd9d9ba014b9b41f0fe401c3 Apalache In Subset True Passed
ec2d081c6aa15d16d62db9151e200bc112bfc0b7 Apalache In Subset False Passed
a3289da7a4c977721bca42c9a01e4abfe32e69b0 Apalache NotIn Subset True Passed
2c5fada064435a4d6568c3c9520db8f5f72c278d Apalache NotIn Subset False Passed
5f386267a713b9d20b139082412e1dc3a02544df Apalache Record Subset True Passed
c28e7560929637ab489aab97ef06165345fecc88 Apalache Record Subset False Passed
21d5024b84b202c94a8d3d09f0dd7f698a898fb6 Apalache Tuple Subset True Passed
298f62286577a6b40d50c6f414d893351b7b33b6 Apalache Tuple Subset False Passed
81c71bd37ee26c22cd13dd8fae8dcfbed975b913 Apalache FunApp Subset True Passed
50d522e97c9bccf438acb419e9e45289b1a1a31b Apalache FunApp Subset False Passed
af9109c6f6b1158ed71de4adaaceb0c68b44d149 Apalache Except1Fun Subset True Passed
4b41dccac6e3c980523de133d251922f1a42f8d0 Apalache Except1Fun Subset False Passed
1836e204ec171880cf71a07f21ad32ed84aa3c80 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Subset True Passed
f24ca527bf3bf1d6ca89e1bff24d227a13a946e1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Subset False Passed
8453926e4f75b347c677a4dc2fb38a85bfbd0c0a Apalache Except1Rec Subset True Passed
1b9e154fc3c423adf38cdcb2c16d60750fab1ea0 Apalache Except1Rec Subset False Passed
5b31e4a5d427773758aa0e3e6882e07d00c848cf TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Subset True Passed
e90ea7aaafe3cf88958706dda20c9860901a986d TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Subset False Passed
4783790b8100a9c6916caafb48693f71f7b320d6 Apalache Except2Fun Subset True Passed
11dc6b099f14d60fc19f37b2480f21a4616f4a81 Apalache Except2Fun Subset False Passed
295072cd68dc892752447e42d0a4b0aa5d2dcb45 Apalache Prime Subset True Passed
be8489df6f163c090b00fa5d3ece7ac7afa77b23 Apalache Prime Subset False Passed
b531181a979b0ed476949c75093ebeda84452855 Apalache DefFun Subset True Passed
00a9c11cd8a64061cdbdd858e2ed8d47760bdf11 Apalache DefFun Subset False Passed
7f351314e614fcdc717ae26744a8b606f2750821 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Subset True Passed
c22145116d0f0242ed7fee64efdc1a4ca6def195 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Subset False Passed
e57ef7fce02faac9c8f305df28ac23c07479da32 Apalache DefFunRecursive Subset True Passed
20e03bc9ce7de30f31aa737eb5bbd0b15e712099 Apalache DefFunRecursive Subset False Passed
80c0044f1466c51178dd02f4658770a2b1557075 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Subset True Passed
36924ecf4ed614465d21a6d2c3e29dadb5fbae6a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Subset False Passed
e9d30cd23359f88da0b0a41683959ef13a1f8416 Apalache Def0 Subset True Passed
1d57decaa1bad21dc4e2a96492eabbde6c04a264 Apalache Def0 Subset False Passed
b56a98a392f43bd323b7ef80a2fa551599491787 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Subset True Passed
a5670a6c70c1cdc8596550d85a57b9c65b555e90 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Subset False Passed
8d01c41eca61b746a4437b65732b21482131d64f Apalache Def1 Subset True Passed
0056aa995a02d7c2c0b5dfacdfa3b1061c606703 Apalache Def1 Subset False Passed
9b9da29360dbb71bd259362ad04d81458ff9f2b4 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Subset True Passed
b66ebee914bf46fac75cc3a5be91c668cf5f9f16 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Subset False Passed
6f7d7f6e1bc850def3287d828f7ebebd4e8dc027 Apalache Def2 Subset True Passed
bf161336fbd1d19a34f07befdb0be4c72e04d9aa Apalache Def2 Subset False Passed
5e6cdd6c975eb796a50e45fc67bb32bc6919fb77 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Subset True Passed
7eb98081297f950aa3d04274d6bb7fe14b196e05 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Subset False Passed
3275cd3597ee9b6c3e392c23a647ae90a0ef4291 Apalache Def1Recursive Subset True Passed
003923df3d4b0a247ba52aadf6459c5ad19ed97f Apalache Def1Recursive Subset False Passed
bc8311c59b6d5f9402c77ed7f4a4aa0e53b3a360 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Subset True Passed
e570f762b76893627f7fbf7f36522e8a4168ebfc TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Subset False Passed
9ac34bae1e04b44d090f547bc7c831e49f2e36ef Apalache Extends Subset True Passed
72f542fa240887e788d0fb6f7e812491788cb593 Apalache Extends Subset False Passed
f96ea086322e8d91ad3856710a717adc0d250787 Apalache ExtendsInDifferentFolder Subset True Passed
15519bc2812d9aee3d24b1f9ddb2c27d9e715e7e Apalache ExtendsInDifferentFolder Subset False Passed
d300cc219af6071dee9f30e17ae1d28c62f98173 Apalache Variable Subset True Passed
2e3b8afcd96d5a9caf31227bedfc68bd1d83661e Apalache Variable Subset False Passed
59e42c7feb6c0c7784803f6191da0ca8da71c3ca TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Subset True Passed
c424ad8e82c58b87846c170004b495b805ff3d59 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Subset False Passed
ca6c1fd94417f2d9b4623434587eb479efaf6dd1 Apalache Constant Subset True Passed
c77e1ad5cca7382d090b1986ac49795e88a93dc8 Apalache Constant Subset False Passed
61ffa1fdc1e84edc0907f94fd63c458a24109360 Apalache ConstantRank1 Subset True Passed
92886dec7a58db5ac013bbcfe2a8098716f10e2e Apalache ConstantRank1 Subset False Passed
28b8e15c811fb8a53ccc827975130cde933f15e0 Apalache Instance Subset True Passed
7ca71106bbbbaf830b2183ffaf2a1557b6912ab5 Apalache Instance Subset False Passed
6e5be8e66ed9900c644862531c0d2ebb2d09c5f5 Apalache InstanceWith Subset True Passed
3c981a27e09d155f78ee81acb33ca364cfb1882a Apalache InstanceWith Subset False Passed
d3bd390dcf4d2439a78b7288017c3863eb6c7cad Apalache InstanceNamed Subset True Passed
16da8840d4af26100b5f9b28d6a64225f708f0a7 Apalache InstanceNamed Subset False Passed
935c0fc858bbe3875238ae677e516fe055085f49 Apalache InstanceNamedWith Subset True Passed
dd1395acd76eaa5f1ca36c66ad1e6e35bf245852 Apalache InstanceNamedWith Subset False Passed
3a8eb4835409eb41f7251892a4b57bb03854f59d Apalache InstanceInFolder Subset True Passed
5e1e76170a6430ae1007e337c7423de32f2049af Apalache InstanceInFolder Subset False Passed
28b9c846e7565636460f0c0358b5536d3967ab3b Apalache InstanceWithInFolder Subset True Passed
e8fbd810e87fc2560ecb57a2bf040f4298553130 Apalache InstanceWithInFolder Subset False Passed
9a4d88d6b27fd48b1257dbb3c8b59f3ef5b237f5 Apalache InstanceNamedInFolder Subset True Passed
0882ba03be4d76fa7a386c526b392ae3ceb5b9d2 Apalache InstanceNamedInFolder Subset False Passed
9bf8af9e7ba23ccc0c84f2931ce35451044f8321 Apalache InstanceNamedWithInFolder Subset True Passed
1c7cbd16e6476bf48e70ad590dac645cd49acb53 Apalache InstanceNamedWithInFolder Subset False Passed
fc4aaa7686f17d7b9a5657a59fb45e2dda60d514 Apalache Lambda Subset True Passed
967ccbc3d512b486f99bc819f4f3049cacdb4d0a Apalache Lambda Subset False Passed
ec8d4ebb11d7fef58cdc76680004062a08af5496 Apalache Cross2 Subset True Passed
5079c11dae9a9ee5bec835ede4ad2a46f7d02b5b Apalache Cross2 Subset False Passed
2cc86d609db77278cdbe36bcb5aae004c48a348c Apalache Cross3 Subset True Passed
a8223e6e7ce3ac238df291712db8808e54d48cb3 Apalache Cross3 Subset False Passed
13e30e480f625b6dc089d440543f8e721bfb3c4d TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet Subset True Passed
d3f7b7507a7bd8f23220299173ccde573749ec5a TLC with reduction strategy:
  • Case Feature: For finite R replace [D -> R] with explicit function set enumeration; for infinite R replace (f \in [D -> R]) with conjunction (DOMAIN f = D /\ (\A x \in D : f[x] \in R))
FunSet Subset False Passed
dbc4081718eb94ba7da0269847a27f23bcea9780 TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet Subset True Passed
0ac90ba8fe7d662edb94d1b7c14897da67661c3a TLC with reduction strategy:
  • Case Feature: For finite R replace [field : R] with explicit function set enumeration; for infinite R replace (f \in [field : R]) with conjunction (DOMAIN f = {'field'} /\ f['field'] \in R)
RecordSet Subset False Passed
56edabd084c4806ba85f869409baff12e623e422 Apalache SetDiff Subset True Passed
89b74b055ae528aaa9bf04fbbab89fc6ba54b745 Apalache SetDiff Subset False Passed
3dbf797f191cd13166210303543c152c54fc65b6 Apalache SetUnion Subset True Passed
4335ec0bb7d5e2cfd6bc965e673eea83f9d0610c Apalache SetUnion Subset False Passed
e70d24a555b98da18ab1d32600552152b0211021 Apalache SetIntersect Subset True Passed
ccac5eabbed77da002e702370b909f4e69551305 Apalache SetIntersect Subset False Passed
c9604330b704159560a7de45b2eae40cfa7cf140 Apalache SubsetEq Subset True Passed
23684752f31df6d3e342d1aaa773daefb2d37011 Apalache SubsetEq Subset False Passed
7abfbf743f38547c69ea39ea9ef739f0348ccb19 Apalache IfThen Subset True Passed
0b86f4ab58d9a7ccbefadc500be065fdee824ade Apalache IfThen Subset False Passed
1a9fe566d89ffd34563515faf1dcdb72db68645a Apalache IfElse Subset True Passed
078557b4958912cb0296b453d8cc45fb06b8d5e6 Apalache IfElse Subset False Passed
c6974ce424643138a72979b42cb9e09db2c11294 Apalache Subset Subset True Passed
9933ff964715bffb5a386d7048b99bbe3a8ac2c4 Apalache Subset Subset False Passed
7064790e221a088bad0fc8e3c7d572415d77f501 Apalache Union Subset True Passed
565f6ac6d5f13d6229a323f22f84286ce2b04965 Apalache Union Subset False Passed
700c2575640ae4d7617d37281ea76a06bf4251c3 Apalache Unchanged Subset True Passed
c80bb031fdafd09e1b867929d46b9496387f558f Apalache Unchanged Subset False Passed
274b58f49b919b6fefb3e95530a8396cb8f68813 Apalache SeqSeq Subset True Passed
59e6bcc2c4a7d7fd2599d801ee935e9c39d57f9a Apalache SeqSeq Subset False Passed
f9558ceb65aa1465c39c0c040ce8c0a2bf7f1514 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Subset True Passed
d2120fdbb33821a27b5c7e4464094454c34194f5 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Subset False Passed
bf9f3d0f5935aa2e7c00258e691f3c1bccd99e18 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Subset True Passed
3f0bbb47538d6896beed3df1cc87dd9c78eaa54b TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Subset False Passed
115c075e140397aa5569eb1766254731c81c6117 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Subset True Passed
7db96ec1ee44ac9d9e8549344264111854379d37 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Subset False Passed
9c3f76c3547e29d631d048f9afe146f9e4bb878c Apalache BagSetToBag Subset True Passed
882423bf498074c809f3b36d04bd5d9243822498 Apalache BagSetToBag Subset False Passed
e802afbd177e3aff33a61aeace8aaaab14b0b574 Apalache BagBagIn Subset True Passed
0e3ad2d68bb594bdd71dfcfe6284426b60d6854f Apalache BagBagIn Subset False Passed
37e9c39aeeee048ddf741307d268c67a25924431 Apalache BagCopiesIn Subset True Passed
ae0496c2c7728c771ce55f94648bcab7813a8156 Apalache BagCopiesIn Subset False Passed
420d0fb2a36b7d10337b926e540910f19b7cba19 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Subset True Passed
40ae7d32c3e1015fcd205fb468362366651a9073 TLC with reduction strategy:
  • Case Feature: IsFiniteSet(B) is reduced to either TRUE or FALSE, depending on type information (finite and infinite sets have different types)
FiniteSetsIsFiniteSet Subset False Passed
bfc2ca3d0cb9d48779d7b4a45786e66b2c8a9d9a Apalache FiniteSetsCardinality Subset True Passed
061b789b1147b4b81feebffb21c6341cc64a378e Apalache FiniteSetsCardinality Subset False Passed
cd38c1f2eabba978362c7adf4ce4e48674b53526 Apalache SeqAppend Subset True Passed
43970ecc14a15dda98c167b85598b4de709d2604 Apalache SeqAppend Subset False Passed