Лабораторная работа: Архив практики
Описание
Характеристики лабораторной работы
Список файлов
- Архив практики
- mc01
- 427_KovalenkoAI.c 9,99 Kb
- solution.txt 1,25 Kb
- task.txt 577 b
- mc02
- 427_KovalenkoAI_2.c 14,33 Kb
- 427_KovalenkoAI_2.pml 836 b
- abstract_lts_m12.dot 419 b
- abstract_lts_m12.png 35,23 Kb
- log.txt 1,01 Kb
- lts_m1.dot 423 b
- lts_m1.png 26,48 Kb
- lts_m12.dot 11,14 Kb
- lts_m12.png 576,66 Kb
- lts_m2.dot 420 b
- lts_m2.png 27,29 Kb
- state.txt 530 b
- mc03
- 427_KovalenkoAI_3.pml 1,14 Kb
- log.txt 1,08 Kb
- solution.txt 962 b
- task3.txt 6,79 Kb
- xspin.png 6,87 Kb
- mc04
- task47.txt 920 b
- mc05
- check1.pml 1,63 Kb
- check1.pml.trail 308 b
- check1_counterexample.txt 2,27 Kb
- check1_out.txt 806 b
- check2.pml 1,99 Kb
- check2.pml.trail 704 b
- check2_counterexample.txt 5,46 Kb
- check2_out.txt 807 b
- check3.pml 2,43 Kb
- check3.pml.trail 761 b
- check3_out.txt 910 b
- check4.pml 1,65 Kb
- check4_out.txt 911 b
- check5.pml 1,78 Kb
- check5_out.txt 905 b
- model_assert.pml 1,26 Kb
- solutions.txt 1,96 Kb
- spec1.ltl 469 b
- spec2.ltl 815 b
- spec3.ltl 1,25 Kb
- spec4.ltl 435 b
- spec5.ltl 494 b
- task5_nonprogress_out.txt 763 b
Число потенциальных состояний для функции f
Переменных: 5 (a,b,h,x,y)
Операторов: 12
Потенциальных состояний - 12 * 2 ^(32 * 5) = 12 * 2^160
Число достижимых состояний для функции f
x принимает 3 значения (#, 5, 8)
y принимает 2 значения (#, 2)
Данный кусок кода не достижим, т.к. y = 2, а в условии y > 5
{
x = 2;
}
Итого: 11 * 3 * 2 * 2^96
(f_x == # || f_x == 5 || f_x == 8) && (f_y == # || f_y == 2) && (c_f != 9) && (c_f < 11)
Число потенциальных состояний для функции g
Переменных: 5(a,b,h,x,y)
Операторов: 18
Потенциальных состояний - 18 * 2^160
Число достижимых состояний для функции g
x принимает 3 значения (#, 10, 4)
y принимает 3 значения (#, 7, 6)
Данный кусок не достижим, т.к. x = 10, а в условии x < 0
{
if (y > 10)
{
if (h > 5)
{
x = 6;
h = 3;
}
x = 7;
}
}
Данный кусок не достижим, т.к. x = 10, а в условии x > 10
{
x = 2;
}
Итого: 12 * 3 * 3 * 2^96
(g_x == # || g_x == 10 || g_x == 4) && (g_y == # || g_y == 7 || g_y == 6) && (c_g < 4 || (c_g > 9 && c_g != 14 && c_g < 17))
Для всей программы.
В функциях f и g по 4 переменных и переменная h глобальная
Потенциальных: 12 * 18 * 2^(32*(4+4+1)) = 150 * 2^288
Достижимых: 11 * 3 * 2 * 12 * 3 * 3 * 2^(2*5) = 7128 * 2^160
int h;
void f (int a, int b)
{
0:int x, y;
1:x = 5;
2:y = 2;
3:h = 6;
4:h = y;
5:h = y - b;
6:if (h > b - x)
{
7:if (h > y - b)
{
8:if (y > 5)
{
9:x = 2;
}
else
{
10:x = 8;
}
}
}
11:}
void g (int a, int b)
{
0:int x, y;
1:x = 10;
2:y = 7;
3:h = 4;
4:if (x < 0)
{
5:if (y > 10)
{
6:if (h > 5)
{
7:x = 6;
8:h = 3;
}
9:x = 7;
}
}
10:y = 6;
11:while (x > 5)
{
12:if (h > 0) break;
13:if (x > 10)
{
14:x = 2;
}
15:h = 4;
16:x = 4;
}
17:}
(Spin Version 6.0.1 -- 16 December 2010)
Full statespace search for:
never claim - (none specified)
assertion violations+
cycle checks - (disabled by -DSAFETY)
invalid end states+
State-vector 68 byte, depth reached 25, errors: 0
149 states, stored
101 states, matched
0 matches within stack
250 transitions (= stored+matched)
1 atomic steps
hash conflicts: 0 (resolved)
stackframes: 3/0
stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
4.577memory usage (Mbyte)
unreached in proctype F
427_KovalenkoAI_2.pml:17, state 9, "x = 2"
(1 of 20 states)
unreached in proctype G
427_KovalenkoAI_2.pml:39, state 7, "x = 6"
427_KovalenkoAI_2.pml:40, state 8, "h = 3"
427_KovalenkoAI_2.pml:38, state 10, "((h>5))"
427_KovalenkoAI_2.pml:38, state 10, "else"
427_KovalenkoAI_2.pml:43, state 12, "x = 7"
427_KovalenkoAI_2.pml:58, state 27, "x = 2"
(5 of 38 states)
unreached in init
(0 of 4 states)
pan: elapsed time 0 seconds
Распознанный текст из изображения:
оа б
х=га
ОДЗХ,ОДО.О
1.0. †,5. 9,9
-10 -С
у=г
2,0 б 5 2 Я 1.1«Ь5. †.10.9 о.г..о,ыгод
17=6
17=4
х=ы
3,0.6.«.г.о.
г 1.9, .г 10 9
г.г.-..-.яДО. О.З 4.6. ДОЗ
' «х«01
17=6
1г=у
х=га
3 — 2
3,1.6.5.2.10.9
г.г. Дьгдад 1З 4д.одод 0,9.4.9..10.7
4.о,ггьгзх
'(х 'ОЗ вЂ” с
1г=т-Ь
1г=у
1=6
з=г
-«а
гзд,5581ОУ 0.10.4.9,,10,6
«.О.о,з.гзхо
З.г.б.«.2.10,7
г.з,с.«.гда.
4 1 2 \ ДДО о
1«.*Ь-х ~=10
1г=у-Ь 1г=у 17=4 7=6
18.=03 =г
с=б — 5 х:5
О.о.огьг.*.= бд.о..-.гдо.= 4.г.г.с.гдад зззгьгдод з.зоь-.г.год
гызз.гдо. 1.20 4,«з.га.б 0.11.4.ОЫ.10.6
СЬ.у-оз -га 1«..Ь-х 1г=у-Ь «=4 7=1' 1г=у ' «х«07
' «х«07 «=б =б =2 х..« — 5
1г.о
ы,о,о 5.2. ы 6.2,0.«.гдо. с.г,а..-„гдод 4.ЗЗ,с.гза. 4.3.2.5,2.10. зызгьгдод
г 10 4 с г 10 б 1.11.4.5..10.6
3,9.6.5,2„10.7
0.16.4.9, .10,6
т с
— 1О
Ь=у
«=У.Ь 1«=У.Ь '(х'«03
ь: а — с
«Х'«03 7=\'
1г=у
с=б
10.1.0.5.2,10.:
5« з,оз гдо;
3,10.6.5.2.10.6
2.11.4.«.2.10.6
О.г.о « г,год
4 оз.с,гдод
4 о.г.с,гдод
3.10,4.5.2,10.6
1,16.4 с Ы10 б
1«=у х.
'охгоз г=У-Ь 1г=у-Ь вЂ
«хЬ х
«Ь«У-Ьг 7=4
17'О =2
х.'5 7=6
ы.г.огьгдод
6.3.4.«.2.10. «ыз -,гдо 7
б.з.о.с.гдоз 5.9.0 5.2 год 4.10.4.5.2.10.6
3.11.4.5.2.10.6
3.11.6.5.2.10.6
2.16.4.«.2.10.6
4 10 2 с 2 10 б
1«- 0 87=6
17. у-Ь '(хто) 17- Ь-х — б
1г=у-Ь ттх. 5
1г=у 1«: 0
'87«.-у-о) 'тх: 07 7:Ь-х — б г=у-Ь
х 5
5 го 5
4.11.4.5 Д.10.6 4.11.2.5,2,10,6
6.9.0.5.2.10,7 с за а 5 гзо6
3.16.6.5 Д.10.6
3.16.4.5.2.10.6
Ох*'03 О«: у-ьг — б 01-
ь:-о
1г=т
г — -Ь Ь=з-о Ьг 0
«.11.4.«,2.10.6
6.10.0.«.2.10.6
.11.0.5.2 10.6
4.16.4.5.2.10.6 4.16.2.5,2.10.6
10.9.0.5.2.10.
«,гдод
ыд.«.гдоз
6.10.4.5.2.10.6
17'.0
с=б '87«ху'-Щ
1г=у-Ь г=у-Ь
7. Ь-х
'77 -*О>
х 5
.10.4.5.2.10.6
6.11.4.5.2.10.6
5.16.4.«.2.10.6
10.10.0.«.2.10.6
6.11.0.5.2.10.6
с 12 0 5 2 10 б
«.16.0.«.2.10.6
оыз,«.гдод
0.7
1«: Ь-х тх. 107
17:.Ь-х
Мо.у-ю МЬ. >
9.10.4.«,2,10,6
„11.4.5.2,10,6 6.16.4.5.2,10.6
10.11.0.5,2.10,6
6,12,0.5 Д.10.6
..14.03 .г 10.6
,г.ыд
'Ох:оз
.16.4,5.2.10.6
5.15.4.«.2.10.6
9.11.4.«.2.10.6
10.12.0.«.2.10.6
10.4,8.2.10,6
х- х=В 17''0 '«3«*57
Пх- -Ь>
1О*Ь-х — 4
'(х. 10>
9 16.43.2.Ы.О
6.15.4.5.2.10.6
5.10.4.5.2.4.6
10.14,0.5.2,10,6
10.11,4.8.2.10.6
7:.у-Ь х=4 «.Ь-х 787 53
.15.4.5,2,10,6 6.10.4.5,2,4.6 5.16.4,5,2.4.6
17. 0
1 О, 1 6 .4 . 8 .2 . 1 0 .6
От'53 -4 «ху-ь 18'-сз ' ь-
9,15.4.« ДД0.6 7,10.4.5.2.4.6 ОД6.4.с.2,4.6
— 8 х=4 'Оу 5) '(хс 5) т-Ь
9.10.4.5.2.4.6
7.16.4.«.2.4.6
10.15.4.8.2.10.6
х=4 х=я '(х'5) 'буаз)
9,16.4.5.2,4.6
10,10.4.8.2.4.6
Ох'.53 — 8
10.16,4.8.2.4.6
.с.ЗЗ.«.г,гау
17 'Ь.х Фах 01
.3.4,5,2.10. 6.9.4.5.2.10. 5.10.4.5.2.10.6 10.3.0.5.2.10, Ос" 53 Ох* 03 17. 3'-ь — 6 18 1-
х=В '(х«0) 'ОУ« 5) с=б 7 т-Ь х. «17. Ь-х
тог х=8 « — б 'гу'.53 х с Ь.-у.-о Ь:-О
3=6 — я 037 53 ьхо 1«хт-Ь
7=4
10Д5.4,5.2,10.6
'Ох -Ьз 080103 6,14.0.«,2.10.6
б 16 0 с 2 10 б
х
10.16.0,5,2.10.6
Согласно верификатору, у модели - 149 достижимых состояний
В LTS для программы - 128 достижимых состояний
Запуск с параметрами -o1 -o2 -o3 -DNOREDUCE
Количество состояний отличается потому, что:
1. В верификаторе добавлен процесс init, который составляет 3 состояния (2 run и 1 -end-)
2. В верификаторе добавлены 26 состояний -end- (по одному на каждый оператор в функции f - 10 состояний, и в функции g - 16 состояний)
3. В верификаторе 8 операторов -end- совпадают с окончанием вычислений в LTS
149 - 3 - 26 + 8 = 128
0:proc - (:root:) creates proc 1 (model)
0:proc - (:root:) creates proc 2 (manager)
1:proc 1 (model) 427_KovalenkoAI_3.pml:22 (state 3)[goto B]
2:proc 1 (model) 427_KovalenkoAI_3.pml:22 (state 3)[(1)]
3:proc 0 (model) 427_KovalenkoAI_3.pml:22 (state 3)[goto B]
4:proc 0 (model) 427_KovalenkoAI_3.pml:22 (state 3)[goto B]
5:proc 1 (model) 427_KovalenkoAI_3.pml:27 (state 4)[.(goto)]
6:proc 1 (model) 427_KovalenkoAI_3.pml:12 (state 9)[flag[procNum] = 1]
7:proc 1 (model) 427_KovalenkoAI_3.pml:9 (state 6)[turn = (1-procNum)]
8:proc 1 (model) 427_KovalenkoAI_3.pml:10 (state 7)[(((flag[(1-procNum)]==0)||(turn==proc Num)))]
9:proc 0 (model) 427_KovalenkoAI_3.pml:22 (state 3)[(1)]
10:proc 0 (model) 427_KovalenkoAI_3.pml:27 (state 4)[.(goto)]
-------------
depth-limit (-u10 steps) reached
#processes: 3
flag[0] = 0
flag[1] = 1
turn = 0
mutex = 0
10:proc 2 (manager) 427_KovalenkoAI_3.pml:76 (state 8)
10:proc 1 (model) 427_KovalenkoAI_3.pml:11 (state 8)
10:proc 0 (model) 427_KovalenkoAI_3.pml:12 (state 9)
3 processes created
Возможно не удалось распознать кодировку файла
/*
* Function lpfc_bsg_ct_unsol_event at linux-2.6.38/drivers/scsi/lpfc/lpfc_bsg. c:759-994
* Allocation call kzalloc at 88
* Release call kfree at 139
* DEG: 21 LOC: 51
*/
lpfc_bsg_ct_unsol_event(struct lpfc_hba *phba, struct lpfc_sli_ring *pring,
struct lpfc_iocbq *piocbq)
{
uint32_t evt_req_id = 0;
uint32_t cmd;
uint32_t len;
struct lpfc_dmabuf *dmabuf = NULL;
struct lpfc_bsg_event *evt;
struct event_data *evt_dat = NULL;
struct lpfc_iocbq *iocbq;
size_t offset = 0;
struct list_head head;
struct ulp_bde64 *bde;
dma_addr_t dma_addr;
int i;
struct lpfc_dmabuf *bdeBuf1 = piocbq->context2;
struct lpfc_dmabuf *bdeBuf2 = piocbq->context3;
struct lpfc_hbq_entry *hbqe;
struct lpfc_sli_ct_request *ct_req;
struct fc_bsg_job *job = NULL;
unsigned long flags;
int size = 0;
INIT_LIST_HEAD(&head);
list_add_tail(&head, &piocbq->list);
if (piocbq->iocb.ulpBdeCount == 0 ||
piocbq->iocb.un.cont64[0].tus.f.bdeSize == 0)
goto error_ct_unsol_exit;
if (phba->link_state == LPFC_HBA_ERROR ||
(!(phba->sli.sli_flag & LPFC_SLI_ACTIVE)))
goto error_ct_unsol_exit;
if (phba->sli3_options & LPFC_SLI3_HBQ_ENABLED)
dmabuf = bdeBuf1;
else {
dma_addr = getPaddr(piocbq->iocb.un.cont64[0].addrH igh,
piocbq->iocb.un.cont64[0].addrLow);
dmabuf = lpfc_sli_ringpostbuf_get(phba, pring, dma_addr);
}
if (dmabuf == NULL)
goto error_ct_unsol_exit;
ct_req = (struct lpfc_sli_ct_request *)dmabuf->virt;
evt_req_id = ct_req->FsType;
cmd = ct_req->CommandResponse.bits.CmdRsp;
len = ct_req->CommandResponse.bits.Size;
if (!(phba->sli3_options & LPFC_SLI3_HBQ_ENABLED))
lpfc_sli_ringpostbuf_put(phba, pring, dmabuf);
spin_lock_irqsave(&phba->ct_ev_lock, flags);
list_for_each_entry(evt, &phba->ct_ev_waiters, node) {
if (!(evt->type_mask & FC_REG_CT_EVENT) ||
evt->req_id != evt_req_id)
continue;
lpfc_bsg_event_ref(evt);
spin_unlock_irqrestore(&phba->ct_ev_lock , flags);
evt_dat = kzalloc(sizeof(*evt_dat), GFP_KERNEL);
if (evt_dat == NULL) {
spin_lock_irqsave(&phba->ct_ev_lock, flags);
lpfc_bsg_event_unref(evt);
lpfc_printf_log(phba, KERN_WARNING, LOG_LIBDFC,
"2614 Memory allocation failed for "
"CT event\n");
break;
}
if (phba->sli3_options & LPFC_SLI3_HBQ_ENABLED) {
/* take accumulated byte count from the last iocbq */
iocbq = list_entry(head.prev, typeof(*iocbq), list);
evt_dat->len = iocbq->iocb.unsli3.rcvsli3.acc_len;
} else {
list_for_each_entry(iocbq, &head, list) {
for (i = 0; i < iocbq->iocb.ulpBdeCount; i++)
evt_dat->len +=
iocbq->iocb.un.cont64[i].tus.f.bdeSize;
}
}
evt_dat->data = kzalloc(evt_dat->len, GFP_KERNEL);
if (evt_dat->data == NULL) {
lpfc_printf_log(phba, KERN_WARNING, LOG_LIBDFC,
"2615 Memory allocation failed for "
"CT event data, size %d\n",
evt_dat->len);
kfree(evt_dat);
spin_lock_irqsave(&phba->ct_ev_lock, flags);
lpfc_bsg_event_unref(evt);
spin_unlock_irqrestore(&phba->ct_ev_lock , flags);
goto error_ct_unsol_exit;
}
list_for_each_entry(iocbq, &head, list) {
size = 0;
if (phba->sli3_options & LPFC_SLI3_HBQ_ENABLED) {
bdeBuf1 = iocbq->context2;
bdeBuf2 = iocbq->context3;
}
for (i = 0; i < iocbq->iocb.ulpBdeCount; i++) {
if (phba->sli3_options &
LPFC_SLI3_HBQ_ENABLED) {
if (i == 0) {
hbqe = (struct lpfc_hbq_entry *)
&iocbq->iocb.un.ulpWord[0];
size = hbqe->bde.tus.f.bdeSize;
dmabuf = bdeBuf1;
} else if (i == 1) {
hbqe = (struct lpfc_hbq_entry *)
&iocbq->iocb.unsli3.
sli3Words[4];
size = hbqe->bde.tus.f.bdeSize;
dmabuf = bdeBuf2;
}
if ((offset + size) > evt_dat->len)
size = evt_dat->len - offset;
} else {
size = iocbq->iocb.un.cont64[i].
tus.f.bdeSize;
bde = &iocbq->iocb.un.cont64[i];
dma_addr = getPaddr(bde->addrHigh,
bde->addrLow);
dmabuf = lpfc_sli_ringpostbuf_get(phba,
pring, dma_addr);
}
if (!dmabuf) {
lpfc_printf_log(phba, KERN_ERR,
LOG_LIBDFC, "2616 No dmabuf "
"found for iocbq 0x%p\n",
iocbq);
kfree(evt_dat->data);
kfree(evt_dat);
spin_lock_irqsave(&phba->ct_ev_lock,
flags);
lpfc_bsg_event_unref(evt);
spin_unlock_irqrestore(
&phba->ct_ev_lock, flags);
goto error_ct_unsol_exit;
}
memcpy((char *)(evt_dat->data) + offset,
dmabuf->virt, size);
offset += size;
if (evt_req_id != SLI_CT_ELX_LOOPBACK &&
!(phba->sli3_options &
LPFC_SLI3_HBQ_ENABLED)) {
lpfc_sli_ringpostbuf_put(phba, pring,
dmabuf);
} else {
switch (cmd) {
case ELX_LOOPBACK_DATA:
diag_cmd_data_free(phba,
(struct lpfc_dmabufext *)
dmabuf);
break;
case ELX_LOOPBACK_XRI_SETUP:
if ((phba->sli_rev ==
LPFC_SLI_REV2) ||
(phba->sli3_options &
LPFC_SLI3_HBQ_ENABLED
)) {
lpfc_in_buf_free(phba,
dmabuf);
} else {
lpfc_post_buffer(phba,
pring,
1);
}
break;
default:
if (!(phba->sli3_options &
LPFC_SLI3_HBQ_ENABLED))
lpfc_post_buffer(phba,
pring,
1);
break;
}
}
}
}
spin_lock_irqsave(&phba->ct_ev_lock, flags);
if (phba->sli_rev == LPFC_SLI_REV4) {
evt_dat->immed_dat = phba->ctx_idx;
phba->ctx_idx = (phba->ctx_idx + 1) % 64;
/* Provide warning for over-run of the ct_ctx array */
if (phba->ct_ctx[evt_dat->immed_dat].flags &
UNSOL_VALID)
lpfc_printf_log(phba, KERN_WARNING, LOG_ELS,
"2717 CT context array entry "
"[%d] over-run: oxid:x%x, "
"sid:x%x\n", phba->ctx_idx,
phba->ct_ctx[
evt_dat->immed_dat].oxid,
phba->ct_ctx[
evt_dat->immed_dat].SID);
phba->ct_ctx[evt_dat->immed_dat].oxid =
piocbq->iocb.ulpContext;
phba->ct_ctx[evt_dat->immed_dat].SID =
piocbq->iocb.un.rcvels.remoteID;
phba->ct_ctx[evt_dat->immed_dat].flags = UNSOL_VALID;
} else
evt_dat->immed_dat = piocbq->iocb.ulpContext;
evt_dat->type = FC_REG_CT_EVENT;
list_add(&evt_dat->node, &evt->events_to_see);
if (evt_req_id == SLI_CT_ELX_LOOPBACK) {
wake_up_interruptible(&evt->wq);
lpfc_bsg_event_unref(evt);
break;
}
list_move(evt->events_to_see.prev, &evt->events_to_get);
lpfc_bsg_event_unref(evt);
job = evt->set_job;
evt->set_job = NULL;
if (job) {
job->reply->reply_payload_rcv_len = size;
/* make error code available to userspace */
job->reply->result = 0;
job->dd_data = NULL;
/* complete the job back to userspace */
spin_unlock_irqrestore(&phba->ct_ev_lock , flags);
job->job_done(job);
spin_lock_irqsave(&phba->ct_ev_lock, flags);
}
}
spin_unlock_irqrestore(&phba->ct_ev_lock , flags);
error_ct_unsol_exit:
if (!list_empty(&head))
list_del(&head);
if (evt_req_id == SLI_CT_ELX_LOOPBACK)
return 0;
return 1;
}
Распознанный текст из изображения:
га га гз гз гз гз за за згг згг ого ого гзз гзз гзз гзз гоз гоз гоо гоо
а>а
Вариант 47
Задача 1 После наступления события 'процесс p находится на метке iter_begin' верно: никогда не выполняется 'процесс q находится на метке received'
#define P "p@iter_begin"
#define Q "q@received"
[](P -> []!Q)
Задача 2 Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: никогда не выполняется 'из канала d принимается сообщение ack'
#define A (state==enter)
#define B (state==leave)
#define C d?ack
[]((A & !B & <>B) -> (!C U B))
Задача 3 После наступления события 'процесс p находится на метке iter_begin' верно: сразу за событием 'процесс q находится на метке received' наступает событие 'процесс p находится на метке sent' (полученное свойство не обязательно может быть инвариантным к прореживанию)
#define P "p@iter_begin"
#define Q "q@received"
#define Z "p@sent"
[](P -> (Q -> XZ))
Starting :init: with pid 0
Starting :never: with pid 1
Never claim moves to line 106[(1)]
Starting model with pid 2
2:proc 0 (:init:) line 120 "D:/Study/ВПНМ/mc05/check1.pml" (state 1)[(run model())]
Starting manager with pid 3
3:proc 0 (:init:) line 120 "D:/Study/ВПНМ/mc05/check1.pml" (state 2)[(run manager())]
Never claim moves to line 104[((!((model._p==ALLC))&&(model._p==B) ))]
5:proc 1 (model) line 31 "D:/Study/ВПНМ/mc05/check1.pml" (state 1)[(1)]
Never claim moves to line 110[(!((model._p==ALLC)))]
7:proc 1 (model) line 14 "D:/Study/ВПНМ/mc05/check1.pml" (state 5)[flag[procNum] = 1]
9:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check1.pml" (state 6)[turn = (1-procNum)]
11:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check1.pml" (state 7)[(((flag[(1-procNum)]==0)||(turn==proc Num)))]
13:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check1.pml" (state 8)[mutex = (mutex+1)]
15:proc 1 (model) line 22 "D:/Study/ВПНМ/mc05/check1.pml" (state 10)[mutex = (mutex-1)]
17:proc 1 (model) line 23 "D:/Study/ВПНМ/mc05/check1.pml" (state 11)[flag[procNum] = 0]
19:proc 1 (model) line 14 "D:/Study/ВПНМ/mc05/check1.pml" (state 14)[flag[procNum] = 1]
21:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check1.pml" (state 15)[turn = (1-procNum)]
23:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check1.pml" (state 16)[(((flag[(1-procNum)]==0)||(turn==pro cNum)))]
25:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check1.pml" (state 17)[mutex = (mutex+1)]
27:proc 1 (model) line 22 "D:/Study/ВПНМ/mc05/check1.pml" (state 76)[mutex = (mutex-1)]
29:proc 1 (model) line 23 "D:/Study/ВПНМ/mc05/check1.pml" (state 77)[flag[procNum] = 0]
Never claim moves to line 111[((!((model._p==ALLC))&&(model._p==EN D)))]
31:proc 1 (model) line 81 "D:/Study/ВПНМ/mc05/check1.pml" (state 79)[(1)]
Never claim moves to line 114[(1)]
spin: trail ends after 33 steps
#processes: 3
flag[0] = 0
flag[1] = 0
turn = 0
mutex = 0
33:proc 2 (manager) line 87 "D:/Study/ВПНМ/mc05/check1.pml" (state 8)
33:proc 1 (model) line 30 "D:/Study/ВПНМ/mc05/check1.pml" (state 3)
33:proc 0 (:init:) line 121 "D:/Study/ВПНМ/mc05/check1.pml" (state 4) <valid end state>
33:proc - (:never:) line 115 "D:/Study/ВПНМ/mc05/check1.pml" (state 16) <valid end state>
3 processes created
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan: claim violated! (at depth 32)
pan: wrote check1.pml.trail
(Spin Version 5.2.4 -- 2 December 2009)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations+ (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states- (disabled by never claim)
State-vector 36 byte, depth reached 32, errors: 1
18 states, stored
2 states, matched
20 transitions (= stored+matched)
1 atomic steps
hash conflicts: 0 (resolved)
2.501memory usage (Mbyte)
pan: elapsed time 0.003 seconds
Скопировано файлов: 1.
Starting :init: with pid 0
Starting :never: with pid 1
Never claim moves to line 109[(1)]
Starting model with pid 2
2:proc 0 (:init:) line 132 "D:/Study/ВПНМ/mc05/check2.pml" (state 1)[(run model())]
Starting manager with pid 3
3:proc 0 (:init:) line 132 "D:/Study/ВПНМ/mc05/check2.pml" (state 2)[(run manager())]
Never claim moves to line 107[((!((model._p==END))&&(model._p==B)) )]
5:proc 1 (model) line 32 "D:/Study/ВПНМ/mc05/check2.pml" (state 1)[(1)]
Never claim moves to line 113[(!((model._p==END)))]
7:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check2.pml" (state 5)[flag[procNum] = 1]
Never claim moves to line 123[(!((model._p==END)))]
9:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check2.pml" (state 6)[turn = (1-procNum)]
Never claim moves to line 113[(!((model._p==END)))]
11:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check2.pml" (state 7)[(((flag[(1-procNum)]==0)||(turn==proc Num)))]
Never claim moves to line 123[(!((model._p==END)))]
13:proc 1 (model) line 17 "D:/Study/ВПНМ/mc05/check2.pml" (state 8)[mutex = (mutex+1)]
Never claim moves to line 113[(!((model._p==END)))]
15:proc 1 (model) line 23 "D:/Study/ВПНМ/mc05/check2.pml" (state 10)[mutex = (mutex-1)]
Never claim moves to line 123[(!((model._p==END)))]
17:proc 1 (model) line 24 "D:/Study/ВПНМ/mc05/check2.pml" (state 11)[flag[procNum] = 0]
Never claim moves to line 113[(!((model._p==END)))]
19:proc 1 (model) line 43 "D:/Study/ВПНМ/mc05/check2.pml" (state 13)[(1)]
Never claim moves to line 123[(!((model._p==END)))]
21:proc 1 (model) line 48 "D:/Study/ВПНМ/mc05/check2.pml" (state 22)[ch!alloc]
22:proc 2 (manager) line 92 "D:/Study/ВПНМ/mc05/check2.pml" (state 1)[ch?alloc]
Never claim moves to line 113[(!((model._p==END)))]
24:proc 2 (manager) line 94 "D:/Study/ВПНМ/mc05/check2.pml" (state 2)[ch!alloc_ok]
25:proc 1 (model) line 54 "D:/Study/ВПНМ/mc05/check2.pml" (state 33)[ch?alloc_ok]
Never claim moves to line 123[(!((model._p==END)))]
27:proc 1 (model) line 55 "D:/Study/ВПНМ/mc05/check2.pml" (state 34)[(1)]
Never claim moves to line 113[(!((model._p==END)))]
29:proc 1 (model) line 64 "D:/Study/ВПНМ/mc05/check2.pml" (state 48)[goto :b1]
Never claim moves to line 123[(!((model._p==END)))]
31:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check2.pml" (state 52)[flag[procNum] = 1]
Never claim moves to line 113[(!((model._p==END)))]
33:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check2.pml" (state 53)[turn = (1-procNum)]
Never claim moves to line 123[(!((model._p==END)))]
35:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check2.pml" (state 54)[(((flag[(1-procNum)]==0)||(turn==pro cNum)))]
Never claim moves to line 113[(!((model._p==END)))]
37:proc 1 (model) line 17 "D:/Study/ВПНМ/mc05/check2.pml" (state 55)[mutex = (mutex+1)]
Never claim moves to line 123[(!((model._p==END)))]
39:proc 1 (model) line 71 "D:/Study/ВПНМ/mc05/check2.pml" (state 58)[(1)]
Never claim moves to line 113[(!((model._p==END)))]
41:proc 1 (model) line 77 "D:/Study/ВПНМ/mc05/check2.pml" (state 69)[(1)]
Never claim moves to line 123[(!((model._p==END)))]
43:proc 1 (model) line 23 "D:/Study/ВПНМ/mc05/check2.pml" (state 10)[mutex = (mutex-1)]
Never claim moves to line 113[(!((model._p==END)))]
45:proc 1 (model) line 24 "D:/Study/ВПНМ/mc05/check2.pml" (state 11)[flag[procNum] = 0]
Never claim moves to line 123[(!((model._p==END)))]
47:proc 1 (model) line 43 "D:/Study/ВПНМ/mc05/check2.pml" (state 13)[(1)]
Never claim moves to line 113[(!((model._p==END)))]
49:proc 1 (model) line 48 "D:/Study/ВПНМ/mc05/check2.pml" (state 22)[ch!alloc]
50:proc 2 (manager) line 92 "D:/Study/ВПНМ/mc05/check2.pml" (state 1)[ch?alloc]
Never claim moves to line 123[(!((model._p==END)))]
52:proc 2 (manager) line 94 "D:/Study/ВПНМ/mc05/check2.pml" (state 2)[ch!alloc_ok]
53:proc 1 (model) line 54 "D:/Study/ВПНМ/mc05/check2.pml" (state 33)[ch?alloc_ok]
Never claim moves to line 114[(((!((model._p==END))&&!((model._p== FFREE)))&&(model._p==ALLC_OK)))]
55:proc 1 (model) line 55 "D:/Study/ВПНМ/mc05/check2.pml" (state 34)[(1)]
Never claim moves to line 118[(!((model._p==FFREE)))]
57:proc 1 (model) line 64 "D:/Study/ВПНМ/mc05/check2.pml" (state 48)[goto :b1]
59:proc 1 (model) line 15 "D:/Study/ВПНМ/mc05/check2.pml" (state 52)[flag[procNum] = 1]
61:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check2.pml" (state 53)[turn = (1-procNum)]
63:proc 1 (model) line 16 "D:/Study/ВПНМ/mc05/check2.pml" (state 54)[(((flag[(1-procNum)]==0)||(turn==pro cNum)))]
65:proc 1 (model) line 17 "D:/Study/ВПНМ/mc05/check2.pml" (state 55)[mutex = (mutex+1)]
67:proc 1 (model) line 70 "D:/Study/ВПНМ/mc05/check2.pml" (state 57)[goto :b0]
69:proc 1 (model) line 23 "D:/Study/ВПНМ/mc05/check2.pml" (state 76)[mutex = (mutex-1)]
71:proc 1 (model) line 24 "D:/Study/ВПНМ/mc05/check2.pml" (state 77)[flag[procNum] = 0]
Never claim moves to line 119[((!((model._p==FFREE))&&(model._p==E ND)))]
73:proc 1 (model) line 84 "D:/Study/ВПНМ/mc05/check2.pml" (state 79)[(1)]
Never claim moves to line 127[(1)]
spin: trail ends after 75 steps
#processes: 3
flag[0] = 0
flag[1] = 0
turn = 0
mutex = 0
75:proc 2 (manager) line 90 "D:/Study/ВПНМ/mc05/check2.pml" (state 8)
75:proc 1 (model) line 31 "D:/Study/ВПНМ/mc05/check2.pml" (state 3)
75:proc 0 (:init:) line 133 "D:/Study/ВПНМ/mc05/check2.pml" (state 4) <valid end state>
75:proc - (:never:) line 128 "D:/Study/ВПНМ/mc05/check2.pml" (state 28) <valid end state>
3 processes created
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan: claim violated! (at depth 74)
pan: wrote check2.pml.trail
(Spin Version 5.2.4 -- 2 December 2009)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations+ (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states- (disabled by never claim)
State-vector 36 byte, depth reached 106, errors: 1
93 states, stored
10 states, matched
103 transitions (= stored+matched)
1 atomic steps
hash conflicts: 0 (resolved)
2.501memory usage (Mbyte)
pan: elapsed time 0.006 seconds
Скопировано файлов: 1.
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
(Spin Version 5.2.4 -- 2 December 2009)
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations+ (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states- (disabled by never claim)
State-vector 36 byte, depth reached 78, errors: 0
122 states, stored
21 states, matched
143 transitions (= stored+matched)
1 atomic steps
hash conflicts: 0 (resolved)
2.501memory usage (Mbyte)
unreached in proctype model
line 86, state 80, "-end-"
(1 of 81 states)
unreached in proctype manager
line 102, state 11, "-end-"
(1 of 11 states)
unreached in proctype :init:
(0 of 4 states)
pan: elapsed time 0.001 seconds
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
(Spin Version 5.2.4 -- 2 December 2009)
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations+ (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states- (disabled by never claim)
State-vector 44 byte, depth reached 1169, errors: 0
1784 states, stored
1840 states, matched
3624 transitions (= stored+matched)
2 atomic steps
hash conflicts: 1 (resolved)
2.501memory usage (Mbyte)
unreached in proctype model
line 83, state 81, "-end-"
(1 of 82 states)
unreached in proctype manager
line 99, state 11, "-end-"
(1 of 11 states)
unreached in proctype :init:
(0 of 5 states)
pan: elapsed time 0.005 seconds
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
(Spin Version 5.2.4 -- 2 December 2009)
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations+ (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states- (disabled by never claim)
State-vector 36 byte, depth reached 50, errors: 0
43 states, stored
8 states, matched
51 transitions (= stored+matched)
1 atomic steps
hash conflicts: 0 (resolved)
2.501memory usage (Mbyte)
unreached in proctype model
line 83, state 80, "-end-"
(1 of 81 states)
unreached in proctype manager
line 99, state 11, "-end-"
(1 of 11 states)
unreached in proctype :init:
(0 of 4 states)
pan: elapsed time 0 seconds
1.В ходе выполнения тела функции рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc*.
Модель модифицирована - запускается только один процесс, моделирующий функцию, на котором проверяется свойство.
#define start (model@B)
#define end (model@END)
#define allc (model@ALLC)
/* ) */
2.В ходе выполнения тела функции после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free*
Модель модифицирована - запускается только один процесс, моделирующий функцию, на котором проверяется свойство.
#define start (model@B)
#define end (model@END)
#define allc_ok (model@ALLC_OK)
#define ffree (model@FFREE)
/* ) U end)) */
3.На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера ресурсов.
Модель модифицирована - запускается только один процесс, моделирующий функцию, на котором проверяется свойство.
#define start (model@B)
#define end (model@END)
#define allc (model@ALLC)
#define allc_ok (model@ALLC_OK)
#define ffree (model@FFREE)
#define ffree_ok (model@FFREE_OK)
/* )&&(ffree -> (!end U ffree_ok))) U end)) */
4.В критической секции (между вызовами spin_lock* и spin_unlock*) может находиться не более одного процесса.
#define lock_1 (model[1]@LOCK1 || model[1]@LOCK2 || model[1]@LOCK3 || model[1]@LOCK4 || model[1]@LOCK5 || model[1]@LOCK6)
#define lock_2 (model[2]@LOCK1 || model[2]@LOCK2 || model[2]@LOCK3 || model[2]@LOCK4 || model[2]@LOCK5 || model[2]@LOCK6)
/* <>(lock_1 && lock_2) */
5.В ходе выполнения тела функции, функция kfree вызывается не более одного раза.
Модель модифицирована - запускается только один процесс, моделирующий функцию, на котором проверяется свойство.
#define start (model@B)
#define end (model@END)
#define free (model@FFREE)
/* )) */
(Spin Version 5.2.4 -- 2 December 2009)
+ Partial Order Reduction
Full statespace search for:
never claim +
assertion violations+ (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states- (disabled by never claim)
State-vector 40 byte, depth reached 1237, errors: 0
3382 states, stored (5028 visited)
9251 states, matched
14279 transitions (= visited+matched)
0 atomic steps
hash conflicts: 10 (resolved)
2.598memory usage (Mbyte)
unreached in proctype model
line 79, state 80, "-end-"
(1 of 80 states)
unreached in proctype manager
line 95, state 11, "-end-"
(1 of 11 states)
pan: elapsed time 0.024 seconds
pan: rate 209500 states/second
Начать зарабатывать
zzyxel
