0.3.0

A third "major" release of the HCTL model checker. This time, the changes are centred around extending functionality regarding "wild-card propositions" and the addition of optional "variable domains" (described below) to the formulae. Other changes come with the project's more extensive refactoring and restructuring (changes in modules).

Domains of quantified variables can now be restricted directly in HCTL formulae. The logic behind these variable domains is similar to wild-card propositions introduced in version 0.2.0. Basically, you specify a special "domain proposition" and an arbitrary (coloured) set to which it will evaluate. The syntax is following: !{x} in %domain%:, and the same goes for other quantifiers. This way, the user can directly restrict the domain of every {x} encountered during bottom-up computation (makes the formula more readable and speeds up the computation). See #17 for more details. This part required extending many public methods, but mainly to modify internal parts of the parsing, evaluation, and caching.

The refactoring part is mainly concerned with the following things:

• simplify or remove redundant and unnecessary methods/trait implementations
• restructure the test suite and improve documentation (both doc strings and comments)
• simplify and shorten complex method/struct/function/variable names
• simplify complex types, make new types/aliases

Also, some bugs were fixed, mostly in the parser (whitespaces after quantifiers are now parsed correctly, and some new edge cases are now handled).

The following things changed in the library's API:

• changes in top-level modules:
  • algorithms from module aeon were moved to an internal module _aeon_algorithms
  • new module for loading inputs from files or archives - load_inputs
  • new module to generate result archives - generate_output
  • all of the complex model-checking tests were moved to a separate internal test module, _test_model_checking
• there are new simplified aliases for some common complex types used within various functions/methods/classes:
  • LabelToSetMap instead of HashMap<String, GraphColoredVertices> to map propositions to their valuations
  • VarDomainMap instead of BTreeMap<String, Option<String>> for mapping of free variables to (optional) labels of their domain
  • FormulaWithDomains instead of (String, VarDomainMap) for a sub-formula and mapping of its free variables
  • VarRenameMap instead of HashMap<String, String> as a shorthand for mapping between variable names
• most significant changes in the preprocessing module:
  • submodule node was renamed to more fitting hctl_tree
  • HctlTreeNode formulae representations are now serialized (and displayed) in the same format that can be parsed back
  • variants of operator enums UnaryOp and BinaryOp were changed to uppercase in order to support new unified serialization
  • variant NodeType::Hybrid of the NodeType enum now has an additional Option<String> field to represent the optional domain proposition; the same happens for the method mk_hybrid and for the variant Hybrid of the HctlToken enum
  • HctlTreeNode has a new method new_random_boolean for random generating propositional-logic trees
  • names of all of all mk_* methods of HctlTreeNode were shortened (such as mk_hybrid_node -> mk_hybrid)
  • names of all variants of the NodeType enum were shortened (such as HybridNode -> Hybrid)
  • utility function check_props_and_rename_vars is renamed to validate_and_rename_recursive, and simplified wrapper validate_props_and_rename_vars is added
  • new utilities validate_wild_cards and validate_and_divide_wild_cards
  • submodule read_inputs was removed, part of the functionality is redundant, part moved to module load_inputs
• most significant changes in the evaluation module:
  • the EvalContext struct was extended with fields domain_raw_sets and free_var_domains to track how to evaluate variables during computation. Some of its methods take additional arguments due to this. The field cache was also extended with domains.
  • in sub-module canonization, function get_canonical_and_mapping was changed to more meaningful get_canonical_and_renaming; a similar change happened to arguments of function canonize_subform
  • rename sub-module hctl_operators_evaluation to hctl_operators_eval
  • rename sub-module mark_duplicate_subform to mark_duplicates
• other refactoring changes in the model_checking module
  • all of the main functions in module model_checking (such as parse_and_validate or model_check_formula) now take the formula as &str instead of String
  • name of parse_hctl_and_validate is simplified to parse_and_validate
  • name of collect_unique_wild_card_props_recursive is simplified to collect_unique_wild_cards_recursive
• in module analysis:
  • functions analyse_formulae and analyse_formula now take two additional arguments with optional paths to input archive and output archive

Many of these changes are now also available as part of the tool itself, not just the library. The model checker can now load an archive with BDDs to be substituted for the wild-card properties and variable domains. It can also generate an archive with resulting BDDs. For details of how the CLI tool currently behaves, see the main README file. These changes also correspond to changes in the module analysis, as mentioned above.

Other minor changes in the project:

• The minimal Rust version in the CI was set to 1.77.0.