Assertions

[nickgian]

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 declaration), maybe it should be an option from the user on how to behave when an assertion fails. One of the advantages of simulation is that you can find multiple/all problems in one go there is no reason to remove that.

2. The second problem is more challenging/research-oriented: tracking problems is more difficult now. With the old system, when an assertion failed we knew which node was associated with it. In the new system, if you use something like foldNodes you basically get a yes or no answer which makes it hard to track down the problem. We should find a way to attach more information to which part of an assertion failed.

[alberdingk-thijm]

Re: 2, how does foldNodes get transformed? One way to make the assertion errors more helpful might be to have some special behavior when using foldNodes and foldEdges to unroll the folds, get back the expressions containing the offending nodes and edges and then return those. Something like this, maybe?

Given this nv file:

let nodes = 2
let edges = {0=1;}

let init n = match n with
  | 0n -> 0
  | 1n -> 10
let trans e x = x + 1
let merge n x y = if x < y then x else y

let sol = solution { init = init; trans = trans; merge = merge }
assert (foldNodes (fun u v acc -> acc && v = 0) sol true)

Unroll the assert as:

assert true && sol[0n] = 0 && sol[1n] = 0

And then on failure, identify which conjuncts did not pass the test:

assert true && sol[0n] = 0 && sol[1n] = 0
                              ^^^^^^^^^^^

We could then report this information to the user.