User Manual

• The menu toolbar
  • File Menu
    • Open
    • Exit
  • Description Menu
    • Asynchronous requests
    • Asynchronous requests
  • FC2 Param. Menu
    • Generate FC2 parameterized (pFC2)
    • Generate hierarchical pFC2 subtree
    • Save FC2 parameterized
    • Save hierarchical pFC2 tree
  • LOTOS Menu
  • About
  
  
• Hierarchical tree frame
• Tabs
  • Description tab
  • FC2Parameterized tab
  • Instantiation tab
  • LOTOS tab
  
  
• Specification of observable events
  • Visibility of the methods
  • Visibility of the method's arguments
  • Multiplicity of the components
  • Specify names and arguments domains
    • Note
  
  
• Contact and bugs report

The main window is composed by three sections as seen in figure 2: the menu on top, the hierarchical tree on the left and tabs in the main frame.

Figure 2: Main window

The menu toolbar

The available menus in the application are: File, Description, FC2 Param, LOTOS and About.

File Menu

Open:

Choose the fractal file. Note: the directory where the complementary files are located must be defined in the classpath before launching the application.

Exit:

closes the application.

Description Menu

Asynchronous requests:

Sets the translation output into asynchronous messages.

Asynchronous requests:

Sets the translation output into synchronous method calls.

FC2 Param. Menu

Generate FC2 parameterized (pFC2):

generates the hierarchical FC2 code associated with the selected component. The output will be written into the main frame described in section. Note that both the component and its subcomponents are included, but not further descendants.

Generate hierarchical pFC2 subtree:

generates the full hierarchical FC2 code starting from the selected component from the hierarchical tree frame. The output will be placed in the main frame.

Save FC2 parameterized:

saves the generated FC2 parameterized (pFC2) into a user defined filename (example <filename>.fc2) and the associated instantiation file in the same folder (example <filename>Inst.fc2).

Save hierarchical pFC2 tree:

saves the code to an user defined file generated by "Generate hierarchical pFC2 subtree" and then writes the instantiation file and the SVL script.

Figure 5: FC2 Param. Menu

LOTOS Menu

This feature is still under construction.

About

General information about the program and its developers.

Figure 6: About Menu

Hierarchical tree frame

Shows the system structure as a tree. The user may select a component and see its description in the main frame (figure 2) or generate either FC2 or LOTOS code.

Tabs

Description tab

Shows the description of the component selected by the hierarchical tree frame. In this section it is possible to set the multiplicity of the components and the visibility of each method and its arguments.

Within the description, the user may see the component name, the behaviour file (LOTOS filename if it is a primitive component), its multiplicity and the attached interfaces.

In the same window there is a list of currently defined variables. If one is selected, the new variable will be created as its alias, i.e., both variables will be given the same instantiation.

FC2Parameterized tab

Shows the generated FC2 code with the latest selected option from the FC2Param menu.

Instantiation tab

Shows the FC2 code instantiation, i.e., defined variables and associated values.

LOTOS tab

This feature is still under construction.

Specification of observable events

Visibility of the methods

For each method shown in the description, it is possible to define if it will be visible or not (in the FC2 translation). If a method is visible, its synchronisation vector will be labelled with a non-internal action, whereas if invisible it will be internal (tau). By default all methods are visible.

The communications and synchronisations will still happen as usual for the invisible methods, but the user will not be able to see them as they are considered internal actions. This allows the various model-checking tools to minimise the resulting automata and remove many unwanted intermediate method calls not relative to the property the user may be seeking to prove. Remember to always choose a proper abstraction to keep the model as simple as possible, otherwise you are very likely to have the state-explosion problem.

Visibility of the method's arguments

It is possible to define which arguments will be visible. If the argument is visible, it will be included in the FC2 code. By default all arguments are hidden (invisible).

When unchecked, the arguments will not be included and should be considered as a simplification to the model. By combining the visibility strategies of the methods with their arguments, the user may tackle more realistic models while letting the model-checkers find more human-readable counter-examples.

Multiplicity of the components

To set the method's multiplicity, the multiple checkbox must be selected (if not checked) or click the 'Add' button. A new window will appear as seen in figure 7, on which the variable name and value must be specified. A default value will be suggested. To accept the new instantiation click on 'Add'. The recently created variable can now be seen in the component description.

Specify names and arguments domains

The name pattern must contain only letters or the '_' symbol, and must start with a letter.
Valid name: var, var_a
Invalid name: _var

There are 4 instantiation types:

• integer: A non-negative discrete value, example 1.
• string: Associate this variable to a previously defined one (alias).
• interval: integer interval, either lower or upper bound may be integers (non-negative) or name variables. Must start with '(' and finish with ')' and be separated by ','. Example:
  • (1,4)
  • (2,var)
  • (var_a,var_b)
• set: set of elements specified between '{' and '}'. Items are separated by ','. Example: {1,3,5,7}

Note:

To specify global variables, the user should add variables to the root component. (Figure 9)

Figure 9: Add global variable window

Contact and bugs report

For information on the latest releases, updates and papers please visit http://www-sop.inria.fr/oasis/Vercors/index.html or send us an email to vercors < at > sophia.inria.fr. This is the first version of the program, therefore any comments are welcomed.