(→Model) |
|||
| Line 16: | Line 16: | ||
== 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. | |||
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. | |||
== History == | == History == | ||
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 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.
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.
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.