Index


  • Introduction

  • Skipped feature combinations
  • Failed test cases
  • Tests by feature combinations
  • SYMMETRY tests
  • Tests under anomalous conditions

  • Tests by feature combinations: -workers 2
  • SYMMETRY tests: -workers 2

  • Tests by feature combinations: -workers auto
  • SYMMETRY tests: -workers auto

Tests by case feature SetDiff; CLI Option: -workers 1

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
60d9e459ec4681b8299e4fd48cc5742a2df0762d TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SetDiff OneLineComment True Passed
  • Model Under Test
  • Equivalent Model
f3cfd137c4b4a8143c56097436196b023a56565e TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SetDiff OneLineComment False Passed
  • Model Under Test
  • Equivalent Model
cb6b50e3a0d3b19619f6cbfff4c4d47d7205fac4 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SetDiff MultiLineComment True Passed
  • Model Under Test
  • Equivalent Model
dca270a24e13d19fe53f829443ccc1d1ba687f20 TLC with reduction strategy:
  • Plug Feature: Replace spec with the same without comments
SetDiff MultiLineComment False Passed
  • Model Under Test
  • Equivalent Model
5dc2821b1998ed5abb291892ee6be213571bfd05 Apalache SetDiff BoolSet True Passed
  • Model Under Test
  • Equivalent Model
0a5ec998b4a0d19e18bcadef3b778204d0badd0f Apalache SetDiff BoolSet False Passed
  • Model Under Test
  • Equivalent Model
5cd0d00aac8c6c3eb78379bcb50caf862b3d4aae Apalache SetDiff Let True Passed
  • Model Under Test
  • Equivalent Model
29673f1eae00123d768df6b4c88bd2d70aadf487 Apalache SetDiff Let False Passed
  • Model Under Test
  • Equivalent Model
bb8ad8da01655c3203b1e8e00c477fb2332bac8e Apalache SetDiff SetEmpty True Passed
  • Model Under Test
  • Equivalent Model
1af53ce965a0fdbe314dc9840799afe6f61c3983 Apalache SetDiff SetEmpty False Passed
  • Model Under Test
  • Equivalent Model
0b8aec9e34e98a278a42d22c2e56ef0e86156b19 Apalache SetDiff Set0 True Passed
  • Model Under Test
  • Equivalent Model
ea2dcf4cad53060cdc1b55d4dda28ed6ef99466d Apalache SetDiff Set0 False Passed
  • Model Under Test
  • Equivalent Model
0bce217cb7b8f6ea7de2de10e9a280681eba9020 Apalache SetDiff Set1 True Passed
  • Model Under Test
  • Equivalent Model
68ab78d97fa901704f3ff3dcab8d69aa5b16fd33 Apalache SetDiff Set1 False Passed
  • Model Under Test
  • Equivalent Model
ef24f6946fa0723be11121e072254eb6901a8c3c Apalache SetDiff Set2 True Passed
  • Model Under Test
  • Equivalent Model
0bdec915cbd37249ecf4f227642fd9271b360905 Apalache SetDiff Set2 False Passed
  • Model Under Test
  • Equivalent Model
a805a539899b05d97f630ee531e0346bce16161a Apalache SetDiff Choose True Passed
  • Model Under Test
  • Equivalent Model
079b95763e73acf537817987bab44219413bc9a5 Apalache SetDiff Choose False Passed
  • Model Under Test
  • Equivalent Model
379aa8f13a9aa6f3f2edd4efb2b70d8de007df51 Apalache SetDiff FunApp True Passed
  • Model Under Test
  • Equivalent Model
47d5ab33a19e8d82e6f69220c7c7b2cce8b2c03e Apalache SetDiff FunApp False Passed
  • Model Under Test
  • Equivalent Model
9254992bcfbf659d7b21d737ad7957750ddfd2f3 Apalache SetDiff Prime True Passed
  • Model Under Test
  • Equivalent Model
d449fd3ad2727aeadb5d02b4a00bcda78495b47b Apalache SetDiff Prime False Passed
  • Model Under Test
  • Equivalent Model
432c4541bdc1a33ede7070351c758e9420301ad6 Apalache SetDiff Def0 True Passed
  • Model Under Test
  • Equivalent Model
618f00b11e31ebfb5bbd11b4b8cb755cc7e2179a Apalache SetDiff Def0 False Passed
  • Model Under Test
  • Equivalent Model
