event-b - 如何在事件 b 中使用公理填充关系

Question

所以，我有一个罗丹 event-b 项目，想定义一个已知的静态关系。例如，假设我有一个集合 {a,b,c} 并想指定关系常数，它等于 {(a,1),(a,2),(b,3)} 在上下文公理。（可以是多行的，但如果可行的话最好是单行的）

我该怎么办？

CONTEXT

example 

SETS

list 

CONSTANTS  
a       
b  
c 

relation 

AXIOMS

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

axm2   :    relation ∈ list↔1‥5 

axm3   : ???


END

Answer 1

axm3:  relation = {a↦1, a↦2, b↦3}