New use of AALpy library

[xiaopeng-ye]

We think that you can include a new section to use the AALpy library as a debugger tool for software that is internally based on state machine as well as Vim, which is a text editor based on modes as shown in the following image, in the current versions of Vim they include modes that do not appear in the previous link so at first, our objective was to generate the graph so that they could cover those states, but during the process we discovered bugs and we thought it could be a totally valid tool having the advantage of being more visual and with much less code. The bugs found and the model generated are detailed below.

Vim model

In the code, I used the Neovim editor specifically because it provided an API for many languages including Python. Neovim and Vim have the relationship that each patch of Vim is brought to Neovim by the community since Neovim was developed from Vim.

import neovim
from aalpy.base import SUL
from aalpy.automata import MooreMachine
from aalpy.oracles import StatePrefixEqOracle
from aalpy.learning_algs import run_Lstar
from aalpy.utils import visualize_automaton, save_automaton_to_file
from time import sleep
from random import seed
seed(100)  # all experiments will be reproducible


class MooreSUL(SUL):
    """
    System under learning for Mealy machines.
    """

    def __init__(self):
        super().__init__()
        self.cast_mode = {'n': 'Normal', 'no': 'Operator-pending', 'nov': 'Operator-pending charwise',
                          'noV': 'Operator-pending linewise', 'niI': 'Insert Normal', 'ix': 'Insert Ctrl-X Mode',
                          'i': 'Insert', 'c': 'Command-line editting', 'v': 'Visual', 'V': 'Visual Line',
                          '\x16': 'Visual Block', 'ic': 'Insert Command-line completion', 's': 'Select', 'S': 'Select Line',
                          '\x13': 'Select Block', 'R': 'Replace', 'Rv': 'Virtual Replace', 'no\x16': 'Operator-pending blockwise',
                          'niV': 'Virtual Replace Normal', 'niR': 'Replace Normal', 'Rx': 'Replace Ctrl-X Mode', 'Rc': 'Replace Command-line completion',
                          'r': 'Hit-enter prompt', 'cv': 'Ex mode', 'rm': 'The more prompt', 't': 'Terminal',
                          # new modes added by vim on the path 8.2.3236
                          'vs': 'Select Visual', 'Vs': 'Select Visual Line', '\x16s': 'Select Visual Block'}

    def pre(self):
        """ """
        self.n = neovim.attach(
            "child", argv=['/bin/env', 'nvim', '--clean', '--embed', '--headless', '--noplugin', 'filename'])
        self.n.input(":set cmdheight=2<CR>")

    def post(self):
        self.n.close()

    def step(self, letter):
        current_mode = self.n.api.get_mode()
        if letter is not None:
            if current_mode["blocking"] is True:
                self.n.input(letter)
            elif current_mode["mode"] in ('ce'):
                return self.cast_mode[current_mode["mode"]]
            elif letter == '<C-o>' and current_mode["mode"] == 's':
                self.n.feedkeys(self.n.replace_termcodes('<C-o>'), 't')
            elif letter == '<C-o>' and current_mode["mode"] == 'i':
                self.n.feedkeys(self.n.replace_termcodes('<C-o>'), 'L')
            elif letter == '<C-o>' and current_mode["mode"] == 'v':
                self.n.feedkeys(self.n.replace_termcodes('<C-o>'), 'Lx')
            elif letter == '<C-o>' and current_mode["mode"] == 'vs':
                self.n.feedkeys(self.n.replace_termcodes('<C-o>'), 'xt')
            elif letter == 'gh':
                self.n.feedkeys(self.n.replace_termcodes('gh'), 't')
            elif letter == 'vi':
                if current_mode["mode"] == 'ce':
                    self.n.input('vi<CR>')
                else:
                    return self.cast_mode[current_mode["mode"]]
            else:
                self.n.feedkeys(self.n.replace_termcodes(letter), 't')

        next_mode = self.n.api.get_mode()

        if next_mode["blocking"] is True:
            if next_mode['mode'] == current_mode['mode'] and next_mode['mode'] in ('i', 'R'):
                return self.cast_mode[next_mode['mode']] + ' Special character pending'

        return self.cast_mode[next_mode["mode"]]


if __name__ == '__main__':
    sul = MooreSUL()

    input_al = ['i', ':', 'v', 'V', '<C-v>', '<C-q>', '<C-x>',
                '<Esc>', 'gh', '<C-o>', 'Q', 'vi', 'R', 'c', 'gH', 'g<C-h>']

    state_origin_eq_oracle = StatePrefixEqOracle(
        input_al, sul, walks_per_state=15, walk_len=10)
    learned_moore = run_Lstar(input_al, sul, state_origin_eq_oracle, cex_processing='rs',
                            closing_strategy='single', automaton_type='moore', cache_and_non_det_check=True, print_level=3)

    visualize_automaton(learned_moore, file_type='svg')

    save_automaton_to_file(learned_moore, path='nvim-moore', file_type='dot')

The currently generated model only includes the most significant Vim inputs for state transitions.

The image below looks clearer but with fewer inputs because there are 10 MB restrictions on github.

input_al = ['i', ':', 'v', 'V', '<C-v>', '<C-q>', '<C-x>', '<Esc>', 'gh', '<C-o>', 'Q', 'vi', 'R', 'c']

Bugs

When professor Pierre tried to generate the diagram with certain inputs, he generated a non-deterministic behavior for what he suspected as a Vim bug, then he reported it as an issue and it was finally fixed by the community.
vim/vim#8323

[emuskardin]

We will certainly add a note in README and Wiki about your interesting use case and put a link to your post here.

We are happy to hear that you have used AALpy and managed to find bugs with it :)

[pierreganty]

A second bug, this time in Neovim, was confirmed neovim/neovim#15288 and fixed neovim/neovim#15292 .

[pierreganty]

I got back to it. A new issue vim/vim#12045 has been discovered and fixed (at least partially) thanks to Moore machines learning algorithm.

[pierreganty]

One more issue discovered and fixed with AALpy: vim/vim#12684

[pierreganty]

And another one: vim/vim#12115

[pierreganty]

And one more: vim/vim#13091

[pierreganty]

Paper published at the SPIN conference 2024

[emuskardin]

Very cool, nice write-up that Imo could be used to teach automata learning from a practical perspective on concrete software examples :)