Safe, reliable and efficient computer networks are essential for modern digital communication. Configuring these networks is a challenging task, which today is mostly performed manually. To aid in this task, the tool AalWiNes provides polynomial-time analysis of the behaviour of a type of network, called MPLS network, even under the scenario of multiple link failures. AalWiNes answers queries on MPLS networks by translating them into reachability queries on pushdown systems.
We extend AalWiNes with quantitative properties of network traces and implement an efficient algorithm to find traces minimizing these properties. We also define an algorithm for automatically generating MPLS networks, and we implement algorithms for pushdown system reachability in the library PDAAAL used by AalWiNes. Our experimental evaluation demonstrates that we outperform the state-of-the-art tool previously used by AalWiNes for pushdown reachability checking, and that our shortest trace algorithm for weighted pushdown systems only incurs a small overhead compared to unweighted reachability checking.