엔지니어들은 네트워크를 설계할 때 트레이드오프(trade-offs)를 탐색해야 합니다 (예: 한 토폴로지는 더 많은 집계 대역폭을 제공하고, 다른 하나는 낮은 지연 시간이나 더 나은 복원력을 가집니다). 이러한 트레이드오프는 정량적 속성에 대한 추론을 요구합니다. 우리는 가중치 NetKAT(wNetKAT)를 기반으로 하는 빠른 분석기를 제시합니다. wNetKAT는 반환체(semiring)에서 추출된 가중치를 사용하여 네트워크 동작을 모델링함으로써 정량적 추론에 의미론적 기초를 제공하는 도메인 특화 언어입니다. 우리의 개발 핵심은 가중치 심볼릭 패킷 프로그램(wSPPs)이라는 심볼릭 데이터 구조의 설계입니다. 이는 가중치 정책의 의미론을 간결하게 표현하며, 이를 직접 구현하는 것은 불가능합니다. 우리는 모든 정책 구성 요소를 기호적으로 계산하는 방법을 보여줍니다. 놀랍지 않게도 핵심은 클린 스타(Kleene star)이며, 이를 위해 맞춤형 알고리즘을 설계했습니다. 또한, 여러 목표의 경계면(multi-objective frontiers)과 그것들을 실현하는 네트워크 경로를 함께 계산하는 트레이스 캐링 파레토 반환체(trace-carrying Pareto semirings)를 개발합니다. 우리는 Lean에 이 개발 과정을 형식화하고 최적화된 Rust 구현을 제공합니다. 우리의 구현은 반환체를 매개변수로 하므로, 고전적인 분석과 정량적 분석 모두를 포괄합니다: 우리는 이것이 크게 최적화된 Boolean-reachability verifier인 KATch와 경쟁력이 있으며, 확률론적 분석에서는 McNetKAT 및 Storm보다 수 배나 빠르다는 것을 보여줍니다. Fat-tree와 Jellyfish 데이터센터 토폴로지를 비교한 사례 연구는 이 프레임워크가 다중 목표 설계 시간 분석을 지원함을 보여줍니다.