ProB API

From Event-B
Revision as of 07:54, 4 February 2009 by 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...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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