Difference between revisions of "Accessing Proof Obligations"
From Event-B
Jump to navigationJump to searchimported>Maria (New page: ==File Types== For each machine and each context there exists one of each of the following files: *IPSFile (.bps): This file contains the statuses (IPSStatus) of the proof obligations. *...) |
imported>Maria |
||
| Line 10: | Line 10: | ||
If one has any of these files, one get the others though the functions <code>getMachineFile()</code>, <code>getContextFile()</code>, <code>getPSFile()</code> and <code>getPOFile()</code>. | If one has any of these files, one get the others though the functions <code>getMachineFile()</code>, <code>getContextFile()</code>, <code>getPSFile()</code> and <code>getPOFile()</code>. | ||
| − | == Accessing the sequents of an IPOFile == | + | ==Accessing the sequents of an IPOFile== |
*All sequents of ''file'': <code>IPOSequent[] sequents = file.getSequents()</code> | *All sequents of ''file'': <code>IPOSequent[] sequents = file.getSequents()</code> | ||
*A specific sequent (e.g. INITIALISATION/inv1/INV) of ''file'': <code>IPOSequent sequent = file.getSequent("INITIALISATION/inv1/INV")</code> | *A specific sequent (e.g. INITIALISATION/inv1/INV) of ''file'': <code>IPOSequent sequent = file.getSequent("INITIALISATION/inv1/INV")</code> | ||
| − | == Accessing the statuses of an IPSFile == | + | ==Accessing the statuses of an IPSFile == |
*All statuses of ''file'': <code>IPSStatus[] statuses = file.getStatuses()</code> | *All statuses of ''file'': <code>IPSStatus[] statuses = file.getStatuses()</code> | ||
*A specific status (e.g. INITIALISATION/inv1/INV) of ''file'': <code>IPSStatus status = file.getStatus("INITIALISATION/inv1/INV")</code> | *A specific status (e.g. INITIALISATION/inv1/INV) of ''file'': <code>IPSStatus status = file.getStatus("INITIALISATION/inv1/INV")</code> | ||
==Finding the corresponding status to a sequent== | ==Finding the corresponding status to a sequent== | ||
| − | *1. Find the IPOFile that contains ''sequent'': <code>IPOFile | + | *1. Find the IPOFile that contains ''sequent'': <code>IPOFile poFile = sequent.getAncestor(IPOFile.ELEMENT_TYPE);</code> |
| − | *2. Find the matching IPSFile: <code>IPSFile | + | *2. Find the matching IPSFile: <code>IPSFile isFile = poFile.getPSFile();</code> |
| − | *3. Find the machting status: <code>IPSStatus status = | + | *3. Find the machting status: <code>IPSStatus status = psFile.getStatus(sequent.getElementName);</code> |
==Accessing all proof obligations of a project== | ==Accessing all proof obligations of a project== | ||
| Line 27: | Line 27: | ||
*All IPSFiles of ''project'': <code>IPSFile[] psfiles = project.getChildrenOfType(IPSFile.ELEMENT_TYPE);</code> | *All IPSFiles of ''project'': <code>IPSFile[] psfiles = project.getChildrenOfType(IPSFile.ELEMENT_TYPE);</code> | ||
| − | |||
| − | |||
==Accessing the proof obligations of a given machine or context== | ==Accessing the proof obligations of a given machine or context== | ||
| + | *1. Find the machting IPOFile for ''machine'' (IMachineFile): <code>IPOFile poFile = machine.getPOFile();</code> | ||
| + | *2. Get all sequents: [[Accessing_Proof_Obligations#Accessing_the_sequents_of_an_IPOFile | Accessing the sequents of an IPOFile]] | ||
| + | *1. Find the machting IPSFile for ''machine'': <code>IPSFile psFile = machine.getPSFile();</code> | ||
| + | *3. For each sequent access the status with the same name in the IPSFile: [[Accessing_Proof_Obligations#Accessing_the_statuses_of_an_IPSFile | Accessing the statuses of an IPSFile]] | ||
Revision as of 11:49, 16 September 2008
Contents
File Types
For each machine and each context there exists one of each of the following files:
- IPSFile (.bps): This file contains the statuses (IPSStatus) of the proof obligations.
- IPOFile (.bpo): This file contains the sequents (IPOSequent) of the proof obligations.
The Connection
An IPSFile, an IPOFile and an IMachineFile or IContextFile are connected through the name. For example machine m0 has IMachineFile m0.bum, IPSFile m0.bps and IPOFile m0.bpo. The name of each of these files is accessible via file.getBarName().
If one has any of these files, one get the others though the functions getMachineFile(), getContextFile(), getPSFile() and getPOFile().
Accessing the sequents of an IPOFile
- All sequents of file:
IPOSequent[] sequents = file.getSequents() - A specific sequent (e.g. INITIALISATION/inv1/INV) of file:
IPOSequent sequent = file.getSequent("INITIALISATION/inv1/INV")
Accessing the statuses of an IPSFile
- All statuses of file:
IPSStatus[] statuses = file.getStatuses() - A specific status (e.g. INITIALISATION/inv1/INV) of file:
IPSStatus status = file.getStatus("INITIALISATION/inv1/INV")
Finding the corresponding status to a sequent
- 1. Find the IPOFile that contains sequent:
IPOFile poFile = sequent.getAncestor(IPOFile.ELEMENT_TYPE); - 2. Find the matching IPSFile:
IPSFile isFile = poFile.getPSFile(); - 3. Find the machting status:
IPSStatus status = psFile.getStatus(sequent.getElementName);
Accessing all proof obligations of a project
- All IPOFiles of project:
IPOFile[] pofiles = project.getChildrenOfType(IPOFile.ELEMENT_TYPE);
- All IPSFiles of project:
IPSFile[] psfiles = project.getChildrenOfType(IPSFile.ELEMENT_TYPE);
Accessing the proof obligations of a given machine or context
- 1. Find the machting IPOFile for machine (IMachineFile):
IPOFile poFile = machine.getPOFile(); - 2. Get all sequents: Accessing the sequents of an IPOFile
- 1. Find the machting IPSFile for machine:
IPSFile psFile = machine.getPSFile(); - 3. For each sequent access the status with the same name in the IPSFile: Accessing the statuses of an IPSFile
