Promela에서 개체의 발사체 탄환을 모델링하고 모델의 일부 속성을 확인하려고합니다. 그러나 Promela에는 부동 소수점 데이터 형식이 없습니다. 예를 들어, 발사체 모션 매개 변수를 계산할 수 없습니다. 예를 들어 사인/코사인과 같은 삼각 함수를 계산할 수 없기 때문에 나는 발사체 모션을 모델링 할 수 없습니다.Promela의 부동 소수점 계산
이 문제를 해결할 수있는 방법은 무엇입니까? Promela에서 이러한 시스템을 모델링하는 방법은 무엇입니까?
Promela/SPIN에서 C 메모리가 철저하게 탐색 된 상태 공간의 일부로 간주되어야하는 사양을 포함하여 임의의 C 코드를 포함시킬 수 있습니다. 언어 구조를 살펴보십시오. c_code, c_decl, c_state, c_track 및 c_expr입니다.
일반적으로 부동 소수점 숫자를 포함하는 것이 좋습니다. 하나는 아니지만 확실히 하나 이상. 부동 소수점 값을 NOT 상태 공간의 일부로 만들 수있는 방법을 찾아야합니다.이 경우 중간 계산 값이거나 문제 공간을 discretize해야합니다. 이는 중요한 모델 검사 개념의 구체적인 예입니다. 정확하지만 계산 불가능한 모드와 거의 내용이없는 고급 모델 간의 적절한 추상화 수준을 찾습니다.
이와 관련하여 부동 소수점 숫자의 생략은 원래 PROMELA/SPIN 디자인에서 의식적으로 디자인 결정을 VERY입니다.
참고 : 귀하의 경우에는 입력 매개 변수가 하나 있고 출력 매개 변수가 '대상을 누르십시오'라는 단일 매개 변수가있을 수 있습니다. 그런 다음 모든 부동 소수점 계산은 중간 단계이며 누락 된 대상으로 이어지는 매개 변수의 조합과 같이 정확성 주장이 발견됩니다.
Promela가 이산 상태 공간을 모델링한다고 가정하면 "실제 숫자"(또는 부동 소수점 근사값)가 실제 문제가되는 것을 볼 수 있습니다. 얼마나 많은 주에서 "실제"값을 취할 수 있습니까? –
내 대답이 도움이 되었습니까? – GoZoner