Programmatic Abstractions in the ProB 2.0 API: Difference between revisions

No edit summary
 
(3 intermediate revisions by the same user not shown)
Line 4: Line 4:


=== Background ===
=== Background ===
The ProB 1.0 API takes advantage of one basic abstraction: developers can create Java commands that can be sent to the prolog kernel where something will be calculated. The result can then be used by the developer. Each Java command corresponds to one prolog command in the ProB kernel.
The original ProB plug-in for Rodin introduced one basic abstraction: developers can create Java commands specifying calculations that are to be made by the ProB CLI binary. The result that is calculated by ProB can then be interpreted and manipulated by the developer. Each Java command corresponds to one prolog instruction in the ProB kernel.


=== Current Implementation ===
=== Current Implementation ===
The developer is still able to use commands in order to get information from the prolog kernel. But as we were considering how the ProB core should be structured, we realized that many commands may be used over and over again in the same (or very similar) concepts. Therefore, we created the programmatic abstractions that will be described in the following sections.
We have maintained the abstractions of the commands in order to communicate with the ProB kernel. However, as we were considering how the ProB core should be structured, we realized that many commands may be used over and over again in the same (or very similar) concepts. Therefore, we created the programmatic abstractions that will be described in the following sections.


== Model ==
== Model ==
Line 15: Line 15:
This abstraction is available so that it is possible to have access to the static information about the model during an animation without having to contact ProB directly.  
This abstraction is available so that it is possible to have access to the static information about the model during an animation without having to contact ProB directly.  


Currently, the Model abstraction is implemented for the Classical B and Event B formalisms. But because we have implemented the abstraction with other formalisms in mind, it should not be difficult to implement new formalisms.
Currently, the Model abstraction is implemented for the Classical B and Event B formalisms. But because we have implemented the abstraction with other formalisms in mind, it should not be difficult to implement new formalisms. We have also implemented a Model abstraction for CSP-M specifications, but it is currently not possible to access any static information about the model. TLA+ specifications can be represented in the API as Classical B models.


== StateSpace ==
== StateSpace ==


There is a one-to-one relationship between a StateSpace and a model. The StateSpace is the corresponding label transition system for a particular model.  
There is a one-to-one relationship between a StateSpace and a model. The StateSpace is the corresponding label transition system for a particular model.  
It is actually implemented as a graph (using the JGraphT library), so there are built in graph functions and support for graphical representations. In the graph, the vertices are states and the edges are events (including solutions and choices for local variables and non-deterministic assignments).


Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace that has not yet been explored, ProB will fetch the information from Prolog automatically and transparently. The only observation that can be made is that the fetching of some states takes longer than the ones that are already "cached" in the StateSpace.
Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace, ProB will fetch the information from Prolog automatically and transparently. The only observation that can be made is that the fetching of some states takes longer than the ones that are already "cached" in the StateSpace. For performance reasons, not all states in the state space are saved indefinitely. The states in the StateSpace are saved as State objects, which then hold the information about the outgoing transitions and formulas of interest that have been evaluated for the given state. In the StateSpace, these objects are cached in an LRU cache so that if not accessed for a given period of time, the garbage collector can clean them up.
 
The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.


== Trace ==
== Trace ==

Latest revision as of 14:47, 5 November 2014


Overview

Background

The original ProB plug-in for Rodin introduced one basic abstraction: developers can create Java commands specifying calculations that are to be made by the ProB CLI binary. The result that is calculated by ProB can then be interpreted and manipulated by the developer. Each Java command corresponds to one prolog instruction in the ProB kernel.

Current Implementation

We have maintained the abstractions of the commands in order to communicate with the ProB kernel. However, as we were considering how the ProB core should be structured, we realized that many commands may be used over and over again in the same (or very similar) concepts. Therefore, we created the programmatic abstractions that will be described in the following sections.

Model

The Model is an abstraction that provides static information about the current model that is being animated or checked. For Classical B and Event B, this includes all of the information about the refinement chain and all of the different components (Machines, Contexts, Invariants, Variables, etc.).

This abstraction is available so that it is possible to have access to the static information about the model during an animation without having to contact ProB directly.

Currently, the Model abstraction is implemented for the Classical B and Event B formalisms. But because we have implemented the abstraction with other formalisms in mind, it should not be difficult to implement new formalisms. We have also implemented a Model abstraction for CSP-M specifications, but it is currently not possible to access any static information about the model. TLA+ specifications can be represented in the API as Classical B models.

StateSpace

There is a one-to-one relationship between a StateSpace and a model. The StateSpace is the corresponding label transition system for a particular model.

Conceptually, the state space is completely there and completely evaluated. When you access a state within the StateSpace, ProB will fetch the information from Prolog automatically and transparently. The only observation that can be made is that the fetching of some states takes longer than the ones that are already "cached" in the StateSpace. For performance reasons, not all states in the state space are saved indefinitely. The states in the StateSpace are saved as State objects, which then hold the information about the outgoing transitions and formulas of interest that have been evaluated for the given state. In the StateSpace, these objects are cached in an LRU cache so that if not accessed for a given period of time, the garbage collector can clean them up.

Trace

For some tools, the StateSpace abstraction may be sufficient. But when it comes to animation and the concept of a "current state", a further abstraction becomes necessary. The Trace provides this abstraction.

A Trace consists of a linked list of states which correspond to a path through the StateSpace. There is also a pointer in the list which identifies the current state. The Trace behaves like a browser history; it is possible to move forward and backward within the current trace.

A Trace corresponds to exactly one trace within the animation. Each Trace is associated with exactly one StateSpace, but we can have many different Trace objects on top of a single StateSpace.

The Trace is immutable. This means that whenever an animation step is performed (forward, backward, or simply adding a transition to the trace) a new Trace is returned.