nv
nv copied to clipboard
NetworkVerification
A Framework for Modeling and Analyzing Network Configurations
For some examples, particularly those in [`benchmarks/SinglePrefix/Random`](https://github.com/NetworkVerification/nv/tree/master/benchmarks/SinglePrefix/Random) and [`examples/TopologyZoo/kdl/`](https://github.com/NetworkVerification/nv/tree/master/examples/TopologyZoo/kdl), NV will randomly fail to parse an SMT reply if the input has a very large number of partitions it creates....
It would be great if we could use other values to refer to nodes rather than simply numbers. This could be a simple case where we internally just store all...
Here's an odd bug that seems to occur when flattening and then encoding certain examples. The below code leads to an assertion failure during execution of `SmtUnboxed.encode_exp_z3_single`: ```ocaml type attribute...
Given the network below, NV currently appears to get stuck during the second round of inlining, following map unrolling. ```ocaml (* Benchmark testing fault tolerance reachability to the destination. *)...
Per commit [89efe79](https://github.com/NetworkVerification/nv/commit/89efe796965ca5c5ea14bd5f9e71d0777497f5ad), we currently have a bug in Kirigami when handling remapping of node expressions. [`examples/kirigami/node-eq.nv`](https://github.com/NetworkVerification/nv/tree/master/examples/kirigami/node-eq.nv) gives a MWE of this. Essentially, the issue is as follows: When encoding...
Would be nice to write e.g. `let trans _ x = x + 1` instead of having to declare an unused variable for the edge. It would also be easier...
I've been trying to get results from simulating `benchmarks/SinglePrefix/TopologyZoo/USCarrier.nv`, but while I can verify it in SMT in about a minute, simulation appears to hang. Uncommenting the print statement at...
The current precedence levels used when printing seem to have some minor inconsistencies which lead to the absence or redundancy of parentheses in some places. These occur in a couple...
A possible extension to the tool that would be handy from a development and debugging standpoint would be more robust logging. We could add a new dependency (e.g. [logs](https://erratique.ch/software/logs/doc/Logs/index.html)) and...
There are two separate issues with assertions and simulation: 1. Simulation should not halt after a failed assertion, at least simulation of subsequent assertions should continue (before hitting another solution...
Metadata
Owner
Metadata
A Framework for Modeling and Analyzing Network Configurations