合金新手 - 在運行命令的上下文中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的整數。