Expand description
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 (partially specified) BNs.
- Various formulae pre-processing utilities, such as tokenizing, parsing, or 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.
- generate_
output - load_
inputs - Contains wrappers for loading inputs from the files
- mc_
utils - Model checking utilities such as generating extended STG or checking if an STG supports enough sets of symbolic variables.
- 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 responsible for the preprocessing of HCTL formulae before model checking.
- result_
print - Print results of the computation, either aggregated version only, or a full set of satisfying states.