Settings

Settings are general-purpose, serializable and deserializable descriptions of various parameters, including settings of components, descriptions of job parameters, etc. It is implemented as a hierarchical key-value store with support for lists.

Settings model

SettingsMetamodel
Figure: SettingsMetamodel
  • Every settings node implements the abstract superclass Settings (composite pattern).
  • A settings node can either be a settings element or a settings list.
    • The type of a settings node can be determined using its kind() method.
    • Every settings node has a parent (getParent()) except for the root element that is created by SettingsElement.createRootElement().
  • A settings element (SettingsElement) contains a single string value (read: value(), write: setValue()) that can also be null, and zero or more attributes.
    • An attribute is a settings element with a unique key.
    • A new non-root settings element can be created by SettingsElement.empty() or by SettingsElement.ofValue(String). The former creates an empty element, the latter creates an element with the given string as value.
    • The value of a settings element can be read using the value() method. For diagnostic purposes (to find unread parts of the settings subtree), reading the value will be registered and after the first read the isConsumed() method will return true. If a value needs to be read without setting the consumed flag (e.g., in a copy operation), the valueWithoutConsuming() method can be used. This is for exceptional cases.
  • A settings list (SettingsList) contains one or more settings node with integer indices. The indices are not necessarily consecutive.
  • Naming. Each settings node has a name.
    • For the root settings element, the name can be set arbitrarily.
    • For a non-root settings node with a settings element parent, the name is the unique key its parent knows it as an attribute.
    • For a non-root settings node with a settings list parent, the name is its index in its parent settings list.
    • Each settings node has a fully qualified name (FQN) that is the concatenation of the names of the nodes from the root to the given element, separated by .s. The FQN can be accessed using the fqn() method.
  • Various utility methods can be found in the SettingsUtils class.

Textual syntax of the settings model

When a settings node tree is described typically, the syntax used is a list of each settings element in the following format: -<fqn>=<value>. If the values are separated by new line characters (\n or \r\n), we call it a settings file format. If the values are separated by (one or more) whitespace, we call it command line format. The SettingsSerializer.parseSettings*() methods can be used to parse the textual syntax, the SettingsSerializer.serialize*() methods can be used to produce the textual syntax of a settings node tree.

