Algorithms that do not Generate a Counter Example
- Project integrity check
- Project meet
- Project sync
- Project synthesis
- BDD meet
- BDD sync product
- BDD synthesis
- Level wise synthesis
- BDD subsystem level wise synthesis
- Check LD interface
- All distributed algorithms
Moreover, no counter example is generated in the following scenarios:
- Every algorithm first checks the project integrity, if the integrity fails the algorithm is not run; so no counter example is generated.
- If the interface consistency check fails at point 2, no counter example is generated.
- The SD controllability check and the S Singular prohibitive behaviour check are currently combined, if the result of these tests is not determined, no counter example is generated.