Rukia
Rukia is a C++ library to explore graphical models by generating at random paths in automata.
Instead of using an isotropic random walk (i.e., choosing the next state uniformly at random among the successors of the current state), Rukia guides the random walk to guarantee a global uniform distribution among the elements to be covered, whatever the model topology. To do that, Rukia uses combinatorial techniques to count the number of elements to be covered and then guide the model exploration in order to maximize the minimal probability of covering one of those elements.
One particularity of Rukia is the use of space-efficient algorithms that leverage the limitation on the size of model and the length of paths that can be generated with this approach (See, for example, the Dichopile algorithm). Thus, it was possible to generate paths of length 4000 in an automaton with more than 12 million states.
Currently, Rukia supports the following coverage criteria:
- All paths of length n (there is a trick to also allow all paths of length less or equal to n)
- All lassos (kind of paths that end by a cycle -- useful for Monte Carlo model-checking)
- An extension is under development for handling additional criteria besides "all paths" : "all edges" and "all vertices" and maybe criteria describing other sets of edges or vertices.