Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
3e9a5d262c6c778d4b324a4150f3d1177cab9256 Apalache In SeqSeq True Passed
68b0919b779c9fae97f7ad96230b98381981e0e9 Apalache In SeqSeq False Passed
ccafe4ba02c3dfbf72bfccd0182bb618796f22d9 Apalache NotIn SeqSeq True Passed
f9c2529976d03e48875873f11ea097bdde31f21e Apalache NotIn SeqSeq False Passed
47147b6791d04cb91b4bc7d204710cd99864c04d 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 SeqSeq True Passed
1467cac28a17329a0da2729082c4b81b3515066d 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 SeqSeq False Passed
0563e49e991555a9054f98712b882015d7640675 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 SeqSeq True Passed
7aece2ccb85d5787842b6810080c25cf7e91b657 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 SeqSeq False Passed
565ea71bd4f22b6beb30f46e9e02300c44e50839 Apalache SeqSeq SeqSeq True Passed
9e40200b57c8392d0b74fcd69878b2b34f88d4b7 Apalache SeqSeq SeqSeq False Passed
38f365e60ab3097a0595d81dead517922c5438d3 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 SeqSeq True Passed
6717eac93ae3f40ec78c1b4da7e7db2ecf861a3c 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 SeqSeq False Passed