Как получить следующий элемент в последовательности (последовательности)?

Самолет летит последовательность ног. За каждым этапом должен следовать соответствующий следующий этап. NextLegTable содержит соответствующие (Leg -> Leg) пары.

Таким образом, каждая пара ног в полете должна находиться в NextLegTable. Я реализовал это ограничение в приведенном ниже Fact.

Вот описание моей реализации: Каждая пара ножек (leg и leg'), такая что indexOf(leg) + 1 = indexOf(leg'), должна быть в NextLegTable. По-видимому, этот подход неверен, так как я не получаю «экземпляров».

Каков правильный подход? Учитывая отрезок, как мне найти его следующий отрезок в последовательности?

sig Flight {
    legs: seq Leg
}

sig Leg {}

one sig NextLegTable {
    nextLeg: Leg -> Leg
}

fact Flight_legs_In_NexLegTable {
    all f: Flight |
        all leg, leg': Leg { 
            leg in f.legs.elems
            leg' in f.legs.elems 
            plus[f.legs.idxOf[leg], 1] =  f.legs.idxOf[leg']
            (leg -> leg') in NextLegTable.nextLeg
        }
}

pred Show (f: Flight) {#f.legs > 1} 
run Show

alloy
person Roger Costello    schedule 09.04.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вот две строки, на которые стоит обратить внимание:

    plus[f.legs.idxOf[leg], 1] =  f.legs.idxOf[leg']
    (leg -> leg') in NextLegTable.nextLeg

Это решение в настоящее время пытается найти экземпляр, в котором все Legs из Flight, которые следуют за другим Leg, также отображаются в сигнале NextLegTable. Однако вы не указали ему, что нужно поместить эти сопоставления в таблицу. Вам нужно сказать, что когда Leg следует за другим Leg, поместите Leg -> Leg' в NextLegTable:

(plus[f.legs.idxOf[leg], 1] =  f.legs.idxOf[leg']) =>
(leg -> leg') in NextLegTable.nextLeg

Это говорит программе помещать сопоставления в таблицу всякий раз, когда выполняется первое условие.

person LEJ    schedule 10.04.2017
comment
Фантастика! Спасибо, ЛЭЙ. - person Roger Costello; 10.04.2017