Странное поведение сигнатуры, ограничивающее сигнатуру 5 (git commit 30b41ae8125f69657) - PullRequest
Новая
       1

Странное поведение сигнатуры, ограничивающее сигнатуру 5 (git commit 30b41ae8125f69657)

0 голосов
/ 29 ноября 2018

Может кто-нибудь уточнить, что здесь происходит не так: 

enum Stage { Receive, Check, Drop, Save, Forward, Delivered }

sig StartStage in Receive {}
-- { StartStage = Receive } -- do not constrain StartStage???
-- if uncommented here, but commented in fact below, then StartStage may be empty
-- Why? Is it a bug?

sig FinalStage in Drop + Delivered {}

fact {
  StartStage = Receive
  FinalStage = Drop + Delivered
}

В этом коде StartStage может быть ограничен только отдельным разделом fact .Почему?

1 Ответ

0 голосов
/ 30 ноября 2018

Не уверен, почему кто-то отказывается, так как мой вопрос может быть полезен для новичков.

Ответ прост, в разделе ограничений после раздела полей подписи есть неявное количественное определение:

enum E {A, B, C}

sig S {} {S = A + B} на самом деле sig S {} {все это: S |S = A + B}, который удовлетворяется двумя значениями S: пустое множество {} и множество A + B.

Это упоминается в документации (неявное количественное определение), но в некоторых случаях поведение AlloyTools может выглядеть несколько неожиданнодля начинающих (я, например).

...