Crate biodivine_hctl_model_checker

A small library regarding analysis of dynamic properties of Boolean networks through HCTL model checking. As of now, the library supports:

• Model-checking analysis of HCTL properties on a (partially specified) BNs.
• Various formulae preprocessing utilities, such as tokenizing, parsing, or some canonization.
• Manipulation with abstract syntactic trees for HCTL formulae.
• Searching for common sub-formulae across multiple properties.
• Optimised evaluation for several patterns, such as various attractor types or reachability.
• Simultaneous evaluation of several formulae, sharing common computation via cache.

Modules

• analysis
  Model-checking analysis from start to finish, with progress output and result prints.
• evaluation
  Components regarding the evaluation of formulae, including the main model-checking algorithm.
• mc_utils
  Model checking utilities such as generating extended STG or checking STG for variable support.
• model_checking
  High-level functionality regarding the whole model-checking process. Several variants of the model-checking procedure are provided:
• postprocessing
  Components regarding the postprocessing of model-checking results.
• preprocessing
  Components regarding the preprocessing of HCTL formulae, e.g., tokenizing, parsing, validating, or renaming of variables.
• result_print
  Print results of the computation, either aggregated version only, or a full set of satisfying states.