Bogor Website - Running Bogor

An introduction to Bogor Graphical User Interface (GUI) and Command-line Interface (CLI).

2. Using Bogor

After familiarizing yourself with the Eclipse platform, we are now ready to explore the Bogor user interface. Bogor provides a customized text editor for BIR that features syntax highlighting and well-formed-ness checking (e.g., type checking). The BIR text editor is activated by default whenever you open a file with extension bir. The syntax highlighting colors BIR constructs differently according to their categories.

For example, BIR keywords are colored purple, while identifiers are yellow. This makes it easier to understand BIR code. The BIR well-formed-ness checking is integrated in the editor. It is activated when the editor is opened, and also whenever its content is saved (e.g., by pressing Ctrl+s). If the checker finds the model in the editor is ill-formed, then it will try to mark the line numbers that have the errors. The error markers will also be displayed in the Tasks view.

Note that there are several tabs in the editor. The "Symbol Table" tab in the editor presents a text representation of Bogor symbol table for the model (used for debugging purposes). The "Output" tab is used to display the output from the Bogor model checker. The "Counter-Example" tab is used to display graphical representation of states when using the counter-example display, which will be explained in the next subsections.

Figure 2. Creating a simple Eclipse project to contain BIR models

Use Eclipse's "Simple" project type

Give the project a name

Figure 3. Creating a new BIR model

Use Bogor's wizard to create a new model file

Name the model and configure some basic options

To try the editor features, create a simple project in Eclipse called bogor-models, and then create a file called 2DiningPhilosphers.bir using the BIR model creation wizard (see Figure 2, “Creating a simple Eclipse project to contain BIR models�?). Figure 4, “Bogor BIR Editor�? presents the screen shot of Eclipse after you created the BIR file. Note that the well-formed-ness check was activated when the file was created, and it found that the (empty) model has an error. It indicates the first line with an error marker and displays the error message in the Tasks view. In this case, the system keyword should be followed by a legal identifier. The default name (deduced from the filename 2DiningPhilosophers.bir) is illegal; it should start with an alphabetic character.

Figure 4. Bogor BIR Editor

Figure 5. A 2 Dining Philosophers BIR Model

system TwoDiningPhilosophers {
  boolean fork1 := false;
  boolean fork2 := false;
  
  active thread Philosopher1() {
    loc loc0: live {} // take first fork
      when !fork1 do { fork1 := true; }
      goto loc1;

    loc loc1: live {} // take second fork 
      when !fork2 do { fork2 := true; }
      goto loc2;

    loc loc2: live {} // put second fork 
      do { fork2 := false; }
      goto loc3;

    loc loc3: live {} // put first fork
      do { fork1 := false; }
      goto loc0;
  }

  active thread Philosopher2() {
    loc loc0: live {} // take second fork
      when !fork2 do { fork2 := true; }
      goto loc1;

    loc loc1: live {} // take first fork
      when !fork1 do { fork1 := true; }
      goto loc2;

    loc loc2: live {} // put first fork
      do { fork1 := false; }
      goto loc3;

    loc loc3: live {} // put second fork
      do { fork2 := false; }
      goto loc0;
  }
}

Copy and paste the model in Figure 5, “ A 2 Dining Philosophers BIR Model �?, and save the file. Note that the model is now well-formed, thus, the checker does not display any error messages.

2.1. Model Checking BIR Models

Figure 6. Bogor Model Checker

Invoking the model checker

Summary of model checking analysis

By default, Bogor can check for deadlock and safety properties expressed as assertions and invariants. You can run the model checker by right-clicking the BIR editor of the model that you want to check, and then selecting "Model check..." in the pop-up menu. Try it now on the BIR editor of the dining philosophers model. Bogor will open its status view as illustrated in Figure 6, “Bogor Model Checker�?. The status view contains statistics information about the system name, the number of transitions it has made so far, the number of unique states that it has found, the number of revisited states, the number of errors it has found, and the time elapsed so far.

After model checking is finished, Bogor writes a trail file with the extension bogor-trails if any errors have been found (such as shown in Figure 6, “Bogor Model Checker�?). The trail file contains schedule information and state transitions that lead to the errors. Bogor features a counter-example display for visualizing the error paths to help understand what went wrong. You can open the counter-example display by double-clicking the trail file.

2.2. Counter-example Display

Figure 7. Bogor Counter-example Display

Figure 7, “Bogor Counter-example Display�? presents the Bogor counter-example view. If you open several trail files, then you can select which one you want to look at by selecting it from the first combo box. By default, Bogor will open the first error path in the trail file (corresponding to the first error found by the model checker). You can select the error path that you want to see (if there are several) by selecting it from the second combo box. The State Tree below the first combo box displays the global variables and threads that are alive in the current state. If you select a variable or a thread, then its value or state will be displayed in the Value Tree (next to the State Tree). The Detail Text Box below it displays detailed information of the values you selected in the Value Tree.

