Alloy programming for example network configuration

Question

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?

Answer 1

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

If you run it:

┌───────────┬────────────┐
│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¹¹│
└─────────┴────┘

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.