Skip to content

more doc handling of prop_universal for fused initial states

Alexandre Duret-Lutz requested to merge adl/560 into next

Fixes #560 (closed).

  • spot/parseaut/parseaut.yy: Add more comments about handling of prop_universal in present of multiple initial states. It took me time to figure out that it was done correctly. Also only reset prop_complete() in the case an initial state is reused.
  • tests/core/det.test: Add a test case for the deterministic property.
  • tests/python/parsetgba.py: Add tests for complete.
  • doc/org/hoa.org: Add more text about the effect of fusing initial states.
  • doc/org/concepts.org (properties): Replace "deterministic" by "universal". The former was obsoleted in Spot 2.4.

Merge request reports