Почему для этого предиката не найдено ни одного экземпляра? (Сплав) - PullRequest
Новая
       9

Почему для этого предиката не найдено ни одного экземпляра? (Сплав)

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

Я пытаюсь смоделировать ошибку в механизме загрузки плагинов O365, в основном это похоже на пример адресной книги в книге, ошибка возникает, когда вы загружаете один плагин и выходите из модального плагина, а затем снова открываете его. Причина root заключается в том, что когда вы загружаете плагин в первый раз, веб-страница outlook загружает плагин и записывает экземпляр плагина в простой объект javascript с URL-адресом плагина в качестве ключа, а когда вы закрываете модальное окно, он очистить весь экземпляр, но ключи остаются в объекте, поэтому при втором его открытии загрузчик получает пустой объект.

Я записал механизм, но, что интересно, я не могу сгенерировать экземпляр для загрузки что-то в пустой DI (фактически, то же самое происходит, когда я добавляю предикат в пример адресной книги из книги, например addressBook1h.als). Может ли кто-нибудь помочь мне указать, где я поступил неправильно? Спасибо. 

sig DI {
  plugins: Name one -> lone Kls
} {
  all disj n, n': Name |
    plugins[n] != plugins[n']
}

sig Name, Kls {}

fun lookup [d: DI, n: Name] : set Kls {
    n.(d.plugins)
}

pred load[d, d': DI, p: Name, k: Kls] {
  (no lookup[d, p]) => {
    d'.plugins = d.plugins + p->k
  }
  else
  d'.plugins = d.plugins
}

pred exit[d, d': DI] {
  d'.plugins.Kls = d.plugins.Kls
  and
  all n: Name |
   some d.plugins[n] => d'.plugins[n] = none
}

-- no instances
run {
  all disj d,d':DI|
    let n = Name |
      let k = Kls {
        no d.plugins
        and
        load[d, d', n, k]
      }
} for 3 but exactly 2 DI, exactly 1 Name, exactly 1 Kls

1 Ответ

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

просто удалите «точно», и вы получите экземпляры: 

sig DI {


plugins: Name one -> lone Kls

} {



all disj n, n': Name |
    plugins[n] != plugins[n']
}

sig Name, Kls {}

fun lookup [d: DI, n: Name] : set Kls {
    n.(d.plugins)
}

pred load[d, d': DI, p: Name, k: Kls] {
  (no lookup[d, p]) => {
    d'.plugins = d.plugins + p->k
  }
  else
  d'.plugins = d.plugins
}

pred exit[d, d': DI] {
  d'.plugins.Kls = d.plugins.Kls
  and
  all n: Name |
   some d.plugins[n] => d'.plugins[n] = none
}

-- no instances
run {
  all disj d,d':DI|
    let n = Name |
      let k = Kls {
        no d.plugins
        and
        load[d, d', n, k]
      }
} for 3 but  2 DI ,  1 Name ,  1 Kls
...