At the moment, pGCL, the probabilistic guarded command langage, is the only supported frontend.
We have a tool,
pgcl2heyvl, that automatically generates HeyVL code from pGCL programs.
Most of pGCL's syntax can be encoded in fairly straightforward manner, but loops are a bit more complicated and require additional user annotations (loop invariants). The tool supports both Park induction and the more general k-induction.
pgcl2heyvl is a Python program that reads a pGCL program from a file and uses additional user-provided annotations to encode loops.
The output is a HeyVL file.
poetry run pgcl2heyvl FILE --post POST --pre PRE --k K > OUTFILE
FILE is a file name with the pGCL program,
POST is a post-expectation, and
PRE is a pre-expectation (in pGCL syntax).
K argument is an integer that specifies which
k-induction to use for the encoding.
OUTFILE is the name of the output file with the HeyVL code.
If the pGCL program includes a single loop, then
PRE will be used as the loop invariant.
When the program includes multiple loops, additional invariants must be specified using
If the input file starts with a comment
// ARGS: followed by command-line arguments, it will use these as defaults.
The command-line interface documentation is available by invoking
poetry run pgcl2heyvl --help.
And yes, we're aware the user experience of this tool is particularly horrible. We're working on it!
You can find pGCL examples in the
They include all necessary parameters to generate verifying HeyVL files.
For these examples, the generated HeyVL files are located under
caesar requires the
--raw command-line flag since these files are just sequences of HeyVL statements.
Instructions on how to (re-)generate these examples are located in
caesar with the generated HeyVL files, refer to the benchmarks section of Caesar's documentation.
pgcl2heyvl uses the
probably Python library to parse and type-check pGCL programs.
That means the pGCL syntax of
probably is used for the pGCL programs and the
--invariant command-line parameters.
There is no formal specification for the exact pGCL syntax that
probably accepts, but here are some pointers: