Skip to content

sbacc: remove spurious initial state in some output

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

This fixes #492 (closed), based on a report from Jérôme Dubois.

  • spot/twaalgos/sbacc.cc: If the initial state is in a rejecting component, start with an initial state whose colors are unsat_mark.
  • tests/core/sbacc.test: Add test case.
  • tests/python/pdegen.py: Adjust it.

Merge request reports