Potřebné informace o smv najdete na adrese spinroot.com/.
Jde se zde doklikat i k manuálu, podle kterého bylo toto stvořeno
Bez větších problému přesně podle popisu ze zmíněných stránek
Mapsani kodu stanic, hlavni stanice, monituru, ktery obsahuje kontrolovane invarianty.
Kod pozuity pro verifikaci a simulaci
/* pojmenovani jednotlivych stanic */
#define station_S 1
#define station_A 2
#define station_B 3
#define no_station 4
/* kolik vlaku se vejde do stanice S */
#define station_size 10
/*kolik vlaku se vejde na trat, je >= nez station_size, nemusi se pak testovat, zda je plny*/
#define track_size 10
#define max_track_length 3
/* delka trate v jednotkach casu, kterou ji vlak pojede */
#define track_A_S_length 2
/* delka trate v jednotkach casu, kterou ji vlak pojede */
#define track_B_S_length 3
/* delka stani (minimalni) na stanici */
#define min_time_on_station 2
/* pokud uz takhle dlouho z koncove stanice nevyjel vlak, tak pokud muze, urcite vyjede */
#define try_send_train_interval 5
/* po jake dobe se vynuti jizda vlaku nejakym smerem, pokud tam uz dlouho nejel */
#define one_direction_timeout_A 5
#define one_direction_timeout_B 7
/* maximum z vyse */
#define max_direction_timeout 7
#define SEMAPHORE_UP 1
#define SEMAPHORE_DOWN 0
#define TRUE 1
#define FALSE 0
/* jak dlouhe je kolecko pro cas. je vhodne ho dat vzhedem state - expolsion volit co nejmensi */
#define TIME_MODULO 15
/* typ pro vlak, ktery je posilan kanalem, trati */
typedef train_t {
byte dest; /* cilova stanice, bud A nebo B */
byte arrival_time; /* cas, kdy vlak vyrazil */
};
/* typ pro trat, jednak vlaky, ktere se vydaly na cestu, a jednak stav trati */
typedef track_t {
chan trains = [track_size] of {train_t}; /* kanal, kde jsou vsecky vlaky vyslane na cestu */
byte length;
bool semaphore_from_S; /* semafor v prislusnem smeru */
bool semaphore_to_S; /* semafor v prislusnem smeru */
byte leading_to; /* kam vede tato trat */
bit time; /* jestli uz v tomto case byla provedena akce v rpislusne stanici(pripadne vyslani vlaku) */
short last_train_to_S; /* pocitadlo casu, kdy jel posledni vlak do S po teto trati */
short last_train_from_S; /* pocitadlo casu, kdy jel posledni vlak z S po teto trati */
bit force_sending; /* pokud je true, je vynuceno posilani vlaku z S do ES, a ceka se, nez takovy nejaky vlak pojede */
};
/* typ pro nastupiste */
typedef platform_t {
bool isfull; /* zda je obsazene */
train_t train; /* vlak na danem nastupisti */
int departure_time; /* cas odjezdu */
byte continue_to; /* v jakem smeru vlak pokracuje */
bit should_gone; /* priznak, pokud vlak uz mel odjet a jeste tak neucinil protoze trat byla plna */
}
/************************************************************************************************/
/* GLOBALNI PROMENNE */
/************************************************************************************************/
/* trati se stanice A do S a ze stanice B do S */
track_t track_A_S;
track_t track_B_S;
/* znacka, pro aktualni cas, neni to absolutni cas, ale je to cyklicka promenna, jedina podminka na ni je, aby
byla vetsi nez nejdelasi trat.
*/
byte global_time;
byte n_free_platforms = station_size; /* pocet volnych nastupist na stanici S */
short tmpx; /*pomocna promenna*/
bit checked_in_this_time = FALSE;
/*funkce na praci se zacyklenym casem */
inline increase_byte_modulo(base, addition){
tmpx = base + addition;
do
::(tmpx > TIME_MODULO)->
tmpx = tmpx - TIME_MODULO;
::(tmpx == TIME_MODULO)->
tmpx = 0;
::else -> break;
od;
base = tmpx;
}
/*funkce na inkrementaci casu a vseho co s nim souvisi */
inline increase_time(){
track_A_S.last_train_to_S++;
track_A_S.time = FALSE;
track_B_S.time = FALSE;
track_A_S.last_train_from_S++;
track_B_S.last_train_to_S++;
track_B_S.last_train_from_S++;
checked_in_this_time = FALSE;
increase_byte_modulo(global_time, 1);
}
/* ..z koncovych stanic do S. musi byt volna z atomic bloku, kde se vi, ze semaform pro danou trat je UP */
inline send_train_toS(track){
printf("Sending train from station %d , to oposit station is %d,
semaphore to S is %d \n", track.leading_to, oposit_station_name, track.semaphore_to_S);
arr_time = global_time;
increase_byte_modulo(arr_time, track.length)
train.arrival_time = arr_time;
train.dest = oposit_station_name;
n_free_platforms --; /* zabrat si misto na statnici S */
track.semaphore_from_S = SEMAPHORE_DOWN; /*posilame vlak do S, takze semafor z S musi byt DOWN */
printf("semaphore from S set to %d \n", track.semaphore_from_S);
track.trains ! train;
track.last_train_to_S = 0; /* vynulovat cas, kdy tam mel jet vlak */
}
/* nedeterministicky se rozhodne, zda vlak poslat, nebo ne. Pokud uz dlouho neposlal, tak pokud muze, tak posle */
inline maybe_send_train_toS(track){
if
/* pokud jsme uz dlouho neposlali vlak, tak ho posleme urcite, pokud muzeme */
::(track.last_train_to_S > try_send_train_interval)->
send_train_toS(track);
/* jinak se rozhodnem nedeterministicky, zda ho posleme, nebo ne */
::(track.last_train_to_S <= try_send_train_interval)->
send_train_toS(track);
::(track.last_train_to_S <= try_send_train_interval)->
skip;
::(track.last_train_to_S <= try_send_train_interval)->
skip;
::(track.last_train_to_S <= try_send_train_interval)->
skip;
fi;
}
/* jedna z koncovych stanic */
proctype EndStationA(){
train_t train;
byte oposit_station_name;
byte arr_time;
oposit_station_name = station_B;
do
/* pokud muzes poslat vlak do S */
::((track_A_S.semaphore_to_S == SEMAPHORE_UP) && (track_A_S.time == FALSE)
&& (n_free_platforms > 0) && (track_A_S.force_sending == FALSE) )->
atomic { /* test and set atomicky, jeste jednou zkontrolovat, mohlo se to preplanovat, a nekdo mohl
treba poslat vlak z druhe strany */
if
::((track_A_S.semaphore_to_S == SEMAPHORE_UP) && (n_free_platforms > 0) && (track_A_S.time == FALSE) && (track_A_S.force_sending == FALSE) )->
maybe_send_train_toS(track_A_S);
track_A_S.time = TRUE;
:: else -> skip;
fi;
}
/* prijmout vlaky, ktere maji dorazit v tomto case */
::(track_A_S.trains?[station_A, eval(global_time)])->
track_A_S.trains ? train; /* do toho nam nikdo nemuze skocit, nemusi to byt atomicky */
track_A_S.force_sending = FALSE;
track_A_S.last_train_from_S = 0;
atomic { /* ale do tohohle uz jo */
if
:: (empty(track_A_S.trains) ) -> track_A_S.semaphore_to_S = SEMAPHORE_UP;
:: (nempty(track_A_S.trains) )->skip;
fi
}
printf ("train arived to station A \n");
od;
}
/* jedna z koncovych stanic */
proctype EndStationB(){
train_t train;
byte oposit_station_name;
byte arr_time;
oposit_station_name = station_A;
do
/* pokud muzes poslat vlak do S */
::((track_B_S.semaphore_to_S == SEMAPHORE_UP) && (n_free_platforms > 0)
&& (track_B_S.time == FALSE) && (track_B_S.force_sending == FALSE) )->
atomic { /* test and set atomicky, jeste jednou zkontrolovat, mohlo se to preplanovat, a nekdo mohl
treba poslat vlak z druhe strany */
if
::((track_B_S.semaphore_to_S == SEMAPHORE_UP) && (n_free_platforms > 0) && (track_B_S.time == FALSE) && (track_B_S.force_sending == FALSE))->
maybe_send_train_toS(track_B_S);
track_B_S.time = TRUE;
printf("semaphore from S set to %d \n", track_B_S.semaphore_from_S);
:: else -> skip;
fi;
}
/* prijmout vlaky, ktere maji dorazit v tomto case */
::(track_B_S.trains?[station_B, eval(global_time)])->
track_B_S.trains? train; /* do toho nam nikdo nemuze skocit, nemusi to byt atomicky */
track_B_S.force_sending = FALSE;
track_B_S.last_train_from_S = 0;
atomic { /* ale do tohohle uz jo */
if
:: (empty(track_B_S.trains) ) -> track_B_S.semaphore_to_S = SEMAPHORE_UP;
:: (nempty(track_B_S.trains) )->skip;
fi
}
printf ("train arived to station B \n");
od;
}
/* vycisteni nastupiste po tom co z nej odjede vlak */
inline clear_platform(platform){
platform.isfull = FALSE;
platform.should_gone = FALSE;
}
/*procedura na vyslani vlaku ze stanice S na trat track */
inline send_train_from_S(track) {
if
::(track.semaphore_from_S == SEMAPHORE_UP)->
track.semaphore_to_S = SEMAPHORE_DOWN;
increase_byte_modulo(tmp, track.length);
platforms[index].train.arrival_time = tmp;
track.trains!platforms[index].train;
clear_platform(platforms[index]);
n_free_platforms ++;
::else->skip; /* nechceme, aby se nam to tu zablokovalo */
fi;
}
/*zkontroluje, zda nejdou nejake vlaky odeslat a pripadne je vysle */
inline send_prepared_trains(){
index = 0;
tmp = global_time;
do
::(index < station_size)->
if
::(platforms[index].isfull == TRUE &&
platforms[index].departure_time == global_time)-> platforms[index].should_gone = TRUE;
::else -> skip;
fi;
if
::(platforms[index].isfull == TRUE && platforms[index].should_gone
&& platforms[index].continue_to == station_A && track_A_S.semaphore_from_S == SEMAPHORE_UP )->
atomic {send_train_from_S(track_A_S) };
::(platforms[index].isfull == TRUE && platforms[index].should_gone
&& platforms[index].continue_to == station_B && track_B_S.semaphore_from_S == SEMAPHORE_UP )->
atomic {send_train_from_S(track_B_S)};
::else -> skip;
fi;
index++;
::(index == station_size)-> break;
od;
}
/* prijia vlaky do stanice S muze byt volana jen z bloku chraneneho jako atomic */
inline receive_train(track){
index = 0;
do
::(index < station_size)->
if
:: (platforms[index].isfull == FALSE)-> /* najit si nejake volne nastupiste */
break;
:: (platforms[index].isfull == TRUE)-> skip;
fi;
index ++;
:: (index == station_size)->
printf("Pruser jako svina, sem se to nikda nemelo dostat\n");
assert(!(index == station_size) );
od;
track.trains ? train;
tmp = global_time;
increase_byte_modulo(tmp,min_time_on_station);
platforms[index].departure_time = tmp;
platforms[index].isfull = TRUE;
platforms[index].continue_to = train.dest;
platforms[index].train.dest = train.dest;
if
::(empty(track.trains))-> //trat je prazdna, zvednout semafor semafor
track.semaphore_from_S = SEMAPHORE_UP;
::(nempty(track.trains))-> skip;
fi;
}
/* vynuti to, ze v konecnem case bude vyaln vlak z A do prislusne stanice */
inline force_send(track){
track.force_sending = TRUE;
}
proctype StationS (){
/* pole nastupist */
platform_t platforms[station_size];
byte index;
byte tmp;
train_t train;
/*inicializace nastupist */
index = 0;
do
::(index < station_size)->
clear_platform(platforms[index]);
index ++;
:: (index == station_size)->
break;
od;
do
/*zkontrolovat zda je na nadrazi je nejaky vlak, ktery muze odjet*/
::(checked_in_this_time == FALSE)->
checked_in_this_time = TRUE;
send_prepared_trains();
/* je na trati je nejaky vlak k prijeti z A? */
::(track_A_S.trains ? [ station_B , eval(global_time)])->
atomic {receive_train(track_A_S);} /* nesmime se preplanovat v pulce prijimani vlaku, */
/* je na trati je nejaky vlak k prijeti z B? */
::(track_B_S.trains ? [station_A , eval(global_time)])->
atomic { receive_train(track_B_S); }
/*dlouho jsme neposlali vlak do A*/
::(track_A_S.last_train_from_S > one_direction_timeout_A && track_A_S.force_sending == FALSE )->
force_send(track_A_S);
/*dlouho jsme neposlali vlak do B*/
::(track_B_S.last_train_from_S > one_direction_timeout_B && track_B_S.force_sending == FALSE )->
force_send(track_B_S);
od;
}
/* spousti se, pokud nic jineho nemuze popojet, posouva u vlaku, jak dlouho jsou na trati/nastupisti */
proctype Timer(){
do
::timeout ->
increase_time();
od;
}
/*kontroluje model, ze je v poradku */
proctype Monitor(){
byte max_time_S_End = 255;
byte max_time_End_S = 255;
do
/*kontrola, ze se nesrazeji vlaky na trati A_S */
:: ( (track_A_S.trains ?? [station_B,_]) && track_A_S.trains ?? [station_A,_] ) ->
assert( !(track_A_S.trains ?? [station_B,_] && track_A_S.trains ?? [station_A,_]) );
/*kontrola, ze se nesrazeji vlaky na trati B_S */
:: (track_B_S.trains ?? [station_B,_] && track_B_S.trains ?? [station_A,_]) ->
assert(!(track_B_S.trains ?? [station_B,_] && track_A_S.trains ?? [station_A,_]) );
/* jde se ve zhora omezenem case dostat z z S do konocovych stanic */
:: (track_A_S.last_train_from_S > max_time_S_End) ->
assert(!(track_A_S.last_train_from_S > max_time_S_End));
:: (track_B_S.last_train_from_S > max_time_S_End)->
assert(!(track_B_S.last_train_from_S > max_time_S_End));
/* jde se ve zhora omezenem case dostat z koncovych stanic do S */
:: (track_A_S.last_train_to_S > max_time_S_End)->
assert(!(track_A_S.last_train_from_S > max_time_S_End));
:: (track_B_S.last_train_from_S > max_time_S_End)->
assert(!(track_B_S.last_train_from_S > max_time_S_End));
od;
}
init{
/* inicializovat trati */
track_A_S.length = 3;
track_A_S.time = FALSE;
track_A_S.force_sending = FALSE;
track_B_S.force_sending = FALSE;
track_A_S.semaphore_from_S = 1;
track_A_S.semaphore_to_S = 1;
track_A_S.leading_to = station_A;
track_B_S.length = 4;
track_B_S.semaphore_from_S = 1;
track_B_S.semaphore_to_S = 1;
track_B_S.leading_to = station_B;
track_B_S.time = FALSE;
/* spusteni koncovych stanic */
run EndStationA();
/* spusteni stanice S */
run StationS();
/* spusteni koncovych stanic */
run EndStationB();
/*timer */
run Timer();
/* kontorla */
run Monitor();
}
Simulace je pekna v xspinu, je tam pekne videt napr, ze se vlaky nesrazi. Pri ladeni, kdyz byla v protokolu chyba objevila se v simulaci velmi brzy
Mela by se pouzit exhaustiv, ale protoze na to jsem nemel pamet, pouzil jsem bitstate (jen nektere stavy a hasovani mezi nimi)
Kod pozuity pro verifikaci a simulaci
error: max search depth too small
Depth= 999999 States= 1e+06 Transitions= 1.07884e+06 Memory= 53.801
Depth= 999999 States= 2e+06 Transitions= 2.86111e+06 Memory= 53.801
Depth= 999999 States= 3e+06 Transitions= 4.64646e+06 Memory= 53.801
Depth= 999999 States= 4e+06 Transitions= 6.56122e+06 Memory= 53.801
Depth= 999999 States= 5e+06 Transitions= 8.51564e+06 Memory= 53.801
Depth= 999999 States= 6e+06 Transitions= 1.04725e+07 Memory= 53.801
Depth= 999999 States= 7e+06 Transitions= 1.228e+07 Memory= 53.801
Depth= 999999 States= 8e+06 Transitions= 1.40956e+07 Memory= 53.801
Depth= 999999 States= 9e+06 Transitions= 1.59908e+07 Memory= 53.801
Depth= 999999 States= 1e+07 Transitions= 1.77607e+07 Memory= 53.801
Depth= 999999 States= 1.1e+07 Transitions= 1.93466e+07 Memory= 53.801
Depth= 999999 States= 1.2e+07 Transitions= 2.09984e+07 Memory= 53.801
Depth= 999999 States= 1.3e+07 Transitions= 2.26599e+07 Memory= 53.801
Depth= 999999 States= 1.4e+07 Transitions= 2.4494e+07 Memory= 53.801
Depth= 999999 States= 1.5e+07 Transitions= 2.62457e+07 Memory= 53.801
Depth= 999999 States= 1.6e+07 Transitions= 2.81444e+07 Memory= 53.801
Depth= 999999 States= 1.7e+07 Transitions= 2.98162e+07 Memory= 53.801
Depth= 999999 States= 1.8e+07 Transitions= 3.15215e+07 Memory= 53.801
Depth= 999999 States= 1.9e+07 Transitions= 3.32735e+07 Memory= 53.801
(Spin Version 4.2.7 -- 23 June 2006)
+ Partial Order Reduction
Bit statespace search for:
never claim - (not selected)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 244 byte, depth reached 999999, errors: 0
1.96241e+07 states, stored
1.47749e+07 states, matched
3.4399e+07 transitions (= stored+matched)
1.87497e+07 atomic steps
hash factor: 3.41971 (best if > 100.)
bits set per state: 3 (-k3)
Stats on memory usage (in Megabytes):
4866.782 equivalent memory usage for states (stored*(State-vector + overhead))
16.777 memory used for hash array (-w26)
36.000 memory used for DFS stack (-m1000000)
0.964 other (proc and chan stacks)
0.060 memory lost to fragmentation
53.801 total actual memory usage
unreached in proctype EndStationA
line 220, "pan_in", state 80, "-end-"
(1 of 80 states)
unreached in proctype EndStationB
line 256, "pan_in", state 81, "-end-"
(1 of 81 states)
unreached in proctype StationS
line 321, "pan_in", state 100, "assert(!((index==10)))"
line 321, "pan_in", state 142, "assert(!((index==10)))"
line 381, "pan_in", state 181, "-end-"
(3 of 181 states)
unreached in proctype Timer
line 134, "pan_in", state 11, "tmpx = (tmpx-15)"
line 390, "pan_in", state 25, "-end-"
(2 of 25 states)
unreached in proctype Monitor
line 400, "pan_in", state 2, "assert(!((track_A_S.trains??[3,_]&&track_A_S.trains??[2,_])))"
line 403, "pan_in", state 4, "assert(!((track_B_S.trains??[3,_]&&track_A_S.trains??[2,_])))"
line 406, "pan_in", state 6, "assert(!((track_A_S.last_train_from_S>max_time_S_End)))"
line 408, "pan_in", state 8, "assert(!((track_B_S.last_train_from_S>max_time_S_End)))"
line 411, "pan_in", state 10, "assert(!((track_A_S.last_train_from_S>max_time_S_End)))"
line 413, "pan_in", state 12, "assert(!((track_B_S.last_train_from_S>max_time_S_End)))"
line 415, "pan_in", state 16, "-end-"
(7 of 16 states)
unreached in proctype :init:
(0 of 18 states)
85.80user 0.09system 1:26.32elapsed 99%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+13296minor)pagefaults 0swaps
Na prvnim řádku, že jsme neprošli celý satvový prostor, že to je jen odhad, jak by to mohlo dopadnout.
Nedosažitelné stavy v monitoru a ve stanici S značí, že žádná z kontrolovaných cest neporušila žádný konrolovaný invariant
Nedosažitelný stav v timeru je způsoben tím, že procedura increase_byte_modulo může mít jako druhý parametr i něco jiného
než jedničku, ovšem timer vždy zvyšuje čas jen o jedničku. Tento nedosažitelný stav je tedy OK (daná inline procedura je společná
několika procesům, v jiných je tento stav dosažitelný)
Důležité je zejména, že invarianty jsou validní a je značná šance, že protokol je funkční
Programovaci jazyk se tvari jako normalni, (if - fi;), ale normalne se nechova (blokovaniv if),. Nepodarilo se mi vymyslet, jak predat nejakou promennou procesu referenci a ne hodnotou.