ProB API

From Event-B
Jump to navigationJump to search

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

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);
 }