合金式の型チェックに失敗しました

Question

私は合金（仕様言語）の初心者で、here（コードは5ページ）のケーススタディに基づいてさらに作業を行う必要があります。該当するコード：「この式は型検査に失敗した」、そして、それはlet t' = T0/t.nextでt'浮き彫りに：

open util/ordering[Time] as T0 

pred Eavesdropping() { 
    some pro:Process | some m:Protected_Msg | 
    some t: (Time - T0/last) - T0/prev[T0/last] | let t' = T0/t.next | 
    let t'' = T0/t'.next | !HasReadAccess[pro,m] && (m->t in pro.knows) 
    && (m.contents->t not in pro.knows) && (m.contents->t'' in 
    pro.knows) && IsUnique(m.contents) } 

いくつかの構文を修正した後は、私は、このエラーメッセージが表示されます。 t'をタイプチェックするにはどうすればよいですか？

Answer 1

ここで誤差は次のエイリアスT0によって参照モジュール内の関数であるので、LET結合のRHS上の発現は、t.T0/nextとしないT0/t.nextなければならないということです。しかし実際には合金は参照されているモジュールを決定できるので、とにかくT0は必要ありません。だから、T0への参照をすべて削除してください。それはうまくコンパイルする必要があります。

別のコメント：あなたはすべてのそれらの組み合わせの記号を削除して、暗黙の組み合わせを使用し、

{ A B C } 

の代わりA && B && Cを書くことができます。