package lstar-rocq
Formally-verified automata learning in Rocq
Install
dune-project
Dependency
Authors
Maintainers
Sources
lstar-rocq-3.0.tbz
sha256=ae76ede9f91f2b2898340aee12dea0f948de2b668733ff61d15f97536c637eb3
sha512=a35b569227d661aec37e13a029229a294a68c5ee5c2ad107afc0e592cf0097b40d395a565d4209ee6b7055b8501017dc24f8f4ca95d98996e9e0172f45477fc7
doc/CHANGES.html
v3.0
Breaking changes. Teacher modules have changed substantially. TTT for DFAs, L* for Moore and Mealy machines are now supported.
v2.0
Breaking changes. Both L* and KV signatures have changed, requiring passing fuel in via the Teacher module rather than upon calling the learner loop. This arises from new guarantees about termination and minimality for both algorithms.
v1.0
Initial release