1
UPPAAL에서 두 플립 플롭의 시간 모델을 모델링했습니다. 몇 가지 속성을 확인하려고했는데 6M 상태에 도달했고 노트북이 RAM에서 빠져 나왔습니다. 약 5Go가 소비되었고 누군가가 무엇을 말할 수 있습니까? UPPAAL이 처리 할 수있는 대략적인 주 번호입니까? UPPAAL에서 주 폭발을 다루기위한 가능한 기술은 무엇입니까?
당신에게UPPAAL의 상태 공간 폭발
A
답변
1
감사 상태의 수에 따라 달라집니다
사용할 수있는 메모리의 크기를. 32 비트 아키텍처에서는 4GB로 제한됩니다.
각 주 크기/발자국.
상태 공간의 모양과 탐사 순서.
기호 상태의 세분성 (제한 조건 간격의 범위 : 시간이 이산화 된 경우 기호 기술이 잘못 조정됩니다).
다음과 같은 방법을 시도 할 수 : 변수 CONST을 사용하지 않는 한 전이 통신 전용 변수를 표시 할 수 있습니다 때 제로로 변수를 설정 :
추상화를 적용하고 불필요한 변수를 제거 "메타"(이걸 남용하지 마라. 기괴한 행동으로 곤경에 처하게 될 것이다).
상태 공간 감소를 적극적으로 설정하여 공간 소비를 최적화하십시오.
부분 순서 감소, 대칭 감소를 적용합니다.
은 스윕 라인 방법을 적용합니다 (Uppaal 도움말에서 키워드 "진행률"을 찾으십시오).
자세한 내용은 Uppaal 튜토리얼을보십시오.
@mariusm에 감사드립니다. 자습서에서 UPPAAL이 부분 순서 축소를 지원하지 않는다고 설명했지만 대칭 감소 및 스윕 라인 방법을 이해하기 위해 노력 중입니다! 당신이 생각하는 다른 UPPAAL 버전에서도 지원 되었습니까? 4.1.19로 작업하십시오 –
Uppaal은 * automatic * partial order reduction을 지원하지 않지만, 여전히 모델을 부분적인 주문 감소 방식으로 만들 수 있습니다. – mariusm
내 모델을 구축하기 위해 UPPAAL의 그래픽 인터페이스를 사용하고 있다면 피드백을 위해 @mariusm을 보내 주셔서 감사합니다. 텍스트 버전 *으로 전환해야하는 것과 같이 UPPAAL의 부분 주문 감소 방식을 어떻게 따라야할까요? xta를 사용하고 내 모델을 최적화하는 알고리즘을 만들거나 UPPAAL의 그래픽 인터페이스에 남아 특정 방법론을 따르십니까? 감사합니다. –