合金编程例如网络配置答案

【问题标题】：Alloy programming for example network configuration合金编程例如网络配置
【发布时间】：2018-12-10 09:45:55
【问题描述】：

假设有8个pc和1个switch，我想划分三个子网，alloy语言程序怎么用？可以举个例子吗？

【问题讨论】：

欢迎来到 Stack Overflow。请阅读the help pages、the SO tour、阅读how to ask good questions，以及this question checklist。最后学习如何创建minimal reproducible example。

【解决方案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²│
└───────┴───────┘

免责声明：这很快就被破解了，因此可能存在建模错误。

【讨论】：

谢谢。当我使用合金分析仪 4.1.0 运行时出现错误。错误是 LET 声明只允许在顶层段落中以及如何解决它。
我是合金语言的初学者。你能记下你的程序吗？再次感谢
你应该合金 5 ... github.com/AlloyTools/org.alloytools.alloy。我认为记录程序没有用，因为它主要是学习语言。 Alloy 可读性极强（虽然很难写）。评论它将在很大程度上取代已经存在的内容。阅读 Daniel Jackson 为运营商编写的书。
如何在windows平台上运行alloy5？对于alloy4，我只需要在window命令下执行java -jar alloy4.jar。但是对于alloy5不能运行。对于注释程序，我想了解你的建模想法。谢谢你的建议。
您可以在 Alloy 4.2 中运行此模型。在此处下载 jar：alloytools.org/download.html 并以与 Alloy4.1 相同的方式启动它

【解决方案2】：

Alloy 是一种建模语言，主要用于推理设计。所以忘掉“编程”吧。

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

【讨论】：

我不确定我是否完全同意。您可以按照您的说法使用 Alloy，但是您可以创建一个可以驱动网络配置的实例？我们缺少一些功能来简化此操作，但我认为这是对 Alloy 的有趣使用。
没错，这绝对是可能的。让我做出反应的是“Alloy 编程”，因为将 Alloy 视为一种编程语言已经显示出混乱的迹象。
感谢您的 cmets。