Difference between revisions of "ProB API"
From Event-B
Jump to navigationJump to searchimported>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...) |
imported>Mathieu |
||
(4 intermediate revisions by one other user not shown) | |||
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]] | ||
+ | |||
+ | == 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 | ||
+ | |||
+ | ==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); | ||
+ | } | ||
+ | |||
+ | [[Category:ProB]] | ||
+ | [[Category:Developer documentation]] |
Latest revision as of 08:20, 4 February 2009
Contents
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
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
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); }