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