У меня есть программа, которая использует каналы для обмена сообщениями между процессами. Это сводит меня с ума.
Когда я запускаю свою программу, набирая:
spin ipc_verify.pml
Она работает нормально (показано отпечатками в моей программе) и выходит изящно, как и планировалось. Тем не менее, когда я пытаюсь проверить, выполнив следующее:
spin -a ipc-verify.pml
gcc -DVECTORSZ=4096 -DVERBOSE -o pan pan.c
./pan
Сбой в первом операторе на сервере, где сервер пытается прочитать на канале, с ошибкой:
pan:1: missing pars in receive (at depth 20)
Кажется, я упускаю что-то очень простое, но не могу понять это. Я новичок в Spin, делаю это как часть моей курсовой работы, поэтому прошу прощения, если это простой, глупый вопрос.
Вот краткое описание программы: Программа запускает 3 процесса - 1 сервер и 2 клиента. Клиент отправляет число на сервер, который отвечает квадратом числа. Существует канал запроса, по которому каждый клиент отправляет свой запрос (сообщение имеет идентификатор клиента, с помощью которого сервер знает, на какой клиент отвечать), и канал ответа, по которому сервер отправляет ответ клиентам. Клиенты используют случайный прием на канале, чтобы найти сообщение для своего идентификатора.
Строка кода, в которой, как мне кажется, она терпит неудачу, такова:
:: ch_clientrequest ? msgtype, client_id, client_request ->
У меня на самом деле есть большая программа, демонстрирующая такое поведение, поэтому я попытался воспроизвести ее в этой программе. Я прочитал различные способы увидеть больше информации об этой ошибке, а также погуглил. Также попытался изменить структуру сообщения, больше полей, меньше полей, не делать случайный прием, а получать регулярно, и т. Д. c. Ничто не может изменить эту ошибку!
Вот полная трассировка ошибок при запуске ./pan:
pan:1: missing pars in receive (at depth 20)
pan: wrote ipc-verify.pml.trail
(Spin Version 6.5.1 -- 20 December 2019)
Warning: Search not completed
+ Partial Order Reduction
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 2104 byte, depth reached 20, errors: 1
21 states, stored
0 states, matched
0 matches within stack
21 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
stackframes: 0/0
stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
Stats on memory usage (in Megabytes):
0.043 equivalent memory usage for states (stored*(State-vector + overhead))
1.164 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
129.315 total actual memory usage
Я пытался найти, что означает это сообщение во время выполнения при проверке, но не смог найти много , Основываясь на различных экспериментах с кодом, кажется, что верификатор считает, что сообщение, которое я пытаюсь получить, должно иметь больше параметров, чем то, что я пытаюсь прочитать. Я пытался увидеть, реагирует ли оно на фактическое полученное сообщение, и, возможно, в нем меньше полей, но, похоже, это не так.
Я бился головой об этом сегодня целый день без всяких поводов. Любые указатели или идеи, чтобы решить эту проблему, будут очень признательны. Я запускаю это на своей linux коробке, Spin 6.5.
/*
One hub controller (server), 8 clients.
Each client sends a message to the hub, hub responds with the message it received.
*/
#define N 2 // Number of clients
#define MQLENGTH 100
mtype = {START_CLIENT, COMPUTE_REQUEST, COMPUTE_RESPONSE, STOP_CLIENT, STOP_HUB}
typedef ClientRequest {
byte num;
}
typedef HubResponse {
bool isNull; // To indicate whether there is data or not. Set True for START and STOP messages
int id;
byte num;
int sqnum;
}
typedef IdList {
byte ids[N]; // Use to store the ids assigned to each client process
}
IdList idlist;
chan ch_clientrequest = [MQLENGTH] of {mtype, byte, ClientRequest} // Hub listens to this
chan ch_hubresponse = [MQLENGTH] of {mtype, byte, HubResponse} // Clients read from this
int message_served = 0
proctype Client(byte id) {
// A client reads the message and responds to it
mtype msgtype
HubResponse hub_response
ClientRequest client_request
do
:: ch_hubresponse ?? msgtype, eval(id), hub_response ->
printf("\nClient Id: %d, Received - MsgType: %e", id, msgtype)
if
:: (msgtype == COMPUTE_RESPONSE) ->
// print the message
printf("\nClient Id: %d, Received - num = %d, sqnum = %d", id, hub_response.num, hub_response.sqnum)
// send another message. new num = sqnum
client_request.num = hub_response.sqnum % 256// To keep it as byte
if
:: (client_request.num < 2) ->
client_request.num = 2
:: else ->
skip
fi
ch_clientrequest ! COMPUTE_REQUEST(id, client_request)
printf("\nClient Id: %d, Sent - num = %d", id, client_request.num)
:: (msgtype == STOP_CLIENT) ->
// break from the do loop
break;
:: (msgtype == START_CLIENT) ->
client_request.num = id // Start with num = id
ch_clientrequest ! COMPUTE_REQUEST(id, client_request)
printf("\nClient Id: %d, Sent - num = %d", id, client_request.num)
fi
od
printf("\nClient exiting. Id = %d", id)
}
proctype Hub() {
// Hub sends a start message to each client, and then keeps responding to what it receives
HubResponse hr
ClientRequest client_request
mtype msgtype
byte client_id
int i
byte num
for (i: 0 .. ( N - 1) ) {
// Send a start message
hr.isNull = true
ch_hubresponse ! START_CLIENT(idlist.ids[i], hr) // Send a start message
}
// All of the clients have been started. Now wait for the message and respond appropriately
do
:: ch_clientrequest ? msgtype, client_id, client_request ->
printf("\nHub Controller. Received - MsgType: %e", msgtype)
if
:: (msgtype == COMPUTE_REQUEST) ->
// handle the message
num = client_request.num
hr.isNull = false
hr.id = client_id
hr.num = num
hr.sqnum = num * num
ch_hubresponse ! COMPUTE_RESPONSE(client_id, hr) // Send a response message
message_served ++
:: (msgtype == STOP_HUB) ->
// break from the do loop, send stop message to all clients, and exit
break;
fi
od
// loop through the ids and send stop message
for (i: 0 .. ( N - 1) ) {
// Send a start message
hr.isNull = true
ch_hubresponse ! STOP_CLIENT(idlist.ids[i], hr) // Send a start message
}
printf("\nServer exiting.")
}
active proctype Main() {
// Start the clients and give them an id to use
ClientRequest c
pid n;
n = _nr_pr;
byte i
for (i: 1.. N ) {
run Client(i)
idlist.ids[i-1] = i
}
// Start the hub and give it the list of ids
run Hub()
// Send a message to Hub to stop serving
(message_served >= 100);
ch_clientrequest ! STOP_HUB(0, c)
// Wait for all processes to exit
(n == _nr_pr);
printf("\nAll processes have exited!")
}