Difference between revisions of "ProB API"

From Event-B
Jump to navigationJump to search
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...)
 
imported>Jens
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]]

Revision as of 07:56, 4 February 2009

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