<<

Приложение Б. Модель и вывод Spinпри верификации логики в игре Tutrleball

Модель

#define AWall_Start 0

#define AWall_GrowHorizontal 1

#define AWall_GrowVertical 2

#define AWall_Kill 3

#define AWall_Wall 4

#define APlatform_Start 0

#define APlatform_GrowOtherWall 1

#define APlatform_Grow2Walls 2

#define APlatform_GrowOneWall 3

#define Reset 1

#define NewHorizontal 2

#define NewVertical 3

#define SetWall 4

#define Bounce 5

#define Kill 6

#define StopOtherSide 7

#define StopOneSide 8

#define StartGrow 9

#define Update 10

#define AWall_KillAll 1

#define APlatform_DoGrowWallOther 2

#define APlatform_DoGrowWallOne 3

typedef AWallData

{

byte state;

byte curEvent;

byte ID;

byte functionCall;

byte nestedMachine;

byte forkMachine;

bool started;

bool finished;

}

typedef APlatformData

{

byte state;

byte curEvent;

byte ID;

byte functionCall;

byte nestedMachine;

byte forkMachine;

bool started;

bool finished;

}

inline random(var, nBits)

{

int index = 0;

var = 0;

do

:: index < nBits ->

index = index + 1;

var = var * 2;

if

:: var = var + 1;

:: var = var + 0;

fi;

:: else -> break;

od;

}

chan awall_ch = [0] of {int}

chan platform_ch = [0] of {int}

inline AWall(machine, evt)

