Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
01ed4385a97083bac252f551ca17a0a9906e7496 Apalache Eq Set1 True Passed
d48f6693357a7f716fc7df53407291552eec13c1 Apalache Eq Set1 False Passed
a8b8ce929472dce1b538a01ab78ccc83e19bef60 Apalache Ne Set1 True Passed
af74f6ed35a011d700cfccc8bfb1d02a497163f7 Apalache Ne Set1 False Passed
fbc15e4dd73d8ef1f136a9af5b4ff222d9be9922 Apalache Let Set1 True Passed
04931032ba178e883eddfa429b5b251e0388948f Apalache Let Set1 False Passed
6b1e4a526251991016fb6e38e9824defc7a99cff Apalache Set0 Set1 True Passed
4f0ab6230a54595f041b4074953f84c07146a939 Apalache Set0 Set1 False Passed
0748c979b2df58205e84218d394628f110b2e32a Apalache Set1 Set1 True Passed
180511a1c23f042b40d6ace4dc7a5fe211050a9c Apalache Set1 Set1 False Passed
89bb8ebb57a1bce8760c2d6bc5662a20a926dee5 Apalache Set2 Set1 True Passed
c66659e3e601ad7fb675bd0d7c03ee108150cf60 Apalache Set2 Set1 False Passed
9f3b4d5181fed248ffccc250b30da905c281afb4 Apalache Fun Set1 True Passed
d4cb5b5910d86f80a7b5336480110e4070f8c658 Apalache Fun Set1 False Passed
3b863e6217325abc25f14aa292cb796dba83a983 Apalache In Set1 True Passed
9afb41abf400cb2aa7855cb087db35fa61cee6a9 Apalache In Set1 False Passed
b2ba8168c2e8d84700e802418d40502a01153fdb Apalache NotIn Set1 True Passed
2744bd81714e13b5e52b61df4587b2049c1ab52a Apalache NotIn Set1 False Passed
4a67c526a94a3e8852d6c8eab5b65eba679e57a8 Apalache Record Set1 True Passed
8aa70ba8d1110e3d674cc1810eebea98b2d9044a Apalache Record Set1 False Passed
b2414c01bde639a3d0f4d9e329dc08ad58d0c123 Apalache Tuple Set1 True Passed
c6105fd0ebbcdb24d6b410982549f6bfdeef895f Apalache Tuple Set1 False Passed
e02bdb8a3ba6eadb306381ae3319bb111387dc8b Apalache FunApp Set1 True Passed
bcac5fc0c2b805a74714dc4863c9d1b46b4a427b Apalache FunApp Set1 False Passed
474fe47219f91dca08030e69bbea18a524bab803 Apalache Except1Fun Set1 True Passed
afb30d049f321adc12e3aa7fcce09aed8dcd4606 Apalache Except1Fun Set1 False Passed
7b21b1d3508d2dafd0f1f64ec858b701ba810727 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Set1 True Passed
deaa9d8f38e69a18ed60bad7c61b989c147e2765 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Set1 False Passed
7becc42d69fec8950342c3a6e1efb755832037ee Apalache Except1Rec Set1 True Passed
88961b160f6cfd571849c3524d7dd1987c8b638c Apalache Except1Rec Set1 False Passed
26281f2b1311b85b92a551d42119c91990efd02a TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set1 True Passed
07f0189a4a11a28829a941a86e579f27e4abf7c2 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set1 False Passed
f19c8fd31c886c9c548abf7d3fec541a63c18e66 Apalache Except2Fun Set1 True Passed
8525be60e9217ca22fda9d5cf6c6459f47dab337 Apalache Except2Fun Set1 False Passed
0271b578fea21d1444e45c6167ee3bcd11f7bcdb Apalache Prime Set1 True Passed
4a5029562ae36f925588716870309754b1795848 Apalache Prime Set1 False Passed
6c08c127c61cc43512e00ae402c5cd81ba269247 Apalache DefFun Set1 True Passed
b28bd361d0fef4fdec91e752a489490e65f1fa62 Apalache DefFun Set1 False Passed
908949efdb50c9c5c062812feab74ffd3f4df685 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set1 True Passed
e5787f039c62b8dee60d83c2d4aacc0c5b43082e TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set1 False Passed
0b16d9d3f81bdb4fde9534f779ffea79c31ad4cb Apalache DefFunRecursive Set1 True Passed
06e25ed1db5f4126156509c432fa8c7ec8fc1503 Apalache DefFunRecursive Set1 False Passed
e6677a6daf84263adfc8841bd7966cd7552a4f07 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set1 True Passed
d8dd5eaf6c2cc53188bb5cd67f6e541ba9921f68 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set1 False Passed
ea00806e4061f93e7a01937e55bb05c0f9dff9f0 Apalache Def0 Set1 True Passed
119bd8821b4a3c1b26dc1b77c8c1fac891c98447 Apalache Def0 Set1 False Passed
abcdff8bdc8013ec5aa6ccbb7cef354be821fb71 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set1 True Passed
434d9d99a1b1cfe5c4ca76463df967b26347efb7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set1 False Passed
4d9d144d677bf798c55ab70d4488c7bc9a55eb85 Apalache Def1 Set1 True Passed
74905f1ad84615425f92401b83a3c5c40efdc630 Apalache Def1 Set1 False Passed
5e1fb2e6d4b08dc187890e70b23fa8da742ef619 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set1 True Passed
e6bbf11c85063e4bbd50d88aa27a9c6d080d32eb TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set1 False Passed
e8ab6a857dcdd0ce7906f3e9320e5896affa7ae8 Apalache Def2 Set1 True Passed
1e37385d7a078665f66692f93301a8c92785b32e Apalache Def2 Set1 False Passed
c9fa2b89098529d1b81426e0eadab5e89b645ad3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set1 True Passed
f324121853306122b9446991972dd4a550988227 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set1 False Passed
7949800f588db802aebdbaa2117b87b95f72c854 Apalache Def1Recursive Set1 True Passed
152cbbc9f31bb43e0c307360d6e290c01a0bf5a0 Apalache Def1Recursive Set1 False Passed
22a3194ae05907c352350f00a1be68e38da93bef TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set1 True Passed
d74e3b88c4a1cf9e84c6b819f6e70b95aa86656f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set1 False Passed
269bb933c8f2508763ee7b13574e33e7078d3b52 Apalache Extends Set1 True Passed
5f83f5318246759db76315b0f148cec2bf05d113 Apalache Extends Set1 False Passed
59743986e6f8b08ef898a8abbee872434dd95ebd Apalache ExtendsInDifferentFolder Set1 True Passed
c1ef4186a6658a337685f6b113700bf87fd7618b Apalache ExtendsInDifferentFolder Set1 False Passed
068e14de8c80cef3b795aef517cd90ec1cec69f5 Apalache Variable Set1 True Passed
8dc7134a89b38a4e75d7d8b79bc5f43deec4de47 Apalache Variable Set1 False Passed
24e619a9cca88880055711e095b8455fa920ce95 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Set1 True Passed
2ca81380ef4799ae66c07ca3f167b0f0ac0cc1ec TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Set1 False Passed
8d93fc9b3a743c34fa1fd8c82891e8201164ed06 Apalache Constant Set1 True Passed
06c8f031f4ec3e7565109935165dd9024ecd8b11 Apalache Constant Set1 False Passed
ffa7b3dc422d89a2065d4db6cc2749b2080816e8 Apalache ConstantRank1 Set1 True Passed
4f819e927ce7c2b5e883f53425f32b3feaccd8d9 Apalache ConstantRank1 Set1 False Passed
d38bcc86d842c347c92060c9709fb4a2f78e5e00 Apalache Instance Set1 True Passed
0dd0d9f4cb949ce4bd44117f1c993a3e313737a7 Apalache Instance Set1 False Passed
74d389ae15c1c73c1fc75e441d9c0603060f8169 Apalache InstanceWith Set1 True Passed
5e4541f4f905b8885777e1be7cf84de2a30baa95 Apalache InstanceWith Set1 False Passed
e364f2e64f758ae2b5e93cbb00357c4e60f59f59 Apalache InstanceNamed Set1 True Passed
caedbcfd713b6254b4f89fd04ffa98ab6d8d582a Apalache InstanceNamed Set1 False Passed
66f025eadec97bf2c8f5aeca57eab0ac0bbb9e31 Apalache InstanceNamedWith Set1 True Passed
4a1af04168017cce8826e5ffde0598ebd33440f6 Apalache InstanceNamedWith Set1 False Passed
d530b7523dcef07c40b0856d5ae3708ccf68957b Apalache InstanceInFolder Set1 True Passed
f6259814710d2f2b9864e0e44d0aff6d5833cae5 Apalache InstanceInFolder Set1 False Passed
24aa595971a30ae486e2360a128ebea2641bd919 Apalache InstanceWithInFolder Set1 True Passed
731e153e8a8806ce6a5a020cbda3beddd96b9cbd Apalache InstanceWithInFolder Set1 False Passed
7e22ba8563493f3e08a8f116702277a626e8496a Apalache InstanceNamedInFolder Set1 True Passed
8e1152cd9c1bb80e6033db93114a33209c8f9511 Apalache InstanceNamedInFolder Set1 False Passed
c95ad536714a6df2d7e5f0a69f230b8da59b1a5f Apalache InstanceNamedWithInFolder Set1 True Passed
ed81fd3f797eac096d94483ad1a1933f12843c7e Apalache InstanceNamedWithInFolder Set1 False Passed
4ff48ca21a2c9f563f26a0ed04075d01bb8b11f4 Apalache Lambda Set1 True Passed
f7f35d0f2c1656563160891fb6fe4437f3ace7ea Apalache Lambda Set1 False Passed
8d732a1a10be322268ffcd98e6a695a72bd2bebc Apalache Cross2 Set1 True Passed
af9857f4975232709ef6900af5bb1a4b5de6bb89 Apalache Cross2 Set1 False Passed
215b2949c6a1daa42b9b8fb66d9a8b0a04054c85 Apalache Cross3 Set1 True Passed
3cb371ab2833ef974b72d85231068bbc9ba08df4 Apalache Cross3 Set1 False Passed
3bf62a9cc6b1869c77599b2937f271cd90a39abb 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 Set1 True Passed
b8d11f08e04c65040eece38265c61da3a6f90bc0 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 Set1 False Passed
a300026ee96f65da841658ba9d24e53434ecb04e 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 Set1 True Passed
8e8b9bea7f22220e5d8aa3fcaeb28a7fcfca6aea 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 Set1 False Passed
0bce217cb7b8f6ea7de2de10e9a280681eba9020 Apalache SetDiff Set1 True Passed
68ab78d97fa901704f3ff3dcab8d69aa5b16fd33 Apalache SetDiff Set1 False Passed
26af49a9f6a873769108cbe8f42322e263a74d6b Apalache SetUnion Set1 True Passed
f94dd0d88458c0cb2ba28c6031eb7ce7c30c2743 Apalache SetUnion Set1 False Passed
4609a92c646015a1f4857e9b728a58a05c4c92e9 Apalache SetIntersect Set1 True Passed
194ad938390e9a3c573efecc0b737dc847e9973b Apalache SetIntersect Set1 False Passed
33f6a62ddbf47d6871f8fa8cc3c09e314420a1a9 Apalache SubsetEq Set1 True Passed
74f08d36d4172264cd41659ced866e9aff9ad4c1 Apalache SubsetEq Set1 False Passed
5d42827a24eb341449faf1a5f4d98479c84163b2 Apalache IfThen Set1 True Passed
27e081b43ee503d55e31b8f0dd54bf1646cd019b Apalache IfThen Set1 False Passed
1fd581b9bfc95d775d99fb648a288e41ef43b992 Apalache IfElse Set1 True Passed
fc37752c680821654c8fec8d96e48bb9e9f13711 Apalache IfElse Set1 False Passed
a45584d40038a069aa432f45b9244401b7870c3a Apalache Subset Set1 True Passed
f5b10c79d2220f6616b8a952a3e854effa650913 Apalache Subset Set1 False Passed
ba8ff3e8f0e834c414509120d0c2ad0948ad67ec Apalache Union Set1 True Passed
3d44db042e2902df6def69af48a26bfa3784aa10 Apalache Union Set1 False Passed
f08d94f1a9d33a9d9ea53abc9bd0c593c785bad5 Apalache Unchanged Set1 True Passed
39b8b66c66b9cf762dd66539e6e7ae2069741c44 Apalache Unchanged Set1 False Passed
275028cf8a193ac5c01d8951d4ff665c7382188b Apalache SeqSeq Set1 True Passed
d59baf9dc1623816134121128c2d205bea7ee502 Apalache SeqSeq Set1 False Passed
b801084a27c312a39e6501f002e4bdc5d686a0c2 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set1 True Passed
dca9df2c930bcc6547a16db7c2849997cdcde1ef TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set1 False Passed
f97ce67b3b9ea98b71f566074bcd0bead9e04cde TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set1 True Passed
3905ee6ccfd4006ea8acae80be1b937af4fd6c63 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set1 False Passed
178c457c55e1dd69c1c96a01e9547ceebd30ac9e TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set1 True Passed
2dc34db7120caabe497de80b6d53bc8209a83432 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set1 False Passed
0a29ad8bf14395e3293a275a54340639ff16004a Apalache BagSetToBag Set1 True Passed
1e05eb222044e49ab81914235f4406d22236e629 Apalache BagSetToBag Set1 False Passed
3262a04f970ace5e458f55fa4505c82582cb850e Apalache BagBagIn Set1 True Passed
98f399845c7239eb480caff82f377c7fb98b3cd7 Apalache BagBagIn Set1 False Passed
d4a6455baaef4269b33ea0c2b443824658377e18 Apalache BagCopiesIn Set1 True Passed
4b79093d89016ad3d5f43247ce52dd15f0035ea8 Apalache BagCopiesIn Set1 False Passed
68e41f5d2a0a3b3884971bad35502722a6d5f0f8 Apalache BagBagUnion Set1 True Passed
fcfcad326fb460e4b13b23b2605e94d6b0db67ee Apalache BagBagUnion Set1 False Passed
76f2aa28f579244f3ef4c9ee05b1bd9cf7a3da32 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 Set1 True Passed
a954c412070e683115aed11c2b7bd725185ce78f 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 Set1 False Passed
c4b6a63875659ca6983e65cdda29233cb2403a1b Apalache FiniteSetsCardinality Set1 True Passed
cd4000fa7fadc352f1ecddfe328229563e22ca63 Apalache FiniteSetsCardinality Set1 False Passed
f68ff2552b826fac9b2f6ffe0b351e70e3ff5115 Apalache SeqAppend Set1 True Passed
f20609d54b89e8746a992bbbfbada216030f6802 Apalache SeqAppend Set1 False Passed