合金编程，例如网络配置 [英] Alloy programming for example network configuration

问题描述

假设有8个PC和1个开关，我想划分三个子网.如何使用Alloy语言程序?您能举个例子吗?

Suppose there are 8 pcs and 1 switch, I want to divide three subnets.how to use alloy language program?Can you give an example?

推荐答案

以下模型对小型网络进行了建模.

The following models a small network.

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分配给了哪个子网.然后转到评估程序并输入:

You'd probably like to see what PCs are assigned to what subnet. Then go to the evaluator and type:

ips.~range

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

免责声明::这很快就被黑客入侵，因此可能会出现建模错误.

Disclaimer: This was quickly hacked together so there might be modeling errors.

这篇关于合金编程，例如网络配置的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！