# Accessing Proof Obligations

## File Types

For each machine and each context there exists one of each of the following roots:

- IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps.

- IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.

## The Connection between different root types

An IPSRoot, an IPORootand an IMachineRoot or IContextRoot are connected through the name. For example machine *m0* has IMachineRoot that is in file *m0.bum*, IPSRoot in *m0.bps* and IPORoot in *m0.bpo*. If one has any of these roots, one get the others though the functions `getMachineRoot()`

, `getContextRoot()`

, `getPSRoot()`

and `getPORoot()`

.

## Accessing the sequents of an IPORoot

- All sequents of
*root*:`IPOSequent[] sequents = root.getSequents()`

- A specific sequent (e.g. INITIALISATION/inv1/INV) of
*root*:`IPOSequent sequent = root.getSequent("INITIALISATION/inv1/INV")`

## Accessing the statuses of an IPSRoot

- All statuses of
*root*:`IPSStatus[] statuses = root.getStatuses()`

- A specific status (e.g. INITIALISATION/inv1/INV) of
*root*:`IPSStatus status = root.getStatus("INITIALISATION/inv1/INV")`

## Finding the corresponding status to a given sequent

- 1. Find the IPORoot that contains
*sequent*:`IPORoot poRoot = sequent.getParent;`

- 2. Find the matching IPSRoot:
`IPSRoot psRoot = poRoot.getPSRoot();`

- 3. Find the machting status:
`IPSStatus status = psRoot.getStatus(sequent.getElementName);`

## Finding the corresponding sequent to a given status

Use the function `getPOSequent()`

in IPSStatus.

## Accessing the proof obligations of a given machine or context

- 1. Find the machting IPORoot for
*machine*(IMachineRoot):`IPORoot poRoot = machine.getPORoot();`

- 2. Get all sequents: Accessing the sequents of an IPORoot
- 1. Find the machting IPSFile for
*machine*:`IPSFile psFile = machine.getPSFile();`

- 3. For each sequent access the status with the same name in the IPSRoot: Accessing the statuses of an IPSRoot

## The sources of a proof obligations

The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).
They can be accessed from the IPOSequent: `IPOSource[] sources = sequents[i].getSources();`

An IPOSource can be an instance of an element like IInvariant, ITheorem etc or it can be an IAction, IWitness or IGuard.

## Finding all the proof obligations for a given Invariant

It is not possible to directly find the proof obligations for a given invariant or any other element. Instead check if the sources of the proof obligations contain the invariant.