首页 文章

合金编程,例如网络配置

提问于
浏览 805
0

假设有8个pc和1个交换机,我想划分三个子网 . 如何使用合金语言程序?你能举个例子吗?

2 回答

  • 1

    以下是小型网络的型号 .

    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²│
    └───────┴───────┘
    

    Disclaimer: 这很快被黑客攻击,因此可能存在建模错误 .

  • 0

    Alloy是一种建模语言,主要用于推理设计 . 所以忘了“编程” .

    您在Alloy中可以做的是定义pc,开关和子网如何相互关联的一般规则 . 然后,您可以验证这些规则是否允许将这些pc分成三个子网,以及该分区是否与您的预期相符 . 如果没有,恭喜,您在规范中发现了一个“错误”,解决它将提高您对当前建模系统固有约束的理解 .

相关问题