0.3.4

(this summary is LLM-generated, but validated by project developers)

Changes Since v0.3.3

API-breaking changes

• 🛠️ The minimum supported Rust version (MSRV) has been increased to 1.88.0. Projects using this library must now be compiled with Rust 1.88.0 or newer.

Other changes

• 🦀 The library has been migrated to the Rust 2024 edition, adopting the latest language features and idioms.
• 📦 Core dependencies have been updated to their latest compatible versions, including biodivine-lib-bdd, biodivine-lib-param-bn, clap, and termcolor.
• ✨ The codebase has been updated to adhere to the new formatting rules and clippy lints associated with the Rust 2024 edition, enhancing code quality and consistency.
• 🤖 The continuous integration (CI) pipeline has been significantly improved by transitioning to reusable workflows for building, validation, and automated releases.

0.3.3

(this summary is LLM-generated, but validated by project developers)

Changes Since v0.3.2

New features

• ✨ Added progress tracking capabilities to model-checking functions for extended formulae (those containing wild-card propositions). This is exposed through the following new functions which accept a progress_callback:
  • _model_check_extended_formula
  • _model_check_extended_formula_dirty
  • _model_check_multiple_extended_formulae
  • _model_check_multiple_extended_formulae_dirty

Bug fixes

• Fixed a typographical error in an internal source code comment.

Other changes

• ⚙️ The Rust version used in the continuous integration pipeline has been updated to 1.86.0.

0.3.2

(this summary is LLM-generated, but validated by project developers)

Changes Since v0.3.1

API-breaking changes

• The signature of the public function evaluation::algorithm::eval_node has been changed. It now accepts an additional progress_callback argument, which is a function that can be used to monitor the progress of the evaluation.

New features

