3.1.5 Sample configuration file

The following configuration file sets lbtt up for testing two imaginary LTL-to-Büchi translators.

     # Sample configuration file for lbtt
     
     Translator
     {
       Name = Translator\ 1
       Path = /home/lbtt-user/bin/t-1    # location of the translator
                                         # executable
       Enabled = Yes
     }
     
     Translator
     {
       Name = "Translator 2"
       Path = /home/lbtt-user/bin/t-2
       Parameters = "-x -y 3 -v 0"       # parameters to be passed to the
                                         # executable
       Enabled = Yes
     }
     
     GlobalOptions
     {
       Rounds = 100                      # 100 test rounds
     
       Interactive = OnError,OnBreak     # pause testing in case of an error
                                         # or when receiving a break signal
     
       Verbosity = 1                     # show only numeric statistics
     
       ComparisonTest = Yes              # enable all tests except the
       ConsistencyTest = Yes             # Büchi automata intersection
       IntersectionTest = No             # emptiness test
     
       ModelCheck = Local                # perform the tests only in a
                                         # single state of each state
                                         # space
     
       TranslatorTimeout = 30s           # abort the execution of a
                                         # translator if it fails to give
                                         # a result in 30 seconds
     }
     
     FormulaOptions
     {
       AbbreviatedOperators = Yes        # formula generation mode
       GenerateMode = Normal
       OutputMode = NNF                  # rewrite formulas in negation
                                         # normal form before passing
                                         # them to the translators
     
       ChangeInterval = 1                # new formula after each round
     
       RandomSeed = 4632912              # random seed
     
       Size = 5-15                       # 5 to 15 nodes in the parse
                                         # tree of each formula
     
       Propositions = 3                  # allow at most three different
                                         # propositions in each LTL formula
     
       PropositionPriority = 50          # priorities for propositional
       TruePriority = 1                  # symbols
       FalsePriority = 1
     
       AndPriority = 10                  # priorities for some logical
       OrPriority = 10                   # operators
       NotPriority = 10
       EquivalencePriority = 5
     
       NextPriority = 5                  # priorities for some temporal
       UntilPriority = 5                 # operators
       ReleasePriority = 5
       FinallyPriority = 2
     
       DefaultOperatorPriority = 0       # disable all the remaining
                                         # operators
     }
     
     StatespaceOptions
     {
       GenerateMode = RandomGraph        # generate random (not
                                         # necessarily connected) graphs
                                         # as state spaces
     
       ChangeInterval = 10               # new state space after every
                                         # 10th test round
     
       RandomSeed = 37620                # random seed
     
       Size = 50                         # 50 states in each state space
     
       Propositions = 3                  # three propositions in each
                                         # state of each state space
     
       EdgeProbability = 0.1             # approximate probability of
                                         # having a transition between
                                         # any two states
     
       TruthProbability = 0.5            # probability with which any
                                         # atomic proposition is true in
                                         # a state
     }