Skip to content

#878 Accounting for runtime errors earlier during data based synthesis

Closes #878 (closed).

It's probably best to review commit-by-commit. Summary of changes:

  • I updated CifBddEdge to no longer use updateGuardErrorNot but to use updateGuard instead. Likewise for updateGuardErrorNotSupport.
  • I updated CifToBddConverter to strengthen all edge guards with not error.
    • At a few places, guard.and(error) (or the precomputed guardError) was being used. This no longer works since guard and error is now equivalent to origGuard and (not error) and error, which is equivalent to false. So instead, the original guards have to be used at any such place, e.g., in CifBddEdge#mergeEdges.
  • I moved the application of runtime errors from CifBddEdge#apply to a new method in CifToBddConverter. Now it's applied only once.
  • I simplified CifBddEdge#apply to reduce the number of function parameters. I also made some changes at other places as a consequence of that.
  • I updated practically all datasynth regression test cases (as well as a controller check test case) since the output is now different, plus the edge guards are now different. Nevertheless the synthesis results themselves are always the same (I checked all output files).
  • I ran the CIF benchmarks to see the impact on performance of these changes. The performance hasn't changed.

Summary of end user visible changes:

  • CIF data-based synthesis: prevention of runtime errors has been improved, taking them into account once before the main synthesis fixed point computations, rather than repeatedly during synthesis. As a result of this, more potential issues about events that are disabled may be detected and warned about before synthesis as well.
  • CIF data-based synthesis: the dependency sets of the workset algorithm now take into account the potential for runtime errors to occur as edges are applied.
  • CIF controller properties checker: it may now better handle models with runtime errors.
Edited by Dennis Hendriks

Merge request reports

Loading