88 lines
1.5 KiB
Plaintext
88 lines
1.5 KiB
Plaintext
#######################################
|
|
# Fischer's mutual exclusion protocol #
|
|
#######################################
|
|
# #
|
|
# przy setv1, setv2 - duza delta #
|
|
# przy enter1, enter2 - mala delta #
|
|
# #
|
|
# wzajemne wykluczanie przy: #
|
|
# #
|
|
# mala delta >= duza delta #
|
|
# #
|
|
#######################################
|
|
|
|
net {
|
|
actions {
|
|
start1;
|
|
setv1;
|
|
enter1;
|
|
setv01;
|
|
|
|
start2;
|
|
setv2;
|
|
enter2;
|
|
setv02;
|
|
};
|
|
|
|
automaton proc1 {
|
|
clocks {
|
|
x1;
|
|
};
|
|
locations {
|
|
idle1 { init; };
|
|
try1;
|
|
wait1;
|
|
crit1;
|
|
};
|
|
trans {
|
|
idle1 -> try1, start1, , { x1; };
|
|
try1 -> wait1, setv1, x1 < 1, { x1; };
|
|
wait1 -> crit1, enter1, x1 > 2, { };
|
|
crit1 -> idle1, setv01, , { };
|
|
};
|
|
};
|
|
|
|
automaton proc2 {
|
|
clocks {
|
|
x2;
|
|
};
|
|
locations {
|
|
idle2 { init; };
|
|
try2;
|
|
wait2;
|
|
crit2;
|
|
};
|
|
trans {
|
|
idle2 -> try2, start2, , { x2; };
|
|
try2 -> wait2, setv2, x2 < 1, { x2; };
|
|
wait2 -> crit2, enter2, x2 > 2, { };
|
|
crit2 -> idle2, setv02, , { };
|
|
};
|
|
};
|
|
|
|
automaton varV {
|
|
locations {
|
|
v0 { init; };
|
|
v1;
|
|
v2;
|
|
};
|
|
trans {
|
|
v0 -> v0, start1, , { };
|
|
v0 -> v0, start2, , { };
|
|
v0 -> v1, setv1, , { };
|
|
v0 -> v2, setv2, , { };
|
|
|
|
v1 -> v0, setv01, , { };
|
|
v1 -> v1, enter1, , { };
|
|
v1 -> v1, setv1, , { };
|
|
v1 -> v2, setv2, , { };
|
|
|
|
v2 -> v0, setv02, , { };
|
|
v2 -> v2, enter2, , { };
|
|
v2 -> v1, setv1, , { };
|
|
v2 -> v2, setv2, , { };
|
|
|
|
};
|
|
};
|
|
|
|
}; |