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