sig IP {}
some sig Subnet {
range : some IP
}
abstract sig Node {
ips : some IP
}
sig Router extends Node {
subnets : IP -> lone Subnet
} {
ips = subnets.Subnet
all subnet : Subnet {
lone subnets.subnet
subnets.subnet in subnet.range
}
}
sig PC extends Node {} {
one ips
}
let routes = { disj s1, s2 : Subnet | some r : Router | s1+s2 in r.subnets[IP] }
let subnet[ip] = range.ip
let route[a,b] = subnet[a]->subnet[b] in ^ routes
fact NoOverlappingRanges { all ip : IP | one range.ip }
fact DHCP { all disj a, b : Node | no (a.ips & b.ips) }
fact Reachable { all disj a, b : IP | route[a,b] }
run {
# PC = 8
# Subnet = 3
# Router = 1
} for 12
2 回答
以下是小型网络的型号 .
如果你运行它：
您可能希望看到哪些PC分配给哪个子网 . 然后转到评估者并输入：
Disclaimer: 这很快被黑客攻击，因此可能存在建模错误 .
Alloy是一种建模语言，主要用于推理设计 . 所以忘了“编程” .
您在Alloy中可以做的是定义pc，开关和子网如何相互关联的一般规则 . 然后，您可以验证这些规则是否允许将这些pc分成三个子网，以及该分区是否与您的预期相符 . 如果没有，恭喜，您在规范中发现了一个“错误”，解决它将提高您对当前建模系统固有约束的理解 .