Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
e747106d5f66198ec2e801c3cfd2616cb1f975a1 Apalache In IntSet True Passed
d84904b2883396232e0217281725209e6f637e15 Apalache In IntSet False Passed
6d284d5152bb822207cf54e9a1be82189884beed Apalache NotIn IntSet True Passed
eeb7bafedea481a6646c01c9f8c4aad09d83a91c Apalache NotIn IntSet False Passed
74a7658a28aff48fcf8e7033a86daa955a7a3204 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 IntSet True Passed
68e395c21c68a7a05e6672b34b7ff5fd83a7fd08 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 IntSet False Passed
9c6ccaa9787c83b634dd756817ccf59e230184ea 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 IntSet True Passed
b81dc644b5c72051e5c1540dffa1b2bf5f78018b 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 IntSet False Passed
c17231d50527c3e5fdfc42fbb77a8cb24db6f25b Apalache SeqSeq IntSet True Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Int)
072786e1f8f0bf2d59e8b8468ac417a79ea7f6dc Apalache SeqSeq IntSet False Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Int)
665e71eddb22111536affb76507082a702dbd871 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 IntSet True Passed
d1e286a1084c37053079a3d12986c36f5b2afe9c 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 IntSet False Passed