Above the Value Tree are the Navigation Buttons and Scroll Bar. You can step forward and backward through the transitions using those buttons and the scroll bar. To their left is a label displaying the state number you are currently at and the total number of states in the current error path. The green highlight in the Counter-example Model Viewer indicates the transition that Bogor will execute when you step forward, and the blue highlights indicate the other threads that are enabled in that state.

2.3. Random Simulation Mode

Bogor has a random simulation mode. Random simulation does not explore all possible paths as in model checking, instead, it picks a transition randomly whenever there is a non-deterministic choice between enabled transitions at a certain state. This is analogous to executing the model without a particular scheduling policy. Thereore, it may miss some errors, however, it is cheaper because it does not explore all possible paths in the state-space of the model. Similar to model checking, Bogor will write a trail file if an error is found.

2.4. User-guided Simulation Mode

Figure 8. Bogor User-guided Simulation

Figure 9. Selecting Branches in User-guided Simulation

Bogor also has a user-guided simulation mode, where the user will be asked to choose a transition from the enabled transitions of a state whenever there is a non-deterministic choice to be made. Figure 9, “Selecting Branches in User-guided Simulation�? presents Bogor in user-guided simulation mode. The Choose Dialog displays the current state where the first non-deterministic choice has to be made. Similar to the Counter-example Display, it also has a State Tree, a Value Tree, and a Detail Text Box. The Choose Dialog has a Choice List Box instead of the navigation buttons and scroll bar in the Counter-example. The list box displays the enabled transitions in that state of which you have to choose. In order to choose one, you need to click the transition and then click the Select Button at the bottom of the dialog.

2.5. Selecting Core Model Checker Components

Figure 10. Bogor Configuration

The Bogor Configuration Dialog is allows users to fine-tune aspects of a state-space search. Here, an implementation for each of the core model-checking components is selected. By default, the default version supplied with the Bogor distribution is configured for each module. As pictured in Figure 10, “Bogor Configuration�?, the Configuration dialog allows the user to easy choose from among the available implementations of each pluggable model checker component. The set of options pictured for the ISearcher corresponds to an installation of Bogor plus a rich mix of add-on model checking bundles.

Once the selection of core model-checking components is made, expanding the tree for a module (e.g., ISearcher reveals the set of options supported by the particular implementation. The DefaultSearcher, for example, supports several options for limiting the scope of the state space search and specifying simple invariant properties. These are pictured below in Figure 11, “Configuring Module-specific Options�?.

Figure 11. Configuring Module-specific Options

For example, the configuration ...ISearcher.maxErrors=1 is intended for the ISearcher module, and it tells the maximum errors before the model checker aborts the state-exploration (i.e., Bogor should not stop exploring until it finds 1 error or all states have been explored). If maxErrors is unset, the model checker exhaustively explores the state space to find all errors. The screenshot in Figure 11, “Configuring Module-specific Options�? also contains some erroneous DefaultSearcher option specifications (allAsErrors and invariants). The Bogor user interface validates these and gives an explaination why each is not a legal configuration.

Configurations can be saved to and loaded from files. The context menu activated by right-clicking anywhere inside the main area of the Configuration dialog contains options to import from and export to regular files. As a convention, it is recommended to use thebogor-config file extension for Bogor configuration files.

2.6. Bogor Command-line Interface

Bogor provides a command-line interface which is convenient to use in batch mode. Suppose that ECLIPSE_DIR is an environment variable naming the directory on your computer which contains the Eclipse installation (by default this is called "eclipse"). Then you can run Bogor in a command shell as follows.

sh $ECLIPSE_DIR/plugins/edu.ksu.cis.projects.bogor_99.99/bogor.sh {config} {model}

Note

To users of Bourne shells: if this variable is defined but the script nonetheless complains that ECLIPSE_DIR can't be found, try the following:

export ECLIPSE_DIR

This command informs the shell to make the ECLIPSE_DIR variable visible to any programs started from the shell.

The default Bogor configuration file (default.bogor-conf) is included in bogor.jar. You can also generate a configuration file by saving the configuration in the Bogor Configuration Dialog.

When you execute Bogor with the default configuration for model checking the dining philosophers example, Bogor outputs the same information that you can see in the Console view of the Eclipse user interface:

Bogor v.1.0 (build <VERSION>)
(c) Copyright by Kansas State University

Web: http://bogor.projects.cis.ksu.edu


Transitions: 1, States: 2, Matched States: 0, Max Depth: 1, Errors found: 0

[Time: 51 ms, Depth: 6] Error found: Invalid end state

Transitions: 14, States: 10, Matched States: 5, Max Depth: 9, Errors found: 1
Total memory before search: 322,832 bytes (0.31 Mb)
Total memory after search: 268,552 bytes (0.26 Mb)
Total search time: 61 ms (0:0:0)
States count: 10
Matched states count: 5
Max depth: 9

Generating error trace 0...

Done!

1. Installing Bogor