«Экземпляр не найден» при использовании seq - PullRequest
Новая
       23

«Экземпляр не найден» при использовании seq

0 голосов
/ 27 января 2020

Я озадачен тем, что Alloy сообщает No instance found для этой модели, используя seq: 

one sig Const {
  T: seq (seq Int)
}

fact const_facts {
  Const.T = {
    0 -> {0->1 + 1->9} +
    1 -> {0->3 + 1->15}
  }
}

run {} for 20 but 6 Int, 8 seq

В то время как следующая модель, где я просто заменил каждый seq на Int -> , имеет экземпляр, как и следовало ожидать: 

one sig Const {
  T: Int -> (Int -> Int)
}

fact const_facts {
  Const.T = {
    0 -> {0->1 + 1->9} +
    1 -> {0->3 + 1->15}
  }
}

run {} for 20 but 6 Int

Это меня особенно смущает, поскольку https://alloytools.org/quickguide/seq.html, похоже, подразумевает, что seq X и Int -> X - это одно и то же мудрый.

Есть мысли?

1 Ответ

0 голосов
/ 27 января 2020

Аргумент Const.T, который вы создаете, имеет арность 3, а seq должен быть арностью 2. 

┌──────────┬──────┐
│this/Const│T     │
├──────────┼─┬─┬──┤
│Const⁰    │0│0│1 │
│          │ ├─┼──┤
│          │ │1│9 │
│          ├─┼─┼──┤
│          │1│0│3 │
│          │ ├─┼──┤
│          │ │1│15│
└──────────┴─┴─┴──┘

Предикаты и функции для seq предполагают арность 2. Т.е. seq не похож на объект, это соглашение для функций и предикатов, которые принимают набор кортежей arity 2, где первый столбец является целым числом.

...