config.yaml

---

# The name of performed experiment (used as a folder name to save results)
# If not specified, name of the config file will be used instead.
experiment: "frontend-testing"

# If set to true, experiment folder will contain information about the build.
printBuildInfo: true  # default true

# If set to true, experiment folder will contain information about the 
# operating system, memory, number of cores, etc.
printEnvironmentInfo: true # default true

# log level that should be printed to console
# (Everything lower will be printed only into files)
consoleLogLevel: info # all/error/warning/info/fine/finer/finest/off, default info 

# Here you can specify a list of tasks you want to execute.
# Right now, only supported task type is ctlParamEstimation,
# future plan is to have things like odeModelAbstraction or 
# symba in separate tasks with chainable results.
tasks:

  - type: CTLParameterEstimation # default CTLParameterEstimation

    # Timeout in seconds for this task. Negative value means no timeout.
    # Warning: doesn't work for MPJ tasks yet.
    timeout: 3600   #default -1
    # Maximal memory per worker in megabytes.
    # In case of shared memory computation, one process with workers * maxMemory limit will be started
    maxMemory: 1024 # default 1024

    # Type of job queue.
    jobQueue: blockingQueue # blockingQueue/mergeQueue, default blockingQueue

    # There are four types of communicators:

    # This is for a single core computation
    #communicator: none

    # Use blocking queues as channels. All workers run in one process.
    #communicator:
    #  type: sharedMemory
    #  workers: 2

    # Local variant of MPJ computation (equivalent to running runmpj.sh -np -jar biodivine....)
    #communicator:
    #  type: mpjLocal
    #  workers: 2
    #  mpjHome: "/path/to/mpj/" # You don't have to specify this if environmental variable MPJ_HOME is properly set

    # Cluster variant of MPJ computation
    #communicator:
    #  type: mpjCluster
    #  portRange: "10000-10100" # Port range used for mpj communication
    #  hosts: ["pheme02", "pheme03", "pheme04"] # list of ssh hosts that will perform the computation

    communicator:
      type: sharedMemory #sharedMemory/mpjLocal/mpjCluster/none default none
      workers: 1  # default 1

    partitioning:
      type: block # uniform/slice/hash/block, default uniform
      #if you use block partitioning, you can set additional property: blockSize - default is 100
      blockSize: 10

    colors: rectangular # smt/rectangular, default rectangular

    checker:
      logLevel: error

    # Ctl parser settings.
    ctlParser:
      # optimize formulas after parsing and normalizing (remove double negation, etc.)
      optimize: true # default true
      # normalize to standard set of operators
      normalForm: until # default until (EU/AU/EX/&&/||/!), use none to disable normalization
      # parser log level
      logLevel: info

    # You can give list of several properties, each will be verified in specified order
    # A copy of the property will be also included in results
    properties:
      # You can use "inlined" formulas
      - formula: "pRB > 3.0 EU E2F1 > 6"
        # type of results that should be printed.
        # size - only print size of the result set // log
        # stats - additional info about performance // log
        # human - print full results in human readable format // only file
        results: ["size", "stats"] # default []
      # You can specify a property by name from a file
      - file: "test_prop.ctl"
        verify: "bistab"
        results: ["size", "stats", "human"]
      # You can use a hybrid notation - referencing formulas defined in a file,
      # but ultimately verifying an inlined formula
      - file: "test_prop.ctl"
        formula: "pRB > 3.0 EU lowStable"
        results: ["size", "stats", "human"]

    # Here you should specify your model. For now, only supported model type is ODE.
    model:
      type: ODE
      #Model file path
      file: "tcbb.bio"
      # Use faster, but less precise approximation method
      fastApproximation: true # default false
      # Cut off autogenerated thresholds that exceed specified model bounds
      cutToRange: false # default false
      selfLoops: false # default true