ソフトウェア工学コミュの誰か教えてください（モデル検査、演習問題）

状態遷移図と直積の関係を知りたいですね。
プロセスAの状態、プロセスBの状態を対称に考えると20個と言う気はしますが。

ちゃりさん、SopranoSax_YSS-875Sさん、ありがとうございます。関係箇所を、抜粋します。変数名は原文では小文字でボールドなのですが、ここでは大文字で表記します(RA, RB, TURN)。
The two users now decide to share 3 variables:
a variable RA (r for "request") which the user A sets to true when he wishes to print. Initially rA is false;
similarly, RB plays the corresponding role for user B;
and again the TURN variable, to settle conflicts.
The automaton modeling the behavior of user A is shown on figure 1.19 (the automaton modeling B is symmetrical, simply exchanging the roles of A and B). As in the elevator example, we associate with each state a unique elementary proposition corresponding to its name. The property "being in state 4" corresponds to the printing of a document by the corresponding user.
【ここに、図１．１９が来ます。このトピックの最初に載せた図です。】
The automaton modeling the algorithm is thus built from these two automata and from the three shared variables RA, RB and TURN. A state is then a tuple consisting of, in that order, the state of the automaton for A, the state of the automaton B, the value of RA, the value of RB and that of TURN. This automaton thus has 4x4x2x2x2=128 states. In fact, the number of reachable states is only 21. In particular, we can show (or ask a model checker to show) that no state of the form (4,4,-,-,-) is reachable, guarateeing in this way that the two users cannot be printing simultaneously.
オートマトンAの状態が{1,2,3,4}のどれかで、４通り。オートマトンBの状態も同じく、４通り。RAが{true, false}のどちらかで、２通り。RBも同じく、２通り。TURNは{A,B}のどちらかで２通り。なので、直積は4x4x2x2x2=128となります。

私が自分で数え上げた状態（２０個見つかりました）は、次のとおりです。trueをT、falseをFと略記します。
(オートマトンAの状態,オートマトンBの状態,RA,RB,TURN)∈{(1,1,F,F,A), (2,1,T,F,A), (3,1,T,F,B), (4,1,T,F,B), (4,2,T,T,B), (1,1,F,F,B), (1,2,F,T,B), (1,3,F,T,A), (1,4,F,T,A), (2,4,T,T,A), (1,2,F,T,A), (2,1,T,F,B), (2,2,T,T,A), (2,2,T,T,B), (3,2,T,T,B), (2,3,T,T,A), (3,3,T,T,A), (3,3,T,T,B), (4,3,T,T,A), (3,4,T,T,B)}

近しい分野を研究していて本があったので確かめてみたのですが２０で合っていると思います。
一応プログラムで全探索をして調べたので間違いないと思います。

(ノビ９１@5 さん)
> 私が自分で数え上げた状態（２０個見つかりました）

面白そうだったので、考えてみました。

==

この状態の自由度は、確かに、五つのパラメータ

SA : オートマントン A の状態 ( 1 〜 4 ) : 4 通り
SB : オートマントン B の状態 ( 1 〜 4 ) : 4 通り
RA : 共有変数 ( T/F ) だが、A しか変更しない (参照するのは B) : 2 通り
RB : 共有変数 ( T/F ) だが、B しか変更しない (参照するのは A) : 2 通り
T : 真の共有変数 ( A/B ) で、A/B 共に変更する : 2 通り

の直積 4x4x2x2x2=128 のように見えますが、まず、RA, RB は、SA, SB の関数
( RA := (SA==1), RB := (SB==1) ) なので、SA, SB が決れば、自動的に RA,
RB が確定します。

したがって、状態の区別をする場合は、RA/RB は不要で、取りあえず 1/4 の 4x4x2=32
通り考えることになります。

また、後で述べるように、共に 4 に入ることはないので、(4,4,-) も取り除く
ことができます ( ので、残りは 30 ) し、また、逆に、T の値に拘らなければ、
その 4,4 以外の SA,SB の組み合わせは必ずあります。

つまり、特定の SA,SB の組み合わせで、T が A, B 一方しかとれない場合があ
ると、その分だけ状態数が減って行くことになります。

==

まず、状態遷移の規則をまとめて置きます。

