Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c7aa1ffbc51a3a92153bd6f7d11f35282b7b57e8 Apalache Eq Set2 True Passed
865fa781444739a80b044344544a1db182f8c50c Apalache Eq Set2 False Passed
5538b6f0beb7d412ab09db158597fb2aa56a16ae Apalache Ne Set2 True Passed
9807923866f6ffeb28a8a724d6e1d4d703656488 Apalache Ne Set2 False Passed
bb60025931e9e5e07634bd3983d02ef77dc1dea0 Apalache Let Set2 True Passed
016b357f030cc6dd41907c8023313e0318c50955 Apalache Let Set2 False Passed
402c3eaf82f1221421935f164a868f9a0c09202a Apalache Set0 Set2 True Passed
ea977177471455ad26781c7fa0d0426b8e64efe3 Apalache Set0 Set2 False Passed
294b007f12ed3df7e15a62d4b8b2ecbe109a9c58 Apalache Set1 Set2 True Passed
b1af68601a2a117614915238863db72d8bde20f6 Apalache Set1 Set2 False Passed
424ab54c3792f3dbb573a3e0f86bdc07b0263ce6 Apalache Set2 Set2 True Passed
89ffcc238b6073552d6bba98dd76f2a8235b1fa1 Apalache Set2 Set2 False Passed
2cf6cf84fc762455433b31c8915dadfd3388943a Apalache Fun Set2 True Passed
768a99a3ee2ec91b8e03be1019b530889b656439 Apalache Fun Set2 False Passed
0baff7c1b4603055affee8e088df05829ab730b2 Apalache In Set2 True Passed
b4e31ed97fcb3cc62be56c6154796732c28e20d5 Apalache In Set2 False Passed
8f1a81bc8c5209f0c3b9410f12d72c07737ba67a Apalache NotIn Set2 True Passed
ccb59e19ad00d3a5249ae3c7ae7ecf57f9a95faf Apalache NotIn Set2 False Passed
9282ccc70d1f9f6f2b303457776de018f2322d6b Apalache Record Set2 True Passed
a8b595a443f2b3199702955e35c0ab2b90f2da93 Apalache Record Set2 False Passed
50d76a7ffb386dba2f7c6e0661680114768d2a5d Apalache Tuple Set2 True Passed
58d62a5b86a27abadd571af734e6f5cd614135aa Apalache Tuple Set2 False Passed
55a16b965fa57846985aa2e4d1fe31f8d34f58b8 Apalache FunApp Set2 True Passed
a4453836f6f4b080cd87b17e75bb85676684ffa6 Apalache FunApp Set2 False Passed
1ef88b6d80a58c4433d8c752322575a7ef52b391 Apalache Except1Fun Set2 True Passed
8252e897684d7037cda6d4376f6e6bb41e19b6cf Apalache Except1Fun Set2 False Passed
2dc142d868b52142de915db0b2316460823bd196 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Set2 True Passed
93883f3d5e1bfed875f76de0bf1582323eff697c TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt Set2 False Passed
51893b3886b57eb473d4e95254727fac5acc74cc Apalache Except1Rec Set2 True Passed
ba96bdfa28a81b9ecbea3ab0c9a7b5091146c6c6 Apalache Except1Rec Set2 False Passed
f163c367655f22408de2f7c5b76b02a72308278b TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set2 True Passed
4696b1867c1ccb09c189b5163ed57d820024ecaa TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt Set2 False Passed
42c5d06a9a22523df67423c4760c1e454d189c4e Apalache Except2Fun Set2 True Passed
715c5b9c3ea80f11a4ce094ceb2a275cc639ef80 Apalache Except2Fun Set2 False Passed
85a797f21bcaf5cdaa3b3bbdd48373e5ea50d1a9 Apalache Prime Set2 True Passed
45808ab7ca15ddf89da9835f67d9fc08aa4ff27d Apalache Prime Set2 False Passed
0d41736bbe1f9b94c23892d2757503ef0f611921 Apalache DefFun Set2 True Passed
afa43d95c08839e39ce1d71a8f1d3bb015b7f1c0 Apalache DefFun Set2 False Passed
ab4865f1c856ffd737bee2a649457706c20bb497 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set2 True Passed
6fb4d752e0db44a6771f50d1fac510148ed65750 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun Set2 False Passed
6037a69a13c8cd5d00a1708d80126853d7bb4958 Apalache DefFunRecursive Set2 True Passed
7a221620e089952895fb1b42b40a77db1ccf8d94 Apalache DefFunRecursive Set2 False Passed
0b011a338e2d8e7f178b463d04e6531a344ed50f TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set2 True Passed
ec02b4ad0621a689541729d26b816f806afbdfdd TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive Set2 False Passed
04ab5030227aa07512503178cb6965460499e57e Apalache Def0 Set2 True Passed
3abe61b341ef9a688d29b1623a0dff9d1c849ffa Apalache Def0 Set2 False Passed
5b64e2c83ab900cf6910ffcb0b623b315e644948 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set2 True Passed
b27ef13055407ca9bf18440486575e6020bc3d79 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 Set2 False Passed
c676b62faa75596d351782856ca25d571950afdf Apalache Def1 Set2 True Passed
e431d12862eb5d74d3d71a00f43e12bfdef3a309 Apalache Def1 Set2 False Passed
11b839e20e8e00b9754470aa189fa420b64951f0 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set2 True Passed
163070e978a06b35bd0a3562cd881163199672d5 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 Set2 False Passed
ccfa875b7e0860e624d426ae33c67e5b6a230ddc Apalache Def2 Set2 True Passed
d8662c476d529de05eca6b9cc2a000007350b921 Apalache Def2 Set2 False Passed
b9dc496ec39a9df0f49b6dcd69ac7c4e55674485 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set2 True Passed
a1fa45bc75656739a1c0c8066826170d0f4b2f0c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 Set2 False Passed
a3eed04f3cf08e82225e6ba461a72d7d304ccb4d Apalache Def1Recursive Set2 True Passed
dce87082448bad2395bae7dcf79b452aabf7b784 Apalache Def1Recursive Set2 False Passed
9171ab6dc630406d3430a08efd65023e54dc597a TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set2 True Passed
750a3ca21679a74c5964a3bec229e323f3cec4b1 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive Set2 False Passed
5e58fbca4ab3db3d3cf322a56ac9f4b531020b33 Apalache Extends Set2 True Passed
2237141ba951d1fdb99969226b6fe5d8c88cefcc Apalache Extends Set2 False Passed
0f17a273ee052b69c823599bd700dc8a8a9e5175 Apalache ExtendsInDifferentFolder Set2 True Passed
29538b60e766a86e5002cad51e06e1679d700f9b Apalache ExtendsInDifferentFolder Set2 False Passed
ee1972068799f60b7c0e62eec03e1e291f3b6d53 Apalache Variable Set2 True Passed
2fb39c6ac66c165c0b3eb059e726250b0e81bca5 Apalache Variable Set2 False Passed
174318b15148038887e242355ab8e807eea282f6 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Set2 True Passed
6dab1d30753288cfa5a0da3c51f61ef219399435 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude Set2 False Passed
46652d6017722908a269fd6273c67185c0623722 Apalache Constant Set2 True Passed
13f5ec9b0125028e75391dc202eb646a062ebc34 Apalache Constant Set2 False Passed
6bb75e8c7d3cec138c32ea785cdd50cd77e6882a Apalache ConstantRank1 Set2 True Passed
38deba176cdbf83bb6d6ae6f844b231fa4bbb23d Apalache ConstantRank1 Set2 False Passed
275eafa860654ab4cf8e44eec2126f3965cd6d0d Apalache Instance Set2 True Passed
c4924d71d3c1073598ee780584896f913bca6b1c Apalache Instance Set2 False Passed
50c4b84fbb5f4df1b222547b87aa8e401c45ebbf Apalache InstanceWith Set2 True Passed
66d2c5d7332524e241f7e572264480d34351d2f3 Apalache InstanceWith Set2 False Passed
252ae88a89376d839fb4339c7c08461a6389c4d7 Apalache InstanceNamed Set2 True Passed
cb6e6de01fbd51ba3b7b536175ec41f462f90cbe Apalache InstanceNamed Set2 False Passed
1c83206a98d2a96d71867992901db5e8068fd1e7 Apalache InstanceNamedWith Set2 True Passed
911fb60d2fbdacd15da4ce239975cea6cb312ee6 Apalache InstanceNamedWith Set2 False Passed
7e1d7c034fd8f18d99a44c8805bafae727191738 Apalache InstanceInFolder Set2 True Passed
2fc9a304668272d4939053bfd885a534e2de3410 Apalache InstanceInFolder Set2 False Passed
9958cb29f87aa4021a4fc44ce17f4f3636c93d2a Apalache InstanceWithInFolder Set2 True Passed
bdd8058ebfea47f92b595f941b351708caec66e3 Apalache InstanceWithInFolder Set2 False Passed
6d22d0bf4c40e71d96dd5e2cf5c2bbe68d858b1a Apalache InstanceNamedInFolder Set2 True Passed
d526fdad1b596b5383ac97069c9a1b8d5bcc8e21 Apalache InstanceNamedInFolder Set2 False Passed
fe71850937e6e692358f1a46ab4205f1bbc52d0a Apalache InstanceNamedWithInFolder Set2 True Passed
b7303ea0f093b5e32754cd5a1aa7568dd46936e4 Apalache InstanceNamedWithInFolder Set2 False Passed
b052856fdc1197c0286c38af0ab2dd9b4b0d9069 Apalache Lambda Set2 True Passed
97d58d460bec5e3095423f307cdb356c01e4b86f Apalache Lambda Set2 False Passed
85d648d3ef42225dee2419b2330e07d2170a626e Apalache Cross2 Set2 True Passed
0a2b8133e1e9192ae03abf84ebe9854ff263d605 Apalache Cross2 Set2 False Passed
fe6dc76f018fc4f8b90494dd415559dfb3b51c52 Apalache Cross3 Set2 True Passed
7c4c0e83a7fbb635245aa978e278b2202c4ead9e Apalache Cross3 Set2 False Passed
30abbd6b16901eea121f473e53b5daed372c7298 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 Set2 True Passed
8cc03b183a07944d744174ff06434418246cf6d4 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 Set2 False Passed
92c8c10ea8e35b69f600562943e981b9b8ea8288 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 Set2 True Passed
4fd273bf7d5fbb4bd951aef3106d8ef5eb8dcd19 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 Set2 False Passed
ef24f6946fa0723be11121e072254eb6901a8c3c Apalache SetDiff Set2 True Passed
0bdec915cbd37249ecf4f227642fd9271b360905 Apalache SetDiff Set2 False Passed
e782231b3783f1f0cbb0362d6f6557cfaaa6dc16 Apalache SetUnion Set2 True Passed
6044bab7fd7b8c6dce57880102a929cc12511f88 Apalache SetUnion Set2 False Passed
e17e6e01642595b331fd1f77fd9e5de9dd65cb18 Apalache SetIntersect Set2 True Passed
99e3d9ad4a8858d1e927c5ffd226eb7393dac28d Apalache SetIntersect Set2 False Passed
2d86faaf48756bfefa2bf8a104d9d58c24f3525a Apalache SubsetEq Set2 True Passed
a321fe1dd9147eb0cbf9e7468519c4fdf113bc4c Apalache SubsetEq Set2 False Passed
15404a3d9f37d76d4507fc871bcea245e7a72614 Apalache IfThen Set2 True Passed
2d8f7e4df2c95bd6879a18765e4fb3e9f8ac2f91 Apalache IfThen Set2 False Passed
8e6cc3e8790ec3517faf62472432c5c7fd1fb736 Apalache IfElse Set2 True Passed
9c1ec197763536493fe203c9d3af264d7fa520df Apalache IfElse Set2 False Passed
1f3e714ee9a86aa4fb163837cab9b13d28a14e20 Apalache Subset Set2 True Passed
68a137c89c133547d3cb0dde5ba712b7d34843b1 Apalache Subset Set2 False Passed
67ed4b296dceedae1eab159b515325d8327d4b52 Apalache Union Set2 True Passed
65ad2c4a02f201ee4ca77a535caaa6711bf88f33 Apalache Union Set2 False Passed
760ac35a9218a12b065fdcccb2c3381bb042f40c Apalache Unchanged Set2 True Passed
586160080189793d3323b4814ca5808f22047758 Apalache Unchanged Set2 False Passed
c553224269f36340be8ff0add9b1e1a8f5eb4209 Apalache SeqSeq Set2 True Passed
9fc5ecebc244abaf10dfa28077f1a1cdf3668bd8 Apalache SeqSeq Set2 False Passed
a9473a8e93eba52d8452315b1173c6aa620e0b7b TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set2 True Passed
64adecbc09e71d882e35afaaecf9cf8675f1961c TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun Set2 False Passed
2b64300a43962ecf1f927a65760c67a5a1771d58 TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set2 True Passed
ece313d99b47d268ad0fc9958744f392d9ea117d TLC with reduction strategy:
  • Case Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
