Skip to content

0.2.0
Compare
Choose a tag to compare
@ondrej33 ondrej33 released this 22 Sep 21:05
· 41 commits to master since this release
v0.2.0
5dc65a5
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

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
Assets 2
Loading