3.6 Deploy Theory

If the theory is deemed sound (i.e., all proof obligations are discharged), it can be deployed to be used by models (i.e., Event-B contexts and machines). A theory can be deployed as follows:

Select the theory you want to deploy.
right-click on the theory in the Event-B explorer, then click on Deploy.
the following wizard shows up:

$\includegraphics{Deploy.png}$
Figure 8: Deploy Theory Wizard
if you check the button, the workspace will be rebuilt if the deployment is successful. A workspace rebuild is desirable to reflect any potential changes to the mathematical language.
you can finish, or proceed to the next page which looks like the following:

$\includegraphics{DeployPage2.png}$
Figure 9: Deploy Theory Wizard - Info Page
if the theory is successfully deployed, the following message is displayed:

$\includegraphics{DeploySuc.png}$
Figure 10: Deploy Theory - Success

Note that theories in the Event-B Explorer may have three different icons:

$\includegraphics{thy.png}$ signifies that theory is not deployed (does not have a deployed counterpart).
$\includegraphics{thyDep.png}$ signifies that theory is deployed (has a deployed counterpart).
$\includegraphics{thy-outdated.png}$ signifies that theory has been deployed, but changes has been made to the theory since.