TlcPermuteFun Set2 False Passed
f4bcb7b3acd4754cf4b8b87397ac2dd86c778866 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set2 True Passed
6ad601a110bf85c61148f0640a21ba1be94e08fb TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval Set2 False Passed
a09d5d19c86b4502221ac86075c35568c717261c Apalache BagSetToBag Set2 True Passed
9e5312599e30412ebe42eecd3cf0daef9e0db837 Apalache BagSetToBag Set2 False Passed
d909b1d86207d7d9e112ebd18be28e315a7b0c00 Apalache BagBagIn Set2 True Passed
fda019148619539e565ce38d30d86dd6789b15b3 Apalache BagBagIn Set2 False Passed
79668250b8ac79f6ef785994b82da5228caff788 Apalache BagCopiesIn Set2 True Passed
3d53272c51c6b1931122621f9c4c5c498c113b94 Apalache BagCopiesIn Set2 False Passed
2cb05cd6b11db355e725e1d47d0fb7c11ca0478c Apalache BagBagUnion Set2 True Passed
f5c4c9af99d3612a230c6bb0a6e6601a9036c0b0 Apalache BagBagUnion Set2 False Passed
0bf56d634f507f062fdd6beffd59bc1807502d22 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 Set2 True Passed
5bc256c1a6657e00d80d42eaec28369fda13d56e 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 Set2 False Passed
6865e03554998a943227589283839b241a09befc Apalache FiniteSetsCardinality Set2 True Passed
59b1989ba548b10aaed4b61190296837a6550d09 Apalache FiniteSetsCardinality Set2 False Passed
1eca01673111ba69ad04be7cbfa479283824cba7 Apalache SeqAppend Set2 True Passed
b61108026eb379106586099c855d0a2eb5b42063 Apalache SeqAppend Set2 False Passed