spin

1열

1답변

스핀을 이용한 Promela 모델링

저는 매우 간단한 promela 모델을 만들고 있습니다. 두 개의 다른 모듈을 사용하여 횡단 보도/교통 신호등의 역할을합니다. 첫 번째 모듈은 현재 신호 (녹색, 빨간색, 노란색, 보류 중)를 출력하는 신호등입니다. 이 모듈은 또한 "보행자"라는 신호를 입력으로받습니다.이 신호는 교차하려는 보행자가 있음을 나타내는 지표 역할을합니다. 두 번째 모듈은 횡단면

model-checking spin promela 2017-04-06

---

2열

1답변

Jspin에서 mtype을 사용할 때 선언되지 않은 변수 오류

나는 Jspin 및 Promela을 처음 사용합니다. 개인 ID 키 또는 암호를 사용하여 집 경보 시스템을 활성화 및 비활성화 할 수 있습니다. 활성화 후 시스템은 사용자가 대피 할 수있는 대기 시간 (약 30 초)으로 들어갑니다. 경보가 발령 된 보안 구역, 침입이 감지 된 경우에도 경보가 울리는 시간 또는 15 초의 지연이 내장되어있어 침입자가 암호를

model-checking promela spin 2017-11-08

---

1열

1답변

Proctype 오류가 Promela SPIN에 전달되지 않았습니다.

저는 SPIN 및 Promela에 대해 매우 익숙하며 내 모델에서 활성 속성을 확인할 때이 오류를 발견했습니다. 오류 코드 : unreached in proctype P (0 of 29 states) unreached in proctype monitor mutex_assert.pml:39, state 1, "assert(!((mute

cygwin mutual-exclusion model-checking spin promela 2016-10-11

---

2열

1답변

Error : VECTORSZ가 너무 작습니다.

Promela 및 특히 SPIN에서 일하는 것이 처음입니다. 나는 문제를 해결하기 위해 SPIN의 출력을 이해할 수없는 모델을 가지고 있습니다. 여기 내가 무슨 짓을 : pan:1: VECTORSZ is too small, edit pan.h (at depth 0) pan: wrote untitled.pml.trail (Spin Version 6.4.

concurrency formal-verification model-checking promela spin 2017-11-22

---

0열

1답변

SPIN 모델의 최대 프로세스 수

여러 개의 프로세스가 생성되어 다른 프로세스가 생성됩니다. 따라서 SPIN 모델은 "너무 많은 프로세스 (Max 255)"인쇄를 유지합니다. 그러나, 그것은 여전히 ​​나에게 최종 결과를주고있다. 255 개가 넘는 프로세스를 처리 할 수 ​​없다면 어떻게 최종 결과를 얻을 수 있습니까?

spin promela 2014-12-05

---

0열

1답변

Promela 구문 오류 : 오류 : 불완전한 구조 참조 '테이블'\t saw 'operator : ='

다음과 같은 typedef가 있습니다. PUB 유형은 두 개의 int를 유지하며 pub_table은 게시자와 int 배열을 유지합니다. typedef pub{ int nodeid; int tid }; typedef pub_table{ pub table[TABLE_SIZE]; int last }; 다음 라인 나는

spin promela 2015-02-01

---

1열

1답변

SPIN 모델 검사기에서 최대 검색 깊이를 너무 작게 해결하는 방법은 무엇입니까? 가능한 이유는 무엇입니까?

내 모델 검증을하는 동안 나는이 오류를 얻고있다 는 컴파일 문자열 tesTdma.pml -a 스핀 최대 검색 깊이가 너무 작고, 깊이 = 9999 주 I입니다 이 오류의 원인을 이해하지 못합니다. 나요 누군가가 1.1.4과 SPIN 버전이 사용 ISPIN 건너 온 6.4.7

formal-verification model-checking spin formal-methods 2017-12-12

---

2열

1답변

Promela에서 배열 요소의 비 결정적 값을 선택할 수 있습니까?

다음은 내가 작성중인 Promela 코드입니다. 내가 코드를 시뮬레이션하려고하면 491 byte api1[5]; 492 byte api2[5]; 493 byte api3[5]; 494 byte reftask1[5] 495 byte reftask2[5]; 496 byte reftask3[5]; 497 byte rid1[5]; 498

spin promela 2016-09-26

---

1열

1답변

promela에서 대기열을 모델링하는 방법은 무엇입니까?

좋아요, 그래서 Promela에서 CLH-RW lock을 모델로 만들려고합니다. 잠금이 작동 방법은 정말 간단하다 : 큐는 tail 구성이있는 독자와 작가 모두 새로운 노드를 생성하고 CAS는 - 보내고하여 하나의 bool succ_must_wait 그들이 그렇게 포함하는 노드를 대기열에 그것은 tail입니다. 그러면 꼬리가 노드의 전신 인 pred이됩니다

multithreading locking model-checking promela spin 2017-11-03

---

1열

1답변

스핀에서 여러 (또는 모두) 위반 추적을 요청하십시오.

스핀을 사용하여 속성에 대해 여러 (또는 모두) 위반 추적을받을 수 있습니까? byte mutex = 0; active proctype A() { A1: mutex==0; /* Is free? */ A2: mutex++; /* Get mutex */ A3: /* A's critical section */ A4: mutex--; /* Release

model-checking spin promela 2016-08-30

---