【訂正】Alloy Analyzer で、あの格言をモデリングする その3〜石の上にも三年って、具体的に何年から何年まで？〜

前回のモデリング、を何度もいじくり回しているうちに、間違いが2点見つかったので、まず訂正します。
一つ目は、MinInterval。

当年と座り始めた年との間には、最低3目盛り、距離でいうと、4離れていないといけない

という理由で、

one sig MinInterval { val: one Int  } { val = 4}

というシグネチャと、それを使った制約を使っていたんですが、これは要らなかったですね。
どんな事例を提示するか（出来るか）は、Alloy に任せればそれでよかった。
もちろんそのためには、数値のスコープは、仕様に合わせて管理しないといけないわけですが。

二つ目は、算術演算の使用について。
4 Int というスコープ内で、例えば、6.minus[-5] っていう減算が出てきたとき、解である 11 が、
スコープ外になってしまうので、期待と違う動作になってしまうことがわかりました。
今回の仕様でいうと、減算しか使っていないので、もし登場する Int がどれも正の数であれば、
こういことが起こる心配はとりあえず排除できるんで、これは fact を直すことで対処することにします。
修正したモデリングの全文は、これです。

abstract sig Border { val: one Int }
one sig BorderThree extends Border {} { val = 3 } // 0〜7 をアサイン可能。
one sig BorderZero extends Border {} { val = 0 }

abstract sig Year { val: one Int }
one sig ThisYear extends Year {}
sig SinceYear extends Year { whose: one Craftman }

sig Craftman { sinceYear: one SinceYear } 

abstract sig Career { guys: set Craftman }
one sig Rookie, FullGrown extends Career {}

fact generic {
  // CraftmanのsinceYearとして作用していないSinceYearは、不要。
  sinceYear = ~whose
  // rookieGuysとfullGrownGuysは互いに素。
  disj[Rookie.guys, FullGrown.guys]
  // 開始年は過去である、等。
  all sYear:SinceYear, tYear:ThisYear | 
    tYear.val >= sYear.val && sYear.val >= BorderZero.val
}
fact bizLogic {
  all c:Craftman, r:Rookie, f:FullGrown, y:ThisYear, b:BorderThree |
    let rGuys = r.guys, fGuys = f.guys |
      y.val.minus[c.sinceYear.val]  > b.val implies 
        c in fGuys else
        c in rGuys
}
run {} for 4 Int, 4 Craftman, 6 Year

以上、過去エントリの訂正でした。