JPF Inspector Architecture

JPF Inspector consists of the following:

• The frontends. The frontend's job is to create the client, then accept commands from the user and pass them to the client. It must also create an output stream where the client will write its output. There are two frontends:
  • Graphical frontend for JPF Shell.
  • A command-line frontend.
• The client. The client parses commands using the ANTLR client command grammar. It then executes these commands, usually by calling a method on the server. The server usually returns some representation of the rules which the client then formats and displays to the user.
• InspectorListener. When JPF is started, the Inspector automatically attaches its own listener, the InspectorListener. This listnener then passes some events to the server. This is used, for example, to trigger breakpoints.
• The server. The server accepts commands from the client and events from the InspectorListener and acts upon them. For example, it examines whether a breakpoint was hit and if so, it stops JPF execution. The server may not directly inform the user of its actions. To do this, it uses callbacks which are its only means of calling methods of the client.