ProB API

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