[1] SA, SB は、順番 ( 1 -> 2 -> 3 -> 4 -> 1 ) に変更される
[2] 自由に変更できないのは 3 -> 4 の時だけで、他の場合は、常に変更可能
[2-a] SA が 3 -> 4 と遷移できるのは、次の何れかの場合 (SB も同様)
[2-a-1] SB が 1 の時
[2-a-2] T が A の時
[3] T が変更されるのは、2 -> 3 の時だけ ( しかも移動/変更したもの
と反対の値になる ) で、他の場合は変更されない

さて、この状態で順番に考えて行ましょう。

Th1. (1,1,A) と (1,1,B) は、共に到達可能

[証明] 初期状態 (1,1,T) の T が A/B のどちらであれ、A が SA=1 の状態を
維持すれば SB は3->4 の遷移も可能であり、一周まわって、SB=1 に戻った場
合は、T=A となっている。同様に T=B ともできる。

Th2. SA : 1 〜 2, SB : 1 〜 2, T : A 〜 B の任意の組み合わせが到達でき
る。

[証明] Th1. より (1,1,A/B) に到達可能、ここから 1 -> 2 の遷移がおきても、
T は変化しない。従って、SA, SB が 1 〜 2 であれば、(1,1,A/B) の状態から
T を変化させずに到達できる。

Th3. (3,3,A/B) はどちらも到達可能

[証明] (2,2,A/B) の状態から先に SA が 3 に遷移した後に、SB が 3 に遷移
すれば、(3,3,A) が、逆順に遷移すれば、(3,3,B) となる。

# ここまでは、到達できる例でしたが、今度は到達できない例です。

Th4. (4,3,B)、(3,4,A) は到達できない [基本命題]

[証明] (4,3,-) に到達するには、(3,3,-) から変化するか、(4,2,-) から到達
するかの何方かである。処が、(3,3,T) から、(4,3,-) に遷移するには、T が、
A の時に限るし、また、(4,2,-) から (4,3,-) に遷移すると、自動的に T は
A になる。したがって、(4,3,A) は到達可能だが、(4,3,B) は到達不可能であ
る。(3,4,A) についても同様である。

Th5. (4,4,-) には到達できない [main 定理]

[証明] (4,4,-) に到達するには、(4,3,-) か (3,4,-) から遷移する必要がある。
ところが、Th4. より (4,3,B) には到達できないので (4,3,A) を経由することに
なるが、ここからは (4,4,-) に遷移することはできない。同様に、(3,4,-)からも
遷移できないので、(4,4,-) に到達することはない。

Th6. (1,3,B), (3,1,A) には到達できない

[証明] (1,3,-) に到達するには、(4,3,-) か、(1,2,-) から到達するしかない
処が、(4,3,-) は、Th4 より (4,3,A) しかなく、これから遷移しても T が変
化しないので、(1,3,A) となる。一方、(1,2,T) から遷移すると、T に無関係
に (1,3,A) となり、いずれにせよ、(1,3,B) に到達することはない。

Th7. (2,3,B), (3,2,A) には到達できない

[証明] Th6 と同様である。

Th8. (2,3,B), (3,2,A) には到達できない

[証明] Th6 と同様である。

Th9. (1,4,B),(2,4,B),(4,1,A),(4,2,A) には到達できない

[証明] Th6 と同様である。

Th10. 到達可能な状態は次の 20 状態だけである。

(1,1,A) (1,2,A) (1,3,A) (1,4,A)
(1,1,B) (1,2,B)
(2,1,A) (2,2,A) (2,3,A) (2,4,A)
(2,1,B) (2,2,B)
(3,1,B) (3,2,B) (3,3,A) (3,4,B)
(3,3,B)
(4,1,B) (4,2,B) (4,3,A)

[証明] Th1 〜 Th9

Col.ノビ９１ の説明は正しい。 :-)

[証明] Th10

皆さま、どうもありがとうございました。２０個、ということで、安心いたしました。
このコミュニティは、すばらしいです。今後とも、ご指導、よろしくお願いいたします。

私も勉強になりました。MUTEXとかセマフォとか、20年前は自分でアセンブラで組んでたのに、すっかりOSや言語にお任せになってます。
やはりこういう基本のアルゴリズムは思い出しておく価値あります。

ノビ９１さん、またネタ出して下さいね。