nusmv

-1열

1답변

NuSMV 웹 사이트에서 파일을 다운로드했지만 시스템에서 실제로 응용 프로그램을 실행할 수 없습니다. 모든 리드가 인정 될 것입니다. , 빈, lib 디렉토리, 공유 당신은 커맨드 라인을 통해 그것을 실행해야합니다

1열

1답변

현재 시스템 프로토 타입을 전환 시스템 모델로 변환하려고합니다. 일부 LTL 속성이 있고 모델 검사 도구 NuSMV를 사용하여 이러한 속성을 확인하려고합니다. 필자는 단지 원자 속성 및 기타 수학적 측면을 정의하여 모델링을 시작하는 방법에 대한 정보만을 제공합니다. NuSMV 그 전환 시스템의에 Pictorial Representation of Model

1열

2답변

NuSMV 적어도 5 시간 걸려 승리하려면

나는 NuSMV 프로그램을 가지고 있으며 CTL 또는 LTL에서 프로그램 (게임)을 5 단계 미만으로 획득 할 수 없다고 명시해야합니다. 또는 더 형식적 : 게임을 승리하기 위해 적어도 5 단계의 단계가 필요합니다. 나는 명시적인 시간 변수가 없으므로 확인을 위해 만들고 싶지 않습니다. 이미 만들어진 전환 양을 계산할 수있는 방법이 있습니까? 방문한 국가의

0열

1답변

NuSMV에서 전역 상수를 어떻게 정의 할 수 있습니까?

나는 C에 #define n 5 유사한 방식으로, NuSMV에 전역 상수를 선언하는 방법을 모르겠어요. NuSMV에서 어떻게 할 수 있습니까?

-2열

1답변

UPPAAL 또는 NuSMV를 사용한 엘리베이터 컨트롤

저는 NuSMV 및 UPPAAL을 처음 사용하며이 문제를 해결하기 위해 노력하고 있습니다. 다음 질문 중 하나를 해결할 수 있습니까? 모델 (5 4 말 또는)과 liXs의 번호 (예를 들어 2 또는 3) 숫자와 바닥의 수를 제공하여 자신의 디자인의 엘리베이터 시스템의 제어 시스템을 분석 사용자가 개별 층에 있으며 서로 젤에 대한 개별적인 희망이 있습니다 층

1열

1답변

NuSMV에서 간단한 Kripke 모델을 만드는 방법은 무엇입니까?

저는 현재 LTL (Linear-time Temporal Logic)과 CTL (Computation Tree Logic)에 대한 이론적 연구를하고 있습니다. 나는 NuSMV를 처음 사용하고 있으며 간단한 Kripke 구조를 만드는 데 어려움이 있습니다. 내 구조는 다음과 같습니다. S = {s0, s1, s2}는 가능한 상태 집합, R은 다음과 같은 전이

1열

1답변

모델 검사기를 사용하여 하나의 특정 추적을 확인하십시오.

오픈 상호 작용 프로토콜에 대한 규칙을 정의하기 위해 LTL을 사용하고 있습니다. 그런 다음 특정 상호 작용이 사양을 따르는 지 또는 규칙이 깨져 있는지 확인하려고합니다. 나의 즉각적인 접근 방식은 NuSMV를 사용하는 것이었지만 문제는 내가 확인하고자하는 상호 작용의 모델이 아니라 단지 하나의 특정 유한 추적 (모든 주에서 모든 변수의 값)이라는 것입니다

2열

1답변

xSAP 오류

내가 xSAP (버전 1.2.0)는 SMV 모델에 전달하려고했지만, 내가 모델은 NuSMV (버전 2.6.0와 잘 작동이 오류 [email protected]:~/Desktop$ python /home/panda/Desktop/xSAP/scripts/extend_model.py -v /home/panda/Desktop/brca.smv /home/panda/

1열

1답변

NuSMV에서 UART의 공식 모델을 구축 하시겠습니까?

저는 교육에 대한 모델 검사와 NuSMV를 배우고 있습니다. NuSMV 코드를 편집하고 실행할 수 있으며 UART가 무엇인지에 대해 공정하게 이해하고 있습니다. 내 작업은 공식적으로 NuSMV로 UART를 모델링하는 것이지만 현재로서는 어떻게해야할지 모르겠다. UART가 8 바이트 순차 비트로 1 바이트를 전송한다는 것을 알고 있지만 어떻게 모델링 할 수

1열

1답변

사양 실행 중에 NuSMV가 사용할 수있는 메모리 양을 늘릴 수있는 옵션이 있습니까?

nusmv에서 실행되는 사양 중에 몇 시간이 걸리며 결과적으로 "kill 9"가 반환됩니다. 실행 속도를 높이려면 어떻게해야합니까? 사양 실행 중에 NuSMV가 사용할 수있는 메모리 양을 늘릴 수있는 옵션이 있습니까?