Для проверок (с ispin), в которых никогда не используются утверждения, я получаю выходные данные с depth reached большим, чем количество состояний и количество переходов, например:
Full statespace search for:
never claim + (REQ5)
assertion violations + (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by never claim)
State-vector 60 byte, depth reached 87, errors: 1
41 states, stored
10 states, matched
51 transitions (= stored+matched)
9 atomic steps
hash conflicts: 0 (resolved)
Я нахожу это немного неинтуитивным. Есть ли где-нибудь точное описание семантики "достигнутой глубины" (более подробное, чем вывод pan описание формата)? Может быть, смысл
самый длинный путь поиска в глубину содержал 87 переходов
относится не к 51 переходу, а к переходам системных автоматов, составленных с претензией никогда?
