Как отобразить последовательность пар в сплаве?

Question

Я хотел бы знать, как я могу определить пару и последовательность пары в сплаве? Например, в нотации Z мы можем иметь определение переменной, например c, как последовательность пар, то есть «c: seq (A \ cross B)». Есть ли какой-либо эквивалент этого определения в языке сплава?

Answer 1

Alloy довольно выразителен, и часто вы можете перевести прямо из Z в Alloy. В этом случае, например, вы можете объявить подпись, представляющую пары

sig Pair {first, second: X}

, а затем определить поле как последовательность пар

s: seq Pair

Но обычно есть лучший способДелать это. Например, может быть, лучше иметь две последовательности;возможно последовательности могут быть представлены как упорядочения;или, может быть, вам не нужны последовательности вообще, и наборы подойдут. Обычно это то, что люди находят при моделировании с использованием Alloy: упрощение анализа облегчает понимание и выражение. Удачи!