合金新手 - 在运行命令的上下文中int是什么意思？

Question

下面是该示例的合金代码我们在我的课去在：

abstract sig Airport { 
    flight: set Airport 
} 
one sig CMX, DTW, MSP, BRD, CDG extends Airport {} 

fact { 
-- flight = CMX->DTW + DTW->MSP + MSP->CMX + DTW->CDG + CDG->DTW + MSP->BRD + BRD->MSP 
} 

fun flight2: Airport->Airport {flight.flight} 
fun flight3: Airport->Airport {flight.flight2} 
fun flight4: Airport->Airport {flight.flight3} 
fun flight5: Airport->Airport {flight.flight4} 

pred show { 
    flight5 in flight2 
    flight2 not in flight5 
-- #flight = 10 
} 

run show for 5 Airport, 6 Int 

我想知道最后一行表示。具体来说，“6 Int”是什么意思？

Answer 1

最后一行定义了在运行此命令时找到的任何令人满意的实例中符合给定概念的原子数的上限（称为范围）。

在您的示例中，您将查找包含至多5个机场原子的实例。 Int是合金中的内置型。由于您没有声明任何Int类型字段，因此第6部分的Int不会对实例查找过程产生很大影响。

范围中与Int关联的数字不对应于要找到的实例中的Int atom的最大数量，而是与用于表示整数的位宽度相对应。 位宽为6时，您的实例将包含从-32到31的整数。