New use of AALpy library#13

xiaopeng-ye started this conversation inIdeas

xiaopeng-ye

Aug 5, 2021

· 7 comments· 1 reply

Return to top

Discussion options

xiaopeng-ye
Aug 5, 2021

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 followingimage, 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.

importneovimfromaalpy.baseimportSULfromaalpy.automataimportMooreMachinefromaalpy.oraclesimportStatePrefixEqOraclefromaalpy.learning_algsimportrun_Lstarfromaalpy.utilsimportvisualize_automaton,save_automaton_to_filefromtimeimportsleepfromrandomimportseedseed(100)# all experiments will be reproducibleclassMooreSUL(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'}defpre(self):""" """self.n=neovim.attach("child",argv=['/bin/env','nvim','--clean','--embed','--headless','--noplugin','filename'])self.n.input(":set cmdheight=2<CR>")defpost(self):self.n.close()defstep(self,letter):current_mode=self.n.api.get_mode()ifletterisnotNone:ifcurrent_mode["blocking"]isTrue:self.n.input(letter)elifcurrent_mode["mode"]in ('ce'):returnself.cast_mode[current_mode["mode"]]elifletter=='<C-o>'andcurrent_mode["mode"]=='s':self.n.feedkeys(self.n.replace_termcodes('<C-o>'),'t')elifletter=='<C-o>'andcurrent_mode["mode"]=='i':self.n.feedkeys(self.n.replace_termcodes('<C-o>'),'L')elifletter=='<C-o>'andcurrent_mode["mode"]=='v':self.n.feedkeys(self.n.replace_termcodes('<C-o>'),'Lx')elifletter=='<C-o>'andcurrent_mode["mode"]=='vs':self.n.feedkeys(self.n.replace_termcodes('<C-o>'),'xt')elifletter=='gh':self.n.feedkeys(self.n.replace_termcodes('gh'),'t')elifletter=='vi':ifcurrent_mode["mode"]=='ce':self.n.input('vi<CR>')else:returnself.cast_mode[current_mode["mode"]]else:self.n.feedkeys(self.n.replace_termcodes(letter),'t')next_mode=self.n.api.get_mode()ifnext_mode["blocking"]isTrue:ifnext_mode['mode']==current_mode['mode']andnext_mode['mode']in ('i','R'):returnself.cast_mode[next_mode['mode']]+' Special character pending'returnself.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

You must be logged in to vote