implement optional undefined semantics

[Smattr]

We don't currently implement the additional value, undefined, for each primitive type. This concept itself is a bit of a mixed blessing. If you ever read undefined it's considered an error and explicitly setting a value to undefined is only useful to aid symmetry reduction. In practice some models would be better off without it and the extra state bits it induces.

My current plan is to add optional undefined semantics. You can set the default (whether a primitive has an undefined or not) via the command-line. This default will apply to all non-specific types. For a type that wants a non-default (wants an undefined value always or never), you can use nullable or non-nullable types:

type
  foo_t: 0 .. 1!; -- <- explicitly non-nullable (has no undefined value)
  bar_t: 0 .. 1?; -- <- explicitly nullable (has an undefined value)

This syntax is new, but I think can be implemented in such a way that it doesn't conflict with existing syntax.