Details of the syntax

  • Quoting values with whitespace. The <value> needs to be quoted ("<value>") if it contains whitespace character(s). The values can always be quoted if necessary.
    • If the value contains a quotation character ("), it will be replaced with '' at the serialization.
  • List syntaxes. There is a shorthand for the settings list description: instead of -list.0=A -list.1=B -list.2=C [...], the following syntax can be used: -list={A, B, C, [...]}. The elements will be indexed from zero using this syntax.
    • The values within the curly brackets can also be quoted if needed. The whitespace after the element separator , character is optional. However, when there is no whitespace character after the ,, the curly braces can be omitted. I.e., the following descriptions are equivalent:
      • -list={A,B,C}
      • -list=A,B,C
      • -list="A","B","C"
      • -list={"A", "B", "C"}
      • -list.0=A -list.1=B -list.2=C
    • The empty list can only be represented as -list={}.
  • Line comments. Parts of the lines after // will be ignored.
  • Multiple values cannot be defined for the same settings element. E.g., -key1=val1 -key1=val2 is illegal.

Example settings and parsed settings tree

The following figure shows an example to demonstrate the parsed settings tree for a textual representation. __root : SettingsElementvalue = nulllf : SettingsElementvalue = step7inline : SettingsElementvalue = nulljob : SettingsElementvalue = verifjob.reporters : SettingsListjob.reporters.0 : SettingsElementvalue = plaintextjob.backend : SettingsElementvalue = nusmvjob.requirement : SettingsElementvalue = assertionjob.requirement.inputs : SettingsListjob.requirement.inputs.0 : SettingsElementvalue = var1job.requirement.inputs_1 : SettingsElementvalue = var2job.requirement.bindings : SettingsListjob.requirement.bindings.0 : SettingsElementvalue = nulljob.requirement.bindings.0.input : SettingsElementvalue = var5job.requirement.bindings.0.value : SettingsElementvalue = 0job.requirement.params : SettingsListjob.requirement.params.0 : SettingsElementvalue = var3job.requirement.params.1 : SettingsElementvalue = var4reductions : SettingsListreductions.0 : SettingsElementvalue = basic_reductionsname : SettingsElementvalue = "Demo settings"description : SettingsElementvalue = "Demo description"output : SettingsElementvalue = C:\TEMP\id : SettingsElementvalue = IDsourcefiles : SettingsListsourcefiles.0 : SettingsElementvalue = a.sclsourcefiles.1 : SettingsElementvalue = "a file.scl"sourcefiles.1.encoding : SettingsElementvalue = UTF-8-description = "Demo description"-id = ID-lf = step7-name = "Demo settings"-output = C:\TEMP\-reductions.0 = basic_reductions-job = verif-job.backend = nusmv-job.reporters.0 = plaintext-job.requirement = assertion-job.requirement.bindings.0.input = var5-job.requirement.bindings.0.value = 0-job.requirement.inputs.0 = var1-job.requirement.inputs.1 = var2-job.requirement.params.0 = var3-job.requirement.params.1 = var4-sourcefiles.0 = a.scl-sourcefiles.1 = "a file.scl"-sourcefiles.1.encoding = UTF-8lfinline[0]reportersbackend[0][1]inputsinputvalue[0]bindings[0][1]paramsrequirementjob[0]reductionsnamedescriptionoutputid[0]encoding[1]sourcefiles

Overriding settings

It is possible to merge two settings trees using the Settings.overrideWith(Settings) method. Here are the rules for this operation:

  • A settings element aa can only be overridden by another settings element bb.
    • The value of aa will be modified to the value of bb.
    • All attributes (descendants) of bb will be included in aa. If aa contains an attribute with the same name as bb, the subtree of that attribute will be overridden by aa. If aa contains an attribute that is not present in bb, the subtree of that attribute will not be modified.
  • A settings list aa can only be overridden by another settings list bb.
    • If for an index ii both the settings lists aa and bb contain a settings node, a[i]a[i] will be overridden by b[i]b[i].
    • If for an index ii the settings list aa does not contain a settings node but bb does, a[i]a[i] will be set to b[i]b[i].
    • If for an index ii the settings list aa does contain a settings node but bb does not, a[i]a[i] will not be modified.
  • Overriding is done recursively.
  • The settings tree passed as an argument to the overrideWith() method may be destroyed or altered. Do not use that object later on, or create a copy of it first.

Example.

Let's assume the following two settings trees: -key1=value1 -key2=value2 and -key1=Xvalue1 -key3=Xvalue3. The result of overriding the first settings tree with the second one will be: -key1=Xvalue1 -key2=value2 -key3=Xvalue3.

Note that when a settings node is overridden by another one, the subtree will be merged, not simply overwritten. For instance, the result of overriding -key1=val1 -key1.subkey1=subval1 with -key1=Xval1 will be -key1=Xval1 -key1.subkey1=subval1.

In case of lists, the index of the elements does count too. For example, the result of overriding -list.0=A -list.1=B with -list.0=X -list.2=Y will be -list.0=X -list.1=B -list.2=Y.

[info] Effective setting calculation

Merging settings is typically used for calculating the effective settings of several settings trees coming from different sources (e.g., from the user, from the plug-in defaults, from the installation-specific settings). These may be stored in different formats (see Specific settings). The EffectiveSettings class helps to cope with these differences.

Specific settings

It is possible to hide the low-level details of the settings object model and automatically parse the Settings object hierarchy into a more convenient Java object model. For this, follow the steps below.

  1. Create a new class that extends the cern.plcverif.base.common.settings.specific.AbstractSpecificSettings class.
  2. Create fields for the different settings element. (The fields can be private.)
    • Annotate with @PlcverifSettingsElement all elementary settings, i.e., fields with type boolean, int, long, String, Path or any enumeration type.
    • Annotate with @PlcverifSettingsList all List<String> fields. Currently lists with types other than String are not supported.
    • Annotate with @PlcverifSettingsComposite all composite fields that also extend the AbstractSpecificSettings class and which should be parsed as specific settings.
    • Parameters of the annotations:
      • name (mandatory): determines the key of the Settings object that will be loaded into the annotated field.
      • description (optional): describes the purpose of the field.
      • mandatory (optional): determines whether the given field is mandatory or optional, i.e., if it is a parsing error if a value is not present for the annotated field. If the field is optional and there is no corresponding value in the generic settings that is being parsed, the field will keep its initial value.
  3. Call the SpecificSettingsSerializer.parse(SettingsElement settingsToBeParsed, Class<? extends AbstractSpecificSettings> specificSettingsType) that will parse the given settingsToBeParsed and returns a new object with the type specificSettingsType containing the parsed values. It throws an exception if an error occurs during parsing or if a mandatory field is missing in the settingsToBeParsed.
  4. Similarly, a specific settings object (subclass of AbstractSpecificSettings) can be serialized to string settings representation (SpecificSettingsSerializer.serialize) or can be translated into generic Settings (SpecificSettingsSerializer.toGenericSettings).

Example. Consider the following class:

    public static class MinmaxSpecificSettings 
             extends AbstractSpecificSettings {
        @PlcverifSettingsElement(name = "min")
        private int minimum;

        @PlcverifSettingsElement(name = "max", 
            mandatory = PlcverifSettingsMandatory.OPTIONAL)
        private int maximum = 100;
    }

The following textual generic settings can be parsed into a MinmaxSpecificSettings:

  -min = 10
  -max = 30

If the line -max = 30 is omitted, the field maximum will keep its initial value 100. If the line -min = 10 is omitted, the parsing will throw an exception.

Types of settings

When PLCverif is executed, the user has to provide a set of settings either as command line arguments, or in a separate file. However, the user does not have to specify each of the settings. There are various ways to provide / specify the settings, as listed below. The items are in order of precedence, the topmost having the highest precedence.

  1. User settings as command line arguments. The settings defined directly as command line arguments have the highest priority.
  2. User settings loaded from file. Such settings can be provided by passing a file name as the first argument to PLCverif. They are overwritten by eventual command line arguments. E.g., plcverif-cli script.txt -id=ID123 will set the id setting to ID123 even if the script.txt defines a different id.
  3. Installation-specific settings. These settings are optionally defined in the settings/<plugin_id>.settings files for each plug-in. (The path to the folder of installation-specific settings files is returned by PlatformConfig.getSettingsDirectory().) This allows the user to set up installation-specific settings, such as the location of external verification backends. These settings files will be loaded automatically by the platform (Platform) for the platform plug-ins, and they shall be loaded by the job plug-ins (implementers of IJobExtension, such as VerificationJobExtension). The other plug-ins should not check these files directly.
  4. Plug-in default settings. Plug-ins may contain default settings as resources (typically with name default.settings). The SettingsSerializer.loadDefaultSettings() method can be used to load the settings from the default.settings file. This is optional, especially if specific settings are used to handle the settings, and there are no platform-specific settings.

    The settings may be operating-system-specific, in those cases the typical names are default.${OS}.settings, where ${OS} is typically win32, linux or macos. The full list of possible platforms is in SettingsSerializer.SUPPORTED_OPERATING_SYSTEMS. The method SettingsSerializer.replaceOsPlaceholder can be used to replace the text ${OS} with the current operating system. The SettingsSerializer.loadOsSpecificDefaultSettings() method can also be used to load the settings from the default.${OS}.settings file.

  5. Default settings in the specific settings. If a plug-in uses the specific settings, the initial values defined for the fields representing optional settings elements will be taken into account, however these values have the lowest precedence. Note that these values should not be platform-specific.

results matching ""

    No results matching ""