(→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 == | ||
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.
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.
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.
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.
The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.
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.