Settings File

A settings file, commonly ending with the suffix .attestor, is a collection of command line options that can be imported using the --load option (link). All additionally provided command line options are interpreted after loading a settings file and thus overwrite its options.

Settings files may contain all command line options except for --load, where each line of the settings file must contain at most one option, i.e. empty lines are permitted. Furthermore, lines starting with '#' are comments and thus ignored.

A collection of settings files is found in the examples repository.

Example file

    # Benchmark: DLL reversal
    # Specification: Check reachability
    --description "Prove that initially head reaches tail via next pointers and tail reaches head via prev pointers. Also prove the reverse upon termination."

    # Analyzed method
    --classpath "configuration/code"
    --class "DLList"
    --method "reverse"

    # Grammar 
    --predefined-grammar "DLList"
    --rename DLListNode=DLList next=nextAlt prev=prevAlt

    # Initial states
    --initial "configuration/inputs/DLLHeadTail.json"

    # Verification
    --model-checking "XX ( {isReachable(head,tail,[nextAlt])} & {isReachable(tail,head,[prevAlt])})"
    --model-checking " F (X {terminated} -> ( {isReachable(head,tail,[prevAlt])} & {isReachable(tail,head,[nextAlt])}))"

    # Options
    --admissible-abstraction