抽象によるソフトウェア設計 付録A 練習問題 その18

付録A.4 のメタモデルに入ります。

• A.4.1 状態機械の定義
  • ライブロックの定義は「全ての状態からある状態に到達できる経路がある」かつ「そのある状態に到達しない無限の経路もある」という意味に読みとったのですがちょっと違うかもしれませんね。

sig State { next: set State }
sig StateMachine { states: some State, first: some State }

fact {
  #StateMachine = 1
  all s: State | s in StateMachine.states
}

pred Definite {
  all s: State | lone s.next
}
run Definite

pred NonDefinite {
}
run NonDefinite 

pred Unreachable {
  all m: StateMachine | {
    some m.states - m.first.^next - m.first
  }
}
run Unreachable

pred Reachable {
  all m: StateMachine | {
    m.states in m.first.^next + m.first
  }
}
run Reachable

pred StronglyConnected {
  all m: StateMachine | {
    all disj s1, s2: m.states | {
      s1 in s2.^next or s2 in s1.^next
    }
  }
}
run StronglyConnected

pred DeadLock {
  all m: StateMachine | {
    some s: m.states | {
      s in m.first.^next and no s.next
    }
  }
}
run DeadLock

pred LiveLock {
  all m: StateMachine | {
    all s: m.states | {
      some s': m.states - s| {
        s' in s.^next
        s in s.^next
      }
    }
  }
}
run LiveLock