Alloy 编程例如网络配置

Question

假设有8个pcs和1个switch，我想分成三个subnets.how来使用alloy语言程序？能举个例子吗？

Answer 1

Alloy 是一种建模语言，主要用于推理设计。所以忘记 "programming"。

您在 Alloy 中可以做的是定义 pc、交换机和子网如何相互关联的一般规则。然后您可以验证这些规则是否允许将这些 pc 划分为三个子网，以及该划分是否符合您的期望。如果没有，恭喜，您已经在规范中找到了 "bug"，解决它会提高您对当前正在建模的系统固有约束的理解。

Answer 2

以下是一个小型网络模型。

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

如果你运行它：

┌───────────┬────────────┐
│this/Router│subnets     │
├───────────┼────┬───────┤
│Router⁰    │IP² │Subnet¹│
│           ├────┼───────┤
│           │IP³ │Subnet⁰│
│           ├────┼───────┤
│           │IP¹¹│Subnet²│
└───────────┴────┴───────┘

┌───────────┬─────┐
│this/Subnet│range│
├───────────┼─────┤
│Subnet⁰    │IP³  │
│           ├─────┤
│           │IP⁴  │
├───────────┼─────┤
│Subnet¹    │IP¹  │
│           ├─────┤
│           │IP²  │
│           ├─────┤
│           │IP⁵  │
│           ├─────┤
│           │IP⁶  │
│           ├─────┤
│           │IP⁷  │
│           ├─────┤
│           │IP⁸  │
│           ├─────┤
│           │IP⁹  │
│           ├─────┤
│           │IP¹⁰ │
├───────────┼─────┤
│Subnet²    │IP⁰  │
│           ├─────┤
│           │IP¹¹ │
└───────────┴─────┘

┌─────────┬────┐
│this/Node│ips │
├─────────┼────┤
│PC⁰      │IP¹⁰│
├─────────┼────┤
│PC¹      │IP⁹ │
├─────────┼────┤
│PC²      │IP⁸ │
├─────────┼────┤
│PC³      │IP⁷ │
├─────────┼────┤
│PC⁴      │IP⁶ │
├─────────┼────┤
│PC⁵      │IP⁵ │
├─────────┼────┤
│PC⁶      │IP⁴ │
├─────────┼────┤
│PC⁷      │IP¹ │
├─────────┼────┤
│Router⁰  │IP² │
│         ├────┤
│         │IP³ │
│         ├────┤
│         │IP¹¹│
└─────────┴────┘

您可能想查看哪些 PC 分配给了哪些子网。然后转到评估器并键入：

ips.~range

┌───────┬───────┐
│PC⁰    │Subnet¹│
├───────┼───────┤
│PC¹    │Subnet¹│
├───────┼───────┤
│PC²    │Subnet¹│
├───────┼───────┤
│PC³    │Subnet¹│
├───────┼───────┤
│PC⁴    │Subnet¹│
├───────┼───────┤
│PC⁵    │Subnet¹│
├───────┼───────┤
│PC⁶    │Subnet⁰│
├───────┼───────┤
│PC⁷    │Subnet¹│
├───────┼───────┤
│Router⁰│Subnet⁰│
│       ├───────┤
│       │Subnet¹│
│       ├───────┤
│       │Subnet²│
└───────┴───────┘

免责声明：这很快就被拼凑在一起，因此可能存在建模错误。

Alloy 编程例如网络配置

Alloy programming for example network configuration

network-programming

alloy