교착 상태 검사 Uppaal

Question

를 조회, 검증 오류로 중지 :

The verification was aborted due to an error. Most likely, this is caused by an out-of-range assignment or out-of-range array lookup.

이 암시 내 모델이 교착 상태임을 뜻

"범위를 벗어난 배열 또는 범위를 벗어나는 어레이 조회"가 발생할 때까지 무료입니까?

Answer 1

이 솔루션은 교착 상태가있을 경우 우리가 범위를 벗어 실행할 때, 그것이 있어야

A[] not deadlock || indexVarble => 24

처럼, 인덱스 변수 쿼리를 확장했다. (이 예에서는 범위가 [0-23])

Answer 2

UPPAAL이 쿼리에 응답 할 수있는 경우 상태 공간 검색을 계속하는 것은 의미가 없습니다. 따라서 UPPAAL에서 검색 할 수있는 상태 공간의 일부가 교착 상태가 아니라고 가정 할 수 있다고 생각합니다.

여러 추적을 통해 오류 상태에 도달 할 수 있지만 해당 모델의 종속 항목에 도달 할 수 있습니다.

이 오류가 발생하는 이유는 이미 알고있는 것 같습니다. 이 오류 상태로 끝나지 않도록 가드 !willCauseError()을 모델에 추가하여 문제를 해결할 수 있습니다. 그 자체로는 교착 상태가 발생할 수 있습니다. 이를 방지하려면 해당 위치의 전이를 반대 보호자 willCauseError()과 함께 자체에 추가 할 수 있습니다. 이렇게하면 프로그램이 교착 상태가 아닌 라이브 록 상태가됩니다. 교착 상태를 검사 할 때