Quels types d'états et de transitions la "profondeur atteinte" de Spin prend-elle en compte?

Question

Pour les vérifications (avec ispin) que ne jamais utiliser les revendications, je reçois des sorties avec depth reached plus grand que le nombre d'états et le nombre de transitions, par exemple .:

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) 

Je trouve cela un peu unintuitive. Y a-t-il une description précise de la sémantique de "profondeur atteinte" quelque part (plus approfondie que pan's output format description)? Peut-être le sens de

le plus long chemin de recherche en profondeur d'abord contenait 87 transitions

ne se réfère pas aux 51 transitions, mais aux transitions des automates du système composé avec le ne prétendra jamais?

Answer 1

Oui, vous êtes (en quelque sorte) juste quand vous le dites se référer aux transitions de l'automate système composé avec le jamais réclamer. Pourtant, en même temps, c'est la longueur du chemin dans le système qui est vérifiée, car une étape du système composé sans revendication est exactement une étape du système. Bien sûr, en fonction de ne jamais prétendre, il peut être nécessaire d'explorer plus ou moins de transition que le système a. Les chemins ne sont même pas nécessaires sans boucle (en fonction de la réclamation) et même pas minimal (sauf si une option spéciale est définie).