Programmatic Abstractions in the ProB 2.0 API - Revision history

Joy Clark: /* StateSpace */

2014-11-05T14:47:58Z

StateSpace

← Older revision		Revision as of 14:47, 5 November 2014
Line 20:		Line 20:

	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 ==

Joy Clark: /* Model */

2014-11-05T14:40:15Z

Model

← Older revision		Revision as of 14:40, 5 November 2014
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 ==

Joy Clark: /* Overview */

2014-11-05T14:38:21Z

Overview

← Older revision		Revision as of 14:38, 5 November 2014
Line 7:		Line 7:

	=== 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 ==

Joy Clark: /* Background */

2014-11-05T14:34:09Z

Background

← Older revision		Revision as of 14:34, 5 November 2014
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 ===

Lukas Ladenberger at 15:29, 30 October 2014

2014-10-30T15:29:55Z

← Older revision		Revision as of 15:29, 30 October 2014
Line 1:		Line 1:
			[[Category:ProB Java API]]

	== Overview ==		== Overview ==

Joy Clark at 11:57, 4 June 2013

2013-06-04T11:57:19Z

← Older revision		Revision as of 11:57, 4 June 2013
Line 24:		Line 24:
	The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.		The StateSpace object is actually mutable, but it is always growing. No data ever gets replaced by any new data.

	== ~~History~~ ==		== 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 ~~History~~ provides this abstraction.		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.

	~~The History~~ 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 ~~History~~ behaves like a browser history; it is possible to move forward and backward within the current trace.		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.

	~~And important concept to understand when considering the History is that the idea of a "history" is in this sense equivalent with the concept of an "animation".~~ A ~~History~~ corresponds to exactly one animation ~~trace~~. Each ~~History~~ is associated with exactly one StateSpace, but we can have many different ~~History~~ objects on top of a single StateSpace.		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 ~~History~~ is immutable. This means that whenever an animation step is performed (forward, backward, or simply adding a transition to the trace) a new ~~History~~ is returned.		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.

Joy Clark: /* History */

2012-11-30T10:23:12Z

History

← Older revision		Revision as of 10:23, 30 November 2012
Line 25:		Line 25:

	== History ==		== History ==

			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 History provides this abstraction.

			The History 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 History behaves like a browser history; it is possible to move forward and backward within the current trace.

			And important concept to understand when considering the History is that the idea of a "history" is in this sense equivalent with the concept of an "animation". A History corresponds to exactly one animation trace. Each History is associated with exactly one StateSpace, but we can have many different History objects on top of a single StateSpace.

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

Joy Clark: /* StateSpace */

2012-11-30T10:10:30Z

StateSpace

← Older revision		Revision as of 10:10, 30 November 2012
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 ==

Joy Clark: /* Model */

2012-11-30T10:05:05Z

Model

← Older revision		Revision as of 10:05, 30 November 2012
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 ==

Joy Clark: /* Overview */

2012-11-30T09:48:41Z

Overview

← Older revision		Revision as of 09:48, 30 November 2012
Line 5:		Line 5:

	=== 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 the ProB ~~model~~		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.

	== Model ==		== Model ==