Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
c2b07476f88b5d91b985b93efb74059f1514fc64 Apalache And SubsetEq True Passed
d7e0b3939d20b41a19ecd2fd95740d3f51fddb1d Apalache And SubsetEq False Passed
468b08c81ef3e9ea45411bd83957fd833c85505f TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine SubsetEq True Passed
e914847c456ca3d7e2ac11f092bab3119eedd11e TLC with reduction strategy:
  • Case Feature:
    /\ A
    /\ B
    == (A /\ B)
AndMultiLine SubsetEq False Passed
6258dfe4a8755b592e95df1533819bb148b8c4e4 Apalache Imply SubsetEq True Passed
30b8d27d5ae889357caf16af577e2639a1d3ffb1 Apalache Imply SubsetEq False Passed
03a640d76c7722ef979ed4499846722132aaf550 Apalache Not SubsetEq True Passed
962eaf3f81ad12faaf9e3b760ba90e7964e2af77 Apalache Not SubsetEq False Passed
4c28b26bcfff72b0a8e572b1cfbfdc66797d671f TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or SubsetEq True Passed
766f3dd1ab4e2ed643e6ec250be602bca89caa6c TLC with reduction strategy:
  • Case Feature: A \/ B == ~(~A /\ ~B)
Or SubsetEq False Passed
fa71cf9440a65578f75e936f08f2a70223c3af2e TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine SubsetEq True Passed
62b0d4c91c74a9f7b4f855b5d6d3210ab9da8363 TLC with reduction strategy:
  • Case Feature:
    \/ A
    \/ B
    == (A \/ B)
OrMultiLine SubsetEq False Passed
68e9809ad348a1c53c2a4241d5d50fd02443056e Apalache AndProp SubsetEq True Passed
5321abd1d5835a94dc5a7a0950b9fdd710c0c91e Apalache AndProp SubsetEq False Passed
aa084976132c09075335eee320a7e8b1d1c3d9cf Apalache Boxed SubsetEq True Passed
039feda9b875ebcf1684f699d36a6d537e8ac28e Apalache Boxed SubsetEq False Passed
0abba89e5e10558101e8f811ed19355ad92689dc Apalache Eq SubsetEq True Passed
cc15e1de5aef65266e07a310c4f65d32f311074d Apalache Eq SubsetEq False Passed
dda4409df0bf2decda25bf5a61a58775bdba7244 Apalache Ne SubsetEq True Passed
b0eea226c8a0913ec79b96949f1328c3df4676a7 Apalache Ne SubsetEq False Passed
daa68428b7b23a665da6bb6342fb194b7a092ccc Apalache Let SubsetEq True Passed
8e46b29ec711e83a6edbf6dfa04ab71a3a4a3bc3 Apalache Let SubsetEq False Passed
97aa34fd492dd0514b6239ba9555225b43efa27f Apalache Set0 SubsetEq True Passed
c591d6e9fdfeb24dd7fce0f5de3c066a65c8fef8 Apalache Set0 SubsetEq False Passed
fec567fcd7dcbb8b7d1eafc5b96bee1ee29ed80d Apalache Set1 SubsetEq True Passed
b69ed043e998e806e15bf37a03404ec989d597ea Apalache Set1 SubsetEq False Passed
a0e9bb7750a9bfc392d95abbc94f5052a2ab023d Apalache Set2 SubsetEq True Passed
ead598d05059d5bab6068558f66c2b7692fa1d67 Apalache Set2 SubsetEq False Passed
2868a62b892561d4b4b6020dc8fa5e800a25821c Apalache Fun SubsetEq True Passed
5abf0fa0e017afeef0ba796509e58a9ae605bfef Apalache Fun SubsetEq False Passed
73f89f6b570cf951f19dd203b206903305b91b78 Apalache In SubsetEq True Passed
c3d6cea1346664fc1fc0382612023ea8d00439ba Apalache In SubsetEq False Passed
2b4f71a53302ee0d745acdb86997af1b30ebe75b Apalache NotIn SubsetEq True Passed
8dc7cfbef89d978d9704dfe217a615857608752f Apalache NotIn SubsetEq False Passed
75a4a11f4d1a8bb9b9bd497066e058a52f364de2 Apalache Exists SubsetEq True Passed
258744b787bbc7f7506ceef1751d2b556268050b Apalache Exists SubsetEq False Passed
560436d5c99edbc9867f4f3d8929f14c16c1020b Apalache Forall SubsetEq True Passed
0415c092621a3357e2bf45da854a675c75ec2a3c Apalache Forall SubsetEq False Passed
efcbb86d8e825035422ef00dabb32e954a932280 Apalache Choose SubsetEq 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.
c2e7701c74244b41eb1004ddb9a7e058a47a0c1a Apalache Choose SubsetEq 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.
7d5d2fb640c48b003cc86759c20589f2e9151687 Apalache Record SubsetEq True Passed
cb18bb6bd8ee0a649d9f0ecf47bd952b81d1aa29 Apalache Record SubsetEq False Passed
4611a026b2d4ebe6312d0ecc7b78ab189375b5d9 Apalache Tuple SubsetEq True Passed
b2562641e8ca5dfe14df8d27c21636daa22f863c Apalache Tuple SubsetEq False Passed
6d4df3c15d6f16bc9338a83da8d5b116cf7f1a36 Apalache FunApp SubsetEq True Passed
5017a5f4cb15b1062303bce83f8d1a607b4c4d8a Apalache FunApp SubsetEq False Passed
9d52b7eeb408ac9c77bf16585db1b30313a24199 Apalache Except1Fun SubsetEq True Passed
a830ed8fb7b9bf957951fe6dd4d32a6edc4ede68 Apalache Except1Fun SubsetEq False Passed
c86659c1728e8d22e995873587604e18006a4017 TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt SubsetEq True Passed
06c780a58af3045a65961a295fa851f9991e5a9f TLC with reduction strategy:
  • Case Feature: @ is reduced to F[arg]
