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

Модель

#define ALoader_Antsys 0

#define

ALoader_______________________ Kind________________________ 1

#define ALoader_AE 2

#define kind 1

#define Index 2

#define id 3

#define Kind 4

#define ASName 5

#define BegFreq 6

#define EndFreq 7

#define Roll 8

#define Pitch 9

#define Yaw 10

#define Latitude 11

#define Longitude 12

#define Height 13

#define ae 14

#define x 15

#define y 16

#define z 17

#define phase 18

#define ALoader_SetIndex 1

#define ALoader_SetId 2

#define ALoader_SetKind 3

#define ALoader_SetASName 4

#define ALoader_SetBegFreq 5

#define ALoader_SetEndFreq 6

#define ALoader_SetRoll 7

#define ALoader_SetPitch 8

#define ALoader_SetYaw 9

#define ALoader_SetLatitude 10

#define ALoader_SetLongitude 11

#define ALoader_SetHeight 12

#define ALoader_AddAE 13

#define ALoader_NewAE 14

#define ALoader_SetAEid 15

#define ALoader_SetAEX 16

#define ALoader_SetAEY 17

#define ALoader_SetAEZ 18

#define ALoader_SetAEPhase 19

typedef ALoaderData

{

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;

}

#define p0 (loader.state == ALoader_AE)

#define p1 (loader.state == ALoader_AE)

#define p2 (loader.curEvent == kind)

chan loader_ch = [0] of {int}

inline ALoader(machine, evt)

{

byte sendEvt;

if

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

printf("machine%d.state = ALoader.Antsys \n",

machine.ID);

if

::((evt == kind)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d.

_kind_ \n", machine.ID); machine.curEvent = kind;

}

//Code

//Code

:: else ->

skip;

fi;

::(machine.state ==

ALoader_______________________ Kind________________________ ) -

>

printf("machine%d.state =

ALoader.______________________ Kind________________________

\n", machine.ID);

if

::((evt == Index)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d.

_Index_ \n", machine.ID);

machine.curEvent = Index;

}

//Code

//Code

atomic

{

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

machine.functionCall = 1;

}

::((evt == id)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_id_ \n", machine.ID); machine.curEvent = id;

}

//Code

//Code

atomic

{

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

machine.functionCall = 2;

}

::((evt == Kind)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_Kind_ \n", machine.ID); machine.curEvent = Kind;

}

//Code

//Code

atomic

{

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

machine.functionCall = 3;

}

::((evt == ASName)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_ASName_ \n", machine.ID); machine.curEvent = ASName;

}

//Code

//Code

atomic

{

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

machine.functionCall = 4;

}

::((evt == BegFreq)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_BegFreq_ \n", machine.ID);

machine.curEvent = BegFreq;

}

//Code

//Code

atomic

{

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

machine.functionCall = 5;

}

::((evt == EndFreq)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_EndFreq_ \n", machine.ID);

machine.curEvent = EndFreq;

}

//Code

//Code

atomic

{

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

machine.functionCall = 6;

}

::((evt == Roll)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d.

_Roll_ \n", machine.ID); machine.curEvent = Roll;

}

//Code

//Code

atomic

{

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

machine.functionCall = 7;

}

::((evt == Pitch)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_Pitch_ \n", machine.ID); machine.curEvent = Pitch;

}

//Code

//Code

atomic

{ printf("machine%d.SetPitch()\n",

machine.ID); machine.functionCall = 8;

}

::((evt == Yaw)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{ printf("machine%d. event_happened:

_Yaw_ \n", machine.ID); machine.curEvent = Yaw;

}

//Code

//Code

atomic

{ printf("machine%d.SetYaw()\n",

machine.ID); machine.functionCall = 9;

}

::((evt == Latitude)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_Latitude_ \n", machine.ID);

machine.curEvent = Latitude;

}

//Code

//Code

atomic

{

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

machine.functionCall = 10;

}

::((evt == Longitude)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_Longitude_ \n", machine.ID); machine.curEvent = Longitude;

}

//Code

//Code

atomic

{ printf("machine%d.SetLongitude()\n",

machine.ID);

machine.functionCall = 11;

}

::((evt == Height)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{ printf("machine%d. event_happened:

_Height_ \n", machine.ID); machine.curEvent = Height;

}

//Code

//Code

atomic

{ printf("machine%d.SetHeight()\n",

machine.ID);

machine.functionCall = 12;

}

::((evt == ae)) ->

machine.state = ALoader_AE;

atomic

{ printf("machine%d.

_ae_ \n", machine.ID);

machine.curEvent = ae;

}

//Code

//Code

atomic

{

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

machine.functionCall = 14;

}

:: else -> skip;

fi;

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

printf("machine%d.state = ALoader.AE \n", machine.ID);

if

::((evt == ae)) ->

machine.state =

ALoader_______________________ Kind________________________ ;

atomic

{

printf("machine%d. event_happened:

_ae_ \n", machine.ID);

machine.curEvent = ae;

}

//Code

//Code

atomic

{

printf("machine%d.AddAE()\n",

machine.ID);

machine.functionCall = 13;

}

::((evt == id)) ->

machine.state = ALoader_AE;

atomic

{ printf("machine%d. event_happened:

_id_ \n", machine.ID);

machine.curEvent = id;

}

//Code

//Code

atomic

{

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

machine.functionCall = 15;

}

::((evt == x)) ->

machine.state = ALoader_AE;

atomic

{ printf("machine%d. event_happened:

_x_ \n", machine.ID); machine.curEvent = x;

}

//Code

//Code

atomic

{

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

machine.functionCall = 16;

}

::((evt == y)) ->

machine.state = ALoader_AE;

atomic

{

printf("machine%d. event_happened:

_y_ \n", machine.ID); machine.curEvent = y;

}

//Code

//Code

atomic

{

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

machine.functionCall = 17;

}

::((evt == z)) ->

machine.state = ALoader_AE;

atomic

{

printf("machine%d. event_happened:

_z_ \n", machine.ID);

machine.curEvent = z;

}

//Code

//Code

atomic

{

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

machine.functionCall = 18;

}

::((evt == phase)) ->

machine.state = ALoader_AE;

atomic

{

printf("machine%d.

_phase_ \n", machine.ID); machine.curEvent = phase;

}

//Code

//Code

atomic

{

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

machine.functionCall = 19;

}

:: else -> skip;

fi;

fi;

}

inline loaderVolatileChange()

{

int r;

int ind = 0;

}

inline loaderParamChange()

{

int r;

int ind = 0;

}

ALoaderData loader;

proctype loaderProc ()

{

byte newEvt;

loader.started= true;

loader_ch ? newEvt;

loaderParamChange();

do

:: loader.finished == false ->

loader_ch ? newEvt;

ALoader(loader, newEvt);

:: else -> skip;

od;

}

proctype loaderEventSource ()

{

byte newEvt;

do

:: (loader.state == ALoader_Antsys) ->

if

:: (1) -> newEvt = kind;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _kind_\n");

}

fi;

:: (loader.state ==

ALoader_______________________ Kind________________________ ) -

>

if

:: (1) -> newEvt = Index;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Index_\n");

}

:: (1) -> newEvt = id;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _id_\n");

}

:: (1) -> newEvt = Kind;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Kind_\n");

}

:: (1) -> newEvt = ASName;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _ASName_\n");

}

:: (1) -> newEvt = BegFreq;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _BegFreq_\n");

}

:: (1) -> newEvt = EndFreq;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _EndFreq_\n");

}

:: (1) -> newEvt = Roll;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Roll_\n");

}

:: (1) -> newEvt = Pitch;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Pitch_\n");

}

:: (1) -> newEvt = Yaw;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Yaw_\n");

}

:: (1) -> newEvt = Latitude;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Latitude_\n");

}

:: (1) -> newEvt = Longitude;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent

_Longitude_\n");

}

:: (1) -> newEvt = Height;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _Height_\n");

}

