Alloy следов и проекционные вопросы

Question

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

В следующем примере я пытаюсь проецировать Курс и посмотреть, как учащиеся учатся, но похоже, что они никогда не имеют никакого отношения.

Когда я использую обычный вид (без проецирования), я получаю несколько решений, которые хороши. Но я хочу знать, как (поэтапно) узнать, как они были созданы с помощью трассировки (трассировка назад).

open util/ordering[Course] 
sig Student {} 
sig Course { 
    roster : set Student 
} 

pred Enroll (c, c' : Course, sNew : Student) { 
    c'.roster = c.roster + sNew 
} 

pred init(c: Course) { 
    no c.roster 
} 

fact traces { 
    init[first] 
    all c: Course - last | let c' = next[c] | 
    some s: Student | Enroll[c, c', s] 
} 

pred show {} 
run show for 5 

Answer 1

Я не уверен, что вы пытаетесь выполнить. Я думаю, что понятие «Время» отсутствует в вашей модели. Обычно вам нравится иметь список для данного курса, который меняется в течение этого времени.

Похоже, вы обошли эту «хорошую практику», напрямую заказывая концепцию курса, поэтому, я думаю, вы хотите, чтобы на первом курсе не было студента, второй курс - для нового и т. Д. (Что не означает, t имеет смысл, но nvm).

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

Причина в том, что, когда вы пишете некоторые из них: Студент | Зарегистрируйтесь [c, c ', s], вы ожидаете, что s будет совершенно новым, а это означает только, что есть хотя бы один. Я предлагаю вам написать вместо этого: some s: Student | s не в c.roster и Enroll [c, c ', s]