川渡り問題
問題
3匹ずつの狼と小鳥を、すべて向こう岸に渡せ。
ただし、以下の条件がある。
ただし、以下の条件がある。
- いかだに乗れるのは2匹まで。
- 1匹も乗っていないと動かない。
- どちらの岸でも狼が小鳥の数より多くなると、小鳥が食べられて失敗する。
モデル
--------------------------- MODULE RiverCrossing ---------------------------
EXTENDS Integers, FiniteSets
(*--algorithm RiverCrossing {
\* 初期状態
variables (* LSideとRSideはそれぞれ左岸と右岸の状態を表すレコード *)
LSide = [wolf |-> 3, bird |->3], RSide = [wolf |-> 0, bird |->0],
(* sideは現在のボートの位置 *)
boat = [side |-> "left", wolf |-> 0, bird |->0],
(* OnBoatはボートに乗ることができる狼と小鳥の組み合わせを表す *)
OnBoat = {<<1,0>>,<<0,1>>,<<1,1>>,<<2,0>>, <<0,2>>};
define
{
(* どちらの岸でも狼の数が小鳥の数より多くなると真となる *)
GetsEaten == /\ LSide.wolf > LSide.bird /\ LSide.bird > 0
/\ RSide.wolf > RSide.bird /\ RSide.bird > 0
(* ボートが安全に移動できるかどうかを判断する *)
safeBoats(from, to, t) == /\ from.wolf >= t[1]
/\ from.bird >= t[2]
/\ (from.wolf - t[1]) <= (from.bird - t[2]) \/ (from.bird - t[2]) = 0
/\ (to.wolf + t[1]) <= (to.bird + t[2]) \/ (to.bird + t[2]) = 0
(* Remainは、左岸にまだ動物が残っているかどうか *)
Remain == (LSide.wolf + LSide.bird) /= 0
};
(* 左岸から右岸へボートを移動 *)
process ( LeftToRight = 0 )
{ l: while ( Remain )
{ await (boat.side = "left");
(* ボートから降りる *)
l_GetOff:
LSide.wolf := LSide.wolf + boat.wolf || LSide.bird := LSide.bird + boat.bird;
boat.wolf := 0 || boat.bird := 0;
(* ボートに乗ることができる安全な組み合わせを選び、
その組み合わせをボートに乗せて反対側の岸へ移動する *)
l_GetOn:
with(t \in {tuple \in OnBoat : safeBoats(LSide, RSide, tuple)} )
{
LSide.wolf := LSide.wolf - t[1] || LSide.bird := LSide.bird - t[2];
boat.wolf := t[1] || boat.bird := t[2] || boat.side := "right";
}
}
}
(* 右岸から左岸へボートを移動 *)
process ( RightToLeft = 1 )
{ r: while (Remain)
{ await (boat.side = "right");
r_GetOff:
RSide.wolf := RSide.wolf + boat.wolf || RSide.bird := RSide.bird + boat.bird;
boat.wolf := 0 || boat.bird := 0;
r_GetOn:
with(t \in {tuple \in OnBoat : safeBoats(RSide, LSide, tuple)} )
{
RSide.wolf := RSide.wolf - t[1] || RSide.bird := RSide.bird - t[2];
boat.wolf := t[1] || boat.bird := t[2] || boat.side := "left";
};
}
}
}*)
\* BEGIN TRANSLATION
VARIABLES LSide, RSide, boat, OnBoat, pc
(* define statement *)
GetsEaten == /\ LSide.wolf > LSide.bird /\ LSide.bird > 0
/\ RSide.wolf > RSide.bird /\ RSide.bird > 0
safeBoats(from, to, t) == /\ from.wolf >= t[1]
/\ from.bird >= t[2]
/\ (from.wolf - t[1]) <= (from.bird - t[2]) \/ (from.bird - t[2]) = 0
/\ (to.wolf + t[1]) <= (to.bird + t[2]) \/ (to.bird + t[2]) = 0
Remain == (LSide.wolf + LSide.bird) /= 0
vars == << LSide, RSide, boat, OnBoat, pc >>
ProcSet == {0} \cup {1}
Init == (* Global variables *)
/\ LSide = [wolf |-> 3, bird |->3]
/\ RSide = [wolf |-> 0, bird |->0]
/\ boat = [side |-> "left", wolf |-> 0, bird |->0]
/\ OnBoat = {<<1,0>>,<<0,1>>,<<1,1>>,<<2,0>>, <<0,2>>}
/\ pc = [self \in ProcSet |-> CASE self = 0 -> "l"
[] self = 1 -> "r"]
l == /\ pc[0] = "l"
/\ IF Remain
THEN /\ (boat.side = "left")
/\ pc' = [pc EXCEPT ![0] = "l_GetOff"]
ELSE /\ pc' = [pc EXCEPT ![0] = "Done"]
/\ UNCHANGED << LSide, RSide, boat, OnBoat >>
l_GetOff == /\ pc[0] = "l_GetOff"
/\ LSide' = [LSide EXCEPT !.wolf = LSide.wolf + boat.wolf,
!.bird = LSide.bird + boat.bird]
/\ boat' = [boat EXCEPT !.wolf = 0,
!.bird = 0]
/\ pc' = [pc EXCEPT ![0] = "l_GetOn"]
/\ UNCHANGED << RSide, OnBoat >>
l_GetOn == /\ pc[0] = "l_GetOn"
/\ \E t \in {tuple \in OnBoat : safeBoats(LSide, RSide, tuple)}:
/\ LSide' = [LSide EXCEPT !.wolf = LSide.wolf - t[1],
!.bird = LSide.bird - t[2]]
/\ boat' = [boat EXCEPT !.wolf = t[1],
!.bird = t[2],
!.side = "right"]
/\ pc' = [pc EXCEPT ![0] = "l"]
/\ UNCHANGED << RSide, OnBoat >>
LeftToRight == l \/ l_GetOff \/ l_GetOn
r == /\ pc[1] = "r"
/\ IF Remain
THEN /\ (boat.side = "right")
/\ pc' = [pc EXCEPT ![1] = "r_GetOff"]
ELSE /\ pc' = [pc EXCEPT ![1] = "Done"]
/\ UNCHANGED << LSide, RSide, boat, OnBoat >>
r_GetOff == /\ pc[1] = "r_GetOff"
/\ RSide' = [RSide EXCEPT !.wolf = RSide.wolf + boat.wolf,
!.bird = RSide.bird + boat.bird]
/\ boat' = [boat EXCEPT !.wolf = 0,
!.bird = 0]
/\ pc' = [pc EXCEPT ![1] = "r_GetOn"]
/\ UNCHANGED << LSide, OnBoat >>
r_GetOn == /\ pc[1] = "r_GetOn"
/\ \E t \in {tuple \in OnBoat : safeBoats(RSide, LSide, tuple)}:
/\ RSide' = [RSide EXCEPT !.wolf = RSide.wolf - t[1],
!.bird = RSide.bird - t[2]]
/\ boat' = [boat EXCEPT !.wolf = t[1],
!.bird = t[2],
!.side = "left"]
/\ pc' = [pc EXCEPT ![1] = "r"]
/\ UNCHANGED << LSide, OnBoat >>
RightToLeft == r \/ r_GetOff \/ r_GetOn
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == LeftToRight \/ RightToLeft
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================
不変条件にRemainと~GetsEatenを指定し、モデルチェックを行うと~GetsEatenに違反せずにRemainが違反となる。
[Amazon商品]
