Skip to content

#1110 CIF explorer gets various improvements/fixes relating to 'not too many initial states' precondition

  • 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 maintains Count instead of separate value and isPrecise. More of the logic is now in CifValueUtils.
    • 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 a Count, 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 the Count record, rather than having to check them in places of use:
      • The value must not be NaN and not be negative. This prevents crashes.
      • It may only be precise if the value is finite. Essentially a sanity check.
    • 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 and ExplorerBuilder now use CifValueUtils to determine which automata/variables may have no/multiple initial states, and how many, for consistency with the precondition check. This prevents crashes.
    • Explorer and ExplorerBuilder 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

Merge request reports

Loading