A few non-trivial updates:
- (H)CTL model checker has been updated to version
0.3.0
and now supports quantifiers with domain (i.e.V{x} in %domain%
). PerturbedAsynchronousGraph
cannot be created from a network with implicit parameters. This simplifies a lot of correctness reasoning, because the color sets of the internal graphs and the original network are always compatible.- CI is now testing that example notebooks work.
- Several methods where it makes sense (mostly various
mk_*
methods) can take aModel
object instead of raw values (e.g.VertexModel
instead ofdict[VariableId, bool]
).
Other misc stuff:
- Added
Bdd.validate
implemented inlib-bdd
version0.5.22
. - Added
VertexSet.enclosed_subspace
andVertexSet.enclosed_named_subspace
.