ссылка на неправильный объект sig при выполнении состояния в Alloy - PullRequest
Новая
       53

ссылка на неправильный объект sig при выполнении состояния в Alloy

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

Я новичок в Alloy. Я пытаюсь формализовать систему с использованием Alloy. Здесь я хочу выполнить определенные операции на основе событий. Для этого у меня есть список событий, которые я хочу отслеживать, используя enum Event. И я прохожу через весь штат, используя функцию заказа Alloy. В каждом состоянии я беру объект смеси и запускаю операцию.

Проблема, с которой я сталкиваюсь в настоящее время: - В моей системе у меня есть два объекта sig - ClassA и ClassB. После выполнения кода сплава я создаю блок-схему. К сожалению, я заметил, что мой ClassB ссылается на ClassA объекта Mixture. Я прилагаю диаграмму

enter image description here

Я также прилагаю свой полный код здесь. Может кто-нибудь помочь мне отладить проблему, пожалуйста? Я пытался навязать разные предикаты и логику, но ни один из них не сработал. 

open util/ordering[State]


abstract sig Base{
 name: String,
 value : Int
}{
value >= 0
}

sig ClassA extends Base{

}{

name = "Class A"
}

sig ClassB extends Base{


}{
name = "Class B"
}

enum Event {EVENT1, EVENT2}


sig State{

mixture: Mixture
}

sig Mixture{
classA: Base,
classB: Base
} {
    classA != classB
}


fact {
    all s: State, s': s.next{
        s.mixture ! in  s'.*next.mixture
        operation [s.mixture]       

    }
}


pred operation [mixture: Mixture]{
    all ev: Event| ev = EVENT1 => {
        mixture.classA.name = "Class A" => {
                mixture.classA.value = 1    
        }
    }

}

run random {} for 3

1 Ответ

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

У вас есть 

sig Mixture{
classA: Base,
classB: Base
}

На вашей диаграмме отношения имеют имена classA и classB. Поскольку каждый из них может указывать на любой произвольный Base, ничто не мешает classA указывать на экземпляр ClassB. Вы, вероятно, хотите что-то вроде 

sig Mixture {
    , classA: ClassA
    , classB: ClassB
}
...