#1110 CIF explorer gets various improvements/fixes relating to 'not too many initial states' precondition
requested to merge 1110-cif-explorer-crashes-due-to-inconsistent-calculations-of-number-of-possible-initial-states into develop
- Best to review per commit.
- End-user visible changes:
- The CIF explorer has various improvements and fixes relating to the precondition that there may not be too many initial states. These changes primarily prevent crashes and incorrect results. They may also lead to better estimates of the possible number of initial states, as well as improved output in case of a precondition violation. Performance of computing the initial states has also been improved in certain cases, but the tool could now give less feedback in case there is no initial state.
- Other changes:
-
SpecNoTooManyPossibleInitialStatesCheck
now maintainsCount
instead of separatevalue
andisPrecise
. More of the logic is now inCifValueUtils
. -
CifValueUtils.getPossibleInitialValuesCount(DiscVariable)
has multiple improvements:- Detect single explicit initial value expression as a special case, such that it can be indicated as a precise count. Improves for instance the precondition check output in certain cases. Could also improve performance.
- Improved a comment.
-
CifValueUtils.getPossibleInitialValuesCount(InputVariable)
now also returns aCount
, for consistency with discrete variables and automata, and to make it easier to handle them all in the same way. -
CifValueUtils.Count
has more invariants now, centralizing them in theCount
record, rather than having to check them in places of use:- The
value
must not beNaN
and not be negative. This prevents crashes. - It may only be precise if the
value
is finite. Essentially a sanity check.
- The
-
CifValueUtils.combine
has been added, to share the combine logic in a single place. It properly maintains the invariants of the class. This prevents crashes. -
Explorer
andExplorerBuilder
now useCifValueUtils
to determine which automata/variables may have no/multiple initial states, and how many, for consistency with the precondition check. This prevents crashes. -
Explorer
andExplorerBuilder
now don't only collect automata/variables with multiple possible initial locations/values, but also no locations/values and ones for which it can't be being statically decidable. I therefore renamed some fields/parameters/etc and improved some JavaDocs/comments. -
ExplorerBuilder.collectComponent
now uses newer java concepts and its comments have been reformatted to 120 characters line length. -
Explorer
handling of no potential initial states has been improved. If there is no initial state, nothing is computed for the state. This simplifies the code. It also greatly improves performance in certain cases, like when there is an automaton without initial locations but also some variables with very many initial locations. These changes may lead to less explorer warnings about why no initial state exists.
-
Closes #1110 (closed)
Edited by Dennis Hendriks