rendered paste bodydeathstarNotEasy: CONTEXT =
BEGIN
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% starship without any modules!
% egysegek tipusai
pilotsType: TYPE = [0..3];
rohamosztagType: TYPE = [0..3];
diplomataType: TYPE = [0..3];
karbantartoType: TYPE = [0..2];
rendfenntartoType: TYPE = [0..5];
% a jobok es a lazado bazisok maximalis szama
MaxLazadoB: NATURAL = 5;
MaxJobs: NATURAL = 5;
state: TYPE = {not_running, rendfenntartas, lazado_bazis_felszamolas,
titkos_kuldetes, haboru_idegen_fajjal, diplomacia};
result: TYPE = {noop, siker, sikertelen};
jobsIdx: TYPE = [1..MaxJobs];
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% push the counter for vader
%%%%%%%%%%%%
update_vader(v: BOOLEAN, v_c: [0..5]): [0..5] =
IF v AND v_c /= 5 THEN v_c + 1
ELSE v_c ENDIF;
main: MODULE =
BEGIN
LOCAL
pilots: pilotsType,
rohamosztag: rohamosztagType,
diplomatak: diplomataType,
karbantartok: karbantartoType,
rendfenntartok: rendfenntartoType,
lazado_bazisok: [0..MaxLazadoB],
vader_is_on_base: BOOLEAN,
flag: array jobsIdx of BOOLEAN,
vader_jobs: [0..5],
tasks: array jobsIdx of state,
helper: result,
tasks_result: array jobsIdx of result
INITIALIZATION
% kezdetben a taskok nem futnak!
tasks = [[i:jobsIdx] not_running];
tasks_result = [[i:jobsIdx] noop];
% kezdeti egysegek szama
pilots = 2;
rohamosztag = 3;
diplomatak = 3;
karbantartok = 2;
rendfenntartok = 5;
% kezdeti lazado bazisok szama
lazado_bazisok = 0;
% vader kezdetben nincs a bazison
vader_is_on_base = FALSE;
vader_jobs = 0;
flag = [[i: jobsIdx] FALSE];
helper in {n:result | n /= noop};
TRANSITION
[
%%%%%%%%%%%%%%%%%%%%%%%%%%%% vader tranziccioi %%%%%%%%%%%%%%%%%%%%%%%%%%%%
vader_comes:
NOT vader_is_on_base
--> vader_is_on_base' = TRUE;
pilots' = pilots + 1
[]
vader_goes:
vader_is_on_base AND pilots /= 0 AND vader_jobs = 5
--> pilots' = pilots - 1;
vader_is_on_base' = FALSE;
vader_jobs' = 0
[]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Adot feladttipusok megkezdeset megvalosito tranziciok %%%%%%%%%%%%%%%%
([] (i: jobsIdx):
rendfenntartas:
tasks[i] = not_running AND rohamosztag /= 0
--> tasks' = tasks WITH [i] := rendfenntartas;
tasks_result'[i] =
helper;
% IF lazado_bazisok = MaxLazadoB THEN siker ELSE helper ENDIF;
rohamosztag' = rohamosztag - 1)
[]
([] (i: jobsIdx):
lazado_bazis_felszamolasa:
tasks[i] = not_running AND pilots /= 0 AND rohamosztag /= 0 AND lazado_bazisok /= 0
--> tasks' = tasks WITH [i] := lazado_bazis_felszamolas;
tasks_result' = tasks_result WITH [i] := helper;
rohamosztag' = rohamosztag - 1;
pilots' = pilots -1;
lazado_bazisok' = lazado_bazisok -1)
[]
([] (i: jobsIdx):
diplomaciai_Kapcs_felvetel:
tasks[i] = not_running AND diplomatak /= 0
--> tasks' = tasks WITH [i] := diplomacia;
tasks_result' = tasks_result WITH [i] := helper;
diplomatak' = diplomatak - 1)
[]
([] (i: jobsIdx):
titkos_kuldetes:
tasks[i] = not_running AND pilots /= 0 AND rohamosztag /= 0 AND diplomatak /= 0 AND karbantartok /= 0 AND rendfenntartok /= 0
--> tasks' = tasks WITH [i] := titkos_kuldetes;
tasks_result' = tasks_result WITH [i] := helper;
pilots' = pilots - 1;
rohamosztag' = rohamosztag - 1;
diplomatak' = diplomatak - 1;
karbantartok' = karbantartok - 1;
rendfenntartok' = rendfenntartok - 1)
[]
([] (i: jobsIdx):
haboru_idegen_fajjal:
tasks[i] = not_running AND ( (1 < rohamosztag) OR (vader_is_on_base AND 1 <= rohamosztag ) )
AND 1 < pilots AND karbantartok /= 0
--> tasks' = tasks WITH [i] := haboru_idegen_fajjal;
tasks_result' = tasks_result WITH [i] := helper;
flag'[i] = IF vader_is_on_base THEN TRUE ELSE FALSE ENDIF;
rohamosztag' = IF vader_is_on_base THEN rohamosztag - 1
ELSE rohamosztag - 2 ENDIF;
pilots' = pilots - 2;
karbantartok' = karbantartok - 1)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%% feladatok lezarasa %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
[]
([] (i: jobsIdx):
sikeres_diplomacia:
tasks[i] = diplomacia AND tasks_result[i] = siker AND rendfenntartok /= 0
--> diplomatak' = diplomatak + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
sikertelen_diplomacia_titkos:
tasks[i] = diplomacia AND tasks_result[i] = sikertelen
AND pilots /= 0 AND rohamosztag /= 0 AND diplomatak /= 0
AND karbantartok /= 0 AND rendfenntartok /= 0
--> tasks' = tasks WITH [i] := titkos_kuldetes;
tasks_result' = tasks_result WITH [i] := helper;
pilots' = pilots - 1;
rohamosztag' = rohamosztag - 1;
diplomatak' = diplomatak - 1;
karbantartok' = karbantartok - 1;
rendfenntartok' = rendfenntartok - 1)
[]
([] (i: jobsIdx):
sikertelen_diplomacia_haboru:
tasks[i] = diplomacia AND tasks_result[i] = sikertelen
AND ( (1 < rohamosztag) OR (vader_is_on_base AND 1 <= rohamosztag ) )
AND 1 < pilots AND karbantartok /= 0
--> tasks' = tasks WITH [i] := haboru_idegen_fajjal;
tasks_result' = tasks_result WITH [i] := helper;
flag'[i] = IF vader_is_on_base THEN TRUE ELSE FALSE ENDIF;
rohamosztag' = IF vader_is_on_base THEN rohamosztag - 1
ELSE rohamosztag - 2 ENDIF;
pilots' = pilots - 2;
karbantartok' = karbantartok - 1;
diplomatak' = diplomatak + 1)
[]
([] (i: jobsIdx):
sikeres_titkos_kuldetes:
tasks[i] = titkos_kuldetes AND tasks_result[i] = siker AND rendfenntartok /= 0
--> pilots' = pilots + 1;
rohamosztag' = rohamosztag + 1;
diplomatak' = diplomatak + 1;
karbantartok' = karbantartok + 1;
rendfenntartok' = rendfenntartok + 1;
lazado_bazisok' = lazado_bazisok + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
sikertelen_titkos_kuldetes:
tasks[i] = titkos_kuldetes AND tasks_result[i] = sikertelen
--> pilots' = pilots + 1;
rohamosztag' = rohamosztag + 1;
diplomatak' = diplomatak + 1;
karbantartok' = karbantartok + 1;
rendfenntartok' = rendfenntartok + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
haboru_idegen_fajjal_kis_javitas:
tasks[i] = haboru_idegen_fajjal AND tasks_result[i] = siker AND rendfenntartok /= 0
--> rohamosztag' = IF flag[i] THEN rohamosztag + 1
ELSE rohamosztag + 2 ENDIF;
pilots' = pilots + 2;
karbantartok' = karbantartok + 1;
flag'[i] = FALSE;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
haboru_idegen_fajjal_nagy_javitas:
tasks[i] = haboru_idegen_fajjal AND tasks_result[i] = sikertelen AND rendfenntartok /= 0
AND (karbantartok /= 0 OR vader_is_on_base = TRUE)
--> rohamosztag' = IF flag[i] THEN rohamosztag + 1
ELSE rohamosztag + 2 ENDIF;
pilots' = pilots + 2;
karbantartok' = karbantartok + 1;
flag'[i] = FALSE;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
lazado_bazis_leigazas_javitas_nelkul:
tasks[i] = lazado_bazis_felszamolas AND tasks_result[i] = siker AND rendfenntartok /= 0
--> rohamosztag' = rohamosztag + 1;
pilots' = pilots + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
lazado_bazis_leigazas_javitassal:
tasks[i] = lazado_bazis_felszamolas AND tasks_result[i] = sikertelen AND rendfenntartok /= 0
AND karbantartok /= 0
--> rohamosztag' = rohamosztag + 1;
pilots' = pilots + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
sikeres_rendfenntartas:
tasks[i] = rendfenntartas AND tasks_result[i] = siker AND rendfenntartok /= 0
--> rohamosztag' = rohamosztag + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
[]
([] (i: jobsIdx):
sikertelen_rendfenntartas:
tasks[i] = rendfenntartas AND tasks_result[i] = sikertelen AND lazado_bazisok < 5
--> rohamosztag' = rohamosztag + 1;
tasks' = tasks WITH [i] := not_running;
tasks_result' = tasks_result WITH [i] := noop;
lazado_bazisok' = lazado_bazisok + 1;
vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
]
END;
stateSzam(tasks: array jobsIdx of state, jobCnt: jobsIdx, typeOfstate: state, sum: NATURAL): NATURAL =
IF jobCnt = 0 THEN
sum
ELSE
IF (tasks[jobCnt] = typeOfstate) THEN
stateSzam(tasks, jobCnt - 1, typeOfstate, sum + 1)
ELSE
stateSzam(tasks, jobCnt - 1, typeOfstate, sum)
ENDIF
ENDIF;
numOfRunningJobs(tasks: array jobsIdx of state, jobCnt: jobsIdx, sum: NATURAL): NATURAL =
IF jobCnt = 0 THEN
sum
ELSE
IF (tasks[jobCnt] /= not_running) THEN
numOfRunningJobs(tasks, jobCnt - 1, sum + 1)
ELSE
numOfRunningJobs(tasks, jobCnt - 1, sum)
ENDIF
ENDIF;
noDead9: THEOREM main |-
(
G( (numOfRunningJobs(tasks, MaxJobs, 0) = 5 ) =>
(F((EXISTS (i: jobsIdx): tasks[i] = not_running)) )
)
);
%%%% 2. a rendszer fair, barmely feladatot el tudja vegezni a halalcsillag
fairSystem: THEOREM main |-
(
FORALL (j: jobsIdx): (tasks[j] /= not_running) => F(tasks[j] = not_running)
);
%%%% 3.
varakozasiSor: THEOREM main |-
(
G(FORALL (i:jobsIdx):
F( (tasks[i] /= not_running) => X(tasks[i] /= not_running) )
)
);
%%%% 4. RENDFENNTARTO ROBOTOK SOSEM FOGYNAK EL A HALALCSILLAGON
rendfenntartok: THEOREM main |- G( 0 < rendfenntartok );
END