:: (1) -> newEvt = ae;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _ae_\n");

}

fi;

:: (loader.state == ALoader_AE) ->

if

:: (1) -> newEvt = ae;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _ae_\n");

}

:: (1) -> newEvt = id;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _id_\n");

}

:: (1) -> newEvt = x;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _x_\n");

}

:: (1) -> newEvt = y;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _y_\n");

}

:: (1) -> newEvt = z;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _z_\n");

}

:: (1) -> newEvt = phase;

loaderVolatileChange();

atomic

{

loader_ch ! newEvt;

printf("loadersource sent _phase_\n");

}

fi;

od;

}

init

{

loader.ID = 0;

loader.started = false;

loader.finished = false;

loader.state = ALoader_Antsys;

run loaderProc();

run loaderEventSource();

}

Вывод верификатора Spin

ltl f0 {( p0 ) -> (!p1 U p2)}

ltl f0: (! ( ((loader.state==2)))) || ((! ((loader.state==2)))

U ((loader.curEvent==1)))

ltl f1: [] ((! (((loader.state==1)) && ((loader.curEvent==14))))

|| ((! ((loader.state==1))) U ((loader.curEvent==14))))

ltl f2: [] ((! (((loader.state==2)) && ((loader.curEvent==15))))

|| (((loader.functionCall==16)) U ((loader.state==2)))) the model contains 3 never claims: 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 224 byte, depth reached 58, errors: 0

90 states, stored

8 states, matched

98 transitions (= stored+matched)

0 atomic steps

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

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

0.021 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.001 seconds

(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 224 byte, depth reached 5094, errors: 0

35274 states, stored

15475 states, matched

50749 transitions (= stored+matched)

0 atomic steps

hash factor: 3805 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

8.074 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)

398.153 total actual memory usage

pan: elapsed time 0.303 seconds

pan: rate 116415.84 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 224 byte, depth reached 5094, errors: 0

35274 states, stored

15475 states, matched

50749 transitions (= stored+matched)

0 atomic steps

hash factor: 3805 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):

8.074 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)

398.153 total actual memory usage

pan: elapsed time 0.292 seconds

pan: rate 120801.37 states/second