Releases: sybila/biodivine-hctl-model-checker
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
- algorithms from module
- there are new simplified aliases for some common complex types used within various functions/methods/classes:
LabelToSetMap
instead ofHashMap<String, GraphColoredVertices>
to map propositions to their valuationsVarDomainMap
instead ofBTreeMap<String, Option<String>>
for mapping of free variables to (optional) labels of their domainFormulaWithDomains
instead of(String, VarDomainMap)
for a sub-formula and mapping of its free variablesVarRenameMap
instead ofHashMap<String, String>
as a shorthand for mapping between variable names
- most significant changes in the
preprocessing
module:- submodule
node
was renamed to more fittinghctl_tree
HctlTreeNode
formulae representations are now serialized (and displayed) in the same format that can be parsed back- variants of operator enums
UnaryOp
andBinaryOp
were changed to uppercase in order to support new unified serialization - variant
NodeType::Hybrid
of theNodeType
enum now has an additionalOption<String>
field to represent the optional domain proposition; the same happens for the methodmk_hybrid
and for the variantHybrid
of theHctlToken
enum HctlTreeNode
has a new methodnew_random_boolean
for random generating propositional-logic trees- names of all of all
mk_*
methods ofHctlTreeNode
were shortened (such asmk_hybrid_node
->mk_hybrid
) - names of all variants of the
NodeType
enum were shortened (such asHybridNode
->Hybrid
) - utility function
check_props_and_rename_vars
is renamed tovalidate_and_rename_recursive
, and simplified wrappervalidate_props_and_rename_vars
is added - new utilities
validate_wild_cards
andvalidate_and_divide_wild_cards
- submodule
read_inputs
was removed, part of the functionality is redundant, part moved to moduleload_inputs
- submodule
- most significant changes in the
evaluation
module:- the
EvalContext
struct was extended with fieldsdomain_raw_sets
andfree_var_domains
to track how to evaluate variables during computation. Some of its methods take additional arguments due to this. The fieldcache
was also extended with domains. - in sub-module
canonization
, functionget_canonical_and_mapping
was changed to more meaningfulget_canonical_and_renaming
; a similar change happened to arguments of functioncanonize_subform
- rename sub-module
hctl_operators_evaluation
tohctl_operators_eval
- rename sub-module
mark_duplicate_subform
tomark_duplicates
- the
- other refactoring changes in the
model_checking
module- all of the main functions in module
model_checking
(such asparse_and_validate
ormodel_check_formula
) now take the formula as&str
instead ofString
- name of
parse_hctl_and_validate
is simplified toparse_and_validate
- name of
collect_unique_wild_card_props_recursive
is simplified tocollect_unique_wild_cards_recursive
- all of the main functions in module
- in module
analysis
:- functions
analyse_formulae
andanalyse_formula
now take two additional arguments with optional paths to input archive and output archive
- functions
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
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
andmodel_check_multiple_extended_formulae
for running the whole model-checking procedure on extended formulaeparse_extended_formula
andparse_and_minimize_extended_formula
to generate syntactic trees for extended formulaetry_tokenize_extended_formula
for tokenizing an extended formula- a new field of Enum
Atomic
calledWildCardProp
is added to represent the special properties in syntactic trees EvalContext
providesextend_context_with_wild_cards
method to extend the cache with "raw sets" regarding wild-card propositionsmark_duplicates_canonized_multiple
now also considers terminal wild-card-proposition nodes as duplicatescollect_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 suitableEvalContext
, 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
HctlTreeNode
s (such ascreate_hybrid
orcreate_unary
) are now provided as static methods of theHctlTreeNode
, with names such asmk_hybrid_node
ormk_unary_node
EvalContext
provides getterget_cache
check_hctl_var_support
now computes the number of unique variables internally, and thus, they don't have to be computed outsideHctlTreeNode::new
now generates the tree from HCTL tokens, instead of confusingly creating a constant default nodeHctlTreeNode::default
is removed because it was confusingmodel_check_trees
renamed tomodel_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 usedworkflow
issue that arose with the newesttarpaulin
is fixed