CIF controller properties checker improvements/extensions overview
This issue provides an overview of issues relating to or listing improvements and extensions for the CIF controller properties checker. Some of the listed issues thus have additional list of their own, that are not repeated here.
- Adding new checks, and improvements on them:
-
#621 Improve bounded response check (various ideas) -
#410 Improve nonblocking under control check (various ideas) -
#891 Add uncontrollables-preserving property check to CIF controller properties checker -
#844 Change confluence check algorithm to a complete algorithm -
#894 Add 'runtime errors free' check to the CIF controller properties checker -
#937 (closed) CIF controller properties checker: improve debug output -
#407 Allow multiple checks to conclude partial confluence for a single event pair -
#977 (closed) CIF controller properties checker: warn if input model doesn't have input variables -
#1003 Confluence check: also check confluence for uncontrollable event pairs -
#1007 (closed) Confluence check: improve debug output in case of a single (controllable) event in the specification -
#1011 Confluence check: improve debug output to show what it is doing, and how it reached it conclusions -
#1008 (closed) Confluence check: improve termination checking responsiveness -
#1012 CIF controller properties checker: prevent constructing debug output if debug output is enabled -
#1050 CIF controller properties checker: add various BDD-related options from CIF data-based synthesis tool
-
- Potential adaptations needed to consistency with other tools:
-
#628 (closed) PLC code generators perform both controllable and uncontrollable events in any order -> superseded by #970 (closed) -
#896 (closed) Adapt CIF tools other than controller properties checker for 'controller:properties' annotation -
#970 (closed) Document and use a consistent transition execution order for CIF tools that use it -
#978 SBE process: explain steps also with example, hardware mapping, etc -
#1001 (closed) CIF execution scheme: change whether certain CIF to CIF transformations remove the controller properties annotation -
#1045 (closed) Add optional 'execution mode' to CIF simulator
-
- Performance of the checks:
-
#693 (closed) Controller checker: performance issue in converting updates of an edge to an MDD relation -
#695 (closed) Controller checker: checker is not very performant (mostly the confluence check) -
#911 CIF controller properties checker (BDD-based checks) OutOfMemoryError: Maximum size of node array reached -
#971 (closed) Improve bounded response check performance by checking only a single order -
#1000 Make new BDD library that supports parallelism, larger node tables and other types of decision diagrams -
#1004 (closed) Confluence check: improve performance by assuming the execution scheme (checking only for that order) -
#1005 Bounded response check: improve efficiency of the input variable events event loop -
#1006 (closed) Confluence check: improve performance by interleaving the zero variables -
#1010 (closed) Confluence check: improve performance by creating zero/old relations only for relevant variables
-
- Cleanups:
-
#893 Deprecate finite response check of the CIF controller properties checker -
#917 (closed) CIF 'ControllerCheckerApp' has too much code -
#1002 (closed) Confluence check: update outdated comment about zero-variables not being removed not affecting other checks -
#1009 (closed) Confluence check: introduce methods for separate checks (mutual exclusive, update equivalent, etc)
-
Edited by Dennis Hendriks