1) We added support for all remaining template static properties. Currently, all templates are encoded into FO logic and then evaluated via the FOL evaluator. There are new methods to encode monotonicity (including the 'dual' case) and essentiality, as well as to encode that a property must be valid in a particular context.
2) We fully implemented the consistency checking. The check is now implicitly done whenever starting the inference workflow, as well as explicitly via a button. It now properly checks whether all IDs referenced in properties are valid, checks if dataset variables are valid, and checks all details regarding FOL and HCTL formulas (including context formulas of static properties).
Furthermore:
we added a button to hide all automatically generated regulation properties
we extended the data with a few additional models for testing
we simplified how sketch data are sent from the editor to the analysis session (when starting a new analysis)
we moved methods for encoding dynamic properties into the algorithms module
we fixed a few issues in the evaluation of FOL formulas
This PR focuses on two (interconnected) things:
1) We added support for all remaining template static properties. Currently, all templates are encoded into FO logic and then evaluated via the FOL evaluator. There are new methods to encode monotonicity (including the 'dual' case) and essentiality, as well as to encode that a property must be valid in a particular context.
2) We fully implemented the consistency checking. The check is now implicitly done whenever starting the inference workflow, as well as explicitly via a button. It now properly checks whether all IDs referenced in properties are valid, checks if dataset variables are valid, and checks all details regarding FOL and HCTL formulas (including context formulas of static properties).
Furthermore:
algorithms
module