Running Pegasus separately
Using Pegasus as a standalone tool can be achieved by navigating to
keymaerax-core/src/main/resources/Pegasus inside the folder containing the KeYmaera X source directory. The file
Pegasus.m serves as the main package from which invariant generation strategies may be called. Various examples of invariant generation using this file are contained in the
Tests/ sub-folder. Keep in mind that by running Pegasus separately using Mathematica one only obtains
invariant candidates, whereas KeYmaera X additionally
formally proves the invariance property of these candidates.
In Mathematica, an input problem for Pegasus takes the form of a continuous Hoare triple:
{precondition, {vector_field, state_variables, evolution_constraint}, postcondition}
where
precondition,
postcondition and
evolution_constraint are first-order formulas of real arithmetic,
state_variables is a finite list of the system's state variables (e.g.
{x,y,z}), and
vector_field is a list of equal size containing polynomials in those variables (corresponding to the right-hand side of the system of ODEs). For instance, when calling from a notebook file in the
Test/ sub-folder in the Pegasus main directory:
| In[1] = SetDirectory[ParentDirectory[NotebookDirectory[]]] |
| In[2] = Needs["Pegasus`", FileNameJoin[{Directory[], "Pegasus.m"}]] |
| In[3] = InvGen[{(-2 + x)^2 + y^2 <= 1/5 || (2 + x)^2 + (-2 + y)^2 <= 1/3, {{-4 y, x}, {x, y}, True}, y <= 4 && y >= -4 && x^2 + y^2 > 1/3}] |
In the illustration of this verification problem below, the unsafe sets are shown in light red and the initial states in light green:
The output is a nested list, whose
first formal entry is the invariant candidate (other entries in the list serve to facilitate proof construction within KeYmaera X and may be ignored when using Pegasus separately).
Out[4] = {{106345581/44105831 < x^2+4 y^2 < 784012261/25449817,{{x^2+4 y^2 < 784012261/25449817,kyx`ProofHint==kyx`FirstIntegral},{x^2+4 y^2 > 106345581/44105831,kyx`ProofHint==kyx`FirstIntegral}}},True}
When drawn, the invariant looks as follows (shown in light blue):
