Как заполнить отношение аксиомой в событии b - PullRequest
2 голосов
/ 29 мая 2020

Итак, у меня есть проект Rodin event-b, и я хотел бы определить известное отношение c stati. В качестве примера, допустим, у меня есть набор {a, b, c}, и я хотел бы указать константу отношения, которая равна {(a, 1), (a, 2), (b, 3)} в аксиома контекста. (Может быть многострочным, но желательно одинарным, если это возможно)

Как мне go об этом?

CONTEXT

example 

SETS

list 

CONSTANTS  
a       
b  
c 

relation 

AXIOMS

axm1   :    partition(list, {a}, {b}, {c}) 

axm2   :    relation ∈ list↔1‥5 

axm3   : ???


END

1 Ответ

1 голос
/ 29 мая 2020
axm3:  relation = {a↦1, a↦2, b↦3}
Добро пожаловать на сайт PullRequest, где вы можете задавать вопросы и получать ответы от других членов сообщества.
...