687a57397018fade20b90a617e951ca36fbfa00a TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef0 True Passed
  • Model Under Test
  • Equivalent Model
31b936798ab75817a8b7a8895e9dfbed3d0375cf TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef0 False Passed
  • Model Under Test
  • Equivalent Model
27d97aeb296a24ee8e9ee88ea67d9699308cbbe8 Apalache SetDiff Def1 True Passed
  • Model Under Test
  • Equivalent Model
a2f22082256d509abf69e690d3897aaf2157d8c7 Apalache SetDiff Def1 False Passed
  • Model Under Test
  • Equivalent Model
e39cd9d712c0fad295c6fd6dacf15a8fc03fc669 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef1 True Passed
  • Model Under Test
  • Equivalent Model
5688d2458465e2431865ed267daac686ea20dcd9 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef1 False Passed
  • Model Under Test
  • Equivalent Model
38bdc35b84aaa00ab5993c7014f890def2003480 Apalache SetDiff Def2 True Passed
  • Model Under Test
  • Equivalent Model
bcea28c4466a51d465c42a76c4f2038361bfda9f Apalache SetDiff Def2 False Passed
  • Model Under Test
  • Equivalent Model
310e80f84a258c4c06c0b13f9a957b63d60f1b6c TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef2 True Passed
  • Model Under Test
  • Equivalent Model
1431473e17542a1b2bb0483eb8443fe125f0d983 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef2 False Passed
  • Model Under Test
  • Equivalent Model
332417e636454c0ee4ae54295e6d16fafd78c00f Apalache SetDiff Def1Recursive True Passed
  • Model Under Test
  • Equivalent Model
9d6fc06c443ec2ea0d25498fa975ce2286e35ed5 Apalache SetDiff Def1Recursive False Passed
  • Model Under Test
  • Equivalent Model
9f7a67dde75544188b3dffa54c40d9663f8e79f7 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef1Recursive True Passed
  • Model Under Test
  • Equivalent Model
3f7d189af49ce478b938e57352c03f853ecbd888 TLC with reduction strategy:
  • Plug Feature: LET definitions are reduced to global definitions
SetDiff LetDef1Recursive False Passed
  • Model Under Test
  • Equivalent Model
5d2384957665aefd9de98dffba13a76a36ad2ad5 Apalache SetDiff Extends True Passed
  • Model Under Test
  • Equivalent Model
f78c94f89abde0d721cac27ff78f552d4fb98214 Apalache SetDiff Extends False Passed
  • Model Under Test
  • Equivalent Model
24ad79168b452dccae01828be6bbaeb7726be68d Apalache SetDiff ExtendsInDifferentFolder True Passed
  • Model Under Test
  • Equivalent Model
a19147603a6f206580727b7097e7ae1dc56886c5 Apalache SetDiff ExtendsInDifferentFolder False Passed
  • Model Under Test
  • Equivalent Model
e520ec93be4d1ec24a42fd01fa64dcdd76bfda79 Apalache SetDiff Variable True Passed
  • Model Under Test
  • Equivalent Model
9e909d7a98b6a1ef212b05b5d1a36b293cd3b2b6 Apalache SetDiff Variable False Passed
  • Model Under Test
  • Equivalent Model
568a4ed98fd0092bcd9568f301d880b9c8748aef Apalache SetDiff Constant True Passed
  • Model Under Test
  • Equivalent Model
4eea0664065806df26bffe1f9fb7e345046ebcb6 Apalache SetDiff Constant False Passed
  • Model Under Test
  • Equivalent Model
9917d4610b835ba3c8a66257d5200a8e1824281f Apalache SetDiff ConstantRank1 True Passed
  • Model Under Test
  • Equivalent Model
4848fe673ee12b63a6a63750bdf064572a9b8a9d Apalache SetDiff ConstantRank1 False Passed
  • Model Under Test
  • Equivalent Model
678edab2cc009b1341a58654148eda06f795e9cb Apalache SetDiff Instance True Passed
  • Model Under Test
  • Equivalent Model
1371de522c5bd3b80d018b026539587e5dd53f42 Apalache SetDiff Instance False Passed
  • Model Under Test
  • Equivalent Model
2a54f93ab41141c61b4b4240f30768071468113c Apalache SetDiff InstanceWith True Passed
  • Model Under Test
  • Equivalent Model
d60d85069d2718596d5268e170c3544bebd2c344 Apalache SetDiff InstanceWith False Passed
  • Model Under Test
  • Equivalent Model