• ✨ A progress tracking mechanism has been introduced to the model-checking algorithm (resolves #20). For each public function in the model_checking module (e.g., model_check_formula), a new "underscored" variant (e.g., _model_check_formula) is now available. These variants accept a callback function to report on intermediate computation progress, such as the start of a new sub-formula evaluation or the BDD size during fixed-point computations. The original API remains unchanged and does not report progress by default.

Other changes

• The Rust version used for continuous integration has been updated to 1.85.0.
• The internal evaluation algorithm has been refactored to accommodate the new progress reporting feature.
• Minor internal code style improvements have been implemented.

0.3.1

(this summary is LLM-generated, but validated by project developers)

Changes Since v0.3.0

New features

• HCTL formula syntax has been extended to support an alternative long-form notation for hybrid operators. Alongside the existing short-hand symbols, you can now use named operators prefixed with a backslash: \bind, \jump, \exists, and \forall. For example, a formula can now be written as \bind {x}: AG EF {x}. The default serialization format remains the short-hand version. (#19) ✨

Other changes

• The continuous integration (CI) workflow has been updated to use more modern GitHub Actions and improve build times.
• Dependencies on biodivine-lib-bdd and biodivine-lib-param-bn have been updated. ⬆️

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.

0.2.2

(this summary is LLM-generated, but validated by project developers)

Changes Since v0.2.1

Bug fixes

• The sanitization functions (sanitize_colored_vertices, sanitize_colors, sanitize_vertices) no longer require the SymbolicAsyncGraph to have an associated BooleanNetwork. This change prevents a potential panic, making the functions more robust. 🐛
• Added internal verification to ensure that formulas using the binder operator (e.g., !{x}: FORMULA) are correctly evaluated as equivalent to their universal quantifier counterpart (V{x}: ({x} => FORMULA)), improving the reliability of the model checker. ✅

Other changes

• The dependency on biodivine-lib-param-bn has been updated to version 0.5.1 or newer. 📦

0.2.1

(this summary is LLM-generated, but validated by project developers)

Changes Since v0.2.0

API-breaking changes

• This version updates its core dependency biodivine-lib-param-bn to version 0.5.0 or newer. This update introduces several breaking changes from the dependency that are reflected in this library's API:
  • Methods on SymbolicAsyncGraph that previously accessed the underlying BooleanNetwork (e.g., graph.as_network().variables()) have been changed. Many of these properties, such as variables() and num_vars(), can now be accessed directly on the SymbolicAsyncGraph instance.
  • The SymbolicAsyncGraph::as_network() method now returns an Option<&BooleanNetwork>.
  • Methods for creating empty sets, such as SymbolicAsyncGraph::mk_empty_vertices, have been replaced with their colored counterparts, like SymbolicAsyncGraph::mk_empty_colored_vertices.
• The formula parsing functions preprocessing::parser::parse_and_minimize_hctl_formula and preprocessing::parser::parse_and_minimize_extended_formula now require a SymbolicContext as an argument instead of a BooleanNetwork.
• The public function postprocessing::sanitizing::sanitize_bdd has been removed. Its functionality has been superseded by the SymbolicContext::transfer_from method in biodivine-lib-param-bn.
• The function signature for mc_utils::get_extended_symbolic_graph has been updated to accept a borrowed &BooleanNetwork instead of an owned value.

New features

• ✨ Added new "dirty" model checking functions: model_check_extended_formula_dirty and model_check_multiple_extended_formulae_dirty. These versions skip the final sanitization step of removing auxiliary HCTL variables from the result, which can offer a performance benefit in specific use cases.

Other changes

• The library's dependencies on biodivine-lib-bdd and biodivine-lib-param-bn have been updated to versions >=0.5.7 and >=0.5.0 respectively.
• The internal implementation for sanitizing model checking results has been refactored to use the generalized BDD transfer functionality now provided by biodivine-lib-param-bn, removing redundant code. (PR #12)

0.2.0

A second "major" release of HCTL model checker. The new functionality revolves around adding "wild-card propositions" (described below). There are also some further changes to the public API. Some more changes are expected in the future 0.3.0, as there is still a lot of refactoring of the project to be done. However, we are hopefully getting closer to a stable 1.0.0 release.

Wild-card propositions are special propositions that are evaluated as an arbitrary (coloured) set given by the user. This allows, for instance, the re-use of already pre-computed results in subsequent computations. In formulae, we now allow including such properties as %property_name%.
Note that the BDD representation of provided coloured sets (to which wild-card propositions are evaluated) must contain the same symbolic variables as the original extended STG.

We provide the following new functionality with regard to the evaluation of the wild-card propositions:

• model_check_extended_formula and model_check_multiple_extended_formulae for running the whole model-checking procedure on extended formulae
• parse_extended_formula and parse_and_minimize_extended_formula to generate syntactic trees for extended formulae
• try_tokenize_extended_formula for tokenizing an extended formula
• a new field of Enum Atomic called WildCardProp is added to represent the special properties in syntactic trees
• EvalContext provides extend_context_with_wild_cards method to extend the cache with "raw sets" regarding wild-card propositions
• mark_duplicates_canonized_multiple now also considers terminal wild-card-proposition nodes as duplicates
• collect_unique_wild_card_props to get all unique wild-card propositions in a tree

Some further refactoring changes and other code improvements include:

• EvalInfo struct is renamed to a more suitable EvalContext, and similarly, the module name is changed (eval_info -> eval_context)
• function collect_unique_hctl_vars does not take the (initially empty) HashSet anymore, but instead creates it internally and calls an internal recursive sub-procedure
• functions to generate various versions of HctlTreeNodes (such as create_hybrid or create_unary) are now provided as static methods of the HctlTreeNode, with names such as mk_hybrid_node or mk_unary_node
• EvalContext provides getter get_cache
• check_hctl_var_support now computes the number of unique variables internally, and thus, they don't have to be computed outside
• HctlTreeNode::new now generates the tree from HCTL tokens, instead of confusingly creating a constant default node
• HctlTreeNode::default is removed because it was confusing
• model_check_trees renamed to model_check_multiple_trees for consistency

There are also the following little changes to the overall project:

• slight refactoring and documentation improvements, but there is a lot of work to be done (focus of the future release)
• test suite is extended (but refactoring and modifications are still needed in future)
• githooks are removed, as they were not used
• workflow issue that arose with the newest tarpaulin is fixed

0.1.7

The first released stable version of the HCTL model checker.