#878 Accounting for runtime errors earlier during data based synthesis
requested to merge wytseoortwijn/escet:878-accounting-for-runtime-errors-earlier-during-data-based-synthesis into develop
Closes #878 (closed).
It's probably best to review commit-by-commit. Summary of changes:
- I updated
CifBddEdge
to no longer useupdateGuardErrorNot
but to useupdateGuard
instead. Likewise forupdateGuardErrorNotSupport
. - I updated
CifToBddConverter
to strengthen all edge guards withnot error
.- At a few places,
guard.and(error)
(or the precomputedguardError
) was being used. This no longer works sinceguard and error
is now equivalent toorigGuard and (not error) and error
, which is equivalent tofalse
. So instead, the original guards have to be used at any such place, e.g., inCifBddEdge#mergeEdges
.
- At a few places,
- I moved the application of runtime errors from
CifBddEdge#apply
to a new method inCifToBddConverter
. 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