Except1FunWithAt SubsetEq False Passed
61ebd580b8c840279b696e63f3c4eeffc03849f4 Apalache Except1Rec SubsetEq True Passed
da403a25e38ee00a8db839ec66fbc9784b7852ac Apalache Except1Rec SubsetEq False Passed
03928a7d98f416bcc52f2234716136af8181d859 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SubsetEq True Passed
745e2864ba7f85c5aa402ee63643da424513e4c9 TLC with reduction strategy:
  • Case Feature: @ is reduced to F.arg
Except1RecWithAt SubsetEq False Passed
30d55acd9cf0ed349e39b1dd01d498f0dbc94a77 Apalache Except2Fun SubsetEq True Passed
9f861880b81e4e76dd1ee48e59dda780cd51db2f Apalache Except2Fun SubsetEq False Passed
05fe350874feca2135c971d0502e010daa8f085d Apalache Prime SubsetEq True Passed
ad3d502fb7e0c6527054b9078f4e4746ba079243 Apalache Prime SubsetEq False Passed
a80c8590f3e3db87625e0fa99aab4e21b4d3bda9 Apalache DefFun SubsetEq True Passed
07e22fd6bd16b9e8f9c2701b7ec85b29d1f94388 Apalache DefFun SubsetEq False Passed
f9e33b17c46e84d2d2534e0c281c2d7f7d3e3d23 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SubsetEq True Passed
7cba8823e8cc2da70ec97d9c1ee6380149de2a42 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFun SubsetEq False Passed
fc98a6e17a2c0ef25cbe9c8004881d80af8e7784 Apalache DefFunRecursive SubsetEq True Passed
f72e67d0debd4bcc4f5e0ee2f224400ff9897b79 Apalache DefFunRecursive SubsetEq False Passed
334094e853d8240f092b30d0b5ee61e2d9077aff TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SubsetEq True Passed
0a9f3c9ed2ebf74569c29c29fdf9d5a9d899edb7 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDefFunRecursive SubsetEq False Passed
8949c932947aa837b246cf524660bcd9555c369e Apalache Def0 SubsetEq True Passed
e27b4f1d6d532473ffaeebb3011835966e670a4c Apalache Def0 SubsetEq False Passed
efb1763a7190591c70d89e79e116f42a40b8b798 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SubsetEq True Passed
96f66918403db3cf22146a3172c1511bd7d9f912 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef0 SubsetEq False Passed
fcff809e0e0261e6bbf5811c8630237b99a36a86 Apalache Def1 SubsetEq True Passed
9390a4f961de0be59055656c9fc91492f360c487 Apalache Def1 SubsetEq False Passed
ee1c53143a8029593f3df12ed0221e5a0b62fca3 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SubsetEq True Passed
88b569803c1bda88093843d7a1a38a4ad7a8a957 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1 SubsetEq False Passed
0b7b47bfc760086539f2b75e1b35dc31da2dd2b7 Apalache Def2 SubsetEq True Passed
ade048e30d16eb694211b7239fb2777c378550a2 Apalache Def2 SubsetEq False Passed
e98772d34b75c00102d32ce1e11b8d4c42ef466c TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SubsetEq True Passed
c602e95afb65070372f8fa5100d420c9ef747c2b TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef2 SubsetEq False Passed
10d34e8ac77a2d48cebc6c502e3c451172e59ddd Apalache Def1Recursive SubsetEq True Passed
b6336fa9f27ea140e1b4a2ed40401fda1ce59c19 Apalache Def1Recursive SubsetEq False Passed
eb9e79071ff8f654ab89584c49451f757ef360d8 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SubsetEq True Passed
4d6497ba28223bd4ac4bc664036456c61a28e011 TLC with reduction strategy:
  • Case Feature: LET definitions are reduced to global definitions
