ProB API - Revision history

imported>Mathieu: Category:ProBCategory:Developer documentation

2009-02-04T08:20:25Z

Category:ProB Category:Developer documentation

← Older revision		Revision as of 08:20, 4 February 2009
Line 65:		Line 65:
	state = new State(stateId, initialised, invariantKo, timeoutOccured,maxOperationReached, stateValues, enabledOperations, errors);		state = new State(stateId, initialised, invariantKo, timeoutOccured,maxOperationReached, stateValues, enabledOperations, errors);
	}		}

			[[Category:ProB]]
			[[Category:Developer documentation]]

imported>Jens at 08:08, 4 February 2009

2009-02-04T08:08:03Z

← Older revision		Revision as of 08:08, 4 February 2009
Line 36:		Line 36:
	* Creates a tree structure representing the term		* Creates a tree structure representing the term
	** Convenient to create Data-Objects from a term		** Convenient to create Data-Objects from a term

			==Command Example==
			* Direct usage of Prolog API
			* Getting the ID of the current state

			public final static String COMMAND =
			new PrologTermStringOutput().openTerm("getCurrentStateID").
			printVariable("ID").closeTerm().fullstop().toString();

			public void execute(Animator animator,IServerConnection connector) throws CoreException {
			synchronized (id) {
			Map<String, PrologTerm> bindings = BindingGenerator.createBinding(connector.sendCommand(COMMAND));
			if (bindings == null) throw new CoreException("Prolog query failed.");
			id = bindings.get("ID").toString();
			}
			}

			* Getting state information using other commands

			public synchronized void execute(final Animator animator,final IServerConnection connector) throws CoreException {

			final List<Operation> enabledOperations = GetEnabledOperationsCommand.getOperations(animator, stateId);

			final StateValuesResult stateValues = GetStateValuesCommand.getStateValues(animator, stateId);

			// [...] some more Command calls

			state = new State(stateId, initialised, invariantKo, timeoutOccured,maxOperationReached, stateValues, enabledOperations, errors);
			}

imported>Jens at 08:00, 4 February 2009

2009-02-04T08:00:45Z

← Older revision		Revision as of 08:00, 4 February 2009
Line 28:		Line 28:

	[[Image:Prob api1.png]]		[[Image:Prob api1.png]]

			== Communication API ==
			* Builder to create well formed Prolog Queries
			* Communication Interface to send Queries to ProB
			** Hides possible distributed calculation, i.e. "feels" like having a single ProB
			* Parses the result from ProB (i.e. a Prolog term)
			* Creates a tree structure representing the term
			** Convenient to create Data-Objects from a term

imported>Jens at 07:59, 4 February 2009

2009-02-04T07:59:19Z

← Older revision		Revision as of 07:59, 4 February 2009
Line 26:		Line 26:
	== Using the API ==		== Using the API ==
	Most Commands have a static method to create and execute an instance in a single method call		Most Commands have a static method to create and execute an instance in a single method call

	[[Image:Prob api1.png]]		[[Image:Prob api1.png]]

imported>Jens at 07:56, 4 February 2009

2009-02-04T07:56:48Z

← Older revision		Revision as of 07:56, 4 February 2009
Line 26:		Line 26:
	== Using the API ==		== Using the API ==
	Most Commands have a static method to create and execute an instance in a single method call		Most Commands have a static method to create and execute an instance in a single method call
			[[Image:Prob api1.png]]

imported>Jens: New page: = ProB API = ==Animator== * Animator represents one run of ProB * Currently: At most one Animator per file (might change) * Each animator has at least one corresponding probcli * Gettin...

2009-02-04T07:54:16Z

New page: = ProB API = ==Animator== * Animator represents one run of ProB * Currently: At most one Animator per file (might change) * Each animator has at least one corresponding probcli * Gettin...

New page

= ProB API =

==Animator==
* Animator represents one run of ProB
* Currently: At most one Animator per file (might change)
* Each animator has at least one corresponding probcli
* Getting the Animator associated with a file: AnimatorRegistry.getAnimator(file)

==ICommand==
* A Command encapsulate a sequence of ProB (Prolog) queries
* Commands can be composed from other Commands, e.g. Exploring a state
** Get enabled events
**Get values for constants and variables
** Get other properties (Invariant violation, Timeout, ...)
''Note: Exploration could also be implemented by a sequence of Prolog Queries. This is a design decision that depends on whether we want to reuse parts of the sequence or not''

== Some implemented basic commands ==
* Load Machine
* Explore a State (i.e. calculate sucessors, invariant, ...)
* Execute (i.e. observe) an Event
* Evaluate an Expression or Predicate
* Consistency Checking
* LTL Model Checking

== Using the API ==
Most Commands have a static method to create and execute an instance in a single method call