Tag(sp22)
UPDATE: If you're running Windows, there is a fix to a freeze bug in version 1.5.0. Update if you haven't already!
Some notes:
always
go? Inside the property predicate? Outside the property predicate?unsat
or theorem
test failure. I'd like this to go to Sterling, but I can't promise that quickly.)root
is not the top of the stack; is the bottom. This isn't very realistic, even I was confused a bit after having paged out the assignment! It is admittedly contrived, and exists only to get you practice using reachability and transitive closure.
How to write the "top of stack" helper? It can be either a fun
or pred
. The key is: what describes the top of the stack? Perhaps these would be a good start:
If you want to turn that into a function, you can use set comprehension, e.g., {e: Element | ...}
.
Don't use next is linear
on Stack. While it might work nominally, there are risks in a partially-constructed model. Can make some debugging tricks below more difficult, since cores don't know about bounds annotations.
Examples in temporal mode are only good for talking about one state traces. You can't use priming on the left-hand side of a bind, and you can't refer to state objects on the right-hand side.
Moreover, because of how bounds are passed to the engine, bounds in an example apply to all states. So beware! See this example:
Unnecessary quantification causes branching; eliminate this when possible! Consider this example:
Instead, either use let
to give a name to the result of the helper, or just use the helper expression.
Some of you are experiencing a problematic difference in performance (seemingly mostly on Windows). We're looking into this, but for now, here are some workarounds.
The fragment below is taken from a student's question, so it's incomplete:
This test can be rewritten:
It's less detailed, but requires less quantification.
If we weren't in temporal mode, this would be a great time for an example
or inst
. Unfortunately, we are.
one
sigsThe key is to reduce symmetry. We can still do that by adding one
sigs to represent the constant values and cells in the test. I suggest creating a separate Forge file for this:
This is just the original test verbatim, but without the quantifiers. It finishes quickly.
Debugging an unsatisfiable run can be challenging. I want to step through the process I usually follow, based on (a fragment of) a student's question on EdStem. This is meant to exist within the buffer problem:
We would expect both tests to pass. Unfortunately, exactly 3 Cell
does not. What's the problem?
Forge has an experimental option to try and find a minimal subset of the constraints that are responsible for unsatisfiability. Add the following 4 lines to your spec if you want to use the feature:
The console output will include a list of line numbers that, together, yield unsat (under the bounds given). At the moment, the output sometimes involves references to Forge's library. E.g., in this example, we got a reference to line 638 of a certain file, which is where Forge issues constraints for one
or func
fields.
Try this on a spec of your own! Just remember to disable the 4 options when you're done, as they can impact performance.
In this case, there's not much in the core: init
, for instance, isn't included. The always ...
formula, however, is.
always
is involvedThe core in this case pointed to the always
. To debug this further, we'll unroll it to specify:
Mantra: "the problem might be caused by temporal mode looking only for lassos". In this case, it turned out that we didn't give Forge enough states to build a lasso using those transitions. To fix this, we'll increase the trace length (6 suffices, but let's make it 10):
option max_tracelength 10
Recall that there are two very different kinds of "tests" in Forge. Consider these two:
push
predicate over-constrained?"The first is about checking the model is a reasonable approximation of the system we're trying to understand through the model. The second is using the model to learn something about the system (modulo the model's correctness and sufficient detail). Don't confuse these.