Skip to content

Instantly share code, notes, and snippets.

@Slava0135

Slava0135/peterson2.smv

Created December 12, 2023 09:03
Show Gist options
  • Save Slava0135/93aa8d32f2241c0270b4306db1bd9304 to your computer and use it in GitHub Desktop.
Save Slava0135/93aa8d32f2241c0270b4306db1bd9304 to your computer and use it in GitHub Desktop.
Download ZIP
peterson algorithm (nuXMV)
Raw
peterson2.smv
MODULE mutex(turn, flag, n)
VAR
state : { IDLE, WAIT, CRIT };
ASSIGN
init(state) := IDLE;
next(state) :=
case
state = IDLE : { IDLE, WAIT };
state = WAIT & !(flag[w] & turn = w) : CRIT;
state = CRIT : { CRIT, IDLE };
TRUE : state;
esac;
next(turn) :=
case
state = IDLE & next(state) = WAIT : w;
TRUE : turn;
esac;
next(flag[n]) :=
case
state = IDLE & next(state) = WAIT : TRUE;
state = CRIT & next(state) = IDLE : FALSE;
TRUE : flag[n];
esac;
DEFINE
w := (n = 0) ? 1 : 0;
FAIRNESS running;
MODULE main
VAR
turn : 0..1;
flag : array 0..1 of boolean;
proc0 : process mutex(turn, flag, 0);
proc1 : process mutex(turn, flag, 1);
ASSIGN
init(turn) := { 0, 1 };
init(flag[0]) := FALSE;
init(flag[1]) := FALSE;
CTLSPEC -- отсутствие одновременного нахождения любых двух процессов в критической секции
AG ( ( proc0.state = CRIT -> proc1.state != CRIT ) & ( proc1.state = CRIT -> proc0.state != CRIT ) )
CTLSPEC -- любой процесс, захотевший войти в крит. секцию, в конце концов в нее войдет
AG ( ( proc0.state = WAIT -> EF ( proc0.state = CRIT ) ) & ( proc1.state = WAIT -> EF ( proc1.state = CRIT ) ) )
LTLSPEC -- отсутствие дедлока у процессов
!F G ( proc0.state = WAIT & proc1.state = WAIT )
Raw
peterson4.smv
MODULE mutex(level, last_to_enter, i)
VAR
state : { IDLE, WAIT, CRIT };
l : 0..3;
ASSIGN
init(state) := IDLE;
next(state) :=
case
state = IDLE : { IDLE, WAIT };
state = WAIT & l = 3 : CRIT;
state = CRIT : { CRIT, IDLE };
TRUE : state;
esac;
next(l) :=
case
state = IDLE & next(state) = WAIT : 0;
state = WAIT & l < 3 & !(
last_to_enter[l] = i & (
(i != 0 & level[0] >= l) |
(i != 1 & level[1] >= l) |
(i != 2 & level[2] >= l) |
(i != 3 & level[3] >= l)
)
) : l + 1;
TRUE : l;
esac;
next(level[i]) :=
case
state = IDLE & next(state) = WAIT : 0;
state = WAIT : next(l);
state = CRIT & next(state) = IDLE : -1;
TRUE : level[i];
esac;
next(last_to_enter[0]) :=
case
state = IDLE & next(state) = WAIT : i;
TRUE : last_to_enter[0];
esac;
next(last_to_enter[1]) :=
case
state = WAIT & next(l) = 1 & l != next(l) : i;
TRUE : last_to_enter[1];
esac;
next(last_to_enter[2]) :=
case
state = WAIT & next(l) = 2 & l != next(l) : i;
TRUE : last_to_enter[2];
esac;
FAIRNESS running;
MODULE main
VAR
level : array 0..3 of -1..3;
last_to_enter : array 0..2 of 0..3;
proc0 : process mutex(level, last_to_enter, 0);
proc1 : process mutex(level, last_to_enter, 1);
proc2 : process mutex(level, last_to_enter, 2);
proc3 : process mutex(level, last_to_enter, 3);
ASSIGN
init(level[0]) := -1;
init(level[1]) := -1;
init(level[2]) := -1;
init(level[3]) := -1;
init(last_to_enter[0]) := 0;
init(last_to_enter[1]) := 0;
init(last_to_enter[2]) := 0;
CTLSPEC -- отсутствие одновременного нахождения любых двух процессов в критической секции
AG (
( proc0.state = CRIT -> proc1.state != CRIT & proc2.state != CRIT & proc3.state != CRIT ) &
( proc1.state = CRIT -> proc0.state != CRIT & proc2.state != CRIT & proc3.state != CRIT ) &
( proc2.state = CRIT -> proc0.state != CRIT & proc1.state != CRIT & proc3.state != CRIT ) &
( proc3.state = CRIT -> proc0.state != CRIT & proc1.state != CRIT & proc2.state != CRIT )
)
CTLSPEC -- любой процесс, захотевший войти в крит. секцию, в конце концов в нее войдет
AG (
( proc0.state = WAIT -> EF ( proc0.state = CRIT ) ) &
( proc1.state = WAIT -> EF ( proc1.state = CRIT ) ) &
( proc2.state = WAIT -> EF ( proc2.state = CRIT ) ) &
( proc3.state = WAIT -> EF ( proc3.state = CRIT ) )
)
LTLSPEC -- отсутствие дедлока у процессов
!F G ( proc0.state = WAIT & proc1.state = WAIT & proc2.state = WAIT & proc3.state = WAIT )
Raw
peterson5.smv
MODULE mutex(level, last_to_enter, i)
VAR
state : { IDLE, WAIT, CRIT };
l : 0..4;
ASSIGN
init(state) := IDLE;
next(state) :=
case
state = IDLE : { IDLE, WAIT };
state = WAIT & l = 4 : CRIT;
state = CRIT : { CRIT, IDLE };
TRUE : state;
esac;
next(l) :=
case
state = IDLE & next(state) = WAIT : 0;
state = WAIT & l < 4 & !(
last_to_enter[l] = i & (
(i != 0 & level[0] >= l) |
(i != 1 & level[1] >= l) |
(i != 2 & level[2] >= l) |
(i != 3 & level[3] >= l) |
(i != 4 & level[4] >= l)
)
) : l + 1;
TRUE : l;
esac;
next(level[i]) :=
case
state = IDLE & next(state) = WAIT : 0;
state = WAIT : next(l);
state = CRIT & next(state) = IDLE : -1;
TRUE : level[i];
esac;
next(last_to_enter[0]) :=
case
state = IDLE & next(state) = WAIT : i;
TRUE : last_to_enter[0];
esac;
next(last_to_enter[1]) :=
case
state = WAIT & next(l) = 1 & l != next(l) : i;
TRUE : last_to_enter[1];
esac;
next(last_to_enter[2]) :=
case
state = WAIT & next(l) = 2 & l != next(l) : i;
TRUE : last_to_enter[2];
esac;
next(last_to_enter[3]) :=
case
state = WAIT & next(l) = 3 & l != next(l) : i;
TRUE : last_to_enter[3];
esac;
FAIRNESS running;
MODULE main
VAR
level : array 0..4 of -1..4;
last_to_enter : array 0..3 of 0..4;
proc0 : process mutex(level, last_to_enter, 0);
proc1 : process mutex(level, last_to_enter, 1);
proc2 : process mutex(level, last_to_enter, 2);
proc3 : process mutex(level, last_to_enter, 3);
proc4 : process mutex(level, last_to_enter, 4);
ASSIGN
init(level[0]) := -1;
init(level[1]) := -1;
init(level[2]) := -1;
init(level[3]) := -1;
init(level[4]) := -1;
init(last_to_enter[0]) := 0;
init(last_to_enter[1]) := 0;
init(last_to_enter[2]) := 0;
init(last_to_enter[3]) := 0;
CTLSPEC -- отсутствие одновременного нахождения любых двух процессов в критической секции
AG (
( proc0.state = CRIT -> proc1.state != CRIT & proc2.state != CRIT & proc3.state != CRIT & proc4.state != CRIT ) &
( proc1.state = CRIT -> proc0.state != CRIT & proc2.state != CRIT & proc3.state != CRIT & proc4.state != CRIT ) &
( proc2.state = CRIT -> proc1.state != CRIT & proc0.state != CRIT & proc3.state != CRIT & proc4.state != CRIT ) &
( proc3.state = CRIT -> proc1.state != CRIT & proc2.state != CRIT & proc0.state != CRIT & proc4.state != CRIT ) &
( proc4.state = CRIT -> proc1.state != CRIT & proc2.state != CRIT & proc3.state != CRIT & proc0.state != CRIT )
)
CTLSPEC -- любой процесс, захотевший войти в крит. секцию, в конце концов в нее войдет
AG (
( proc0.state = WAIT -> EF ( proc0.state = CRIT ) ) &
( proc1.state = WAIT -> EF ( proc1.state = CRIT ) ) &
( proc2.state = WAIT -> EF ( proc2.state = CRIT ) ) &
( proc3.state = WAIT -> EF ( proc3.state = CRIT ) ) &
( proc4.state = WAIT -> EF ( proc4.state = CRIT ) )
)
LTLSPEC -- отсутствие дедлока у процессов
!F G ( proc0.state = WAIT & proc1.state = WAIT & proc2.state = WAIT & proc3.state = WAIT & proc4.state = WAIT )
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment