peterson.rb

#!/usr/bin/env ruby

#
# アルゴリズム概要
#     1. 初期状態 (0,0,f,f,0) から遷移可能な状態を網羅すし、PC0=4かつPC1=4なる状態が存在しない事を確かめる。
#     2. 全ての状態の中からPC0=2の状態を全て取り出す。
#     3. 2で取り出したそれぞれの状態を初期状態として、その状態から遷移可能な全ての状態を網羅する。
#     4. 3で網羅された状態の中にPC0=4なる状態が存在する事を確かめる。
#
module Peterson
  class << self
    def run(initial_state)
      all_states = search(initial_state)

      all_states.each do |state|
        if state[0] == 2
          states = search(state)
          raise Exception.new("Can't reach state where pc0=4") unless states.map(&:first).include?(4)
        end
      end
    end

    def search(initial_state)
      @states = []
      rec_search(initial_state)
      @states
    end

    def rec_search(state)
      raise Exception.new("Invalid state") if state[0] == 4 && state[1] == 4

      return if @states.include?(state)

      @states << state

      zero = Peterson.next_state(state, 0)
      rec_search(zero)

      one  = Peterson.next_state(state, 1)
      rec_search(one)
    end

    #
    # 0: flags[me] = true;
    # 1: turn = other;
    # 2: if (flags[other] != true) goto 4;
    # 3: if (turn != other) goto 4; else goto 2;
    # 4: critical section;
    # 5: flags[me] = false;
    # 6: either goto 6 or goto 0;
    #
    # state: (pc0, pc1, flags[0], flags[1], turn)
    def next_state(current_state, turn)
      next_state = current_state.clone

      pc = current_state[0+turn]
      case pc
      when 0
        next_state[2+turn] = true;
        next_state[0+turn] += 1
      when 1
        next_state[4] = (1+turn) % 2
        next_state[0+turn] += 1
      when 2
        if next_state[3-turn] != true
          next_state[0+turn] = 4
        else
          next_state[0+turn] += 1
        end
      when 3
        if next_state[4] != (1+turn) % 2
          next_state[0+turn] = 4
        else
          next_state[0+turn] = 2
        end
      when 4
        next_state[0+turn] += 1
      when 5
        next_state[2+turn] = false
        next_state[0+turn] += 1
      when 6
        next_state[0+turn] = 0
      else
        raise Exception("Invalid PC")
      end

      next_state
    end
  end
end

Peterson.run([0, 0, false, false, 0])