No edit summary |
|||
| (3 intermediate revisions by the same user not shown) | |||
| Line 4: | Line 4: | ||
=== Background === | === Background === | ||
The ProB | 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 === | ||
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. | ||
Conceptually, the state space is completely there and completely evaluated. When you access a state within 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 | |||
== Trace == | == Trace == | ||
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.
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.
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.