41f9576c42f9096dc2d055a0a9b3fa68e011aca2 Apalache SetDiff InstanceNamed True Passed
  • Model Under Test
  • Equivalent Model
0620af8569893f43c9afc45063974e4bac1598ce Apalache SetDiff InstanceNamed False Passed
  • Model Under Test
  • Equivalent Model
e9e8b5d07ebfdaf22ff8e34ec08af72ffbf84bb4 Apalache SetDiff InstanceNamedWith True Passed
  • Model Under Test
  • Equivalent Model
c40696204950162cef22ded7825de24387ecebf7 Apalache SetDiff InstanceNamedWith False Passed
  • Model Under Test
  • Equivalent Model
41aafa18eaa9c32a9c77dde1b38730647505a456 Apalache SetDiff InstanceInFolder True Passed
  • Model Under Test
  • Equivalent Model
38e879a0b86ea26477913de3a5938785be28ecac Apalache SetDiff InstanceInFolder False Passed
  • Model Under Test
  • Equivalent Model
cc24f1c3a81fc9cf5b87de5fb1e08c993c1b5ac9 Apalache SetDiff InstanceWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
e38ac06842eb01b1dd0ba32879b4fa1c1b73cbfc Apalache SetDiff InstanceWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
ffb7a9483c7b9fb73dc524eb3f1ea8ac721d15dc Apalache SetDiff InstanceNamedInFolder True Passed
  • Model Under Test
  • Equivalent Model
48d9dc792d0447bc724731e6aac383867d9fb591 Apalache SetDiff InstanceNamedInFolder False Passed
  • Model Under Test
  • Equivalent Model
679f7d5ac3be6564f59c30ae495d89588a5c48ac Apalache SetDiff InstanceNamedWithInFolder True Passed
  • Model Under Test
  • Equivalent Model
31f481e899ad64fc8a604190321cc1b2cac08315 Apalache SetDiff InstanceNamedWithInFolder False Passed
  • Model Under Test
  • Equivalent Model
6e7ef9f9df2448f1a10d64003f6390ccd1e12cbf Apalache SetDiff Cross2 True Passed
  • Model Under Test
  • Equivalent Model
879bd9822e8a0652244bdc7bf2e62b31a1e2a4ae Apalache SetDiff Cross2 False Passed
  • Model Under Test
  • Equivalent Model
30c859e738d289a7ab98d3fe451a52a90d1d1003 Apalache SetDiff Cross3 True Passed
  • Model Under Test
  • Equivalent Model
401b0d6342fefd117ed68ef002ec7c50cef17c95 Apalache SetDiff Cross3 False Passed
  • Model Under Test
  • Equivalent Model
71dd9c5f5c5dbd64ecabe9a88671f13d0e977dda TLC with reduction strategy:
  • Plug 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))
SetDiff FunSet True Passed
  • Model Under Test
  • Equivalent Model
4bb5f232677209fe91091e84de306372aaccbe77 TLC with reduction strategy:
  • Plug 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))
SetDiff FunSet False Passed
  • Model Under Test
  • Equivalent Model
33fcc86d2b9b9c6075cba403490a0501093b286d TLC with reduction strategy:
  • Plug 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)
SetDiff RecordSet True Passed
  • Model Under Test
  • Equivalent Model
cb5e427f4b1c6a4e3d030aab224ae155c4414a0b TLC with reduction strategy:
  • Plug 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)
SetDiff RecordSet False Passed
  • Model Under Test
  • Equivalent Model
c8957b34b87d6a92d8b9533a38ba3b6265c97d43 Apalache SetDiff SetDiff True Passed
  • Model Under Test
  • Equivalent Model
503b17ad8dcc64232e451996974cc45fef1fc40d Apalache SetDiff SetDiff False Passed
  • Model Under Test
  • Equivalent Model
789b549272813cbd7ea4dd09ec42773ff11c55b9 Apalache SetDiff SetUnion True Passed
  • Model Under Test
  • Equivalent Model
f903582e33409c5bf6190e2276aa9258901cff21 Apalache SetDiff SetUnion False Passed
  • Model Under Test
  • Equivalent Model
f369aaa2c9fa84888c7aea2f36003f81195e151e Apalache SetDiff SetIntersect True Passed
  • Model Under Test
  • Equivalent Model
2ef4db587c707392de7a31d5d6ffc28d183aa743 Apalache SetDiff SetIntersect False Passed
  • Model Under Test
  • Equivalent Model
