(for MIO Workbench 1.4.1, not yet updated for 2.0.0)
The command-line shell of the MIO Workbench can be accessed either by switching to the MIO Workbench perspective (and reset it), or by selecting Window > Show View > Other > MIO Workbench > Command-Line Shell.
The purpose of the shell is to perform complex verification tasks with your MIOs. To load a .mio file in the shell, just drag the file from the Navigator and drop it in the shell view. Then, you are asked to enter a name for the variable under which the MIO should be accessable in the shell. We recommend to use the filename (without file extension) in order to avoid confusion.
The shell can have two types of variables: variables that reference .mio files (these variables are created by drag-and-drop, as decribed before) and auxiliary, temporary variables which do not reference a .mio file but store a MIO model. All declared variables are listed in another view, Shell Information, which is displayed at the bottom right corner (in the standard MIO Workbench perspective).
The input grammar of the shell is given as follows.
<stat> ::= 'list' // Lists all currently declared variables of the shell.
| 'show' <intf> // Returns a textual description of <intf>.
| 'actions' <intf> // Returns all actions of <intf>.
| save <id> // Saves <id> (a temporary variable storing a MIO) to a file.
| open <id> // Opens <id> (a variable referencing a MIO file) in the editor.
| <id> := <intf> // Declares a new variable <id>.
| <intf> <= <intf> // Checks for strong modal refinement between two MIOs.
| <intf> <=* <intf> // Checks for weak modal refinement between two MIOs.
| <intf> <--> <intf> // Checks for strong modal compatibility between two MIOs.
| <intf> <==> <intf> // Checks for weak modal compatibility between two MIOs.
| help // Prints this help.
<intf> ::= <id> | <conj> | <comp> | <optcomp> | <quot>
<conj> ::= '(' <intf> ( '&&' <intf>)+ ')'
<comp> ::= '(' <intf> ( '||' <intf>)+ ')'
<optcomp> ::= '(' <intf> ( '||opt' <intf>)+ ')'
<quot> ::= '(' <intf> '--' <intf> ')'
<id> ::= ( 'a'..'z' | 'A'..'Z' | '_' ) ( 'a'..'z' | 'A'..'Z' | '0'..'9' | '_' )*
Comments are closed.