{

byte sendEvt;

if

::(machine.state == AWall_Start) ->

printf("machine%d.state = AWall.Start \n", machine.ID);

if

::((evt == NewHorizontal)) ->

machine.state = AWall_GrowHorizontal; atomic

{

printf("machine%d.

event_happened:

_NewHorizontal_ \n", machine.ID); machine.curEvent = NewHorizontal;

}

//Code

//Code

::((evt == NewVertical)) ->

machine.state = AWall_GrowVertical; atomic

{

printf("machine%d. event_happened:

_NewVertical_ \n", machine.ID); machine.curEvent = NewVertical;

}

//Code

//Code

::((evt == SetWall)) ->

machine.state = AWall_Wall;

atomic

{ printf("machine%d.

event_happened:

_SetWall_ \n", machine.ID);

machine.curEvent = SetWall;

}

//Code

//Code

:: else ->

skip;

fi;

::(machine.state == AWall_GrowHorizontal) ->

printf("machine%d.state = AWall.GrowHorizontal \n", machine.ID);

if

::((evt == Bounce)) ->

machine.state = AWall_Kill;

atomic

{ printf("machine%d. event_happened:

_Bounce_ \n", machine.ID);

machine.curEvent = Bounce;

}

//Code

//Code

atomic

{

printf("machine%d.KillAll()\n", machine.ID);

machine.functionCall = 1;

}

::((evt == Kill)) ->

machine.state = AWall_Kill;

atomic

{ printf("machine%d. event_happened:

_Kill_ \n", machine.ID); machine.curEvent = Kill;

}

//Code

//Code

atomic

{

printf("machine%d.KillAll() \n", machine.ID);

machine.functionCall = 1;

}

::((evt == SetWall)) ->

machine.state = AWall_Wall;

atomic

{ printf("machine%d. event_happened:

_SetWall_ \n", machine.ID); machine.curEvent = SetWall;

}

//Code

//Code

:: else ->

skip;

fi;

::(machine.state == AWall_GrowVertical) ->

printf("machine%d.state = AWall.GrowVertical \n", machine.ID);

if

::((evt == Bounce)) ->

machine.state = AWall_Kill;

atomic

{

printf("machine%d. event_happened:

_Bounce_ \n", machine.ID); machine.curEvent = Bounce;

}

//Code

//Code

atomic

{

printf("machine%d.KillAll()\n", machine.ID);

machine.functionCall = 1;

}

::((evt == Kill)) ->

machine.state = AWall_Kill;

atomic

{

printf("machine%d. event_happened:

_Kill_ \n", machine.ID);

machine.curEvent = Kill;

}

//Code

//Code

atomic

{

printf("machine%d.KillAll() \n", machine.ID);

machine.functionCall = 1;

}

::((evt == SetWall)) ->

machine.state = AWall_Wall;

atomic

{

printf("machine%d. event_happened:

_SetWall_ \n", machine.ID);

machine.curEvent = SetWall;

}

//Code

//Code

:: else ->

skip;

fi;

::(machine.state == AWall_Kill) ->

printf("machine%d.state = AWall.Kill \n", machine.ID);

if

::((evt == Reset)) ->

machine.state = AWall_Start;

atomic

{ printf("machine%d.

event_happened:

_Reset_ \n", machine.ID);

machine.curEvent = Reset;

}

//Code

//Code

:: else -> skip;

fi;

::(machine.state == AWall_Wall) ->

printf("machine%d.state = AWall.Wall \n",

machine.ID);

if

:: else -> skip;

fi;

fi;

}

inline APlatform(machine, evt)

{

byte sendEvt;

if

::(machine.state == APlatform_Start) ->

printf("machine%d.state = APlatform.Start \n", machine.ID);

if

::((evt == StartGrow)) ->

machine.state = APlatform_Grow2Walls; atomic

{

printf("machine%d. event_happened:

_StartGrow_ \n", machine.ID); machine.curEvent = StartGrow;

}

//Code

//Code

:: else ->

skip;

fi;

::(machine.state == APlatform_GrowOtherWall) -> printf("machine%d.state = APlatform.GrowOtherWall

\n", machine.ID);

if

::((evt == StopOtherSide)) ->

machine.state = APlatform_Start; atomic

{

printf("machine%d. event_happened:

_StopOtherSide_ \n", machine.ID); machine.curEvent = StopOtherSide;

}

//Code

//Code

::((evt == Update)) ->

machine.state = APlatform_GrowOtherWall; atomic

{

printf("machine%d. event_happened:

_Update_ \n", machine.ID); machine.curEvent = Update;

}

//Code

//Code

atomic

{

printf("machine%d.DoGrowWallOther()\n", machine.ID); machine.functionCall = 2;

}

:: else ->

skip;

fi;

::(machine.state == APlatform_Grow2Walls) -> printf("machine%d.state = APlatform.Grow2Walls \n", machine.ID);

if

::((evt == Update)) ->

machine.state = APlatform_Grow2Walls; atomic

{

printf("machine%d. event_happened:

_Update_ \n", machine.ID);

machine.curEvent = Update;

}

//Code

//Code

atomic

{

printf("machine%d.DoGrowWallOne()\n", machine.ID); machine.functionCall = 3;

}

atomic

{

printf("machine%d.DoGrowWallOther()\n", machine.ID); machine.functionCall = 2;

}

::((evt == StopOneSide)) ->

machine.state = APlatform_GrowOtherWall; atomic

{

printf("machine%d.

event_happened:

_StopOneSide_ \n", machine.ID); machine.curEvent = StopOneSide;

}

//Code

//Code

::((evt == StopOtherSide)) ->

machine.state = APlatform_GrowOneWall;

atomic

{

printf("machine%d. event_happened:

_StopOtherSide_ \n", machine.ID); machine.curEvent = StopOtherSide;

}

//Code

//Code

:: else ->

skip;

fi;

::(machine.state == APlatform_GrowOneWall) -> printf("machine%d.state = APlatform.GrowOneWall

\n", machine.ID);

if

::((evt == StopOneSide)) ->

machine.state = APlatform_Start; atomic

{

printf("machine%d. event_happened:

_StopOneSide_ \n", machine.ID); machine.curEvent = StopOneSide;

}

//Code

//Code

::((evt == Update)) ->

machine.state = APlatform_GrowOneWall;

atomic

{

printf("machine%d. event_happened:

_Update_ \n", machine.ID); machine.curEvent = Update;

}

//Code

//Code

atomic

{

printf("machine%d.DoGrowWallOne()\n", machine.ID); machine.functionCall = 3;

}

:: else ->

skip;

fi;

fi;

}

inline awallVolatileChange()

{

int r;

int ind = 0;

}

inline awallParamChange()

{

int r;

int ind = 0;

}

inline platformVolatileChange()

{

int r;

int ind = 0;

}

inline platformParamChange()

{

int r;

int ind = 0;

}

AWallData awall;

APlatformData platform;

proctype awallProc ()

{

byte newEvt;

awall.started= true;

awall_ch ? newEvt;

awallParamChange();

do

:: awall.finished == false ->

awall_ch ? newEvt;

AWall(awall, newEvt);

:: else -> skip;

od;

}

proctype awallEventSource ()

{

byte newEvt;

do

:: (awall.state == AWall_Start) ->

if

:: (1) -> newEvt = NewHorizontal;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt;

printf("awallsource sent

_NewHorizontal_\n");

}

:: (1) -> newEvt = NewVertical;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt;

printf("awallsource sent

_NewVertical_\n");

}

:: (1) -> newEvt = SetWall;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt; printf("awallsource sent _SetWall_\n");

}

fi;

:: (awall.state == AWall_GrowHorizontal) ->

if

:: (1) -> newEvt = Bounce;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt; printf("awallsource sent _Bounce_\n");

}

:: (1) -> newEvt = Kill;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt; printf("awallsource sent _Kill_\n");

}

:: (1) -> newEvt = SetWall;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt; printf("awallsource sent _SetWall_\n");

}

fi;

:: (awall.state == AWall_GrowVertical) ->

if

:: (1) -> newEvt = Bounce;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt; printf("awallsource sent _Bounce_\n");

}

:: (1) -> newEvt = Kill;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt; printf("awallsource sent _Kill_\n");

}

:: (1) -> newEvt = SetWall;

awallVolatileChange(); platformVolatileChange();

atomic

{

awall_ch ! newEvt;

printf("awallsource sent _SetWall_\n");

}

fi;

:: (awall.state == AWall_Kill) ->

if

:: (1) -> newEvt = Reset;

awallVolatileChange();

platformVolatileChange();

atomic

{

awall_ch ! newEvt;

printf("awallsource sent _Reset_\n");

}

fi;

:: (awall.state == AWall_Wall) ->

skip;

od;

}

proctype platformProc ()

{

byte newEvt;

platform.started= true;

platform_ch ? newEvt;

platformParamChange();

do

:: platform.finished == false ->

platform_ch ? newEvt;

APlatform(platform, newEvt);

:: else -> skip;

od;

}

proctype platformEventSource ()

{

byte newEvt;

do

:: (platform.state == APlatform_Start) ->

if

:: (1) -> newEvt = StartGrow;

awallVolatileChange(); platformVolatileChange(); atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_StartGrow_\n");

}

fi;

:: (platform.state == APlatform_GrowOtherWall) -> if

:: (1) -> newEvt = StopOtherSide;

awallVolatileChange(); platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_StopOtherSide_\n");

}

:: (1) -> newEvt = Update;

awallVolatileChange();

platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_Update_\n");

}

fi;

:: (platform.state == APlatform_Grow2Walls) ->

if

:: (1) -> newEvt = Update;

awallVolatileChange();

platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_Update_\n");

}

:: (1) -> newEvt = StopOneSide;

awallVolatileChange();

platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_StopOneSide_\n");

}

:: (1) -> newEvt = StopOtherSide;

awallVolatileChange();

platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_StopOtherSide_\n");

}

fi;

:: (platform.state == APlatform_GrowOneWall) ->

if

:: (1) -> newEvt = StopOneSide;

awallVolatileChange(); platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_StopOneSide_\n");

}

:: (1) -> newEvt = Update;

awallVolatileChange();

platformVolatileChange();

atomic

{

platform_ch ! newEvt;

printf("platformsource sent

_Update_\n");

}

fi;

od;

}

init

{

awall.ID = 0;

awall.started = false;

awall.finished = false;

awall.state = AWall_Start;

platform.ID = 1;

platform.started = false;

platform.finished = false;

platform.state = APlatform_Start;

run awallProc();

run awallEventSource();

run platformProc();

run platformEventSource();

}

Верификация автомата AWall

Формулы

#define p0 (platform.state == APlatform_Grow2Walls)

#define p1 (platform.state == APlatform_Grow2Walls)

#define p2 (platform.state == APlatform_GrowOneWall)

#define p3 (platform.state == APlatform_GrowOtherWall)

#define p4 (platform.state == APlatform_Grow2Walls)

#define p5 (platform.state == APlatform_GrowOneWall)

#define p6 (platform.state == APlatform_GrowOtherWall)

#define p7 (awall.state == AWall_Kill)

#define p8 (awall.curEvent == Bounce)

#define p9 (awall.state == AWall_Wall)

ltl f0 {[]((p0) -> (p1 U (p2 || p3)))}

ltl f1 {[]((p4 U (p5 || p6)))}

Вывод Spin

ltl f0: [] ((! ((awall.state==3))) || ( ((awall.state==0))))

ltl f1: [] ((! (! ( ((awall.state==3))))) || (

((awall.state==4))))

the model contains 2 never claims: f1, f0

only one claim is used in a verification run

choose which one with ./pan -N name (defaults to -N f0)

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f0)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 144 byte, depth reached 404, errors: 0

2412 states, stored (2804 visited)

1808 states, matched

4612 transitions (= visited+matched)

0 atomic steps

hash factor: 47866.5 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.368 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0.019 seconds

pan: rate 147578.95 states/second

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f1)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 144 byte, depth reached 404, errors: 0

3365 states, stored (4710 visited)

4404 states, matched

9114 transitions (= visited+matched)

0 atomic steps

hash factor: 28496.3 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.513 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0.035 seconds

pan: rate 134571.43 states/second

Верификация автомата APlatform

Формулы:

#define p0 (aplatform.state == APlatform_Grow2Walls)

#define p1 (aplatform.state == APlatform_Grow2Walls)

#define p2 (aplatform.state == APlatform_GrowOneWall)

#define p3 (aplatform.state == APlatform_GrowOtherWall)

#define p4 (aplatform.state == APlatform_Grow2Walls)

#define p5 (aplatform.state == APlatform_GrowOtherWall)

#define p6 (aplatform.state == APlatform_GrowOtherWall)

#define p7 (aplatform.state == APlatform_Start)

#define p8 (aplatform.state == APlatform_GrowOtherWall)

#define p9 (aplatform.curEvent == StopOneSide)

#define p10 (aplatform.curEvent == StopOtherSide)

#define p11 (aplatform.state == APlatform_Start)

#define p12 (aplatform.state == APlatform_GrowOtherWall)

#define p13 (aplatform.state == APlatform_GrowOneWall)

#define p14 (aplatform.state == APlatform_GrowOtherWall)

#define p15 (aplatform.state == APlatform_GrowOneWall)

#define p16 (aplatform.state == APlatform_Grow2Walls)

#define p17 (aplatform.state == APlatform_GrowOtherWall)

#define p18 (aplatform.state == APlatform_GrowOneWall)

#define p19 (aplatform.state == APlatform_GrowOtherWall)

#define p20 (aplatform.state == APlatform_GrowOneWall)

#define p21 (aplatform.state == APlatform_Grow2Walls)

ltl f0 {[]((p0) -> ((p1 U (p2 || p3)) || [](p4)))}

ltl f1 {[]((p5) -> ((p6 U p7) || [](p8)))}

ltl f2 {(( p9) &&( p10)) -> ( p11)}

ltl f3 {( (p12 || p13)) -> (!(p14 &&p15) U p16)}

ltl f4 {( (p17 || p18)) -> (!(p19 &&p20) U p21)}

Вывод Spin

ltl f0: [] ((! ((aplatform.state==2))) ||

((((aplatform.state==2)) U (((aplatform.state==3)) ||

((aplatform.state==1)))) || ([] ((aplatform.state==2)))))

ltl f1: [] ((! ((aplatform.state==1))) ||

((((aplatform.state==1)) U ((aplatform.state==0))) || ([]

((aplatform.state==1)))))

ltl f2: (! (( ((aplatform.curEvent==8))) && (

((aplatform.curEvent==7))))) || ( ((aplatform.state==0)))

ltl f3: (! ( (((aplatform.state==1)) ||

((aplatform.state==3))))) || ((! (((aplatform.state==1)) &&

((aplatform.state==3)))) U ((aplatform.state==2)))

ltl f4: (! ( (((aplatform.state==1)) ||

((aplatform.state==3))))) || ((! (((aplatform.state==1)) &&

((aplatform.state==3)))) U ((aplatform.state==2)))

the model contains 5 never claims: f4, f3, f2, f1, f0

only one claim is used in a verification run

choose which one with ./pan -N name (defaults to -N f0)

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f0)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 132 byte, depth reached 665, errors: 0

3225 states, stored

2090 states, matched

5315 transitions (= stored+matched)

0 atomic steps

hash factor: 41617.9 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.455 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0.02 seconds

pan: rate 161250 states/second

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f1)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 132 byte, depth reached 665, errors: 0

2965 states, stored

1690 states, matched

4655 transitions (= stored+matched)

0 atomic steps

hash factor: 45267.4 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.418 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0.019 seconds

pan: rate 156052.63 states/second

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f2)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 48 byte, depth reached 0, errors: 0

1 states, stored

0 states, matched

1 transitions (= stored+matched)

0 atomic steps

hash factor: 1.34218e+008 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.000 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0 seconds

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f3)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 132 byte, depth reached 56, errors: 0

47 states, stored

7 states, matched

54 transitions (= stored+matched)

0 atomic steps

hash factor: 2.8557e+006 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.007 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0 seconds

(Spin Version 6.2.3 -- 24 October 2012)

+ Partial Order Reduction

Bit statespace search for:

never claim + (f4)

assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 132 byte, depth reached 56, errors: 0

47 states, stored

7 states, matched

54 transitions (= stored+matched)

0 atomic steps

hash factor: 2.8557e+006 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.007 equivalent memory usage for states (stored*(State-

vector + overhead))

16.000 memory used for hash array (-w27)

38.147 memory used for bit stack

343.323 memory used for DFS stack (-m10000000)

397.665 total actual memory usage

pan: elapsed time 0 seconds

<< |
Источник: Лукин Михаил Андреевич. Верификация автоматных программ. Диссертация на соискание ученой степени кандидата технических наук. Санкт-Петербург - 2014. 2014

Еще по теме Приложение Б. Модель и вывод Spinпри верификации логики в игре Tutrleball:

  1. Лукин Михаил Андреевич. Верификация автоматных программ. Диссертация на соискание ученой степени кандидата технических наук. Санкт-Петербург - 2014, 2014
  2. Основные расчетные модели силового сопротивления железобетона
  3. Построение имитационной модели коммутационного устройства
  4. Развитие теории хеджирования и ценообразования опционов после открытия модели Блэка-Шоулса
  5. Структурная модель устройства коммутации с параллельно­конвейерной диспетчеризацией пакетов
  6. 2.2. Анализ метода квантильного хеджирования в рамках модели Блэка-Шоулса
  7. §1. Историческое развитие и современные модели организации нотариата
  8. МЕТОД И АЛГОРИТМ КОММУТАЦИИ С ПАРАЛЛЕЛЬНО­КОНВЕЙЕРНОЙ ДИСПЕТЧЕРИЗАЦИЕЙ ПАКЕТОВ. СТРУКТУРНАЯ МОДЕЛЬ КОММУТАЦИОННОГО УСТРОЙСТВА
  9. Особенности применения метода хеджирования ожидаемых потерь в зависимости от параметров модели
  10. Анализ метода хеджирования ожидаемых потерь в рамках модели Блэка-Шоулса
  11. ПРИЛОЖЕНИЕ В.