promela

1열

1답변

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

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

1열

1답변

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

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

2열

1답변

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

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

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

1열

1답변

PROMELA 프로세스에서 시간 초과/교착 상태없이 송수신하는 방법은 무엇입니까?

PROMELA 문제로 머리를 감쌀 수 없습니다. 채널 ("to_pc")을 통해 메시지를 보내고받을 수있는 N 개의 프로세스 ("pc")가 있습니다. 각 프로세스에는 메시지를 수신하는 자체 채널이 있습니다. 프로세스가 수신하려면 들어오는 메시지의 채널을 확인하는 루프를 유지해야합니다. 두 번째 루프 옵션으로 프로세스는 다른 모든 채널에 메시지를 전송합니다.

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

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.

0열

1답변

SPIN 모델의 최대 프로세스 수

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

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 }; 다음 라인 나는