Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
b51a0e507fdc4195fddd68e1da0346fd227c2037 Apalache And Exists True Passed
6104c8efaea0866af691c0128ed03de675df84ef Apalache And Exists False Passed
2895119d8fb523fb3281cc62f11e1f47a529346f TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Exists True Passed
15a026aecb472ec964759506a0906d1761cf36c6 TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine Exists False Passed
f5aa585d9c4b687503d49ac6634ce891520d16bd Apalache Imply Exists True Passed
bdd91d8e8142b3d40d5c3f4e74131d3ab0022223 Apalache Imply Exists False Passed
c0dcae3eeb35be4ced3ecfbc03015357e56be819 Apalache Not Exists True Passed
590f69222f3f626b034735d408ab5fc0f116e64e Apalache Not Exists False Passed
22d496105213b93fca7cfc72f8eae2bbfcd479e3 TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Exists True Passed
1a9678d8c80976a1195cfa53edab58d735e37fab TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or Exists False Passed
5da6c7c7fbf113dadbb539e7b910db8f64372546 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Exists True Passed
500777f5405e429ff21fd24d57c2d3268a807c74 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine Exists False Passed
997fbf116338fe4ee0c0bde809d5452e725bd4b7 Apalache AndProp Exists True Passed
5e2cdd9f589ab0902ba6332a5925f904f23f77d3 Apalache AndProp Exists False Passed
1efb29054d4663c82ada6ab74a50566fb1e84c32 Apalache Boxed Exists True Passed
730dca1655c1e9a5243b2c91dc2158e8f106f46f Apalache Boxed Exists False Passed
d6a8e19db585546d21b71e6c96a3676eb13291a1 Apalache Eq Exists True Passed
2f1227faf1e9fea2b3e9f297afb8f90620f36a73 Apalache Eq Exists False Passed
42ff11476ac9ee3ac267f1ec0b3d2edbf3ec7a70 Apalache Ne Exists True Passed
15f809673c284044c5022d6470af3c14198da8ec Apalache Ne Exists False Passed
a5da83a5ff27fdf544d45e52184f5273d41f7931 Apalache Let Exists True Passed
aea5feec63a83011e2b7d60efd981fe0f0876f1d Apalache Let Exists False Passed
b685357743842335043cea92d0868e0baecfc233 Apalache Set0 Exists True Passed
b1b8930b99b5f7117f74106708913a06cdecef4a Apalache Set0 Exists False Passed
d7c4c3db8ba3c54220aeac23fd4f7e44ef128347 Apalache Set1 Exists True Passed
5c50704311e08a185bbf5235c4fa4db2173ac801 Apalache Set1 Exists False Passed
b32dfa3fdbe2faa1e49a8f8f7951d17ecb1ef290 Apalache Set2 Exists True Passed
b3ff89cf279ae41aa9aaad855ac953e88976efbf Apalache Set2 Exists False Passed
fb4173c6891b844f9ef0cf857575440058773e85 Apalache Fun Exists True Passed
768639d9c291976a4f335cddab1fd0bdb2d65660 Apalache Fun Exists False Passed
77aade69a87583f673b25b0af79254ad3a423eb5 Apalache In Exists True Passed
acf64dbe8cd7609fac078eef612b1ae86b1e883d Apalache In Exists False Passed
89b56861bc4aacbe6ccbc67ab7ca33c1d86d2ffb Apalache NotIn Exists True Passed
63282ae70c7d4d191ab4344e6a778a1fea31571b Apalache NotIn Exists False Passed
05f0c757ef74c3548f82af4f943646d7b0a0a0a1 Apalache Exists Exists True Passed
167b4a9e00643baf9424f1a445f5252904dcde18 Apalache Exists Exists False Passed
205b0f52aa1883b07e738fc22a80cb86a8a1ad1e Apalache Forall Exists True Passed
1ee477e330d86725d6634c83a0485e9952a87d54 Apalache Forall Exists False Passed
6913cd1a256636118c9a1a114581d24ef2384c62 Apalache Choose Exists True Passed
e7c51f80ee3b9b7f88137bcdd4d347974c939293 Apalache Choose Exists False Passed
c4e8022de588ee00970518649bb7b6cf1d70ff14 Apalache Record Exists True Passed
50e28fca077176eec1a3f925b38bac43ed4a0b0f Apalache Record Exists False Passed
b6d5387799c3c02774273822428add677ebbabe3 Apalache Tuple Exists True Passed
5275b153b8e3997b7202511c7650a7430b9b57e4 Apalache Tuple Exists False Passed
3367010539b900ab6c3b83982f31c691c0ffacdb Apalache FunApp Exists True Passed
4b7c7843fdeaee1618938e4165020e573a836996 Apalache FunApp Exists False Passed
7ba6485b5279838460f2e4616de86519325c3e7d Apalache Except1Fun Exists True Passed
64f8d4a1f8953ceb344f78c5f9e4941b3b124653 Apalache Except1Fun Exists False Passed
b50a4195d958118eec329daae5aef154df1f94b3 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Exists True Passed
b5f6b41ee61a9de73a48d042ccb56086b828212c TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Exists False Passed
1aa2b58c2c5875206d9ec2d3c51c93cd429fb26c Apalache Except1Rec Exists True Passed
0f3775313e435bd7a539b1c76cadcded0a8b68c2 Apalache Except1Rec Exists False Passed
c53379140a0a6fdec06509b9ee96ad7cdab4ed7f TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Exists True Passed
25dc159fcb84a14bc417c2f618b0984135622fe1 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Exists False Passed
25b6e4b0860943d216a5ea53acdce3291968821b Apalache Except2Fun Exists True Passed
2492aaf31955c9a42fd4e14e562c35c673a08901 Apalache Except2Fun Exists False Passed
4162b3c9b4040a3e9be1ec54bacb8f6773513d29 Apalache Prime Exists True Passed
11dbdebf053d201660054ef9cd1cd87ae8fa43f3 Apalache Prime Exists False Passed
ee7828a2e5b5e5a4d4c2151ff8d2e0d224fc8f57 Apalache DefFun Exists True Passed
4125c3ae7bcf6d165b73d47abae26552e161faaa Apalache DefFun Exists False Passed
324abd0b181a961b2f7ab08247780c6097ad5b0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Exists True Passed
a8f898e840d084959ebe021b06550238ae27ed47 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Exists False Passed
5df4c4e3bc1a93dc94c1ecf0d0b9a2af59e375e5 Apalache DefFunRecursive Exists True Passed
a8ed4344e1ac25ea5e2f4f72bdded2b98614efe5 Apalache DefFunRecursive Exists False Passed
67cc4d81be11806033702eb1a32832fe860e3dbd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Exists True Passed
72af27fbd1e56911435d8694fa1e142504e7eb89 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Exists False Passed
d739d39a9a44b4ce6c40aa1a2a54130cc848e67c Apalache Def0 Exists True Passed
1b1bb161250df1a9d47e92c043388ad6caffd487 Apalache Def0 Exists False Passed
d7e5536e6a550fcf128050f39553db0f3356c14d TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Exists True Passed
41ab87c4881041bfded302e381416b9b7b31734a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Exists False Passed
ac81c5edd195b333d629d3a4a5c0cff2899d8f3f Apalache Def1 Exists True Passed
27de23117c5b9f302c7c359570e821c9c69b3b63 Apalache Def1 Exists False Passed
bcd3e40d9a1962aee490cdd3076a283772f80a60 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Exists True Passed
3586ae638a3458b96c356e1b808e6a8a73ac44b5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Exists False Passed
734902e311f007e601207404b9fbfc19fe99a58c Apalache Def2 Exists True Passed
5d877915a231dd54a10161c575f13538d1bb537d Apalache Def2 Exists False Passed
437f34dd639a50d2b0d6a241e147eaf94a005a1a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Exists True Passed
8805f467c4e7dfce221fa9450eeabb615b3afedf TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Exists False Passed
27dc70e56ab9f817e577c041e76a43079ed0be23 Apalache Def1Recursive Exists True Passed
4999f1d5016f12816eaca77be4afb84aa8b2fbae Apalache Def1Recursive Exists False Passed
eb301ccfb8e602582016182acbbb81e7f48a56d9 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Exists True Passed
0926f5562d9edc3b3abe4c84d5c2bbbbc8c42ce7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Exists False Passed
0a47c83c6d3c2dd6fbc68210e76f96ef1554a002 Apalache Extends Exists True Passed
423373703102bb2454985190a03855d721be2114 Apalache Extends Exists False Passed
9af42c39df03466c933f987c58bb5403d9921e5a Apalache ExtendsInDifferentFolder Exists True Passed
d3218685c0f422df16f2bbba86a6e8bb49d2295c Apalache ExtendsInDifferentFolder Exists False Passed
1c2790181ecba2cf49b0a6eab1631ae7d062950b Apalache Variable Exists True Passed
b7f65231bec3bf99beaa1818ef07322b803aa7e4 Apalache Variable Exists False Passed
812a9d0ac12ed919be8b4094eb67ff89a74ae4d2 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Exists True Passed
25cf3ca0f4998a78e330086cdfe6c0cdef714f17 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Exists False Passed
2b8e71360ffc1421c50b4c63a3487ed8a7553062 Apalache Constant Exists True Passed
72576b9a55b71d004e33dae885041afaed092d19 Apalache Constant Exists False Passed
83aaf308c8c1fa630b334739a3f65b657a349327 Apalache ConstantRank1 Exists True Passed
1a9b4c2d0e042bc8ddb84271d783173d600e0d78 Apalache ConstantRank1 Exists False Passed
04f159752747c08d7e0727c822f63a3265c8f01c Apalache Instance Exists True Passed
0f23a4d3bba8f3003d962c8c376ff4a64cd70d6e Apalache Instance Exists False Passed
b1762bd7ebf25f91a8f34d569cbdabbd42a7d878 Apalache InstanceWith Exists True Passed
a4270fafac8478aaaa4b0abc08db049a5a94220a Apalache InstanceWith Exists False Passed
84cfebc977ed15fd1d9579efe46645c0eddfdbc2 Apalache InstanceNamed Exists True Passed
960ac43eb830b3000e398fbbda5877e21e296fcd Apalache InstanceNamed Exists False Passed
62588c3466e7a792b2e3906a2a41c005e33e157b Apalache InstanceNamedWith Exists True Passed
af2937ecba65c762c622052403fe711749df6a2a Apalache InstanceNamedWith Exists False Passed
c70d4ad27dfe62690f4051e7302bfc4529423f2f Apalache InstanceInFolder Exists True Passed
8bf16afa4a6d7857b1e2bbc1157c3fd07467762a Apalache InstanceInFolder Exists False Passed
34d187b19eb18e6f7e14cd16014eb9809236e3d4 Apalache InstanceWithInFolder Exists True Passed
ca5bec5bc2e25dbe655519da0e89ea5a25d96f3e Apalache InstanceWithInFolder Exists False Passed
799a7d3983731cc982776441ab53d19e7b2c292e Apalache InstanceNamedInFolder Exists True Passed
d3082d9ff7933dde83e49474e75b4f51ba076c02 Apalache InstanceNamedInFolder Exists False Passed
2f0dcc7e967480e5e17c0e7d10f8896f758b4081 Apalache InstanceNamedWithInFolder Exists True Passed
ca77ec52133494836aaf3fcf4fa8f765cbdf414e Apalache InstanceNamedWithInFolder Exists False Passed
59b8c1b98c55d31b0b5769fab978d360809101b7 Apalache Enabled Exists True Passed
8d4a467079c9e833198b228ed7d3ea09d19faaaf Apalache Enabled Exists False Passed
4dbffcce3b3329b78ac3f85a9f6d37fad61bc875 Apalache Assume Exists True Passed
f595523a45eb0583dc0c44528d9637c037672828 Apalache Assume Exists False Passed
f668dd3ea8a96a4767ee8e1191f9d0225590adcc Apalache AssumeNamed Exists True Passed
fda9d08c98e9c6c6c8490dd7a44692f04d0593ab Apalache AssumeNamed Exists False Passed
1c15a66f277e42aa838b9487b12a49b4c0437648 Apalache Lambda Exists True Passed
dfd76f2a8d6583bbca288d3899cc11993ca62ffd Apalache Lambda Exists False Passed
dd8f0121f919336b8810c2d5c721f3e0c142892f Apalache IfCond Exists True Passed
ec93584919db49c5ac98183fdad4eb257f1b1a45 Apalache IfCond Exists False Passed
fb6f718803f912148eb1d392d28bf71e64d91b10 Apalache IfThen Exists True Passed
61fafc0ad631ae658edcb082d08bbbbf47c01415 Apalache IfThen Exists False Passed
e73ac132d11c1db2e4b73d56da435e3941d51515 Apalache IfElse Exists True Passed
d3bebae73f36834d51ff9b36f46af2c2f8f294f2 Apalache IfElse Exists False Passed
a3dc6f4e5c0ce209b268896de09141016a614c27 Apalache Unchanged Exists True Passed
be4dba9edb3d94702ce677095eedf378c7dc0ae3 Apalache Unchanged Exists False Passed
07d89faf7f6dce89a704fd55bf9c47d175d171a0 Apalache Equivalence Exists True Passed
de2ba4fa641e5a457e6ba4215abcb11543f6b2b7 Apalache Equivalence Exists False Passed
630f0b23f8ee31060c382b77b1bdf121c7d170eb TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Exists True Passed
60225ed731f52901b9cbd7e6875ab0994e6715ff TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Exists False Passed
bc8f8555b111ac116d64ecec262ffe983e700d6b TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Exists True Passed
f5a1b4a1bf7cca773e0cd6e6ef2f45d83515960a TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Exists False Passed
f665a0b1ab700a5b31f777c9a65fa0e8d2efc0a9 Apalache BagBagIn Exists True Passed
6d7985ce99cab1f9b198f25ecd85cc7d4577850b Apalache BagBagIn Exists False Passed
b43eb8152fd3ea55ac44d95c0f08761f59dabce9 Apalache BagCopiesIn Exists True Passed
92787ffd3eeac7ba3337057ab4bb0a51e74f97cb Apalache BagCopiesIn Exists False Passed
0a82954757914548879b9ea29ffc9c7b89614ab7 Apalache SeqAppend Exists True Passed
02c7a8eb9ec491c30096321f455d020a53cde63a Apalache SeqAppend Exists False Passed