基于SAT求解器的自动门控配置

原文链接

讲解视频

目标

这个示例演示了一个门调度配置器，它使用多元线性不等式系统解决自动配置问题，直接从变量生成门控列表。

INET version: 4.4

Source files location: inet/showcases/tsn/gatescheduling/sat

模型

基于SAT求解器的自动门控配置器需要启用INET的 Z3 Gate Scheduling Configurator 特性，并安装libz3-dev或Z3-devel包。

仿真网络结构如下：

配置如下：

# 创建一个TSN双哑铃网络
network = inet.networks.tsn.TsnDumbbellNetwork
description = "Z3 SAT based gate scheduling"
sim-time-limit = 0.2s

# 定义交换机类型
*.switch1.typename = "TsnSwitch1"
*.switch2.typename = "TsnSwitch2"

# 客户端应用程序配置
*.client*.numApps = 2
*.client*.app[*].typename = "UdpSourceApp"
*.client*.app[0].display-name = "best effort"
*.client*.app[1].display-name = "video"
*.client*.app[0].io.destAddress = "server1"
*.client*.app[1].io.destAddress = "server2"
*.client1.app[0].io.destPort = 1000
*.client1.app[1].io.destPort = 1002
*.client2.app[0].io.destPort = 1001
*.client2.app[1].io.destPort = 1003
*.client*.app[*].source.packetNameFormat = "%M-%m-%c"
*.client*.app[0].source.packetLength = 1000B
*.client*.app[1].source.packetLength = 500B
*.client*.app[0].source.productionInterval = 500us # ~16Mbps
*.client*.app[1].source.productionInterval = 250us # ~16Mbps

# 服务器应用程序配置
*.server*.numApps = 4
*.server*.app[*].typename = "UdpSinkApp"
*.server*.app[0..1].display-name = "best effort"
*.server*.app[2..3].display-name = "video"
*.server*.app[0].io.localPort = 1000
*.server*.app[1].io.localPort = 1001
*.server*.app[2].io.localPort = 1002
*.server*.app[3].io.localPort = 1003

# 启用客户端的出站流
*.client*.hasOutgoingStreams = true

# 客户端流标识
*.client*.bridging.streamIdentifier.identifier.mapping = [{stream: "best effort", packetFilter: expr(udp.destPort == 1000)},
                                                              {stream: "video", packetFilter: expr(udp.destPort == 1002)},
                                                              {stream: "best effort", packetFilter: expr(udp.destPort == 1001)},
                                                              {stream: "video", packetFilter: expr(udp.destPort == 1003)}]

# 客户端流编码
*.client*.bridging.streamCoder.encoder.mapping = [{stream: "best effort", pcp: 0},
                                                  {stream: "video", pcp: 4}]

# 启用交换机的入站和出站流
*.switch*.hasIncomingStreams = true
*.switch*.hasOutgoingStreams = true

*.switch*.bridging.streamCoder.decoder.mapping = [{pcp: 0, stream: "best effort"},
                                                  {pcp: 4, stream: "video"}]

*.switch*.bridging.streamCoder.encoder.mapping = [{stream: "best effort", pcp: 0},
                                                  {stream: "video", pcp: 4}]

# 启用服务器的入站流
*.server*.hasIncomingStreams = true

# 启用出口流量整形
*.switch*.hasEgressTrafficShaping = true

# 使用两个队列进行时间感知流量整形
*.switch*.eth[*].macLayer.queue.numTrafficClasses = 2
*.switch*.eth[*].macLayer.queue.queue[0].display-name = "best effort"
*.switch*.eth[*].macLayer.queue.queue[1].display-name = "video"

# 自动门调度配置
*.gateScheduleConfigurator.typename = "Z3GateScheduleConfigurator"
*.gateScheduleConfigurator.gateCycleDuration = 1ms
# 58B = 8B (UDP) + 20B (IP) + 4B (802.1 Q-TAG) + 14B (ETH MAC) + 4B (ETH FCS) + 8B (ETH PHY)
*.gateScheduleConfigurator.configuration =
   [{pcp: 0, gateIndex: 0, application: "app[0]", source: "client1", destination: "server1", packetLength: 1000B + 58B, packetInterval: 500us, maxLatency: 500us},
    {pcp: 4, gateIndex: 1, application: "app[1]", source: "client1", destination: "server2", packetLength: 500B + 58B, packetInterval: 250us, maxLatency: 500us},
    {pcp: 0, gateIndex: 0, application: "app[0]", source: "client2", destination: "server1", packetLength: 1000B + 58B, packetInterval: 500us, maxLatency: 500us},
    {pcp: 4, gateIndex: 1, application: "app[1]", source: "client2", destination: "server2", packetLength: 500B + 58B, packetInterval: 250us, maxLatency: 500us}]

# 门调度可视化配置
*.visualizer.gateScheduleVisualizer.displayGateSchedules = true
*.visualizer.gateScheduleVisualizer.displayDuration = 100us
*.visualizer.gateScheduleVisualizer.gateFilter = "*.switch1.eth[2].** or *.switch2.eth[0].**.transmissionGate[0] or *.switch2.eth[1].**.transmissionGate[1]"
*.visualizer.gateScheduleVisualizer.height = 16