ultimate-pa/hanfor

Variable mass-import

Closed this issue · 1 comments

Requirements documents may include a list of known observables, types and possibly invariants for the observable.
One should be able to import such document into a Hanfor session to add the variables all at once.

Format for a requirement import could be csv formatted

{name, description, enum_name, type, value, invariant}

with enum_name signifying the enum name if applicable (else empty) and invariant being the observable of an "Generally, it is always the case that observable holds" pattern. Alternatively bounds could be given for the last. For constants, value has to be filled and type is CONST, else value has to be empty. Description can be any text, storing additional text could be useful when mass importing.

e.g.

my_varname, "this is a description of the variable",, int,,,
an_enum_type, "this is the enum type",, enum_int,,,
an_enum_value,, an_enum_type,,1,,
another_enum_value,, an_enum_type,,2,,
a_constant,"this is a constant,,,3.2,
var_with_invariant,"""this var has an invariant""",,real,"",, var_with_invariant > 10.0 && var_with_invariant < 100.0
an_enum_type_w_invar, "this is the enum type",, enum_int,,,"an_enum_type_w_invar > 0"
an_other_enum_value,, an_enum_type_w_invar,,1,,
hauff commented
  • The import button is located at Variables > Import > Import CSV

    image

  • Restrictions

    • the import will silently fail if there are any errors during import (e.g. ENUM does not exist or variable type is unsupported)
    • the types are case sensitive: bool, int, real must be written in lower case, all other types in upper case
    • ENUMs must be declared before its corresponding ENUMERATORs
    • existing variables will be ignored
  • An example of an input csv, that contains all supported types of variables

    "name","enum_name","description","type","value","constraint"
    "integer_constant",,"variable description","CONST","0","integer_constant >= 0 && integer_constant <= 0"
    "real_constant","integer_constant","variable description","CONST","0.0","real_constant >= 0.0 && real_constant <= 0.0"
    "boolean_variable",,"variable description","bool",,"boolean_variable != false"
    "integer_variable",,"variable description","int",,"integer_variable >= 0 && integer_variable <= 10"
    "real_variable",,"variable description","real",,"real_variable >= 0.0 && real_variable <= 10.0"
    "integer_enum",,"variable description","ENUM_INT",,"integer_enum >= 0 && integer_enum <= 10"
    "integer_enum_enumerator_0","integer_enum","variable description","ENUMERATOR_INT","0",
    "real_enum",,"variable description","ENUM_REAL",,"real_enum >= 0.0 && real_enum <= 10.0"
    "real_enum_enumerator_0","real_enum","variable description","ENUMERATOR_REAL","0.0",