как этот сигнал добавляется в отношение в Alloy? - PullRequest
Новая
       10

как этот сигнал добавляется в отношение в Alloy?

2 голосов
/ 23 октября 2019

Я моделирую встроенную систему комментариев Google Docs в Alloy. В частности, я моделирую взаимодействия пользовательского интерфейса, которые может выполнять пользователь. На английском языке существуют следующие ограничения:

  • пользователи могут иметь любое количество комментариев
  • пользователи могут иметь любое количество комментариев, составляющих одновременно
  • комментарии могут бытьлибо сочинение, либо редактирование, но не оба
  • (в конце концов) пользователи могут расширять один комментарий за раз, чтобы просмотреть его - в противном случае текст обрезается.

до сих пор я только смоделировал добавлениеНовый комментарий - или я так думаю! Когда я запускаю модель ниже, я ожидаю увидеть, что Alloy не может найти никаких контрпримеров, но он находит тот, где комментарий находится одновременно в отношениях composed и composing.

Я думаюв моей ментальной модели может быть что-то непонятное, как работает Alloy в этом случае. Я не могу понять, как комментарий может быть добавлен к отношению composed здесь: я думаю, что init установит, что все черновики будут иметь пустые отношения, и что действия в Traces исключат возможность когда-либо быть комментариемдобавлено к composed. НО! Я явно ошибаюсь, поскольку Alloy находит пример, где composed не пусто. Кто-нибудь знает, что на самом деле здесь происходит? 

module inlineComments

open util/ordering [Time] as TimeOrdering

sig Time {}

sig Draft {
  composing: set Comment -> Time,
  composed: set Comment -> Time,
  -- expanded: lone Comment -> Time,
}

sig Comment {}

-- What can we do with these?

pred newComment (t, t': Time, c: Comment, d: Draft) {
  -- comment is not already known to us
  c not in d.composing.t
  c not in d.composed.t

  -- start composing the comment
  d.composing.t' = d.composing.t + c
}

pred init (t: Time) {
  all d: Draft, c: Comment | c not in d.composing.t
  all d: Draft, c: Comment | c not in d.composed.t
}

fact Traces {
  init[TimeOrdering/first]

  all t: Time - TimeOrdering/last |
    let t' = TimeOrdering/next[t] |
      some d: Draft, c: Comment |
        newComment [t, t', c, d]
}

-- Is the world how we expect it to be?

assert validState {
  -- comments cannot be composing and composed at the same time
  all t: Time, d: Draft | d.composing.t & d.composed.t = none
}

check validState for 3 but 1 Draft

1 Ответ

1 голос
/ 23 октября 2019

Это известно как «проблема с фреймами»: вы указали, что новые комментарии могут быть добавлены в composing, но больше ничего не происходит! Вы должны четко указать, что единственный способ изменить систему - это через newComment. Вот один из способов сделать это: 

fact Traces {
  init[TimeOrdering/first]

  all t: Time - TimeOrdering/last |
    let t' = TimeOrdering/next[t] |
      some d: Draft, c: Comment {
        newComment [t, t', c, d]
        d.composed.t = d.composed.t' -- d.composed doesn't change
      }
}

Обратите внимание, что это работает только потому, что вы явно ограничены максимум 1 черновиком. Если вы тестируете с двумя черновиками, вы также должны показать, что ни один из черновиков не изменяется. Если это всегда будет иметь место, когда есть только один черновик, вы можете написать one sig Draft для обеспечения этого.

...