Не удалось проверить выражение сплава - PullRequest
Новая
       43

Не удалось проверить выражение сплава

1 голос
/ 16 ноября 2011

Я новичок в Alloy (язык спецификаций) и мне нужно проделать дополнительную работу, основываясь на тематическом исследовании, которое можно найти здесь (код на странице 5). Соответствующий код: 

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' в let t' = T0/t.next. Как мне проверить тип t'?

1 Ответ

4 голосов
/ 16 ноября 2011

Ошибка здесь заключается в том, что next - это функция в модуле, на которую ссылается псевдоним T0, поэтому выражение для RHS привязки let должно быть t.T0/next, а не T0/t.next. Но на самом деле вам не нужен T0, так как Alloy может определить, к какому модулю обращаются. Так что просто удалите все ссылки на T0, и он должен хорошо скомпилироваться.

Еще один комментарий: вы можете удалить все эти символы соединения и использовать неявное соединение, написав 

{ A B C }

вместо A && B && C.

...