Предикат сплава не работает так, как это должно быть - PullRequest
Новая
       29

Предикат сплава не работает так, как это должно быть

0 голосов
/ 23 мая 2019

Определение системы: всякий раз, когда происходит определенное событие, я хочу изменить состояние объекта соответствующей операции на _1 или _0.

Но всякий раз, когда я выполняю свой предикат, он всегда дает мне неверную информацию о состоянии моего объекта. К сожалению, я получаю некоторый объект, связанный с _1, но я не предоставил это определение.

Я выполняю всю операцию, используя следующий факт: 

fact {
     all u:Environment-last {
         some r:Operation | {
              execute [u, u.next, r]
         }
     }
}

Вот что я пытаюсь сделать: для всего списка окружения и некоторых операций я выполняю операции, используя предикат 'execute'. А также отправьте следующее событие для добавления нового события из события результата операции и удаления текущего события из события (функциональность аналогична сохранению очереди событий. Затем извлечение одного из очереди и добавление нового к существующему очередь).

Ниже приводится определение моего предиката выполнения: 

pred execute [u:UserEnv, u':UserEnv, r:Operation] {
     all e: u.ev, ns, ns':u.obj | {
      e = r.event.name &&
      ns = r.objectA &&
      ns' = r.objectB  
            => {
          u'.ev = u.ev + r.result.name - r.event.name
          ns.state = r.event.state 
          ns'.state = r.result.state  
      }
     }
}

Здесь я пытаюсь сделать следующее: всякий раз, когда я получаю событие, я выполняю соответствующую операцию. Я получаю соответствующие два объекта из этой операции. Затем включите событие результата в качестве следующего события, такого как очередь, и удалите имя события, которое уже выполнено. Я изменяю состояние этих двух объектов в зависимости от события операции и состояния результата.

Может кто-нибудь указать мне, где я делаю неправильно?

...