Currently, data-based synthesis can calculate an estimation or precise state space size of the controlled system, where the latter is obtained if the forward reachability is turned on. But this information is only presented if data-based synthesis is run in debug mode.
For use-case papers, we often report the state space size of the uncontrolled and controlled system. Therefore, I think it would fit better if this becomes an option under statistics and is being decoupled from the mode.
It feels like a different kind of statistics than BDD statistics, as it is not about the BDD representation of the (un)controlled behavior, but about how many states are represented, independently of how they are represented. Would we need a different statistics option for it?
I agree that it is not a BDD statistics, but Statistics is under Synthesis in the option menu, and also includes Timing (also not BDD specific). Therefore, I think it would fit there as an option.
Currently it is under debug mode, which does not feel right for a modeler, as obtaining this statistics has nothing to do with debugging the model nor the tool. Maybe it has some historical context why it is related to the debug mode?
Then maybe we need to move the option to a different category.
Or move the other BDD options to the BDD options window, where it is closer to all other BDD options. Then Timing remains a Synthesis statistic option.
Then maybe we need change the output mode under which it is printed from 'debug' to 'normal'.
That's also an option. Generating statistics often comes with additional calculation overhead (especially the BDD options we have), degregating the performance of synthesis significantly. Do you know whether obtaining the controlled system state space size (even the approximated version) has overhead? Having this under 'normal' implies that this statistic is always calculated. If the requires some overhead, maybe move it to a separate option that is by default disabled. If it does not really require much overhead, we can safely include it with the 'normal' output mode.
Or move the other BDD options to the BDD options window, where it is closer to all other BDD options. Then Timing remains a Synthesis statistic option.
Separating the options would be backward incompatible. Something to consider. Ideally we prevent that, if possible.
Do you know whether obtaining the controlled system state space size (even the approximated version) has overhead?
It involves calculating the number of satisfying assignments of a BDD.
Having this under 'normal' implies that this statistic is always calculated.
No. We would still have separate options to configure which statistics you want printed and what output you want to see. So changing the output mode that is used to 'normal', does not make that statistics are enabled by default.
If the requires some overhead, maybe move it to a separate option that is by default disabled.
We already have that option.
If it does not really require much overhead, we can safely include it with the 'normal' output mode.
The options to control the output mode and whether you want statistics to be printed are separate, and should remain separate options, I think.
No, there is no explicit option to calculate the uncontrolled state space. But you can still get this with some pre-processing of the specification. First you remove all requirements (use the CIf to CIF transformation for this) and then label all locations (and discrete variables if one uses a marked predicate for that) as marked. If you then input this specification to synthesis, the result equals the input, hence the 'controlled' state space is the uncontrolled state space of the plant models.
Yes, the purpose of this issue is not to get the uncontrolled state space automatically calculated. Just how to control as a end-user on how to obtain the currently calculated controlled system state space size number.