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

Test Specification: Index By Feature For workers=1

This page is an index of all test cases, produced by pairwise combining of the TLA+ language features. Feature is an operator, constant, variable, or other TLA+ language construct, which is required by the use cases. How to use this index:
  • This index list all the features
  • In generated test cases, a feature can be either case or plug. Note that the same feature can be case in one test case and plug in the other
  • Column Case Index allows to see all test cases, where a given feature participates as case
  • Column Plug Index allows to see all test cases, where a given feature participates as plug
  • Test Cases

    Case Index Plug Index
    And And
    AndMultiLine AndMultiLine
    AndProp AndProp
    Assume Assume
    AssumeNamed AssumeNamed
    BagAddBag BagAddBag
    BagBagCardinality BagBagCardinality
    BagBagIn BagBagIn
    BagBagOfAll BagBagOfAll
    BagBagSub BagBagSub
    BagBagToSet BagBagToSet
    BagBagUnion BagBagUnion
    BagCopiesIn BagCopiesIn
    BagEmptyBag BagEmptyBag
    BagSetToBag BagSetToBag
    BagSubBag BagSubBag
    BagSubsetEqBag BagSubsetEqBag
    BoolFalse BoolFalse
    BoolSet BoolSet
    BoolTrue BoolTrue
    Boxed Boxed
    Choose Choose
    ChooseInDef ChooseInDef
    Constant Constant
    ConstantModelValue ConstantModelValue
    ConstantRank1 ConstantRank1
    Cross2 Cross2
    Cross3 Cross3
    Def0 Def0
    Def1 Def1
    Def1Recursive Def1Recursive
    Def2 Def2
    DefFun DefFun
    DefFunInDef DefFunInDef
    DefFunRecursive DefFunRecursive
    Domain Domain
    Enabled Enabled
    Eq Eq
    Equivalence Equivalence
    Except0 Except0
    Except1Fun Except1Fun
    Except1FunWithAt Except1FunWithAt
    Except1Rec Except1Rec
    Except1RecWithAt Except1RecWithAt
    Except2Fun Except2Fun
    Except2FunTuple Except2FunTuple
    Exists Exists
    ExistsInDef ExistsInDef
    Extends Extends
    ExtendsInDifferentFolder ExtendsInDifferentFolder
    FiniteSetsCardinality FiniteSetsCardinality
    FiniteSetsIsFiniteSet FiniteSetsIsFiniteSet
    Forall Forall
    ForallInDef ForallInDef
    Fun Fun
    FunApp FunApp
    FunInDef FunInDef
    FunSet FunSet
    IfCond IfCond
    IfElse IfElse
    IfThen IfThen
    Imply Imply
    In In
    InDef0 InDef0
    InDef1 InDef1
    InDef2 InDef2
    Instance Instance
    InstanceInFolder InstanceInFolder
    InstanceNamed InstanceNamed
    InstanceNamedInFolder InstanceNamedInFolder
    InstanceNamedWith InstanceNamedWith
    InstanceNamedWithInFolder InstanceNamedWithInFolder
    InstanceWith InstanceWith
    InstanceWithInFolder InstanceWithInFolder
    IntSet IntSet
    Lambda Lambda
    Let Let
    LetDef0 LetDef0
    LetDef1 LetDef1
    LetDef1Recursive LetDef1Recursive
    LetDef2 LetDef2
    LetDefFun LetDefFun
    LetDefFunInDef LetDefFunInDef
    LetDefFunRecursive LetDefFunRecursive
    MultiLineComment MultiLineComment
    NatSet NatSet
    Ne Ne
    Not Not
    NotIn NotIn
    NumDiv NumDiv
    NumGe NumGe
    NumGt NumGt
    NumLe NumLe
    NumLt NumLt
    NumMaxInt NumMaxInt
    NumMinus NumMinus
    NumMod NumMod
    NumMul NumMul
    NumOne NumOne
    NumPlus NumPlus
    NumPow NumPow
    NumRange NumRange
    NumUnaryMinus NumUnaryMinus
    NumZero NumZero
    OneLineComment OneLineComment
    Or Or
    OrMultiLine OrMultiLine
    Prime Prime
    Record Record
    RecordSet RecordSet
    SeqAppend SeqAppend
    SeqConcat SeqConcat
    SeqHead SeqHead
    SeqLen SeqLen
    SeqSelectSeq SeqSelectSeq
    SeqSeq SeqSeq
    SeqSubSeq SeqSubSeq
    SeqTail SeqTail
    Set0 Set0
    Set1 Set1
    Set1InDef Set1InDef
    Set2 Set2
    Set2InDef Set2InDef
    SetDiff SetDiff
    SetEmpty SetEmpty
    SetIntersect SetIntersect
    SetUnion SetUnion
    String String
    StringEmpty StringEmpty
    StringSet StringSet
    Subset Subset
    SubsetEq SubsetEq
    TlcEval TlcEval
    TlcExtendFun TlcExtendFun
    TlcPermuteFun TlcPermuteFun
    TlcSingletonFun TlcSingletonFun
    TlcSortSeq TlcSortSeq
    Tuple Tuple
    TupleEmpty TupleEmpty
    Unchanged Unchanged
    Union Union
    Variable Variable
    VariableViewExclude VariableViewExclude