Finer Plugin - Refinement Automation for the Rodin Platform


Installation

The plugin can be downloaded from

http://www.iliasov.org/ncl.plugin.finer_0.0.1.jar

The plugin is installed by simply copying it into the plugins folder of the Rodin Platform distribution. After this, the platform should start with plugin activated. The plugin menu should appear in the top menu bar:

Getting Patterns

In addition to manual creation, patterns can be imported from an Internet repository. This is done by selecting Patterns/Import menu. The following dialog pops-up:

     


After selecting a pattern repository from the list or typing in one manually, another dialog shows up to select among individual patterns. This dialog is used throughout the plugin. Patterns are imported one by one.


Using Patterns

A pattern is used to refine an existing B specification. Pattern application is done by the Refinement Wizard which can be found in the context menu of a specification in the Project Explorer view.


A pattern will typically prompt user to supply additional information required to apply the pattern.  This reflects the step by step pattern rule evaluation.

 

Finally, a user is presented the summary of actions that will be used to create the refined specification.



Pattern wizard can stop with an error, which means that there is a semantic error in the pattern. It can also abort early if it finds that the pattern cannot be applied to the selected specification (it's application will lead to the exact copy of the original specification).

Creating Patterns

A new pattern is created by selecting menu Patterns/New. A pattern template is automatically created and opened in editor. Patterns are described in XML - this saves
programming efforts but might have negative readability impact.

A typical pattern template looks as follows:

<pattern>

<preamble>

    <name>newtest</name>
    <version major='0' minor='1' revision='0'/>
    <description>
        <!-- TODO: put pattern description here -->
    </description>
    <category>By Project/test</category>
</preamble>

<system>

    <!-- TODO: put pattern rules here -->
</system>

</pattern>


It's made of two parts - preamble and the pattern itself. Preamble contains optional description of a pattern, such as a user-friendly name, description and most importantly, classification into one or more categories.

Preamble may also contain HTML help for the pattern. It's written inside comment quotes and is accessible in the pattern selection dialog.



Preamble can be omitted, in this case the enclosing <pattern> clause also is not needed.
The following is the simplest possible valid pattern (which, of cause, simply produces the copy of input):

<system/>

Annotations

The main limiting factor for a refinement pattern is its ability to distinguish between elements
of a specification. Mathematically identical objects may be given different interpretations by a user and meaningful model transformation can be only achieved when there is a way to capture
this information.

In the plugin this is done by introducing a new database element, called annotation. Any number of such elements can be attached to any part of a specification. Annotation is simply a pair of strings, which is interpreted as name/value pair. Names and values are completely arbitrary and are invisible to the other parts of the Rodin Platform.

Annotation have visual representation and they can be edited in the same manner as other specification elements:


Writing a Pattern

A patterns is described by a combination of predefined basic rules. There are two rule types: matching rules and update rules. Matching rules select an element of a specification according to some criteria. Update rules produce actions which transform an abstract model into a refined one.

The summary of matching rules:
Name Arguments Description
system name Matches a system. Must be the outer-most rule of a pattern
event name guards params actions Matches an event
variable name type init Matches a variable or an event parameter
guard guard Matches an event guard
action variable expression Matches substitution in an event
select:event (as for event) These are notational shortcuts which instead of selecting a random matching element prompt user to provide the selection.
select:variable (as for variable)
select:guard (as for guard)
select:action (as for action)
The summary of update rules:
Name Arguments Description
system name Matches a system. Must be the outer-most rule of a pattern
define:event name Defines a new event
define:variable name type init Defines a new variable or an event parameter
define:guard guard Defines a new event guard
define:action variable expression Defines a new event action
comment Defines a comment

Any rule can take the following arguments:
id='name' - rule name. Can be used to refer to it by its child rules;
scope='id' - the scope of the rule. The argument must be an id of an enclosing rule.
In addition, these arguments can be used with all matching rules:
:name='value' - requires that the rule contain the given annotation name/value pair;
contains='a1, a2, ... an' -  a rule is enabled only if the given annotations are be present in the rule;
predicate='expr'a rule is enabled only if the given predicate holds for the rule.

The following pattern adds a comment to all events of an input specification:

<system>
    <event>
        <comment>comment</comment>
    </event>
</system>

This one, however does nothing (cannot be applied) for any input specification:

<system>
    <event predicate='FALSE'>
        <comment>comment</comment>
    </event>
</system>

Case Study

This case study uses patterns available from tracker http://www.iliasov.org/patt.trackers.
Alternatively, the whole development is available at http://www.iliasov.org/test.tar.gz.In this case a number of simple refinement patterns are used to define skeleton control flow
using program counter variables. This case study is not specific in any way to the plugin.

The aim of this development is to automate the design of protocols. As a starting we use an actual development (hand-coded) which resulted in the following specification:

The specification contains event sequencing, choice and loop. It is very likely that anyone describing a protocol using pure Event-B will have to use these or similar building blocks. It is quite easy to express these building blocks as  B refinement patterns.

To keep the example small and clear, all the shown specifications are automatically generated (except the first one).


The initial specification is (just to have something non-empty):

MACHINE test
VARIABLES counter
INVARIANTS inv1: counter ∈ 0‥10
EVENTS
    INITIALISATION = BEGIN act1: counter ≔ 0 END
    increment = WHEN grd3: counter < 10 THEN act1: counter ≔ counter + 1 END
END

The first pattern that will be applied to this model creates a sequence made of two events. One of the events is the existing event increment, the other is some new event. The pattern also creates program counter variable, which defines a thread of control.
The pattern is called FlowNewSequence and its body is:

<system id='system'>
    <!-- Ask user to select an event from which a sequence will be created -->
    <select:event id='event'>
        <!-- Define program counter variable -->
        <define:variable id='pc' scope='system' type='NAT' init='2'>
            <hint>Program counter variable</hint>
            <comment>Program Counter variable generated by the FlowNewSequence pattern</comment>
            <!-- Define the new event for the sequence -->
            <define:event id='newevent'>
                <define:guard>$pc.name$ = 2</define:guard>
                <define:guard copyfrom='$event.name$'/>
                <define:action variable='$pc.name$'>$pc.name$ - 1</define:action>
                <comment>
                        This event is a part of a sequence defined
                        by the program counter variable $pc.name$
                </comment>

            </define:event>
            <!-- Update the existing event -->
            <define:guard>$pc.name$ = 1</define:guard>
            <define:action variable='$pc.name$'>
                $pc.name$ - 1
                <comment>Pass control to the next event</comment>
            </define:action>
            <define:annotation name='sequence' value='pc'/>           
        </define:variable>
    </select:event>
</system>

The pattern asks user to select an event which be the parent of a new control flow thread (the last event in it). Inside this rule a new event is defined along with the program counter
variable. Note the $$ symbols - any text placed inside $$ is interpreted as an expression and the result of the expression evaluation is substituted in place of the expression.

The pattern application results in the following model:

MACHINE test1
REFINES test
VARIABLES counter,
    pc /* Program Counter variable generated by the FlowNewSequence pattern */
INVARIANTS
    inv1: counter ∈ 0‥10
    inv2: pc∈ℕ
EVENTS
    INITIALISATION = BEGIN act2: counter≔0 || act4: pc≔2 END
    increment = REFINES increment
                    WHEN grd1: counter < 10 grd2: pc = 1
                    THEN
                        act5: counter≔counter+1
                        act6: pc≔pc − 1 /* Pass control to the next event */
                    END
    new1 =
 /* This event is a part of a sequence defined by the program counter variable pc */
                    WHEN grd3: pc = 2
                    THEN
                        act7: pc≔pc − 1
                    END
END

The next pattern is very similar - it adds a new event to the top of a sequence, it requires, however, an existing sequence which is detected by looking for variable with special annotation.

<system id='system'>
    <!-- Select PC -->
    <select:variable scope='system' id='pc' :sequence='pc'>
        <define:event id='newvent'>
            <define:guard>$pc.name$ = $pc.init + 1$</define:guard>
            <define:action variable='$pc.name$'>$pc.name$ - 1</define:action>
            <comment>TODO: put event body here</comment>
        </define:event>   
        <!-- Update PC initialisation -->
        <define:action scope='pc' variable='$pc.name$'>$pc.init + 1$</define:action>
    </select:variable>
</system>This pattern will ask user to select on of the existing program counter variables. If no such variable exists the pattern cannot be applied. Pattern application results in the following machine:

MACHINE test2
REFINES test1
VARIABLES
    counter
    pc
INVARIANTS
    inv1: counter ∈ 0‥10
    inv2: pc∈ℕ
EVENTS
INITIALISATION = BEGIN act2: counter≔0 || act4: pc≔3 END
increment = REFINES increment
                    WHEN
                        grd1: counter < 10
                        grd2: pc = 1
                    THEN
                        act5: counter≔counter+1
                        act6: pc≔pc−1
                    END
new1 =         REFINES new1
                    WHEN
                        grd3: pc = 2
                    THEN
                        act7: pc≔pc−1
                    END
new2 =
 /* TODO: put event body here */
                    WHEN
                        grd4: pc = 3
                    THEN
                        act8: pc≔pc − 1
                    END
END



The next pattern introduces choice - possibility to alternate between two or more events:

<system id='system'>
    <!-- Select an event to split into a choice of two events -->
    <select:event id='event' hint='This event will be split into two events'>
        <define:event id='newvent' copyfrom='$event.name$'/>
    </select:event>
</system>

The pattern simply creates a copy of an existing event, here it is applied to event new1:

MACHINE test3
REFINES test2
VARIABLES
    counter
    pc
INVARIANTS
    inv1: counter ∈ 0‥10
    inv2: pc∈ℕ
EVENTS
    INITIALISATION = BEGIN act2: counter≔0 || act4: pc≔3 END
      
     ...

   
    new1a = WHEN

                        grd5: pc = 2
                    THEN
                        act9: pc≔pc−1
                    END
END


At the next step we introduce loop. A loop is described by supplying two events: one for normal activity and another for loop termination:

<system id='system'>
    <!-- Select PC -->
    <select:variable scope='system' id='pc' :sequence='pc'>
        <define:event id='loop'>
            <define:guard>$pc.name$ = $pc.init + 1$</define:guard>
            <comment>Main loop event</comment>
            <define:event name='$loop.name$_break'>
                <define:guard>$pc.name$ = $pc.init + 1$</define:guard>
                <define:action variable='$pc.name$'>$pc.name$ - 1</define:action>
                <comment>This event terminates loop $loop.name$</comment>
            </define:event>   
        </define:event>   
        <!-- Update PC initialisation -->
        <define:action scope='pc' variable='$pc.name$'>$pc.init + 1$</define:action>
    </select:variable>
</system>

The resulting machine (omitting the identical parts) is:

MACHINE test4
REFINES test3
VARIABLES
    counter
    pc
INVARIANTS
    inv1: counter ∈ 0‥10
    inv2: pc∈ℕ
EVENTS
    INITIALISATION = BEGIN act2: counter≔0 || act4: pc≔4 END
   
    ...

    loop =

 /* TODO: put loop body into this event */
                    WHEN
                        grd6: pc = 4
                    THEN
                        skip
                    END
    loop_break =
 /* TODO: this event terminates the loop */
                    WHEN
                        grd7: pc = 4
                    THEN
                        act10: pc≔pc − 1
                    END
END

In the last refinement we refine the loop body into a sequence by introducing a new control thread using our first pattern - FlowNewSequence:

MACHINE test5
REFINES test4
VARIABLES
    counter
    pc
    pcloop /* Program Counter variable generated by the FlowNewSequence pattern */
INVARIANTS
    inv1: counter ∈ 0‥10
    inv2: pc∈ℕ
    inv3: pcloop∈ℕ
EVENTS
    INITIALISATION BEGIN act2: counter≔0 || act4: pc≔4 || act6: pcloop≔2 END

    ...

    loop =     REFINES loop

                    WHEN
                        grd6: pc = 4
                        grd7: pcloop = 1
                    THEN
                        act12: pcloop≔pcloop − 1 /* Pass control to the next event */
                    END
    loop_break = REFINES loop_break
                    WHEN
                        grd8: pc = 4
                    THEN
                        act13: pc≔pc−1
                    END
    loop1 =
 /* This event is a part of a sequence defined by the program counter variable pcloop */
                    WHEN
                        grd9: pcloop = 2
                        grd10: pc = 4
                    THEN
                        act14: pcloop≔pcloop − 1
                    END
END

Five refinement steps were generated completely automatically. The result is not a complete specification, still it is a significant help for a user. Naturally, all the refinement steps proved automatically. The essence of the patterns mechanism is that pattern application is completely oblivious to peculiarities of an input specification, it does not "see" details irrelevant to pattern application.

Refinement Capture

Refinement patterns mechanism can be used to describe and save refinement information to review or replay it later.

The Refinement Capture in the context pop-up menu creates a refinement pattern that describes the steps leading to a given specification. For an abstract machine, it simply transforms Event B notation into the patterns notation.

For example, capturing refinement leading to the last refinement of the case study results in the following pattern:

<system>

    <define:variable name='pcloop' fulltype='pcloop∈ℕ' type='pcloop∈ℕ' fullinit='pcloop:=2'  init='2'>
    </define:variable>
    <select:event :name='loop'>
        <define:guard>
            pcloop = 1
        </define:guard>
        <define:action variable='pcloop' style=':='>
            pcloop−1
        </define:action>
    </select:event>
    <define:event name='loop1'>
        <define:guard>
            pcloop = 2
        </define:guard>
        <define:guard>
            pc = 4
        </define:guard>
        <define:action variable='pcloop' style=':='>
            pcloop−1
        </define:action>
    </define:event>
</system>Compare this to the FlowNewSequence. The effect of application of these patterns to the fourth
refinement step is identical. However, a captured pattern is most likely inapplicable to any other machine.

Dealing with problem patterns

If a pattern is invalid (has broken XML syntax) it is not shown in the refinement wizard. However, it can be selected in using the Patterns/Edit menu where it should appear in the Broken category:



Pattern description is temprorarily replaced with an error message.