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 subsection.
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 1.5, “Creating a simple Eclipse project to contain BIR models”). Figure 1.7, “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 1.8. 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 1.8, “ 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.
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 1.9, “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 1.9, “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.
Figure 1.10, “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.
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.
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 1.12, “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.
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 1.13, “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 1.14, “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 1.14, “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. We will return to the subject of Bogor modules, extensions, and options in Chapter 3, Bogor Architecture.
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.
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!
Ignore the last five lines in the output for now; we will come back to it later when discussing the symmetry reduction in Chapter 4, Extensions.