LetDef1Recursive SubsetEq False Passed
9adee1aa885cac38fbe8ee0f009e542d191c2fe6 Apalache Extends SubsetEq True Passed
1f49285e532031a60a80eb3072a1af443129ee64 Apalache Extends SubsetEq False Passed
60a6fd79c5553e2a8353717c2fd2f5f67d914e8c Apalache ExtendsInDifferentFolder SubsetEq True Passed
62972b8fb0f490b2acd9e588523e0fa71ee1c43f Apalache ExtendsInDifferentFolder SubsetEq False Passed
29d425169cd50e7c5ab59bb0ceb4e26acfff825d Apalache Variable SubsetEq True Passed
e750757304eb5003425923b9a189f55c3f2f00a6 Apalache Variable SubsetEq False Passed
986be3e9fe3d35921ee5a86e5ab60dbf260bbbf5 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude SubsetEq True Passed
a762fadc313c2acce5357ec9526edce0f575b6e6 TLC with reduction strategy:
  • Case Feature: Model with VIEW is reduced to the same model without VIEW: VIEW must not change TLC behavior
VariableViewExclude SubsetEq False Passed
c7d010bc39d687b5e54d80093ec35e0b9a8fcfe2 Apalache Constant SubsetEq True Passed
d37a36590b8d62d8bc00fb299ef777a0de66f8bb Apalache Constant SubsetEq False Passed
999637f394812dd97a54cd2a5840dad65d848f8f Apalache ConstantRank1 SubsetEq True Passed
64a9b363a11fab3b481ec76b73bd2965074b9184 Apalache ConstantRank1 SubsetEq False Passed
75b7069cd90f4544db24467992cc3dfe7d758dae Apalache Instance SubsetEq True Passed
5a8c25e223a6d56ca9f3245379136cd97f1b54d6 Apalache Instance SubsetEq False Passed
62dae35b17c6dea31b0998f1774b803862a8cea6 Apalache InstanceWith SubsetEq True Passed
40edbd152ed883211a7039cd98f510be752b8eda Apalache InstanceWith SubsetEq False Passed
66d54f41f44ab4bf16f59faa36ea302c46276e77 Apalache InstanceNamed SubsetEq True Passed
e0187e8694c71b7b3218d2e217744c14c8c2769a Apalache InstanceNamed SubsetEq False Passed
69bc46b6bd2a4f71a46f36989edb258419c2ffed Apalache InstanceNamedWith SubsetEq True Passed
abd4937179dda3adf507d83962ced00642a2cac4 Apalache InstanceNamedWith SubsetEq False Passed
5858b6f285e5c81c7dec7e384e6c5548178c6bcd Apalache InstanceInFolder SubsetEq True Passed
7c996a6b003b2a4837bc28e06f7c4a36236e2643 Apalache InstanceInFolder SubsetEq False Passed
cd44d2732f3f92ab78514992f2bb9ca48ee0fee9 Apalache InstanceWithInFolder SubsetEq True Passed
09f922de8eafac7ae30768c1638ceea58da22da6 Apalache InstanceWithInFolder SubsetEq False Passed
4fd0eff534c9832ac6055769c0bbb5ee2ae0209e Apalache InstanceNamedInFolder SubsetEq True Passed
2c33d5d63e11a38f71d0b452f493126c7e0ce88b Apalache InstanceNamedInFolder SubsetEq False Passed
d06877a58cc350d4969a417b648ec00362b86b70 Apalache InstanceNamedWithInFolder SubsetEq True Passed
fc2d667859f60fcff7f1a33cae1b66081e7b9fb1 Apalache InstanceNamedWithInFolder SubsetEq False Passed
ebdac084d2b75a3cbe114ff589e159127c590580 Apalache Enabled SubsetEq True Passed
0730291349ce5aedbbc410e9d476e32bbc601c00 Apalache Enabled SubsetEq False Passed
45dd31ed60b43a5c79a36332d8e21394d0bda955 Apalache Assume SubsetEq True Passed
89a13a5014ddc948e2be7537746b23a8c0747b47 Apalache Assume SubsetEq False Passed
bdc8b909660018e50d629facb6cf2b592d9c604e Apalache AssumeNamed SubsetEq True Passed
a42a1bc4dd32e43fba18213ad4fafaa9706f3f2e Apalache AssumeNamed SubsetEq False Passed
810e4cd5b6144041cacbed11d236e25c8aab94ee Apalache Lambda SubsetEq True Passed
b88c56bab7c072e947cb6b764adb0c76d673a401 Apalache Lambda SubsetEq False Passed
4b46a6a4c366a14e731937fc7e75f5ee89a66b9a Apalache IfCond SubsetEq True Passed
a8709300b4c78327c0485e55ea5d44e034a66926 Apalache IfCond SubsetEq False Passed
aa4acbe020bbcc018ea3c98ea43b889a42677914 Apalache IfThen SubsetEq True Passed
b4b04f78f7f8ecd8dfd7e707c7cdc50158eca505 Apalache IfThen SubsetEq False Passed
527bb61865a3d5125388f10cc51e9741504915cc Apalache IfElse SubsetEq True Passed
6b6498a0d0ac2e2c4f116c920fc552bf90903c8c Apalache IfElse SubsetEq False Passed
5c22900208f11ded0b3612bbdbbf4133578f81da Apalache Unchanged SubsetEq True Passed
e64115a60d9efd0732b29639d370d946f3a8893a Apalache Unchanged SubsetEq False Passed
99b3766ccb2bb736ead0c99af168cc3d9e914c48 Apalache Equivalence SubsetEq True Passed
2505d706a0411efe02631fb5d72e1486235520b3 Apalache Equivalence SubsetEq False Passed
7d5c444841bb6093a6561a8cb4df11cebf56170d TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SubsetEq True Passed
526f4e0649e7679957807b9f28e759d21e4b4629 TLC with reduction strategy:
  • Case Feature: x :> y is replaced with equivalent [u \in {x} |-> y]
TlcSingletonFun SubsetEq False Passed
2e5e3229ee1e7c01e181264b9586442885d62d9d TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SubsetEq True Passed
3ca5b623a2db08e305e2269f2452d71dcc97f4d6 TLC with reduction strategy:
  • Case Feature: TLCEval(expr) is reduced to just expr
TlcEval SubsetEq False Passed
977a39be4f1846f434f2e0bc612c51fcab821770 Apalache BagBagIn SubsetEq True Passed
e60294d7972a593849e86fd901ca4b1f6f5188bd Apalache BagBagIn SubsetEq False Passed
51e2a3bf3f83336a838d5b8e28909c4e9750bcce Apalache BagCopiesIn SubsetEq True Passed
5e6fb77fa9d409153f881d10e79bfc16c5547075 Apalache BagCopiesIn SubsetEq False Passed
2c9cbf345e9f8639af53c41f94937ce759e1a8dc Apalache SeqAppend SubsetEq True Passed
8500e801f0a0a9898ea59b91df4cc0a0a47bad5b Apalache SeqAppend SubsetEq False Passed