28de05b2294345fcb32917f08ea49f1c48365c65 Apalache SetDiff IfCond True Passed
  • Model Under Test
  • Equivalent Model
e6b27023ba1ea24381f3e91b8496ebc1a77fcbdb Apalache SetDiff IfCond False Passed
  • Model Under Test
  • Equivalent Model
7f7307d677136e5a5fc7b2470d32f6d4389b97d3 Apalache SetDiff IfThen True Passed
  • Model Under Test
  • Equivalent Model
a38d0bd66c26e45af9dfeae13fd255b59e206fca Apalache SetDiff IfThen False Passed
  • Model Under Test
  • Equivalent Model
d4e4040e34bcf9a4fe7680334482800f9518b465 Apalache SetDiff IfElse True Passed
  • Model Under Test
  • Equivalent Model
9bb39eb3a879a71a1c558ef1aa6c2b4585aa434e Apalache SetDiff IfElse False Passed
  • Model Under Test
  • Equivalent Model
56edabd084c4806ba85f869409baff12e623e422 Apalache SetDiff Subset True Passed
  • Model Under Test
  • Equivalent Model
89b74b055ae528aaa9bf04fbbab89fc6ba54b745 Apalache SetDiff Subset False Passed
  • Model Under Test
  • Equivalent Model
38819ad0219940f4532aed003d03832847e7d2e9 Apalache SetDiff Domain True Passed
  • Model Under Test
  • Equivalent Model
2b7640c187cb3eec3606292e612da1c4c4753d08 Apalache SetDiff Domain False Passed
  • Model Under Test
  • Equivalent Model
c42579a40ac06a96f15f6cd469396709794aa613 Apalache SetDiff Union True Passed
  • Model Under Test
  • Equivalent Model
103821a97ec9a78c0c9037271b05acd332eb16e5 Apalache SetDiff Union False Passed
  • Model Under Test
  • Equivalent Model
a01e98d9279f9a53e804f1cb35d5a9b684e25320 TLC with reduction strategy:
  • Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
SetDiff NumRange True Passed
  • Model Under Test
  • Equivalent Model
390aece71c6abb87bbd12bf952a6371a4220b279 TLC with reduction strategy:
  • Plug Feature: n..m is replaced with { x \in { n, n + 1, ... } : x <= m }; it falls back to crash (through CHOOSE Q : FALSE) if m is too big: this crash forces to do manual test review
SetDiff NumRange False Passed
  • Model Under Test
  • Equivalent Model
e71c409003a2d0823d39cb482b317aa91ac5c24a TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetDiff TlcPermuteFun True Passed
  • Model Under Test
  • Equivalent Model
fcea10f31ccc885decdaf7c460eea6232c8d3a72 TLC with reduction strategy:
  • Plug Feature: Permutations(S) is reduced to equivalent: { f \in [S -> S] : { f[u] : u \in S } = S }
SetDiff TlcPermuteFun False Passed
  • Model Under Test
  • Equivalent Model
92a08a9601ffa0ce05edafbed778c15e2a656889 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetDiff TlcEval True Passed
  • Model Under Test
  • Equivalent Model
3c1152c687361f06ba846eb9990f2a851b9544f5 TLC with reduction strategy:
  • Plug Feature: TLCEval(expr) is reduced to just expr
SetDiff TlcEval False Passed
  • Model Under Test
  • Equivalent Model
b3de66a1e0021966d27c211247cee7b6e8a98090 Apalache SetDiff BagBagToSet True Passed
  • Model Under Test
  • Equivalent Model
9797f09c7f7ad2066e3461d8b8489e916e1e7dca Apalache SetDiff BagBagToSet False Passed
  • Model Under Test
  • Equivalent Model
dd1f04641a22f7aa7750d72c3468a0f1b7dec0f2 TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetDiff BagSubBag True Passed
  • Model Under Test
  • Equivalent Model
029c9cf567206e22d904532543bf81d11fd19c8c TLC with reduction strategy:
  • Plug Feature: SubBag(B) is reduced to equivalent SubBagR implementation
SetDiff BagSubBag False Passed
  • Model Under Test
  • Equivalent Model
35ff6a727939f360083f4009153b819709dd25a6 Apalache SetDiff SeqHead True Passed
  • Model Under Test
  • Equivalent Model
9c3e6693f8754bff86ed51491a36a7556189e737 Apalache SetDiff SeqHead False Passed
  • Model Under Test
  • Equivalent Model