Index

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

Id Type Case Feature Plug Feature Check Deadlock Test Results Test Models
57467abad19a6ff7e1944ca8f5ee33899a5b1de0 Apalache In NatSet True Passed
54c7176ac91d77a1725d1c092c2502cabbbae0b8 Apalache In NatSet False Passed
f71d80fe0e422d806ae958e9fd2d0cd6e4e15120 Apalache NotIn NatSet True Passed
f4d2e40badf9b932ee1964eef3eeead2347268dd Apalache NotIn NatSet False Passed
ff63b490b2a81d353ae868af8a9339879234343f 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 NatSet True Passed
df75a2a53dd9e0deca87614db29bc035cd85bffd 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 NatSet False Passed
1e94ed03d0dd3bffddd0b8bebbf2421feb82cb7f 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 NatSet True Passed
03a250429d50dc2277d125125b6a9b791582f1f2 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 NatSet False Passed
e7d5262aa94a255dfbd4ba5e2f1e9a54c97c7e4f Apalache SeqSeq NatSet True Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Nat)
2588a3aac4ad1d167993af497aa0ceab3769e752 Apalache SeqSeq NatSet False Failed: TLC model check results are correct. Apalache is unable to check the model, SeqSeq replacement does not work with infinite sets (Nat)
275ac05756ef0ddc2b9456215acedc8c959823f1 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 NatSet True Passed
b266b317154a8085295880e8164e6fbe7c595ae7 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 NatSet False Passed