Можно ли использовать бессмысленные выражения в фактах подписи? - PullRequest
Новая
       6

Можно ли использовать бессмысленные выражения в фактах подписи?

0 голосов
/ 23 сентября 2019

Предположим, у нас есть следующая модель сплава: 

sig A {}

sig B  {
  R : A
  } 

fact {
  R.~R in iden
  }

run {}

При выполнении прогона сплав находит экземпляр.Я думал, что попытаюсь изменить факт модели на факт подписи , как показано ниже: 

sig A {}

sig B  {
  R : A
    } {
    R.~R in iden
    }

run {}

, но когда я это сделаю, сплав скажет мне: 

A type error has occurred:
~ can be used only with a binary relation.
Instead, its possible type(s) are:
{this/A}

Ответы [ 2 ]

2 голосов
/ 24 сентября 2019

В дополнение к уже данному ответу, да, это возможно.

Вы можете использовать оператор @. 

sig A {}

sig B  {
  R : A
    } {
    @R.~@R in iden
    }

run {}
1 голос
/ 23 сентября 2019

Внутри сигнатуры R рассматривается как тип A, а не B-> A.

Но этот факт принадлежит за пределами сигнатуры, поскольку касается глобальной структуры R, а не локальной части R,bR, для каждого b: B.

Если бы у вас было второе отношение в B, скажем S: A, вы могли бы иметь такие сигнатурные факты, как R! = S, которые переводятся в bR! = bS, для каждого b: B.

...